Tweaking refcell.

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq da3aa7e4497878a70b00f17bf109e18ef2a079d3
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq da56bbb0f26f4f77fe28efea60f81f06d8a2ac59

theories/lifetime/lifetime_sig.v

@@ -130,7 +130,7 @@ Module Type lifetime_sig.
   Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
   Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
   Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
-  Parameter lft_incl_mono : ∀ κ1 κ1' κ2 κ2',
+  Parameter lft_glb_mono : ∀ κ1 κ1' κ2 κ2',
     κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
   Parameter lft_incl_acc : ∀ E κ κ' q,
     ↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).

theories/lifetime/model/primitive.v

@@ -340,7 +340,7 @@ Proof.
   - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
 Qed.
 
-Lemma lft_incl_mono κ1 κ1' κ2 κ2' :
+Lemma lft_glb_mono κ1 κ1' κ2 κ2' :
   κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
 Proof.
   iIntros "#H1 #H2". iApply (lft_incl_glb with "[]").

theories/lifetime/model/reborrow.v

@@ -68,7 +68,7 @@ Proof.
     iNext. iMod "Hclose" as "_".
     iApply (bor_fake with "LFT >"); first done.
     iApply (lft_incl_dead with "[] H†"); first done.
-    by iApply (lft_incl_mono with "Hκ⊑"). }
+    by iApply (lft_glb_mono with "Hκ⊑"). }
   rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #Hislice]".
   iDestruct "Hislice" as (P') "[#HPP' Hislice]".
   rewrite lft_inv_alive_unfold;
@@ -100,6 +100,6 @@ Proof.
     iFrame. rewrite /lft_inv lft_inv_alive_unfold. iLeft.
     iFrame "%". iExists Pb'', Pi. iFrame. }
   iModIntro. rewrite /bor. iExists κ''. iFrame. subst κ''.
-  by iApply (lft_incl_mono with "Hκ⊑").
+  by iApply (lft_glb_mono with "Hκ⊑").
 Qed.
 End reborrow.

theories/typing/uniq_bor.v

