From f931a587a4d25e3dc151ca1ed1fdd4ec6f926ec4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Nov 2016 14:10:10 +0100
Subject: [PATCH] Update Iris, fix some cases in rebor, tweak some proofs.

In particular, I started changing some lemmas in borrow.v to not
unfold everything right away. Unfolding everything right away
yields very big goals that do not fit in one screen and makes stuff
slow.
---
 iris                          |   2 +-
 theories/lang/heap.v          |   5 +-
 theories/lang/proofmode.v     |  21 ++++---
 theories/lifetime/accessors.v |   1 -
 theories/lifetime/borrow.v    | 107 +++++++++++++++++++---------------
 theories/lifetime/creation.v  |   4 +-
 theories/lifetime/derived.v   |   5 +-
 theories/lifetime/rebor.v     |  57 +++++++++---------
 8 files changed, 105 insertions(+), 97 deletions(-)

diff --git a/iris b/iris
index 42cf780a..1bc26dc9 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 42cf780adc3d61438701a106e50e07977c9b6abb
+Subproject commit 1bc26dc9822d6595df8d134fe365dd0356a4ac0b
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index af3550b3..92899448 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -69,10 +69,9 @@ Section definitions.
   Proof. apply _. Qed.
 End definitions.
 
-Typeclasses Opaque heap_ctx heap_mapsto heap_freeable.
+Typeclasses Opaque heap_ctx heap_mapsto heap_freeable heap_mapsto_vec.
 Instance: Params (@heap_mapsto) 4.
 Instance: Params (@heap_freeable) 5.
-Instance: Params (@heap_ctx) 2.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
@@ -128,7 +127,7 @@ Section heap.
   Proof. done. Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
-  Proof. apply _. Qed.
+  Proof. rewrite /heap_mapsto_vec. apply _. Qed.
 
   Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
   Proof.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 2b327fe5..fb4d20e8 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -14,7 +14,7 @@ Implicit Types Δ : envs (iResUR Σ).
 
 Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → 0 < n →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   (∀ l vl, n = length vl → ∃ Δ'',
     envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
       = Some Δ'' ∧
@@ -23,7 +23,7 @@ Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
 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_later_env_sound; apply later_mono, forall_intro=> l;
+  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.
@@ -32,7 +32,7 @@ Qed.
 
 Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → n = length vl →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
   envs_delete i1 false Δ' = Δ'' →
   envs_lookup i2 Δ'' = Some (false, †l…n')%I →
@@ -44,13 +44,13 @@ 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_later_env_sound -!later_sep; apply later_mono.
+  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 →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   (Δ' ⊢ |={E}=> Φ v) →
   Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
@@ -58,18 +58,18 @@ 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_later_env_sound -later_sep envs_lookup_split //; simpl.
+    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_later_env_sound -later_sep envs_lookup_split //; simpl.
+    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 →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
@@ -78,14 +78,13 @@ 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_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    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_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    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) :=
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index 3c74848b..55c85215 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -30,5 +30,4 @@ Lemma idx_bor_atomic_acc E q κ i P :
               ▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i) ∨
               [†κ] ∗ (|={E∖↑lftN,E}=> idx_bor_own q i).
 Proof. Admitted.
-
 End accessors.
\ No newline at end of file
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 239a0e22..e13617a0 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -35,9 +35,9 @@ Proof.
           ?elem_of_dom // /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in.
   iDestruct "Hinv" as "[[[_ >%]|[Hinv >%]]Hclose']". naive_solver.
   iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-  iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+  iMod (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
   unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
-  iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame "∗%". eauto.
+  iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame. eauto.
 Qed.
 
 Lemma bor_create E κ P :
@@ -46,67 +46,77 @@ Lemma bor_create E κ P :
 Proof.
   iIntros (HE) "#Hmgmt HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   iMod (ilft_create _ _ κ with "HI HA Hinv") as (A' I') "(Hκ & HI & HA & Hinv)".
-  iDestruct "Hκ" as %Hκ. rewrite big_sepS_later.
-  rewrite big_sepS_elem_of_acc
-          ?elem_of_dom // /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in.
-  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]]Hclose']".
-  - rewrite lft_inv_alive_unfold /lft_bor_alive /lft_inh.
-    iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
-    iDestruct "Halive" as (B) "(HboxB & >HownB & HB)".
-    iDestruct "Hinh" as (PE) "[>HownE HboxE]".
-    iMod (box_insert_full with "HP HboxB") as (γB) "(HBlookup & HsliceB & HboxB)".
-      by solve_ndisj.
+  iDestruct "Hκ" as %Hκ. iDestruct (@big_sepS_later with "Hinv") as "Hinv".
+  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
+  { by apply elem_of_dom. }
+  rewrite {1}/lft_inv. iDestruct "Hinv" as "[[Hinv >%]|[Hinv >%]]".
+  - rewrite {1}lft_inv_alive_unfold;
+      iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+    rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(HboxB & >HownB & HB)".
+    rewrite /lft_inh; iDestruct "Hinh" as (PE) "[>HownE HboxE]".
+    iMod (slice_insert_full _ _ true with "HP HboxB")
+      as (γB) "(HBlookup & HsliceB & HboxB)"; first by solve_ndisj.
     rewrite lookup_fmap. iDestruct "HBlookup" as %HBlookup.
