Seal lifetime logic behind a signature

Coq's module system is wholly inadequate :/

_CoqProject

 -Q theories lrust
-theories/lifetime/definitions.v
-theories/lifetime/derived.v
-theories/lifetime/faking.v
-theories/lifetime/creation.v
-theories/lifetime/primitive.v
-theories/lifetime/accessors.v
-theories/lifetime/raw_reborrow.v
-theories/lifetime/borrow.v
-theories/lifetime/reborrow.v
+theories/lifetime/model/definitions.v
+theories/lifetime/model/faking.v
+theories/lifetime/model/creation.v
+theories/lifetime/model/primitive.v
+theories/lifetime/model/accessors.v
+theories/lifetime/model/raw_reborrow.v
+theories/lifetime/model/borrow.v
+theories/lifetime/model/reborrow.v
+theories/lifetime/lifetime_sig.v
+theories/lifetime/lifetime.v
 theories/lifetime/shr_borrow.v
 theories/lifetime/frac_borrow.v
 theories/lifetime/na_borrow.v

theories/lifetime/frac_borrow.v

@@ -2,7 +2,7 @@ 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 .
+From lrust.lifetime Require Export shr_borrow.
 Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
@@ -128,7 +128,7 @@ Section frac_bor.
   Lemma frac_bor_lft_incl κ κ' q:
     lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
-    iIntros "#LFT#Hbor!#". iSplitR.
+    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.

theories/lifetime/derived.v → theories/lifetime/lifetime.v

-From lrust.lifetime Require Export primitive accessors faking.
-From lrust.lifetime Require Export raw_reborrow.
+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".
-(* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven
-in the model, depends on this file. *)
+
+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_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
+Lemma bor_acc_cons E q κ P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
+    ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
 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").
+  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 :
@@ -80,8 +99,9 @@ Qed.
 
 Lemma lft_incl_static κ : (κ ⊑ static)%I.
 Proof.
-  iIntros "!#". iSplitR.
+  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/lifetime_sig.v

