theories/lifetime/model/primitive.v → lifetime/model/primitive.v

 From lrust.lifetime.model Require Export definitions.
-From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import boxes fractional.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris.algebra Require Import csum auth frac gmap agree gset proofmode_classes.
+From iris.base_logic.lib Require Import boxes.
+From iris.bi Require Import fractional.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
 Import uPred.
 
+Lemma lft_init `{!invGS Σ, !lftGpreS Σ} E userE :
+  ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftGS Σ userE, lft_ctx.
+Proof.
+  iIntros (? HuserE). rewrite /lft_ctx.
+  iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
+  iMod (own_alloc (● ∅ : authR ilftUR)) as (γi) "Hi"; first by apply auth_auth_valid.
+  set (HlftGS := LftG _ _ _ _ γa _ γi _ _ _ HuserE). iExists HlftGS.
+  iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
+  iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
+  rewrite /to_alftUR /to_ilftUR !fmap_empty. iFrame.
+  rewrite dom_empty_L big_sepS_empty. done.
+Qed.
+
 Section primitive.
-Context `{invG Σ, lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
   {[i := (q%Qp, to_agree s)]} ≼ to_borUR B → B !! i = Some s.
 Proof.
-  rewrite singleton_included=> -[qs []]. unfold_leibniz.
+  rewrite singleton_included_l=> -[qs []]. unfold_leibniz.
   rewrite lookup_fmap fmap_Some_equiv=> -[s' [-> ->]].
   by move=> /Some_pair_included [_] /Some_included_total /to_agree_included=>->.
 Qed.
 
-Lemma lft_init `{!lftPreG Σ} E :
-  ↑lftN ⊆ E → (|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
-Proof.
-  iIntros (?). rewrite /lft_ctx.
-  iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first done.
-  iMod (own_alloc (● ∅ : authR ilftUR)) as (γi) "Hi"; first done.
-  set (HlftG := LftG _ _ _ γa _ γi _ _ _). iExists HlftG.
-  iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
-  iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
-  rewrite /to_alftUR /to_ilftUR !fmap_empty. iFrame.
-  rewrite dom_empty_L big_sepS_empty. done.
-Qed.
-
 (** Ownership *)
 Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
   own_ilft_auth I -∗
     own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
-    as %[[? [Hl ?]]%singleton_included _]%auth_valid_discrete_2.
-  unfold to_ilftUR in *. simplify_map_eq.
+    as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid_discrete.
+  revert Hl. rewrite /to_ilftUR lookup_fmap.
+  case: (I !! _)=> [γs'|] Hl; first by eauto.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
 
@@ -47,8 +48,8 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
     own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
 Proof.
   iIntros "HA HΛ".
-  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_valid_discrete_2.
-  iPureIntro. move: HA=> /singleton_included [qs [/leibniz_equiv_iff]].
+  iCombine "HA HΛ" gives %[HA _]%auth_both_valid_discrete.
+  iPureIntro. move: HA=> /singleton_included_l [qs [/leibniz_equiv_iff]].
   rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
   move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
 Qed.
@@ -58,25 +59,33 @@ Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
 Qed.
+
 Lemma own_bor_op κ x y : own_bor κ (x ⋅ y) ⊣⊢ own_bor κ x ∗ own_bor κ y.
 Proof.
   iSplit.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
-  iExists γs. iSplit. done. rewrite own_op; iFrame.
+  iCombine "Hγs Hγs'" gives %Hγs. move : Hγs.
+  rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
+  iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_op κ x x1 x2 :
-  IntoOp x x1 x2 → IntoAnd false (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
+  IsOp x x1 x2 → IntoSep (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
 Proof.
-  rewrite /IntoOp /IntoAnd=>->. by rewrite -own_bor_op.
+  rewrite /IsOp /IntoSep=>-> /=. by rewrite -own_bor_op.
 Qed.
 Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
+Proof. apply entails_wand, wand_intro_r. rewrite -own_bor_op. iApply own_bor_valid. Qed.
+Global Instance own_bor_sep_gives κ x y :
+  CombineSepGives (own_bor κ x) (own_bor κ y) (✓ (x ⋅ y)).
+Proof.
+  rewrite /CombineSepGives. iIntros "[H1 H2]".
+  iDestruct (own_bor_valid_2 with "H1 H2") as "#?"; auto.
+Qed.
+
 Lemma own_bor_update κ x y : x ~~> y → own_bor κ x ==∗ own_bor κ y.
 Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -84,7 +93,7 @@ Qed.
 Lemma own_bor_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_bor κ x1 ⊢ own_bor κ x2 ==∗ own_bor κ y.
 Proof.
-  intros. apply wand_intro_r. rewrite -own_bor_op. by apply own_bor_update.
+  intros. apply wand_intro_r. rewrite -own_bor_op. by iApply own_bor_update.
 Qed.
 
 Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜is_Some (I !! κ)⌝.
@@ -98,19 +107,25 @@ Proof.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
+  iCombine "Hγs Hγs'" gives %Hγs. move: Hγs.
+  rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L=> <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_op κ x x1 x2 :
-  IntoOp x x1 x2 → IntoAnd false (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
+  IsOp x x1 x2 → IntoSep (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
 Proof.
-  rewrite /IntoOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_cnt_op.
+  rewrite /IsOp /IntoSep=> ->. by rewrite -own_cnt_op.
 Qed.
 Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_cnt_valid_2 κ x y : own_cnt κ x -∗ own_cnt κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
+Proof. apply entails_wand, wand_intro_r. rewrite -own_cnt_op. iApply own_cnt_valid. Qed.
+Global Instance own_cnt_sep_gives κ x y :
+  CombineSepGives (own_cnt κ x) (own_cnt κ y) (✓ (x ⋅ y)).
+Proof.
+  rewrite /CombineSepGives. iIntros "[H1 H2]".
+  iDestruct (own_cnt_valid_2 with "H1 H2") as "#?"; auto.
+Qed.
 Lemma own_cnt_update κ x y : x ~~> y → own_cnt κ x ==∗ own_cnt κ y.
 Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -118,7 +133,7 @@ Qed.
 Lemma own_cnt_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_cnt κ x1 -∗ own_cnt κ x2 ==∗ own_cnt κ y.
 Proof.
-  intros. apply wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
+  intros. apply entails_wand, wand_intro_r. rewrite -own_cnt_op. by iApply own_cnt_update.
 Qed.
 
 Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜is_Some (I !! κ)⌝.
@@ -132,19 +147,25 @@ Proof.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
-  iExists γs. iSplit. done. rewrite own_op; iFrame.
+  iCombine "Hγs Hγs'" gives %Hγs. move: Hγs.
+  rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L=> <-.
+  iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_op κ x x1 x2 :
-  IntoOp x x1 x2 → IntoAnd false (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
+  IsOp x x1 x2 → IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
 Proof.
-  rewrite /IntoOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_inh_op.
+  rewrite /IsOp /IntoSep=> ->. by rewrite -own_inh_op.
 Qed.
 Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_inh_valid_2 κ x y : own_inh κ x -∗ own_inh κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
+Proof. apply entails_wand, wand_intro_r. rewrite -own_inh_op. iApply own_inh_valid. Qed.
+Global Instance own_inh_sep_gives κ x y :
+  CombineSepGives (own_inh κ x) (own_inh κ y) (✓ (x ⋅ y)).
+Proof.
+  rewrite /CombineSepGives. iIntros "[H1 H2]".
+  iDestruct (own_inh_valid_2 with "H1 H2") as "#?"; auto.
+Qed.
 Lemma own_inh_update κ x y : x ~~> y → own_inh κ x ==∗ own_inh κ y.
 Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -152,20 +173,20 @@ Qed.
 Lemma own_inh_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_inh κ x1 ⊢ own_inh κ x2 ==∗ own_inh κ y.
 Proof.
-  intros. apply wand_intro_r. rewrite -own_inh_op. by apply own_inh_update.
+  intros. apply wand_intro_r. rewrite -own_inh_op. by iApply own_inh_update.
 Qed.
 
 (** Alive and dead *)
 Global Instance lft_alive_in_dec A κ : Decision (lft_alive_in A κ).
 Proof.
   refine (cast_if (decide (set_Forall (λ Λ, A !! Λ = Some true)
-                  (dom (gset atomic_lft) κ))));
+                  (dom κ))));
     rewrite /lft_alive_in; by setoid_rewrite <-gmultiset_elem_of_dom.
 Qed.
 Global Instance lft_dead_in_dec A κ : Decision (lft_dead_in A κ).
 Proof.
   refine (cast_if (decide (set_Exists (λ Λ, A !! Λ = Some false)
-                  (dom (gset atomic_lft) κ))));
+                  (dom κ))));
       rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
 Qed.
 
@@ -173,9 +194,9 @@ Lemma lft_alive_or_dead_in A κ :
   (∃ Λ, Λ ∈ κ ∧ A !! Λ = None) ∨ (lft_alive_in A κ ∨ lft_dead_in A κ).
 Proof.
   rewrite /lft_alive_in /lft_dead_in.
-  destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom (gset _) κ)))
+  destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom κ)))
     as [(Λ & ?%gmultiset_elem_of_dom & HAΛ)|HA%(not_set_Exists_Forall _)]; first eauto.
-  destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom (gset _) κ)))
+  destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom κ)))
     as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)]; first eauto.
   right; left. intros Λ HΛ%gmultiset_elem_of_dom.
   move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[]|]; naive_solver.
@@ -200,6 +221,14 @@ Proof.
   intros HΛ Halive Λ' HΛ'.
   rewrite lookup_insert_ne; last (by intros ->); auto.
 Qed.
+Lemma lft_alive_in_union_false A κ Λs b :
+  (∀ Λ, Λ ∈ Λs → Λ ∉ κ) → lft_alive_in A κ → lft_alive_in (gset_to_gmap b Λs ∪ A) κ.
+Proof.
+  intros HΛ Halive Λ' HΛ'.
+  rewrite lookup_union_r; [by apply Halive|].
+  apply lookup_gset_to_gmap_None.
+  by intros ?%HΛ.
+Qed.
 
 Lemma lft_dead_in_insert A κ Λ b :
   A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
@@ -215,12 +244,32 @@ Proof.
   - exists Λ. by rewrite lookup_insert.
   - exists Λ'. by rewrite lookup_insert_ne.
 Qed.
+Lemma lft_dead_in_union_false A κ Λs :
+  lft_dead_in A κ → lft_dead_in (gset_to_gmap false Λs ∪ A) κ.
+Proof.
+  intros (Λ&?&HΛ). destruct (decide (Λ ∈ Λs)) as [|].
+  - exists Λ. rewrite lookup_union_l'.
+    + by rewrite lookup_gset_to_gmap_Some.
+    + exists false; by rewrite lookup_gset_to_gmap_Some.
+  - exists Λ. rewrite lookup_union_r.
+    + done.
+    + by rewrite lookup_gset_to_gmap_None.
+Qed.
 Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
 Proof. exists Λ. by rewrite lookup_insert. Qed.
+Lemma lft_dead_in_union_false' A κ Λs Λ :
+  Λ ∈ κ → Λ ∈ Λs → lft_dead_in (gset_to_gmap false Λs ∪ A) κ.
+Proof.
+  intros HΛκ HΛ.
+  exists Λ; split; [done|].
+  rewrite lookup_union_l'.
+  - by apply lookup_gset_to_gmap_Some.
+  - exists false; by apply lookup_gset_to_gmap_Some.
+Qed.
 Lemma lft_dead_in_alive_in_union A κ κ' :
-  lft_dead_in A (κ ∪ κ') → lft_alive_in A κ → lft_dead_in A κ'.
+  lft_dead_in A (κ ⊓ κ') → lft_alive_in A κ → lft_dead_in A κ'.
 Proof.
-  intros (Λ & [Hin|Hin]%elem_of_union & HΛ) Halive.
+  intros (Λ & [Hin|Hin]%gmultiset_elem_of_disj_union & HΛ) Halive.
   - contradict HΛ. rewrite (Halive _ Hin). done.
   - exists Λ. auto.
 Qed.
@@ -241,14 +290,6 @@ Proof.
   by rewrite HAinsert.
 Qed.
 
-Lemma lft_inv_alive_twice κ : lft_inv_alive κ -∗ lft_inv_alive κ -∗ False.
-Proof.
-  rewrite lft_inv_alive_unfold /lft_inh.
-  iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
-  iDestruct "Hinh" as (E) "[HE _]"; iDestruct "Hinh'" as (E') "[HE' _]".
-  by iDestruct (own_inh_valid_2 with "HE HE'") as %?.
-Qed.
-
 Lemma lft_inv_alive_in A κ : lft_alive_in A κ → lft_inv A κ -∗ lft_inv_alive κ.
 Proof.
   rewrite /lft_inv. iIntros (?) "[[$ _]|[_ %]]".
@@ -261,10 +302,23 @@ Proof.
 Qed.
 
 (** Basic rules about lifetimes  *)
-Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
-Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
-
-Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ∪ κ2].
+Local Instance lft_inhabited : Inhabited lft := _.
+Local Instance lft_eq_dec : EqDecision lft := _.
+Local Instance lft_countable : Countable lft := _.
+Local Instance bor_idx_inhabited : Inhabited bor_idx := _.
+Local Instance bor_idx_eq_dec : EqDecision bor_idx := _.
+Local Instance bor_idx_countable : Countable bor_idx := _.
+Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
+Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
+Local Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
+Local Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
+Local Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
+Local Instance lft_intersect_right_id : RightId eq static (⊓) := _.
+
+Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
+Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
+
+Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
 Proof.
   rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
   rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
@@ -273,34 +327,63 @@ Qed.
 Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False.
 Proof.
   rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
-  iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
-  iDestruct (own_valid_2 with "H H'") as %Hvalid.
-  move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
+  iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
+  iCombine "H H'" gives %Hvalid.
+  move: Hvalid=> /auth_frag_valid /=; by rewrite singleton_op singleton_valid.
 Qed.
 
-Lemma lft_tok_static q : q.[static]%I.
+Lemma lft_tok_static q : ⊢ q.[static].
 Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
 
 Lemma lft_dead_static : [† static] -∗ False.
 Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
 
+Lemma lft_intersect_static_cancel_l κ κ' : κ ⊓ κ' = static → κ = static.
+Proof.
+  rewrite !gmultiset_eq=>Heq Λ. move:(Heq Λ).
+  rewrite multiplicity_disj_union multiplicity_empty Nat.eq_add_0.
+  naive_solver.
+Qed.
+
+Lemma lft_tok_valid q κ : 
+  q.[κ] -∗ ⌜(q ≤ 1)%Qp⌝ ∨ ⌜κ = static⌝.
+Proof.
+  rewrite /lft_tok. 
+  destruct (decide (κ = static)) as [-> | Hneq]; first by eauto.
+  edestruct (gmultiset_choose _ Hneq) as (Λ & Hel).
+  iIntros "Hm". iPoseProof (big_sepMS_elem_of with "Hm") as "Hm"; first done.
+  iPoseProof (own_valid with "Hm") as "%Hv".
+  iLeft. iPureIntro. rewrite auth_frag_valid in Hv. apply singleton_valid in Hv. done.
+Qed.
+
 (* Fractional and AsFractional instances *)
 Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
 Proof.
-  intros p q. rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper.
-  intros Λ ?. rewrite -Cinl_op -op_singleton auth_frag_op own_op //.
+  intros p q. rewrite /lft_tok -big_sepMS_sep. apply big_sepMS_proper.
+  intros Λ ?. rewrite Cinl_op -singleton_op auth_frag_op own_op //.
 Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional q.[κ] (λ q, q.[κ])%I q.
-Proof. split. done. apply _. Qed.
+Proof. split; first done. apply _. Qed.
+Global Instance frame_lft_tok p κ q1 q2 q :
+  FrameFractionalQp q1 q2 q →
+  Frame p q1.[κ] q2.[κ] q.[κ] | 5.
+(* FIXME(https://github.com/coq/coq/issues/17688): Φ is not inferred. *)
+Proof. apply: (frame_fractional (λ q, q.[κ])%I). Qed.
+
 Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
 Proof.
   intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
-  rewrite -auth_frag_op op_singleton pair_op agree_idemp. done.
+  rewrite -auth_frag_op singleton_op -pair_op agree_idemp. done.
 Qed.
 Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
-Proof. split. done. apply _. Qed.
+Proof. split; first done. apply _. Qed.
+Global Instance frame_idx_bor_own p i q1 q2 q :
+  FrameFractionalQp q1 q2 q →
+  Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
+(* FIXME(https://github.com/coq/coq/issues/17688): Φ is not inferred. *)
+Proof. apply: (frame_fractional (λ q, idx_bor_own q i)%I). Qed.
 
 (** Lifetime inclusion *)
 Lemma lft_incl_acc E κ κ' q :
@@ -320,25 +403,27 @@ Proof.
 Qed.
 
 Lemma lft_incl_intro κ κ' :
-  □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
-               lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
-      (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
-Proof. reflexivity. Qed.
+  □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+      ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
+Proof. iIntros "?". done. Qed.
 
-Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
+Lemma lft_intersect_incl_l κ κ' : ⊢ κ ⊓ κ' ⊑ κ.
 Proof.
-  iIntros (->%gmultiset_union_difference) "!#". iSplitR.
+  unfold lft_incl. iIntros "!>". iSplitR.
   - iIntros (q). rewrite <-lft_tok_sep. iIntros "[H Hf]". iExists q. iFrame.
     rewrite <-lft_tok_sep. by iIntros "!>{$Hf}$".
   - iIntros "? !>". iApply lft_dead_or. auto.
 Qed.
 
-Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
-Proof. by apply lft_le_incl. Qed.
+Lemma lft_intersect_incl_r κ κ' : ⊢ κ ⊓ κ' ⊑ κ'.
+Proof. rewrite comm. apply lft_intersect_incl_l. Qed.
+
+Lemma lft_incl_refl κ : ⊢ κ ⊑ κ.
+Proof. unfold lft_incl. iIntros "!>"; iSplitR; auto 10 with iFrame. Qed.
 
-Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
+Lemma lft_incl_trans κ κ' κ'' : κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
 Proof.
-  rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†] !#". iSplitR.
+  rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†] !>". iSplitR.
   - iIntros (q) "Hκ".
     iMod ("H1" with "Hκ") as (q') "[Hκ' Hclose]".
     iMod ("H2" with "Hκ'") as (q'') "[Hκ'' Hclose']".
@@ -347,52 +432,54 @@ Proof.
   - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
 Qed.
 
-Lemma lft_glb_acc κ κ' q q' :
-  q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
+Lemma lft_intersect_acc κ κ' q q' :
+  q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
 Proof.
   iIntros "Hκ Hκ'".
-  destruct (Qp_lower_bound q q') as (qq & q0 & q'0 & -> & ->).
+  destruct (Qp.lower_bound q q') as (qq & q0 & q'0 & -> & ->).
   iExists qq. rewrite -lft_tok_sep.
   iDestruct "Hκ" as "[$$]". iDestruct "Hκ'" as "[$$]". auto.
 Qed.
 
-Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
 Proof.
-  rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
+  rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!>". iSplitR.
   - iIntros (q) "[Hκ'1 Hκ'2]".
     iMod ("H1" with "Hκ'1") as (q') "[Hκ' Hclose']".
     iMod ("H2" with "Hκ'2") as (q'') "[Hκ'' Hclose'']".
-    iDestruct (lft_glb_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
+    iDestruct (lft_intersect_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
     iExists qq. iFrame. iIntros "!> Hqq".
     iDestruct ("Hclose" with "Hqq") as "[Hκ' Hκ'']".
     iMod ("Hclose'" with "Hκ'") as "$". by iApply "Hclose''".
-  - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
+  - rewrite -lft_dead_or. iIntros "[H†|H†]".
+    + by iApply "H1†".
+    + by iApply "H2†".
 Qed.
 
-Lemma lft_glb_mono κ1 κ1' κ2 κ2' :
-  κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+Lemma lft_intersect_mono κ1 κ1' κ2 κ2' :
+  κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ⊓ κ2 ⊑ κ1' ⊓ κ2'.
 Proof.
   iIntros "#H1 #H2". iApply (lft_incl_glb with "[]").
-  - iApply (lft_incl_trans with "[] H1").
-    iApply lft_le_incl. apply gmultiset_union_subseteq_l.
-  - iApply (lft_incl_trans with "[] H2").
-    iApply lft_le_incl. apply gmultiset_union_subseteq_r.
+  - iApply (lft_incl_trans with "[] H1"). iApply lft_intersect_incl_l.
+  - iApply (lft_incl_trans with "[] H2"). iApply lft_intersect_incl_r.
 Qed.
 
 (** Basic rules about borrows *)
-Lemma raw_bor_iff_proper i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'.
+Lemma raw_bor_iff i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'.
 Proof.
   iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
   iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
-  iNext. iAlways. iSplit; iIntros.
-  by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
+  iNext. iModIntro. iSplit; iIntros.
+  - by iApply "HPP'"; iApply "Hiff".
+  - by iApply "Hiff"; iApply "HPP'".
 Qed.
 
-Lemma idx_bor_iff_proper κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
+Lemma idx_bor_iff κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 Proof.
   unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
-  iExists P0. iFrame. iNext. iAlways. iSplit; iIntros.
-  by iApply "HPP'"; iApply "HP0P". by iApply "HP0P"; iApply "HPP'".
+  iExists P0. iFrame. iNext. iModIntro. iSplit; iIntros.
+  - by iApply "HPP'"; iApply "HP0P".
+  - by iApply "HP0P"; iApply "HPP'".
 Qed.
 
 Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
@@ -400,14 +487,13 @@ Proof.
   rewrite /bor /raw_bor /idx_bor /bor_idx. iSplit.
   - iDestruct 1 as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
     iExists (κ', s). by iFrame.
-  - iDestruct 1 as ([κ' s]) "[[??]?]".
-    iExists κ'. iFrame. iExists s. by iFrame.
+  - iDestruct 1 as ([κ' s]) "[[??]?]". iFrame.
 Qed.
 
-Lemma bor_iff_proper κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
+Lemma bor_iff κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
 Proof.
   rewrite !bor_unfold_idx. iIntros "#HPP' HP". iDestruct "HP" as (i) "[??]".
-  iExists i. iFrame. by iApply (idx_bor_iff_proper with "HPP'").
+  iExists i. iFrame. by iApply (idx_bor_iff with "HPP'").
 Qed.
 
 Lemma bor_shorten κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
@@ -446,25 +532,25 @@ Proof.
     as (γE) "(% & #Hslice & Hbox)".
   iMod (own_inh_update with "HE") as "[HE HE◯]".
   { by eapply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[γE]}),
-      disjoint_singleton_l, lookup_to_gmap_None. }
+      disjoint_singleton_l, lookup_gset_to_gmap_None. }
   iModIntro. iSplitL "Hbox HE".
   { iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
-    rewrite to_gmap_union_singleton. iFrame. }
-  clear dependent PE. rewrite -(left_id_L ∅ op (◯ GSet {[γE]})).
+    rewrite gset_to_gmap_union_singleton. iFrame. }
+  clear dependent PE. rewrite -(left_id ε op (◯ GSet {[γE]})).
   iDestruct "HE◯" as "[HE◯' HE◯]". iSplitL "HE◯'".
   { iIntros (I) "HI". iApply (own_inh_auth with "HI HE◯'"). }
   iIntros (Q'). rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
   iDestruct (own_inh_valid_2 with "HE HE◯")
-    as %[Hle%gset_disj_included _]%auth_valid_discrete_2.
+    as %[Hle%gset_disj_included _]%auth_both_valid_discrete.
   iMod (own_inh_update_2 with "HE HE◯") as "HE".
   { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
   iMod (slice_delete_full _ _ true with "Hslice Hbox")
     as (Q'') "($ & #? & Hbox)"; first by solve_ndisj.
-  { rewrite lookup_to_gmap_Some. set_solver. }
+  { rewrite lookup_gset_to_gmap_Some. set_solver. }
   iModIntro. iExists Q''. iSplit; first done.
   iNext. rewrite /lft_inh. iExists (PE ∖ {[γE]}). iFrame "HE".
   rewrite {1}(union_difference_L {[ γE ]} PE); last set_solver.
-  rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None.
+  rewrite gset_to_gmap_union_singleton delete_insert // lookup_gset_to_gmap_None.
   set_solver.
 Qed.
 
@@ -475,7 +561,7 @@ Proof.
   rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
   iDestruct "Hinh" as (E') "[Hinh Hbox]".
   iMod (box_fill with "Hbox HQ") as "?"=>//.
-  rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
+  rewrite fmap_gset_to_gmap. iModIntro. iExists E'. by iFrame.
 Qed.
 
 (* View shifts *)
@@ -487,18 +573,16 @@ Proof.
   iApply ("Hvs" $! I'' with "Hinv HPb H†").
 Qed.
 
-(* TODO RJ: Are there still places where this lemma
-   is re-proven inline? *)
-Lemma lft_vs_cons q κ Pb Pb' Pi :
-  (lft_bor_dead κ ∗ ▷ Pb' ={⊤ ∖ ↑mgmtN}=∗ lft_bor_dead κ ∗ ▷ Pb) -∗
-  ▷?q lft_vs κ Pb Pi -∗ ▷?q lft_vs κ Pb' Pi.
+Lemma lft_vs_cons κ Pb Pb' Pi :
+  (▷ Pb'-∗ [†κ] ={userE ∪ ↑borN}=∗ ▷ Pb) -∗
+  lft_vs κ Pb Pi -∗ lft_vs κ Pb' Pi.
 Proof.
-  iIntros "Hcons Hvs". iNext. rewrite !lft_vs_unfold.
+  iIntros "Hcons Hvs". rewrite !lft_vs_unfold.
   iDestruct "Hvs" as (n) "[Hn● Hvs]". iExists n. iFrame "Hn●".
   iIntros (I). rewrite {1}lft_vs_inv_unfold.
-  iIntros "(Hdead & Hinv & Hκs) HPb #Hκ†".
-  iMod ("Hcons" with "[$Hdead $HPb]") as "[Hdead HPb]". 
-  iApply ("Hvs" $! I with "[Hdead Hinv Hκs] HPb Hκ†").
+  iIntros "(Hinv & Hκs) HPb #Hκ†".
+  iMod ("Hcons" with "HPb Hκ†") as "HPb".
+  iApply ("Hvs" $! I with "[Hinv Hκs] HPb Hκ†").
   rewrite lft_vs_inv_unfold. by iFrame.
 Qed.
 End primitive.

theories/lifetime/model/raw_reborrow.v → lifetime/model/reborrow.v

-From lrust.lifetime Require Export primitive.
-From lrust.lifetime Require Import faking.
-From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
+From lrust.lifetime Require Import borrow accessors.
+From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
 
-Section rebor.
-Context `{invG Σ, lftG Σ}.
+Section reborrow.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
    κ ≠ κ'.  Still, it is probably more instructing to require
    κ ⊂ κ' in this lemma (as opposed to just κ ⊆ κ'), and it
    should not increase the burden on the user. *)
