Commit 760d90c0 by Daniël Louwrink

### update remaining rules, split mutex into lib

parent dd104e06
 ... ... @@ -27,5 +27,6 @@ theories/logrel/operators.v theories/logrel/term_typing_judgment.v theories/logrel/subtyping_rules.v theories/logrel/term_typing_rules.v theories/logrel/lib/mutex.v theories/logrel/examples/double.v theories/logrel/examples/pair.v
 From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Export spin_lock. From actris.logrel Require Export term_types term_typing_judgment subtyping. From actris.logrel Require Import environments. From actris.channel Require Import proofmode. From iris.heap_lang Require Import metatheory. Definition lty_mutex `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ∃ (γ : gname) (l : loc) (lk : val), ⌜ w = PairV lk #l ⌝ ∗ is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner))%I. Definition lty_mutex_guard `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ∃ (γ : gname) (l : loc) (lk : val) (v : val), ⌜ w = PairV lk #l ⌝ ∗ is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗ spin_lock.locked γ ∗ l ↦ v)%I. Instance: Params (@lty_mutex) 3 := {}. Instance: Params (@lty_mutex_guard) 3 := {}. Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope. Notation "'mutex_guard' A" := (lty_mutex_guard A) (at level 10) : lty_scope. Section properties. Context `{heapG Σ, lockG Σ}. Implicit Types A : ltty Σ. Global Instance lty_mutex_contractive : Contractive lty_mutex. Proof. solve_contractive. Qed. Global Instance lty_mutex_ne : NonExpansive lty_mutex. Proof. solve_proper. Qed. Global Instance lty_mutex_guard_contractive : Contractive lty_mutex_guard. Proof. solve_contractive. Qed. Global Instance lty_mutex_guard_ne : NonExpansive lty_mutex_guard. Proof. solve_proper. Qed. Lemma lty_le_mutex A1 A2 : ▷ (A1 <:> A2) -∗ mutex A1 <: mutex A2. Proof. iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (γ l lk ->) "Hinv". iExists γ, l, lk. iSplit; first done. iApply (spin_lock.is_lock_iff with "Hinv"). iIntros "!> !>". iSplit. - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1". - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2". Qed. Lemma lty_copyable_mutex A : ⊢ lty_copyable (mutex A). Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed. Lemma lty_le_mutex_guard A1 A2 : ▷ (A1 <:> A2) -∗ mutex_guard A1 <: mutex_guard A2. Proof. iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (γ l lk w ->) "[Hinv [Hlock Hinner]]". iExists γ, l, lk, w. iSplit; first done. iFrame "Hlock Hinner". iApply (spin_lock.is_lock_iff with "Hinv"). iIntros "!> !>". iSplit. - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1". - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2". Qed. End properties. Section rules. Context `{heapG Σ, lockG Σ}. (** Mutex properties *) Definition mutex_alloc : val := λ: "x", (newlock #(), ref "x"). Lemma ltyped_mutex_alloc A : ⊢ ∅ ⊨ mutex_alloc : A → mutex A. Proof. iIntros (vs) "!> HΓ /=". iApply wp_value. iSplitL; last by iApply env_ltyped_empty. iIntros "!>" (v) "Hv". rewrite /mutex_alloc. wp_pures. wp_alloc l as "Hl". wp_bind (newlock _). set (N := nroot .@ "makelock"). iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I with "[Hl Hv]" as "Hlock". { iExists v. iFrame "Hl Hv". } wp_apply (newlock_spec with "Hlock"). iIntros (lk γ) "Hlock". wp_pures. iExists γ, l, lk. iSplit=> //. Qed. Definition mutex_acquire : val := λ: "x", acquire (Fst "x");; ! (Snd "x"). Lemma ltyped_mutex_acquire Γ (x : string) A : Γ !! x = Some (mutex A)%lty → ⊢ Γ ⊨ mutex_acquire x : A ⫤ <[x := (mutex_guard A)%lty]> Γ. Proof. iIntros (Hx vs) "!> HΓ /=". iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv. rewrite /mutex_acquire. wp_pures. iDestruct "HA" as (γ l lk ->) "#Hlock". wp_bind (acquire _). wp_apply (acquire_spec with "Hlock"). iIntros "[Hlocked Hinner]". iDestruct "Hinner" as (v) "[Hl HA]". wp_pures. wp_load. iFrame "HA". iAssert (ltty_car (mutex_guard A)%lty (lk, #l)) with "[Hlocked Hl]" as "Hguard". { iExists γ, l, lk, v. iSplit=>//. iFrame "Hlocked Hl Hlock". } iDestruct (env_ltyped_insert _ _ x with "Hguard HΓ") as "HΓ". rewrite /binder_insert insert_delete (insert_id _ _ _ Hv). iFrame "HΓ". Qed. Definition mutex_release : val := λ: "guard" "inner", Snd "guard" <- "inner";; release (Fst "guard");; #(). Lemma ltyped_mutex_release Γ Γ' (x : string) e A : Γ' !! x = Some (mutex_guard A)%lty → (Γ ⊨ e : A ⫤ Γ') -∗ Γ ⊨ mutex_release x e : () ⫤ <[x := (mutex A)%lty]> Γ'. Proof. iIntros (Hx) "#He". iIntros (vs) "!> HΓ /=". wp_bind (subst_map vs e). iApply (wp_wand with "(He HΓ)"). iIntros (v) "[HA HΓ']". iDestruct (env_ltyped_lookup with "HΓ'") as (g Hg) "[Hguard HΓ']"; first done; rewrite Hg. iDestruct "Hguard" as (γ l lk inner ->) "(#Hlock & Hlocked & Hinner)". rewrite /mutex_release. wp_pures. wp_store. wp_pures. wp_bind (release _). iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I with "[Hinner HA]" as "Hinner". { iExists v. iFrame "Hinner HA". } wp_apply (release_spec γ _ (∃ inner, l ↦ inner ∗ ltty_car A inner)%I with "[Hlocked Hinner]"). { iFrame "Hlock Hlocked". iDestruct "Hinner" as (w) "[Hl HA]". eauto with iFrame. } iIntros "_". wp_pures. iSplit=> //. iAssert (ltty_car (mutex A)%lty (lk, #l)) with "[Hlock]" as "Hmutex". { iExists γ, l, lk. iSplit=>//. } iDestruct (env_ltyped_insert _ _ x with "Hmutex HΓ'") as "HΓ'". rewrite /binder_insert insert_delete (insert_id _ _ _ Hg). iFrame "HΓ'". Qed. End rules.
 ... ... @@ -236,33 +236,6 @@ Section subtyping_rules. ⊢ lty_copyable (ref_shr A). Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed. Lemma lty_le_mutex A1 A2 : ▷ (A1 <:> A2) -∗ mutex A1 <: mutex A2. Proof. iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (γ l lk ->) "Hinv". iExists γ, l, lk. iSplit; first done. iApply (spin_lock.is_lock_iff with "Hinv"). iIntros "!> !>". iSplit. - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1". - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2". Qed. Lemma lty_copyable_mutex A : ⊢ lty_copyable (mutex A). Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed. Lemma lty_le_mutexguard A1 A2 : ▷ (A1 <:> A2) -∗ mutexguard A1 <: mutexguard A2. Proof. iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (γ l lk w ->) "[Hinv [Hlock Hinner]]". iExists γ, l, lk, w. iSplit; first done. iFrame "Hlock Hinner". iApply (spin_lock.is_lock_iff with "Hinv"). iIntros "!> !>". iSplit. - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1". - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2". Qed. Lemma lty_le_chan S1 S2 : ▷ (S1 <: S2) -∗ chan S1 <: chan S2. ... ...
 ... ... @@ -7,7 +7,7 @@ From actris.channel Require Export channel. Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I). Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, □ ltty_car A w)%I. Definition lty_copy_inv {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)). Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)). Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ := tc_opaque (A <: lty_copy A)%I. ... ... @@ -35,21 +35,11 @@ Definition ref_shrN := nroot .@ "shr_ref". Definition lty_ref_shr `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ∃ l : loc, ⌜w = #l⌝ ∗ inv (ref_shrN .@ l) (∃ v, l ↦ v ∗ ltty_car A v))%I. Definition lty_mutex `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ∃ (γ : gname) (l : loc) (lk : val), ⌜ w = PairV lk #l ⌝ ∗ is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner))%I. Definition lty_mutexguard `{heapG Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ∃ (γ : gname) (l : loc) (lk : val) (v : val), ⌜ w = PairV lk #l ⌝ ∗ is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗ spin_lock.locked γ ∗ l ↦ v)%I. Definition lty_chan `{heapG Σ, chanG Σ} (P : lsty Σ) : ltty Σ := Ltty (λ w, w ↣ lsty_car P)%I. Instance: Params (@lty_copy) 1 := {}. Instance: Params (@lty_copy_inv) 1 := {}. Instance: Params (@lty_copy_minus) 1 := {}. Instance: Params (@lty_copyable) 1 := {}. Instance: Params (@lty_arr) 2 := {}. Instance: Params (@lty_prod) 1 := {}. ... ... @@ -58,14 +48,12 @@ Instance: Params (@lty_forall) 2 := {}. Instance: Params (@lty_sum) 1 := {}. Instance: Params (@lty_ref_mut) 2 := {}. Instance: Params (@lty_ref_shr) 2 := {}. Instance: Params (@lty_mutex) 3 := {}. Instance: Params (@lty_mutexguard) 3 := {}. Instance: Params (@lty_chan) 3 := {}. Notation any := lty_any. Notation "()" := lty_unit : lty_scope. Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope. Notation "'copy-' A" := (lty_copy_inv A) (at level 10) : lty_scope. Notation "'copy-' A" := (lty_copy_minus A) (at level 10) : lty_scope. Notation "A ⊸ B" := (lty_arr A B) (at level 99, B at level 200, right associativity) : lty_scope. ... ... @@ -81,9 +69,6 @@ Notation "∃ A1 .. An , C" := Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : lty_scope. Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope. Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope. Notation "'mutexguard' A" := (lty_mutexguard A) (at level 10) : lty_scope. Notation "'chan' A" := (lty_chan A) (at level 10) : lty_scope. Section term_types. ... ... @@ -92,7 +77,7 @@ Section term_types. Global Instance lty_copy_ne : NonExpansive (@lty_copy Σ). Proof. solve_proper. Qed. Global Instance lty_copy_inv_ne : NonExpansive (@lty_copy_inv Σ). Global Instance lty_copy_minus_ne : NonExpansive (@lty_copy_minus Σ). Proof. solve_proper. Qed. Global Instance lty_copyable_plain A : Plain (lty_copyable A). ... ... @@ -144,17 +129,6 @@ Section term_types. Global Instance lty_ref_shr_ne `{heapG Σ} : NonExpansive lty_ref_shr. Proof. solve_proper. Qed. Global Instance lty_mutex_contractive `{heapG Σ, lockG Σ} : Contractive lty_mutex. Proof. solve_contractive. Qed. Global Instance lty_mutex_ne `{heapG Σ, lockG Σ} : NonExpansive lty_mutex. Proof. solve_proper. Qed. Global Instance lty_mutexguard_contractive `{heapG Σ, lockG Σ} : Contractive lty_mutexguard. Proof. solve_contractive. Qed. Global Instance lty_mutexguard_ne `{heapG Σ, lockG Σ} : NonExpansive lty_mutexguard. Proof. solve_proper. Qed. Global Instance lty_chan_ne `{heapG Σ, chanG Σ} : NonExpansive lty_chan. Proof. solve_proper. Qed. End term_types.
 ... ... @@ -14,19 +14,6 @@ Notation "Γ ⊨ e : A ⫤ Γ'" := (ltyped Γ Γ' e A) Notation "Γ ⊨ e : A" := (Γ ⊨ e : A ⫤ Γ) (at level 100, e at next level, A at level 200). Lemma ltyped_frame `{!heapG Σ} (Γ Γ' Γ1 Γ1' Γ2 : gmap string (ltty Σ)) e A : env_split Γ Γ1 Γ2 -∗ env_split Γ' Γ1' Γ2 -∗ (Γ1 ⊨ e : A ⫤ Γ1') -∗ Γ ⊨ e : A ⫤ Γ'. Proof. iIntros "#Hsplit #Hsplit' #Htyped !>" (vs) "Henv". iDestruct ("Hsplit" with "Henv") as "[Henv1 Henv2]". iApply (wp_wand with "(Htyped Henv1)"). iIntros (v) "[\$ Henv1']". iApply "Hsplit'". iFrame "Henv1' Henv2". Qed. Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' : (∀ `{heapG Σ}, ∃ A Γ', ⊢ ∅ ⊨ e : A ⫤ Γ') → rtc erased_step ([e], σ) (es, σ') → e' ∈ es → ... ...
 ... ... @@ -14,6 +14,20 @@ Section properties. Implicit Types S T : lsty Σ. Implicit Types Γ : gmap string (ltty Σ). (** Frame rule *) Lemma ltyped_frame `{!heapG Σ} (Γ Γ' Γ1 Γ1' Γ2 : gmap string (ltty Σ)) e A : env_split Γ Γ1 Γ2 -∗ env_split Γ' Γ1' Γ2 -∗ (Γ1 ⊨ e : A ⫤ Γ1') -∗ Γ ⊨ e : A ⫤ Γ'. Proof. iIntros "#Hsplit #Hsplit' #Htyped !>" (vs) "Henv". iDestruct ("Hsplit" with "Henv") as "[Henv1 Henv2]". iApply (wp_wand with "(Htyped Henv1)"). iIntros (v) "[\$ Henv1']". iApply "Hsplit'". iFrame "Henv1' Henv2". Qed. (** Variable properties *) Lemma ltyped_var Γ (x : string) A : Γ !! x = Some A → ⊢ Γ ⊨ x : A ⫤ <[x := (copy- A)%lty]> Γ. ... ... @@ -73,9 +87,9 @@ Section properties. Qed. (* Typing rule for introducing copyable functions *) Lemma ltyped_rec Γ Γ' f x e A1 A2 : Lemma ltyped_rec Γ Γ' Γ'' f x e A1 A2 : env_copy Γ Γ' -∗ (binder_insert f (A1 → A2)%lty (binder_insert x A1 Γ') ⊨ e : A2) -∗ (binder_insert f (A1 → A2)%lty (binder_insert x A1 Γ') ⊨ e : A2 ⫤ Γ'') -∗ Γ ⊨ (rec: f x := e) : A1 → A2 ⫤ ∅. Proof. iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures. ... ... @@ -114,45 +128,6 @@ Section properties. iApply env_ltyped_delete=> //. Qed. Fixpoint lty_arr_list (As : list (ltty Σ)) (B : ltty Σ) : ltty Σ := match As with | [] => B | A :: As => A ⊸ lty_arr_list As B end. Lemma lty_arr_list_spec_step A As (e : expr) B ws y i : (∀ v, ltty_car A v -∗ WP subst_map (<[y+:+pretty i:=v]> ws) (switch_lams y (S i) (length As) e) {{ ltty_car (lty_arr_list As B) }}) -∗ WP subst_map ws (switch_lams y i (S (length As)) e) {{ ltty_car (lty_arr_list (A :: As) B) }}. Proof. iIntros "H". wp_pures. iIntros (v) "HA". iDestruct ("H" with "HA") as "H". rewrite subst_map_insert. wp_apply "H". Qed. Lemma lty_arr_list_spec As (e : expr) B ws y i n : n = length As → (∀ vs, ([∗ list] A;v ∈ As;vs, ltty_car A v) -∗ WP subst_map (map_string_seq y i vs ∪ ws) e {{ ltty_car B }}) -∗ WP subst_map ws (switch_lams y i n e) {{ ltty_car (lty_arr_list As B) }}. Proof. iIntros (Hlen) "H". iInduction As as [|A As] "IH" forall (ws i e n Hlen); simplify_eq/=. - iDestruct ("H" \$! [] with "[\$]") as "H"=> /=. by rewrite left_id_L. - iApply lty_arr_list_spec_step. iIntros (v) "HA". iApply ("IH" with "[//]"). iIntros (vs) "HAs". iSpecialize ("H" \$! (v::vs)); simpl. do 2 rewrite insert_union_singleton_l. rewrite (map_union_comm ({[y +:+ pretty i := v]})); last first. { apply map_disjoint_singleton_l_2. apply lookup_map_string_seq_None_lt. eauto. } rewrite assoc_L. iApply ("H" with "[\$HA \$HAs]"). Qed. (** Product properties *) Lemma ltyped_pair Γ1 Γ2 Γ3 e1 e2 A1 A2 : (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗ (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗ ... ... @@ -164,19 +139,38 @@ Section properties. wp_pures. iFrame "HΓ". iExists w1, w2. by iFrame. Qed. Definition split : val := λ: "pair" "f", "f" (Fst "pair") (Snd "pair"). Lemma ltyped_fst Γ A1 A2 (x : string) : Γ !! x = Some (A1 * A2)%lty → ⊢ Γ ⊨ Fst x : A1 ⫤ <[x := (copy- A1 * A2)%lty]> Γ. Proof. iIntros (Hx vs) "!> HΓ /=". iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv. iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures. iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m". { iApply coreP_intro. iApply "HA1". } iFrame "HA1". iAssert (ltty_car (copy- A1 * A2) (v1, v2))%lty with "[HA2]" as "HA". { iExists v1, v2. iSplit=>//. iFrame "HA1m HA2". } iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ". rewrite /binder_insert insert_delete (insert_id _ _ _ Hv). iFrame "HΓ". Qed. Lemma ltyped_split A1 A2 B : ⊢ ∅ ⊨ split : A1 * A2 → (A1 ⊸ A2 ⊸ B) ⊸ B. Lemma ltyped_snd Γ A1 A2 (x : string) : Γ !! x = Some (A1 * A2)%lty → ⊢ Γ ⊨ Snd x : A2 ⫤ <[x := (A1 * copy- A2)%lty]> Γ. Proof. iIntros (vs) "!> HΓ /=". iApply wp_value. iSplitL; last by iApply env_ltyped_empty. iIntros "!>" (v) "Hv". rewrite /split. wp_pures. iDestruct "Hv" as (w1 w2 ->) "[Hw1 Hw2]". iIntros (f) "Hf". wp_pures. iPoseProof ("Hf" with "Hw1") as "Hf". wp_apply (wp_wand with "Hf"). iIntros (g) "Hg". iApply ("Hg" with "Hw2"). iIntros (Hx vs) "!> HΓ /=". iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv. iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures. iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m". { iApply coreP_intro. iApply "HA2". } iFrame "HA2". iAssert (ltty_car (A1 * copy- A2) (v1, v2))%lty with "[HA1]" as "HA". { iExists v1, v2. iSplit=>//. iFrame "HA2m HA1". } iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ". rewrite /binder_insert insert_delete (insert_id _ _ _ Hv). iFrame "HΓ". Qed. (** Sum Properties *) ... ... @@ -247,7 +241,6 @@ Section properties. wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB \$]". by iExists M. Qed. (* TODO(TYRULES) *) Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 (x : string) e (C : lty Σ k → ltty Σ) A : Γ1 !! x = Some (lty_exist C) → (∀ X, binder_insert x (C X) Γ1 ⊨ e : A ⫤ Γ2) -∗ ... ... @@ -313,175 +306,116 @@ Section properties. Qed. (** Weak Reference properties *) Definition fetch_and_add : val := λ: "r" "inc", FAA "r" "inc". Lemma ltyped_fetch_and_add : ⊢ ∅ ⊨ fetch_and_add : ref_shr lty_int → lty_int → lty_int. Lemma ltyped_upgrade_shared Γ Γ' e A : (Γ ⊨ e : ref_mut A ⫤ Γ') -∗ Γ ⊨ e : ref_shr A ⫤ Γ'. Proof. iIntros (vs) "!> _ /=". iApply wp_value. iSplitL; last by iApply env_ltyped_empty. iIntros "!>" (r) "Hr". iApply wp_fupd. rewrite /fetch_and_add; wp_pures. iDestruct "Hr" as (l ->) "Hr". iMod (fupd_mask_mono with "Hr") as "#Hr"; first done. iIntros "!> !>" (inc) "Hinc". wp_pures. iDestruct "Hinc" as %[k ->]. iInv (ref_shrN .@ l) as (n) "[>Hl >Hn]" "Hclose". iDestruct "Hn" as %[m ->]. wp_faa. iMod ("Hclose" with "[Hl]") as %_. { iExists #(m + k). iFrame "Hl". by iExists (m + k)%Z. } by iExists m. iIntros "#He" (vs) "!> HΓ". iApply wp_fupd. iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv HΓ']". iDestruct "Hv" as (l w ->) "[Hl HA]". iFrame "HΓ'". iExists l. iMod (inv_alloc (ref_shrN .@ l) _ (∃ v : val, l ↦ v ∗ ltty_car A v) with "[Hl HA]") as "Href". { iExists w. iFrame "Hl HA". } iModIntro. by iFrame "Href". Qed. (* TODO(COPY) *) (* Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} : *) (* ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A). *) (* Proof. *) (* iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr". *) (* iApply wp_fupd. rewrite /load; wp_pures. *) (* iDestruct "Hr" as (l ->) "Hr". *) (* iMod (fupd_mask_mono with "Hr") as "#Hr"; first done. *) (* wp_bind (!#l)%E. *) (* iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose". *) (* wp_load. *) (* iMod ("Hclose" with "[Hl HA]") as "_". *) (* { iExists v. iFrame "Hl HA". } *) (* iIntros "!>". wp_pures. iIntros "!>". *) (* iExists _, _. *) (* iSplit; first done. *) (* iFrame "HA". *) (* iExists _. *) (* iSplit; first done. *) (* by iFrame "Hr". *) (* Qed. *) Lemma ltyped_ref_shrstore A : ⊢ ∅ ⊨ store : ref_shr A → A → ref_shr A. Lemma ltyped_load_shared Γ Γ' e A : (Γ ⊨ e : ref_shr A ⫤ Γ') -∗ Γ ⊨ ! e : copy- A ⫤ Γ'. Proof. iIntros (vs) "!> _ /=". iApply wp_value. iSplitL; last by iApply env_ltyped_empty. iIntros "!>" (r) "Hr". iApply wp_fupd. rewrite /store; wp_pures. iDestruct "Hr" as (l ->) "#Hr". iIntros "!> !>" (x) "HA". wp_pures. wp_bind (_ <- _)%E. iInv (ref_shrN .@ l) as (v) "[>Hl _]" "Hclose". wp_store. iMod ("Hclose" with "[Hl HA]") as "_". { iExists x. iFrame "Hl HA". } iModIntro. wp_pures. iExists _. iSplit; first done. by iFrame "Hr". iIntros "#He" (vs) "!> HΓ /=". wp_bind (subst_map vs e). iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv HΓ]". iDestruct "Hv" as (l ->) "#Hv". iInv (ref_shrN .@ l) as (v) "[>Hl HA]" "Hclose". wp_load. iAssert (ltty_car (copy- A) v)%lty as "#HAm". { iApply coreP_intro. iApply "HA". } iMod ("Hclose" with "[Hl HA]") as "_". { iExists v. iFrame "Hl HA". } iModIntro. iFrame "HAm HΓ". Qed. Section with_lock. Context `{lockG Σ}. (** Mutex properties *) Definition mutexalloc : val := λ: "x", (newlock #(), ref "x"). Lemma ltyped_mutexalloc A : ⊢ ∅ ⊨ mutexalloc : A → mutex A. Proof. iIntros (vs) "!> HΓ /=". iApply wp_value. iSplitL; last by iApply env_ltyped_empty. iIntros "!>" (v) "Hv". rewrite /mutexalloc. wp_pures. wp_alloc l as "Hl". wp_bind (newlock _). set (N := nroot .@ "makelock"). iAssert (∃ inner, l ↦ inner ∗ ltty_car A inner)%I with "[Hl Hv]" as "Hlock". { iExists v. iFrame "Hl Hv". } wp_apply (newlock_spec with "Hlock"). iIntros (lk γ) "Hlock". wp_pures. iExists γ, l, lk. iSplit=> //. Qed. Definition mutexacquire : val := λ: "x", acquire (Fst "x");; (! (Snd "x"), "x"). Lemma ltyped_mutexacquire A : ⊢ ∅ ⊨ mutexacquire : mutex A → A * mutexguard A. Proof. iIntros (vs) "!> HΓ /=". iApply wp_value. iSplitL; last by iApply env_ltyped_empty. iIntros "!>" (m) "Hm". rewrite /mutexacquire. wp_pures. iDestruct "Hm" as (γ l lk ->) "Hlock". iMod (fupd_mask_mono with "Hlock") as "#Hlock"; first done. wp_bind (acquire _). wp_apply (acquire_spec with "Hlock"). iIntros "[Hlocked Hinner]". wp_pures. iDestruct "Hinner" as (v) "[Hl HA]". wp_load. wp_pures. iExists v, (lk, #l)%V. iSplit=> //. iFrame "HA".