-    iMod (box_insert_empty _ P with "HboxE") as (γE) "(% & HsliceE & HboxE)".
+    iMod (slice_insert_empty _ _ true _ P with "HboxE")
+      as (γE) "(% & HsliceE & HboxE)".
     rewrite -(fmap_insert bor_filled _ _ Bor_in) -to_gmap_union_singleton.
     iMod (own_bor_update with "HownB") as "HownB".
-    { apply auth_update_alloc.
-      apply: (alloc_local_update _ _ γB (1%Qp, DecAgree Bor_in)); last done.
-      rewrite lookup_fmap. by destruct (B!!γB). }
+    { eapply auth_update_alloc,
+        (alloc_local_update _ _ γB (1%Qp, DecAgree Bor_in)); last done.
+      rewrite lookup_fmap. by destruct (B !! γB). }
     iMod (own_inh_update with "HownE") as "HownE".
     { by eapply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[γE]}),
-                disjoint_singleton_l, lookup_to_gmap_None. }
+        disjoint_singleton_l, lookup_to_gmap_None. }
     rewrite -fmap_insert own_bor_op own_inh_op insert_empty.
     iDestruct "HownB" as "[HB● HB◯]". iDestruct "HownE" as "[HE● HE◯]".
     iSpecialize ("Hclose'" with "[Hvs HboxE HboxB HB● HE● HB]").
-    { iNext. iLeft. iFrame "%". iExists _, (P ∗ Pi)%I.
+    { iNext. rewrite /lft_inv. iLeft. iFrame "%".
+      rewrite lft_inv_alive_unfold. iExists (P ∗ Pb)%I, (P ∗ Pi)%I.
       iSplitL "HboxB HB● HB"; last iSplitL "Hvs".
-      - iExists _. iFrame "HboxB HB●". rewrite big_sepM_insert /=.
-          by iFrame. by destruct (B !! γB).
+      - rewrite /lft_bor_alive.
+        iExists _. iFrame "HboxB HB●".
+        iApply @big_sepM_insert; first by destruct (B !! γB).
+        simpl. iFrame.
       - rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hcnt Hvs]".
         iExists n. iFrame "Hcnt". iIntros (I'') "Hvsinv [$ HPb] H†".
         iApply ("Hvs" $! I'' with "Hvsinv HPb H†").
-      - iExists _. iFrame. }
+      - rewrite /lft_inh. iExists _. iFrame. }
     iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
-    + unfold bor, raw_bor, idx_bor_own. iExists (κ, γB).
-      iSplitL "". by iApply lft_incl_refl. by iFrame.
-    + clear -HE. iIntros "!>H†".
+    + rewrite /bor /raw_bor /idx_bor_own. iExists (κ, γB); simpl.
+      iFrame. by iApply lft_incl_refl.
+    + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
       iDestruct (own_inh_auth with "HI HE◯") as %Hκ.
-      rewrite big_sepS_elem_of_acc ?elem_of_dom //
-              /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in /lft_dead /lft_inh.
-      iDestruct "H†" as (Λ) "[% #H†]".
+      iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
+      { by apply elem_of_dom. }
+      rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
       iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
