diff --git a/_CoqProject b/_CoqProject
index 033fbd5de6c5b0189b71cab7a402acb849240858..0846fe89bed10771af6d3617ab9c0aaa3c59b138 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -22,5 +22,6 @@ theories/logrel/lsty.v
theories/logrel/session_types.v
theories/logrel/types.v
theories/logrel/subtyping.v
+theories/logrel/copying.v
theories/logrel/examples/double.v
theories/logrel/examples/pair.v
diff --git a/theories/logrel/copying.v b/theories/logrel/copying.v
new file mode 100644
index 0000000000000000000000000000000000000000..acc00305d90dcbe6443d29cfb82dc2684b07179c
--- /dev/null
+++ b/theories/logrel/copying.v
@@ -0,0 +1,211 @@
+From actris.logrel Require Import ltyping types subtyping.
+From actris.channel Require Import channel.
+From iris.base_logic.lib Require Import invariants.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import notation proofmode.
+From iris.bi.lib Require Export core.
+
+(* TODO: Coq fails to infer what the Σ should be if I move some of these
+definitions out of the section or into a different section with its own Context
+declaration. *)
+
+Section copying.
+ Context `{heapG Σ, chanG Σ}.
+ Implicit Types A : lty Σ.
+ Implicit Types S : lsty Σ.
+
+ (* We define the copyability of semantic types in terms of subtyping. *)
+ Definition copyable (A : lty Σ) : iProp Σ :=
+ A <: copy A.
+
+ (* Subtyping for `copy` and `copy-` *)
+ Lemma lty_le_copy A :
+ ⊢ copy A <: A.
+ Proof. by iIntros (v) "!> #H". Qed.
+
+ (* TODO(COPY): have A <: copy- A rule *)
+ (* TODO(COPY): Show derived rules about copyability of products, sums, etc. *)
+ (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
+
+ (* TODO(COPY) *)
+ Lemma coreP_desired_lemma (P : iProp Σ) :
+ □ (P -∗ □ P) -∗ coreP P -∗ P.
+ Proof.
+ iIntros "HP Hcore".
+ Admitted.
+
+ Lemma lty_le_copy_minus A :
+ copyable A -∗ copy- A <: A.
+ Proof.
+ iIntros "#HA". iIntros (v) "!> #Hv".
+ iSpecialize ("HA" $! v).
+ iApply coreP_desired_lemma.
+ - iModIntro. iApply "HA".
+ - iApply "Hv".
+ Qed.
+
+ (* Copyability of types *)
+ Lemma lty_unit_copyable :
+ ⊢ copyable ().
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+ Lemma lty_bool_copyable :
+ ⊢ copyable lty_bool.
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+ Lemma lty_int_copyable :
+ ⊢ copyable lty_int.
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+ (* TODO: Use Iris quantification here instead of Coq quantification? (Or doesn't matter?) *)
+ Lemma lty_copy_copyable A :
+ ⊢ copyable (copy A).
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+ Lemma lty_copyminus_copyable A :
+ ⊢ copyable (copy- A).
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+ Lemma lty_any_copyable :
+ ⊢ copyable any.
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+ Lemma lty_ref_shr_copyable A :
+ ⊢ copyable (ref_shr A).
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+ Lemma lty_mutex_copyable A :
+ ⊢ copyable (mutex A).
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+ (* Rules about combining `copy` and other type formers *)
+ Lemma lty_prod_copy_comm A B :
+ ⊢ copy A * copy B <:> copy (A * B).
+ Proof.
+ iSplit; iModIntro; iIntros (v) "#Hv"; iDestruct "Hv" as (v1 v2 ->) "[Hv1 Hv2]".
+ - iModIntro. iExists v1, v2. iSplit=>//. iSplitL; iModIntro; auto.
+ - iExists v1, v2. iSplit=>//. iSplit; iModIntro; iModIntro; auto.
+ Qed.
+
+ Lemma lty_sum_copy_comm A B :
+ ⊢ copy A + copy B <:> copy (A + B).
+ Proof.
+ iSplit; iModIntro; iIntros (v) "#Hv";
+ iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[Heq Hw]";
+ try iModIntro.
+ - iLeft. iExists w. iFrame "Heq". iModIntro. iApply "Hw".
+ - iRight. iExists w. iFrame "Heq". iModIntro. iApply "Hw".
+ - iLeft. iExists w. iFrame "Heq". iModIntro. iModIntro. iApply "Hw".
+ - iRight. iExists w. iFrame "Heq". iModIntro. iModIntro. iApply "Hw".
+ Qed.
+
+ Lemma lty_exist_copy_comm F :
+ ⊢ (∃ A, copy (F A)) <:> copy (∃ A, F A).
+ Proof.
+ iSplit; iModIntro; iIntros (v) "#Hv";
+ iDestruct "Hv" as (A) "Hv"; try iModIntro;
+ iExists A; repeat iModIntro; iApply "Hv".
+ Qed.
+
+ (* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
+
+ (* Copyability of recursive types *)
+ Lemma lty_rec_copy C `{!Contractive C} :
+ □ (∀ A, ▷ copyable A -∗ copyable (C A)) -∗ copyable (lty_rec C).
+ Proof.
+ iIntros "#Hcopy".
+ iLöb as "IH".
+ iIntros (v) "!> Hv".
+ rewrite /lty_rec.
+ rewrite {2}fixpoint_unfold.
+ iSpecialize ("Hcopy" with "IH").
+ rewrite {3}/lty_rec_aux.
+ iSpecialize ("Hcopy" with "Hv").
+ iDestruct "Hcopy" as "#Hcopy".
+ iModIntro.
+ iEval (rewrite fixpoint_unfold).
+ iApply "Hcopy".
+ Qed.
+
+ (* TODO: Get rid of side condition that x does not appear in Γ *)
+ Lemma env_split_copy Γ Γ1 Γ2 (x : string) A:
+ Γ !! x = None → Γ1 !! x = None → Γ2 !! x = None →
+ copyable A -∗
+ env_split Γ Γ1 Γ2 -∗
+ env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2).
+ Proof.
+ iIntros (HΓx HΓ1x HΓ2x) "#Hcopy #Hsplit". iIntros (vs) "!>".
+ iSplit.
+ - iIntros "HΓ".
+ iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
+ iDestruct "Hv" as (v ?) "HAv2".
+ iDestruct ("Hcopy" with "HAv2") as "#HAv".
+ iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
+ iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto.
+ - iIntros "[HΓ1 HΓ2]".
+ iPoseProof (big_sepM_insert with "HΓ1") as "[Hv HΓ1]"; first by assumption.
+ iPoseProof (big_sepM_insert with "HΓ2") as "[_ HΓ2]"; first by assumption.
+ iApply (big_sepM_insert_2 with "[Hv]")=> //.
+ iApply "Hsplit". iFrame "HΓ1 HΓ2".
+ Qed.
+
+ Definition env_copy (Γ Γ' : gmap string (lty Σ)) : iProp Σ :=
+ □ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs.
+
+ Lemma env_copy_empty : ⊢ env_copy ∅ ∅.
+ Proof. iIntros (vs) "!> _ !> ". by rewrite /env_ltyped. Qed.
+
+ Lemma env_copy_extend x A Γ Γ' :
+ Γ !! x = None →
+ env_copy Γ Γ' -∗
+ env_copy (<[x:=A]> Γ) Γ'.
+ Proof.
+ iIntros (HΓ) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
+ iDestruct (big_sepM_insert with "Hvs") as "[_ Hvs]"; first by assumption.
+ iApply ("Hcopy" with "Hvs").
+ Qed.
+
+ Lemma env_copy_extend_copy x A Γ Γ' :
+ Γ !! x = None →
+ Γ' !! x = None →
+ copyable A -∗
+ env_copy Γ Γ' -∗
+ env_copy (<[x:=A]> Γ) (<[x:=A]> Γ').
+ Proof.
+ iIntros (HΓx HΓ'x) "#HcopyA #Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
+ iDestruct (big_sepM_insert with "Hvs") as "[HA Hvs]"; first done.
+ iDestruct ("Hcopy" with "Hvs") as "#Hvs'".
+ iDestruct "HA" as (v ?) "HA2".
+ iDestruct ("HcopyA" with "HA2") as "#HA".
+ iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto.
+ Qed.
+
+ (* TODO: Maybe move this back to `typing.v` (requires restructuring to avoid
+ circular dependencies). *)
+ (* Typing rule for introducing copyable functions *)
+
+ Lemma ltyped_rec Γ Γ' f x e A1 A2 :
+ env_copy Γ Γ' -∗
+ (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.
+ iDestruct ("Hcopy" with "HΓ") as "HΓ".
+ iMod (fupd_mask_mono with "HΓ") as "#HΓ"; first done.
+ iModIntro. iSplitL; last by iApply env_ltyped_empty.
+ iLöb as "IH".
+ iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
+ iDestruct ("He" $!(binder_insert f r (binder_insert x v vs))
+ with "[HΓ HA1]") as "He'".
+ { iApply (env_ltyped_insert with "IH").
+ iApply (env_ltyped_insert with "HA1 HΓ"). }
+ iDestruct (wp_wand _ _ _ _ (λ v, A2 v) with "He' []") as "He'".
+ { iIntros (w) "[$ _]". }
+ destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
+ destruct (decide (x = f)) as [->|].
+ - by rewrite subst_subst delete_idemp !insert_insert -subst_map_insert.
+ - rewrite subst_subst_ne // -subst_map_insert.
+ by rewrite -delete_insert_ne // -subst_map_insert.
+ Qed.
+
+End copying.
diff --git a/theories/logrel/ltyping.v b/theories/logrel/ltyping.v
index ba5810713f167f6d257a2960b5d5d3cde097698a..f5f5934b67d257565f7a84eaf63d2327aa8ca285 100755
--- a/theories/logrel/ltyping.v
+++ b/theories/logrel/ltyping.v
@@ -52,10 +52,6 @@ Class LTyUnOp {Σ} (op : un_op) (A B : lty Σ) :=
Class LTyBinOp {Σ} (op : bin_op) (A1 A2 B : lty Σ) :=
lty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌠∗ B w.
-(* Copy types *)
-Class LTyCopy `{invG Σ} (A : lty Σ) :=
- lty_copy_pers v :> Persistent (A v).
-
Section Environment.
Context `{invG Σ}.
Implicit Types A : lty Σ.
@@ -160,57 +156,6 @@ Section Environment.
by iApply env_split_comm.
Qed.
- (* TODO: Get rid of side condition that x does not appear in Γs *)
- Lemma env_split_copy Γ Γ1 Γ2 (x : string) A:
- Γ !! x = None → Γ1 !! x = None → Γ2 !! x = None →
- LTyCopy A →
- env_split Γ Γ1 Γ2 -∗
- env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2).
- Proof.
- iIntros (HΓx HΓ1x HΓ2x Hcopy) "#Hsplit". iIntros (vs) "!>".
- iSplit.
- - iIntros "HΓ".
- iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
- iDestruct "Hv" as (v ?) "#HAv".
- iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
- iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto.
- - iIntros "[HΓ1 HΓ2]".
- iPoseProof (big_sepM_insert with "HΓ1") as "[Hv HΓ1]"; first by assumption.
- iPoseProof (big_sepM_insert with "HΓ2") as "[_ HΓ2]"; first by assumption.
- iApply (big_sepM_insert_2 with "[Hv]")=> //.
- iApply "Hsplit". iFrame "HΓ1 HΓ2".
- Qed.
-
- (* TODO: Prove lemmas about this *)
- Definition env_copy (Γ Γ' : gmap string (lty Σ)) : iProp Σ :=
- □ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs.
-
- Lemma env_copy_empty : ⊢ env_copy ∅ ∅.
- Proof. iIntros (vs) "!> _ !> ". by rewrite /env_ltyped. Qed.
-
- Lemma env_copy_extend x A Γ Γ' :
- Γ !! x = None →
- env_copy Γ Γ' -∗
- env_copy (<[x:=A]> Γ) Γ'.
- Proof.
- iIntros (HΓ) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
- iDestruct (big_sepM_insert with "Hvs") as "[_ Hvs]"; first by assumption.
- iApply ("Hcopy" with "Hvs").
- Qed.
-
- Lemma env_copy_extend_copy x A Γ Γ' :
- Γ !! x = None →
- Γ' !! x = None →
- LTyCopy A →
- env_copy Γ Γ' -∗
- env_copy (<[x:=A]> Γ) (<[x:=A]> Γ').
- Proof.
- iIntros (HΓx HΓ'x HcopyA) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
- iDestruct (big_sepM_insert with "Hvs") as "[HA Hvs]"; first done.
- iDestruct ("Hcopy" with "Hvs") as "#Hvs'".
- iDestruct "HA" as (v ?) "#HA".
- iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto.
- Qed.
End Environment.
(* The semantic typing judgement *)
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 7c4629991955d758f90f83db5363d19c3dae3188..dfb5b60bf0c5e367e2790aa102d374212b731c6e 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -61,11 +61,12 @@ Section subtype.
Lemma lty_bi_le_sym A1 A2 : A1 <:> A2 -∗ A2 <:> A1.
Proof. iIntros "[$$]". Qed.
- Lemma lty_le_copy A : ⊢ copy A <: A.
- Proof. by iIntros (v) "!> #H". Qed.
-
- Lemma lty_le_copyable A `{LTyCopy Σ A} : ⊢ A <: copy A.
- Proof. by iIntros (v) "!> #H". Qed.
+ Lemma lty_le_copy A B :
+ A <: B -∗ copy A <: copy B.
+ Proof.
+ iIntros "#Hsub". iIntros (v) "!> #HA !>".
+ iApply ("Hsub" with "HA").
+ Qed.
Lemma lty_le_arr A11 A12 A21 A22 :
▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 41c4c543e24cdf9632ca636729ad6d48da260aa3..5925e5670d0f0571dc38b6afc78063d3ed9eb523 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -2,6 +2,7 @@ From stdpp Require Import pretty.
From actris.utils Require Import switch.
From actris.logrel Require Export ltyping session_types.
From actris.channel Require Import proto proofmode.
+From iris.bi.lib Require Export core.
From iris.heap_lang Require Export lifting metatheory.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang.lib Require Import assert.
@@ -14,6 +15,7 @@ Section types.
Definition lty_bool : lty Σ := Lty (λ w, ∃ b : bool, ⌜ w = #b âŒ)%I.
Definition lty_int : lty Σ := Lty (λ w, ∃ n : Z, ⌜ w = #n âŒ)%I.
Definition lty_copy (A : lty Σ) : lty Σ := Lty (λ w, □ (A w))%I.
+ Definition lty_copyminus (A : lty Σ) : lty Σ := Lty (λ w, coreP (A w)).
Definition lty_arr (A1 A2 : lty Σ) : lty Σ := Lty (λ w,
∀ v, ▷ A1 v -∗ WP w v {{ A2 }})%I.
(* TODO: Make a non-linear version of prod, using ∧ *)
@@ -55,6 +57,7 @@ End types.
Notation "()" := lty_unit : lty_scope.
Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
+Notation "'copy-' A" := (lty_copyminus A) (at level 10) : lty_scope.
Notation "A → B" := (lty_copy (lty_arr A B)) : lty_scope.
Notation "A ⊸ B" := (lty_arr A B) (at level 99, B at level 200, right associativity) : lty_scope.
Infix "*" := lty_prod : lty_scope.
@@ -86,16 +89,10 @@ Section properties.
(** Basic properties *)
Global Instance lty_unit_unboxed : @LTyUnboxed Σ ().
Proof. by iIntros (v ->). Qed.
- Global Instance lty_unit_copy : @LTyCopy Σ _ ().
- Proof. iIntros (v). apply _. Qed.
Global Instance lty_bool_unboxed : @LTyUnboxed Σ lty_bool.
Proof. iIntros (v). by iDestruct 1 as (b) "->". Qed.
- Global Instance lty_bool_copy : @LTyCopy Σ _ lty_bool.
- Proof. iIntros (v). apply _. Qed.
Global Instance lty_int_unboxed : @LTyUnboxed Σ lty_int.
Proof. iIntros (v). by iDestruct 1 as (i) "->". Qed.
- Global Instance lty_int_copy : @LTyCopy Σ _ lty_int.
- Proof. iIntros (v). apply _. Qed.
Lemma ltyped_unit Γ : ⊢ Γ ⊨ #() : ().
Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed.
@@ -152,9 +149,6 @@ Section properties.
Global Instance lty_copy_ne : NonExpansive (@lty_copy Σ).
Proof. solve_proper. Qed.
- Global Instance lty_copy_copy A : LTyCopy (copy A).
- Proof. iIntros (v). apply _. Qed.
-
(** Arrow properties *)
Global Instance lty_arr_contractive n :
Proper (dist_later n ==> dist_later n ==> dist n) lty_arr.
@@ -207,30 +201,6 @@ Section properties.
Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ ∅.
Proof. iIntros "#He1 #He2". iApply ltyped_app=> //. by iApply ltyped_lam. Qed.
- Lemma ltyped_rec Γ Γ' f x e A1 A2 :
- env_copy Γ Γ' -∗
- (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.
- iDestruct ("Hcopy" with "HΓ") as "HΓ".
- iMod (fupd_mask_mono with "HΓ") as "#HΓ"; first done.
- iModIntro. iSplitL; last by iApply env_ltyped_empty.
- iLöb as "IH".
- iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
- iDestruct ("He" $!(binder_insert f r (binder_insert x v vs))
- with "[HΓ HA1]") as "He'".
- { iApply (env_ltyped_insert with "IH").
- iApply (env_ltyped_insert with "HA1 HΓ"). }
- iDestruct (wp_wand _ _ _ _ (λ v, A2 v) with "He' []") as "He'".
- { iIntros (w) "[$ _]". }
- destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
- destruct (decide (x = f)) as [->|].
- - by rewrite subst_subst delete_idemp !insert_insert -subst_map_insert.
- - rewrite subst_subst_ne // -subst_map_insert.
- by rewrite -delete_insert_ne // -subst_map_insert.
- Qed.
-
Fixpoint lty_arr_list (As : list (lty Σ)) (B : lty Σ) : lty Σ :=
match As with
| [] => B
@@ -274,8 +244,6 @@ Section properties.
Qed.
(** Product properties *)
- Global Instance lty_prod_copy `{!LTyCopy A1, !LTyCopy A2} : LTyCopy (A1 * A2).
- Proof. iIntros (v). apply _. Qed.
Global Instance lty_prod_contractive n:
Proper (dist_later n ==> dist_later n ==> dist n) (@lty_prod Σ).
Proof. solve_contractive. Qed.
@@ -308,8 +276,6 @@ Section properties.
Qed.
(** Sum Properties *)
- Global Instance lty_sum_copy `{!LTyCopy A1, !LTyCopy A2} : LTyCopy (A1 + A2).
- Proof. iIntros (v). apply _. Qed.
Global Instance lty_sum_contractive n :
Proper (dist_later n ==> dist_later n ==> dist n) (@lty_sum Σ).
Proof. solve_contractive. Qed.
@@ -409,10 +375,6 @@ Section properties.
Qed.
(** Existential properties *)
- Global Instance lty_exist_copy C (Hcopy : ∀ A, LTyCopy (C A)) :
- (LTyCopy (lty_exist C)).
- Proof. intros v. apply bi.exist_persistent. intros A.
- apply bi.later_persistent. apply Hcopy. Qed.
Global Instance lty_exist_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ).
Proof. solve_proper. Qed.
@@ -420,10 +382,6 @@ Section properties.
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ).
Proof. solve_contractive. Qed.
- Global Instance lty_exist_lsty_copy C (Hcopy : ∀ A, LTyCopy (C A)) :
- (LTyCopy (lty_exist_lsty C)).
- Proof. intros v. apply bi.exist_persistent. intros A.
- apply bi.later_persistent. apply Hcopy. Qed.
Global Instance lty_exist_lsty_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist_lsty Σ).
Proof. solve_proper. Qed.
@@ -514,19 +472,19 @@ Section properties.
by iModIntro.
Qed.
- Lemma ltyped_load_copy A {copyA : LTyCopy A} :
- ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut A.
- Proof.
- iIntros (vs) "!> HΓ /=".
- iApply wp_value.
- iSplitL; last by iApply env_ltyped_empty.
- iIntros "!>" (v) "Hv". rewrite /load. wp_pures.
- iDestruct "Hv" as (l w ->) "[Hl #Hw]".
- wp_load. wp_pures.
- iExists w, #l. iSplit=> //. iFrame "Hw".
- iExists l, w. iSplit=> //. iFrame "Hl".
- by iModIntro.
- Qed.
+ (* TODO(COPY) *)
+ (* Lemma ltyped_load_copy A {copyA : LTyCopy A} : *)
+ (* ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut A. *)
+ (* Proof. *)
+ (* iIntros (vs) "!> HΓ /=". *)
+ (* iApply wp_value. *)
+ (* iIntros "!>" (v) "Hv". rewrite /load. wp_pures. *)
+ (* iDestruct "Hv" as (l w ->) "[Hl #Hw]". *)
+ (* wp_load. wp_pures. *)
+ (* iExists w, #l. iSplit=> //. iFrame "Hw". *)
+ (* iExists l, w. iSplit=> //. iFrame "Hl". *)
+ (* by iModIntro. *)
+ (* Qed. *)
Definition store : val := λ: "r" "new", "r" <- "new";; "r".
@@ -548,8 +506,6 @@ Section properties.
Proof. solve_proper. Qed.
Global Instance lty_ref_shr_unboxed A : LTyUnboxed (ref_shr A).
Proof. iIntros (v). by iDestruct 1 as (l ->) "?". Qed.
- Global Instance lty_ref_shr_copy A : LTyCopy (ref_shr A).
- Proof. iIntros (v). apply _. Qed.
Definition fetch_and_add : val := λ: "r" "inc", FAA "r" "inc".
Lemma ltyped_fetch_and_add :
@@ -570,28 +526,27 @@ Section properties.
by iExists m.
Qed.
- Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} :
- ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A).
- Proof.
- iIntros (vs) "!> _ /=". iApply wp_value.
- iSplitL; last by iApply env_ltyped_empty.
- 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.
+ (* 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 : lty Σ) :
⊢ ∅ ⊨ store : ref_shr A → A → ref_shr A.