Commit fc59d6d0 authored by Ralf Jung's avatar Ralf Jung

fix nits

parent 7fa7361b
...@@ -22,6 +22,6 @@ Proof. ...@@ -22,6 +22,6 @@ Proof.
iMod (gen_heap_init σ.(heap)) as (?) "Hh". iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init κs σ.(used_proph)) as (?) "Hp". iMod (proph_map_init κs σ.(used_proph)) as (?) "Hp".
iModIntro. iModIntro.
iExists (fun σ κs => (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph))%I). iFrame. iExists (λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph))%I). iFrame.
iApply (Hwp (HeapG _ _ _ _)). iApply (Hwp (HeapG _ _ _ _)).
Qed. Qed.
...@@ -176,7 +176,6 @@ Record state : Type := { ...@@ -176,7 +176,6 @@ Record state : Type := {
heap: gmap loc val; heap: gmap loc val;
used_proph: gset proph; used_proph: gset proph;
}. }.
Implicit Type σ : state.
(** Equality and other typeclass stuff *) (** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v. Lemma to_of_val v : to_val (of_val v) = Some v.
......
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic. From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par. From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(** Nondeterminism and Speculation: (** Nondeterminism and Speculation:
...@@ -11,31 +9,33 @@ Set Default Proof Using "Type". ...@@ -11,31 +9,33 @@ Set Default Proof Using "Type".
Logical Relations for Fine-Grained Concurrency by Turon et al. (POPL'13) *) Logical Relations for Fine-Grained Concurrency by Turon et al. (POPL'13) *)
Definition rand: val := Definition rand: val :=
λ: "_", λ: "_",
let: "y" := ref #false in let: "y" := ref #false in
Fork ("y" <- #true) ;; Fork ("y" <- #true) ;;
!"y". !"y".
Definition earlyChoice: val := Definition earlyChoice: val :=
λ: "x", λ: "x",
let: "r" := rand #() in let: "r" := rand #() in
"x" <- #0 ;; "x" <- #0 ;;
"r". "r".
Definition lateChoice: val := Definition lateChoice: val :=
λ: "x", λ: "x",
let: "p" := NewProph in let: "p" := NewProph in
"x" <- #0 ;; "x" <- #0 ;;
let: "r" := rand #() in let: "r" := rand #() in
resolve_proph: "p" to: "r" ;; resolve_proph: "p" to: "r" ;;
"r". "r".
Section coinflip. Section coinflip.
Context `{!heapG Σ} (N: namespace). Context `{!heapG Σ}.
Local Definition N := nroot .@ "coin".
Lemma rand_spec : Lemma rand_spec :
{{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}. {{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
Proof using N. Proof.
iIntros (Φ) "_ HP". iIntros (Φ) "_ HP".
wp_lam. wp_alloc l as "Hl". wp_lam. wp_lam. wp_alloc l as "Hl". wp_lam.
iMod (inv_alloc N _ ( (b: bool), l #b)%I with "[Hl]") as "#Hinv"; first by eauto. iMod (inv_alloc N _ ( (b: bool), l #b)%I with "[Hl]") as "#Hinv"; first by eauto.
...@@ -50,7 +50,7 @@ Section coinflip. ...@@ -50,7 +50,7 @@ Section coinflip.
earlyChoice #x earlyChoice #x
@ @
<<< (b: bool), x #0, RET #b >>>. <<< (b: bool), x #0, RET #b >>>.
Proof using N. Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam. iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_bind (rand _)%E. iApply rand_spec; first done. wp_bind (rand _)%E. iApply rand_spec; first done.
iIntros (b) "!> _". wp_let. iIntros (b) "!> _". wp_let.
...@@ -62,7 +62,7 @@ Section coinflip. ...@@ -62,7 +62,7 @@ Section coinflip.
iModIntro. wp_seq. done. iModIntro. wp_seq. done.
Qed. Qed.
Definition val_to_bool v : bool := Definition val_to_bool (v : option val) : bool :=
match v with match v with
| Some (LitV (LitBool b)) => b | Some (LitV (LitBool b)) => b
| _ => true | _ => true
...@@ -73,7 +73,7 @@ Section coinflip. ...@@ -73,7 +73,7 @@ Section coinflip.
lateChoice #x lateChoice #x
@ @
<<< (b: bool), x #0, RET #b >>>. <<< (b: bool), x #0, RET #b >>>.
Proof using N. Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam. iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_apply wp_new_proph; first done. wp_apply wp_new_proph; first done.
iIntros (v p) "Hp". iIntros (v p) "Hp".
......
...@@ -8,7 +8,6 @@ Definition proph_map (P V : Type) `{Countable P} := gmap P (option V). ...@@ -8,7 +8,6 @@ Definition proph_map (P V : Type) `{Countable P} := gmap P (option V).
Definition proph_val_list (P V : Type) := list (P * V). Definition proph_val_list (P V : Type) := list (P * V).
Section first_resolve. Section first_resolve.
Context {P V : Type} `{Countable P}. Context {P V : Type} `{Countable P}.
Implicit Type pvs : proph_val_list P V. Implicit Type pvs : proph_val_list P V.
Implicit Type p : P. Implicit Type p : P.
...@@ -132,7 +131,6 @@ Section to_proph_map. ...@@ -132,7 +131,6 @@ Section to_proph_map.
End to_proph_map. End to_proph_map.
Lemma proph_map_init `{proph_mapPreG P V PVS} pvs ps : Lemma proph_map_init `{proph_mapPreG P V PVS} pvs ps :
(|==> _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I. (|==> _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
Proof. Proof.
......
...@@ -97,11 +97,11 @@ Ltac of_expr e := ...@@ -97,11 +97,11 @@ Ltac of_expr e :=
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(CAS e0 e1 e2) constr:(CAS e0 e1 e2)
| heap_lang.FAA ?e1 ?e2 => | heap_lang.FAA ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2) let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
| heap_lang.NewProph => | heap_lang.NewProph =>
constr:(NewProph) constr:(NewProph)
| heap_lang.ResolveProph ?e1 ?e2 => | heap_lang.ResolveProph ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(ResolveProph e1 e2) let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(ResolveProph e1 e2)
| to_expr ?e => e | to_expr ?e => e
| of_val ?v => constr:(Val v (of_val v) (to_of_val v)) | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
| language.of_val ?v => constr:(Val v (of_val v) (to_of_val v)) | language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
......
...@@ -12,6 +12,6 @@ Proof. ...@@ -12,6 +12,6 @@ Proof.
iMod (gen_heap_init σ.(heap)) as (?) "Hh". iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init [] σ.(used_proph)) as (?) "Hp". iMod (proph_map_init [] σ.(used_proph)) as (?) "Hp".
iModIntro. iModIntro.
iExists (fun σ κs => (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph))%I). iFrame. iExists (λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph))%I). iFrame.
iApply (Hwp (HeapG _ _ _ _)). iApply (Hwp (HeapG _ _ _ _)).
Qed. Qed.
...@@ -187,15 +187,15 @@ Proof. ...@@ -187,15 +187,15 @@ Proof.
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs). iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs).
rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)". rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]". iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); last first. iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); first by eauto.
rewrite app_nil_r. all: eauto with iFrame. rewrite app_nil_r. eauto with iFrame.
- destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?. - destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
eapply (soundness (M:=iResUR Σ) _ (S (S n))). eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs). iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs).
rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)". rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]". iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv Istate) _ _ _ []); last first. iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv Istate) _ _ _ []); [by eauto..|].
rewrite app_nil_r. all: eauto with iFrame. rewrite app_nil_r. eauto with iFrame.
Qed. Qed.
Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ : Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
......
...@@ -110,12 +110,12 @@ Section language. ...@@ -110,12 +110,12 @@ Section language.
option_list x ++ xs. option_list x ++ xs.
Inductive nsteps : nat cfg Λ list (observation Λ) cfg Λ Prop := Inductive nsteps : nat cfg Λ list (observation Λ) cfg Λ Prop :=
| nsteps_refl ρ : | nsteps_refl ρ :
nsteps 0 ρ [] ρ nsteps 0 ρ [] ρ
| nsteps_l n ρ1 ρ2 ρ3 κ κs : | nsteps_l n ρ1 ρ2 ρ3 κ κs :
step ρ1 κ ρ2 step ρ1 κ ρ2
nsteps n ρ2 κs ρ3 nsteps n ρ2 κs ρ3
nsteps (S n) ρ1 (cons_obs κ κs) ρ3. nsteps (S n) ρ1 (cons_obs κ κs) ρ3.
Hint Constructors nsteps. Hint Constructors nsteps.
Definition erased_step (ρ1 ρ2 : cfg Λ) := κ, step ρ1 κ ρ2. Definition erased_step (ρ1 ρ2 : cfg Λ) := κ, step ρ1 κ ρ2.
...@@ -174,7 +174,7 @@ Section language. ...@@ -174,7 +174,7 @@ Section language.
Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 : Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
t1 t1' erased_step (t1,σ1) (t2,σ2) t2', t2 t2' erased_step (t1',σ1) (t2',σ2). t1 t1' erased_step (t1,σ1) (t2,σ2) t2', t2 t2' erased_step (t1',σ1) (t2',σ2).
Proof. Proof.
intros* Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder. intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
Qed. Qed.
Record pure_step (e1 e2 : expr Λ) := { Record pure_step (e1 e2 : expr Λ) := {
......
...@@ -190,8 +190,7 @@ Proof. ...@@ -190,8 +190,7 @@ Proof.
rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//. rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
iIntros (σ1 κ κs) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR. iIntros (σ1 κ κs) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
{ destruct s; last done. eauto using reducible_no_obs_reducible. } { destruct s; last done. eauto using reducible_no_obs_reducible. }
iIntros (e2 σ2 efs Hstep). iMod ("H" $! _ _ _ _ Hstep) as "(% & Hst & H & Hfork)". iIntros (e2 σ2 efs Hstep). iMod ("H" $! _ _ _ _ Hstep) as "(-> & $ & H & Hfork)".
subst κ. iFrame "Hst".
iApply step_fupd_intro; [set_solver+|]. iNext. iApply step_fupd_intro; [set_solver+|]. iNext.
iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]"). iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
iIntros "!#" (k e' _) "H". by iApply "IH". iIntros "!#" (k e' _) "H". by iApply "IH".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment