Port other kinds of borrows.

_CoqProject

@@ -7,3 +7,5 @@ theories/lifetime/primitive.v
 theories/lifetime/todo.v
 theories/lifetime/borrow.v
 theories/lifetime/shr_borrow.v
+theories/lifetime/frac_borrow.v
+theories/lifetime/tl_borrow.v

theories/frac_borrow.v → theories/lifetime/frac_borrow.v

@@ -2,64 +2,64 @@ 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 Require Export lifetime shr_borrow.
+From lrust.lifetime Require Export shr_borrow .
 
-Class frac_borrowG Σ := frac_borrowG_inG :> inG Σ fracR.
+Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Definition frac_borrow `{invG Σ, lifetimeG Σ, frac_borrowG Σ} κ (Φ : Qp → iProp Σ) :=
+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_borrow κ P)
+Notation "&frac{ κ } P" := (frac_bor κ P)
   (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
 
-Section frac_borrow.
-  Context `{invG Σ, lifetimeG Σ, frac_borrowG Σ}.
+Section frac_bor.
+  Context `{invG Σ, lftG Σ, frac_borG Σ}.
   Implicit Types E : coPset.
 
-  Global Instance frac_borrow_proper :
-    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ).
+  Global Instance frac_bor_proper :
+    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_bor κ).
   Proof. solve_proper. Qed.
-  Global Instance frac_borrow_persistent : PersistentP (&frac{κ}Φ) := _.
+  Global Instance frac_bor_persistent : PersistentP (&frac{κ}Φ) := _.
 
-  Lemma borrow_fracture φ E κ :
+  Lemma bor_fracture φ E κ :
     ↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
   Proof.
     iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
-    iMod (borrow_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
+    iMod (bor_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
     - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
-      { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ").
+      { iExists γ, κ. iSplitR; last by iApply (bor_share with "Hφ").
         iApply lft_incl_refl. }
       iSplitL. by iExists 1%Qp; iFrame; auto.
       iIntros "!>H† HΦ!>". iNext. iDestruct "HΦ" as (q') "(HΦ & _ & [%|Hκ])". by subst.
       iDestruct "Hκ" as (q'') "[_ Hκ]".
-      iDestruct (lft_own_dead with "Hκ H†") as "[]".
+      iDestruct (lft_tok_dead with "Hκ H†") as "[]".
     - iMod ("Hclose" with "*") as "HΦ"; last first.
       iExists γ, κ. iSplitR. by iApply lft_incl_refl.
-      iMod (borrow_fake with "LFT H†"). done. by iApply borrow_share.
+      iMod (bor_fake with "LFT H†"). done. by iApply bor_share.
   Qed.
 
-  Lemma frac_borrow_atomic_acc E κ φ :
+  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_borrow_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
+    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_borrow_acc_strong E q κ Φ:
+  Lemma frac_bor_acc_strong 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_borrow.
+    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_borrow_acc_tok with "LFT Hshr Hκ1") as "[H 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.
@@ -74,7 +74,7 @@ Section frac_borrow.
       - 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_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
+    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. }
@@ -97,33 +97,33 @@ Section frac_borrow.
       iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
   Qed.
 
-  Lemma frac_borrow_acc E q κ `{Fractional _ Φ} :
+  Lemma frac_bor_acc E q κ `{Fractional _ Φ} :
     ↑lftN ⊆ E →
     lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
   Proof.
-    iIntros (?) "LFT". iApply (frac_borrow_acc_strong with "LFT"). done.
+    iIntros (?) "LFT". iApply (frac_bor_acc_strong with "LFT"). done.
     iIntros "!#*". rewrite fractional. iSplit; auto.
   Qed.
 
-  Lemma frac_borrow_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
+  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_borrow_incl κ κ' q:
+  Lemma frac_bor_incl κ κ' q:
     lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
     iIntros "#LFT#Hbor!#". iSplitR.
     - iIntros (q') "Hκ'".
-      iMod (frac_borrow_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
+      iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
       iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
     - iIntros "H†'".
-      iMod (frac_borrow_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
+      iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
       iDestruct "H" as (q') "[>Hκ' _]".
-      iDestruct (lft_own_dead with "Hκ' H†'") as "[]".
+      iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
   Qed.
 
-End frac_borrow.
+End frac_bor.
 
-Typeclasses Opaque frac_borrow.
+Typeclasses Opaque frac_bor.

theories/tl_borrow.v → theories/lifetime/tl_borrow.v

-From lrust Require Export lifetime.
+From lrust.lifetime Require Export derived.
 From iris.base_logic.lib Require Export thread_local.
 From iris.proofmode Require Import tactics.
 
-Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ}
-           (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
-  (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I.
+Definition tl_bor `{invG Σ, lftG Σ, thread_localG Σ}
+           (κ : lft) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
+  (∃ i, idx_bor κ i P ∗ tl_inv tid N (idx_bor_own 1 i))%I.
 
-Notation "&tl{ κ , tid , N } P" := (tl_borrow κ tid N P)
+Notation "&tl{ κ , tid , N } P" := (tl_bor κ tid N P)
   (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
 
-Section tl_borrow.
-  Context `{invG Σ, lifetimeG Σ, thread_localG Σ}
+Section tl_bor.
+  Context `{invG Σ, lftG Σ, thread_localG Σ}
           (tid : thread_id) (N : namespace) (P : iProp Σ).
 
-  Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ,tid,N} P) := _.
-  Global Instance tl_borrow_proper κ :
-    Proper ((⊣⊢) ==> (⊣⊢)) (tl_borrow κ tid N).
+  Global Instance tl_bor_persistent κ : PersistentP (&tl{κ,tid,N} P) := _.
+  Global Instance tl_bor_proper κ :
+    Proper ((⊣⊢) ==> (⊣⊢)) (tl_bor κ tid N).
   Proof.
     intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
   Qed.
 
-  Lemma borrow_tl κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &tl{κ,tid,N}P.
+  Lemma bor_tl κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &tl{κ,tid,N}P.
   Proof.
-    iIntros (?) "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
+    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "[#? Hown]".
     iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
   Qed.
 
-  Lemma tl_borrow_acc q κ E F :
+  Lemma tl_bor_acc q κ E F :
     ↑lftN ⊆ E → ↑tlN ⊆ E → ↑N ⊆ F →
     lft_ctx -∗ &tl{κ,tid,N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
             ▷P ∗ tl_own tid (F ∖ ↑N) ∗
@@ -35,17 +35,17 @@ Section tl_borrow.
     iIntros (???) "#LFT#HP Hκ Htlown".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
     iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
-    iMod (idx_borrow_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
+    iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
     iIntros "{$HP $Htlown}!>HP Htlown".
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
-  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' -∗ &tl{κ'|tid|N}P -∗ &tl{κ,tid,N}P.
+  Lemma tl_bor_shorten κ κ': κ ⊑ κ' -∗ &tl{κ',tid,N}P -∗ &tl{κ,tid,N}P.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-    iApply (idx_borrow_shorten with "Hκκ' H").
+    iApply (idx_bor_shorten with "Hκκ' H").
   Qed.
 
-End tl_borrow.
+End tl_bor.
 
-Typeclasses Opaque tl_borrow.
+Typeclasses Opaque tl_bor.