Commit 11948e6e by Dan Frumin

### Twiggle the notation

- Use the type of literals in `val`
- Notation for `match`
- "Better" coercions
parent 722c917b
 ... ... @@ -7,14 +7,14 @@ Definition bitτ : type := (TVar 0))). Definition bit_bool : val := PackV ((λ: "b", "b"), (λ: "b", BinOp Xor "b" (#♭v true)), #♭v true). PackV ((λ: "b", "b"), (λ: "b", "b" ⊕ true), #♭v true). Definition flip_nat : val := λ: "n", if: BinOp Eq "n" (#n 0) then (#n 1) else (#n 0). if: "n" = 0 then 1 else 0. Definition bit_nat : val := PackV ((λ: "b", BinOp Eq "b" (#n 0)), flip_nat, #nv 0). PackV ((λ: "b", "b" = 0), flip_nat, #nv 0). Lemma bit_bool_type Γ : typed Γ bit_bool bitτ. ... ...
 ... ... @@ -8,13 +8,13 @@ From iris.program_logic Require Import adequacy. From iris_logrel.F_mu_ref_conc Require Import hax. Definition rand : val := λ: <>, let: "y" := (ref (#♭ false)) in Fork ("y" <- #♭ true);; let: "y" := ref false in Fork ("y" <- true);; !"y". Definition lateChoice : val := λ: "x", "x" <- #n 0;; rand #(). "x" <- 0;; rand (). Definition earlyChoice : val := λ: "x", let: "r" := rand #() in "x" <- #n 0;; "r". let: "r" := rand () in "x" <- 0;; "r". Section Refinement. Context `{logrelG Σ}. ... ... @@ -25,7 +25,7 @@ Section Refinement. (∃ f, y ↦ᵢ (#♭v f) ∗ y' ↦ₛ (#♭v f))%I. Lemma wp_rand : (WP rand #() {{ v, ⌜v = #♭v true⌝ ∨ ⌜v = #♭v false⌝}})%I. (WP rand () {{ v, ⌜v = #♭v true⌝ ∨ ⌜v = #♭v false⌝}})%I. Proof. iStartProof. unfold rand. unlock. ... ... @@ -45,7 +45,7 @@ Section Refinement. Lemma rand_l Δ Γ E1 K ρ t τ : ↑choiceN ⊆ E1 → spec_ctx ρ -∗ (∀ b, {E1,E1;Δ;Γ} ⊨ fill K (#♭ b) ≤log≤ t : τ) -∗ {E1,E1;Δ;Γ} ⊨ fill K (rand #())%E ≤log≤ t : τ. -∗ {E1,E1;Δ;Γ} ⊨ fill K (rand ())%E ≤log≤ t : τ. Proof. iIntros (?) "#Hs Hlog". unfold rand. unlock. simpl. ... ... @@ -79,7 +79,7 @@ Section Refinement. ↑choiceN ⊆ E1 → spec_ctx ρ -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#♭ b) : τ -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (rand #())%E : τ. {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (rand ())%E : τ. Proof. iIntros (??) "#Hs Hlog". unfold rand. unlock. ... ... @@ -104,7 +104,7 @@ Section Refinement. rel_rec_l. rel_store_l. simpl. rel_rec_l. rel_bind_l (rand #())%E. rel_bind_l (rand ())%E. iApply (rand_l with "Hs"); eauto. simpl. by iApply "Hlog". Qed. ... ... @@ -119,7 +119,7 @@ Section Refinement. unfold earlyChoice. unlock. rel_rec_r. rel_bind_r (rand #())%E. rel_bind_r (rand ())%E. iApply (rand_r b with "Hspec"); eauto. simpl. rel_rec_r. rel_store_r. simpl. ... ... @@ -134,7 +134,7 @@ Section Refinement. iIntros "#Hspec Hx Hx'". unfold earlyChoice. unlock. rel_rec_l. rel_bind_l (rand #())%E. rel_bind_l (rand ())%E. iApply (rand_l with "Hspec"); eauto. simpl. iIntros (b). rel_rec_l. ... ... @@ -142,12 +142,12 @@ Section Refinement. rel_rec_r. rel_store_r. simpl. rel_rec_r. rel_bind_r (rand #())%E. rel_bind_r (rand ())%E. iApply (rand_r b with "Hspec"); eauto. simpl. rel_store_l. simpl. rel_rec_l. rel_vals; simpl; eauto. Qed. End Refinement.
 ... ... @@ -3,13 +3,13 @@ From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics. From iris_logrel.F_mu_ref_conc Require Export rules_binary typing fundamental_binary relational_properties notation. From iris.base_logic Require Import namespaces. Definition newlock : val := λ: <>, ref (#♭ false). Definition newlock : val := λ: <>, ref false. Definition acquire : val := rec: "acquire" "x" := if: CAS "x" (#♭ false) (#♭ true) then #() if: CAS "x" false true then () else "acquire" "x". Definition release : val := λ: "x", "x" <- #♭ false. Definition release : val := λ: "x", "x" <- false. Definition with_lock : val := λ: "e" "l" "x", acquire "l";; let: "v" := "e" "x" in ... ... @@ -47,7 +47,7 @@ Section proof. Lemma steps_newlock ρ j K (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ j ⤇ fill K (newlock #())%E spec_ctx ρ -∗ j ⤇ fill K (newlock ())%E ={E1}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#♭v false). Proof. iIntros "#Hspec Hj". ... ... @@ -60,7 +60,7 @@ Section proof. Lemma bin_log_related_newlock_r Γ K t τ (Hcl : nclose specN ⊆ E1) : (∀ l : loc, l ↦ₛ (#♭v false) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Loc l) : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (newlock #())%E: τ. -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (newlock ())%E: τ. Proof. iIntros "Hlog". unfold newlock. unlock. ... ...
 ... ... @@ -8,14 +8,15 @@ From iris.program_logic Require Import adequacy. From iris_logrel.F_mu_ref_conc Require Import hax. Definition par : val := λ: "e1" "e2", let: "x1" := ref InjL #() in Fork ("x1" <- InjR ("e1" #()));; let: "x2" := "e2" #() in let: "f" := rec: "f" <> := case: !"x1" of InjL => λ: <>, "f" #() | InjR => λ: "v", "v" end in ("f" #(), "x2"). let: "x1" := ref InjL () in Fork ("x1" <- InjR ("e1" ()));; let: "x2" := "e2" () in let: "f" := rec: "f" <> := match: !"x1" with InjL <> => "f" () | InjR "v" => "v" end in ("f" (), "x2"). Lemma par_type Γ τ1 τ2 : typed Γ par ... ...
 ... ... @@ -51,7 +51,7 @@ Section masked. rewrite bin_log_related_eq. iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=". value_case. iExists UnitV; eauto. iExists (LitV ()); eauto. Qed. Lemma bin_log_related_nat Δ Γ n : {E,E;Δ;Γ} ⊨ #n n ≤log≤ #n n : TNat. ... ... @@ -513,7 +513,7 @@ Section masked. iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=". tp_fork j as i "Hi". fold subst_p. iModIntro. iApply wp_fork. fold subst_p. iNext. iSplitL "Hj". - iExists UnitV; eauto. - iExists (LitV ()); eauto. - iSpecialize ("IH" with "Hs HΓ"). iSpecialize ("IH" \$! i []). simpl. iSpecialize ("IH" with "Hi"). ... ... @@ -583,7 +583,7 @@ Section masked. tp_store j. iMod ("Hclose" with "[Hw2 Hv2]"). { iNext; iExists (_, _); simpl; iFrame. iFrame "IH2". } iExists UnitV; iFrame; auto. iExists (LitV ()); iFrame; auto. Qed. Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ ... ...
 ... ... @@ -51,7 +51,7 @@ Section hax. Qed. Lemma weird_bind e Q : WP App e #() {{ Q }} ⊢ WP e {{ v, WP (App v #()) {{ Q }} }}. WP App e () {{ Q }} ⊢ WP e {{ v, WP (App v ()) {{ Q }} }}. Proof. (* ugh, turns out this is just the inverse bind: Check (wp_bind_inv (fun v => App v #())). *) ... ... @@ -73,11 +73,11 @@ Section hax. iSplitR; eauto. iNext. iIntros (e2 σ2 efs) "Hpst". iDestruct "Hpst" as %Hpst. iSpecialize ("wp" \$! (App e2 #()) σ2 efs). iAssert (⌜prim_step (e #()%E) σ1 (e2 #()%E) σ2 efs⌝)%I as "Hprim'". iSpecialize ("wp" \$! (App e2 ()) σ2 efs). iAssert (⌜prim_step (e (Lit Unit))%E σ1 (e2 (Lit Unit)%E) σ2 efs⌝)%I as "Hprim'". { iPureIntro. inversion Hpst; simpl in *; subst; clear Hpst. eapply (Ectx_step _ σ1 _ σ2 efs (K++[AppLCtx (#())%E])); simpl; eauto. eapply (Ectx_step _ σ1 _ σ2 efs (K++[AppLCtx (())%E])); simpl; eauto. by rewrite fill_app. by rewrite fill_app. } iMod ("wp" with "Hprim'") as "[\$ [wp \$]]". iModIntro. ... ...
 ... ... @@ -96,9 +96,7 @@ Module lang. Inductive val := | RecV (f x : binder) (e : expr) `{!Closed (x :b: f :b: ∅) e} | TLamV (e : expr) `{!Closed ∅ e} (* only closed lambdas are values *) | UnitV | NatV (n : nat) | BoolV (b : bool) | LitV (l : Literal) | PairV (v1 v2 : val) | InjLV (v : val) | InjRV (v : val) ... ... @@ -108,8 +106,8 @@ Module lang. Bind Scope val_scope with val. (* Notation for bool and nat *) Notation "'#♭v' b" := (BoolV b) (at level 20). Notation "'#nv' n" := (NatV n) (at level 20). Notation "'#♭v' b" := (LitV (Bool b)) (at level 20). Notation "'#nv' n" := (LitV (Nat n)) (at level 20). Fixpoint binop_eval (op : binop) (v1 v2 : val) : option val := match op,v1,v2 with ... ... @@ -122,15 +120,13 @@ Module lang. | Xor,#♭v a,#♭v b => Some \$ #♭v(xorb a b) | _,_,_ => None end. Instance val_inh : Inhabited val := populate UnitV. Instance val_inh : Inhabited val := populate (LitV Unit). Fixpoint of_val (v : val) : expr := match v with | RecV f x e _ => Rec f x e | TLamV e _ => TLam e | UnitV => Lit Unit | NatV v => Lit \$ Nat v | BoolV v => Lit \$ Bool v | LitV l => Lit l | PairV v1 v2 => Pair (of_val v1) (of_val v2) | InjLV v => InjL (of_val v) | InjRV v => InjR (of_val v) ... ... @@ -149,9 +145,7 @@ Module lang. if decide (Closed ∅ e) then Some (TLamV e) else None | Lit Unit => Some UnitV | Lit (Nat n) => Some (NatV n) | Lit (Bool b) => Some (BoolV b) | Lit l => Some (LitV l) | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2) | InjL e => InjLV <\$> to_val e | InjR e => InjRV <\$> to_val e ... ... @@ -169,7 +163,6 @@ Module lang. Lemma of_to_val e v : to_val e = Some v → of_val v = e. Proof. revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal. destruct l; simplify_option_eq; auto. Qed. Instance of_val_inj : Inj (=) (=) of_val. ... ...
 ... ... @@ -57,7 +57,7 @@ Section logrel. Solve Obligations with solve_proper. Program Definition interp_unit : listC D -n> D := λne Δ ww, (⌜ww.1 = UnitV⌝ ∧ ⌜ww.2 = UnitV⌝)%I. (⌜ww.1 = LitV Unit⌝ ∧ ⌜ww.2 = LitV Unit⌝)%I. Solve Obligations with solve_proper_alt. Program Definition interp_nat : listC D -n> D := λne Δ ww, ... ... @@ -387,10 +387,10 @@ Section bin_log_def. End bin_log_def. Notation "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" := (bin_log_related E1 E2 Δ Γ e e' τ) (at level 74, E1,E2, e, e', τ at next level). (bin_log_related E1 E2 Δ Γ e%E e'%E τ) (at level 74, E1,E2, e, e', τ at next level). Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" := (bin_log_related E1 E2 [] Γ e e' τ) (at level 74, E1,E2, e, e', τ at next level). (bin_log_related E1 E2 [] Γ e%E e'%E τ) (at level 74, E1,E2, e, e', τ at next level). (* Notation "Δ ',' Γ ⊨ e '≤log≤' e' : τ" := *) (* (bin_log_related ⊤ ⊤ [] Γ e e' τ) (at level 74, e, e', τ at next level). *) Notation "Γ ⊨ e '≤log≤' e' : τ" := (bin_log_related ⊤ ⊤ [] Γ e e' τ) (at level 74, e, e', τ at next level). (bin_log_related ⊤ ⊤ [] Γ e%E e'%E τ) (at level 74, e, e', τ at next level).
 ... ... @@ -4,10 +4,19 @@ From stdpp Require Import strings. Set Default Proof Using "Type". Import lang. Coercion App : expr >-> Funclass. Coercion Var : string >-> expr. Coercion BNamed : string >-> binder. Coercion of_val : val >-> expr. Coercion Nat : nat >-> Literal. Coercion Bool : bool >-> Literal. Definition litunit : unit -> Literal := fun _ => Unit. Coercion litunit : unit >-> Literal. Coercion Lit : Literal >-> expr. Coercion BNamed : string >-> binder. Notation "<>" := BAnon : binder_scope. Notation Lam x e := (Rec BAnon x e). ... ... @@ -27,16 +36,34 @@ Notation "# l" := (Loc l%Z%V) (at level 8, format "# l") : expr_scope. first. *) Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope. Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)). Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := (Match e0 x1%bind e1 x2%bind e2) (e0, x1, e1, x2, e2 at level 200, format "'[' 'match:' e0 'with' '/' '[hv' 'InjL' x1 => '[' e1 ']' '/' | 'InjR' x2 => '[' e2 ']' '/' 'end' ']' ']'") : expr_scope. Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" := (Match e0 x2%bind e2 x1%bind e1) (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope. Notation "'case:' e0 'of' 'InjL' => e1 | 'InjR' => e2 'end'" := (Case e0 e1 e2) (e0, e1, e2 at level 200) : expr_scope. Notation "#()" := Unit : expr_scope. Notation "#()" := UnitV : val_scope. Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. Notation "'ref' e" := (Alloc e%E) (at level 30, right associativity) : expr_scope. Notation "e1 + e2" := (BinOp Add e1%E e2%E) (at level 50, left associativity) : expr_scope. Notation "e1 - e2" := (BinOp Sub e1%E e2%E) (at level 50, left associativity) : expr_scope. Notation "e1 ≤ e2" := (BinOp Le e1%E e2%E) (at level 70) : expr_scope. Notation "e1 < e2" := (BinOp Lt e1%E e2%E) (at level 70) : expr_scope. Notation "e1 = e2" := (BinOp Eq e1%E e2%E) (at level 70) : expr_scope. Notation "e1 ⊕ e2" := (BinOp Xor e1%E e2%E) (at level 70) : expr_scope. (* The unicode ← is already part of the notation "_ ← _; _" for bind. *) Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E) ... ... @@ -71,4 +98,3 @@ Notation "'let:' x := e1 'in' e2" := (Let x%bind e1%E e2%E) (at level 102, x at level 1, e1, e2 at level 200, format "'[' '[hv' 'let:' x := '[' e1 ']' 'in' ']' '/' e2 ']'") : expr_scope. Coercion of_val : val >-> expr.
 ... ... @@ -202,9 +202,7 @@ Fixpoint to_val (e : expr) : option val := | TLam e => if decide (is_closed ∅ e) is left H then Some (@TLamV (to_expr e) (is_closed_correct _ _ H)) else None | Lit Unit => Some UnitV | Lit (Nat n) => Some (NatV n) | Lit (Bool b) => Some (BoolV b) | Lit l => Some (LitV l) | Loc l => Some (LocV l) | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2) | InjL e => InjLV <\$> to_val e ... ...
 ... ... @@ -1050,7 +1050,7 @@ Section test. Lemma test_store Γ y y' : inv choiceN (choice_inv y y') -∗ Γ ⊨ storeFalse #y ≤log≤ storeFalse #y' : TUnit. -∗ Γ ⊨ (storeFalse #y) ≤log≤ (storeFalse #y') : TUnit. Proof. iIntros "#Hinv". unfold storeFalse. unlock. ... ...
 ... ... @@ -714,11 +714,11 @@ Section properties. {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Fork e) : τ. Proof. iIntros "Hlog". pose (Φ := (fun (v : val) => ∃ i, i ⤇ e ∗ ⌜v = #()⌝%V)%I). pose (Φ := (fun (v : val) => ∃ i, i ⤇ e ∗ ⌜v = LitV tt⌝%V)%I). iApply (bin_log_related_step_r Φ with "[]"); cbv[Φ]. { iIntros (ρ j K') "#Hspec Hj". tp_fork j as i "Hi". iModIntro. iExists #()%V. iFrame. eauto. iModIntro. iExists (LitV tt). iFrame. eauto. } iIntros (v). iDestruct 1 as (i) "[Hi %]"; subst. by iApply "Hlog". ... ... @@ -768,11 +768,10 @@ Section properties. -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Store (Loc l) e) : τ. Proof. iIntros (?) "Hl Hlog". pose (Φ := (fun w => ⌜w = UnitV⌝ ∗ l ↦ₛ v')%I). pose (Φ := (fun w => ⌜w = LitV tt⌝ ∗ l ↦ₛ v')%I). iApply (bin_log_related_step_r Φ with "[Hl]"); eauto. { cbv[Φ]. iIntros (ρ j K') "#Hs Hj /=". iExists UnitV. Ltac solve_to_val ::= idtac. iIntros (ρ j K') "#Hs Hj /=". iExists (LitV tt). tp_store j. iFrame. eauto. } iIntros (w) "[% Hl]"; subst. ... ... @@ -790,12 +789,12 @@ Section properties. -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (CAS (Loc l) e1 e2) : τ. Proof. iIntros (????) "Hl Hlog". pose (Φ := (fun w => ⌜w = BoolV false⌝ ∗ l ↦ₛ v)%I). pose (Φ := (fun (w : val) => ⌜w = LitV false⌝ ∗ l ↦ₛ v)%I). iApply (bin_log_related_step_r Φ with "[Hl]"); eauto. { cbv[Φ]. iIntros (ρ j K') "#Hs Hj /=". tp_cas_fail j; auto. iExists (BoolV false). simpl. iExists (LitV false). simpl. iFrame. eauto. } iIntros (w) "[% Hl]"; subst. iApply "Hlog". ... ... @@ -812,12 +811,12 @@ Section properties. -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (CAS (Loc l) e1 e2) : τ. Proof. iIntros (????) "Hl Hlog". pose (Φ := (fun w => ⌜w = BoolV true⌝ ∗ l ↦ₛ v2)%I). pose (Φ := (fun w => ⌜w = LitV true⌝ ∗ l ↦ₛ v2)%I). iApply (bin_log_related_step_r Φ with "[Hl]"); eauto. { cbv[Φ]. iIntros (ρ j K') "#Hs Hj /=". tp_cas_suc j; auto. iExists (BoolV true). simpl. iExists (LitV true). simpl. iFrame. eauto. } iIntros (w) "[% Hl]"; subst. iApply "Hlog". ... ...
 ... ... @@ -62,7 +62,7 @@ Section lang_rules. Lemma wp_store E l v' e v : to_val e = Some v → {{{ ▷ l ↦ᵢ v' }}} Store (Loc l) e @ E {{{ RET UnitV; l ↦ᵢ v }}}. {{{ RET (LitV ()); l ↦ᵢ v }}}. Proof. iIntros (<-%of_to_val Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. ... ... @@ -75,7 +75,7 @@ Section lang_rules. Lemma wp_cas_fail E l q v' e1 v1 e2 v2 : to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → {{{ ▷ l ↦ᵢ{q} v' }}} CAS (Loc l) e1 e2 @ E {{{ RET (BoolV false); l ↦ᵢ{q} v' }}}. {{{ RET (LitV false); l ↦ᵢ{q} v' }}}. Proof. iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. ... ... @@ -88,7 +88,7 @@ Section lang_rules. Lemma wp_cas_suc E l e1 v1 e2 v2 : to_val e1 = Some v1 → to_val e2 = Some v2 → {{{ ▷ l ↦ᵢ v1 }}} CAS (Loc l) e1 e2 @ E {{{ RET (BoolV true); l ↦ᵢ v2 }}}. {{{ RET (LitV true); l ↦ᵢ v2 }}}. Proof. iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. ... ... @@ -175,7 +175,7 @@ Section lang_rules. Qed. Lemma wp_fork E e Φ : ▷ (|={E}=> Φ UnitV) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}. ▷ (|={E}=> Φ (LitV ())) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_head_step (Fork e) Unit [e]) //=; eauto. - rewrite -(wp_value_fupd _ _ (Lit Unit)); auto. ... ... @@ -184,14 +184,14 @@ Section lang_rules. Qed. Lemma wp_if_true E e1 e2 Φ : ▷ WP e1 @ E {{ Φ }} ⊢ WP If (#♭ true) e1 e2 @ E {{ Φ }}. ▷ WP e1 @ E {{ Φ }} ⊢ WP If true e1 e2 @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_head_step_no_fork (If _ _ _) e1); eauto. intros; inv_head_step; eauto. Qed. Lemma wp_if_false E e1 e2 Φ : ▷ WP e2 @ E {{ Φ }} ⊢ WP If (#♭ false) e1 e2 @ E {{ Φ }}. ▷ WP e2 @ E {{ Φ }} ⊢ WP If false e1 e2 @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_head_step_no_fork (If _ _ _) e2); eauto. intros; inv_head_step; eauto. ... ...
 ... ... @@ -214,7 +214,7 @@ Section cfg. Lemma step_store E ρ j K l v' e v: to_val e = Some v → nclose specN ⊆ E → spec_ctx ρ ∗ j ⤇ fill K (Store (Loc l) e) ∗ l ↦ₛ v' ={E}=∗ j ⤇ (fill K (Lit #())%E) ∗ l ↦ₛ v. ={E}=∗ j ⤇ (fill K (Lit ())%E) ∗ l ↦ₛ v. Proof. iIntros (??) "(#Hinv & Hj & Hl)". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def. ... ... @@ -225,13 +225,13 @@ Section cfg. as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2. iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K (Lit #())%E))). } (exclusive_local_update _ (Excl (fill K (Lit ())%E))). } iMod (own_update_2 with "Hown Hl") as "[Hown Hl]". { eapply auth_update, prod_local_update_2, singleton_local_update, (exclusive_local_update _ (1%Qp, to_agree v)); last done. by rewrite /to_gen_heap lookup_fmap Hl. } iFrame "Hj Hl". iApply "Hclose". iNext. iExists (<[j:=fill K (Lit #())%E]> tp), (<[l:=v]>σ). iExists (<[j:=fill K (Lit ())%E]> tp), (<[l:=v]>σ). rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro. eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto. Qed. ... ... @@ -352,7 +352,7 @@ Section cfg. Lemma step_fork E ρ j K e : nclose specN ⊆ E → spec_ctx ρ ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K (Lit #())%E ∗ j' ⤇ e. spec_ctx ρ ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K (Lit ())%E ∗ j' ⤇ e. Proof. iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def. iInv specN as (tp σ) ">[Hown %]" "Hclose". ... ...
 ... ... @@ -16,9 +16,7 @@ Ltac reshape_val e tac := | of_val ?v => v | Rec ?f ?x ?e => constr:(RecV f x e) | TLam ?e => constr:(TLamV e) | Lit Unit => constr:(UnitV) | Lit (Nat ?n) => constr:(NatV n) | Lit (Bool ?b) => constr:(BoolV b) | Lit ?l => constr:(LitV l) | Pair ?e1 ?e2 => let v1 := go e1 in let v2 := go e2 in constr:(PairV v1 v2) | InjL ?e => let v := go e in constr:(InjLV v) ... ... @@ -987,7 +985,7 @@ Lemma test1 E1 j K l n ρ : nclose specN ⊆ E1 → j ⤇ fill K (App (Lam "x" (Store (Loc l) (BinOp Add (Nat 1) (Var "x")))) (Load (Loc l))) -∗ spec_ctx ρ -∗ l ↦ₛ (NatV n) ={E1}=∗ True. l ↦ₛ (#nv n) ={E1}=∗ True. Proof. iIntros (?) "Hj #? Hl". tp_load j. tp_normalise j. ... ... @@ -1005,7 +1003,7 @@ Lemma test2 E j K l n ρ : (App (If (CAS (Loc l) (Nat n) (Nat (n+1))) (Lam "x" (Fs