complete unnesting. this completes the lifetime logic :D

theories/lifetime/accessors.v

@@ -54,24 +54,6 @@ Proof.
   rewrite -insert_delete big_sepM_insert ?lookup_delete //. simpl. by iFrame.
 Qed.
 
-Lemma create_dead A κ:
-  lft_dead_in A κ →
-  own_alft_auth A ==∗ own_alft_auth A ∗ [†κ].
-Proof.
-  iIntros ((Λ & HΛκ & EQΛ)) "HA". unfold own_alft_auth, lft_dead.
-  iMod (own_update _ ((● to_alftUR A)) with "HA") as "HA".
-  { eapply (auth_update_alloc _ _ ({[Λ := Cinr ()]}⋅∅)), op_local_update_discrete=>HA Λ'.
-    specialize (HA Λ'). revert HA.
-    rewrite lookup_op lookup_fmap. destruct (decide (Λ = Λ')) as [<-|].
-    - by rewrite lookup_singleton EQΛ.
-    - rewrite lookup_singleton_ne //. by destruct (to_lft_stateR <$> A !! Λ'). }
-  rewrite right_id. iDestruct "HA" as "[HA HΛ]". iSplitL "HA"; last (iExists _; by iFrame).
-  assert ({[Λ := Cinr ()]} ⋅ to_alftUR A ≡ to_alftUR A) as ->; last done.
-  intros Λ'. rewrite lookup_op. destruct (decide (Λ = Λ')) as [<-|].
-  - by rewrite lookup_singleton lookup_fmap EQΛ.
-  - rewrite lookup_singleton_ne //. by case: (to_alftUR A !! Λ').
-Qed.
-
 Lemma add_vs Pb Pb' P Q Pi κ :
   ▷ ▷ (Pb ≡ (P ∗ Pb')) -∗ ▷ lft_vs κ Pb Pi -∗ ▷ (▷ Q -∗ [†κ] ={⊤∖↑lftN}=∗ ▷ P) -∗
   ▷ lft_vs κ (Q ∗ Pb') Pi.
@@ -122,7 +104,7 @@ Proof.
         as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
       by destruct INCL as [[=]|(? & ? & [=<-] &
         [[_<-]%lookup_to_gmap_Some [[_[=]]|[]%(exclusive_included _)]])].
-  - iMod (create_dead with "HA") as "[_ H†]". done.
+  - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
     iDestruct (lft_tok_dead with "Htok H†") as "[]".
 Qed.
 
@@ -152,7 +134,7 @@ Proof.
     iApply "Hclose''". iLeft. iFrame "%". iExists _, _. iFrame.
     iExists _. iFrame.
     rewrite insert_insert -(fmap_insert _ _ _ Bor_in) insert_id //.
-  - iRight. iMod (create_dead with "HA") as "[HA #H†]". done.
+  - iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]". done.
     iMod ("Hclose'" with "[-Hbor]") as "_".
     + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
     + iMod (lft_incl_dead with "Hle H†"). done. iFrame.
@@ -219,7 +201,7 @@ Proof.
         as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
       by destruct INCL as [[=]|(? & ? & [=<-] &
         [[_<-]%lookup_to_gmap_Some [[_[=]]|[]%(exclusive_included _)]])].
-  - iMod (create_dead with "HA") as "[_ H†]". done.
+  - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
     iDestruct (lft_tok_dead with "Htok H†") as "[]".
 Qed.
 
@@ -265,7 +247,7 @@ Proof.
     iExists _. iFrame "Hbox H●".
     rewrite big_sepM_insert. by rewrite big_sepM_delete.
       by rewrite -fmap_None -lookup_fmap fmap_delete.
-  - iRight. iMod (create_dead with "HA") as "[HA #H†]". done.
+  - iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]". done.
     iMod ("Hclose'" with "[-Hbor]") as "_".
     + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
     + iMod (lft_incl_dead with "Hle H†") as "$". done.
@@ -318,4 +300,4 @@ Proof.
   - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "* HP []"); auto.
   - iRight. by iFrame.
 Qed.
-End accessors.
+End accessors.
\ No newline at end of file

theories/lifetime/primitive.v

@@ -202,6 +202,29 @@ Proof.
 Qed.
 Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
 Proof. exists Λ. by rewrite lookup_insert. Qed.
+Lemma lft_dead_in_alive_in_union A κ κ' :
+  lft_dead_in A (κ ∪ κ') → lft_alive_in A κ → lft_dead_in A κ'.
+Proof.
+  intros (Λ & [Hin|Hin]%elem_of_union & HΛ) Halive.
+  - contradict HΛ. rewrite (Halive _ Hin). done.
+  - exists Λ. auto.
+Qed.
+
+Lemma lft_dead_in_tok A κ:
+  lft_dead_in A κ →
+  own_alft_auth A ==∗ own_alft_auth A ∗ [†κ].
+Proof.
+  iIntros ((Λ & HΛκ & EQΛ)) "HA". unfold own_alft_auth, lft_dead.
+  assert (({[Λ := Cinr ()]} ⋅ to_alftUR A) = to_alftUR A) as HAinsert.
+  { unfold_leibniz=>Λ'. destruct (decide (Λ = Λ')) as [<-|Hne].
+    + rewrite lookup_op lookup_fmap EQΛ lookup_singleton /=. done.
+    + rewrite lookup_op lookup_fmap !lookup_insert_ne // lookup_empty left_id -lookup_fmap. done. }
+  iMod (own_update _ ((● to_alftUR A)) with "HA") as "HA".
+  { eapply (auth_update_alloc _ _ ({[Λ := Cinr ()]}⋅∅)), op_local_update_discrete.
+    by rewrite HAinsert. }
+  rewrite right_id. iDestruct "HA" as "[HA HΛ]". iSplitL "HA"; last (iExists _; by iFrame).
+  by rewrite HAinsert.
+Qed.
 
 Lemma lft_inv_alive_twice κ : lft_inv_alive κ -∗ lft_inv_alive κ -∗ False.
 Proof.
@@ -349,11 +372,23 @@ Proof.
   rewrite /idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'").
 Qed.
 
+Lemma raw_bor_inI I κ P :
+  own_ilft_auth I -∗ raw_bor κ P -∗ ⌜is_Some (I !! κ)⌝.
+Proof.
+  iIntros "HI Hbor". rewrite /raw_bor /idx_bor_own. iDestruct "Hbor" as (?) "[Hbor _]".
+  iApply (own_bor_auth with "HI Hbor").
+Qed.
+
 (* Inheritance *)
 Lemma lft_inh_extend E κ P Q :
   ↑inhN ⊆ E →
   ▷ lft_inh κ false Q ={E}=∗ ▷ lft_inh κ false (P ∗ Q) ∗
+     (* This states that κ will henceforth always be allocated.
+        That's not at all related to extending the inheritance,
+        but it's useful to have it here. *)
      (∀ I, own_ilft_auth I -∗ ⌜is_Some (I !! κ)⌝) ∗
+     (* This is the extraction: Always in the future, we can get
+        ▷ P from whatever lft_inh is at the time. *)
      (∀ Q', ▷ lft_inh κ true Q' ={E}=∗ ∃ Q'',
             ▷ ▷ (Q' ≡ (P ∗ Q'')) ∗ ▷ P ∗ ▷ lft_inh κ true Q'').
 Proof.
@@ -402,4 +437,19 @@ Proof.
   iExists n. iFrame "Hcnt". iIntros (I'') "Hinv [$ HPb] H†".
   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.
+Proof.
+  iIntros "Hcons Hvs". iNext. 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κ†").
+  rewrite lft_vs_inv_unfold. by iFrame.
+Qed.
 End primitive.

theories/lifetime/raw_reborrow.v

@@ -13,14 +13,14 @@ Implicit Types κ : lft.
    κ ≠ κ'.  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 A I Pb Pi P κ i κ' :
+Lemma raw_bor_unnest E q A I Pb Pi P κ i κ' :
   ↑borN ⊆ E →
-  let Iinv := (own_ilft_auth I ∗ ▷ lft_inv A κ)%I in
+  let Iinv := (own_ilft_auth I ∗ ▷?q lft_inv A κ)%I in
   κ ⊂ κ' →
   lft_alive_in A κ' →
-  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.
+  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.
 Proof.
   iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
   rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
@@ -36,13 +36,13 @@ Proof.
   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 _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
+  iMod (slice_empty 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, singleton_local_update,
      (exclusive_local_update _ (1%Qp, DecAgree (Bor_rebor κ'))); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
-  iAssert (▷ lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
+  iAssert (▷?q 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'".
@@ -53,7 +53,7 @@ Proof.
     rewrite -insert_delete 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 _ _ true with "HP Hbox")
+  iMod (slice_insert_full 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]".
@@ -100,6 +100,36 @@ Proof.
   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.
+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".
+Qed.
+
 Lemma raw_rebor E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
   lft_ctx -∗ raw_bor κ P ={E}=∗
@@ -130,7 +160,7 @@ Proof.
   { 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 _ _ _ _ (idx_bor_own 1 (κ, i) ∗ Pi)%I
+  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. }

theories/lifetime/reborrow.v

 From lrust.lifetime Require Export borrow derived.
-From lrust.lifetime Require Import raw_reborrow.
+From lrust.lifetime Require Import raw_reborrow accessors.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
@@ -31,36 +31,60 @@ Lemma bor_unnest E κ κ' P :
 Proof.
   iIntros (?) "#LFT Hκ". rewrite {2}/bor.
   iMod (bor_exists with "LFT Hκ") as (κ0) "Hκ"; first done.
-  rewrite {1}/bor; iDestruct "Hκ" as (κ0') "[#H⊑ Hκ]".
+  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 "[Hinv' Hinv]";
+  iDestruct (big_sepS_delete _ _ κ'' with "Hinv") as "[Hκ'' Hinv]";
     first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hinv'" as "[[Hinv' >%]|[Hdead >%]]"; last first.
-  { rewrite /lft_inv_dead;
-      iDestruct "Hdead" as (Pi) "(Hdead & Hcnt & Hinh)".
-    iMod (raw_bor_fake _ true _ P with "Hdead")
-      as "[Hdead Hbor]"; first solve_ndisj.
-    iMod ("Hclose" with "[- Hbor]") as "_".
+  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; last auto.
-      rewrite /lft_inv_dead. iExists Pi. iFrame. }
-    iApply (step_fupd_mask_mono E _ _ E); try solve_ndisj.
-    rewrite /bor. do 3 iModIntro. 
-    iExists κ''. iFrame "Hbor". rewrite /κ''.
-    (* Why is this going to work out *)
-    admit. }
+      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 (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
-Admitted.
+  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 cotnractive 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.