Make it possible to specify a namespace for shared borrows.

theories/lifetime/frac_borrow.v

@@ -8,7 +8,7 @@ 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 ∗
+  (∃ γ κ', κ ⊑ κ' ∗ &shr{κ',lftN} ∃ 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.
@@ -60,7 +60,7 @@ Section frac_bor.
                                       ∨ [†κ] ∗ |={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.
+    iMod (shr_bor_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]"; try 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.
@@ -75,7 +75,7 @@ Section frac_bor.
     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.
+    iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try 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.
@@ -90,7 +90,7 @@ Section frac_bor.
       - 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.
+    iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try 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. }

theories/lifetime/shr_borrow.v

@@ -4,42 +4,43 @@ 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.
+(* TODO : update the TEX with the fact that we can chose the namespace. *)
+Definition shr_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
+  (∃ i, &{κ,i}P ∗ inv N (∃ q, idx_bor_own q i))%I.
+Notation "&shr{ κ , N } P" := (shr_bor κ N P)
+  (format "&shr{ κ , N }  P", at level 20, right associativity) : uPred_scope.
 
 Section shared_bors.
-  Context `{invG Σ, lftG Σ} (P : iProp Σ).
+  Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
 
-  Global Instance shr_bor_ne κ n : Proper (dist n ==> dist n) (shr_bor κ).
+  Global Instance shr_bor_ne κ n : Proper (dist n ==> dist n) (shr_bor κ N).
   Proof. solve_proper. Qed.
-  Global Instance shr_bor_contractive κ : Contractive (shr_bor κ).
+  Global Instance shr_bor_contractive κ : Contractive (shr_bor κ N).
   Proof. solve_contractive. Qed.
-  Global Instance shr_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
+  Global Instance shr_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ N).
   Proof. solve_proper. Qed.
 
-  Lemma shr_bor_iff κ P' : ▷ □ (P ↔ P') -∗ &shr{κ} P -∗ &shr{κ} P'.
+  Lemma shr_bor_iff κ P' : ▷ □ (P ↔ P') -∗ &shr{κ, N} P -∗ &shr{κ, N} P'.
   Proof.
     iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
     iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
-  Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.
+  Global Instance shr_bor_persistent : PersistentP (&shr{κ, N} P) := _.
 
-  Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
+  Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ, N}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) ∨
+    ↑lftN ⊆ E → ↑N ⊆ E →
+    lft_ctx -∗ &shr{κ,N}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".
+    iIntros (??) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
+    iInv N 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").
@@ -47,22 +48,22 @@ Section shared_bors.
   Qed.
 
   Lemma shr_bor_acc_tok E q κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
+    ↑lftN ⊆ E → ↑N ⊆ E →
+    lft_ctx -∗ &shr{κ,N}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 (??) "#LFT #Hshr Hκ".
+    iMod (shr_bor_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]"; try 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.
+  Lemma shr_bor_shorten κ κ': κ ⊑ κ' -∗ &shr{κ',N}P -∗ &shr{κ,N}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.
+  Lemma shr_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,N}P.
   Proof.
     iIntros (?) "#LFT#H†". iApply (bor_share with ">"). done.
     by iApply (bor_fake with "LFT H†").