Commit 6271cc36 by Dan Frumin

Put the locations into the type of literals

parent 855c3724
 ... ... @@ -16,14 +16,15 @@ Module lang. Instance binop_dec_eq (op op' : binop) : Decision (op = op'). Proof. solve_decision. Defined. Inductive Literal := Unit | Nat (n : nat) | Bool (b : bool). Inductive literal := Unit | Nat (n : nat) | Bool (b : bool) | Loc (l : loc). Inductive expr := | Var (x : string) (* λ-rec *) | Rec (f x : binder) (e : expr) | App (e1 e2 : expr) (* Constants *) | Lit (l : Literal) | Lit (l : literal) | BinOp (op : binop) (e1 e2 : expr) (* If then else *) | If (e0 e1 e2 : expr) ... ... @@ -47,7 +48,6 @@ Module lang. (* Concurrency *) | Fork (e : expr) (* Reference Types *) | Loc (l : loc) (* Should not be present in the surface syntax *) | Alloc (e : expr) | Load (e : expr) | Store (e1 : expr) (e2 : expr) ... ... @@ -58,8 +58,9 @@ Module lang. (* 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'). Instance literal_dec_eq (l l' : literal) : Decision (l = l'). Proof. solve_decision. Defined. Instance expr_dec_eq (e e' : expr) : Decision (e = e'). ... ... @@ -70,7 +71,7 @@ Module lang. match e with | Var x => bool_decide (x ∈ X) | Rec f x e => is_closed (x :b: f :b: X) e | Lit _ | Loc _ => true | Lit _ => true | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Fold e | Unfold e | TLam e | TApp e | Pack e => is_closed X e | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 => ... ... @@ -98,13 +99,12 @@ 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 *) | LitV (l : Literal) | LitV (l : literal) | PairV (v1 v2 : val) | InjLV (v : val) | InjRV (v : val) | FoldV (v : val) | PackV (v : val) | LocV (l : loc). | PackV (v : val). Bind Scope val_scope with val. (* Notation for bool and nat *) ... ... @@ -134,7 +134,6 @@ Module lang. | InjRV v => InjR (of_val v) | FoldV v => Fold (of_val v) | PackV v => Pack (of_val v) | LocV l => Loc l end. Fixpoint to_val (e : expr) : option val := ... ... @@ -153,7 +152,6 @@ Module lang. | InjR e => InjRV <\$> to_val e | Fold e => v ← to_val e; Some (FoldV v) | Pack e => v ← to_val e; Some (PackV v) | Loc l => Some (LocV l) | _ => None end. ... ... @@ -241,7 +239,6 @@ Module lang. | TLam e => TLam (subst x es e) | TApp e => TApp (subst x es e) | Lit l => Lit l | Loc l => Loc l | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2) | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2) | Pair e1 e2 => Pair (subst x es e1) (subst x es e2) ... ... @@ -325,22 +322,22 @@ Module lang. (* Reference Types *) | AllocS e v σ l : to_val e = Some v → σ !! l = None → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) [] head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) [] | LoadS l v σ : σ !! l = Some v → head_step (Load (Loc l)) σ (of_val v) σ [] head_step (Load (Lit (Loc l))) σ (of_val v) σ [] | StoreS l e v σ : to_val e = Some v → is_Some (σ !! l) → head_step (Store (Loc l) e) σ (Lit Unit) (<[l:=v]>σ) [] head_step (Store (Lit (Loc l)) e) σ (Lit Unit) (<[l:=v]>σ) [] (* Compare and swap *) | 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 (Loc l) e1 e2) σ (#♭ false) σ [] head_step (CAS (Lit (Loc l)) e1 e2) σ (#♭ false) σ [] | CasSucS l e1 v1 e2 v2 σ : to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 → head_step (CAS (Loc l) e1 e2) σ (#♭ true) (<[l:=v2]>σ) []. head_step (CAS (Lit (Loc l)) e1 e2) σ (#♭ true) (<[l:=v2]>σ) []. Definition is_atomic (e : expr) : Prop := match e with ... ... @@ -383,7 +380,7 @@ Module lang. Lemma alloc_fresh e v σ : let l := fresh (dom _ σ) in to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) []. to_val e = Some v → head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) []. Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed. End lang. ... ...
 ... ... @@ -9,11 +9,16 @@ Coercion App : expr >-> Funclass. Coercion Var : string >-> expr. Coercion of_val : val >-> expr. Coercion Nat : nat >-> Literal. Coercion Bool : bool >-> Literal. Coercion Nat : nat >-> literal. Coercion Bool : bool >-> literal. Coercion Loc : loc >-> literal. Notation "'tt'" := lang.Unit. Coercion litunit (z : ()) : Literal := Unit. Coercion Lit : Literal >-> expr. Notation "()" := lang.Unit : val_scope. (* No scope for the values, does not conflict and scope is often not inferred properly. *) Notation "# l" := (LitV l%V) (at level 8, format "# l"). Notation "# l" := (Lit l%V) (at level 8, format "# l") : expr_scope. Coercion BNamed : string >-> binder. Notation "<>" := BAnon : binder_scope. ... ... @@ -21,11 +26,6 @@ Notation "<>" := BAnon : binder_scope. Notation Lam x e := (Rec BAnon x e). Notation LamV x e := (RecV BAnon x e). (* No scope for the values, does not conflict and scope is often not inferred properly. *) Notation "# l" := (LocV l%Z%V) (at level 8, format "# l"). Notation "# l" := (Loc l%Z%V) (at level 8, format "# l") : expr_scope. (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come first. *) Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. ... ...
 ... ... @@ -89,7 +89,7 @@ split; intros ?. Qed. Instance pure_if_true e1 e2 : PureExec True (If true e1 e2) e1. PureExec True (If #true e1 e2) e1. Proof. split; intros ?. - intros. do 3 eexists. econstructor; eauto using to_of_val. ... ... @@ -97,7 +97,7 @@ split; intros ?. Qed. Instance pure_if_false e1 e2 : PureExec True (If false e1 e2) e2. PureExec True (If #false e1 e2) e2. Proof. split; intros ?. - intros. do 3 eexists. econstructor; eauto using to_of_val. ... ...
 ... ... @@ -10,7 +10,7 @@ Inductive expr := | Rec (f x : binder) (e : expr) | App (e1 e2 : expr) (* Base Types *) | Lit (l : Literal) | Lit (l : literal) | BinOp (op : binop) (e1 e2 : expr) (* If then else *) | If (e0 e1 e2 : expr) ... ... @@ -34,7 +34,6 @@ Inductive expr := (* Concurrency *) | Fork (e : expr) (* Reference Types *) | Loc (l : loc) | Alloc (e : expr) | Load (e : expr) | Store (e1 : expr) (e2 : expr) ... ... @@ -49,7 +48,6 @@ Fixpoint to_expr (e : expr) : lang.expr := | Rec f x e => lang.Rec f x (to_expr e) | App e1 e2 => lang.App (to_expr e1) (to_expr e2) | Lit l => lang.Lit l | Loc l => lang.Loc l | BinOp op e1 e2 => lang.BinOp op (to_expr e1) (to_expr e2) | If e0 e1 e2 => lang.If (to_expr e0) (to_expr e1) (to_expr e2) | Pair e1 e2 => lang.Pair (to_expr e1) (to_expr e2) ... ... @@ -78,7 +76,6 @@ Ltac of_expr e := | lang.App ?e1 ?e2 => let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2) | lang.Lit ?l => constr:(Lit l) | lang.Loc ?l => constr:(Loc l) | lang.BinOp ?op ?e1 ?e2 => let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2) | lang.If ?e0 ?e1 ?e2 => ... ... @@ -125,7 +122,6 @@ Fixpoint is_closed (X : stringset) (e : expr) : bool := | ClosedExpr e _ => true | Var x => bool_decide (x ∈ X) | Lit l => true | Loc l => true | Rec f x e => is_closed (x :b: f :b: X) e | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | Unpack e1 e2 => is_closed X e1 && is_closed X e2 ... ... @@ -147,7 +143,6 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr := | TLam e => TLam (subst x es e) | TApp e => TApp (subst x es e) | Lit l => Lit l | Loc l => Loc l | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2) | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2) | Pair e1 e2 => Pair (subst x es e1) (subst x es e2) ... ... @@ -193,7 +188,6 @@ Fixpoint to_val (e : expr) : option val := if decide (is_closed ∅ e) is left H then Some (@TLamV (to_expr e) (is_closed_correct _ _ H)) else None | 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 | InjR e => InjRV <\$> to_val e ... ...
 ... ... @@ -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 (LocV l); l ↦ᵢ v }}}. {{{ True }}} Alloc e @ E {{{ l, RET (LitV (Loc l))%E; 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 }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{q} v }}}. {{{ ▷ l ↦ᵢ{q} v }}} (! # l)%E @ 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 %?. ... ... @@ -61,7 +61,7 @@ Section lang_rules. Lemma wp_store E l v' e v : to_val e = Some v → {{{ ▷ l ↦ᵢ v' }}} Store (Loc l) e @ E {{{ ▷ l ↦ᵢ v' }}} # l <- e @ E {{{ RET (LitV tt); l ↦ᵢ v }}}. Proof. iIntros (<-%of_to_val Φ) ">Hl HΦ". ... ... @@ -74,7 +74,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 {{{ ▷ l ↦ᵢ{q} v' }}} CAS (# l) e1 e2 @ E {{{ RET (LitV false); l ↦ᵢ{q} v' }}}. Proof. iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ". ... ... @@ -87,7 +87,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 {{{ ▷ l ↦ᵢ v1 }}} CAS (# l) e1 e2 @ E {{{ RET (LitV true); l ↦ᵢ v2 }}}. Proof. iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ". ... ... @@ -177,21 +177,21 @@ Section lang_rules. Lemma wp_fork E e Φ : ▷ (|={E}=> Φ (LitV tt)) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_head_step (Fork e) tt [e]) //=; eauto. rewrite -(wp_lift_pure_det_head_step (Fork e) #tt [e]) //=; eauto. - rewrite -(wp_value_fupd _ _ (Lit tt)); auto. by rewrite -step_fupd_intro // right_id later_sep. - intros; inv_head_step; eauto. 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. ... ...
 ... ... @@ -18,7 +18,6 @@ Fixpoint subst_p (es : stringmap val) (e : expr) : expr := | TLam e => TLam (subst_p es e) | TApp e => TApp (subst_p es e) | Lit l => Lit l | Loc l => Loc l | BinOp op e1 e2 => BinOp op (subst_p es e1) (subst_p es e2) | If e0 e1 e2 => If (subst_p es e0) (subst_p es e1) (subst_p es e2) | Pair e1 e2 => Pair (subst_p es e1) (subst_p es e2) ... ...
 ... ... @@ -21,7 +21,6 @@ Ltac reshape_val e tac := | InjR ?e => let v := go e in constr:(InjRV v) | Fold ?e => let v := go e in constr:(FoldV v) | Pack ?e => let v := go e in constr:(PackV v) | Loc ?l => constr:(LocV l) end in let v := go e in tac v. Ltac reshape_expr e tac := ... ...
 ... ... @@ -44,9 +44,9 @@ 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 : Γ ⊢ₜ #n n : TNat | Bool_typed b : Γ ⊢ₜ #♭ b : TBool | Unit_typed : Γ ⊢ₜ #tt : TUnit | Nat_typed (n : nat) : Γ ⊢ₜ #n n : TNat | Bool_typed (b : bool) : Γ ⊢ₜ #♭ b : TBool | BinOp_typed_nat op e1 e2 τ : Γ ⊢ₜ e1 : TNat → Γ ⊢ₜ e2 : TNat → binop_nat_res_type op = Some τ → ... ...
 ... ... @@ -9,14 +9,14 @@ Definition bitτ : type := Hint Unfold bitτ : typeable. Definition bit_bool : val := PackV ((λ: "b", "b"), (λ: "b", "b" ⊕ true), #♭v true). PackV ((λ: "b", "b"), (λ: "b", "b" ⊕ #true), #true). Definition flip_nat : val := λ: "n", if: "n" = 0 then 1 else 0. if: "n" = #0 then #1 else #0. Definition bit_nat : val := PackV ((λ: "b", "b" = 0), flip_nat, #nv 0). PackV ((λ: "b", "b" = #0), flip_nat, #0). (** * Typeability *) (** ** Boolean bit *) ... ... @@ -106,7 +106,7 @@ Definition heapify : val := λ: "b", Unpack "b" \$ λ: "b'", let: "x" := ref "init" in let: "flip_ref" := λ: <>, "x" <- "flip" (!"x") in let: "view_ref" := λ: <>, "view" (!"x") in Pack ("view_ref", "flip_ref", ()). Pack ("view_ref", "flip_ref", #()). Lemma heapify_type Γ : typed Γ heapify (TArrow bitτ bitτ). ... ... @@ -200,7 +200,7 @@ Section heapify_refinement. tp_store j. iMod ("Hcl" with "[-Hj]"). { iNext. iExists (_,_). by iFrame. } iModIntro. iExists (LitV ()); iFrame "Hj". eauto. iModIntro. iExists (#()); iFrame "Hj". eauto. - rel_vals; simpl; eauto. Qed. ... ...
 ... ... @@ -4,24 +4,24 @@ From iris_logrel.examples Require Import lock. Definition CG_increment : val := λ: "x" "l" <>, acquire "l";; "x" <- 1 + !"x";; "x" <- #1 + !"x";; release "l". Definition counter_read : val := λ: "x" <>, !"x". Definition CG_counter : val := λ: <>, let: "l" := newlock () in let: "x" := ref 0 in let: "l" := newlock #() in let: "x" := ref #0 in (CG_increment "x" "l", counter_read "x"). Definition FG_increment : val := λ: "v", rec: "inc" <> := let: "c" := !"v" in if: CAS "v" "c" (1 + "c") then () else "inc" (). if: CAS "v" "c" (#1 + "c") then #() else "inc" #(). Definition FG_counter : val := λ: <>, let: "x" := ref 0 in let: "x" := ref #0 in (FG_increment "x", counter_read "x"). Section CG_Counter. ... ... @@ -36,12 +36,12 @@ Section CG_Counter. Hint Resolve CG_increment_type : typeable. Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ x (n : nat) l : 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 ()) : τ)) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment \$/ LocV x \$/ LocV l) ())%E : τ)%I. ({E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit tt) : τ)) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment \$/ (LitV (Loc x)) \$/ LitV (Loc l)) #())%E : τ)%I. Proof. iIntros (?) "Hx Hl Hlog". unfold CG_increment. unlock. simpl_subst/=. ... ... @@ -78,8 +78,8 @@ Section CG_Counter. Lemma bin_log_FG_increment_l Γ K E x n t τ : x ↦ᵢ (#nv n) -∗ (x ↦ᵢ (#nv (S n)) -∗ {E,E;Δ;Γ} ⊨ fill K (Lit ()) ≤log≤ t : τ) -∗ {E,E;Δ;Γ} ⊨ fill K (FG_increment #x ()) ≤log≤ t : τ. (x ↦ᵢ (#nv (S n)) -∗ {E,E;Δ;Γ} ⊨ fill K (Lit tt) ≤log≤ t : τ) -∗ {E,E;Δ;Γ} ⊨ fill K (FG_increment #x #()) ≤log≤ t : τ. Proof. iIntros "Hx Hlog". iApply bin_log_related_wp_l. ... ... @@ -90,7 +90,7 @@ Section CG_Counter. iApply wp_value; eauto. simpl. by rewrite decide_left. iApply wp_rec; eauto. iNext. simpl. wp_bind (Load (Loc x)). wp_bind (Load (# x)). iApply (wp_load with "[Hx]"); auto. iNext. iIntros "Hx". iApply wp_rec; eauto. ... ... @@ -121,7 +121,7 @@ Section CG_Counter. x ↦ₛ (#nv n) -∗ (x ↦ₛ (#nv n) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#n n)%E : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((counter_read \$/ LocV x) ())%E : τ. -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((counter_read \$/ LitV (Loc x)) #())%E : τ. Proof. iIntros "Hx Hlog". unfold counter_read. unlock. simpl. ... ... @@ -137,8 +137,8 @@ Section CG_Counter. □ (|={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 ()) ≤log≤ t : τ)) -∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment \$/ LocV x) ())%E ≤log≤ t : τ). {E2,E1;Δ;Γ} ⊨ fill K (Lit tt) ≤log≤ t : τ)) -∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment \$/ LitV (Loc x)) #())%E ≤log≤ t : τ). Proof. iIntros "#H". unfold FG_increment. unlock. simpl. ... ... @@ -180,7 +180,7 @@ Section CG_Counter. ((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧ (∀ m, x ↦ᵢ (#nv m) ∗ R(m) -∗ {E2,E1;Δ;Γ} ⊨ fill K (#n m) ≤log≤ t : τ)) -∗ {E1,E1;Δ;Γ} ⊨ fill K ((counter_read \$/ LocV x) ())%E ≤log≤ t : τ. -∗ {E1,E1;Δ;Γ} ⊨ fill K ((counter_read \$/ LitV (Loc x)) #())%E ≤log≤ t : τ. Proof. iIntros "#H". unfold counter_read. unlock. simpl. ... ... @@ -196,7 +196,7 @@ Section CG_Counter. (* TODO: try to use with_lock rules *) Lemma FG_CG_increment_refinement l cnt cnt' Γ : inv counterN (counter_inv l cnt cnt') -∗ {⊤,⊤;Δ;Γ} ⊨ FG_increment \$/ LocV cnt ≤log≤ CG_increment \$/ LocV cnt' \$/ LocV l : TArrow TUnit TUnit. {⊤,⊤;Δ;Γ} ⊨ FG_increment \$/ LitV (Loc cnt) ≤log≤ CG_increment \$/ LitV (Loc cnt') \$/ LitV (Loc l) : TArrow TUnit TUnit. Proof. iIntros "#Hinv". iApply bin_log_related_arrow_val. ... ... @@ -227,7 +227,7 @@ Section CG_Counter. Lemma counter_read_refinement l cnt cnt' Γ : inv counterN (counter_inv l cnt cnt') -∗ {⊤,⊤;Δ;Γ} ⊨ counter_read \$/ LocV cnt ≤log≤ counter_read \$/ LocV cnt' : TArrow TUnit TNat. {⊤,⊤;Δ;Γ} ⊨ counter_read \$/ LitV (Loc cnt) ≤log≤ counter_read \$/ LitV (Loc cnt') : TArrow TUnit TNat. Proof. iIntros "#Hinv". iApply bin_log_related_arrow_val. ... ... @@ -280,8 +280,8 @@ Section CG_Counter. unfold CG_increment. unlock. rel_rec_r. rel_rec_r. replace (λ: <>, acquire #l ;; #cnt' <- 1 + (! #cnt');; release #l)%E with (CG_increment \$/ LocV cnt' \$/ LocV l)%E; last first. replace (λ: <>, acquire # l ;; #cnt' <- #1 + (! #cnt');; release # l)%E with (CG_increment \$/ LitV (Loc cnt') \$/ LitV (Loc l))%E; last first. { unfold CG_increment. unlock; simpl_subst/=. reflexivity. } iApply (FG_CG_increment_refinement with "Hinv"). - rel_rec_l. ... ...
 ... ... @@ -2,14 +2,14 @@ From iris.proofmode Require Import tactics. From iris_logrel Require Export logrel. 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" <- 0;; rand (). "x" <- #0;; rand #(). Definition earlyChoice : val := λ: "x", let: "r" := rand () in "x" <- 0;; "r". let: "r" := rand #() in "x" <- #0;; "r". Section Refinement. Context `{logrelG Σ}. ... ... @@ -20,7 +20,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. ... ... @@ -40,7 +40,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. ... ... @@ -73,7 +73,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. ... ...
 From iris.proofmode Require Import tactics. From iris_logrel Require Export logrel. 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 ... ... @@ -45,8 +45,8 @@ Section proof. Lemma steps_newlock ρ j K (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ j ⤇ fill K (newlock ())%E ={E1}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#♭v false). spec_ctx ρ -∗ j ⤇ fill K (newlock #())%E ={E1}=∗ ∃ l : loc, j ⤇ fill K (of_val (# l)) ∗ l ↦ₛ (#♭v 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 (Loc l) : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (newlock ())%E: τ. (∀ l : loc, l ↦ₛ (#♭v false) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit (Loc l)) : τ)%I -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (newlock #())%E: τ. Proof. iIntros "Hlog". unfold newlock. unlock. ... ... @@ -72,13 +72,13 @@ Section proof. Transparent acquire. Lemma steps_acquire ρ j K l (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ l ↦ₛ (#♭v false) -∗ j ⤇ fill K (App acquire (Loc l)) spec_ctx ρ -∗ l ↦ₛ (#♭v false) -∗ j ⤇ fill K (App acquire (Lit (Loc l))) ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v true). Proof. iIntros "#Hspec Hl Hj". unfold acquire. unlock. tp_rec j. tp_cas_suc j. tp_cas_suc j. simpl. tp_if_true j. by iFrame. Qed. ... ... @@ -87,7 +87,7 @@ Section proof. (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 (Loc l)) : τ. -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App acquire (# l)) : τ. Proof. iIntros "Hl Hlog". unfold acquire. unlock. ... ... @@ -102,7 +102,7 @@ Section proof. Transparent release. Lemma steps_release ρ j K l b (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App release (Loc l)) spec_ctx ρ -∗ l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App release (# l)) ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v false). Proof. iIntros "#Hspec Hl Hj". unfold release. unlock. ... ... @@ -115,7 +115,7 @@ Section proof. (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 (Loc l)) : τ. -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App release (# l)) : τ. Proof. iIntros "Hl Hlog". unfold release. unlock. ... ... @@ -132,7 +132,7 @@ Section proof. ={E1}=∗ j ⤇ fill K' (of_val v) ∗ Q) → (nclose specN ⊆ E1) → spec_ctx ρ -∗ P -∗ l ↦ₛ (#♭v false) -∗ j ⤇ fill K (App (with_lock e (Loc l)) (of_val w)) -∗ j ⤇ fill K (App (with_lock e (# l)) (of_val w)) ={E1}=∗ j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#♭v false). Proof. iIntros (Hev Hpf ?) "#Hspec HP Hl Hj". ... ... @@ -140,7 +140,7 @@ Section proof. tp_rec j. tp_rec j. tp_rec j. tp_bind j (App acquire (Loc l)). tp_bind j (App acquire (# l)). tp_apply j steps_acquire with "Hl" as "Hl". tp_rec j. tp_bind j (App e _). ... ... @@ -163,16 +163,16 @@ Section proof. {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 (Loc l) ew) : τ. -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (with_lock e (# l) ew) : τ. Proof. iIntros (????) "HA Hl Hlog". rel_bind_r (with_lock e). unfold with_lock. unlock. (*TODO: unlock here needed *) iApply (bin_log_related_rec_r); eauto. simpl_subst. rel_bind_r (App _ (#l)%E). rel_bind_r (App _ (# l)). iApply (bin_log_related_rec_r); eauto. simpl_subst. iApply (bin_log_related_rec_r); eauto. simpl_subst. rel_bind_r (App acquire (Loc l)). rel_bind_r (App acquire (# l)). iApply (bin_log_related_acquire_r Γ (_ :: K) l with "Hl"); auto. iIntros "Hl". simpl. iApply (bin_log_related_rec_r); eauto. simpl_subst/=. ... ...
 ... ... @@ -2,15 +2,15 @@ From iris.proofmode Require Import tactics. From iris_logrel Require Export logrel. Definition par : val := λ: "e1" "e2", let: "x1" := ref InjL () in Fork ("x1" <- InjR ("e1" ()));; let: "x2" := "e2" () in let: "x1" := ref InjL #() in Fork ("x1" <- InjR ("e1" #()));; let: "x2" := "e2" #() in let: "f" := rec: "f" <> := match: !"x1" with InjL <> => "f" () InjL <> => "f" #()