@@ -67,19 +67,16 @@ Section uniq_bor.
     iDestruct (Hty with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
     iDestruct (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
     - iIntros (? [|[[]|][]]) "H"; try iDestruct "H" as "[]".
-      iApply (bor_shorten with "Hκ"). iApply (bor_iff_proper with "[] H").
+      iApply (bor_shorten with "Hκ"). iApply bor_iff_proper; last done.
       iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
       iExists vl; iFrame; by iApply "Ho".
     - iIntros (κ ??) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
-      { iApply (lft_incl_glb with "[] []").
-        - iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
-          apply gmultiset_union_subseteq_l.
-        - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
+      { iApply lft_glb_mono. done. iApply lft_incl_refl. }
       iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
       iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first set_solver.
       iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
       iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
-      iApply (ty_shr_mono with "[] Hincl'"); [done..|]. by iApply "Hs".
+      iApply ty_shr_mono; [done..|]. by iApply "Hs".
   Qed.
   Global Instance uniq_mono_flip E L :
     Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
@@ -102,7 +99,7 @@ Section uniq_bor.
     Send ty → Send (uniq_bor κ ty).
   Proof.
     iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]".
-    iApply (bor_iff_proper with "[] H"). iNext. iAlways. iApply uPred.equiv_iff.
+    iApply bor_iff_proper; last done. iNext. iAlways. iApply uPred.equiv_iff.
     do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
   Qed.
 

theories/typing/unsafe/cell.v

@@ -34,7 +34,7 @@ Section cell.
     iDestruct (EQ with "LFT HE HL") as "(% & #Hown & #Hshr)".
     iSplit; [done|iSplit; iIntros "!# * H"].
     - iApply ("Hown" with "H").
-    - iApply (na_bor_iff_proper with "[] H"). iSplit; iIntros "!>!# H";
+    - iApply na_bor_iff_proper; last done. iSplit; iIntros "!>!# H";
       iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
   Qed.
   Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2).

theories/typing/unsafe/refcell.v

@@ -26,17 +26,48 @@ Definition writing_st (q : frac) : refcell_stR := Some (Cinl (Excl ())).
 Section refcell.
   Context `{typeG Σ, refcellG Σ}.
 
-  Definition refcell_inv (l : loc) ty tid (a : lft) (γ : gname) : iProp Σ :=
+  Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
     (∃ st, l ↦ #(Z_of_refcell_st st) ∗ own γ (● st) ∗
       match st return _ with
-      | None => &{a}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
-      | Some (Cinr ({|agree_car := v|}, q, n)) =>
-        ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[v] ∗
-              ty.(ty_shr) (a ∪ v) tid (shift_loc l 1) ∗
-              ([†v] ={lftE}=∗ &{a}(shift_loc l 1 ↦∗: ty.(ty_own) tid))
+      | None => &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
+      | Some (Cinr ({|agree_car := ν|}, q, n)) =>
+        ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
+              ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+              ([†ν] ={lftE}=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid))
       | Some _ => True
       end)%I.
 
+  Global Instance refcell_inv_ne n tid l γ α :
+    Proper (dist n ==> dist n) (refcell_inv tid l γ α).
+  Proof.
+    intros ty1 ty2 Hty. unfold refcell_inv.
+    repeat (f_contractive || f_equiv || apply Hty).
+  Qed.
+
+  Lemma refcell_inv_proper E L tid l γ α1 α2 ty1 ty2 :
+    lctx_lft_incl E L α2 α1 → eqtype E L ty1 ty2 →
+    lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
+    refcell_inv tid l γ α1 ty1 -∗ refcell_inv tid l γ α2 ty2.
+  Proof.
+    (* TODO : this proof is essentially [solve_proper], but within the logic.
+              It would easily gain from some automation. *)
+    iIntros (Hα Hty%eqtype_unfold) "#LFT #HE #HL H". unfold refcell_inv.
+    iDestruct (Hty with "LFT HE HL") as "(% & Hown & Hshr)".
+    iAssert (□ (&{α1} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
+                &{α2} shift_loc l 1 ↦∗: ty_own ty2 tid))%I with "[]" as "#Hb".
+    { iIntros "!# H". iApply (bor_shorten with "[]"). by iApply Hα.
+      iApply bor_iff_proper; last done.
+      iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+      iFrame; by iApply "Hown". }
+    iDestruct "H" as (st) "H"; iExists st;
+      iDestruct "H" as "($&$&H)"; destruct st as [[|[[[]]]|]|]; try done;
+      last by iApply "Hb".
+    iDestruct "H" as (q') "(Heq & Htok & Hs & H†)". iExists q'. iFrame. iSplitL "Hs".
+    - iApply (ty_shr_mono); first done; last by iApply "Hshr".
+      by iApply lft_glb_mono; [iApply Hα|iApply lft_incl_refl].
+    - iIntros "?". iApply ("Hb" with ">"). by iApply "H†".
+  Qed.
+
   Program Definition refcell (ty : type) :=
     {| ty_size := S ty.(ty_size);
        ty_own tid vl :=
@@ -45,7 +76,7 @@ Section refcell.
          | _ => False
          end%I;
        ty_shr κ tid l :=
-         (∃ a γ, κ ⊑ a ∗ &na{a, tid, lrustN}(refcell_inv l ty tid a γ))%I |}.
+         (∃ α γ, κ ⊑ α ∗ &na{α, tid, lrustN}(refcell_inv tid l γ α ty))%I |}.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
     iIntros "[_ %]!%/=". congruence.
@@ -64,7 +95,7 @@ Section refcell.
       iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
     iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
     iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
-    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv l ty tid κ γ)%I with ">[-Hclose]"
+    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with ">[-Hclose]"
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "* HQ []") as "[Hb $]".
       - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
@@ -73,16 +104,16 @@ Section refcell.
         iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
     clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
     - iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
-    - iMod (lft_create with "LFT") as (v) "[[Htok1 Htok2] _]". done.
+    - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] _]". done.
       iMod (own_alloc
-         (● Some (Cinr (to_agree (v : leibnizC _), (1/2)%Qp, n)))) as (γ) "Hst".
+         (● Some (Cinr (to_agree (ν : leibnizC _), (1/2)%Qp, n)))) as (γ) "Hst".
       { by apply auth_auth_valid. }
       destruct (Qp_lower_bound (1/2) (q/2)) as (q' & q1 & q2 & H12 & ->). rewrite H12.
       iDestruct "Htok'" as "[Htok' $]". iDestruct "Htok1" as "[Htok1 Htok1']".
       iApply (fupd_mask_mono lftE). done.
-      iMod (rebor _ _ (κ∪v) with "LFT [] Hvl") as "[Hvl Hh]". done.
+      iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
       { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
-      iMod (ty_share _ _ (κ∪v) _ _ q' with "LFT Hvl [Htok' Htok1]")
+      iMod (ty_share _ _ (κ ∪ ν) _ _ q' with "LFT Hvl [Htok' Htok1]")
         as "[Hshr Htok]". done.
       { rewrite -lft_tok_sep. iFrame. }
       rewrite -lft_tok_sep. iDestruct "Htok" as "[$ Htok]".
@@ -94,40 +125,30 @@ Section refcell.
       iFrame. iExists _, _. by iFrame.
   Qed.
   Next Obligation.
-    iIntros (?????) "LFT #Hκ H". iDestruct "H" as (a γ) "[#??]".
+    iIntros (?????) "LFT #Hκ H". iDestruct "H" as (α γ) "[#??]".
     iExists _, _. iFrame. iApply lft_incl_trans; auto.
   Qed.
 
   Global Instance refcell_ne n : Proper (dist n ==> dist n) refcell.
   Proof.
-    move=>??[[]]/=Hsz Hown Hshr. split; [split|]; simpl. congruence.
-    - f_contractive=>tid vl. repeat f_equiv. apply Hown.
-    - intros κ tid l. unfold refcell_inv.
-      repeat (f_contractive || f_equiv); apply dist_S.
-      apply Hshr. apply Hown. apply Hown.
+    move=>ty1 ty2 Hty. split; [split|]; simpl.
+    - f_equiv. apply Hty.
+    - f_contractive=>tid vl. repeat f_equiv. apply Hty.
+    - intros κ tid l. by repeat f_equiv.
   Qed.
 
   Global Instance refcell_mono E L : Proper (eqtype E L ==> subtype E L) refcell.
   Proof.
     (* TODO : this proof is essentially [solve_proper], but within the logic.
               It would easily gain from some automation. *)
-    iIntros (ty1 ty2 EQ%eqtype_unfold) "#LFT #HE #HL".
-    iDestruct (EQ with "LFT HE HL") as "(% & #Hown & #Hshr)".
+    iIntros (ty1 ty2 EQ) "#LFT #HE #HL". pose proof EQ as EQ'%eqtype_unfold.
+    iDestruct (EQ' with "LFT HE HL") as "(% & #Hown & #Hshr)".
     iSplit; [|iSplit; iIntros "!# * H"].
     - iPureIntro. simpl. congruence.
     - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
     - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply (na_bor_iff_proper with "[] H"). iNext. iAlways.
-      iAssert (□ (&{a} shift_loc l 1 ↦∗: ty_own ty1 tid ↔
-                  &{a} shift_loc l 1 ↦∗: ty_own ty2 tid))%I as "#Hbiff".
-      { iSplit; iIntros "!#H"; iApply (bor_iff_proper with "[] H"); iIntros "!>!#"; 
-        iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl; iFrame;
-          by iApply "Hown". }
-      iSplit; iIntros "H"; iDestruct "H" as (st) "H"; iExists st;
-        iDestruct "H" as "($&$&H)"; destruct st as [[|[[[]]]|]|]; try done;
-        (try by iApply "Hbiff");
-      iDestruct "H" as (q') "(Heq & Htok & Hs & H†)"; iExists q'; iFrame;
-      (iSplitL "Hs"; [by iApply "Hshr"| iIntros "?"; iApply "Hbiff"; by iApply "H†"]).
+      iApply na_bor_iff_proper; last done.
+      iSplit; iIntros "!>!# H"; by iApply refcell_inv_proper.
   Qed.
   Lemma refcell_mono' E L ty1 ty2 :
     eqtype E L ty1 ty2 → subtype E L (refcell ty1) (refcell ty2).