-      iDestruct "Hinv" as "[[[_ >%]|[Hinv >%]]Hclose']". naive_solver.
-      iDestruct "Hinv" as (Pinh) "(Hdead & >Hcnt & Hinh)".
-      iDestruct "Hinh" as (ESlices) "[>Hinh Hbox]".
+      rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
+      { unfold lft_alive_in in *. naive_solver. }
+      rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & >Hcnt & Hinh)".
+      rewrite /lft_inh; iDestruct "Hinh" as (ESlices) "[>Hinh Hbox]".
       iDestruct (own_inh_valid_2 with "Hinh HEâ—¯")
         as %[Hle%gset_disj_included _]%auth_valid_discrete_2.
       rewrite <-elem_of_subseteq_singleton in Hle.
       iMod (own_inh_update with "[HE◯ Hinh]") as "HE●"; [|iApply own_inh_op; by iFrame|].
       { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
-      iMod (box_delete_full with "HsliceE Hbox") as (Pinh') "($ & _ & Hbox)".
-        solve_ndisj. by rewrite lookup_to_gmap_Some.
-      iApply "Hclose". iExists _, _. iFrame. iNext. iApply "Hclose'". iRight. iFrame "%".
-      iExists _. iFrame. iExists _. iFrame.
+      iMod (slice_delete_full _ _ true with "HsliceE Hbox")
+        as (Pinh') "($ & _ & Hbox)"; first by solve_ndisj.
+      { by rewrite lookup_to_gmap_Some. }
+      iApply "Hclose". iExists A, I. iFrame. iNext. iApply "Hclose'".
+      rewrite /lft_inv. iRight. iFrame "%".
+      rewrite /lft_inv_dead. iExists Pinh'. iFrame.
+      rewrite /lft_inh. iExists _. iFrame.
       rewrite {1}(union_difference_L {[γE]} ESlices); last set_solver.
-      rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None. set_solver.
+      rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None.
+      set_solver +Hle.
   - iFrame "HP". iApply fupd_frame_r. iSplitR ""; last by auto.
-    iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
-    iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+    rewrite /lft_inv_dead. iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
+    iMod (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
     unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
-    iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame "∗%". eauto.
+    iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iNext.
+    rewrite /lft_inv. iRight. rewrite /lft_inv_dead. iFrame. eauto.
 Qed.
 
 Lemma bor_sep E κ P Q :
@@ -125,8 +135,9 @@ Proof.
     iDestruct "H" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor")
         as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
-    iMod (box_split with "Hslice Hbox") as (γ1 γ2) "(% & % & % & Hs1 & Hs2 & Hbox)".
-      solve_ndisj. by rewrite lookup_fmap EQB.
+    iMod (slice_split _ _ true with "Hslice Hbox")
+      as (γ1 γ2) "(% & % & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
+    { by rewrite lookup_fmap EQB. }
     iCombine "Hown" "Hbor" as "Hbor". rewrite -own_bor_op.
     iMod (own_bor_update with "Hbor") as "Hbor".
     { etrans; last etrans.
@@ -153,8 +164,8 @@ Proof.
     + by rewrite -fmap_None -lookup_fmap fmap_delete.
     + by rewrite lookup_insert_ne // -fmap_None -lookup_fmap fmap_delete.
   - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-    iMod (raw_bor_fake with "Hdead") as (i1) "[Hdead Hbor1]". solve_ndisj.
-    iMod (raw_bor_fake with "Hdead") as (i2) "[Hdead Hbor2]". solve_ndisj.
+    iMod (raw_bor_fake _ true with "Hdead") as (i1) "[Hdead Hbor1]"; first solve_ndisj.
+    iMod (raw_bor_fake _ true with "Hdead") as (i2) "[Hdead Hbor2]"; first solve_ndisj.
     iMod ("Hclose" with "[-Hbor1 Hbor2]") as "_".
     { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
       iRight. iSplit; last by auto. iExists _. iFrame. }
@@ -190,8 +201,11 @@ Proof.
       iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
       exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
       compute. tauto. }
-    iMod (box_combine with "Hslice1 Hslice2 Hbox") as (γ) "(% & Hslice & Hbox)".
-      solve_ndisj. done. by rewrite lookup_fmap EQB1. by rewrite lookup_fmap EQB2.
+    iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
+      as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
+    { done. }
+    { by rewrite lookup_fmap EQB1. }
+    { by rewrite lookup_fmap EQB2. }
     iCombine "Hown" "Hbor1" as "Hbor1". iCombine "Hbor1" "Hbor2" as "Hbor".
     rewrite -!own_bor_op. iMod (own_bor_update with "Hbor") as "Hbor".
     { etrans; last etrans.
@@ -215,11 +229,10 @@ Proof.
       rewrite lookup_delete_ne //.
     + rewrite -fmap_None -lookup_fmap !fmap_delete //.
   - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-    iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+    iMod (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
     iMod ("Hclose" with "[-Hbor]") as "_".
     { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
       iRight. iSplit; last by auto. iExists _. iFrame. }
     unfold bor. iExists (_, _). iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
 Qed.
-
-End borrow.
\ No newline at end of file
+End borrow.
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 0b9e20bf..9dd4c7be 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -15,7 +15,7 @@ Lemma lft_inh_kill E κ Q :
 Proof.
   rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
   iDestruct "Hinh" as (E') "[Hinh Hbox]".
-  iMod (box_fill_all with "Hbox HQ") as "?"=>//.
+  iMod (box_fill with "Hbox HQ") as "?"=>//.
   rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
 Qed.
 
@@ -124,7 +124,7 @@ Proof.
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
       as %[?%nat_included _]%auth_valid_discrete_2; omega. }
-  iMod (box_empty_all with "Hbox") as "[HP Hbox]"=>//; first solve_ndisj.
+  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first solve_ndisj.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
   iDestruct (lft_inv_alive_acc (dom _ I) _ κ with "Halive") as "[Halive Halive']".
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 263a0af2..acbe0197 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -12,7 +12,7 @@ Lemma bor_acc E q κ P :
 Proof.
   iIntros (?) "#LFT HP Htok".
   iMod (bor_acc_strong with "LFT HP Htok") as "[HP Hclose]"; first done.
-  iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
+  iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP} !> _ $".
 Qed.
 
 Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
@@ -40,7 +40,7 @@ Lemma bor_persistent P `{!PersistentP P} E κ q :
 Proof.
   iIntros (?) "#LFT Hb Htok".
   iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
-  by iMod ("Hob" with "HP") as "[_$]".
+  by iMod ("Hob" with "HP") as "[_ $]".
 Qed.
 
 Lemma lft_incl_acc E κ κ' q :
@@ -65,5 +65,4 @@ Proof.
   - 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.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 91b9e902..310dd12b 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -8,48 +8,51 @@ Section rebor.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma raw_bor_fake E κ P :
+Lemma raw_bor_fake E q κ P :
   ↑borN ⊆ E →
-  ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) P.
+  ▷?q lft_bor_dead κ ={E}=∗ ∃ i, ▷?q lft_bor_dead κ ∗ raw_bor (κ, i) P.
 Proof.
   iIntros (?) "Hdead". rewrite /lft_bor_dead.
   iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
-  iMod (box_insert_empty _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
+  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
   iMod (own_bor_update with "Hown") as "Hown".
-  { apply auth_update_alloc.
-    apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
-    do 2 eapply lookup_to_gmap_None. by eauto. }
-  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own. iExists _.
-  iDestruct "Hown" as "[H● H◯]". iSplitL "H● Hbox"; last by eauto.
-  iExists _, _. rewrite -!to_gmap_union_singleton. by iFrame.
+  { eapply auth_update_alloc,
+      (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
+    by do 2 eapply lookup_to_gmap_None. }
+  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own /=. iExists γ.
+  iDestruct "Hown" as "[H● $]". iFrame "Hslice". iModIntro. iNext.
+  iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
 Qed.
 
 Lemma raw_bor_unnest A I Pb Pi P κ κ' i :
   let Iinv := (
     own_ilft_auth I ∗
-    ▷ ([∗ set] κ ∈ dom _ I ∖ {[ κ' ]}, lft_inv A κ))%I in
+    ▷ [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
   κ ⊆ κ' →
   lft_alive_in A κ' →
   Iinv -∗ raw_bor (κ,i) P -∗ ▷ lft_bor_alive κ' Pb -∗
   ▷ lft_vs κ' (Pb ∗ raw_bor (κ,i) P) Pi ={↑borN}=∗ ∃ Pb' j,
     Iinv ∗ raw_bor (κ',j) P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
 Proof.
-  iIntros (Iinv Hκκ' Haliveκ') "(HI & HA) Hraw Hκalive' Hvs".
+  iIntros (Iinv Hκκ' Haliveκ') "(HI● & HI) Hraw Hκalive' Hvs".
   destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iModIntro. iExists Pb, i. rewrite /Iinv. iFrame "HI HA Hκalive' Hraw".
+  { iModIntro. iExists Pb, i. rewrite /Iinv. iFrame "HI● HI Hκalive' Hraw".
     iNext. rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hn Hvs]".
     iExists n. iFrame "Hn". clear Iinv I.
-    iIntros (I) "Hinv HPb Hdead". admit. }
+    iIntros (I). rewrite lft_vs_inv_unfold. iIntros "(Hdead & $ & HI) HPb Hκ†".
+    iMod (raw_bor_fake _ false _ P with "Hdead") as (i') "?"; first solve_ndisj.
+    (* We get the existential too late *)
+    admit. }
   assert (κ ⊂ κ') by (by apply strict_spec_alt).
   rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hcnt Hvs]".
   iMod (own_cnt_update with "Hcnt") as "Hcnt".
   { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
   rewrite own_cnt_op; iDestruct "Hcnt" as "[Hcnt Hcnt1]".
   rewrite {1}/raw_bor /idx_bor_own /=. iDestruct "Hraw" as "[Hbor #Hislice]".
-  iDestruct (own_bor_auth with "HI Hbor") as %?.
+  iDestruct (own_bor_auth with "HI● Hbor") as %?.
   rewrite big_sepS_later.
-  iDestruct (big_sepS_elem_of_acc _ (dom (gset lft) I ∖ _) κ
-    with "HA") as "[HAκ HA]".
+  iDestruct (big_sepS_elem_of_acc _ (dom (gset lft) I ∖ _) κ with "HI")
+    as "[HAκ HI]".
   { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
   iDestruct (lft_inv_alive_in with "HAκ") as "Hκalive";
     first by eauto using lft_alive_in_subseteq.
@@ -58,14 +61,14 @@ Proof.
   rewrite {2}/lft_bor_alive; iDestruct "Hbor'" as (B) "(Hbox & >HκB & HB)".
   iDestruct (own_bor_valid_2 with "HκB Hbor")
     as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (box_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
+  iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HκB Hbor") as "HFOO".
   { eapply auth_update, singleton_local_update,
      (exclusive_local_update _ (1%Qp, DecAgree (Bor_rebor κ'))); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   rewrite own_bor_op. iDestruct "HFOO" as "[HκB Hrebor]".
-  iSpecialize ("HA" with "[Hcnt1 HB Hvs' Hinh' Hbox HκB]").
+  iSpecialize ("HI" with "[Hcnt1 HB Hvs' Hinh' Hbox HκB]").
   { 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'".
@@ -77,14 +80,15 @@ Proof.
     iFrame; simpl; auto. }
   clear B HB Pb' Pi'.
   rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >Hbor & HB)".
-  iMod (box_insert_full with "HP Hbox") as (j) "(HBj & #Hjslice & Hbox)"; first done.
+  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 "Hbor") as "HFOO".
   { apply auth_update_alloc,
      (alloc_singleton_local_update _ j (1%Qp, DecAgree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
   rewrite own_bor_op. iDestruct "HFOO" as "[HκB Hj]".
-  iModIntro. iExists (P ∗ Pb)%I, j. rewrite /Iinv. iFrame "HI HA".
+  iModIntro. iExists (P ∗ Pb)%I, j. rewrite /Iinv. iFrame "HI● HI".
   iSplitL "Hj".
   { rewrite /raw_bor /idx_bor_own. by iFrame. }
   iSplitL "HB HκB Hbox".
@@ -107,10 +111,8 @@ Proof.
      (exclusive_local_update _ (1%Qp, DecAgree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   rewrite own_bor_op. iDestruct "HFOO" as "[Hbor Hrebor]".
-  iMod (box_fill with "Hislice HP [Hbox]") as "Hbox". 3: by iNext. solve_ndisj.
-  by rewrite lookup_fmap HB.
-iAssert (box borN (<[i:=true]> (bor_filled <$> B')) Pb') with "[Hbox]" as "Hbox".
-admit.
+  iMod (slice_fill _ _ false with "Hislice HP Hbox") as "Hbox"; first by solve_ndisj.
+  { by rewrite lookup_fmap HB. }
   iDestruct (@big_sepM_delete with "HB") as "[Hκ HB]"; first done.
   rewrite /=; iDestruct "Hκ" as "[% Hcnt]".
   iMod ("Hvs" $! I with "[Hdead HI Hκs Hbox Hvs' Hinh Hbor HB]
@@ -122,12 +124,10 @@ admit.
     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 /=. iFrame; auto. }
-    iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus.
-(* auth_frag_op. *)
-
+  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
+  by iFrame.
 Admitted.
 
-
 Lemma raw_rebor E κ κ' i P :
   ↑lftN ⊆ E → κ ⊆ κ' →
   lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
@@ -155,5 +155,4 @@ Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
 Proof. Admitted.
-
 End rebor.
-- 
GitLab