Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq

_CoqProject

 -Q theories lrust
 theories/lifetime/definitions.v
 theories/lifetime/derived.v
+theories/lifetime/faking.v
 theories/lifetime/creation.v
 theories/lifetime/primitive.v
 theories/lifetime/accessors.v

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 4417beb8bfa43f89c09a027e8dd55550bf8f7a63
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq fd42adfe6236b6bebacb963e8fed3f7d1f935e26

theories/lifetime/borrow.v

-From lrust.lifetime Require Export primitive creation.
-From lrust.lifetime Require Export raw_reborrow.
+From lrust.lifetime Require Export primitive.
+From lrust.lifetime Require Export faking raw_reborrow.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.

theories/lifetime/creation.v

 From lrust.lifetime Require Export primitive.
+From lrust.lifetime Require Import faking.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
-(* TODO: move lft_inv_alive_acc, ilft_create and bor_fake to another file. The
-files raw_reborrow, borrow and derived solely depend on this file because of
-the aforementioned lemmas. *)
 
 Section creation.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma lft_inv_alive_acc (KI K : gset lft) κ :
-  (∀ κ', κ' ∈ KI → κ' ⊂ κ → κ' ∈ K) →
-  ([∗ set] κ' ∈ K, lft_inv_alive κ') -∗
-    ([∗ set] κ' ∈ KI, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ') ∗
-    (([∗ set] κ' ∈ KI, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ') -∗
-      ([∗ set] κ' ∈ K, lft_inv_alive κ')).
-Proof.
-  intros ?.
-  destruct (proj1 (subseteq_disjoint_union_L (filter (⊂ κ) KI) K)) as (K'&->&?).
-  { intros κ'. rewrite elem_of_filter. set_solver. }
-  rewrite big_sepS_union // big_sepS_filter. iIntros "[$ $]"; auto.
-Qed.
-
-Lemma ilft_create A I κ :
-  own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
-      ==∗ ∃ A' I', ⌜is_Some (I' !! κ)⌝ ∗
-    own_alft_auth A' ∗ own_ilft_auth I' ∗ ▷ ([∗ set] κ ∈ dom _ I', lft_inv A' κ).
-Proof.
-  iIntros "HA HI Hinv".
-  destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
-  { iModIntro. iExists A, I. by iFrame. }
-  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
-  iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
-      (frac * dec_agree bor_state)))) as (γbor) "[Hbor Hbor']";
-    first by apply auth_valid_discrete_2.
-  iMod (own_alloc ((● ∅) :auth (gset_disj slice_name)))
-     as (γinh) "Hinh"; first by done.
-  set (γs := LftNames γbor γcnt γinh).
-  iMod (own_update with "HI") as "[HI Hγs]".
-  { apply auth_update_alloc,
-      (alloc_singleton_local_update _ κ (DecAgree γs)); last done.
-    by rewrite lookup_fmap HIκ. }
-  iDestruct "Hγs" as "#Hγs".
-  iAssert (own_cnt κ (● 0)) with "[Hcnt]" as "Hcnt".
-  { rewrite /own_cnt. iExists γs. by iFrame. }
-  iAssert (own_cnt κ (◯ 0)) with "[Hcnt']" as "Hcnt'".
-  { rewrite /own_cnt. iExists γs. by iFrame. }
-  iAssert (∀ b, lft_inh κ b True)%I with "[Hinh]" as "Hinh".
-  { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
-    iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
-  iAssert (lft_inv_dead κ ∧ lft_inv_alive κ)%I
-    with "[-HA HI Hinv]" as "Hdeadandalive".
-  { iSplit.
-    - rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
-      iSplitL "Hbor"; last by iApply "Hinh".
-      rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !to_gmap_empty.
-      iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
-    - rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
-      { rewrite /lft_bor_alive. iExists ∅.
-        rewrite /to_borUR !fmap_empty big_sepM_empty.
-        iSplitR; [iApply box_alloc|]. iSplit=>//.
-        rewrite /own_bor. iExists γs. by iFrame. }
-      iSplitR "Hinh"; last by iApply "Hinh".
-      rewrite lft_vs_unfold. iExists 0. iFrame "Hcnt Hcnt'". auto. }
-  destruct (lft_alive_or_dead_in A κ) as [(Λ&?&HAΛ)|Haliveordead].
-  - iMod (own_update with "HA") as "[HA _]".
-    { apply auth_update_alloc,
-        (alloc_singleton_local_update _ Λ (Cinr ())); last done.
-      by rewrite lookup_fmap HAΛ. }
-    iModIntro. iExists (<[Λ:=false]>A), (<[κ:=γs]> I).
-    iSplit; first rewrite lookup_insert; eauto.
-    rewrite /own_ilft_auth /own_alft_auth /to_ilftUR /to_alftUR !fmap_insert.
-    iFrame "HA HI". rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
-    iSplitR "Hinv".
-    { rewrite /lft_inv. iNext. iRight. iSplit.
-      { by iDestruct "Hdeadandalive" as "[? _]". }
-      iPureIntro. exists Λ. rewrite lookup_insert; auto. }
-    iNext. iApply (@big_sepS_impl with "[$Hinv]").
-    rewrite /lft_inv. iIntros "!#"; iIntros (κ' ?%elem_of_dom)
-      "[[HA HA']|[HA HA']]"; iDestruct "HA'" as %HA.
-    + iLeft. iFrame "HA". iPureIntro. by apply lft_alive_in_insert.
-    + iRight. iFrame "HA". iPureIntro. by apply lft_dead_in_insert.
-  - iModIntro. iExists A, (<[κ:=γs]> I).
-    iSplit; first rewrite lookup_insert; eauto.
-    rewrite /own_ilft_auth /to_ilftUR fmap_insert. iFrame "HA HI".
-    rewrite dom_insert_L.
-    iApply @big_sepS_insert; first by apply not_elem_of_dom.
-    iFrame "Hinv". iNext. rewrite /lft_inv. destruct Haliveordead.
-    + iLeft. by iDestruct "Hdeadandalive" as "[_ $]".
-    + iRight. by iDestruct "Hdeadandalive" as "[$ _]".
-Qed.
-
-Lemma raw_bor_fake' E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ [†κ] ={E}=∗ raw_bor κ P.
-Proof.
-  iIntros (?) "#LFT H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
-  iDestruct "Hκ" as %Hκ. rewrite /lft_dead. iDestruct "H†" as (Λ) "[% #H†]".
-  iDestruct (own_alft_auth_agree A' Λ false with "HA H†") as %EQAΛ.
-  iDestruct (@big_sepS_elem_of_acc with "Hinv")
-    as "[Hinv Hclose']"; first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
-  { unfold lft_alive_in in *; naive_solver. }
-  rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-  iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
-  iFrame. iApply "Hclose". iExists A', I'. iFrame. iNext. iApply "Hclose'".
-  rewrite /lft_inv /lft_inv_dead. iRight. iFrame. eauto.
-Qed.
-
-Lemma bor_fake E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
-Proof.
-  iIntros (?) "#LFT H†". iMod (raw_bor_fake' with "LFT H†"); first done.
-  iModIntro. unfold bor. iExists κ. iFrame. by rewrite -lft_incl_refl.
-Qed.
-
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
   let Iinv := (
     own_ilft_auth I ∗
@@ -146,7 +36,8 @@ Proof.
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first solve_ndisj.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
-  iDestruct (lft_inv_alive_acc (dom _ I) _ κ with "Halive") as "[Halive Halive']".
+  iDestruct (big_sepS_filter_acc (⊂ κ) _ _ (dom _ I) with "Halive")
+    as "[Halive Halive']".
   { intros κ'. rewrite elem_of_dom. eauto. }
   iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.

theories/lifetime/derived.v

-From lrust.lifetime Require Export primitive accessors creation.
+From lrust.lifetime Require Export primitive accessors faking.
 From lrust.lifetime Require Export raw_reborrow.
 From iris.proofmode Require Import tactics.
 (* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven

theories/lifetime/faking.v

+From lrust.lifetime Require Export primitive.
+From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import boxes.
+From iris.proofmode Require Import tactics.
+
+Section faking.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+Lemma ilft_create A I κ :
+  own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
+      ==∗ ∃ A' I', ⌜is_Some (I' !! κ)⌝ ∗
+    own_alft_auth A' ∗ own_ilft_auth I' ∗ ▷ ([∗ set] κ ∈ dom _ I', lft_inv A' κ).
+Proof.
+  iIntros "HA HI Hinv".
+  destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
+  { iModIntro. iExists A, I. by iFrame. }
+  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
+  iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
+      (frac * dec_agree bor_state)))) as (γbor) "[Hbor Hbor']";
+    first by apply auth_valid_discrete_2.
+  iMod (own_alloc ((● ∅) :auth (gset_disj slice_name)))
+     as (γinh) "Hinh"; first by done.
+  set (γs := LftNames γbor γcnt γinh).
+  iMod (own_update with "HI") as "[HI Hγs]".
+  { apply auth_update_alloc,
+      (alloc_singleton_local_update _ κ (DecAgree γs)); last done.
+    by rewrite lookup_fmap HIκ. }
+  iDestruct "Hγs" as "#Hγs".
+  iAssert (own_cnt κ (● 0)) with "[Hcnt]" as "Hcnt".
+  { rewrite /own_cnt. iExists γs. by iFrame. }
+  iAssert (own_cnt κ (◯ 0)) with "[Hcnt']" as "Hcnt'".
+  { rewrite /own_cnt. iExists γs. by iFrame. }
+  iAssert (∀ b, lft_inh κ b True)%I with "[Hinh]" as "Hinh".
+  { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
+    iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
+  iAssert (lft_inv_dead κ ∧ lft_inv_alive κ)%I
+    with "[-HA HI Hinv]" as "Hdeadandalive".
+  { iSplit.
+    - rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
+      iSplitL "Hbor"; last by iApply "Hinh".
+      rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !to_gmap_empty.
+      iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
+    - rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
+      { rewrite /lft_bor_alive. iExists ∅.
+        rewrite /to_borUR !fmap_empty big_sepM_empty.
+        iSplitR; [iApply box_alloc|]. iSplit=>//.
+        rewrite /own_bor. iExists γs. by iFrame. }
+      iSplitR "Hinh"; last by iApply "Hinh".
+      rewrite lft_vs_unfold. iExists 0. iFrame "Hcnt Hcnt'". auto. }
+  destruct (lft_alive_or_dead_in A κ) as [(Λ&?&HAΛ)|Haliveordead].
+  - iMod (own_update with "HA") as "[HA _]".
+    { apply auth_update_alloc,
+        (alloc_singleton_local_update _ Λ (Cinr ())); last done.
+      by rewrite lookup_fmap HAΛ. }
+    iModIntro. iExists (<[Λ:=false]>A), (<[κ:=γs]> I).
+    iSplit; first rewrite lookup_insert; eauto.
+    rewrite /own_ilft_auth /own_alft_auth /to_ilftUR /to_alftUR !fmap_insert.
+    iFrame "HA HI". rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
+    iSplitR "Hinv".
+    { rewrite /lft_inv. iNext. iRight. iSplit.
+      { by iDestruct "Hdeadandalive" as "[? _]". }
+      iPureIntro. exists Λ. rewrite lookup_insert; auto. }
+    iNext. iApply (@big_sepS_impl with "[$Hinv]").
+    rewrite /lft_inv. iIntros "!#"; iIntros (κ' ?%elem_of_dom)
+      "[[HA HA']|[HA HA']]"; iDestruct "HA'" as %HA.
+    + iLeft. iFrame "HA". iPureIntro. by apply lft_alive_in_insert.
+    + iRight. iFrame "HA". iPureIntro. by apply lft_dead_in_insert.
+  - iModIntro. iExists A, (<[κ:=γs]> I).
+    iSplit; first rewrite lookup_insert; eauto.
+    rewrite /own_ilft_auth /to_ilftUR fmap_insert. iFrame "HA HI".
+    rewrite dom_insert_L.
+    iApply @big_sepS_insert; first by apply not_elem_of_dom.
+    iFrame "Hinv". iNext. rewrite /lft_inv. destruct Haliveordead.
+    + iLeft. by iDestruct "Hdeadandalive" as "[_ $]".
+    + iRight. by iDestruct "Hdeadandalive" as "[$ _]".
+Qed.
+
+Lemma raw_bor_fake E q κ P :
+  ↑borN ⊆ E →
+  ▷?q lft_bor_dead κ ={E}=∗ ▷?q lft_bor_dead κ ∗ raw_bor κ P.
+Proof.
+  iIntros (?). rewrite /lft_bor_dead. iDestruct 1 as (B Pinh) "[>HB● Hbox]".
+  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
+  iMod (own_bor_update with "HB●") as "[HB● H◯]".
+  { eapply auth_update_alloc,
+      (alloc_singleton_local_update _ _ (1%Qp, DecAgree Bor_in)); last done.
+    by do 2 eapply lookup_to_gmap_None. }
+  rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "H◯".
+  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+  - iExists γ. by iFrame.
+Qed.
+
+Lemma raw_bor_fake' E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ [†κ] ={E}=∗ raw_bor κ P.
+Proof.
+  iIntros (?) "#LFT H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
+  iDestruct "Hκ" as %Hκ. rewrite /lft_dead. iDestruct "H†" as (Λ) "[% #H†]".
+  iDestruct (own_alft_auth_agree A' Λ false with "HA H†") as %EQAΛ.
+  iDestruct (@big_sepS_elem_of_acc with "Hinv")
+    as "[Hinv Hclose']"; first by apply elem_of_dom.
+  rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
+  { unfold lft_alive_in in *; naive_solver. }
+  rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
+  iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
+  iFrame. iApply "Hclose". iExists A', I'. iFrame. iNext. iApply "Hclose'".
+  rewrite /lft_inv /lft_inv_dead. iRight. iFrame. eauto.
+Qed.
+
+Lemma bor_fake E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+Proof.
+  iIntros (?) "#LFT H†". iMod (raw_bor_fake' with "LFT H†"); first done.
+  iModIntro. unfold bor. iExists κ. iFrame. iApply lft_incl_refl.
+Qed.
+End faking.

theories/lifetime/primitive.v

@@ -339,21 +339,6 @@ Proof.
   rewrite /idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'").
 Qed.
 
-Lemma raw_bor_fake E q κ P :
-  ↑borN ⊆ E →
-  ▷?q lft_bor_dead κ ={E}=∗ ▷?q lft_bor_dead κ ∗ raw_bor κ P.
-Proof.
-  iIntros (?). rewrite /lft_bor_dead. iDestruct 1 as (B Pinh) "[>HB● Hbox]".
-  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
-  iMod (own_bor_update with "HB●") as "[HB● H◯]".
-  { eapply auth_update_alloc,
-      (alloc_singleton_local_update _ _ (1%Qp, DecAgree Bor_in)); last done.
-    by do 2 eapply lookup_to_gmap_None. }
-  rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "H◯".
-  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
-  - iExists γ. by iFrame.
-Qed.
-
 (* Inheritance *)
 Lemma lft_inh_extend E κ P Q :
   ↑inhN ⊆ E →

theories/lifetime/raw_reborrow.v

-From lrust.lifetime Require Export primitive creation.
+From lrust.lifetime Require Export primitive.
+From lrust.lifetime Require Import faking.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.

theories/lifetime/shr_borrow.v

 From iris.algebra Require Import gmap auth frac.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Export borrow derived.
+From lrust.lifetime Require Export derived.
 
 (** Shared bors  *)
 Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=

theories/typing/perm_incl.v

 From Coq Require Import Qcanon.
 From iris.base_logic Require Import big_op.
 From lrust.typing Require Export type perm.
-From lrust.lifetime Require Import frac_borrow reborrow.
+From lrust.lifetime Require Import borrow frac_borrow reborrow.
 
 Import Perm Types.
 

theories/typing/type.v

@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Export thread_local.
 From iris.program_logic Require Import hoare.
 From lrust.lang Require Export heap notation.
-From lrust.lifetime Require Import frac_borrow reborrow.
+From lrust.lifetime Require Import borrow frac_borrow reborrow.
 
 Class iris_typeG Σ := Iris_typeG {
   type_heapG :> heapG Σ;
@@ -180,9 +180,8 @@ Section types.
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     replace ((mgmtE ∪ ↑N) ∖ ↑N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hb". set_solver.
+    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "[Hb Htok]". set_solver.
       { rewrite bor_unfold_idx. iExists i. eauto. }
-      iIntros "!>". iNext. iMod "Hb" as "[Hb Htok]".
       iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done.
       iApply "Hclose". eauto.
     - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
@@ -194,10 +193,8 @@ Section types.
     iIntros (q') "!#Htok".
     iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
     iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
-    iMod ("Hvs" $! q'' with "Htok") as "Hvs'".
-    iIntros "!>". iNext. iMod "Hvs'" as "[Hshr Htok]".
-    iMod ("Hclose" with "Htok"). iFrame.
-    iApply (ty.(ty_shr_mono) with "LFT Hκ"); last done. done.
+    iMod ("Hvs" $! q'' with "Htok") as "[Hshr Htok]".
+    iMod ("Hclose" with "Htok") as "$". by iApply (ty.(ty_shr_mono) with "LFT Hκ").
   Qed.
   Next Obligation. done. Qed.
 
@@ -234,12 +231,10 @@ Section types.
     - iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
       { rewrite (bor_unfold_idx κ'). eauto. }
       iMod (bor_unnest with "LFT Hb") as "Hb". set_solver.
-      iIntros "!>". iNext. iMod "Hb".
       iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done. set_solver.
       iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
-    - iMod (step_fupd_mask_mono _ _ _ _ True%I with "[]") as "Hclose'"; last first.
-      iIntros "!>". iNext. iMod "Hclose'" as "_".
-      iMod ("Hclose" with "[]") as "_"; by eauto. eauto. done. set_solver.
+    - iMod ("Hclose" with "[]") as "_". by eauto.
+      iApply step_fupd_mask_mono; last by eauto. done. set_solver.
   Qed.
   Next Obligation.
     intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
@@ -251,9 +246,8 @@ Section types.
     iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros (q) "!#Htok".
     iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
     iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod ("Hvs" $! q' with "Htok") as "Hclose'".  iIntros "!>". iNext.
-    iMod "Hclose'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-    iApply (ty_shr_mono with "LFT Hκ0"); last done. done.
+    iMod ("Hvs" $! q' with "Htok") as "[#Hshr Htok]".
+    iMod ("Hclose" with "Htok") as "$". by iApply (ty_shr_mono with "LFT Hκ0").
   Qed.
   Next Obligation. done. Qed.
 
@@ -319,8 +313,10 @@ Section types.
     repeat setoid_rewrite tl_own_union; first last.
     set_solver. set_solver. set_solver. set_solver.
     iDestruct "Htl" as "[[Htl1 Htl2] $]".
-    iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". done. set_solver.
-    iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". done. set_solver.
+    iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]".
+      done. set_solver.
+    iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]".
+      done. set_solver.
     destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
     iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
     rewrite !split_prod_mt.
@@ -352,8 +348,8 @@ Section types.
     ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl emp) tid.
   Proof.
     iSplit; iIntros "H".
-    - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "[% Hown]". subst.
-      iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
+    - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "[% Hown]".
+      subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
       iExists vl'. by iFrame.
     - iDestruct "H" as (i) "[Hmt1 Hown]". iDestruct "Hown" as (vl) "[Hmt2 Hown]".
       iExists (#i::vl). rewrite heap_mapsto_vec_cons. iFrame. eauto.
@@ -390,8 +386,8 @@ Section types.
     rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left.
   Qed.
   Next Obligation.
-    iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
-    simpl. by iDestruct (sum_size_eq with "Hown") as %->.
+    iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)".
+    subst. simpl. by iDestruct (sum_size_eq with "Hown") as %->.
   Qed.
   Next Obligation.
     intros n tyl Hn E N κ l tid q ??. iIntros "#LFT Hown Htok". rewrite split_sum_mt.

theories/typing/type_incl.v

 From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import hoare.
 From lrust.typing Require Export type perm_incl.
-From lrust.lifetime Require Import frac_borrow.
+From lrust.lifetime Require Import frac_borrow borrow.
 
 Import Types.
 
@@ -63,9 +63,7 @@ Section ty_incl.
       iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
       iExists _. by iFrame.
     - iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
-      iIntros (q') "!#Hκ".
-      iMod ("Hvs" $! _ with "Hκ") as "Hvs'". iIntros "!>". iNext.
-      iMod "Hvs'" as "[Hshr $]". iModIntro.
+      iIntros (q') "!#Hκ". iMod ("Hvs" $! _ with "Hκ") as "[Hshr $]".
       by iDestruct ("Hshri" $! _ _ _ with "Hshr") as "[$ _]".
   Qed.
 
@@ -83,8 +81,7 @@ Section ty_incl.
       iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
       iFrame. iIntros (q') "!#Htok".
       iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
-      iMod ("Hupd" with "*Htok") as "Hupd'". iModIntro. iNext.
-      iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
+      iMod ("Hupd" with "*Htok") as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
       by iApply (ty_shr_mono with "LFT Hincl' H").
   Qed.
 

theories/typing/typing.v

@@ -3,8 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Export notation memcpy.
 From lrust.typing Require Export type perm.
 From lrust Require Import typing.perm_incl lang.proofmode.
-From lrust.lifetime Require Import frac_borrow reborrow.
-
+From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 Import Types Perm.
 
 Section typing.
@@ -142,11 +141,10 @@ Section typing.
   Lemma typed_endlft κ ρ:
     typed_step (κ ∋ ρ ∗ 1.[κ] ∗ †κ) Endlft (λ _, ρ)%P.
   Proof.
-    iIntros (tid) "!#(_&_&(Hextr&Htok&Hend)&$)".
-    iApply wp_fupd. iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
-    iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done.
-    iDestruct ("Hend" with "Htok") as "$". by wp_seq.
-    iIntros (v) "[#Hκ _]". by iApply fupd_mask_mono; last iApply "Hextr".
+    rewrite /killable /extract. iIntros (tid) "!#(_&_&(Hextr&Htok&Hend)&$)".
+    iDestruct ("Hend" with "Htok") as "Hend".
+    iApply (wp_fupd_step with "Hend"); try done. wp_seq.
+    iIntros "!>H†". by iApply fupd_mask_mono; last iApply "Hextr".
   Qed.
 
   Lemma typed_alloc ρ (n : nat):
@@ -296,16 +294,15 @@ Section typing.
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b Hown]".
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
-    iSpecialize ("Hown" $! _ with "Htok2").
-    iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
-    - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q'''} v ∗ ⌜v = #vl⌝)%I); try done.
-      iSplitL "Hown"; last by wp_read; eauto.
-      iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ (↑heapN));
-        last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
-    - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
-      iMod ("Hclose'" with "[$H↦]") as "Htok'".
-      iMod ("Hclose" with "[$Htok $Htok']") as "$".
-      iFrame "#". iExists _. eauto.
+    iApply (wp_fupd_step _ (↑heapN) with "[Hown Htok2]"); try done.
+    - rewrite -(left_id (R:=eq) ∅ (∪) (↑heapN)). assert (⊤ = ⊤∖↑heapN ∪ ↑heapN) as ->.
+      { by rewrite (comm (R:=eq)) -union_difference_L. }
+      iApply step_fupd_mask_frame_r; try set_solver.
+      iApply step_fupd_mask_mono; last by iApply ("Hown" with "* Htok2").
+        set_solver. repeat apply union_least; solve_ndisj.
+    - wp_read. iIntros "!>[Hshr ?]". iFrame "H⊑".
+      iSplitL "Hshr"; first by iExists _; auto.
+      iMod ("Hclose'" with "[$H↦]") as "?". iApply "Hclose". iFrame.
   Qed.
 
   Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
@@ -324,15 +321,12 @@ Section typing.
     iMod (bor_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
     iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
     rewrite heap_mapsto_vec_singleton.
-    iApply (wp_strong_mono ⊤ ⊤ _ (λ v, _ ∗ ⌜v = #l'⌝ ∗ l ↦#l')%I). done.
-    iSplitR "Hbor H↦"; last first.
-    - iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done; last first.
-      iSplitL "Hbor". by iApply (bor_unnest with "LFT Hbor"). wp_read. auto.
-    - iIntros (v) "(Hbor & % & H↦)". subst.
-      iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
-      iMod ("Hclose" with "Htok") as "$". iFrame "#".
-      iExists _. iSplitR. done. iApply (bor_shorten with "[] Hbor").
+    iApply (wp_fupd_step  _ (⊤∖↑lftN) with "[Hbor]"); try done.
+      by iApply (bor_unnest with "LFT Hbor").
+    wp_read. iIntros "!> Hbor". iFrame "#". iSplitL "Hbor".
+    - iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
       iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
+    - iMod ("Hclose'" with "[$H↦]") as "[_ ?]". by iApply "Hclose".
   Qed.
 
   Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
@@ -349,17 +343,16 @@ Section typing.
     iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
     { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
     iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
-    iSpecialize ("Hown" $! _ with "Htok").
-    iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
-    - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q''} v ∗ ⌜v = #l'⌝)%I); try done.
-      iSplitL "Hown"; last by wp_read; eauto.
-      iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ (↑heapN));
-        last iApply "Hown"; (set_solver || rewrite ?disjoint_union_l; solve_ndisj).
-    - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
-      iMod ("Hclose''" with "Htok") as "Htok".
-      iMod ("Hclose'" with "[$H↦]") as "Htok'".
-      iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _.
-      iSplitL. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+    iApply (wp_fupd_step _ (↑heapN) with "[Hown Htok]"); try done.
+    - rewrite -(left_id (R:=eq) ∅ (∪) (↑heapN)). assert (⊤ = ⊤∖↑heapN ∪ ↑heapN) as ->.
+      { by rewrite (comm (R:=eq)) -union_difference_L. }
+      iApply step_fupd_mask_frame_r; try set_solver.
+      iApply step_fupd_mask_mono; last by iApply ("Hown" with "* Htok").
+        set_solver. repeat apply union_least; solve_ndisj.
+    - wp_read. iIntros "!>[Hshr Htok]". iFrame "H⊑1". iSplitL "Hshr".
+      + iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+      + iMod ("Hclose''" with "Htok"). iMod ("Hclose'" with "[$H↦]").
+        iApply "Hclose". iFrame.
   Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=