+From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.prelude Require Export gmultiset strings.
+From iris.base_logic.lib Require Export invariants.
+From iris.base_logic.lib Require Import boxes fractional.
+Set Default Proof Using "Type".
+
+Definition lftN : namespace := nroot .@ "lft".
+Definition borN : namespace := lftN .@ "bor".
+Definition inhN : namespace := lftN .@ "inh".
+Definition mgmtN : namespace := lftN .@ "mgmt".
+
+Definition atomic_lft := positive.
+Notation lft := (gmultiset positive).
+Definition static : lft := ∅.
+
+Inductive bor_state :=
+  | Bor_in
+  | Bor_open (q : frac)
+  | Bor_rebor (κ : lft).
+Instance bor_state_eq_dec : EqDecision bor_state.
+Proof. solve_decision. Defined.
+Canonical bor_stateC := leibnizC bor_state.
+
+Record lft_names := LftNames {
+  bor_name : gname;
+  cnt_name : gname;
+  inh_name : gname
+}.
+Instance lft_names_eq_dec : EqDecision lft_names.
+Proof. solve_decision. Defined.
+Canonical lft_namesC := leibnizC lft_names.
+
+Definition lft_stateR := csumR fracR unitR.
+Definition alftUR := gmapUR atomic_lft lft_stateR.
+Definition ilftUR := gmapUR lft (agreeR lft_namesC).
+Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
+Definition inhUR := gset_disjUR slice_name.
+
+Class lftG Σ := LftG {
+  lft_box :> boxG Σ;
+  alft_inG :> inG Σ (authR alftUR);
+  alft_name : gname;
+  ilft_inG :> inG Σ (authR ilftUR);
+  ilft_name : gname;
+  lft_bor_inG :> inG Σ (authR borUR);
+  lft_cnt_inG :> inG Σ (authR natUR);
+  lft_inh_inG :> inG Σ (authR inhUR);
+}.
+
+Module Type lifetime_sig.
+  (** Definitions *)
+  Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
+
+  Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
+  Parameter lft_dead : ∀ `{lftG Σ} (κ : lft), iProp Σ.
+
+  Parameter lft_incl : ∀ `{invG, lftG Σ} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{invG, lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
+
+  Parameter bor_idx : Type.
+  Parameter idx_bor_own : ∀ `{lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
+  Parameter idx_bor : ∀ `{invG, lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  
+  Notation "q .[ κ ]" := (lft_tok q κ)
+      (format "q .[ κ ]", at level 0) : uPred_scope.
+  Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
+
+  Notation "&{ κ } P" := (bor κ P)
+    (format "&{ κ }  P", at level 20, right associativity) : uPred_scope.
+  Notation "&{ κ , i } P" := (idx_bor κ i P)
+    (format "&{ κ , i }  P", at level 20, right associativity) : uPred_scope.
+
+  Infix "⊑" := lft_incl (at level 70) : uPred_scope.
+
+  Section properties.
+  Context `{invG, lftG Σ}.
+
+  (** Instances *)
+  Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
+  Global Declare Instance lft_dead_persistent κ : PersistentP (lft_dead κ).
+  Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
+  Global Declare Instance idx_bor_persistent κ i P : PersistentP (idx_bor κ i P).
+
+  Global Declare Instance lft_tok_timeless q κ : TimelessP (lft_tok q κ).
+  Global Declare Instance lft_dead_timeless κ : TimelessP (lft_dead κ).
+  Global Declare Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
+
+  Global Instance idx_bor_params : Params (@idx_bor) 5.
+  Global Instance bor_params : Params (@bor) 4.
+
+  Global Declare Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
+  Global Declare Instance bor_contractive κ : Contractive (bor κ).
+  Global Declare Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
+  Global Declare Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
+  Global Declare Instance idx_bor_contractive κ i : Contractive (idx_bor κ i).
+  Global Declare Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
+
+  Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
+  Global Declare Instance lft_tok_as_fractional κ q :
+    AsFractional q.[κ] (λ q, q.[κ])%I q.
+  Global Declare Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
+  Global Declare Instance idx_bor_own_as_fractional i q :
+    AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
+
+  (** Laws *)
+  Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
+  Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ∪ κ2].
+  Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [† κ] -∗ False.
+  Parameter lft_tok_static : ∀ q, q.[static]%I.
+  Parameter lft_dead_static : [† static] -∗ False.
+
+  Parameter lft_create : ∀ E, ↑lftN ⊆ E →
+    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
+  Parameter bor_create : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+  Parameter bor_fake : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+
+  Parameter bor_sep : ∀ E κ P Q,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
+  Parameter bor_combine : ∀ E κ P Q,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
+
+  Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
+  Parameter bor_shorten : ∀ κ κ' P, κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+  Parameter idx_bor_shorten : ∀ κ κ' i P, κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
+
+  Parameter rebor : ∀ E κ κ' P,
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+  Parameter bor_unnest : ∀ E κ κ' P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
+
+  Parameter idx_bor_acc : ∀ E q κ i P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
+      ▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
+  Parameter idx_bor_atomic_acc : ∀ E q κ i P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ,i}P -∗ idx_bor_own q i ={E,E∖↑lftN}=∗
+      (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i)) ∨
+                ([†κ] ∗ |={E∖↑lftN,E}=> idx_bor_own q i).
+  Parameter bor_acc_strong : ∀ E q κ P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
+      ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
+  Parameter bor_acc_atomic_strong : ∀ E κ P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+      (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
+         ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+           ([†κ] ∗ |={E∖↑lftN,E}=> True).
+
+  (* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
+     unless we want to prove them twice (both here and in model.primitive) *)
+  Parameter lft_le_incl : ∀ κ κ', κ' ⊆ κ → (κ ⊑ κ')%I.
+  Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
+  Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
+  Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+  Parameter lft_incl_mono : ∀ κ1 κ1' κ2 κ2',
+    κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+  Parameter lft_incl_acc : ∀ E κ κ' q,
+    ↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+  Parameter lft_incl_dead : ∀ E κ κ', ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
+  Parameter lft_incl_intro : ∀ κ κ',
+    □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
+                 lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
+        (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+  (* Same for some of the derived lemmas. *)
+  Parameter bor_exists : ∀ {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  Parameter bor_acc_atomic_cons : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+      (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+      ([†κ] ∗ |={E∖↑lftN,E}=> True).
+  Parameter bor_acc_atomic : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
+       (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
+
+  End properties.
+End lifetime_sig.

theories/lifetime/accessors.v → theories/lifetime/model/accessors.v

@@ -255,18 +255,7 @@ Proof.
       iApply fupd_intro_mask'. solve_ndisj.
 Qed.
 
-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.
-
+(* These derived lemmas are needed inside the model. *)
 Lemma bor_acc_atomic_cons E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
@@ -282,15 +271,6 @@ Proof.
   - iRight. by iFrame.
 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_acc_atomic E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
@@ -301,4 +281,5 @@ Proof.
   - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "* HP []"); auto.
   - iRight. by iFrame.
 Qed.
+
 End accessors.

theories/lifetime/borrow.v → theories/lifetime/model/borrow.v

@@ -182,4 +182,5 @@ Proof.
       iRight. iSplit; last by auto. iExists _. iFrame. }
     unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
 Qed.
+
 End borrow.

theories/lifetime/definitions.v → theories/lifetime/model/definitions.v

-From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.prelude Require Export gmultiset strings.
-From iris.base_logic.lib Require Export invariants.
-From iris.base_logic.lib Require Import boxes.
+From iris.algebra Require Import csum auth frac agree gset.
 From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import boxes.
+From lrust.lifetime Require Export lifetime_sig.
 Set Default Proof Using "Type".
 Import uPred.
 
-Definition lftN : namespace := nroot .@ "lft".
-Definition borN : namespace := lftN .@ "bor".
-Definition inhN : namespace := lftN .@ "inh".
-Definition mgmtN : namespace := lftN .@ "mgmt".
-
-Definition atomic_lft := positive.
-Notation lft := (gmultiset positive).
-Definition static : lft := ∅.
-
-Inductive bor_state :=
-  | Bor_in
-  | Bor_open (q : frac)
-  | Bor_rebor (κ : lft).
-Instance bor_state_eq_dec : EqDecision bor_state.
-Proof. solve_decision. Defined.
-Canonical bor_stateC := leibnizC bor_state.
 
 Definition bor_filled (s : bor_state) : bool :=
   match s with Bor_in => true | _ => false end.
 
-Definition lft_stateR := csumR fracR unitR.
 Definition to_lft_stateR (b : bool) : lft_stateR :=
   if b then Cinl 1%Qp else Cinr ().
-
-Record lft_names := LftNames {
-  bor_name : gname;
-  cnt_name : gname;
-  inh_name : gname
-}.
-Instance lft_names_eq_dec : EqDecision lft_names.
-Proof. solve_decision. Defined.
-Canonical lft_namesC := leibnizC lft_names.
-
-Definition alftUR := gmapUR atomic_lft lft_stateR.
 Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
-
-Definition ilftUR := gmapUR lft (agreeR lft_namesC).
 Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
-
-Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
 
-Definition inhUR := gset_disjUR slice_name.
-
-Class lftG Σ := LftG {
-  lft_box :> boxG Σ;
-  alft_inG :> inG Σ (authR alftUR);
-  alft_name : gname;
-  ilft_inG :> inG Σ (authR ilftUR);
-  ilft_name : gname;
-  lft_bor_inG :> inG Σ (authR borUR);
-  lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_inG :> inG Σ (authR inhUR);
-}.
 
 Section defs.
   Context `{invG Σ, lftG Σ}.
@@ -186,9 +141,9 @@ End defs.
 Instance: Params (@lft_bor_alive) 4.
 Instance: Params (@lft_inh) 5.
 Instance: Params (@lft_vs) 4.
-Instance: Params (@idx_bor) 5.
-Instance: Params (@raw_bor) 4.
-Instance: Params (@bor) 4.
+Instance idx_bor_params : Params (@idx_bor) 5.
+Instance raw_bor_params : Params (@raw_bor) 4.
+Instance bor_params : Params (@bor) 4.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 0) : uPred_scope.
@@ -201,6 +156,9 @@ Notation "&{ κ , i } P" := (idx_bor κ i P)
 
 Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 
+(* TODO: Making all these things opaque is rather annoying, we should
+   find a way to avoid it, or *at least*, to avoid having to manually unfold
+   this because iDestruct et al don't look through these names any more. *)
 Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
   idx_bor_own idx_bor raw_bor bor.
@@ -307,8 +265,8 @@ Proof. rewrite /lft_tok. apply _. Qed.
 
 Global Instance lft_dead_persistent κ : PersistentP [†κ].
 Proof. rewrite /lft_dead. apply _. Qed.
-Global Instance lft_dead_timeless κ : PersistentP [†κ].
-Proof. rewrite /lft_tok. apply _. Qed.
+Global Instance lft_dead_timeless κ : TimelessP [†κ].
+Proof. rewrite /lft_dead. apply _. Qed.
 
 Global Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
 Proof. rewrite /lft_incl. apply _. Qed.

theories/lifetime/faking.v → theories/lifetime/model/faking.v

@@ -112,8 +112,7 @@ Proof.
 Qed.
 
 Lemma bor_fake E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+  ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
 Proof.
   iIntros (?) "#LFT H†". iMod (raw_bor_fake' with "LFT H†"); first done.
   iModIntro. unfold bor. iExists κ. iFrame. iApply lft_incl_refl.

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

-From lrust.lifetime Require Export definitions.
+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.
@@ -353,6 +353,12 @@ Proof.
   iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
 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.
@@ -363,7 +369,7 @@ Proof.
     iExists κ'. iFrame. iExists s. by iFrame.
 Qed.
 
-Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+Lemma bor_shorten κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
 Proof.
   rewrite /bor. iIntros "#Hκκ'". iDestruct 1 as (i) "[#? ?]".
   iExists i. iFrame. by iApply (lft_incl_trans with "Hκκ'").

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

-From lrust.lifetime Require Export borrow derived.
+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.
@@ -10,6 +10,18 @@ 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).

theories/lifetime/na_borrow.v

-From lrust.lifetime Require Export derived.
+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".

theories/lifetime/shr_borrow.v

 From iris.algebra Require Import gmap auth frac.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Export derived.
+From lrust.lifetime Require Export lifetime.
 Set Default Proof Using "Type".
 
 (** Shared bors  *)

theories/typing/borrow.v

 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.

theories/typing/cont.v

 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
 Set Default Proof Using "Type".

theories/typing/cont_context.v

 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
-From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts type_context.
 Set Default Proof Using "Type".
 

theories/typing/fixpoint.v

-From lrust.lifetime Require Import definitions.
 From lrust.typing Require Export lft_contexts type bool.
 Set Default Proof Using "Type".
 

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.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs cont.
 Set Default Proof Using "Type".

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 derived borrow frac_borrow.
+From lrust.lifetime Require Import frac_borrow.
 Set Default Proof Using "Type".
 
 Inductive elctx_elt : Type :=