Make type in shared ref copy.

theories/logrel/subtyping_rules.v

@@ -229,14 +229,13 @@ Section subtyping_rules.
     iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (l ->) "Hinv".
     iExists l. iSplit; first done.
     iApply (inv_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".
+    - iDestruct 1 as (v) "[Hl #HA]". iExists v. iIntros "{$Hl} !>". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl #HA]". iExists v. iIntros "{$Hl} !>". by iApply "Hle2".
   Qed.
   Lemma lty_copyable_shr_ref A :
     ⊢ lty_copyable (ref_shr A).
   Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
 
-
   Lemma lty_le_chan S1 S2 :
     ▷ (S1 <: S2) -∗ chan S1 <: chan S2.
   Proof.

theories/logrel/term_types.v

@@ -33,7 +33,7 @@ Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
   ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I.
 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.
+  ∃ l : loc, ⌜w = #l⌝ ∗ inv (ref_shrN .@ l) (∃ v, l ↦ v ∗ □ ltty_car A v))%I.
 
 Definition lty_chan `{heapG Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
   Ltty (λ w, w ↣ lsty_car P)%I.

theories/logrel/term_typing_rules.v

@@ -306,40 +306,35 @@ Section properties.
 
   (** Weak Reference properties *)
   Lemma ltyped_upgrade_shared  Γ Γ' e A :
-    (Γ ⊨ e : ref_mut A ⫤ Γ') -∗
+    (Γ ⊨ e : ref_mut (copy A) ⫤ Γ') -∗
     Γ ⊨ e : ref_shr A ⫤ Γ'.
   Proof.
-    iIntros "#He" (vs) "!> HΓ".
-    iApply wp_fupd.
+    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".
+    iFrame "HΓ'". iExists l.
+    iMod (inv_alloc (ref_shrN .@ l) _
+      (∃ v : val, l ↦ v ∗ □ ltty_car A v) with "[Hl HA]") as "$"; last done.
+    iExists w. iFrame "Hl HA".
   Qed.
 
   Lemma ltyped_load_shared Γ Γ' e A :
     (Γ ⊨ e : ref_shr A ⫤ Γ') -∗
-    Γ ⊨ ! e : copy- A ⫤ Γ'.
+    Γ ⊨ ! e : A ⫤ Γ'.
   Proof.
     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".
+    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Γ".
+    by iIntros "!> {$HΓ}".
   Qed.
 
   Lemma ltyped_store_shared Γ1 Γ2 Γ3 e1 e2 A :
-    (Γ1 ⊨ e2 : A ⫤ Γ2) -∗
+    (Γ1 ⊨ e2 : copy A ⫤ Γ2) -∗
     (Γ2 ⊨ e1 : ref_shr A ⫤ Γ3) -∗
     (Γ1 ⊨ e1 <- e2 : () ⫤ Γ3).
   Proof.
@@ -353,7 +348,7 @@ Section properties.
     wp_store.
     iMod ("Hclose" with "[Hl Hv]") as "_".
     { iExists v. iFrame "Hl Hv". }
-    iModIntro. iSplit=>//.
+    iModIntro. by iSplit.
   Qed.
 
   Lemma ltyped_fetch_and_add_shared Γ1 Γ2 Γ3 e1 e2 :