-Lemma raw_bor_unnest E q A I Pb Pi P κ i κ' :
+Lemma raw_bor_unnest E A I Pb Pi P κ i κ' :
   ↑borN ⊆ E →
-  let Iinv := (own_ilft_auth I ∗ ▷?q lft_inv A κ)%I in
+  let Iinv := (own_ilft_auth I ∗ ▷ lft_inv A κ)%I in
   κ ⊂ κ' →
   lft_alive_in A κ' →
-  Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷?q lft_bor_alive κ' Pb -∗
-  ▷?q lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
-    Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
+  Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷ lft_bor_alive κ' Pb -∗
+  ▷ lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
+    Iinv ∗ raw_bor κ' P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
 Proof.
   iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
   rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
   iMod (own_cnt_update with "Hn●") as "[Hn● H◯]".
-  { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
+  { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); lia. }
   rewrite {1}/raw_bor /idx_bor_own /=.
   iDestruct (own_bor_auth with "HI Hi") as %?.
   assert (κ ⊆ κ') by (by apply strict_include).
@@ -36,15 +34,14 @@ Proof.
     iDestruct "Hκ" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
   rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
   iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
+    as %[HB%to_borUR_included _]%auth_both_valid_discrete.
+  iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
-  { eapply auth_update. (* FIXME: eapply singleton_local_update loops. *)
-    apply: singleton_local_update; last eapply
+  { eapply auth_update, singleton_local_update; last eapply
      (exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
-  iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
+  iAssert (▷ lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
   { iNext. rewrite /lft_inv. iLeft.
     iSplit; last by eauto using lft_alive_in_subseteq.
     rewrite lft_inv_alive_unfold. iExists Pb', Pi'. iFrame "Hvs' Hinh'".
@@ -52,20 +49,18 @@ Proof.
     rewrite /to_borUR !fmap_insert. iFrame "Hbox HB●".
     iDestruct (@big_sepM_delete with "HB") as "[_ HB]"; first done.
     rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
-    rewrite -insert_delete delete_insert ?lookup_delete //=. iFrame; auto. }
+    rewrite -insert_delete_insert delete_insert ?lookup_delete //=. iFrame; auto. }
   clear B HB Pb' Pi'.
   rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
-  iMod (slice_insert_full with "HP Hbox")
+  iMod (slice_insert_full _ _ true with "HP Hbox")
     as (j) "(HBj & #Hjslice & Hbox)"; first done.
   iDestruct "HBj" as %HBj; move: HBj; rewrite lookup_fmap fmap_None=> HBj.
   iMod (own_bor_update with "HB●") as "[HB● Hj]".
   { apply auth_update_alloc,
      (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
-  iModIntro. iExists (P ∗ Pb)%  I. rewrite /Iinv. iFrame "HI". iFrame.
-  iSplitL "Hj".
-  { rewrite /raw_bor /idx_bor_own. iExists j. iFrame. iExists P.
-    rewrite -uPred.iff_refl. auto. }
+  iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
+  { iExists j. iFrame. iExists P. rewrite -(bi.iff_refl emp). auto. }
   iSplitL "Hbox HB● HB".
   { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
     rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
@@ -73,129 +68,117 @@ Proof.
   clear dependent Iinv I.
   iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hn●".
   iIntros (I) "Hinv [HP HPb] #Hκ†".
-  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
-  iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
+  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(HI & Hinv)".
+  iDestruct (own_bor_auth with "HI Hi") as %?%(elem_of_dom (D:=gset lft)).
   iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
   rewrite lft_inv_alive_unfold.
-  iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
+  iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)".
   rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
-  iDestruct (own_bor_valid_2 with "HB● Hi") 
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
+  iDestruct (own_bor_valid_2 with "HB● Hi")
+    as %[HB%to_borUR_included _]%auth_both_valid_discrete.
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
   { eapply auth_update, singleton_local_update,
      (exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   iMod (slice_fill _ _ false with "Hislice HP Hbox")
-     as "Hbox"; first by solve_ndisj.
+     as "Hbox".
+  { set_solver+. }
   { by rewrite lookup_fmap HB. }
   iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
-  rewrite /=; iDestruct "Hcnt" as "[% H1◯]".
-  iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
-                         [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
-  { rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
-    iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
+  rewrite /=. iDestruct "Hcnt" as "[% H1◯]".
+  iMod ("Hvs" $! I with "[HI Hinv Hvs' Hinh HB● Hbox HB]
+                         [$HPb $Hi] Hκ†") as "($ & $ & Hcnt')".
+  { rewrite lft_vs_inv_unfold. iFrame "HI".
+    iApply (big_sepS_delete _ (dom I) with "[- $Hinv]"); first done.
     iIntros (_). rewrite lft_inv_alive_unfold.
     iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
     iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
-  { rewrite /raw_bor /idx_bor_own /=. auto. }
-  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
+    rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //=. by iFrame. }
+  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op.
   by iFrame.
 Qed.
 
-Lemma raw_bor_unnest' E q A I Pb Pi P κ κ' :
-  ↑borN ⊆ E →
-  let Iinv := (
-    own_ilft_auth I ∗
-    ▷?q [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
-  κ ⊆ κ' →
-  lft_alive_in A κ' →
-  Iinv -∗ raw_bor κ P -∗ ▷?q lft_bor_alive κ' Pb -∗
-  ▷?q lft_vs κ' (raw_bor κ P ∗ Pb) Pi ={E}=∗ ∃ Pb',
-    Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
+Lemma raw_idx_bor_unnest E κ κ' i P :
+  ↑lftN ⊆ E → κ ⊂ κ' →
+  lft_ctx -∗ slice borN i P -∗ raw_bor κ' (idx_bor_own 1 (κ, i))
+  ={E}=∗ raw_bor κ' P.
 Proof.
-  iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hinv) Hraw Hκalive' Hvs".
-  destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iModIntro. iExists Pb. rewrite /Iinv. iFrame "HI Hinv Hκalive' Hraw".
-    iApply (lft_vs_cons with "[]"); last done.
-    iIntros "(Hdead & HPb)".
-    iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
-    by iFrame. }
-  assert (κ ⊂ κ') by (by apply strict_spec_alt).
-  iDestruct (raw_bor_inI with "HI Hraw") as %HI.
-  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose]".
-  { rewrite elem_of_difference elem_of_dom not_elem_of_singleton. done. }
-  rewrite {1}/raw_bor. iDestruct "Hraw" as (i) "[Hi #Hislice]".
-  iDestruct "Hislice" as (P') "[#HPP' Hislice]".
-  iMod (raw_bor_unnest with "[$HI $Hinv] Hi Hislice Hκalive' [Hvs]")
-    as (Pb') "([HI Hκ] & ? & ? & ?)"; [done..| |].
-  { iApply (lft_vs_cons with "[]"); last done.
-    iIntros "[$ [>? $]]". iModIntro. iNext. rewrite /raw_bor.
-    iExists i. iFrame. iExists _. iFrame "#". }
-  iExists Pb'. iModIntro. iFrame. iSplitL "Hclose Hκ". by iApply "Hclose".
-  by iApply (raw_bor_iff_proper with "HPP'").
+  iIntros (? Hκκ') "#LFT #Hs Hraw".
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  iDestruct (raw_bor_inI with "HI Hraw") as %HI'.
+  rewrite (big_sepS_delete _ _ κ') ?elem_of_dom // [_ A κ']/lft_inv.
+  iDestruct "Hinv" as "[[[Hinvκ >%]|[Hinvκ >%]] Hinv]"; last first.
+  { rewrite /lft_inv_dead. iDestruct "Hinvκ" as (Pi) "[Hbordead H]".
+    iMod (raw_bor_fake with "Hbordead") as "[Hbordead $]"; first solve_ndisj.
+    iApply "Hclose". iExists _, _. iFrame.
+    rewrite (big_opS_delete _ (dom _) κ') ?elem_of_dom // /lft_inv /lft_inv_dead.
+    auto 10 with iFrame. }
+  rewrite {1}/raw_bor. iDestruct "Hraw" as (i') "[Hbor H]".
+  iDestruct "H" as (P') "[#HP' #Hs']".
+  rewrite lft_inv_alive_unfold /lft_bor_alive [in _ _ (κ', i')]/idx_bor_own.
+  iDestruct "Hinvκ" as (Pb Pi) "(Halive & Hvs & Hinh)".
+  iDestruct "Halive" as (B) "(Hbox & >H● & HB)".
+  iDestruct (own_bor_valid_2 with "H● Hbor")
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
+  iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]";
+    first solve_ndisj.
+  { by rewrite lookup_fmap EQB. }
+  iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
+  iDestruct (own_bor_auth with "HI [Hidx]") as %HI; [by rewrite /idx_bor_own|].
+  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinvκ Hclose']";
+    first by rewrite elem_of_difference elem_of_dom not_elem_of_singleton;
+    eauto using strict_ne.
+  iMod (slice_delete_empty with "Hs' Hbox") as (Pb') "[#HeqPb' Hbox]";
+    [solve_ndisj|by apply lookup_insert|].
+  iMod (own_bor_update_2 with "H● Hbor") as "H●".
+  { apply auth_update_dealloc, delete_singleton_local_update. apply _. }
+  iMod (raw_bor_unnest with "[$HI $Hinvκ] Hidx Hs [Hbox H● HB] [Hvs]")
+    as (Pb'') "HH"; [solve_ndisj|done|done| | |].
+  { rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
+    iExists (delete i' B). rewrite -fmap_delete. iFrame.
+    rewrite fmap_delete -insert_delete_insert delete_insert ?lookup_delete //=. }
+  { iNext. iApply (lft_vs_cons with "[] Hvs"). iIntros "[??] _ !>". iNext.
+    iRewrite "HeqPb'". iFrame. by iApply "HP'". }
+  iDestruct "HH" as "([HI Hinvκ] & $ & Halive & Hvs)".
+  iApply "Hclose". iExists _, _. iFrame.
+  rewrite (big_opS_delete _ (dom _) κ') ?elem_of_dom //.
+  iDestruct ("Hclose'" with "Hinvκ") as "$".
+  rewrite /lft_inv lft_inv_alive_unfold. auto 10 with iFrame.
 Qed.
 
-Lemma raw_rebor E κ κ' P :
+Lemma raw_bor_shorten E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ raw_bor κ P ={E}=∗
-    raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
+  lft_ctx -∗ raw_bor κ P ={E}=∗ raw_bor κ' P.
 Proof.
-  rewrite /lft_ctx. iIntros (??) "#LFT Hκ".
-  destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iFrame. iIntros "!> #Hκ†". by iApply (raw_bor_fake' with "LFT Hκ†"). }
+  iIntros (? Hκκ') "#LFT Hbor".
+  destruct (decide (κ = κ')) as [<-|Hκneq]; [by iFrame|].
   assert (κ ⊂ κ') by (by apply strict_spec_alt).
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
-  clear A I; rename A' into A; rename I' into I.
-  iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[? >%]|[Hdead >%]]"; last first.
-  { rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & >H● & Hinh)".
-    iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead $]"; first solve_ndisj.
-    iMod ("Hclose" with "[-Hκ]") as "_"; last auto.
-    iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
-    iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom.
-    iFrame "Hinv". rewrite /lft_inv /lft_inv_dead. iRight.
-    iSplit; last done. iExists Pi. by iFrame. }
-  rewrite lft_inv_alive_unfold; iDestruct "Hκinv'" as (Pb Pi) "(Hbor & Hvs & Hinh)".
-  rewrite {1}/raw_bor. iDestruct "Hκ" as (i) "[Hi #Hislice]".
-  iDestruct "Hislice" as (P') "[#HPP' Hislice]".
-  iMod (lft_inh_extend _ _ (idx_bor_own 1 (κ, i)) with "Hinh")
-    as "(Hinh & HIlookup & Hinh_close)"; first solve_ndisj.
-  iDestruct (own_bor_auth with "HI [Hi]") as %?.
-  { by rewrite /idx_bor_own. }
-  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hκ Hκclose]".
-  { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
-  iMod (raw_bor_unnest _ true _ _ _ (idx_bor_own 1 (κ, i) ∗ Pi)%I
-    with "[$HI $Hκ] Hi Hislice Hbor [Hvs]")
-    as (Pb') "([HI Hκ] & HP' & Halive & Hvs)"; [solve_ndisj|done|done|..].
-  { iNext. by iApply lft_vs_frame. }
-  iDestruct (raw_bor_iff_proper with "HPP' HP'") as "$".
-  iDestruct ("Hκclose" with "Hκ") as "Hinv".
-  iMod ("Hclose" with "[HA HI Hinv Halive Hinh Hvs]") as "_".
-  { iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
-    iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
-    rewrite /lft_inv. iLeft. iSplit; last done.
-    rewrite lft_inv_alive_unfold. iExists Pb', (idx_bor_own 1 (κ, i) ∗ Pi)%I.
-    iFrame. }
-  clear dependent A I Pb Pb' Pi. iModIntro. iIntros "H†".
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iDestruct ("HIlookup" with "HI") as %Hκ'.
-  iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[Halive >%]|[Hdead >%]]".
-  - (* the same proof is in bor_fake and bor_create *)
-    rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
-    iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
-    unfold lft_alive_in in *. naive_solver.
-  - rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & Hcnt & Hinh)".
-    iMod ("Hinh_close" $! Pi with "Hinh") as (Pi') "(Heq & >Hbor & Hinh)".
-    iMod ("Hclose" with "[HA HI Hinv Hdead Hinh Hcnt]") as "_".
-    { iNext. rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
-      iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
-      rewrite /lft_inv /lft_inv_dead. iRight. iSplit; last done.
-      iExists Pi'. iFrame. }
-    iModIntro. rewrite /raw_bor. iExists i. iFrame. iExists _. auto.
+  rewrite [_ κ P]/raw_bor. iDestruct "Hbor" as (s) "[Hbor Hs]".
+  iDestruct "Hs" as (P') "[#HP'P #Hs]".
+  iMod (raw_bor_create _ κ' with "LFT Hbor") as "[Hbor _]"; [done|].
+  iApply (raw_bor_iff with "HP'P"). by iApply raw_idx_bor_unnest.
+Qed.
+
+Lemma idx_bor_unnest E κ κ' i P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ,i} P -∗ &{κ'}(idx_bor_own 1 i) ={E}=∗ &{κ ⊓ κ'} P.
+Proof.
+  iIntros (?) "#LFT #HP Hbor".
+  rewrite [(&{κ'}_)%I]/bor. iDestruct "Hbor" as (κ'0) "[#Hκ'κ'0 Hbor]".
+  destruct (decide (κ'0 = static)) as [->|Hκ'0].
+  { iMod (bor_acc_strong with "LFT [Hbor] []") as (?) "(_ & Hbor & _)";
+      [done| |iApply (lft_tok_static 1)|].
+    - rewrite /bor. iExists static. iFrame. iApply lft_incl_refl.
+    - iDestruct "Hbor" as ">Hbor".
+      iApply bor_shorten; [|by rewrite bor_unfold_idx; auto].
+      iApply lft_intersect_incl_l. }
+  rewrite /idx_bor /bor. destruct i as [κ0 i].
+  iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
+  iMod (raw_bor_shorten _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "Hbor";
+    [done|by apply gmultiset_disj_union_subseteq_r|].
+  iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
+    [done|by apply gmultiset_disj_union_subset_l|].
+  iExists _. iDestruct (raw_bor_iff with "HPP' Hbor") as "$".
+    by iApply lft_intersect_mono.
 Qed.
-End rebor.
+End reborrow.

theories/lifetime/na_borrow.v → lifetime/na_borrow.v

 From lrust.lifetime Require Export lifetime.
 From iris.base_logic.lib Require Export na_invariants.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
 
-Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
+Definition na_bor `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
-Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
-  (format "&na{ κ , tid , N }  P", at level 20, right associativity) : uPred_scope.
+Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
+    (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{invG Σ, lftG Σ, na_invG Σ}
+  Context `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
@@ -20,14 +20,15 @@ Section na_bor.
   Proof. solve_contractive. Qed.
   Global Instance na_bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
   Proof. solve_proper. Qed.
-  Lemma na_bor_iff_proper κ P' :
+
+  Lemma na_bor_iff κ P' :
     ▷ □ (P ↔ P') -∗ &na{κ, tid, N} P -∗ &na{κ, tid, N} P'.
   Proof.
     iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
-    iApply (idx_bor_iff_proper with "HPP' HP").
+    iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
-  Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.
+  Global Instance na_bor_persistent κ : Persistent (&na{κ,tid,N} P) := _.
 
   Lemma bor_na κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &na{κ,tid,N}P.
   Proof.
@@ -43,23 +44,23 @@ Section na_bor.
   Proof.
     iIntros (???) "#LFT#HP Hκ Hnaown".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
-    iMod (na_inv_open with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
-    iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
-    iIntros "{$HP $Hnaown}!>HP Hnaown".
+    iMod (na_inv_acc with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
+    iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']"; first done.
+    iIntros "{$HP $Hnaown} !> HP Hnaown".
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
   Lemma na_bor_shorten κ κ': κ ⊑ κ' -∗ &na{κ',tid,N}P -∗ &na{κ,tid,N}P.
   Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+    iIntros "Hκκ' H". iDestruct "H" as (i) "[H ?]". iExists i. iFrame.
     iApply (idx_bor_shorten with "Hκκ' H").
   Qed.
 
   Lemma na_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &na{κ,tid,N}P.
   Proof.
-    iIntros (?) "#LFT#H†". iApply (bor_na with ">"). done.
+    iIntros (?) "#LFT#H†". iApply (bor_na with "[>]"); first done.
     by iApply (bor_fake with "LFT H†").
   Qed.
 End na_bor.
 
-Typeclasses Opaque na_bor.
+Global Typeclasses Opaque na_bor.

make-package

+#!/bin/bash
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
+    echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+make -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*

opam

-opam-version: "1.2"
-name: "coq-lambda-rust"
-version: "dev"
-maintainer: "Ralf Jung <jung@mpi-sws.org>"
-authors: "The RustBelt Team"
-homepage: "http://plv.mpi-sws.org/rustbelt/"
-bug-reports: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq/issues"
-dev-repo: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq.git"
-build: [
-  [make "-j%{jobs}%"]
-]
-install: [make "install"]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
-depends: [
-  "coq-iris"
-]

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 939b747baa303ca3e2e1538cfd76fccd900596cf

theories/lang/derived.v

-From lrust.lang Require Export lifting.
-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
-Set Default Proof Using "Type".
-Import uPred.
-
-(** Define some derived forms, and derived lemmas about them. *)
-Notation Lam xl e := (Rec BAnon xl e).
-Notation Let x e1 e2 := (App (Lam [x] e2) [e1]).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV xl e := (RecV BAnon xl e).
-Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Coercion lit_of_bool : bool >-> base_lit.
-Notation If e0 e1 e2 := (Case e0 [e2;e1]).
-Notation Newlft := (Lit LitUnit) (only parsing).
-Notation Endlft := Skip (only parsing).
-
-Section derived.
-Context `{ownPG lrust_lang Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-
-(** Proof rules for working on the n-ary argument list. *)
-Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el)) vs Φ:
-  is_Some (to_val f) →
-  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
-    (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
-                    WP App f (of_val <$> vs ++ vl) @ E {{ Φ }}) -∗
-    WP App f ((of_val <$> vs) ++ el) @ E {{ Φ }}.
-Proof.
-  intros [vf Hf]. revert vs Ql. induction el as [|e el IH]=>/= vs Ql; inv_vec Ql.
-  - iIntros "_ H". iSpecialize ("H" $! [#]). rewrite !app_nil_r big_sepL_nil.
-      by iApply "H".
-  - intros Q Ql. rewrite /= big_sepL_cons /=. iIntros "[He Hl] HΦ".
-    assert (App f ((of_val <$> vs) ++ e :: el) = fill_item (AppRCtx vf vs el) e)
-      as -> by rewrite /= (of_to_val f) //.
-    iApply wp_bindi. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
-    rewrite cons_middle (assoc app) -(fmap_app _ _ [v]) (of_to_val f) //.
-    iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
-    iApply ("HΦ" $! (v:::vl)). rewrite /= big_sepL_cons. iFrame.
-Qed.
-
-Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
-  is_Some (to_val f) →
-  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
-    (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
-                    WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
-    WP App f el @ E {{ Φ }}.
-Proof.
-  iIntros (Hf). iApply (wp_app_ind _ _ _ _ []). done.
-Qed.
-
-Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
-  length Ql = length el → is_Some (to_val f) →
-  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
-    (∀ vl : list val, ⌜length vl = length el⌝ -∗
-            ([∗ list] k ↦ vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
-             WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
-    WP App f el @ E {{ Φ }}.
-Proof.
-  iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_of_list Ql).
-  generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
-  iApply (wp_app_vec with "Hel"); first done. iIntros (vl) "Hvl".
-  iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
-Qed.
-
-(** Proof rules for the sugar *)
-Lemma wp_lam E xl e eb e' el Φ :
-  e = Lam xl eb →
-  Forall (λ ei, is_Some (to_val ei)) el →
-  Closed (xl +b+ []) eb →
-  subst_l xl el eb = Some e' →
-  ▷ WP e' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
-Proof.
-  iIntros (-> ???) "?". iApply (wp_rec _ _ BAnon)=>//.
-    by rewrite /= option_fmap_id.
-Qed.
-
-Lemma wp_let E x e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed (x :b: []) e2 →
-  ▷ WP subst' x e1 e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. eauto using wp_lam. Qed.
-
-Lemma wp_let' E x e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed (x :b: []) e2 →
-  ▷ WP subst' x (of_val v) e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. intros ?. rewrite (of_to_val e1) //. eauto using wp_let. Qed.
-
-Lemma wp_seq E e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} -∗ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ E {{ Φ }}.
-Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
-
-Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P -∗ ▷ Φ (LitV true)) →
-  (n2 < n1 → P -∗ ▷ Φ (LitV false)) →
-  P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  iIntros (Hl Hg) "HP".
-  destruct (bool_decide_reflect (n1 ≤ n2)); [rewrite Hl //|rewrite Hg; last omega];
-    clear Hl Hg; (iApply wp_bin_op_pure; first by econstructor); iNext; iIntros (?? Heval);
-    inversion_clear Heval; [rewrite bool_decide_true //|rewrite bool_decide_false //].
-Qed.
-
-Lemma wp_eq_int E (n1 n2 : Z) P Φ :
-  (n1 = n2 → P -∗ ▷ Φ (LitV true)) →
-  (n1 ≠ n2 → P -∗ ▷ Φ (LitV false)) →
-  P -∗ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  iIntros (Hl Hg) "HP".
-  destruct (bool_decide_reflect (n1 = n2)); [rewrite Hl //|rewrite Hg //];
-    clear Hl Hg; iApply wp_bin_op_pure; subst.
-  - intros. apply BinOpEqTrue. constructor.
-  - iNext; iIntros (?? Heval). inversion_clear Heval. done. by inversion H.
-  - intros. apply BinOpEqFalse. by constructor.
-  - iNext; iIntros (?? Heval). inversion_clear Heval. by inversion H. done.
-Qed.
-
-(* TODO : wp_eq for locations, if needed. *)
-
-Lemma wp_offset E l z Φ :
-  ▷ Φ (LitV $ LitLoc $ shift_loc l z) -∗
-    WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
-  iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-Lemma wp_plus E z1 z2 Φ :
-  ▷ Φ (LitV $ LitInt $ z1 + z2) -∗
-    WP BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
-  iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-Lemma wp_minus E z1 z2 Φ :
-  ▷ Φ (LitV $ LitInt $ z1 - z2) -∗
-    WP BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
-  iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-(* TODO: Add lemmas for equality test. *)
-
-Lemma wp_if E (b : bool) e1 e2 Φ :
-  (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
-  WP If (Lit b) e1 e2 @ E {{ Φ }}.
-Proof. iIntros "?". by destruct b; iApply wp_case. Qed.
-End derived.

theories/lang/lifting.v

-From iris.program_logic Require Export weakestpre ownp.
-From iris.program_logic Require Import ectx_lifting.
-From lrust.lang Require Export lang.
-From lrust.lang Require Import tactics.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-Import uPred.
-Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
-
-(* TODO : as for heap_lang, directly use a global heap invariant. *)
-
-Section lifting.
-Context `{ownPG lrust_lang Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types ef : option expr.
-
-(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
-Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} -∗ WP fill K e @ E {{ Φ }}.
-Proof. exact: wp_ectx_bind. Qed.
-
-Lemma wp_bindi {E e} Ki Φ :
-  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} -∗
-     WP fill_item Ki e @ E {{ Φ }}.
-Proof. exact: weakestpre.wp_bind. Qed.
-
-(** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ n:
-  0 < n →
-  {{{ ▷ ownP σ }}} Alloc (Lit $ LitInt n) @ E
-  {{{ l σ', RET LitV $ LitLoc l;
-      ⌜∀ m, σ !! (shift_loc l m) = None⌝ ∗
-      ⌜∃ vl, n = length vl ∧ init_mem l vl σ = σ'⌝ ∗
-      ownP σ' }}}.
-Proof.
-  iIntros (? Φ) "HP HΦ". iApply (ownP_lift_atomic_head_step _ σ); eauto.
-  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
-  rewrite big_sepL_nil right_id. by iApply "HΦ"; iFrame; eauto.
-Qed.
-
-Lemma wp_free_pst E σ l n :
-  0 < n →
-  (∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)) →
-  {{{ ▷ ownP σ }}} Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
-  {{{ RET LitV $ LitUnit; ownP (free_mem l (Z.to_nat n) σ) }}}.
-Proof.
-  iIntros (???)  "HP HΦ". iApply (ownP_lift_atomic_head_step _ σ); eauto.
-  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
-  rewrite big_sepL_nil right_id. by iApply "HΦ".
-Qed.
-
-Lemma wp_read_sc_pst E σ l n v :
-  σ !! l = Some (RSt n, v) →
-  {{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ RET v; ownP σ }}}.
-Proof.
-  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto using to_of_val.
-  rewrite big_sepL_nil right_id; iFrame.
-Qed.
-
-Lemma wp_read_na2_pst E σ l n v :
-  σ !! l = Some(RSt $ S n, v) →
-  {{{ ▷ ownP σ }}} Read Na2Ord (Lit $ LitLoc l) @ E
-  {{{ RET v; ownP (<[l:=(RSt n, v)]>σ) }}}.
-Proof.
-  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto using to_of_val.
-  rewrite big_sepL_nil right_id; iFrame.
-Qed.
-
-Lemma wp_read_na1_pst E l Φ :
-  (|={E,∅}=> ∃ σ n v, ⌜σ !! l = Some(RSt $ n, v)⌝ ∧
-     ▷ ownP σ ∗
-     ▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
-          WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }})) -∗
-  WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
-Proof.
-  iIntros "HΦP". iApply (ownP_lift_head_step E); auto.
-  iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
-  iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
-  rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
-Qed.
-
-Lemma wp_write_sc_pst E σ l v v' :
-  σ !! l = Some (RSt 0, v') →
-  {{{ ▷ ownP σ }}} Write ScOrd (Lit $ LitLoc l) (of_val v) @ E
-  {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
-Proof.
-  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
-Qed.
-
-Lemma wp_write_na2_pst E σ l v v' :
-  σ !! l = Some(WSt, v') →
-  {{{ ▷ ownP σ }}} Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E
-  {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
-Proof.
-  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
-Qed.
-
-Lemma wp_write_na1_pst E l v Φ :
-  (|={E,∅}=> ∃ σ v', ⌜σ !! l = Some(RSt 0, v')⌝ ∧
-     ▷ ownP σ ∗
-     ▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=∗
-       WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }})) -∗
-  WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
-Proof.
-  iIntros "HΦP". iApply (ownP_lift_head_step E); auto.
-  iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
-  iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
-  rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
-Qed.
-
-Lemma wp_cas_pst E n σ l e1 lit1 lit2 litl :
-  to_val e1 = Some $ LitV lit1 →
-  σ !! l = Some (RSt n, LitV litl) →
-  (lit_eq σ lit1 litl ∨ lit_neq σ lit1 litl) →
-  (lit_eq σ lit1 litl → n = 0%nat) →
-  {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (Lit lit2) @ E
-  {{{ b, RET LitV $ lit_of_bool b;
-      if b is true then ⌜lit_eq σ lit1 litl⌝ ∗ ownP (<[l:=(RSt 0, LitV lit2)]>σ)
-      else ⌜lit_neq σ lit1 litl⌝ ∗ ownP σ }}}.
-Proof.
-  iIntros (?%of_to_val ? Hdec Hn ?) "HP HΦ". subst.
-  iApply ownP_lift_atomic_head_step; eauto.
-  { destruct Hdec as [Heq|Hneq].
-    - specialize (Hn Heq). subst. do 3 eexists. by eapply CasSucS.
-    - do 3 eexists. by eapply CasFailS. }
-  iFrame. iNext. iIntros (e2 σ2 efs Hs) "Ho".
-  inv_head_step; rewrite big_sepL_nil right_id.
-  - iApply ("HΦ" $! false). eauto.
-  - iApply ("HΦ" $! true). eauto.
-  - exfalso. refine (_ (Hn _)); last done. intros. omega.
-Qed.
-
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e :
-  {{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
-Proof.
-  iIntros (?) "?HΦ". iApply ownP_lift_pure_det_head_step; eauto.
-  by intros; inv_head_step; eauto. iNext.
-  rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
-Qed.
-
-Lemma wp_rec E e f xl erec erec' el Φ :
-  e = Rec f xl erec →
-  Forall (λ ei, is_Some (to_val ei)) el →
-  Closed (f :b: xl +b+ []) erec →
-  subst_l (f::xl) (e::el) erec = Some erec' →
-  ▷ WP erec' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
-Proof.
-  iIntros (-> ???) "?". iApply ownP_lift_pure_det_head_step; subst; eauto.
-  by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
-Qed.
-
-Lemma wp_bin_op_heap E σ op l1 l2 l' :
-  bin_op_eval σ op l1 l2 l' →
-  {{{ ▷ ownP σ }}} BinOp op (Lit l1) (Lit l2) @ E
-  {{{ l'', RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ ∗ ownP σ }}}.
-Proof.
-  iIntros (? Φ) "HP HΦ". iApply ownP_lift_atomic_head_step; eauto.
-  iFrame "HP". iNext. iIntros (e2 σ2 efs Hs) "Ho".
-  inv_head_step; rewrite big_sepL_nil right_id.
-  iApply "HΦ". eauto.
-Qed.
-
-Lemma wp_bin_op_pure E op l1 l2 l' :
-  (∀ σ, bin_op_eval σ op l1 l2 l') →
-  {{{ True }}} BinOp op (Lit l1) (Lit l2) @ E
-  {{{ l'' σ, RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ }}}.
-Proof.
-  iIntros (? Φ) "HΦ". iApply ownP_lift_pure_head_step; eauto.
-  { intros. inv_head_step. done. }
-  iNext. iIntros (e2 efs σ Hs).
-  inv_head_step; rewrite big_sepL_nil right_id.
-  rewrite -wp_value //. iApply "HΦ". eauto.
-Qed.
-
-Lemma wp_case E i e el Φ :
-  0 ≤ i →
-  el !! (Z.to_nat i) = Some e →
-  ▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
-Proof.
-  iIntros (??) "?". iApply ownP_lift_pure_det_head_step; eauto.
-  by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
-Qed.
-End lifting.

theories/lang/proofmode.v

-From iris.base_logic Require Import namespaces.
-From iris.program_logic Require Export weakestpre.
-From iris.proofmode Require Import coq_tactics.
-From iris.proofmode Require Export tactics.
-From lrust.lang Require Export tactics derived heap.
-Set Default Proof Using "Type".
-Import uPred.
-
-(** wp-specific helper tactics *)
-Ltac wp_bind_core K :=
-  lazymatch eval hnf in K with
-  | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
-  end.
-
-(* Solves side-conditions generated by the wp tactics *)
-Ltac wp_done :=
-  match goal with
-  | |- Closed _ _ => solve_closed
-  | |- is_Some (to_val _) => solve_to_val
-  | |- to_val _ = Some _ => solve_to_val
-  | |- language.to_val _ = Some _ => solve_to_val
-  | |- Forall _ [] => fast_by apply List.Forall_nil
-  | |- Forall _ (_ :: _) => apply List.Forall_cons; wp_done
-  | _ => fast_done
-  end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
-
-Ltac wp_seq_head :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-    etrans; [|eapply wp_seq; wp_done]; iNext
-  end.
-
-Ltac wp_finish := intros_revert ltac:(
-  rewrite /= ?to_of_val;
-  try iNext;
-  repeat lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-     etrans; [|eapply wp_seq; wp_done]; iNext
-  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
-  end).
-
-Tactic Notation "wp_value" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
-  | _ => fail "wp_value: not a wp"
-  end.
-
-Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
-Proof. by unlock. Qed.
-
-(* Applied to goals that are equalities of expressions. Will try to unlock the
-   LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
-Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
-
-Tactic Notation "wp_rec" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with App ?e1 _ =>
-(* hnf does not reduce through an of_val *)
-(*      match eval hnf in e1 with Rec _ _ _ => *)
-    wp_bind_core K; etrans;
-      [|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
-(*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
-  | _ => fail "wp_rec: not a 'wp'"
-  end.
-
-Tactic Notation "wp_lam" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with App ?e1 _ =>
-(*    match eval hnf in e1 with Rec BAnon _ _ => *)
-    wp_bind_core K; etrans;
-      [|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
-(*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
-  | _ => fail "wp_lam: not a 'wp'"
-  end.
-
-Tactic Notation "wp_let" := wp_lam.
-Tactic Notation "wp_seq" := wp_let.
-
-Tactic Notation "wp_op" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
-    | BinOp EqOp _ _ => wp_bind_core K; apply wp_eq_int; wp_finish
-    | BinOp OffsetOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
-    | BinOp PlusOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_plus; try fast_done]; wp_finish
-    | BinOp MinusOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_minus; try fast_done]; wp_finish
-    end) || fail "wp_op: cannot find 'BinOp' in" e
-  | _ => fail "wp_op: not a 'wp'"
-  end.
-
-Tactic Notation "wp_if" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | If _ _ _ =>
-      wp_bind_core K;
-      etrans; [|eapply wp_if]; wp_finish
-    end) || fail "wp_if: cannot find 'If' in" e
-  | _ => fail "wp_if: not a 'wp'"
-  end.
-
-Tactic Notation "wp_case" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | Case _ _ _ =>
-      wp_bind_core K;
-      etrans; [|eapply wp_case; wp_done];
-      simpl_subst; wp_finish
-    end) || fail "wp_case: cannot find 'Case' in" e
-  | _ => fail "wp_case: not a 'wp'"
-  end.
-
-Tactic Notation "wp_bind" open_constr(efoc) :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match e' with
-    | efoc => unify e' efoc; wp_bind_core K
-    end) || fail "wp_bind: cannot find" efoc "in" e
-  | _ => fail "wp_bind: not a 'wp'"
-  end.
-
-Section heap.
-Context `{heapG Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types Δ : envs (iResUR Σ).
-
-Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → 0 < n →
-  IntoLaterNEnvs 1 Δ Δ' →
-  (∀ l vl, n = length vl → ∃ Δ'',
-    envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
-      = Some Δ'' ∧
-    (Δ'' ⊢ Φ (LitV $ LitLoc l))) →
-  Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
-Proof.
-  intros ???? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
-  rewrite -always_and_sep_l. apply and_intro; first done.
-  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l;
-  apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
-  apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
-  destruct (HΔ l vl) as (Δ''&?&HΔ'). done.
-  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ' -fupd_intro.
-Qed.
-
-Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → n = length vl →
-  IntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
-  envs_delete i1 false Δ' = Δ'' →
-  envs_lookup i2 Δ'' = Some (false, †l…n')%I →
-  envs_delete i2 false Δ'' = Δ''' →
-  n' = length vl →
-  (Δ''' ⊢ Φ (LitV LitUnit)) →
-  Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
-Proof.
-  intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
-  eapply wand_apply; first exact:wp_free. rewrite -!assoc -always_and_sep_l.
-  apply and_intro; first done.
-  rewrite into_laterN_env_sound -!later_sep; apply later_mono.
-  do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True -fupd_intro.
-Qed.
-
-Lemma tac_wp_read Δ Δ' E i l q v o Φ :
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
-  IntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ Φ v) →
-  Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
-Proof.
-  intros ??[->| ->]???.
-  - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
-    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
-      rewrite -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
-    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
-      rewrite -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
-Qed.
-
-Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
-  to_val e = Some v' →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
-  IntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦ v)%I →
-  envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ Φ (LitV LitUnit)) →
-  Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
-Proof.
-  intros ???[->| ->]????.
-  - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
-    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
-    rewrite right_id -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
-    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
-    rewrite right_id -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
-Qed.
-End heap.
-
-Tactic Notation "wp_apply" open_constr(lem) :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; iApply lem; try iNext; simpl)
-  | _ => fail "wp_apply: not a 'wp'"
-  end.
-
-Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
-    first
-      [reshape_expr e ltac:(fun K e' =>
-         match eval hnf in e' with Alloc _ => wp_bind_core K end)
-      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-    eapply tac_wp_alloc with _ H Hf;
-      [iAssumption || fail "wp_alloc: cannot find heap_ctx"
-      |solve_ndisj
-      |try fast_done
-      |apply _
-      |first [intros l vl ? | fail 1 "wp_alloc:" l "or" vl "not fresh"];
-        eexists; split;
-          [env_cbv; reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
-          |wp_finish]]
-  | _ => fail "wp_alloc: not a 'wp'"
-  end.
-
-Tactic Notation "wp_alloc" ident(l) ident(vl) :=
-  let H := iFresh in let Hf := iFresh in wp_alloc l vl as H Hf.
-
-Tactic Notation "wp_free" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
-    first
-      [reshape_expr e ltac:(fun K e' =>
-         match eval hnf in e' with Free _ _ => wp_bind_core K end)
-      |fail 1 "wp_free: cannot find 'Free' in" e];
-    eapply tac_wp_free;
-      [iAssumption || fail "wp_free: cannot find heap_ctx"
-      |solve_ndisj
-      |try fast_done
-      |apply _
-      |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
-       iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
-      |env_cbv; reflexivity
-      |let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
-       iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
-      |env_cbv; reflexivity
-      |try fast_done
-      |wp_finish]
-  | _ => fail "wp_free: not a 'wp'"
-  end.
-
-Tactic Notation "wp_read" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
-    first
-      [reshape_expr e ltac:(fun K e' =>
-         match eval hnf in e' with Read _ _ => wp_bind_core K end)
-      |fail 1 "wp_read: cannot find 'Read' in" e];
-    eapply tac_wp_read;
-      [iAssumption || fail "wp_read: cannot find heap_ctx"
-      |solve_ndisj
-      |(right; fast_done) || (left; fast_done) ||
-       fail "wp_read: order is neither Na2Ord nor ScOrd"
-      |apply _
-      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-       iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
-      |wp_finish]
-  | _ => fail "wp_read: not a 'wp'"
-  end.
-
-Tactic Notation "wp_write" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
-    first
-      [reshape_expr e ltac:(fun K e' =>
-         match eval hnf in e' with Write _ _ _ => wp_bind_core K end)
-      |fail 1 "wp_write: cannot find 'Write' in" e];
-    eapply tac_wp_write;
-      [let e' := match goal with |- to_val ?e' = _ => e' end in
-       wp_done || fail "wp_write:" e' "not a value"
-      |iAssumption || fail "wp_write: cannot find heap_ctx"
-      |solve_ndisj
-      |(right; fast_done) || (left; fast_done) ||
-       fail "wp_write: order is neither Na2Ord nor ScOrd"
-      |apply _
-      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-       iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
-      |env_cbv; reflexivity
-      |wp_finish]
-  | _ => fail "wp_write: not a 'wp'"
-  end.

theories/lifetime/lifetime.v

-From lrust.lifetime Require Export lifetime_sig.
-From lrust.lifetime.model Require definitions primitive accessors faking borrow
-     reborrow creation.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-
-Module Export lifetime : lifetime_sig.
-  Include definitions.
-  Include primitive.
-  Include borrow.
-  Include faking.
-  Include reborrow.
-  Include accessors.
-  Include creation.
-End lifetime.
-
-Section derived.
-Context `{invG Σ, lftG Σ}.
-Implicit Types κ : lft.
-
-Lemma bor_acc_cons E q κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-    ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
-Proof.
-  iIntros (?) "#LFT HP Htok".
-  iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
-  iIntros "!>*HQ HPQ". iMod ("Hclose" with "HQ [HPQ]") as "[Hb $]".
-  - iNext. iIntros "? _". by iApply "HPQ".
-  - iApply (bor_shorten with "Hκκ' Hb").
-Qed.
-
-Lemma bor_acc E q κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
-Proof.
-  iIntros (?) "#LFT HP Htok".
-  iMod (bor_acc_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
-  iIntros "!>HP". iMod ("Hclose" with "HP []") as "[$ $]"; auto.
-Qed.
-
-Lemma bor_or E κ P Q :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
-Proof.
-  iIntros (?) "#LFT H". rewrite uPred.or_alt.
-  iMod (bor_exists with "LFT H") as ([]) "H"; auto.
-Qed.
-
-Lemma bor_later E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.
-Proof.
-  iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† Hclose]]"; first done.
-  - iDestruct "H" as "[HP  Hclose]". iModIntro. iNext.
-    iApply ("Hclose" with "HP"). by iIntros "!> $".
-  - iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
-Qed.
-
-Lemma bor_later_tok E q κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
-Proof.
-  iIntros (?) "#LFT Hb Htok".
-  iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose]"; first done.
-  iModIntro. iNext. iApply ("Hclose" with "HP []"). by iIntros "!> $".
-Qed.
-
-Lemma bor_persistent P `{!PersistentP P} E κ :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
-Proof.
-  iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic with "LFT Hb") as "[[#HP Hob]|[#H† Hclose]]"; first done.
-  - iMod ("Hob" with "HP") as "_". auto.
-  - iMod "Hclose" as "_". auto.
-Qed.
-
-Lemma bor_persistent_tok P `{!PersistentP P} E κ q :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
-Proof.
-  iIntros (?) "#LFT Hb Htok".
-  iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
-  by iMod ("Hob" with "HP") as "[_ $]".
-Qed.
-
-Lemma lft_incl_static κ : (κ ⊑ static)%I.
-Proof.
-  iApply lft_incl_intro. iIntros "!#". iSplitR.
-  - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
-  - iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
-Qed.
-End derived.

theories/lifetime/model/reborrow.v

-From lrust.lifetime Require Export borrow.
-From lrust.lifetime Require Import raw_reborrow accessors.
-From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-
-Section reborrow.
-Context `{invG Σ, lftG Σ}.
-Implicit Types κ : lft.
-
-(* This lemma has no good place... and reborrowing is where we need it inside the model. *)
-Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
-Proof.
-  iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
-  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
-    iExists x. iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
-  - iExists inhabitant. by iApply (bor_fake with "LFT").
-Qed.
-
-Lemma rebor E κ κ' P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
-Proof.
-  iIntros (?) "#LFT #H⊑". rewrite {1}/bor; iDestruct 1 as (κ'') "[#H⊑' Hκ'']".
-  iMod (raw_rebor _ _ (κ' ∪ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
-  { apply gmultiset_union_subseteq_r. }
-  iModIntro. iSplitL "Hκ''".
-  - rewrite /bor. iExists (κ' ∪ κ''). iFrame "Hκ''".
-    iApply (lft_incl_glb with "[]"); first iApply lft_incl_refl.
-    by iApply (lft_incl_trans with "H⊑").
-  - iIntros "Hκ†". iMod ("Hclose" with "[Hκ†]") as "Hκ''".
-    { iApply lft_dead_or; auto. }
-    iModIntro. rewrite /bor. eauto.
-Qed.
-
-Lemma bor_unnest E κ κ' P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
-Proof.
-  iIntros (?) "#LFT Hκ". rewrite {2}/bor.
-  iMod (bor_exists with "LFT Hκ") as (κ0) "Hκ"; first done.
-  iMod (bor_sep with "LFT Hκ") as "[Hκ⊑ Hκ]"; first done.
-  rewrite {2}/bor; iDestruct "Hκ" as (κ0') "[#Hκ'⊑ Hκ]".
-  iMod (bor_acc_atomic with "LFT Hκ⊑") as "[[#Hκ⊑ Hclose]|[#H† Hclose]]"; first done; last first.
-  { iModIntro. iNext. iMod "Hclose" as "_". iApply (bor_fake with "LFT"); first done.
-    iApply lft_dead_or. iRight. done. }
-  iMod ("Hclose" with "Hκ⊑") as "_".
-  set (κ'' := κ0 ∪ κ0').
-  iMod (raw_rebor _ _ κ'' with "LFT Hκ") as "[Hκ _]"; first done.
-  { apply gmultiset_union_subseteq_r. }
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ'' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
-  clear A I; rename A' into A; rename I' into I.
-  iDestruct (big_sepS_delete _ _ κ'' with "Hinv") as "[Hκ'' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκ''" as "[[Hinv' >%]|[Hdead >Hdeadin]]"; last first.
-  { iDestruct "Hdeadin" as %Hdeadin. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
-    iMod ("Hclose" with "[-]") as "_".
-    { rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
-      iApply (big_sepS_delete _ _ κ''); first by apply elem_of_dom.
-      iNext; iFrame "Hinv". rewrite /lft_inv. iRight. iSplit; auto. }
-    iMod (fupd_intro_mask') as "Hclose"; last iModIntro; first solve_ndisj.
-    iNext. iMod "Hclose" as "_".
-    iApply (bor_fake with "LFT >"); first done.
-    iApply (lft_incl_dead with "[] H†"); first done.
-    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;
-    iDestruct "Hinv'" as (Pb Pi) "(Halive & Hvs & Hinh)".
-  rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(Hbox & >HB● & HB)".
-  iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (slice_delete_full _ _ true with "Hislice Hbox")
-    as (Pb') "(HP & #EQ & Hbox)"; first solve_ndisj.
-  { by rewrite lookup_fmap HB. }
-  iDestruct ("HPP'" with "HP") as "HP".
-  iMod (own_bor_update_2 with "HB● Hi") as "HB●".
-  { apply auth_update_dealloc, delete_singleton_local_update. apply _. }
-  iMod (fupd_intro_mask') as "Hclose'"; last iModIntro; first solve_ndisj.
-  iNext. iMod "Hclose'" as "_".
-  iAssert (lft_bor_alive κ'' Pb') with "[Hbox HB● HB]" as "Halive".
-  { rewrite /lft_bor_alive. iExists (delete i B).
-    rewrite fmap_delete. iFrame "Hbox". iSplitL "HB●".
-    - rewrite /to_borUR fmap_delete. done.
-    - rewrite big_sepM_delete; last done. iDestruct "HB" as "[_ $]". }
-  iMod (raw_bor_unnest' _ false with "[$HI $Hinv] HP Halive [Hvs]") as (Pb'') "([HI Hinv] & HP & Halive & Hvs)";
-    [solve_ndisj|exact: gmultiset_union_subseteq_l|done| |].
-  { (* TODO: Use iRewrite supporting contractive rewriting. *)
-    iApply (lft_vs_cons with "[]"); last done.
-    iIntros "[$ [Hbor HPb']]". iModIntro. iNext. iRewrite "EQ". iFrame. by iApply "HPP'". }
-  iMod ("Hclose" with "[-HP]") as "_".
-  { iNext. simpl. rewrite /lfts_inv. iExists A, I. iFrame.
-    rewrite (big_sepS_delete _ (dom _ I) κ''); last by apply elem_of_dom.
-    iFrame. rewrite /lft_inv lft_inv_alive_unfold. iLeft.
-    iFrame "%". iExists Pb'', Pi. iFrame. }
-  iModIntro. rewrite /bor. iExists κ''. iFrame. subst κ''.
-  by iApply (lft_glb_mono with "Hκ⊑").
-Qed.
-End reborrow.

theories/lifetime/shr_borrow.v

-From iris.algebra Require Import gmap auth frac.
-From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Export lifetime.
-Set Default Proof Using "Type".
-
-(** Shared bors  *)
-Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
-  (∃ i, &{κ,i}P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
-Notation "&shr{ κ } P" := (shr_bor κ P)
-  (format "&shr{ κ }  P", at level 20, right associativity) : uPred_scope.
-
-Section shared_bors.
-  Context `{invG Σ, lftG Σ} (P : iProp Σ).
-
-  Global Instance shr_bor_ne κ n : Proper (dist n ==> dist n) (shr_bor κ).
-  Proof. solve_proper. Qed.
-  Global Instance shr_bor_contractive κ : Contractive (shr_bor κ).
-  Proof. solve_contractive. Qed.
-  Global Instance shr_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
-  Proof. solve_proper. Qed.
-  Lemma shr_bor_iff_proper κ P' : ▷ □ (P ↔ P') -∗ &shr{κ} P -∗ &shr{κ} P'.
-  Proof.
-    iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
-    iApply (idx_bor_iff_proper with "HPP' HP").
-  Qed.
-
-  Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.
-
-  Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
-  Proof.
-    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
-    iExists i. iFrame "#". iApply inv_alloc. auto.
-  Qed.
-
-  Lemma shr_bor_acc E κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
-               [†κ] ∗ |={E∖↑lftN,E}=> True.
-  Proof.
-    iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
-    iInv lftN as (q') ">[Hq'0 Hq'1]" "Hclose".
-    iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
-    iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
-    - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iRight. iFrame. iIntros "!>". by iMod "Hclose".
-  Qed.
-
-  Lemma shr_bor_acc_tok E q κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "#LFT #Hshr Hκ".
-    iMod (shr_bor_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
-    - iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iDestruct (lft_tok_dead with "Hκ H†") as "[]".
-  Qed.
-
-  Lemma shr_bor_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
-  Proof.
-    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-      by iApply (idx_bor_shorten with "H⊑").
-  Qed.
-
-  Lemma shr_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ}P.
-  Proof.
-    iIntros (?) "#LFT#H†". iApply (bor_share with ">"). done.
-    by iApply (bor_fake with "LFT H†").
-  Qed.
-End shared_bors.
-
-Typeclasses Opaque shr_bor.

theories/typing/cont.v

-From iris.base_logic Require Import big_op.
-From iris.proofmode Require Import tactics.
-From lrust.typing Require Export type.
-From lrust.typing Require Import programs.
-Set Default Proof Using "Type".
-
-Section typing.
-  Context `{typeG Σ}.
-
-  (** Jumping to and defining a continuation. *)
-  Lemma type_jump args E L C T k T' :
-    (k ◁cont(L, T'))%CC ∈ C →
-    tctx_incl E L T (T' (list_to_vec args)) →
-    typed_body E L C T (k (of_val <$> args)).
-  Proof.
-    iIntros (HC Hincl) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
-    iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
-    iSpecialize ("HC" with "HE []"); first done.
-    rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "Htl HL HT").
-  Qed.
-
-  Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
-    Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
-    (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) →
-    (∀ k (args : vec val (length argsb)),
-       typed_body E L1 (k ◁cont(L1, T') :: C) (T' args) (subst_v (kb::argsb) (k:::args) econt)) →
-    typed_body E L2 C T (e2 cont: kb argsb := econt).
-  Proof.
-    iIntros (Hc1 Hc2 He2 Hecont) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
-    { simpl. rewrite decide_left. done. }
-    iModIntro. iApply (He2 with "HEAP LFT Htl HE HL [HC] HT"). clear He2.
-    iIntros "HE". iLöb as "IH". iIntros (x) "H".
-    iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE").
-    iIntros (args) "Htl HL HT". iApply wp_rec; try done.
-    { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
-    { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
-    iNext. iApply (Hecont with "HEAP LFT Htl HE HL [HC] HT").
-    by iApply "IH".
-  Qed.
-End typing.

theories/typing/examples/get_x.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section get_x.
-  Context `{typeG Σ}.
-
-  Definition get_x : val :=
-    funrec: <> ["p"] :=
-       let: "p'" := !"p" in
-       letalloc: "r" <- "p'" +ₗ #0 in
-       delete [ #1; "p"] ;; "return" ["r"].
-
-  Lemma get_x_type :
-    typed_instruction_ty [] [] [] get_x
-        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α}Π[int; int]]%T) (λ α, &shr{α} int)%T).
-  Proof.
-    apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>p. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
-      intros p'; simpl_subst.
-    eapply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]=>r. simpl_subst.
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-End get_x.

theories/typing/examples/init_prod.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section init_prod.
-  Context `{typeG Σ}.
-
-  Definition init_prod : val :=
-    funrec: <> ["x"; "y"] :=
-       let: "x'" := !"x" in let: "y'" := !"y" in
-       let: "r" := new [ #2] in
-       "r" +ₗ #0 <- "x'";; "r" +ₗ #1 <- "y'";;
-       delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r"].
-
-  Lemma init_prod_type :
-    typed_instruction_ty [] [] [] init_prod
-        (fn (λ _, []) (λ _, [# int; int]) (λ (_ : ()), Π[int;int])).
-  Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>x y. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>y'. simpl_subst.
-    eapply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
-      intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
-    eapply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|by apply write_own|].
-    eapply type_assign; [solve_typing..|by apply write_own|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-End init_prod.

theories/typing/examples/lazy_lft.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section lazy_lft.
-  Context `{typeG Σ}.
-
-  Definition lazy_lft : val :=
-    funrec: <> [] :=
-      Newlft;;
-      let: "t" := new [ #2] in let: "f" := new [ #1] in let: "g" := new [ #1] in
-      let: "42" := #42 in "f" <- "42";;
-      "t" +ₗ #0 <- "f";; "t" +ₗ #1 <- "f";;
-      let: "t0'" := !("t" +ₗ #0) in "t0'";;
-      let: "23" := #23 in "g" <- "23";;
-      "t" +ₗ #1 <- "g";;
-      let: "r" := new [ #0] in
-      Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; "return" ["r"].
-
-  Lemma lazy_lft_type :
-    typed_instruction_ty [] [] [] lazy_lft
-        (fn (λ _, [])%EL (λ _, [#]) (λ _:(), unit)).
-  Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p. simpl_subst.
-    eapply (type_newlft []); [solve_typing|]=>α.
-    eapply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
-      intros t. simpl_subst.
-    eapply type_new; [solve_typing..|]=>f. simpl_subst.
-    eapply type_new; [solve_typing..|]=>g. simpl_subst.
-    eapply type_int; [solve_typing|]=>v42. simpl_subst.
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply (type_assign _ (&shr{α}_)); [solve_typing..|by eapply write_own|].
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply type_deref; [solve_typing..|apply: read_own_copy|done|]=>t0'. simpl_subst.
-    eapply type_letpath; [solve_typing..|]=>dummy. simpl_subst.
-    eapply type_int; [solve_typing|]=>v23. simpl_subst.
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply (type_assign _ (&shr{α}int)); [solve_typing..|by eapply write_own|].
-    eapply type_new; [solve_typing..|] =>r. simpl_subst.
-    eapply type_endlft; [solve_typing..|].
-    eapply (type_delete (Π[&shr{_}_;&shr{_}_])%T); [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-End lazy_lft.

theories/typing/examples/option_as_mut.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section option_as_mut.
-  Context `{typeG Σ}.
-
-  Definition option_as_mut : val :=
-    funrec: <> ["o"] :=
-      let: "o'" := !"o" in
-      let: "r" := new [ #2 ] in
-      case: !"o'" of
-        [ "r" <-{Σ 0} ();; "k" ["r"];
-          "r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
-      cont: "k" ["r"] :=
-        delete [ #1; "o"];; "return" ["r"].
-
-  Lemma option_as_mut_type τ :
-    typed_instruction_ty [] [] [] option_as_mut
-        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α}Σ[unit; τ]]%T) (λ α, Σ[unit; &uniq{α}τ])%T).
-  Proof.
-    apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>o. simpl_subst.
-    eapply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
-    - intros k. simpl_subst.
-      eapply type_deref; [solve_typing..|apply read_own_move|done|]=>o'. simpl_subst.
-      eapply type_new; [solve_typing..|]. intros r. simpl_subst.
-      eapply type_case_uniq; [solve_typing..|].
-        constructor; last constructor; last constructor; left.
-      + eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
-        eapply (type_jump [_]); solve_typing.
-      + eapply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
-        eapply (type_jump [_]); solve_typing.
-    - move=>/= k r. inv_vec r=>r. simpl_subst.
-      eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
-  Qed.
-End option_as_mut.

theories/typing/examples/rebor.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section rebor.
-  Context `{typeG Σ}.
-
-  Definition rebor : val :=
-    funrec: <> ["t1"; "t2"] :=
-       Newlft;;
-       letalloc: "x" <- "t1" in
-       let: "x'" := !"x" in let: "y" := "x'" +ₗ #0 in
-       "x" <- "t2";;
-       let: "y'" := !"y" in
-       letalloc: "r" <- "y'" in
-       Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
-                 delete [ #1; "x"] ;; "return" ["r"].
-
-  Lemma rebor_type :
-    typed_instruction_ty [] [] [] rebor
-        (fn (λ _, []) (λ _, [# Π[int; int]; Π[int; int]]) (λ (_ : ()), int)).
-  Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
-    eapply (type_newlft []). apply _. move=> α.
-    eapply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
-    eapply (type_letpath (&uniq{α}int)); [solve_typing..|]=>y. simpl_subst.
-    eapply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing..|by apply write_own|].
-    eapply type_deref; [solve_typing..|apply: read_uniq; solve_typing|done|]=>y'. simpl_subst.
-    eapply type_letalloc_1; [solve_typing..|]=>r. simpl_subst.
-    eapply type_endlft; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-End rebor.

theories/typing/examples/unbox.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section unbox.
-  Context `{typeG Σ}.
-
-  Definition unbox : val :=
-    funrec: <> ["b"] :=
-       let: "b'" := !"b" in let: "bx" := !"b'" in
-       letalloc: "r" <- "bx" +ₗ #0 in
-       delete [ #1; "b"] ;; "return" ["r"].
-
-  Lemma ubox_type :
-    typed_instruction_ty [] [] [] unbox
-        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α}box (Π[int; int])]%T) (λ α, &uniq{α} int)%T).
-  Proof.
-    apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
-    intros b'; simpl_subst.
-    eapply type_deref_uniq_own; [solve_typing..|]=>bx; simpl_subst.
-    eapply type_letalloc_1; [solve_typing..|]=>r. simpl_subst.
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
-  Qed.
-End unbox.

theories/typing/examples/unwrap_or.v

-From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
-
-Section unwrap_or.
-  Context `{typeG Σ}.
-
-  Definition unwrap_or τ : val :=
-    funrec: <> ["o"; "def"] :=
-      case: !"o" of
-      [ delete [ #(S τ.(ty_size)); "o"];; "return" ["def"];
-        letalloc: "r" <-{τ.(ty_size)} !("o" +ₗ #1) in
-        delete [ #(S τ.(ty_size)); "o"];; delete [ #τ.(ty_size); "def"];; "return" ["r"]].
-
-  Lemma unwrap_or_type τ :
-    typed_instruction_ty [] [] [] (unwrap_or τ)
-        (fn (λ _, [])%EL (λ _, [# Σ[unit; τ]; τ])%T (λ _:(), τ)).
-  Proof.
-    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>o def. simpl_subst.
-    eapply type_case_own; [solve_typing..|]. constructor; last constructor; last constructor.
-    + right. eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
-    + left. eapply type_letalloc_n; [solve_typing..|by apply read_own_move|solve_typing|]=>r.
-        simpl_subst.
-      eapply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
-      eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
-  Qed.
-End unwrap_or.