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,113 +327,173 @@ 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_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
+Lemma lft_incl_acc E κ κ' q :
+  ↑lftN ⊆ E →
+  κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+Proof.
+  rewrite /lft_incl.
+  iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
+  iMod ("H" with "Hq") as (q') "[Hq' Hclose]". iExists q'.
+  iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
+Qed.
+
+Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
+Proof.
+  rewrite /lft_incl.
+  iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
+Qed.
+
+Lemma lft_incl_intro κ κ' :
+  □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+      ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
+Proof. iIntros "?". done. Qed.
+
+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']".
+    iMod ("H1" with "Hκ") as (q') "[Hκ' Hclose]".
+    iMod ("H2" with "Hκ'") as (q'') "[Hκ'' Hclose']".
     iExists q''. iIntros "{$Hκ''} !> Hκ''".
     iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
   - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
 Qed.
 
-Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+Lemma lft_intersect_acc κ κ' q q' :
+  q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
 Proof.
-  rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
+  iIntros "Hκ Hκ'".
+  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 κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
+Proof.
+  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'']".
-    destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
-    iExists qq. rewrite -lft_tok_sep.
-    iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
-    iIntros "!> [Hκ'0 Hκ''0]".
-    iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
-    iApply "Hclose''". iFrame.
-  - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
+    iMod ("H1" with "Hκ'1") as (q') "[Hκ' Hclose']".
+    iMod ("H2" with "Hκ'2") as (q'') "[Hκ'' 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†".
 Qed.
 
-Lemma lft_incl_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.
 
-Lemma lft_incl_acc E κ κ' q :
-  ↑lftN ⊆ E →
-  κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+(** Basic rules about borrows *)
+Lemma raw_bor_iff i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'.
 Proof.
-  rewrite /lft_incl.
-  iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
-  iMod ("H" with "* Hq") as (q') "[Hq' Hclose]". iExists q'.
-  iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
+  iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
+  iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
+  iNext. iModIntro. iSplit; iIntros.
+  - by iApply "HPP'"; iApply "Hiff".
+  - by iApply "Hiff"; iApply "HPP'".
 Qed.
 
-Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
+Lemma idx_bor_iff κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 Proof.
-  rewrite /lft_incl.
-  iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
+  unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
+  iExists P0. iFrame. iNext. iModIntro. iSplit; iIntros.
+  - by iApply "HPP'"; iApply "HP0P".
+  - by iApply "HP0P"; iApply "HPP'".
 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.
-
-(** Basic rules about borrows *)
 Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
 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 κ 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 with "HPP'").
 Qed.
 
 Lemma bor_shorten κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
@@ -418,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.
 
@@ -447,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 *)
@@ -459,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,19 +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. by iFrame. }
+  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.
@@ -72,124 +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]".
-  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. by iFrame. }
-  iExists Pb'. iModIntro. iFrame. iNext. by iApply "Hclose".
+  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]".
-  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κ] & $ & Halive & Hvs)"; [solve_ndisj|done|done|..].
-  { iNext. by iApply lft_vs_frame. }
-  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. by iFrame.
+  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 κ tid N n :
-    Proper (dist n ==> dist n) (na_bor κ tid N).
+  Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
   Proof. solve_proper. Qed.
-  Global Instance na_bor_contractive κ tid N : Contractive (na_bor κ tid N).
+  Global Instance na_bor_contractive κ : Contractive (na_bor κ tid N).
   Proof. solve_contractive. Qed.
-  Global Instance na_bor_proper κ tid N :
-    Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
+  Global Instance na_bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
   Proof. solve_proper. Qed.
-  Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} 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 with "HPP' HP").
+  Qed.
+
+  Global Instance na_bor_persistent κ : Persistent (&na{κ,tid,N} P) := _.
 
   Lemma bor_na κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &na{κ,tid,N}P.
   Proof.
