Commit aee54795 by Robbert Krebbers

Fix notations for literals.

parent a0399a74
 ... ... @@ -55,11 +55,6 @@ Module lang. | CAS (e0 : expr) (e1 : expr) (e2 : expr). Bind Scope expr_scope with expr. (* Notation for bool and nat *) Notation "#♭ b" := (Lit (Bool b)) (at level 20). Notation "#n n" := (Lit (Nat n)) (at level 20). Notation "#l l" := (Lit (Loc l)) (at level 20). Instance literal_dec_eq (l l' : literal) : Decision (l = l'). Proof. solve_decision. Defined. ... ... @@ -108,18 +103,15 @@ Module lang. Bind Scope val_scope with val. (* Notation for bool and nat *) 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 | Add,#nv a,#nv b => Some \$ #nv(a + b) | Sub,#nv a,#nv b => Some \$ #nv(a - b) | Eq,#nv a,#nv b => Some \$ if (eq_nat_dec a b) then #♭v true else #♭v false | Eq,#♭v a,#♭v b => Some \$ #♭v(eqb a b) | Le,#nv a,#nv b => Some \$ if (le_dec a b) then #♭v true else #♭v false | Lt,#nv a,#nv b => Some \$ if (lt_dec a b) then #♭v true else #♭v false | Xor,#♭v a,#♭v b => Some \$ #♭v(xorb a b) | Add, LitV (Nat a), LitV (Nat b) => Some \$ LitV (Nat (a + b)) | Sub, LitV (Nat a), LitV (Nat b) => Some \$ LitV (Nat (a - b)) | Eq, LitV (Nat a), LitV (Nat b) => Some \$ if eq_nat_dec a b then LitV (Bool true) else LitV (Bool false) | Eq, LitV (Bool a), LitV (Bool b) => Some \$ LitV (Bool (eqb a b)) | Le, LitV (Nat a), LitV (Nat b) => Some \$ if le_dec a b then LitV (Bool true) else LitV (Bool false) | Lt, LitV (Nat a), LitV (Nat b) => Some \$ if lt_dec a b then LitV (Bool true) else LitV (Bool false) | Xor, LitV (Bool a), LitV (Bool b) => Some \$ LitV (Bool (xorb a b)) | _,_,_ => None end. Instance val_inh : Inhabited val := populate (LitV Unit). ... ... @@ -300,9 +292,9 @@ Module lang. head_step (BinOp op e1 e2) σ (of_val v) σ [] (* If then else *) | IfFalse e1 e2 σ : head_step (If (#♭ false) e1 e2) σ e2 σ [] head_step (If (Lit (Bool false)) e1 e2) σ e2 σ [] | IfTrue e1 e2 σ : head_step (If (#♭ true) e1 e2) σ e1 σ [] head_step (If (Lit (Bool true)) e1 e2) σ e1 σ [] (* Recursive Types *) | Unfold_Fold e v σ : to_val e = Some v → ... ... @@ -333,11 +325,11 @@ Module lang. | CasFailS l e1 v1 e2 v2 vl σ : to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some vl → vl ≠ v1 → head_step (CAS (Lit (Loc l)) e1 e2) σ (#♭ false) σ [] head_step (CAS (Lit (Loc l)) e1 e2) σ (Lit (Bool false)) σ [] | CasSucS l e1 v1 e2 v2 σ : to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 → head_step (CAS (Lit (Loc l)) e1 e2) σ (#♭ true) (<[l:=v2]>σ) []. head_step (CAS (Lit (Loc l)) e1 e2) σ (Lit (Bool true)) (<[l:=v2]>σ) []. Definition is_atomic (e : expr) : Prop := match e with ... ...
 ... ... @@ -12,7 +12,6 @@ Coercion of_val : val >-> expr. Coercion Nat : nat >-> literal. Coercion Bool : bool >-> literal. Coercion Loc : loc >-> literal. Notation "'tt'" := lang.Unit. Notation "()" := lang.Unit : val_scope. (* No scope for the values, does not conflict and scope is often not inferred ... ...
 ... ... @@ -40,7 +40,7 @@ Section lang_rules. (** Base axioms for core primitives of the language: Stateful reductions. *) Lemma wp_alloc E e v : to_val e = Some v → {{{ True }}} Alloc e @ E {{{ l, RET (LitV (Loc l))%E; l ↦ᵢ v }}}. {{{ True }}} Alloc e @ E {{{ l, RET #l; l ↦ᵢ v }}}. Proof. iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (σ1) "Hσ !>"; iSplit; first by auto. ... ... @@ -50,7 +50,7 @@ Section lang_rules. Qed. Lemma wp_load E l q v : {{{ ▷ l ↦ᵢ{q} v }}} (! # l)%E @ E {{{ RET v; l ↦ᵢ{q} v }}}. {{{ ▷ l ↦ᵢ{q} v }}} ! #l @ E {{{ RET v; l ↦ᵢ{q} v }}}. Proof. iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. ... ... @@ -58,11 +58,11 @@ Section lang_rules. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iModIntro; iSplit=> //. iFrame. by iApply "HΦ". Qed. Lemma wp_store E l v' e v : to_val e = Some v → {{{ ▷ l ↦ᵢ v' }}} # l <- e @ E {{{ RET (LitV tt); l ↦ᵢ v }}}. {{{ ▷ l ↦ᵢ v' }}} #l <- e @ E {{{ RET #(); l ↦ᵢ v }}}. Proof. iIntros (<-%of_to_val Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. ... ... @@ -74,8 +74,8 @@ 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 (# l) e1 e2 @ E {{{ RET (LitV false); l ↦ᵢ{q} v' }}}. {{{ ▷ l ↦ᵢ{q} v' }}} CAS #l e1 e2 @ E {{{ RET #false; l ↦ᵢ{q} v' }}}. Proof. iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. ... ... @@ -87,8 +87,8 @@ 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 (# l) e1 e2 @ E {{{ RET (LitV true); l ↦ᵢ v2 }}}. {{{ ▷ l ↦ᵢ v1 }}} CAS #l e1 e2 @ E {{{ RET #true; l ↦ᵢ v2 }}}. Proof. iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. ... ... @@ -172,7 +172,7 @@ Section lang_rules. Lemma wp_case_inl E e0 v0 e1 e2 Φ : to_val e0 = Some v0 → ▷ WP (App e1 e0) @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}. ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) _); eauto. intros; inv_head_step; eauto. ... ... @@ -180,17 +180,17 @@ Section lang_rules. Lemma wp_case_inr E e0 v0 e1 e2 Φ : to_val e0 = Some v0 → ▷ WP (App e2 e0) @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}. ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _)); eauto. intros; inv_head_step; eauto. Qed. Lemma wp_fork E e Φ : ▷ (|={E}=> Φ (LitV tt)) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}. ▷ (|={E}=> Φ #()) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_head_step (Fork e) #tt [e]) //=; eauto. - rewrite -(wp_value_fupd _ _ (Lit tt)); auto. rewrite -(wp_lift_pure_det_head_step (Fork e) #() [e]) //=; eauto. - rewrite -(wp_value_fupd _ _ #()); auto. by rewrite -step_fupd_intro // right_id later_sep. - intros; inv_head_step; eauto. Qed. ... ...
 ... ... @@ -44,10 +44,10 @@ Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level). Inductive typed (Γ : stringmap type) : expr → type → Prop := | Var_typed x τ : Γ !! x = Some τ → Γ ⊢ₜ Var x : τ | Unit_typed : Γ ⊢ₜ #tt : TUnit | Nat_typed (n : nat) : Γ ⊢ₜ #n n : TNat | Bool_typed (b : bool) : Γ ⊢ₜ #♭ b : TBool | BinOp_typed_nat op e1 e2 τ : | Unit_typed : Γ ⊢ₜ #() : TUnit | Nat_typed (n : nat) : Γ ⊢ₜ # n : TNat | Bool_typed (b : bool) : Γ ⊢ₜ # b : TBool | BinOp_typed_nat op e1 e2 τ : Γ ⊢ₜ e1 : TNat → Γ ⊢ₜ e2 : TNat → binop_nat_res_type op = Some τ → Γ ⊢ₜ BinOp op e1 e2 : τ ... ... @@ -133,14 +133,14 @@ Tactic Notation "solve_typed" := solve_typed 50. (** Typeability of binops *) Lemma binop_nat_typed_safe (op : binop) (n1 n2 : nat) τ : binop_nat_res_type op = Some τ → is_Some (binop_eval op (#nv n1) (#nv n2)). binop_nat_res_type op = Some τ → is_Some (binop_eval op #n1 #n2). Proof. destruct op; simpl; eauto. inversion 1. Qed. Lemma binop_bool_typed_safe (op : binop) (b1 b2 : bool) τ : binop_bool_res_type op = Some τ → is_Some (binop_eval op (#♭v b1) (#♭v b2)). binop_bool_res_type op = Some τ → is_Some (binop_eval op #b1 #b2). Proof. destruct op; simpl; eauto; try by inversion 1. Qed. ... ...
 From iris.proofmode Require Import tactics. From iris.algebra Require Import agree (* TODO: Why do we need to import this? *). From iris_logrel Require Import logrel. Definition bitτ : type := ... ... @@ -54,7 +53,7 @@ Section bit_refinement. (* This is the graph of the `bitf` function *) Program Definition bitτi : prodC valC valC -n> iProp Σ := λne vv, (∃ b, ⌜vv.1 = #♭v b⌝ ∗ ⌜vv.2 = #nv (bitf b)⌝)%I. (∃ b : bool, ⌜vv.1 = #b⌝ ∗ ⌜vv.2 = #(bitf b)⌝)%I. Next Obligation. solve_proper. Qed. Instance bitτi_persistent ww : PersistentP (bitτi ww). ... ...
 ... ... @@ -27,8 +27,7 @@ Definition FG_counter : val := λ: <>, Section CG_Counter. Context `{logrelG Σ}. Variable (Δ : list (prodC valC valC -n> iProp Σ)). Open Scope expr_scope. (* Coarse-grained increment *) Lemma CG_increment_type Γ : typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))). ... ... @@ -38,10 +37,10 @@ Section CG_Counter. Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ (x l : loc) (n : nat) : nclose specN ⊆ E1 → (x ↦ₛ (#nv n) -∗ l ↦ₛ (#♭v false) -∗ (x ↦ₛ (#nv S n) -∗ l ↦ₛ (#♭v false) -∗ ({E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit tt) : τ)) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment \$/ (LitV (Loc x)) \$/ LitV (Loc l)) #())%E : τ)%I. (x ↦ₛ # n -∗ l ↦ₛ #false -∗ (x ↦ₛ # (S n) -∗ l ↦ₛ #false -∗ ({E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #() : τ)) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment \$/ (LitV (Loc x)) \$/ LitV (Loc l)) #()) : τ)%I. Proof. iIntros (?) "Hx Hl Hlog". unfold CG_increment. unlock. simpl_subst/=. ... ... @@ -76,9 +75,9 @@ Section CG_Counter. Hint Resolve FG_increment_type : typeable. Lemma bin_log_FG_increment_l Γ K E x n t τ : x ↦ᵢ (#nv n) -∗ (x ↦ᵢ (#nv (S n)) -∗ {E,E;Δ;Γ} ⊨ fill K (Lit tt) ≤log≤ t : τ) -∗ Lemma bin_log_FG_increment_l Γ K E x (n : nat) t τ : x ↦ᵢ #n -∗ (x ↦ᵢ # (S n) -∗ {E,E;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ) -∗ {E,E;Δ;Γ} ⊨ fill K (FG_increment #x #()) ≤log≤ t : τ. Proof. iIntros "Hx Hlog". ... ... @@ -114,14 +113,13 @@ Section CG_Counter. Definition counterN : namespace := nroot .@ "counter". Definition counter_inv l cnt cnt' : iProp Σ := (∃ n, l ↦ₛ (#♭v false) ∗ cnt ↦ᵢ (#nv n) ∗ cnt' ↦ₛ (#nv n))%I. (∃ n : nat, l ↦ₛ #false ∗ cnt ↦ᵢ #n ∗ cnt' ↦ₛ #n)%I. Lemma bin_log_counter_read_r Γ E1 E2 K x n t τ Lemma bin_log_counter_read_r Γ E1 E2 K x (n : nat) t τ (Hspec : nclose specN ⊆ E1) : x ↦ₛ (#nv n) -∗ (x ↦ₛ (#nv n) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#n n)%E : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((counter_read \$/ LitV (Loc x)) #())%E : τ. x ↦ₛ #n -∗ (x ↦ₛ #n -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((counter_read \$/ LitV (Loc x)) #())%E : τ. Proof. iIntros "Hx Hlog". unfold counter_read. unlock. simpl. ... ... @@ -134,10 +132,10 @@ Section CG_Counter. a fine-grained increment with a baked in frame. *) (* Unfortunately, the precondition is not baked in the rule so you can only use it when your spatial context is empty *) Lemma bin_log_FG_increment_logatomic R Γ E1 E2 K x t τ : □ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗ ((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧ (∀ m, x ↦ᵢ (#nv (S m)) ∗ R(m) -∗ {E2,E1;Δ;Γ} ⊨ fill K (Lit tt) ≤log≤ t : τ)) □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗ ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧ (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ {E2,E1;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ)) -∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment \$/ LitV (Loc x)) #())%E ≤log≤ t : τ). Proof. iIntros "#H". ... ... @@ -147,7 +145,7 @@ Section CG_Counter. iPoseProof "H" as "H2". (* lolwhat *) rel_load_l_atomic. iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro. iExists (#nv n). iFrame. iNext. iIntros "Hx". iExists #n. iFrame. iNext. iIntros "Hx". iDestruct "Hrev" as "[Hrev _]". iApply fupd_logrel. iMod ("Hrev" with "[HR Hx]"). ... ... @@ -157,13 +155,13 @@ Section CG_Counter. rel_cas_l_atomic. iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl. destruct (decide (n = n')); subst. - iExists (#nv n'). iFrame. - iExists #n'. iFrame. iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. } iIntros "_ !> Hx". simpl. iDestruct "HQ" as "[_ HQ]". iSpecialize ("HQ" \$! n' with "[Hx HR]"). { iFrame. } rel_if_true_l. done. - iExists (#nv n'). iFrame. - iExists #n'. iFrame. iSplitL; eauto; last first. { iDestruct 1 as %Hfoo. exfalso. simplify_eq. } iIntros "_ !> Hx". simpl. ... ... @@ -176,10 +174,10 @@ Section CG_Counter. (* A similar atomic specification for the counter_read fn *) Lemma bin_log_counter_read_atomic_l R Γ E1 E2 K x t τ : □ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗ ((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧ (∀ m, x ↦ᵢ (#nv m) ∗ R(m) -∗ {E2,E1;Δ;Γ} ⊨ fill K (#n m) ≤log≤ t : τ)) □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗ ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧ (∀ m : nat, x ↦ᵢ #m ∗ R m -∗ {E2,E1;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ)) -∗ {E1,E1;Δ;Γ} ⊨ fill K ((counter_read \$/ LitV (Loc x)) #())%E ≤log≤ t : τ. Proof. iIntros "#H". ... ... @@ -206,7 +204,7 @@ Section CG_Counter. { unfold CG_increment. unlock; simpl_subst/=. solve_closed. } iAlways. iIntros (v v') "[% %]"; simpl in *; subst. iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]"). iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I _ _ _ [] cnt with "[Hinv]"). iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro. iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]". ... ... @@ -236,7 +234,7 @@ Section CG_Counter. { unfold counter_read. unlock. simpl. solve_closed. } { unfold counter_read. unlock. simpl. solve_closed. } iAlways. iIntros (v v') "[% %]"; simpl in *; subst. iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]"). iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I _ _ _ [] cnt with "[Hinv]"). iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". iModIntro. iExists n. iFrame "Hcnt Hcnt' Hl". clear n. ... ...
 ... ... @@ -17,16 +17,15 @@ Section Refinement. Definition choiceN : namespace := nroot .@ "choice". Definition choice_inv y y' : iProp Σ := (∃ f, y ↦ᵢ (#♭v f) ∗ y' ↦ₛ (#♭v f))%I. (∃ f : bool, y ↦ᵢ #f ∗ y' ↦ₛ #f)%I. Lemma wp_rand : (WP rand #() {{ v, ⌜v = #♭v true⌝ ∨ ⌜v = #♭v false⌝}})%I. (WP rand #() {{ v, ⌜v = #true⌝ ∨ ⌜v = #false⌝}})%I. Proof. iStartProof. unfold rand. unlock. iApply wp_rec; eauto. iNext. simpl. wp_bind (Alloc _). iApply wp_alloc; auto. iNext. iIntros (y) "Hy". iMod (inv_alloc choiceN _ (y ↦ᵢ (#♭v false) ∨ y ↦ᵢ (#♭v true))%I with "[Hy]") as "#Hinv"; eauto. iMod (inv_alloc choiceN _ (y ↦ᵢ #false ∨ y ↦ᵢ #true)%I with "[Hy]") as "#Hinv"; eauto. iApply wp_rec; eauto. iNext. simpl. wp_bind (Fork _). iApply wp_fork. iNext. iSplitL. ... ... @@ -39,15 +38,15 @@ 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 : τ. spec_ctx ρ -∗ (∀ b : bool, {E1,E1;Δ;Γ} ⊨ fill K #b ≤log≤ t : τ) -∗ {E1,E1;Δ;Γ} ⊨ fill K (rand #()) ≤log≤ t : τ. Proof. iIntros (?) "#Hs Hlog". unfold rand. unlock. simpl. rel_rec_l. rel_alloc_l as y "Hy". simpl. rel_rec_l. iMod (inv_alloc choiceN _ (∃ b, y ↦ᵢ (#♭v b))%I with "[Hy]") as "#Hinv". iMod (inv_alloc choiceN _ (∃ b : bool, y ↦ᵢ #b)%I with "[Hy]") as "#Hinv". { iNext. eauto. } rel_fork_l. iModIntro. iSplitR. ... ... @@ -61,18 +60,18 @@ Section Refinement. rel_rec_l. rel_load_l_atomic. iInv choiceN as (b) "Hy" "Hcl". iExists (#♭v b). iFrame. iExists #b. iFrame. iModIntro. iNext. iIntros "Hy". iMod ("Hcl" with "[Hy]"). { iNext. iExists b. iFrame. } done. Qed. Lemma rand_r b Δ Γ E1 E2 K ρ t τ : Lemma rand_r (b : bool) Δ Γ E1 E2 K ρ t τ : ↑specN ⊆ E1 → ↑choiceN ⊆ E1 → spec_ctx ρ -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#♭ b) : τ -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #b : τ -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (rand #())%E : τ. Proof. iIntros (??) "#Hs Hlog". ... ... @@ -90,7 +89,7 @@ Section Refinement. Lemma lateChoice_l Δ Γ x v ρ t : spec_ctx ρ -∗ x ↦ᵢ v -∗ (x ↦ᵢ (#nv 0) -∗ ∀ b, {⊤,⊤;Δ;Γ} ⊨ #♭ b ≤log≤ t : TBool) -∗ (x ↦ᵢ #0 -∗ ∀ b : bool, {⊤,⊤;Δ;Γ} ⊨ #b ≤log≤ t : TBool) -∗ {⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ t : TBool. Proof. iIntros "#Hs Hx Hlog". ... ... @@ -103,8 +102,8 @@ Section Refinement. Qed. Lemma prerefinement Δ Γ x x' n ρ : (spec_ctx ρ -∗ x ↦ᵢ (#nv n) -∗ x' ↦ₛ (#nv n) -∗ {⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool)%I. spec_ctx ρ -∗ x ↦ᵢ #n -∗ x' ↦ₛ #n -∗ {⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool. Proof. iIntros "#Hspec Hx Hx'". iApply (lateChoice_l with "Hspec Hx"). iIntros "Hx". ... ... @@ -120,8 +119,8 @@ Section Refinement. Qed. Lemma prerefinement2 Δ Γ x x' n ρ : (spec_ctx ρ -∗ x ↦ᵢ (#nv n) -∗ x' ↦ₛ (#nv n) -∗ {⊤,⊤;Δ;Γ} ⊨ earlyChoice #x ≤log≤ lateChoice #x' : TBool)%I. spec_ctx ρ -∗ x ↦ᵢ #n -∗ x' ↦ₛ #n -∗ {⊤,⊤;Δ;Γ} ⊨ earlyChoice #x ≤log≤ lateChoice #x' : TBool. Proof. iIntros "#Hspec Hx Hx'". unfold earlyChoice. unlock. ... ...
 ... ... @@ -45,8 +45,8 @@ Section proof. Lemma steps_newlock ρ j K (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ j ⤇ fill K (newlock #())%E ={E1}=∗ ∃ l : loc, j ⤇ fill K (of_val (# l)) ∗ l ↦ₛ (#♭v false). spec_ctx ρ -∗ j ⤇ fill K (newlock #()) ={E1}=∗ ∃ l : loc, j ⤇ fill K (of_val #l) ∗ l ↦ₛ #false. Proof. iIntros "#Hspec Hj". unfold newlock. unlock. ... ... @@ -57,8 +57,8 @@ 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 (Lit (Loc l)) : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (newlock #())%E: τ. (∀ l : loc, l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #l : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (newlock #()): τ. Proof. iIntros "Hlog". unfold newlock. unlock. ... ... @@ -72,8 +72,8 @@ Section proof. Transparent acquire. Lemma steps_acquire ρ j K l (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ l ↦ₛ (#♭v false) -∗ j ⤇ fill K (App acquire (Lit (Loc l))) ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v true). spec_ctx ρ -∗ l ↦ₛ #false -∗ j ⤇ fill K (acquire #l) ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ #true. Proof. iIntros "#Hspec Hl Hj". unfold acquire. unlock. ... ... @@ -85,9 +85,9 @@ Section proof. Lemma bin_log_related_acquire_r Γ K l t τ (Hcl : nclose specN ⊆ E1) : l ↦ₛ (#♭v false) -∗ (l ↦ₛ (#♭v true) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App acquire (# l)) : τ. l ↦ₛ #false -∗ (l ↦ₛ #true -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (acquire #l) : τ. Proof. iIntros "Hl Hlog". unfold acquire. unlock. ... ... @@ -100,22 +100,22 @@ Section proof. Global Opaque acquire. Transparent release. Lemma steps_release ρ j K l b Lemma steps_release ρ j K l (b : bool) (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App release (# l)) ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v false). spec_ctx ρ -∗ l ↦ₛ #b -∗ j ⤇ fill K (release #l) ={E1}=∗ j ⤇ fill K (#())%E ∗ l ↦ₛ #false. Proof. iIntros "#Hspec Hl Hj". unfold release. unlock. tp_rec j. tp_store j. tp_normalise j. tp_store j. by iFrame. Qed. Lemma bin_log_related_release_r Γ K l t τ b Lemma bin_log_related_release_r Γ K l t τ (b : bool) (Hcl : nclose specN ⊆ E1) : l ↦ₛ (#♭v b) -∗ (l ↦ₛ (#♭v false) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App release (# l)) : τ. l ↦ₛ #b -∗ (l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (release #l) : τ. Proof. iIntros "Hl Hlog". unfold release. unlock. ... ... @@ -131,9 +131,9 @@ Section proof. (∀ K', spec_ctx ρ -∗ P -∗ j ⤇ fill K' (App e (of_val w)) ={E1}=∗ j ⤇ fill K' (of_val v) ∗ Q) → (nclose specN ⊆ E1) → spec_ctx ρ -∗ P -∗ l ↦ₛ (#♭v false) -∗ j ⤇ fill K (App (with_lock e (# l)) (of_val w)) ={E1}=∗ j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#♭v false). spec_ctx ρ -∗ P -∗ l ↦ₛ #false -∗ j ⤇ fill K (with_lock e #l w) ={E1}=∗ j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ #false. Proof. iIntros (Hev Hpf ?) "#Hspec HP Hl Hj". unfold with_lock. unlock. ... ... @@ -161,9 +161,9 @@ Section proof. (nclose specN ⊆ E1) → (∀ K, (Q -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ev : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App e ew) : τ) -∗ l ↦ₛ (#♭v false) -∗ (Q -∗ l ↦ₛ (#♭v false) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ev : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (with_lock e (# l) ew) : τ. l ↦ₛ #false -∗ (Q -∗ l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ev : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (with_lock e #l ew) : τ. Proof. iIntros (????) "HA Hl Hlog". rel_bind_r (with_lock e). ... ...
 ... ... @@ -60,7 +60,7 @@ Definition CG_stack_body : val := λ: "st" "l", (* Instance: Closed ∅ ((λ: "l", #()) newlock). *) (* Proof. solve_closed. Qed *) Definition CG_stack : val := Λ: let: "l" := ref #♭ false in Λ: let: "l" := ref #false in let: "st" := ref Nile in CG_stack_body "st" "l". ... ...
 ... ... @@ -11,12 +11,12 @@ Section Stack_refinement. Implicit Types Δ : listC D. Import lang. Definition sinv τi stk stk' l' {SH: stackG Σ} : iProp Σ := (∃ (istk : loc) v h, (stack_owns h) Definition sinv τi stk stk' l' {SH: stackG Σ} : iProp Σ := (∃ (istk : loc) v h, (stack_owns h) ∗ stk' ↦ₛ v ∗ stk ↦ᵢ (FoldV (#istk)) ∗ stk ↦ᵢ (FoldV #istk) ∗ StackLink τi (#istk, v) ∗ l' ↦ₛ (#♭v false))%I. ∗ l' ↦ₛ #false)%I. Ltac close_sinv Hcl asn := iMod (Hcl with asn) as "_"; ... ... @@ -82,7 +82,7 @@ Section Stack_refinement. Lemma FG_CG_pop_refinement st st' (τi : D) l {τP : ∀ ww, PersistentP (τi ww)} Δ Γ : inv stackN (sinv τi st st' l) -∗ {⊤,⊤;τi::Δ;Γ} ⊨ (FG_pop \$/ LitV (Loc st))%E ≤log≤ (CG_locked_pop \$/ LitV (Loc st') \$/ LitV (Loc l))%E : TArrow TUnit (TSum TUnit (TVar 0)). {⊤,⊤;τi::Δ;Γ} ⊨ FG_pop \$/ LitV (Loc st) ≤log≤ CG_locked_pop \$/ LitV (Loc st') \$/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)). Proof. iIntros "#Hinv". Transparent CG_locked_pop FG_pop CG_pop. ... ... @@ -199,7 +199,7 @@ Section Stack_refinement. Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ} Γ: inv stackN (sinv τi st st' l) -∗ {⊤,⊤;τi::Δ;Γ} ⊨ (FG_read_iter \$/ LitV (Loc st))%E ≤log≤ (CG_snap_iter \$/ LitV (Loc st') \$/ LitV (Loc l))%E : TArrow (TArrow (TVar 0) TUnit) TUnit. {⊤,⊤;τi::Δ;Γ} ⊨ FG_read_iter \$/ LitV (Loc st) ≤log≤ CG_snap_iter \$/ LitV (Loc st') \$/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit. Proof. iIntros "#Hinv". Transparent FG_read_iter CG_snap_iter. ... ...
 ... ... @@ -48,7 +48,7 @@ Section Rules. ∗ ▷ stacklink Q (z1, z2) }*) Program Definition StackLink_pre (Q : D) : D -n> D := λne P v, (∃ (l : loc) w, ⌜v.1 = # l⌝ ∗ l ↦ˢᵗᵏ w ∗ ((⌜w = InjLV (LitV tt)⌝ ∧ ⌜v.2 = FoldV (InjLV (LitV tt))⌝) ∨ ((⌜w = InjLV #()⌝ ∧ ⌜v.2 = FoldV (InjLV #())⌝) ∨ (∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌝ ∗ ⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝ ∗ Q (y1, y2) ∗ ▷ P(z1, z2))))%I. Solve Obligations with solve_proper. ... ... @@ -61,7 +61,7 @@ Section Rules. Lemma StackLink_unfold Q v : StackLink Q v ≡ (∃ (l : loc) w, ⌜v.1 = # l⌝ ∗ l ↦ˢᵗᵏ w ∗ ((⌜w = InjLV (LitV tt)⌝ ∧ ⌜v.2 = FoldV (InjLV (LitV tt))⌝) ∨ ((⌜w = InjLV #()⌝ ∧ ⌜v.2 = FoldV (InjLV #())⌝) ∨ (∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌝ ∗ ⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝ ∗ Q (y1, y2) ∗ ▷ StackLink Q (z1, z2))))%I. ... ...
 From iris_logrel.F_mu_ref_conc Require Import typing reflection notation. Definition prog : val := λ: "x", if: !"x" then (λ: <>, #1)%E else (λ: <>, (Lit 0)). Definition prog : val := λ: "x", if: !"x" then (λ: <>, #1) else (λ: <>, #0). Lemma prog_typed Γ : Γ ⊢ₜ prog : TArrow (Tref TBool) (TArrow TUnit TNat). Proof. ... ... @@ -11,7 +11,7 @@ Hint Resolve prog_typed : typeable. Definition prog2 : val := λ: <>, let: "x" := ref #false in prog "x" #tt. prog "x" #().