@@ -38,24 +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 9fa0b57d44cbba40d7bb272b45cc0875bc68940d

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 e' el Φ :
-  Forall (λ ei, is_Some (to_val ei)) el →
-  Closed (xl +b+ []) e →
-  subst_l xl el e = Some e' →
-  ▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl 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 -∗ ▷ |={E}=> Φ (LitV true)) →
-  (n2 < n1 → P -∗ ▷ |={E}=> Φ (LitV false)) →
-  P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  iIntros (Hl Hg) "HP". iApply wp_fupd.
-  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_offset E l z Φ :
-  ▷ (|={E}=> Φ (LitV $ LitLoc $ shift_loc l z)) -∗
-    WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
-  iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-Lemma wp_plus E z1 z2 Φ :
-  ▷ (|={E}=> Φ (LitV $ LitInt $ z1 + z2)) -∗
-    WP BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
-  iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-Lemma wp_minus E z1 z2 Φ :
-  ▷ (|={E}=> Φ (LitV $ LitInt $ z1 - z2)) -∗
-    WP BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_fupd. 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 → (* to avoids recursive calls being unfolded *)
-  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.proofmode Require Import coq_tactics.
-From iris.proofmode Require Export tactics.
-From iris.base_logic Require Import namespaces.
-From lrust.lang Require Export wp_tactics heap.
-Set Default Proof Using "Type".
-Import uPred.
-
-Ltac wp_strip_later ::= iNext.
-
-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 Δ'' ∧
-    (Δ'' ⊢ |={E}=> Φ (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Δ'.
-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 →
-  (Δ''' ⊢ |={E}=> Φ (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.
-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 →
-  (Δ' ⊢ |={E}=> Φ 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.
-      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.
-      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 Δ'' →
-  (Δ'' ⊢ |={E}=> Φ (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. 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. by apply later_mono, sep_mono_r, wand_mono.
-Qed.
-End heap.
-
-Tactic Notation "wp_apply" open_constr(lem) :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; iApply lem; try iNext)
-  | _ => fail "wp_apply: not a 'wp'"
-  end.
-
-Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
-  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" :=
-  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" :=
-  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" :=
-  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/lang/wp_tactics.v

-From lrust.lang Require Export tactics derived.
-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.
-
-(* FIXME : the [reflexivity] tactic is not able to solve trivial
-   reflexivity proofs, while [exact (reflexivity _)] does. *)
-Ltac wp_done :=
-  rewrite /= ?to_of_val;
-  match goal with
-  | |- _ = _ => exact (reflexivity _)
-  | |- Forall _ [] => fast_by apply List.Forall_nil
-  | |- Forall _ (_ :: _) => apply List.Forall_cons; wp_done
-  | |- is_Some (Some ?v) => exists v; reflexivity
-  | |- _ => fast_done
-  end.
-
-(* sometimes, we will have to do a final view shift, so only apply
-pvs_intro if we obtain a consecutive wp *)
-Ltac wp_strip_pvs :=
-  lazymatch goal with
-  | |- _ ⊢ |={?E}=> _ =>
-    etrans; [|apply fupd_intro];
-    match goal with |- _ ⊢ wp E _ _ => simpl | _ => fail end
-  end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value_fupd; wp_done]; lazy beta.
-
-Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
-
-Ltac wp_seq_head :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-    etrans; [|eapply wp_seq; wp_done]; wp_strip_later
-  end.
-
-Ltac wp_finish := intros_revert ltac:(
-  rewrite /= ?to_of_val;
-  try wp_strip_later;
-  repeat lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-     etrans; [|eapply wp_seq; wp_done]; wp_strip_later
-  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
-  | |- _ ⊢ |={_}=> _ => wp_strip_pvs
-  end).
-
-Tactic Notation "wp_value" :=
-  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.
-
-Tactic Notation "wp_rec" :=
-  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; 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" :=
-  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; 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" :=
-  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 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" :=
-  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" :=
-  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) :=
-  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.

theories/lifetime/frac_borrow.v

-From Coq Require Import Qcanon.
-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import lib.fractional.
-From iris.algebra Require Import frac.
-From lrust.lifetime Require Export shr_borrow.
-Set Default Proof Using "Type".
-
-Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
-
-Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (Φ : Qp → iProp Σ) :=
-  (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
-                       (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
-Notation "&frac{ κ } P" := (frac_bor κ P)
-  (format "&frac{ κ }  P", at level 20, right associativity) : uPred_scope.
-
-Section frac_bor.
-  Context `{invG Σ, lftG Σ, frac_borG Σ}.
-  Implicit Types E : coPset.
-
-  Global Instance frac_bor_contractive κ n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist n) (frac_bor κ).
-  Proof. solve_contractive. Qed.
-  Global Instance frac_bor_ne κ n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (frac_bor κ).
-  Proof. solve_proper. Qed.
-  Global Instance frac_bor_proper κ :
-    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_bor κ).
-  Proof. solve_proper. Qed.
-  Global Instance frac_bor_persistent κ : PersistentP (&frac{κ}Φ) := _.
-
-  Lemma bor_fracture φ E κ :
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
-  Proof.
-    iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
-    iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|[H† Hclose]]". done.
-    - iDestruct "H" as (κ') "(#Hκκ' & Hφ & Hclose)".
-      iMod ("Hclose" with "*[-] []") as "Hφ"; last first.
-      { iExists γ, κ'. iFrame "#". iApply (bor_share with "Hφ"). done. }
-      { iIntros "!>HΦ H†!>". iNext. iDestruct "HΦ" as (q') "(HΦ & _ & [%|Hκ])". by subst.
-        iDestruct "Hκ" as (q'') "[_ Hκ]".
-        iDestruct (lft_tok_dead with "Hκ H†") as "[]". }
-      iExists 1%Qp. iFrame. eauto.
-    - iMod ("Hclose" with "*") as "_"; last first.
-      iExists γ, κ. iSplitR. by iApply lft_incl_refl.
-      iMod (bor_fake with "LFT H†"). done. by iApply bor_share.
-  Qed.
-
-  Lemma frac_bor_atomic_acc E κ φ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
-                                      ∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
-  Proof.
-    iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
-    iMod (shr_bor_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
-    - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
-      iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
-    - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
-      iApply fupd_intro_mask. set_solver. done.
-  Qed.
-
-  Lemma frac_bor_acc' E q κ Φ:
-    ↑lftN ⊆ E →
-    lft_ctx -∗ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
-    &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "#LFT #HΦ Hfrac Hκ". unfold frac_bor.
-    iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
-    iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
-    iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
-    iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & Hq)".
-    destruct (Qp_lower_bound (qκ'/2) (qΦ/2)) as (qq & qκ'0 & qΦ0 & Hqκ' & HqΦ).
-    iExists qq.
-    iAssert (▷ Φ qq ∗ ▷ Φ (qΦ0 + qΦ / 2))%Qp%I with "[HΦqΦ]" as "[$ HqΦ]".
-    { iNext. rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ. iApply "HΦ". by rewrite assoc. }
-    rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ -assoc {1}Hqκ'.
-    iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
-    iMod ("Hclose'" with "[HqΦ Hq Hown Hκq]") as "Hκ1".
-    { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
-      - subst. iExists qq. iIntros "{$Hκq}!%".
-        by rewrite (comm _ qΦ0) -assoc (comm _ qΦ0) -HqΦ Qp_div_2.
-      - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
-        iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -HqΦ Qp_div_2. }
-    clear HqΦ qΦ qΦ0. iIntros "!>HqΦ".
-    iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
-    iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & >[%|Hq])".
-    { subst. iCombine "Hown" "Hownq" as "Hown".
-      by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
-    iDestruct "Hq" as (q') "[HqΦq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
-    iDestruct (own_valid with "Hown") as %Hval. iDestruct "HqΦq'" as %HqΦq'.
-    assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
-    { change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
-      rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
-      destruct Hval as [Hval|Hval].
-      by left; apply ->Qclt_minus_iff. right; apply Qp_eq, Qc_is_canon. by rewrite Hval. }
-    - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
-      iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
-      iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
-      { iNext. iExists (qΦ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "HΦ"; iFrame.
-        iRight. iExists _. iIntros "{$Hq'qκ}!%".
-        revert HqΦq'. rewrite !Qp_eq. move=>/=<-. ring. }
-      iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
-    - iMod ("Hclose'" with "[HqΦ HΦqΦ Hown]") as "Hqκ2".
-      { iNext. iExists (qΦ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "HΦ"; iFrame. auto. }
-      iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
-  Qed.
-
-  Lemma frac_bor_acc E q κ `{Fractional _ Φ} :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "LFT". iApply (frac_bor_acc' with "LFT"). done.
-    iIntros "!#*". rewrite fractional. iSplit; auto.
-  Qed.
-
-  Lemma frac_bor_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
-  Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[#H⊑ ?]". iExists γ, κ0. iFrame.
-    iApply (lft_incl_trans with "Hκκ' []"). auto.
-  Qed.
-
-  Lemma frac_bor_fake E κ Φ:
-    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &frac{κ}Φ.
-  Proof.
-    iIntros (?) "#LFT#H†". iApply (bor_fracture with "LFT >"). done.
-    by iApply (bor_fake with "LFT").
-  Qed.
-
-  Lemma frac_bor_lft_incl κ κ' q:
-    lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
-  Proof.
-    iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
-    - iIntros (q') "Hκ'".
-      iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
-      iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
-    - iIntros "H†'".
-      iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
-      iDestruct "H" as (q') "[>Hκ' _]".
-      iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
-  Qed.
-End frac_bor.
-
-Typeclasses Opaque frac_bor.

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_iff (P Q : iProp Σ) E κ :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ ▷ □ (P ↔ Q) -∗ &{κ}P ={E}=∗ &{κ}Q.
-Proof.
-  iIntros (?) "#LFT #Heq Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[[HP Hclose]|[H† Hclose]]". done.
-  - iApply ("Hclose" with "[HP] []").
-      by iApply "Heq". by iIntros "!>HQ!>"; iApply "Heq".
-  - iMod "Hclose". by iApply (bor_fake with "LFT").
-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_incl_mono with "Hκ⊑"). }
-  rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #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. }
-  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]". iModIntro. iNext. by iRewrite "EQ". }
-  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_incl_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.
-  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/fixpoint.v

-From lrust.lang Require Import proofmode.
-From lrust.typing Require Export lft_contexts type bool.
-Set Default Proof Using "Type".
-
-Section fixpoint.
-  Context `{typeG Σ}.
-
-  Global Instance type_inhabited : Inhabited type := populate bool.
-
-  Context (T : type → type) `{Contractive T}.
-
-  Global Instance fixpoint_copy :
-    (∀ `(!Copy ty), Copy (T ty)) → Copy (fixpoint T).
-  Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ??[[EQsz%leibniz_equiv EQown]EQshr].
-      specialize (λ tid vl, EQown tid vl). specialize (λ κ tid l, EQshr κ tid l).
-      simpl in *=>-[Hp Hsh]; (split; [intros ??|intros ???]).
-      + revert Hp. by rewrite /PersistentP -EQown.
-      + intros F l q. rewrite -EQsz -EQshr. setoid_rewrite <-EQown. auto.
-    - exists bool. apply _.
-    - done.
-    - intros c Hc. split.
-      + intros tid vl. apply uPred.equiv_entails, equiv_dist=>n.
-        by rewrite conv_compl uPred.always_always.
-      + intros κ tid E F l q ? ?.
-        apply uPred.entails_equiv_and, equiv_dist=>n. etrans.
-        { apply equiv_dist, uPred.entails_equiv_and, (copy_shr_acc κ tid E F)=>//.
-            by rewrite -conv_compl. }
-        symmetry.               (* FIXME : this is too slow *)
-        do 2 f_equiv; first by rewrite conv_compl. set (cn:=c n).
-        repeat (apply (conv_compl n c) || f_contractive || f_equiv);
-          by rewrite conv_compl.
-  Qed.
-
-  Global Instance fixpoint_send :
-    (∀ `(!Send ty), Send (T ty)) → Send (fixpoint T).
-  Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ?? EQ ????. by rewrite -EQ.
-    - exists bool. apply _.
-    - done.
-    - intros c Hc ???. apply uPred.entails_equiv_and, equiv_dist=>n.
-      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
-  Qed.
-
-  Global Instance fixpoint_sync :
-    (∀ `(!Sync ty), Sync (T ty)) → Sync (fixpoint T).
-  Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ?? EQ ?????. by rewrite -EQ.
-    - exists bool. apply _.
-    - done.
-    - intros c Hc ????. apply uPred.entails_equiv_and, equiv_dist=>n.
-      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
-  Qed.
-
-  Lemma fixpoint_unfold_eqtype E L : eqtype E L (fixpoint T) (T (fixpoint T)).
-  Proof.
-    unfold eqtype, subtype, type_incl. setoid_rewrite <-fixpoint_unfold.
-    split; iIntros "_ _ _"; (iSplit; first done); iSplit; iIntros "!#*$".
-  Qed.
-End fixpoint.
-
-Section subtyping.
-  Context `{typeG Σ} (E : elctx) (L : llctx).
-
-  (* TODO : is there a way to declare these as a [Proper] instances ? *)
-  Lemma fixpoint_mono T1 `{Contractive T1} T2 `{Contractive T2} :
-    (∀ ty1 ty2, subtype E L ty1 ty2 → subtype E L (T1 ty1) (T2 ty2)) →
-    subtype E L (fixpoint T1) (fixpoint T2).
-  Proof.
-    intros H12. apply fixpoint_ind.
-    - intros ?? EQ ?. etrans; last done. by apply equiv_subtype.
-    - by eexists _.
-    - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc.
-      assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)⌝).
-      { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
-      assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ tid vl, (compl c).(ty_own) tid vl -∗ (fixpoint T2).(ty_own) tid vl)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
-        iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
-      assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ κ tid l,
-                   (compl c).(ty_shr) κ tid l -∗ (fixpoint T2).(ty_shr) κ tid l)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
-        iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
-      iIntros "LFT HE HL". iSplit; [|iSplit].
-      + iApply (Hsz with "LFT HE HL").
-      + iApply (Hown with "LFT HE HL").
-      + iApply (Hshr with "LFT HE HL").
-  Qed.
-
-  Lemma fixpoint_proper T1 `{Contractive T1} T2 `{Contractive T2} :
-    (∀ ty1 ty2, eqtype E L ty1 ty2 → eqtype E L (T1 ty1) (T2 ty2)) →
-    eqtype E L (fixpoint T1) (fixpoint T2).
-  Proof.
-    intros H12. apply fixpoint_ind.
-    - intros ?? EQ ?. etrans; last done. by apply equiv_eqtype.
-    - by eexists _.
-    - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc. setoid_rewrite eqtype_unfold in Hc. rewrite eqtype_unfold.
-      assert (Hsz : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)⌝).
-      { iIntros "LFT HE HL". iDestruct (Hc 0%nat with "LFT HE HL") as "[$ _]". }
-      assert (Hown : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ tid vl, (compl c).(ty_own) tid vl ↔ (fixpoint T2).(ty_own) tid vl)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl (S n) c) as [[_ Heq] _]. setoid_rewrite (λ tid vl, Heq tid vl).
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
-        iDestruct (Hc (S n) with "LFT HE HL") as "[_ [$ _]]". }
-      assert (Hshr : lft_ctx -∗ lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ κ tid l,
-                   (compl c).(ty_shr) κ tid l ↔ (fixpoint T2).(ty_shr) κ tid l)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl n c) as [_ Heq]. setoid_rewrite (λ κ tid l, Heq κ tid l).
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "LFT HE HL".
-        iDestruct (Hc n with "LFT HE HL") as "[_ [_ $]]". }
-      iIntros "LFT HE HL". iSplit; [|iSplit].
-      + iApply (Hsz with "LFT HE HL").
-      + iApply (Hown with "LFT HE HL").
-      + iApply (Hshr with "LFT HE HL").
-  Qed.
-
-  Lemma fixpoint_unfold_subtype_l ty T `{Contractive T} :
-    subtype E L ty (T (fixpoint T)) → subtype E L ty (fixpoint T).
-  Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_subtype_r ty T `{Contractive T} :
-    subtype E L (T (fixpoint T)) ty → subtype E L (fixpoint T) ty.
-  Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_l ty T `{Contractive T} :
-    eqtype E L ty (T (fixpoint T)) → eqtype E L ty (fixpoint T).
-  Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_r ty T `{Contractive T} :
-    eqtype E L (T (fixpoint T)) ty → eqtype E L (fixpoint T) ty.
-  Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-End subtyping.
-
-Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
-
-(* These hints can loop if [fixpoint_mono] and [fixpoint_proper] have
-   not been tried before, so we give them a high cost *)
-Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.

theories/typing/function.v

-From iris.base_logic Require Import big_op.
-From iris.proofmode Require Import tactics.
-From iris.algebra Require Import vector.
-From lrust.typing Require Export type.
-From lrust.typing Require Import programs cont.
-Set Default Proof Using "Type".
-
-Section fn.
-  Context `{typeG Σ} {A : Type} {n : nat}.
-
-  Program Definition fn (E : A → elctx)
-          (tys : A → vec type n) (ty : A → type) : type :=
-    {| st_own tid vl := (∃ fb kb xb e H,
-         ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
-         ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
-            typed_body (E x) []
-                       [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
-                       (zip_with (TCtx_hasty ∘ of_val) xl (tys x))
-                       (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
-  Next Obligation.
-    iIntros (E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
-  Qed.
-
-  Global Instance fn_send E tys ty : Send (fn E tys ty).
-  Proof. iIntros (tid1 tid2 vl). done. Qed.
-
-  Global Instance fn_contractive n' E :
-    Proper (pointwise_relation A (dist_later n') ==>
-            pointwise_relation A (dist_later n') ==> dist n') (fn E).
-  Proof.
-    intros ?? Htys ?? Hty. unfold fn. f_equiv. rewrite st_dist_unfold /=.
-    f_contractive=>tid vl. unfold typed_body.
-    do 12 f_equiv. f_contractive. do 18 f_equiv.
-    - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
-      rewrite !tctx_interp_singleton /tctx_elt_interp. do 3 f_equiv. apply Hty.
-    - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
-      assert (Hprop : ∀ n tid p i, Proper (dist (S n) ==> dist n)
-        (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I);
-        last by apply Hprop, Htys.
-      clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
-      specialize (Hxy i). destruct (x !! i) as [tyx|], (y !! i) as [tyy|];
-        inversion_clear Hxy; last done.
-      transitivity (tctx_elt_interp tid (p ◁ tyx));
-        last transitivity (tctx_elt_interp tid (p ◁ tyy)); last 2 first.
-      + unfold tctx_elt_interp. do 3 f_equiv. by apply ty_own_ne.
-      + apply equiv_dist. iSplit.
-        * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
-        * iIntros "H". by iApply "H".
-      + apply equiv_dist. iSplit.
-        * iIntros "H". by iApply "H".
-        * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
-  Qed.
-
-  Global Instance fn_ne n' E :
-    Proper (pointwise_relation A (dist n') ==>
-            pointwise_relation A (dist n') ==> dist n') (fn E).
-  Proof.
-    intros ?? H1 ?? H2.
-    apply fn_contractive=>u; (destruct n'; [done|apply dist_S]);
-      [apply (H1 u)|apply (H2 u)].
-  Qed.
-End fn.
-
-Section typing.
-  Context `{typeG Σ}.
-
-  Lemma fn_subtype_full {A n} E0 L0 E E' (tys tys' : A → vec type n) ty ty' :
-    (∀ x, elctx_incl E0 L0 (E x) (E' x)) →
-    (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys' x) (tys x)) →
-    (∀ x, subtype (E0 ++ E x) L0 (ty x) (ty' x)) →
-    subtype E0 L0 (fn E' tys ty) (fn E tys' ty').
-  Proof.
-    intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
-    iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
-    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
-    rewrite /typed_body. iIntros "* !# * #HEAP _ Htl HE HL HC HT".
-    iDestruct (elctx_interp_persist with "HE") as "#HEp".
-    iMod (HE with "HE0 HL0 * HE") as (qE') "[HE' Hclose]". done.
-    iApply ("Hf" with "* HEAP LFT Htl HE' HL [HC Hclose] [HT]").
-    - iIntros "HE'". unfold cctx_interp. iIntros (elt) "Helt".
-      iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
-      iMod ("Hclose" with "HE'") as "HE".
-      iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
-      iApply ("HC" $! (_ ◁cont(_, _)%CC) with "[%] * Htl HL >").
-      { by apply elem_of_list_singleton. }
-      rewrite /tctx_interp !big_sepL_singleton /=.
-      iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
-      iDestruct (Hty x with "LFT [HE0 HEp] HL0") as "(_ & #Hty & _)".
-      { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
-      by iApply "Hty".
-    - rewrite /tctx_interp
-         -(fst_zip (tys x) (tys' x)) ?vec_to_list_length //
-         -{1}(snd_zip (tys x) (tys' x)) ?vec_to_list_length //
-         !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
-      iApply big_sepL_impl. iSplit; last done. iIntros "{HT}!#".
-      iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
-      iDestruct "H" as (v) "[? Hown]". iExists v. iFrame.
-      rewrite !lookup_zip_with.
-      iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
-        (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
-      specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
-      iDestruct (Htys with "* [] [] []") as "(_ & #Ho & _)"; [done| |done|].
-      + rewrite /elctx_interp_0 big_sepL_app. by iSplit.
-      + by iApply "Ho".
-  Qed.
-
-  Lemma fn_subtype_ty {A n} E0 L0 E (tys1 tys2 : A → vec type n) ty1 ty2 :
-    (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x) (tys1 x)) →
-    (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
-    subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
-  Proof. intros. by apply fn_subtype_full. Qed.
-
-  (* This proper and the next can probably not be inferred, but oh well. *)
-  Global Instance fn_subtype_ty' {A n} E0 L0 E :
-    Proper (flip (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (subtype E0 L0) v1 v2)) ==>
-            pointwise_relation A (subtype E0 L0) ==> subtype E0 L0) (fn E).
-  Proof.
-    intros tys1 tys2 Htys ty1 ty2 Hty. apply fn_subtype_ty.
-    - intros. eapply Forall2_impl; first eapply Htys. intros ??.
-      eapply subtype_weaken; last done. by apply submseteq_inserts_r.
-    - intros. eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
-  Qed.
-
-  Global Instance fn_eqtype_ty' {A n} E0 L0 E :
-    Proper (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (eqtype E0 L0) v1 v2) ==>
-            pointwise_relation A (eqtype E0 L0) ==> eqtype E0 L0) (fn E).
-  Proof.
-    intros tys1 tys2 Htys ty1 ty2 Hty. split; eapply fn_subtype_ty'; try (by intro; apply Hty);
-      intros x; (apply Forall2_flip + idtac); (eapply Forall2_impl; first by eapply (Htys x)); by intros ??[].
-  Qed.
-
-  Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
-    (∀ x, elctx_sat (E x) [] (E' x)) →
-    subtype E0 L0 (fn E' tys ty) (fn E tys ty).
-  Proof.
-    intros. apply fn_subtype_full; try done. by intros; apply elctx_sat_incl.
-  Qed.
-
-  Lemma fn_subtype_lft_incl {A n} E0 L0 E κ κ' (tys : A → vec type n) ty :
-    lctx_lft_incl E0 L0 κ κ' →
-    subtype E0 L0 (fn (λ x, (κ ⊑ κ') :: E x)%EL tys ty) (fn E tys ty).
-  Proof.
-    intros Hκκ'. apply fn_subtype_full; try done. intros.
-    apply elctx_incl_lft_incl; last by apply elctx_incl_refl.
-    iIntros "#HE #HL". iApply (Hκκ' with "[HE] HL").
-    rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[$ _]".
-  Qed.
-
-  Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :
-    subtype E0 L0 (fn (n:=n) E tys ty) (fn (E ∘ σ) (tys ∘ σ) (ty ∘ σ)).
-  Proof.
-    apply subtype_simple_type=>//= _ vl.
-    iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
-    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
-    rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
-  Qed.
-
-  Lemma type_call' {A} E L E' T p (ps : list path)
-                         (tys : A → vec type (length ps)) ty k x :
-    elctx_sat E L (E' x) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ ty x) :: T)]
-               ((p ◁ fn E' tys ty) :: zip_with TCtx_hasty ps (tys x) ++ T)
-               (call: p ps → k).
-  Proof.
-    iIntros (HE) "!# * #HEAP #LFT Htl HE HL HC".
-    rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
-    wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
-    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
-               vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ ty)) (tys x))%I
-            with "* [Hargs]"); first wp_done.
-    - rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
-      clear dependent ty k p.
-      rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
-              (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
-      iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
-      iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $".
-    - simpl. change (@length expr ps) with (length ps).
-      iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons.
-      iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
-      iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl tys.
-      rewrite <-EQl=>vl tys. iApply wp_rec; try done.
-      { rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
-      { rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::k:::vl)) //. }
-      iNext. iSpecialize ("Hf" $! x k vl).
-      iMod (HE with "HE HL") as (q') "[HE' Hclose]"; first done.
-      iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT]").
-      + by rewrite /llctx_interp big_sepL_nil.
-      + iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
-        iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
-        iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ Hret".
-        iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
-        iApply ("HC" $! args with "Htl HL").
-        rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
-      + rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
-                (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
-        iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
-  Qed.
-
-  Lemma type_call {A} x E L E' C T T' T'' p (ps : list path)
-                        (tys : A → vec type (length ps)) ty k :
-    (p ◁ fn E' tys ty)%TC ∈ T →
-    elctx_sat E L (E' x) →
-    tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
-    (k ◁cont(L, T''))%CC ∈ C →
-    (∀ ret : val, tctx_incl E L ((ret ◁ ty x)::T') (T'' [# ret])) →
-    typed_body E L C T (call: p ps → k).
-  Proof.
-    intros Hfn HE HTT' HC HT'T''.
-    rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
-    - etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
-      apply cctx_incl_cons_match; first done. intros args. by inv_vec args.
-    - etrans; last by apply (tctx_incl_frame_l [_]).
-      apply copy_elem_of_tctx_incl; last done. apply _.
-  Qed.
-
-  Lemma type_letcall {A} x E L E' C T T' p (ps : list path)
-                        (tys : A → vec type (length ps)) ty b e :
-    Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
-    (p ◁ fn E' tys ty)%TC ∈ T →
-    elctx_sat E L (E' x) →
-    tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
-    (∀ ret : val, typed_body E L C ((ret ◁ ty x)::T') (subst' b ret e)) →
-    typed_body E L C T (letcall: b := p ps in e).
-  Proof.
-    intros ?? Hpsc ????. eapply (type_cont [_] _ (λ r, (r!!!0 ◁ ty x) :: T')%TC).
-    - (* TODO : make [solve_closed] work here. *)
-      eapply is_closed_weaken; first done. set_solver+.
-    - (* TODO : make [solve_closed] work here. *)
-      rewrite /Closed /= !andb_True. split.
-      + by eapply is_closed_weaken, list_subseteq_nil.
-      + eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
-        intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
-    - intros.
-      (* TODO : make [simpl_subst] work here. *)
-      change (subst' "_k" k (p (Var "_k" :: ps))) with
-             ((subst "_k" k p) (of_val k :: map (subst "_k" k) ps)).
-      rewrite is_closed_nil_subst //.
-      assert (map (subst "_k" k) ps = ps) as ->.
-      { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
-      eapply type_call; try done. constructor. done.
-    - move=>/= k ret. inv_vec ret=>ret. rewrite /subst_v /=.
-      rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
-      apply subst'_is_closed; last done. apply is_closed_of_val.
-  Qed.
-
-  Lemma type_rec {A} E L E' fb (argsb : list binder) e
-        (tys : A → vec type (length argsb)) ty
-        T `{!CopyC T, !SendC T} :
-    Closed (fb :b: "return" :b: argsb +b+ []) e →
-    (∀ x (f : val) k (args : vec val (length argsb)),
-        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
-                   ((f ◁ fn E' tys ty) ::
-                      zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
-                   (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) →
-    typed_instruction_ty E L T (funrec: fb argsb := e) (fn E' tys ty).
-  Proof.
-    iIntros (Hc Hbody) "!# * #HEAP #LFT $ $ $ #HT". iApply wp_value.
-    { simpl. rewrite ->(decide_left Hc). done. }
-    rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
-    { simpl. rewrite decide_left. done. }
-    iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE.
-    iIntros (x k args) "!#". iIntros (tid' qE) "_ _ Htl HE HL HC HT'".
-    iApply (Hbody with "* HEAP LFT Htl HE HL HC").
-    rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
-    by iApply sendc_change_tid.
-  Qed.
-
-  Lemma type_fn {A} E L E' (argsb : list binder) e
-        (tys : A → vec type (length argsb)) ty
-        T `{!CopyC T, !SendC T} :
-    Closed ("return" :b: argsb +b+ []) e →
-    (∀ x k (args : vec val (length argsb)),
-        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
-                   (zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
-                   (subst_v (BNamed "return" :: argsb) (k ::: args) e)) →
-    typed_instruction_ty E L T (funrec: <> argsb := e) (fn E' tys ty).
-  Proof.
-    intros. apply type_rec; try done. intros. rewrite -typed_body_mono //=.
-    eapply contains_tctx_incl. by constructor.
-  Qed.
-End typing.
-
-Hint Resolve fn_subtype_full : lrust_typing.

theories/typing/lft_contexts.v

-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import fractional.
-From lrust.lifetime Require Import frac_borrow.
-Set Default Proof Using "Type".
-
-Inductive elctx_elt : Type :=
-| ELCtx_Alive (κ : lft)
-| ELCtx_Incl (κ κ' : lft).
-Notation elctx := (list elctx_elt).
-
-Delimit Scope lrust_elctx_scope with EL.
-(* We need to define [elctx] and [llctx] as notations to make eauto
-   work. But then, Coq is not able to bind them to their
-   notations, so we have to use [Arguments] everywhere. *)
-Bind Scope lrust_elctx_scope with elctx_elt.
-
-Notation "☀ κ" := (ELCtx_Alive κ) (at level 70) : lrust_elctx_scope.
-Infix "⊑" := ELCtx_Incl (at level 70) : lrust_elctx_scope.
-
-Notation "a :: b" := (@cons elctx_elt a%EL b%EL)
-  (at level 60, right associativity) : lrust_elctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons elctx_elt x1%EL (@cons elctx_elt x2%EL
-        (..(@cons elctx_elt xn%EL (@nil elctx_elt))..))) : lrust_elctx_scope.
-Notation "[ x ]" := (@cons elctx_elt x%EL (@nil elctx_elt)) : lrust_elctx_scope.
-
-Definition llctx_elt : Type := lft * list lft.
-Notation llctx := (list llctx_elt).
-
-Delimit Scope lrust_llctx_scope with LL.
-Bind Scope lrust_llctx_scope with llctx_elt.
-
-Notation "κ ⊑ κl" := (@pair lft (list lft) κ κl) (at level 70) : lrust_llctx_scope.
-
-Notation "a :: b" := (@cons llctx_elt a%LL b%LL)
-  (at level 60, right associativity) : lrust_llctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons llctx_elt x1%LL (@cons llctx_elt x2%LL
-        (..(@cons llctx_elt xn%LL (@nil llctx_elt))..))) : lrust_llctx_scope.
-Notation "[ x ]" := (@cons llctx_elt x%LL (@nil llctx_elt)) : lrust_llctx_scope.
-
-Section lft_contexts.
-  Context `{invG Σ, lftG Σ}.
-  Implicit Type (κ : lft).
-
-  (* External lifetime contexts. *)
-  Definition elctx_elt_interp (x : elctx_elt) (q : Qp) : iProp Σ :=
-    match x with
-    | ☀ κ => q.[κ]%I
-    | κ ⊑ κ' => (κ ⊑ κ')%I
-    end%EL.
-  Global Instance elctx_elt_interp_fractional x:
-    Fractional (elctx_elt_interp x).
-  Proof. destruct x; unfold elctx_elt_interp; apply _. Qed.
-  Typeclasses Opaque elctx_elt_interp.
-  Definition elctx_elt_interp_0 (x : elctx_elt) : iProp Σ :=
-    match x with
-    | ☀ κ => True%I
-    | κ ⊑ κ' => (κ ⊑ κ')%I
-    end%EL.
-  Global Instance elctx_elt_interp_0_persistent x:
-    PersistentP (elctx_elt_interp_0 x).
-  Proof. destruct x; apply _. Qed.
-  Typeclasses Opaque elctx_elt_interp_0.
-
-  Lemma elctx_elt_interp_persist x q :
-    elctx_elt_interp x q -∗ elctx_elt_interp_0 x.
-  Proof. destruct x; by iIntros "?/=". Qed.
-
-  Definition elctx_interp (E : elctx) (q : Qp) : iProp Σ :=
-    ([∗ list] x ∈ E, elctx_elt_interp x q)%I.
-  Global Arguments elctx_interp _%EL _%Qp.
-  Global Instance elctx_interp_fractional E:
-    Fractional (elctx_interp E).
-  Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
-  Global Instance elctx_interp_as_fractional E q:
-    AsFractional (elctx_interp E q) (elctx_interp E) q.
-  Proof. split. done. apply _. Qed.
-  Global Instance elctx_interp_permut:
-    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) elctx_interp.
-  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque elctx_interp.
-
-  Definition elctx_interp_0 (E : elctx) : iProp Σ :=
-    ([∗ list] x ∈ E, elctx_elt_interp_0 x)%I.
-  Global Arguments elctx_interp_0 _%EL.
-  Global Instance elctx_interp_0_persistent E:
-    PersistentP (elctx_interp_0 E).
-  Proof. apply _. Qed.
-  Global Instance elctx_interp_0_permut:
-    Proper ((≡ₚ) ==> (⊣⊢)) elctx_interp_0.
-  Proof. intros ???. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque elctx_interp_0.
-
-  Lemma elctx_interp_persist x q :
-    elctx_interp x q -∗ elctx_interp_0 x.
-  Proof.
-    unfold elctx_interp, elctx_interp_0. f_equiv. intros _ ?.
-    apply elctx_elt_interp_persist.
-  Qed.
-
-  (* Local lifetime contexts. *)
-
-  Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
-    let κ' := foldr (∪) static (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ∪ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={⊤,⊤∖↑lftN}▷=∗ [†κ0]))%I.
-  Global Instance llctx_elt_interp_fractional x :
-    Fractional (llctx_elt_interp x).
-  Proof.
-    destruct x as [κ κs]. iIntros (q q'). iSplit; iIntros "H".
-    - iDestruct "H" as (κ0) "(% & [Hq Hq'] & #?)".
-      iSplitL "Hq"; iExists _; by iFrame "∗%".
-    - iDestruct "H" as "[Hq Hq']".
-      iDestruct "Hq" as (κ0) "(% & Hq & #?)".
-      iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
-      rewrite (inj (union (foldr (∪) static κs)) κ0' κ0); last congruence.
-      iExists κ0. by iFrame "∗%".
-  Qed.
-  Typeclasses Opaque llctx_elt_interp.
-
-  Definition llctx_elt_interp_0 (x : llctx_elt) : Prop :=
-    let κ' := foldr (∪) static (x.2) in (∃ κ0, x.1 = κ' ∪ κ0).
-  Lemma llctx_elt_interp_persist x q :
-    llctx_elt_interp x q -∗ ⌜llctx_elt_interp_0 x⌝.
-  Proof.
-    iIntros "H". unfold llctx_elt_interp.
-    iDestruct "H" as (κ0) "[% _]". by iExists κ0.
-  Qed.
-
-  Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
-    ([∗ list] x ∈ L, llctx_elt_interp x q)%I.
-  Global Arguments llctx_interp _%LL _%Qp.
-  Global Instance llctx_interp_fractional L:
-    Fractional (llctx_interp L).
-  Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
-  Global Instance llctx_interp_as_fractional L q:
-    AsFractional (llctx_interp L q) (llctx_interp L) q.
-  Proof. split. done. apply _. Qed.
-  Global Instance llctx_interp_permut:
-    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
-  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque llctx_interp.
-
-  Definition llctx_interp_0 (L : llctx) : Prop :=
-    ∀ x, x ∈ L → llctx_elt_interp_0 x.
-  Global Arguments llctx_interp_0 _%LL.
-  Lemma llctx_interp_persist L q :
-    llctx_interp L q -∗ ⌜llctx_interp_0 L⌝.
-  Proof.
-    iIntros "H". iIntros (x ?). iApply llctx_elt_interp_persist.
-    unfold llctx_interp. by iApply (big_sepL_elem_of with "H").
-  Qed.
-
-  Lemma lctx_equalize_lft qE qL κ1 κ2 `{!frac_borG Σ} :
-    lft_ctx -∗ llctx_elt_interp (κ1 ⊑ [κ2]%list) qL ={⊤}=∗
-      elctx_elt_interp (κ1 ⊑ κ2) qE ∗ elctx_elt_interp (κ2 ⊑ κ1) qE.
-  Proof.
-    iIntros "#LFT Hκ". rewrite /llctx_elt_interp /=. (* TODO: Why is this unfold necessary? *)
-    iDestruct "Hκ" as (κ) "(% & Hκ & _)".
-    iMod (bor_create _ κ2 with "LFT [Hκ]") as "[Hκ _]"; first done; first by iFrame.
-    iMod (bor_fracture (λ q, (qL * q).[_])%I with "LFT [Hκ]") as "#Hκ"; first done.
-    { rewrite Qp_mult_1_r. done. }
-    iModIntro. subst κ1. iSplit.
-    - iApply lft_le_incl.
-      rewrite <-!gmultiset_union_subseteq_l. done.
-    - iApply (lft_incl_glb with "[]"); first iApply (lft_incl_glb with "[]").
-      + iApply lft_incl_refl.
-      + iApply lft_incl_static.
-      + iApply (frac_bor_lft_incl with "LFT"). done.
-  Qed.
-
-  Context (E : elctx) (L : llctx).
-
-  (* Lifetime inclusion *)
-
-  Definition lctx_lft_incl κ κ' : Prop :=
-    elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ κ ⊑ κ'.
-
-  Definition lctx_lft_eq κ κ' : Prop :=
-    lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
-
-  Lemma lctx_lft_incl_relf κ : lctx_lft_incl κ κ.
-  Proof. iIntros "_ _". iApply lft_incl_refl. Qed.
-
-  Global Instance lctx_lft_incl_preorder : PreOrder lctx_lft_incl.
-  Proof.
-    split; first by intros ?; apply lctx_lft_incl_relf.
-    iIntros (??? H1 H2) "#HE #HL". iApply (lft_incl_trans with "[#] [#]").
-    iApply (H1 with "HE HL"). iApply (H2 with "HE HL").
-  Qed.
-
-  Global Instance lctx_lft_incl_proper :
-    Proper (lctx_lft_eq ==> lctx_lft_eq ==> iff) lctx_lft_incl.
-  Proof. intros ??[] ??[]. split; intros; by etrans; [|etrans]. Qed.
-
-  Global Instance lctx_lft_eq_equivalence : Equivalence lctx_lft_eq.
-  Proof.
-    split.
-    - by split.
-    - intros ?? Heq; split; apply Heq.
-    - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
-  Qed.
-
-  Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
-  Proof. iIntros "_ _". iApply lft_incl_static. Qed.
-
-  Lemma lctx_lft_incl_local κ κ' κs :
-    (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
-  Proof.
-    iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
-    edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
-    iApply lft_le_incl. etrans; last by apply gmultiset_union_subseteq_l.
-    clear -Hκ'κs. induction Hκ'κs.
-    - apply gmultiset_union_subseteq_l.
-    - etrans. done. apply gmultiset_union_subseteq_r.
-  Qed.
-
-  Lemma lctx_lft_incl_local' κ κ' κ'' κs :
-    (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
-  Proof. intros. etrans; last done. by eapply lctx_lft_incl_local. Qed.
-
-  Lemma lctx_lft_incl_external κ κ' : (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ κ'.
-  Proof.
-    iIntros (?) "H _".
-    rewrite /elctx_interp_0 /elctx_elt_interp_0 big_sepL_elem_of //. done.
-  Qed.
-
-  Lemma lctx_lft_incl_external' κ κ' κ'' :
-    (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
-  Proof. intros. etrans; last done. by eapply lctx_lft_incl_external. Qed.
-
-  (* Lifetime aliveness *)
-
-  Definition lctx_lft_alive (κ : lft) : Prop :=
-    ∀ F qE qL, ↑lftN ⊆ F → elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
-          ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
-
-  Lemma lctx_lft_alive_static : lctx_lft_alive static.
-  Proof.
-    iIntros (F qE qL ?) "$$". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
-  Qed.
-
-  Lemma lctx_lft_alive_local κ κs:
-    (κ ⊑ κs)%LL ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
-  Proof.
-    iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qE qL ?) "HE HL".
-    iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
-    iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
-    iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
-    iAssert (∃ q', q'.[foldr union static κs] ∗
-      (q'.[foldr union static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
-      with ">[HE HL1]" as "H".
-    { move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
-      iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
-      - iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
-      - iDestruct "HL1" as "[HL1 HL2]". iDestruct "HE" as "[HE1 HE2]".
-        iMod (Hκ with "* HE1 HL1") as (q') "[Htok' Hclose]". done.
-        iMod ("IH" with "* HE2 HL2") as (q'') "[Htok'' Hclose']".
-        destruct (Qp_lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
-        iExists q0. rewrite -lft_tok_sep. iDestruct "Htok'" as "[$ Hr']".
-        iDestruct "Htok''" as "[$ Hr'']". iIntros "!>[Hκ Hfold]".
-        iMod ("Hclose" with "[$Hκ $Hr']") as "[$$]". iApply "Hclose'". iFrame. }
-    iDestruct "H" as (q') "[Htok' Hclose']". rewrite -{5}(Qp_div_2 qL).
-    destruct (Qp_lower_bound q' (qL/2)) as (q0 & q'2 & q''2 & -> & ->).
-    iExists q0. rewrite -(lft_tok_sep q0). iDestruct "Htok" as "[$ Htok]".
-    iDestruct "Htok'" as "[$ Htok']". iIntros "!>[Hfold Hκ0]".
-    iMod ("Hclose'" with "[$Hfold $Htok']") as "[$$]".
-    rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
-  Qed.
-
-  Lemma lctx_lft_alive_external κ: (☀κ)%EL ∈ E → lctx_lft_alive κ.
-  Proof.
-    iIntros ([i HE]%elem_of_list_lookup_1 F qE qL ?) "HE $ !>".
-    rewrite /elctx_interp /elctx_elt_interp.
-    iDestruct (big_sepL_lookup_acc with "HE") as "[Hκ Hclose]". done.
-    iExists qE. iFrame. iIntros "?!>". by iApply "Hclose".
-  Qed.
-
-  Lemma lctx_lft_alive_incl κ κ':
-    lctx_lft_alive κ → lctx_lft_incl κ κ' → lctx_lft_alive κ'.
-  Proof.
-    iIntros (Hal Hinc F qE qL ?) "HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hinc with "[HE] [HL]").
-      by iApply elctx_interp_persist. by iApply llctx_interp_persist.
-    iMod (Hal with "HE HL") as (q') "[Htok Hclose]". done.
-    iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']". done.
-    iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with ">").
-    by iApply "Hclose'".
-  Qed.
-
-  Lemma lctx_lft_alive_external' κ κ':
-    (☀κ)%EL ∈ E → (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ'.
-  Proof.
-    intros. eapply lctx_lft_alive_incl, lctx_lft_incl_external; last done.
-    by apply lctx_lft_alive_external.
-  Qed.
-
-  (* External lifetime context satisfiability *)
-
-  Definition elctx_sat E' : Prop :=
-    ∀ qE qL F, ↑lftN ⊆ F → elctx_interp E qE -∗ llctx_interp L qL ={F}=∗
-      ∃ qE', elctx_interp E' qE' ∗
-       (elctx_interp E' qE' ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL).
-
-  Lemma elctx_sat_nil : elctx_sat [].
-  Proof.
-    iIntros (qE qL F ?) "$$". iExists 1%Qp. rewrite /elctx_interp big_sepL_nil. auto.
-  Qed.
-
-  Lemma elctx_sat_alive E' κ :
-    lctx_lft_alive κ → elctx_sat E' → elctx_sat ((☀κ) :: E')%EL.
-  Proof.
-    iIntros (Hκ HE' qE qL F ?) "[HE1 HE2] [HL1 HL2]".
-    iMod (Hκ with "HE1 HL1") as (q) "[Htok Hclose]". done.
-    iMod (HE' with "HE2 HL2") as (q') "[HE' Hclose']". done.
-    destruct (Qp_lower_bound q q') as (q0 & q2 & q'2 & -> & ->). iExists q0.
-    rewrite {5 6}/elctx_interp big_sepL_cons /=.
-    iDestruct "Htok" as "[$ Htok]". iDestruct "HE'" as "[Hf HE']".
-    iSplitL "Hf". by rewrite /elctx_interp.
-    iIntros "!>[Htok' ?]". iMod ("Hclose" with "[$Htok $Htok']") as "[$$]".
-    iApply "Hclose'". iFrame. by rewrite /elctx_interp.
-  Qed.
-
-  Lemma elctx_sat_lft_incl E' κ κ' :
-    lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E')%EL.
-  Proof.
-    iIntros (Hκκ' HE' qE qL F ?) "HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hκκ' with "[HE] [HL]").
-      by iApply elctx_interp_persist. by iApply llctx_interp_persist.
-    iMod (HE' with "HE HL") as (q) "[HE' Hclose']". done.
-    iExists q. rewrite {1 2 4 5}/elctx_interp big_sepL_cons /=.
-    iIntros "{$Hincl $HE'}!>[_ ?]". by iApply "Hclose'".
-  Qed.
-End lft_contexts.
-
-Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
-Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
-Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
-Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
-
-Section elctx_incl.
-  (* External lifetime context inclusion, in a persistent context.
-     (Used for function types subtyping).
-     On paper, this corresponds to using only the inclusions from E, L
-     to show E1; [] |- E2.
-  *)
-
-  Context `{invG Σ, lftG Σ} (E : elctx) (L : llctx).
-
-  Definition elctx_incl E1 E2 : Prop :=
-    ∀ F, ↑lftN ⊆ F → elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-    ∀ qE1, elctx_interp E1 qE1 ={F}=∗ ∃ qE2, elctx_interp E2 qE2 ∗
-       (elctx_interp E2 qE2 ={F}=∗ elctx_interp E1 qE1).
-  Global Instance : RewriteRelation elctx_incl.
-  Arguments elctx_incl _%EL _%EL.
-
-  Global Instance elctx_incl_preorder : PreOrder elctx_incl.
-  Proof.
-    split.
-    - iIntros (???) "_ _ * ?". iExists _. iFrame. eauto.
-    - iIntros (x y z Hxy Hyz ??) "#HE #HL * HE1".
-      iMod (Hxy with "HE HL * HE1") as (qy) "[HE1 Hclose1]"; first done.
-      iMod (Hyz with "HE HL * HE1") as (qz) "[HE1 Hclose2]"; first done.
-      iModIntro. iExists qz. iFrame "HE1". iIntros "HE1".
-      iApply ("Hclose1" with ">"). iApply "Hclose2". done.
-  Qed.
-
-  Lemma elctx_incl_refl E' : elctx_incl E' E'.
-  Proof. reflexivity. Qed.
-
-  Lemma elctx_incl_nil E' : elctx_incl E' [].
-  Proof.
-    iIntros (??) "_ _ * $". iExists 1%Qp.
-    rewrite /elctx_interp big_sepL_nil. auto.
-  Qed.
-
-  Global Instance elctx_incl_app_proper :
-    Proper (elctx_incl ==> elctx_incl ==> elctx_incl) app.
-  Proof.
-    iIntros (?? HE1 ?? HE2 ??) "#HE #HL *". rewrite {1}/elctx_interp big_sepL_app.
-    iIntros "[HE1 HE2]".
-    iMod (HE1 with "HE HL * HE1") as (q1) "[HE1 Hclose1]"; first done.
-    iMod (HE2 with "HE HL * HE2") as (q2) "[HE2 Hclose2]"; first done.
-    destruct (Qp_lower_bound q1 q2) as (q & ? & ? & -> & ->).
-    iModIntro. iExists q. rewrite /elctx_interp !big_sepL_app.
-    iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]".
-    iIntros "[HE1' HE2']".
-    iMod ("Hclose1" with "[$HE1 $HE1']") as "$".
-    iMod ("Hclose2" with "[$HE2 $HE2']") as "$".
-    done.
-  Qed.
-  Global Instance elctx_incl_cons_proper x :
-    Proper (elctx_incl ==> elctx_incl) (cons x).
-  Proof. by apply (elctx_incl_app_proper [_] [_]). Qed.
-
-  Lemma elctx_incl_dup E1 :
-    elctx_incl E1 (E1 ++ E1).
-  Proof.
-    iIntros (??) "#HE #HL * [HE1 HE1']".
-    iModIntro. iExists (qE1 / 2)%Qp.
-    rewrite /elctx_interp !big_sepL_app. iFrame.
-    iIntros "[HE1 HE1']". by iFrame.
-  Qed.
-
-  Lemma elctx_sat_incl E1 E2 :
-    elctx_sat E1 [] E2 → elctx_incl E1 E2.
-   Proof.
-    iIntros (H12 ??) "#HE #HL * HE1".
-    iMod (H12 _ 1%Qp with "HE1 []") as (qE2) "[HE2 Hclose]". done.
-    { by rewrite /llctx_interp big_sepL_nil. }
-    iExists qE2. iFrame. iIntros "!> HE2".
-    by iMod ("Hclose" with "HE2") as "[$ _]".
-   Qed.
-
-  Lemma elctx_incl_lft_alive E1 E2 κ :
-    lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 ((☀κ) :: E2).
-  Proof.
-    intros Hκ HE2. rewrite (elctx_incl_dup E1).
-    apply (elctx_incl_app_proper _ [_]); last done.
-    apply elctx_sat_incl. apply elctx_sat_alive, elctx_sat_nil; first done.
-  Qed.
-
-  Lemma elctx_incl_lft_incl E1 E2 κ κ' :
-    lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E1 E2 →
-    elctx_incl E1 ((κ ⊑ κ') :: E2).
-  Proof.
-    iIntros (Hκκ' HE2 ??) "#HE #HL * HE1".
-    iDestruct (elctx_interp_persist with "HE1") as "#HE1'".
-    iDestruct (Hκκ' with "[HE HE1'] HL") as "#Hκκ'".
-    { rewrite /elctx_interp_0 big_sepL_app. auto. }
-    iMod (HE2 with "HE HL * HE1") as (qE2) "[HE2 Hclose']". done.
-    iExists qE2. rewrite /elctx_interp big_sepL_cons /=. iFrame "∗#".
-    iIntros "!> [_ HE2']". by iApply "Hclose'".
-  Qed.
-End elctx_incl.
-
-Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
-
-(* We first try to solve everything without the merging rules, and
-   then start from scratch with them.
-
-   The reason is that we want we want the search proof search for
-   [tctx_extract_hasty] to suceed even if the type is an evar, and
-   merging makes it diverge in this case. *)
-Ltac solve_typing :=
-  (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
-  (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
-Create HintDb lrust_typing discriminated.
-Create HintDb lrust_typing_merge discriminated.
-
-Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
-Hint Resolve
-     lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
-     lctx_lft_incl_external'
-     lctx_lft_alive_static lctx_lft_alive_local lctx_lft_alive_external
-     elctx_sat_nil elctx_sat_alive elctx_sat_lft_incl
-     elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
-  : lrust_typing.
-Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
-
-Hint Opaque elctx_incl elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
-
-Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
-  lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E L E1 E2 →
-  elctx_incl E L ((☀κ) :: E1) ((☀κ') :: E2).
-Proof.
-  move=> ? /elctx_incl_lft_incl -> //.
-  apply (elctx_incl_app_proper _ _ [_; _] [_]); solve_typing.
-Qed.

theories/typing/tests/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 (λ α, [# box (&uniq{α}Π[int; int])]) (λ α, box (&shr{α} int))).
-  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/tests/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 (λ _, []) (λ _, [# box int; box int]) (λ (_ : ()), box (Π[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.