diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index f092b86dfa5f81abfdfa58f3eadd88e4469fb76d..b03b3b3215a345f2404fb6e31bb07c246768ea4e 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -9,7 +9,7 @@ Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
(∃ γ κ', κ ⊑ κ' ∗ &shr{κ',lftN} ∃ q, φ q ∗ own γ q ∗
- (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
+ (⌜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.
@@ -67,10 +67,10 @@ Section frac_bor.
iApply fupd_intro_mask. set_solver. done.
Qed.
- Lemma frac_bor_acc' E q κ :
- ↑lftN ⊆ E →
+ Lemma frac_bor_acc' E F q κ :
+ ↑lftN ⊆ F →
lft_ctx -∗ □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) -∗
- &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
+ &frac{κ}φ -∗ q.[κ,E] ={F}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={F}=∗ q.[κ,E]).
Proof.
iIntros (?) "#LFT #Hφ Hfrac Hκ". unfold frac_bor.
iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
@@ -84,7 +84,8 @@ Section frac_bor.
rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1".
- { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
+ { assert (∅ ⊆ E) as <- by set_solver.
+ iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
- subst. iExists qq. iIntros "{$Hκq}!%".
by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2.
- iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
@@ -107,15 +108,17 @@ Section frac_bor.
{ iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame.
iRight. iExists _. iIntros "{$Hq'qκ}!%".
revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. }
- iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
+ iApply "Hclose". iFrame. iCombine "Hqκ" "Hκqκ0" as "?".
+ rewrite lft_tok_frac_mask Hqκ' (left_id_L ∅). by iFrame.
- iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2".
{ iNext. iExists (qφ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. }
- iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
+ iApply "Hclose". iFrame. iCombine "Hq'κ" "Hκqκ0" as "?".
+ rewrite lft_tok_frac_mask Hqκ' (left_id_L ∅). by iFrame.
Qed.
- Lemma frac_bor_acc E q κ `{Fractional _ φ} :
- ↑lftN ⊆ E →
- lft_ctx -∗ &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
+ Lemma frac_bor_acc E F q κ `{Fractional _ φ} :
+ ↑lftN ⊆ F →
+ lft_ctx -∗ &frac{κ}φ -∗ q.[κ,E] ={F}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={F}=∗ q.[κ,E]).
Proof.
iIntros (?) "LFT". iApply (frac_bor_acc' with "LFT"). done.
iIntros "!#*". rewrite fractional. iSplit; auto.
@@ -139,9 +142,11 @@ Lemma frac_bor_lft_incl `{invG Σ, lftG Σ, frac_borG Σ} κ κ' q:
lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
Proof.
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.
+ - iIntros (q' E) "Hκ'". iDestruct (lft_tok_mask_bound with "Hκ'") as %HE.
+ iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>[Htok1 Htok2] Hclose]". done.
+ iExists _. iSplitL "Htok1"; first by iApply lft_tok_mono; [|done]; set_solver.
+ iIntros "!>Hκ'". iCombine "Htok2" "Hκ'" as "?".
+ rewrite lft_tok_frac_mask Qp_div_2. rewrite <-union_subseteq_l. by iApply "Hclose".
- iIntros "H†'".
iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
iDestruct "H" as (q') "[>Hκ' _]".
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index c4e26967f4f4b997466a2d512e4d8a6d228666f9..73f03a68aea4bfe69de11a33b0f931c6307ceae8 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -20,10 +20,10 @@ Section derived.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
-Lemma bor_acc_cons E q κ P :
- ↑lftN ⊆ E →
- lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
- ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
+Lemma bor_acc_cons E F q κ P :
+ ↑lftN ⊆ F →
+ lft_ctx -∗ &{κ} P -∗ q.[κ,E] ={F}=∗ ▷ P ∗
+ ∀ Q, ▷ Q -∗ ▷(▷ Q ={E}=∗ ▷ P) ={F}=∗ &{κ} Q ∗ q.[κ,E].
Proof.
iIntros (?) "#LFT HP Htok".
iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
@@ -32,9 +32,9 @@ Proof.
- 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.[κ]).
+Lemma bor_acc E F q κ P :
+ ↑lftN ⊆ F →
+ lft_ctx -∗ &{κ}P -∗ q.[κ,E] ={F}=∗ ▷ P ∗ (▷ P ={F}=∗ &{κ}P ∗ q.[κ,E]).
Proof.
iIntros (?) "#LFT HP Htok".
iMod (bor_acc_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
@@ -60,9 +60,9 @@ Proof.
- iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
Qed.
-Lemma bor_later_tok E q κ P :
- ↑lftN ⊆ E →
- lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
+Lemma bor_later_tok E F q κ P :
+ ↑lftN ⊆ F →
+ lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ,E] ={F}▷=∗ &{κ}P ∗ q.[κ,E].
Proof.
iIntros (?) "#LFT Hb Htok".
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose]"; first done.
@@ -79,9 +79,9 @@ Proof.
- iMod "Hclose" as "_". auto.
Qed.
-Lemma bor_persistent_tok P `{!PersistentP P} E κ q :
- ↑lftN ⊆ E →
- lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
+Lemma bor_persistent_tok P `{!PersistentP P} E F κ q :
+ ↑lftN ⊆ F →
+ lft_ctx -∗ &{κ}P -∗ q.[κ,E] ={F}=∗ ▷ P ∗ q.[κ,E].
Proof.
iIntros (?) "#LFT Hb Htok".
iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
@@ -91,7 +91,8 @@ Qed.
Lemma lft_incl_static κ : (κ ⊑ static)%I.
Proof.
iApply lft_incl_intro. iIntros "!#". iSplitR.
- - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
+ - iIntros (q E) "H". iDestruct (lft_tok_mask_bound with "H") as %?.
+ iExists 1%Qp. iSplitR; [iApply lft_tok_static|]; auto with iFrame.
- iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
Qed.
End derived.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 4684b65d115f0ae967368e629234dcd33e5d3632..85c3028851438612f2ad41b5269fe7a6c046f7ab 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -26,7 +26,7 @@ Module Type lifetime_sig.
(** Definitions *)
Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
- Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
+ Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft) (E : coPset), iProp Σ.
Parameter lft_dead : ∀ `{lftG Σ} (κ : lft), iProp Σ.
Parameter lft_incl : ∀ `{invG, lftG Σ} (κ κ' : lft), iProp Σ.
@@ -37,8 +37,10 @@ Module Type lifetime_sig.
Parameter idx_bor : ∀ `{invG, lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
(** Notation *)
- Notation "q .[ κ ]" := (lft_tok q κ)
- (format "q .[ κ ]", at level 0) : uPred_scope.
+ Notation "q .[ κ , E ]" := (lft_tok q κ E)
+ (format "q .[ κ , E ]", at level 0) : uPred_scope.
+ Notation "q .[ κ ]" := (lft_tok q κ (⊤ ∖ ↑lftN))
+ (format "q .[ κ ]", at level 0) : uPred_scope.
Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
Notation "&{ κ } P" := (bor κ P)
@@ -57,7 +59,11 @@ Module Type lifetime_sig.
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_tok_mono q κ :
+ Proper (flip (⊆) ==> (⊢)) (lft_tok q κ).
+ Global Declare Instance lft_tok_mono_flip q κ :
+ Proper ((⊆) ==> flip (⊢)) (lft_tok q κ).
+ Global Declare Instance lft_tok_timeless q κ E : TimelessP (lft_tok q κ E).
Global Declare Instance lft_dead_timeless κ : TimelessP (lft_dead κ).
Global Declare Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
@@ -71,22 +77,26 @@ Module Type lifetime_sig.
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 lft_tok_fractional κ E : Fractional (λ q, q.[κ,E])%I.
+ Global Declare Instance lft_tok_as_fractional κ q E :
+ AsFractional q.[κ,E] (λ q, q.[κ,E])%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_tok_sep :
+ ∀ q κ1 κ2 E, q.[κ1,E] ∗ q.[κ2,E] ⊣⊢ q.[κ1 ∪ κ2,E].
+ Parameter lft_tok_frac_mask :
+ ∀ q1 q2 κ E1 E2, q1.[κ,E1] ∗ q2.[κ,E2] ⊢ (q1 + q2).[κ, E1 ∪ E2].
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_tok_dead : ∀ q κ E, q.[κ,E] -∗ [† κ] -∗ False.
+ Parameter lft_tok_static : ∀ q E, E ⊥ ↑lftN → q.[static,E]%I.
Parameter lft_dead_static : [† static] -∗ False.
+ Parameter lft_tok_mask_bound : ∀ q κ E, q.[κ,E] -∗ ⌜E ⊥ ↑lftN⌝.
- Parameter lft_create : ∀ E, ↑lftN ⊆ E →
- lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
+ Parameter lft_create : ∀ E F, ↑lftN ⊆ E → ↑lftN ⊆ F →
+ lft_ctx ={F}=∗ ∃ κ, 1.[κ,E∖↑lftN] ∗ □ (∀ E', 1.[κ,E'] ={E,E∖↑lftN}▷=∗ [†κ]).
Parameter bor_create : ∀ E κ P,
↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
Parameter bor_fake : ∀ E κ P,
@@ -110,45 +120,48 @@ Module Type lifetime_sig.
Parameter idx_bor_shorten : ∀ κ κ' i P, κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
Parameter idx_bor_iff : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}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_acc : ∀ E F q κ i P, ↑lftN ⊆ E →
+ lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ,F] ={E}=∗
+ ▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ,F]).
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_strong : ∀ E F q κ P, ↑lftN ⊆ F →
+ lft_ctx -∗ &{κ} P -∗ q.[κ,E] ={F}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
+ ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={E}=∗ ▷ P) ={F}=∗ &{κ'} Q ∗ q.[κ,E].
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) ∨
+ ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ==∗ ▷ 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_glb_acc : ∀ κ κ' q q', q.[κ] -∗ q'.[κ'] -∗
- ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
+ (* 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_tok_combine : ∀ q κ1 κ2 E1 E2,
+ q.[κ1,E1] ∗ q.[κ2,E2] ⊢ q.[κ1 ∪ κ2, E1 ∩ E2].
+ Parameter lft_glb_acc : ∀ κ κ' q q' E, q.[κ,E] -∗ q'.[κ',E] -∗
+ ∃ q'', q''.[κ ∪ κ', E] ∗ (q''.[κ ∪ κ', E] -∗ q.[κ,E] ∗ q'.[κ',E]).
Parameter lft_le_incl : ∀ κ κ', κ' ⊆ κ → (κ ⊑ κ')%I.
Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
Parameter lft_glb_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_acc : ∀ E F κ κ' q, ↑lftN ⊆ E →
+ κ ⊑ κ' -∗ q.[κ,F] ={E}=∗ ∃ q', q'.[κ',F] ∗ (q'.[κ',F] ={E}=∗ q.[κ,F]).
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 κ)) -∗ κ ⊑ κ'.
+ □ ((∀ q E, q.[κ,E] ={↑lftN}=∗ ∃ q',
+ q'.[κ',E] ∗ (q'.[κ',E] ={↑lftN}=∗ q.[κ,E])) ∗
+ ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
(* 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) ∨
+ (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ==∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
([†κ] ∗ |={E∖↑lftN,E}=> True).
Parameter bor_acc_atomic : ∀ E κ P,
↑lftN ⊆ E → lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index b3b74823938427a48cd96861012214619dc76eb7..ce3737c6eb55e4170ddfc598cfaa44059fe580a8 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -10,10 +10,10 @@ Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
(* Helper internal lemmas *)
-Lemma bor_open_internal E P i Pb q :
+Lemma bor_open_internal E F P i Pb q :
↑borN ⊆ E →
slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗
- idx_bor_own 1%Qp i -∗ (q).[i.1] ={E}=∗
+ idx_bor_own 1%Qp i -∗ (q).[i.1,F] ={E}=∗
▷ lft_bor_alive (i.1) Pb ∗
own_bor (i.1) (◯ {[i.2 := (1%Qp, to_agree (Bor_open q))]}) ∗ ▷ P.
Proof.
@@ -30,14 +30,14 @@ Proof.
rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
iExists _. iFrame "∗".
rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete /=; last done.
- iDestruct "HB" as "[_ $]". auto.
+ iDestruct "HB" as "[_ $]". iApply lft_tok_mono; last done. by intros ?.
Qed.
Lemma bor_close_internal E P i Pb q :
↑borN ⊆ E →
slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗
own_bor (i.1) (◯ {[i.2 := (1%Qp, to_agree (Bor_open q))]}) -∗ ▷ P ={E}=∗
- ▷ lft_bor_alive (i.1) Pb ∗ idx_bor_own 1%Qp i ∗ (q).[i.1].
+ ▷ lft_bor_alive (i.1) Pb ∗ idx_bor_own 1%Qp i ∗ (q).[i.1,∅].
Proof.
iIntros (?) "Hslice Halive Hbor HP". unfold lft_bor_alive, idx_bor_own.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
@@ -55,28 +55,30 @@ Proof.
rewrite -insert_delete big_sepM_insert ?lookup_delete //. simpl. by iFrame.
Qed.
-Lemma add_vs Pb Pb' P Q Pi κ :
- ▷ ▷ (Pb ≡ (P ∗ Pb')) -∗ ▷ lft_vs κ Pb Pi -∗ ▷ (▷ Q -∗ [†κ] ={⊤∖↑lftN}=∗ ▷ P) -∗
- ▷ lft_vs κ (Q ∗ Pb') Pi.
+Lemma add_vs E Pb Pb' P Q Pi A κ :
+ (∀ Λ b EΛ, Λ ∈ κ → A !! Λ = Some (b, EΛ) → E ⊆ EΛ) →
+ ▷ ▷ (Pb ≡ (P ∗ Pb')) -∗ ▷ lft_vs A κ Pb Pi -∗ ▷ (▷ Q -∗ [†κ] ={E}=∗ ▷ P) -∗
+ ▷ lft_vs A κ (Q ∗ Pb') Pi.
Proof.
- iIntros "#HEQ Hvs HvsQ". iNext. rewrite !lft_vs_unfold.
+ iIntros (HE) "#HEQ Hvs HvsQ". iNext. rewrite !lft_vs_unfold.
iDestruct "Hvs" as (n) "[Hcnt Hvs]". iExists n.
- iIntros "{$Hcnt}*Hinv[HQ HPb] #H†". iApply fupd_trans.
- iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP". solve_ndisj.
+ iIntros "{$Hcnt} * % Hinv [HQ HPb] #H†". iApply fupd_trans.
+ iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP".
+ { etrans; last by apply union_subseteq_l. auto. }
iModIntro. iAssert (▷ Pb)%I with "[HPb HP]" as "HPb".
{ iNext. iRewrite "HEQ". iFrame. }
- iApply ("Hvs" with "Hinv HPb H†").
+ by iApply ("Hvs" with "[%] Hinv HPb H†").
Qed.
(** Indexed borrow *)
-Lemma idx_bor_acc E q κ i P :
+Lemma idx_bor_acc E F 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.[κ]).
+ lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ,F] ={E}=∗
+ ▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ,F]).
Proof.
unfold idx_bor. iIntros (HE) "#LFT [#Hle #Hs] Hbor Htok".
iDestruct "Hs" as (P') "[#HPP' Hs]".
- iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
+ iMod (lft_incl_acc with "Hle Htok") as (q') "[[Htok HtokE] Hclose]". solve_ndisj.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -86,7 +88,7 @@ Proof.
iMod (bor_open_internal with "Hs Halive Hbor Htok") as "(Halive & Hf & HP')".
solve_ndisj.
iDestruct ("HPP'" with "HP'") as "$".
- iMod ("Hclose'" with "[-Hf Hclose]") as "_".
+ iMod ("Hclose'" with "[-Hf Hclose HtokE]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
iIntros "!>HP'". iDestruct ("HPP'" with "HP'") as "HP". clear -HE.
@@ -99,6 +101,8 @@ Proof.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iMod (bor_close_internal with "Hs Halive Hf HP") as "(Halive & $ & Htok)".
solve_ndisj.
+ iCombine "Htok" "HtokE" as "Htok".
+ rewrite lft_tok_frac_mask Qp_div_2 (left_id_L ∅).
iMod ("Hclose'" with "[-Htok Hclose]") as "_"; last by iApply "Hclose".
iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame.
@@ -149,28 +153,28 @@ Qed.
(** Basic borrows *)
-Lemma bor_acc_strong E q κ P :
- ↑lftN ⊆ E →
- lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
- ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
+Lemma bor_acc_strong E F q κ P :
+ ↑lftN ⊆ F →
+ lft_ctx -∗ &{κ} P -∗ q.[κ,E] ={F}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
+ ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={E}=∗ ▷ P) ={F}=∗ &{κ'} Q ∗ q.[κ,E].
Proof.
- unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
+ unfold bor, raw_bor. iIntros (HF) "#LFT Hbor Htok".
iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
iDestruct "Hs" as (P') "[#HPP' Hs]".
- iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
+ iMod (lft_incl_acc with "Hle Htok") as (q') "[[Htok HtokE] Hclose]". solve_ndisj.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
- iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
- iMod (bor_open_internal _ _ (κ'', s'') with "Hs Halive Hbor Htok")
+ iMod (bor_open_internal _ _ _ (κ'', s'') with "Hs Halive Hbor Htok")
as "(Halive & Hbor & HP')". solve_ndisj.
iDestruct ("HPP'" with "HP'") as "$".
- iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
+ iMod ("Hclose'" with "[-Hbor Hclose HtokE]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
- iExists κ''. iFrame "#". iIntros "!>*HQ HvsQ". clear -HE.
+ iExists κ''. iFrame "#". iIntros "!>*HQ HvsQ". clear -HF.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -183,26 +187,34 @@ Proof.
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
iMod (slice_delete_empty _ _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
- iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
+ iAssert (⌜∀ Λ b EΛ, Λ ∈ κ'' → A !! Λ = Some (b, EΛ) → E ⊆ EΛ⌝)%I
+ with "[HtokE HA]" as %HE.
+ { iIntros (Λ b EΛ Hκ'' HΛ). unfold lft_tok. iDestruct "HtokE" as "[_ HtokE]".
+ iDestruct (big_sepMS_elem_of _ κ'' _ Hκ'' with "HtokE") as (E') "[% HE']".
+ iDestruct (own_alft_auth_agree with "HA HE'") as %HAE'.
+ iPureIntro. rewrite HΛ in HAE'. naive_solver. }
+ iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs"; first done.
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_empty _ _ true with "Hbox") as (j) "(% & #Hs' & Hbox)".
iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
{ apply auth_update. etrans.
- apply delete_singleton_local_update, _.
- apply (alloc_singleton_local_update _ j
- (1%Qp, to_agree (Bor_open q'))); last done.
+ (1%Qp, to_agree (Bor_open (q' / 2)))); last done.
rewrite -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //. }
rewrite own_bor_op. iDestruct "Hown" as "[Hown Hbor]".
iMod (bor_close_internal _ _ (_, _) with "Hs' [Hbox Hown HB] Hbor HQ")
as "(Halive & Hbor & Htok)". solve_ndisj.
- { rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ (Bor_open q'))
+ { rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ (Bor_open (q' / 2)))
/lft_bor_alive. iExists _. iFrame "Hbox Hown".
- rewrite big_sepM_insert. by rewrite big_sepM_delete.
+ rewrite big_sepM_insert. simpl. by rewrite big_sepM_delete // => //=.
by rewrite -fmap_None -lookup_fmap fmap_delete. }
- iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
+ iMod ("Hclose'" with "[-Hbor Htok Hclose HtokE]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
+ iCombine "Htok" "HtokE" as "Htok".
+ rewrite lft_tok_frac_mask Qp_div_2 (left_id_L ∅).
iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
iSplit; first by iApply lft_incl_refl. iExists j. iFrame.
iExists Q. rewrite -uPred.iff_refl. eauto.
@@ -219,7 +231,7 @@ Lemma bor_acc_atomic_strong E κ P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
(∃ κ', κ ⊑ κ' ∗ ▷ P ∗
- ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+ ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ==∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
([†κ] ∗ |={E∖↑lftN,E}=> True).
Proof.
iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
@@ -239,7 +251,8 @@ Proof.
iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
iMod fupd_intro_mask' as "Hclose"; last iIntros "!>*HQ HvsQ". solve_ndisj.
- iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
+ iMod "Hclose" as "_". iDestruct (add_vs ∅ with "EQ Hvs [HvsQ]") as "Hvs".
+ { set_solver+. }
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
solve_ndisj.
@@ -270,7 +283,7 @@ Qed.
Lemma bor_acc_atomic_cons E κ P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
- (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+ (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ==∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
([†κ] ∗ |={E∖↑lftN,E}=> True).
Proof.
iIntros (?) "#LFT HP".
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 77e8b58838c19d1e037370566254aca845dadee1..8180802b15b26d0f6913306a3f1713304326035c 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -51,10 +51,11 @@ Proof.
iDestruct ("HIlookup" with "HI") 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Λ.
- rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
- { unfold lft_alive_in in *. naive_solver. }
+ rewrite /lft_dead; iDestruct "H†" as (Λ E') "[% #H†]".
+ iDestruct (own_alft_auth_agree A Λ with "HA H†") as %EQAΛ.
+ rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >H]|[Hinv >%]]".
+ { iDestruct "H" as %(E'' & HE''); first done.
+ eapply eq_trans in HE''; last by symmetry; apply EQAΛ. done. }
rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & >Hcnt & Hinh)".
iMod ("Hinh_close" $! Pinh with "Hinh") as (Pinh') "(? & $ & ?)".
iApply "Hclose". iExists A, I. iFrame. iNext. iApply "Hclose'".
@@ -88,9 +89,9 @@ Proof.
iMod (slice_iff _ _ true with "HPP' Hslice Hbox")
as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
{ by rewrite lookup_fmap EQB. }
- iAssert (▷ lft_vs κ' Pb' Pi)%I with "[Hvs]" as "Hvs".
- { iNext. iApply (lft_vs_cons false with "[] Hvs"). iIntros "[$ ?]!>".
- by iApply "HPbPb'". }
+ iAssert (▷ lft_vs A κ' Pb' Pi)%I with "[Hvs]" as "Hvs".
+ { iNext. iApply (lft_vs_cons ∅ false with "[] Hvs"); first set_solver+.
+ iIntros "[$ ?]!>". by iApply "HPbPb'". }
iMod (slice_split _ _ true with "Hslice Hbox")
as (γ1 γ2) "(Hγ1 & Hγ2 & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
{ by rewrite lookup_insert. }
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index e731f97ab0cbfbc106d5c67f765bd5a958e7265c..6b3bff93487c8d2d2baddb4e026d6fc97c916ff5 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -10,16 +10,18 @@ Section creation.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
-Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
+Lemma lft_kill (I : gmap lft lft_names) (A : gmap atomic_lft (bool * coPset))
+ (K K' : gset lft) (κ : lft) (E : coPset):
let Iinv := (
own_ilft_auth I ∗
- ([∗ set] κ' ∈ K, lft_inv_alive κ') ∗
+ ([∗ set] κ' ∈ K, lft_inv_alive A κ') ∗
([∗ set] κ' ∈ K', lft_inv_dead κ'))%I in
+ (∀ E', (∀ Λ b EΛ, Λ ∈ κ → A !! Λ = Some (b, EΛ) → E' ⊆ EΛ) → E' ⊆ E) →
(∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K) →
(∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K') →
- Iinv -∗ lft_inv_alive κ -∗ [†κ] ={⊤∖↑mgmtN}=∗ Iinv ∗ lft_inv_dead κ.
+ Iinv -∗ lft_inv_alive A κ -∗ [†κ] ={E ∪ ↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
Proof.
- iIntros (Iinv HK HK') "(HI & Halive & Hdead) Hlalive Hκ".
+ iIntros (Iinv HE HK HK') "(HI & Halive & Hdead) Hlalive Hκ".
rewrite lft_inv_alive_unfold;
iDestruct "Hlalive" as (P Q) "(Hbor & Hvs & Hinh)".
rewrite /lft_bor_alive; iDestruct "Hbor" as (B) "(Hbox & Hbor & HB)".
@@ -34,36 +36,39 @@ 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 with "Hbox") as "[HP Hbox]"=>//; first solve_ndisj.
+ iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
{ intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
iDestruct (big_sepS_filter_acc (⊂ κ) _ _ (dom _ I) with "Halive")
as "[Halive Halive']".
{ intros κ'. rewrite elem_of_dom. eauto. }
- iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
+ iApply fupd_trans. iApply fupd_mask_mono; first apply union_subseteq_l.
+ iMod ("Hvs" $! I E with "[] [HI Halive Hbox Hbor] HP Hκ")
+ as "(Hinv & HQ & Hcnt')"; first done.
{ rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
iExists (dom _ B), P. rewrite !to_gmap_dom -map_fmap_compose.
rewrite (map_fmap_ext _ ((1%Qp,) ∘ to_agree) B); last naive_solver.
iFrame. }
rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
- iSpecialize ("Halive'" with "Halive").
+ iModIntro. iSpecialize ("Halive'" with "Halive").
iMod (own_cnt_update_2 with "Hcnt Hcnt'") as "?".
{ apply auth_update_dealloc, (nat_local_update _ _ 0 0); omega. }
rewrite /Iinv. iFrame "Hdead Halive' HI".
- iMod (lft_inh_kill with "[$Hinh $HQ]"); first solve_ndisj.
+ iMod (lft_inh_kill with "[$Hinh $HQ]"); first set_solver+.
iModIntro. rewrite /lft_inv_dead. iExists Q. by iFrame.
Qed.
-Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
- let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in
+Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) (E : coPset):
+ let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive A κ')%I in
+ (∀ E' κ, κ ∈ K → (∀ Λ b EΛ, Λ ∈ κ → A !! Λ = Some (b, EΛ) → E' ⊆ EΛ) → E' ⊆ E) →
(∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
(∀ κ κ', κ ∈ K → lft_alive_in A κ → is_Some (I !! κ') →
κ' ∉ K → κ' ⊂ κ → κ' ∈ K') →
Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
- ={⊤∖↑mgmtN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
+ ={E ∪ ↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
Proof.
intros Iinv. revert K'.
- induction (collection_wf K) as [K _ IH]=> K' HK HK'.
+ induction (collection_wf K) as [K _ IH]=> K' HE HK HK'.
iIntros "[HI Halive] HK".
pose (Kalive := filter (lft_alive_in A) K).
destruct (decide (Kalive = ∅)) as [HKalive|].
@@ -75,10 +80,11 @@ Proof.
iDestruct (@big_sepS_delete with "HK") as "[[Hκinv Hκ] HK]"; first done.
iDestruct (lft_inv_alive_in with "Hκinv") as "Hκalive"; first done.
iAssert ⌜κ ∉ K'⌝%I with "[#]" as %HκK'.
- { iIntros (Hκ). iApply (lft_inv_alive_twice κ with "Hκalive").
+ { iIntros (Hκ). iApply (lft_inv_alive_twice A κ with "Hκalive").
by iApply (@big_sepS_elem_of with "Halive"). }
specialize (IH (K ∖ {[ κ ]})). feed specialize IH; [set_solver +HκK|].
iMod (IH ({[ κ ]} ∪ K') with "[HI Halive Hκalive] HK") as "[[HI Halive] Hdead]".
+ { intros ?? Hκ ?. eapply HE; last done. set_solver+Hκ. }
{ intros κ' κ''.
rewrite !elem_of_difference !elem_of_singleton=> -[? Hneq] ??.
split; [by eauto|]; intros ->.
@@ -92,7 +98,7 @@ Proof.
{ rewrite /Iinv big_sepS_insert //. iFrame. }
iDestruct (@big_sepS_insert with "Halive") as "[Hκalive Halive]"; first done.
iMod (lft_kill with "[$HI $Halive $Hdead] Hκalive Hκ")
- as "[(HI&Halive&Hdead) Hκdead]".
+ as "[(HI&Halive&Hdead) Hκdead]"; first by eauto.
{ intros κ' ??. eapply (HK' κ); eauto.
intros ?. eapply (minimal_strict_1 _ _ _ Hκmin); eauto.
apply elem_of_filter; split; last done.
@@ -110,7 +116,7 @@ Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
Lemma kill_set_subseteq I Λ : kill_set I Λ ⊆ dom (gset lft) I.
Proof. intros κ [??]%elem_of_kill_set. by apply elem_of_dom. Qed.
-Definition down_close (A : gmap atomic_lft bool)
+Definition down_close (A : gmap atomic_lft (bool * coPset))
(I : gmap lft lft_names) (K : gset lft) : gset lft :=
filter (λ κ, κ ∉ K ∧
set_Exists (λ κ', κ ⊂ κ' ∧ lft_alive_in A κ') K) (dom (gset lft) I).
@@ -130,76 +136,98 @@ Lemma down_close_subseteq A I K :
down_close A I K ⊆ dom (gset lft) I.
Proof. intros κ [??]%elem_of_down_close. by apply elem_of_dom. Qed.
-Lemma lft_create E :
- ↑lftN ⊆ E →
- lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
+Lemma lft_create E F :
+ ↑lftN ⊆ E → ↑lftN ⊆ F →
+ lft_ctx ={F}=∗ ∃ κ, 1.[κ,E∖↑lftN] ∗ □ (∀ E', 1.[κ,E'] ={E,E∖↑lftN}▷=∗ [†κ]).
Proof.
- iIntros (?) "#LFT".
+ iIntros (??) "#LFT".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
destruct (exist_fresh (dom (gset _) A)) as [Λ HΛ%not_elem_of_dom].
iMod (own_update with "HA") as "[HA HΛ]".
- { apply auth_update_alloc, (alloc_singleton_local_update _ Λ (Cinl 1%Qp))=>//.
+ { apply auth_update_alloc,
+ (alloc_singleton_local_update _ Λ (Some (Cinl 1%Qp), to_agree (E∖↑lftN)))=>//.
by rewrite lookup_fmap HΛ. }
iMod ("Hclose" with "[HA HI Hinv]") as "_".
{ iNext. rewrite /lfts_inv /own_alft_auth.
- iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
+ iExists (<[Λ:=(true, _)]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
iApply (@big_sepS_impl with "[$Hinv]").
iAlways. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
- - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
+ - iLeft. rewrite lft_inv_alive_insert //. iFrame "Hκ".
+ iPureIntro. by apply lft_alive_in_insert.
- iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
- iModIntro; iExists {[ Λ ]}.
- rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
- clear I A HΛ. iIntros "!# HΛ".
- iApply (step_fupd_mask_mono ⊤ _ _ (⊤∖↑mgmtN)); [solve_ndisj..|].
+ iAssert (own alft_name (◯ {[Λ := (None, to_agree (E∖↑lftN))]})) as "#HE".
+ { rewrite -{1}(agree_idemp (to_agree _)) -(right_id None _ (Some _)) -pair_op
+ -op_singleton auth_frag_op own_op.
+ iDestruct "HΛ" as "[_ $]". }
+ iModIntro; iExists {[ Λ ]}. iSplitL.
+ { rewrite {1}/lft_tok big_sepMS_singleton. iSplit; first by iPureIntro; set_solver.
+ iExists _. iIntros "{$HΛ} !%". set_solver. }
+ clear I A HΛ. rewrite /lft_tok. iIntros "!# * [_ HΛ]".
+ iApply (step_fupd_mask_mono E _ _ (E∖↑mgmtN)); [solve_ndisj..|].
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
- rewrite /lft_tok big_sepMS_singleton.
+ rewrite big_sepMS_singleton. iDestruct "HΛ" as (E'') "[% HΛ]".
iDestruct (own_valid_2 with "HA HΛ")
- as %[[s [?%leibniz_equiv ?]]%singleton_included _]%auth_valid_discrete_2.
+ as %[[s [Hs Hincl]]%singleton_included Hv]%auth_valid_discrete_2.
+ specialize (Hv Λ). revert Hs Hv.
+ case EQs' : (to_alftUR A !! Λ) => [[]|]; inversion_clear 1=>-[/= _ Hv]. setoid_subst.
+ move: Hincl => /Some_included_total /prod_included /= [/option_included Hincl1 Hincl2].
+ destruct Hincl1 as [[=]|(?&?&[=?]&?&?)]. subst.
+ apply to_agree_uninj in Hv. destruct Hv as [? EQag]. rewrite <-EQag in Hincl2.
+ apply to_agree_included, leibniz_equiv in Hincl2. subst x.
+ iDestruct (own_valid_2 with "HE HΛ") as %Hv. rewrite -auth_frag_op op_singleton in Hv.
+ apply singleton_valid, proj2, to_agree_comp_valid, leibniz_equiv in Hv. subst.
iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
- { by eapply auth_update, singleton_local_update,
- (exclusive_local_update _ (Cinr ())). }
+ { by eapply auth_update, singleton_local_update, prod_local_update_1,
+ option_local_update, (exclusive_local_update _ (Cinr ())). }
iDestruct "HΛ" as "#HΛ". iModIntro; iNext.
pose (K := kill_set I Λ); pose (K' := down_close A I K).
assert (K ⊥ K') by (by apply down_close_disjoint).
- destruct (proj1 (subseteq_disjoint_union_L (K ∪ K')
- (dom (gset lft) I))) as (K''&HI&?).
+ destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom (gset lft) I))) as (K''&HI&HK'').
{ apply union_least. apply kill_set_subseteq. apply down_close_subseteq. }
rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[[HinvK HinvD] Hinv]".
- iAssert ([∗ set] κ ∈ K', lft_inv_alive κ)%I with "[HinvD]" as "HinvD".
+ iAssert ([∗ set] κ ∈ K', lft_inv_alive A κ)%I with "[HinvD]" as "HinvD".
{ iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
iIntros (κ Hκ) "?". iApply lft_inv_alive_in; last done.
eauto using down_close_lft_alive_in. }
- iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK".
+ iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK".
{ iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
+ iApply fupd_trans. iApply (fupd_mask_mono ((E ∖ ↑lftN) ∪ ↑borN ∪ ↑inhN)).
+ { repeat apply union_least; solve_ndisj. }
iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
+ { intros F' κ Hκ HF'. specialize (HF' Λ).
+ rewrite lookup_fmap in EQs'. destruct (A!!Λ) as [[]|]; try done.
+ injection EQs'=>? ?. subst. apply (inj to_agree), leibniz_equiv in EQag. subst.
+ by eapply HF'; first eapply elem_of_kill_set. }
{ intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
split; last done. by eapply gmultiset_elem_of_subseteq. }
{ intros κ κ' ?????. apply elem_of_down_close; eauto 10. }
- iMod ("Hclose" with "[-]") as "_"; last first.
- { iModIntro. rewrite /lft_dead. iExists Λ.
+ iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
+ { iModIntro. rewrite /lft_dead. iExists Λ, _.
rewrite elem_of_singleton. auto. }
- iNext. iExists (<[Λ:=false]>A), I.
- rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
+ iNext. iExists (<[Λ:=(false, _)]>A), I.
+ rewrite /own_alft_auth /to_alftUR fmap_insert -EQag. iFrame "HA HI".
rewrite HI !big_sepS_union //.
iSplitL "HinvK HinvD"; first iSplitL "HinvK".
- iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
iIntros (κ [? _]%elem_of_kill_set) "Hdead". rewrite /lft_inv.
- iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false'.
+ iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_None'.
- iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
iIntros (κ Hκ) "Halive". rewrite /lft_inv.
- iLeft. iFrame "Halive". iPureIntro.
+ assert (Λ ∉ κ).
+ { apply elem_of_down_close in Hκ as (?&HFOO&_).
+ move: HFOO. rewrite elem_of_kill_set. tauto. }
+ iLeft. rewrite lft_inv_alive_insert_notin //. iFrame "Halive". iPureIntro.
assert (lft_alive_in A κ) as Halive by (by eapply down_close_lft_alive_in).
- apply lft_alive_in_insert_false; last done.
- apply elem_of_down_close in Hκ as (?&HFOO&_).
- move: HFOO. rewrite elem_of_kill_set. tauto.
+ by apply lft_alive_in_insert_notin.
- iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!#".
rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
- + iLeft. iFrame. iPureIntro.
- apply lft_alive_in_insert_false; last done.
- assert (κ ∉ K). intros ?. eapply H5. 2: eauto. rewrite elem_of_union. eauto.
- move: H7. rewrite elem_of_kill_set not_and_l. intros [?|?]. done.
- contradict H7. apply elem_of_dom. set_solver +HI Hκ.
- + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
+ + assert (Λ ∉ κ).
+ { have:(κ ∉ K). { intros HK. eapply HK''; [rewrite elem_of_union|]; eauto. }
+ rewrite elem_of_kill_set not_and_l. intros [|HΛ]; first done.
+ contradict HΛ. apply elem_of_dom. set_solver +HI Hκ. }
+ iLeft. rewrite lft_inv_alive_insert_notin //. iFrame. iPureIntro.
+ by apply lft_alive_in_insert_notin.
+ + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_None.
Qed.
End creation.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index e4a59714b23349a25ad148a55d42fefa7eb24b3a..63915eb8bc227f0e320f7d30d8887bdf33203c1d 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -22,8 +22,9 @@ Record lft_names := LftNames {
Instance lft_names_eq_dec : EqDecision lft_names.
Proof. solve_decision. Defined.
Canonical lft_namesC := leibnizC lft_names.
+Canonical coPsetC := leibnizC coPset.
-Definition lft_stateR := csumR fracR unitR.
+Definition lft_stateR := prodR (optionR (csumR fracR unitR)) (agreeR coPsetC).
Definition alftUR := gmapUR atomic_lft lft_stateR.
Definition ilftUR := gmapUR lft (agreeR lft_namesC).
Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
@@ -61,23 +62,27 @@ Proof. solve_inG. Qed.
Definition bor_filled (s : bor_state) : bool :=
match s with Bor_in => true | _ => false end.
-Definition to_lft_stateR (b : bool) : lft_stateR :=
- if b then Cinl 1%Qp else Cinr ().
-Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
+Definition to_lft_stateR (x : bool * coPset) : lft_stateR :=
+ (Some (if x.1 then Cinl 1%Qp else Cinr ()), to_agree (x.2)).
+Definition to_alftUR : gmap atomic_lft (bool * coPset) → alftUR :=
+ fmap to_lft_stateR.
Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
-Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
-
+Definition to_borUR : gmap slice_name bor_state → borUR :=
+ fmap ((1%Qp,) ∘ to_agree).
Section defs.
Context `{invG Σ, lftG Σ}.
- Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
- ([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
+ Definition lft_tok (q : Qp) (κ : lft) (E : coPset) : iProp Σ :=
+ (⌜E ⊥ ↑lftN⌝ ∗
+ [∗ mset] Λ ∈ κ,
+ ∃ E', ⌜E ⊆ E'⌝ ∗
+ own alft_name (◯ {[ Λ := (Some (Cinl q), to_agree E') ]}))%I.
Definition lft_dead (κ : lft) : iProp Σ :=
- (∃ Λ, ⌜Λ ∈ κ⌝ ∗ own alft_name (◯ {[ Λ := Cinr () ]}))%I.
+ (∃ Λ E, ⌜Λ ∈ κ⌝ ∗ own alft_name (◯ {[ Λ := (Some (Cinr ()), to_agree E) ]}))%I.
- Definition own_alft_auth (A : gmap atomic_lft bool) : iProp Σ :=
+ Definition own_alft_auth (A : gmap atomic_lft (bool * coPset)) : iProp Σ :=
own alft_name (● to_alftUR A).
Definition own_ilft_auth (I : gmap lft lft_names) : iProp Σ :=
own ilft_name (● to_ilftUR I).
@@ -101,7 +106,7 @@ Section defs.
Definition bor_cnt (κ : lft) (s : bor_state) : iProp Σ :=
match s with
| Bor_in => True
- | Bor_open q => lft_tok q κ
+ | Bor_open q => lft_tok q κ ∅
| Bor_rebor κ' => ⌜κ ⊂ κ'⌝ ∗ own_cnt κ' (◯ 1)
end%I.
@@ -121,34 +126,39 @@ Section defs.
own_inh κ (● GSet E) ∗
box inhN (to_gmap s E) Pi)%I.
- Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
- (I : gmap lft lft_names) : iProp Σ :=
- (lft_bor_dead κ ∗
- own_ilft_auth I ∗
- [∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
-
- Definition lft_vs_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
- (Pb Pi : iProp Σ) : iProp Σ :=
- (∃ n : nat,
- own_cnt κ (● n) ∗
- ∀ I : gmap lft lft_names,
- lft_vs_inv_go κ lft_inv_alive I -∗ ▷ Pb -∗ lft_dead κ
- ={⊤∖↑mgmtN}=∗
- lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I.
-
- Definition lft_inv_alive_go (κ : lft)
- (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ) : iProp Σ :=
- (∃ Pb Pi,
- lft_bor_alive κ Pb ∗
- lft_vs_go κ lft_inv_alive Pb Pi ∗
- lft_inh κ false Pi)%I.
-
- Definition lft_inv_alive (κ : lft) : iProp Σ :=
- Fix_F _ lft_inv_alive_go (gmultiset_wf κ).
- Definition lft_vs_inv (κ : lft) (I : gmap lft lft_names) : iProp Σ :=
- lft_vs_inv_go κ (λ κ' _, lft_inv_alive κ') I.
- Definition lft_vs (κ : lft) (Pb Pi : iProp Σ) : iProp Σ :=
- lft_vs_go κ (λ κ' _, lft_inv_alive κ') Pb Pi.
+ Section lft_inv_alive.
+ Context (A : gmap atomic_lft (bool * coPset))
+ (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ).
+
+ Definition lft_vs_inv_go (I : gmap lft lft_names) : iProp Σ :=
+ (lft_bor_dead κ ∗
+ own_ilft_auth I ∗
+ [∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
+
+ Definition lft_vs_go (Pb Pi : iProp Σ) : iProp Σ :=
+ (∃ n : nat,
+ own_cnt κ (● n) ∗
+ ∀ (I : gmap lft lft_names) E,
+ ⌜∀ E', (∀ Λ b EΛ, Λ ∈ κ → A !! Λ = Some (b, EΛ) → E' ⊆ EΛ) → E' ⊆ E⌝ -∗
+ lft_vs_inv_go I -∗ ▷ Pb -∗ lft_dead κ
+ ={E ∪ ↑borN}=∗
+ lft_vs_inv_go I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I.
+
+ Definition lft_inv_alive_go : iProp Σ :=
+ (∃ Pb Pi,
+ lft_bor_alive κ Pb ∗
+ lft_vs_go Pb Pi ∗
+ lft_inh κ false Pi)%I.
+ End lft_inv_alive.
+
+ Definition lft_inv_alive (A : gmap atomic_lft (bool * coPset)) (κ : lft) : iProp Σ :=
+ Fix_F _ (lft_inv_alive_go A) (gmultiset_wf κ).
+ Definition lft_vs_inv (A : gmap atomic_lft (bool * coPset)) (κ : lft)
+ (I : gmap lft lft_names) : iProp Σ :=
+ lft_vs_inv_go κ (λ κ' _, lft_inv_alive A κ') I.
+ Definition lft_vs (A : gmap atomic_lft (bool * coPset)) (κ : lft)
+ (Pb Pi : iProp Σ) : iProp Σ :=
+ lft_vs_go A κ (λ κ' _, lft_inv_alive A κ') Pb Pi.
Definition lft_inv_dead (κ : lft) : iProp Σ :=
(∃ Pi,
@@ -156,17 +166,17 @@ Section defs.
own_cnt κ (● 0) ∗
lft_inh κ true Pi)%I.
- Definition lft_alive_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
- ∀ Λ : atomic_lft, Λ ∈ κ → A !! Λ = Some true.
- Definition lft_dead_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
- ∃ Λ : atomic_lft, Λ ∈ κ ∧ A !! Λ = Some false.
+ Definition lft_alive_in (A : gmap atomic_lft (bool * coPset)) (κ : lft) : Prop :=
+ ∀ Λ : atomic_lft, Λ ∈ κ → ∃ E, A !! Λ = Some (true, E).
+ Definition lft_dead_in (A : gmap atomic_lft (bool * coPset)) (κ : lft) : Prop :=
+ ∃ (Λ : atomic_lft) (E : coPset), Λ ∈ κ ∧ A !! Λ = Some (false, E).
- Definition lft_inv (A : gmap atomic_lft bool) (κ : lft) : iProp Σ :=
- (lft_inv_alive κ ∗ ⌜lft_alive_in A κ⌝ ∨
+ Definition lft_inv (A : gmap atomic_lft (bool * coPset)) (κ : lft) : iProp Σ :=
+ (lft_inv_alive A κ ∗ ⌜lft_alive_in A κ⌝ ∨
lft_inv_dead κ ∗ ⌜lft_dead_in A κ⌝)%I.
Definition lfts_inv : iProp Σ :=
- (∃ (A : gmap atomic_lft bool) (I : gmap lft lft_names),
+ (∃ (A : gmap atomic_lft (bool * coPset)) (I : gmap lft lft_names),
own_alft_auth A ∗
own_ilft_auth I ∗
[∗ set] κ ∈ dom _ I, lft_inv A κ)%I.
@@ -174,8 +184,8 @@ Section defs.
Definition lft_ctx : iProp Σ := inv mgmtN lfts_inv.
Definition lft_incl (κ κ' : lft) : iProp Σ :=
- (□ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
- lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
+ (□ ((∀ q E, lft_tok q κ E ={↑lftN}=∗ ∃ q',
+ lft_tok q' κ' E ∗ (lft_tok q' κ' E ={↑lftN}=∗ lft_tok q κ E)) ∗
(lft_dead κ' ={↑lftN}=∗ lft_dead κ)))%I.
Definition bor_idx := (lft * slice_name)%type.
@@ -197,8 +207,8 @@ 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.
+Notation "q .[ κ , E ]" := (lft_tok q κ E)
+ (format "q .[ κ , E ]", at level 0) : uPred_scope.
Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
Notation "&{ κ } P" := (bor κ P)
@@ -220,7 +230,7 @@ Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
(* Unfolding lemmas *)
-Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
+Lemma lft_vs_inv_go_ne κ f f' I n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
Proof.
@@ -228,45 +238,69 @@ Proof.
by apply forall_ne=> Hκ.
Qed.
-Lemma lft_vs_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) Pb Pb' Pi Pi' n :
+Lemma lft_vs_go_ne κ f f' A A' Pb Pb' Pi Pi' n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
+ (∀ Λ, Λ ∈ κ → A !! Λ = A' !! Λ) →
Pb ≡{n}≡ Pb' → Pi ≡{n}≡ Pi' →
- lft_vs_go κ f Pb Pi ≡{n}≡ lft_vs_go κ f' Pb' Pi'.
+ lft_vs_go A κ f Pb Pi ≡{n}≡ lft_vs_go A' κ f' Pb' Pi'.
Proof.
- intros Hf HPb HPi. apply exist_ne=> n'.
- apply sep_ne, forall_ne=> // I. rewrite lft_vs_inv_go_ne //. solve_proper.
+ intros Hf HA HPb HPi. apply exist_ne=> n'.
+ apply sep_ne, forall_ne=> // I. apply forall_ne=> E.
+ apply wand_ne; last (rewrite lft_vs_inv_go_ne //; solve_proper).
+ apply equiv_dist, pure_iff, base.forall_proper=>E'. split; intros HE HE';
+ apply HE; intros; eapply HE'; rewrite // -?HA // HA //.
Qed.
-Lemma lft_inv_alive_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) n :
+Lemma lft_inv_alive_go_ne κ f f' A A' n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
- lft_inv_alive_go κ f ≡{n}≡ lft_inv_alive_go κ f'.
+ (∀ Λ, Λ ∈ κ → A !! Λ = A' !! Λ) →
+ lft_inv_alive_go A κ f ≡{n}≡ lft_inv_alive_go A' κ f'.
Proof.
- intros Hf. apply exist_ne=> Pb; apply exist_ne=> Pi. by rewrite lft_vs_go_ne.
+ intros Hf HA. apply exist_ne=> Pb; apply exist_ne=> Pi. by rewrite lft_vs_go_ne.
Qed.
-Lemma lft_inv_alive_unfold κ :
- lft_inv_alive κ ⊣⊢ ∃ Pb Pi,
- lft_bor_alive κ Pb ∗ lft_vs κ Pb Pi ∗ lft_inh κ false Pi.
+Lemma lft_inv_alive_unfold A κ :
+ lft_inv_alive A κ ⊣⊢ ∃ Pb Pi,
+ lft_bor_alive κ Pb ∗ lft_vs A κ Pb Pi ∗ lft_inh κ false Pi.
Proof.
apply equiv_dist=> n. rewrite /lft_inv_alive -Fix_F_eq.
- apply lft_inv_alive_go_ne=> κ' Hκ.
- apply (Fix_F_proper _ (λ _, dist n)); auto using lft_inv_alive_go_ne.
+ eapply lft_inv_alive_go_ne=> // κ' Hκ.
+ apply (Fix_F_proper _ (λ _, dist n)). eauto using lft_inv_alive_go_ne.
Qed.
-Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) :
- lft_vs_inv κ I ⊣⊢ lft_bor_dead κ ∗
+Lemma lft_vs_inv_unfold A κ (I : gmap lft lft_names) :
+ lft_vs_inv A κ I ⊣⊢ lft_bor_dead κ ∗
own_ilft_auth I ∗
- [∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
+ [∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive A κ'.
Proof.
rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite pure_impl_forall.
Qed.
-Lemma lft_vs_unfold κ Pb Pi :
- lft_vs κ Pb Pi ⊣⊢ ∃ n : nat,
+Lemma lft_vs_unfold A κ Pb Pi :
+ lft_vs A κ Pb Pi ⊣⊢ ∃ n : nat,
own_cnt κ (● n) ∗
- ∀ I : gmap lft lft_names,
- lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={⊤∖↑mgmtN}=∗
- lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
+ ∀ (I : gmap lft lft_names) (E : coPset),
+ ⌜∀ E', (∀ Λ b EΛ, Λ ∈ κ → A !! Λ = Some (b, EΛ) → E' ⊆ EΛ) → E' ⊆ E⌝ -∗
+ lft_vs_inv A κ I -∗ ▷ Pb -∗ lft_dead κ ={E ∪ ↑borN}=∗
+ lft_vs_inv A κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
Proof. done. Qed.
+Lemma lft_inv_alive_A_proper A A' κ :
+ (∀ Λ, Λ ∈ κ → A !! Λ = A' !! Λ) → lft_inv_alive A κ ≡ lft_inv_alive A' κ.
+Proof.
+ intros HA. apply equiv_dist=>n. unfold lft_inv_alive.
+ generalize (gmultiset_wf κ). revert κ HA. fix IH 3. intros ?? []. simpl.
+ apply lft_inv_alive_go_ne, HA. intros κ' [Hκ ?]. apply IH.
+ intros. by eapply HA, gmultiset_elem_of_subseteq.
+Qed.
+
+Global Instance lft_tok_mono q κ : Proper (flip (⊆) ==> (⊢)) (lft_tok q κ).
+Proof.
+ intros E E' ?. rewrite /lft_tok. do 2 f_equiv; intros ?; first set_solver.
+ apply exist_mono=>F. (do 2 f_equiv)=>?. set_solver.
+Qed.
+
+Global Instance lft_tok_mono_flip q κ : Proper ((⊆) ==> flip (⊢)) (lft_tok q κ).
+Proof. intros ??. apply lft_tok_mono. Qed.
+
Global Instance own_bor_proper κ : Proper ((≡) ==> (≡)) (own_bor κ).
Proof. solve_proper. Qed.
Global Instance own_cnt_proper κ : Proper ((≡) ==> (≡)) (own_cnt κ).
@@ -284,10 +318,10 @@ Proof. solve_proper. Qed.
Global Instance lft_inh_proper κ s : Proper ((≡) ==> (≡)) (lft_inh κ s).
Proof. apply (ne_proper _). Qed.
-Global Instance lft_vs_ne κ n :
- Proper (dist n ==> dist n ==> dist n) (lft_vs κ).
+Global Instance lft_vs_ne A κ n :
+ Proper (dist n ==> dist n ==> dist n) (lft_vs A κ).
Proof. intros P P' HP Q Q' HQ. by apply lft_vs_go_ne. Qed.
-Global Instance lft_vs_proper κ : Proper ((≡) ==> (≡) ==> (≡)) (lft_vs κ).
+Global Instance lft_vs_proper κ A : Proper ((≡) ==> (≡) ==> (≡)) (lft_vs A κ).
Proof. apply (ne_proper_2 _). Qed.
Global Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
@@ -312,7 +346,7 @@ Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
Proof. apply (ne_proper _). Qed.
(*** PersistentP and TimelessP and instances *)
-Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
+Global Instance lft_tok_timeless q κ E : TimelessP q.[κ,E].
Proof. rewrite /lft_tok. apply _. Qed.
Global Instance lft_dead_persistent κ : PersistentP [†κ].
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 95287fd03c18cadea6184af9aa495c70956acabb..5666756f44cb340e81c03c0001bf66ef38ca8130 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -36,7 +36,7 @@ Proof.
iAssert (∀ b, lft_inh κ b True)%I with "[Hinh]" as "Hinh".
{ iIntros (b). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
- iAssert (lft_inv_dead κ ∧ lft_inv_alive κ)%I
+ iAssert (lft_inv_dead κ ∧ lft_inv_alive A κ)%I
with "[-HA HI Hinv]" as "Hdeadandalive".
{ iSplit.
- rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
@@ -53,20 +53,21 @@ Proof.
destruct (lft_alive_or_dead_in A κ) as [(Λ&?&HAΛ)|Haliveordead].
- iMod (own_update with "HA") as "[HA _]".
{ apply auth_update_alloc,
- (alloc_singleton_local_update _ Λ (Cinr ())); last done.
+ (alloc_singleton_local_update _ Λ (Some (Cinr ()), to_agree ∅)); last done.
by rewrite lookup_fmap HAΛ. }
- iModIntro. iExists (<[Λ:=false]>A), (<[κ:=γs]> I).
+ iModIntro. iExists (<[Λ:=(false, ∅)]>A), (<[κ:=γs]> I).
iSplit; first rewrite lookup_insert; eauto.
rewrite /own_ilft_auth /own_alft_auth /to_ilftUR /to_alftUR !fmap_insert.
iFrame "HA HI". rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
iSplitR "Hinv".
{ rewrite /lft_inv. iNext. iRight. iSplit.
{ by iDestruct "Hdeadandalive" as "[? _]". }
- iPureIntro. exists Λ. rewrite lookup_insert; auto. }
+ iPureIntro. exists Λ. rewrite lookup_insert; eauto. }
iNext. iApply (@big_sepS_impl with "[$Hinv]").
rewrite /lft_inv. iIntros "!#"; iIntros (κ' ?%elem_of_dom)
"[[HA HA']|[HA HA']]"; iDestruct "HA'" as %HA.
- + iLeft. iFrame "HA". iPureIntro. by apply lft_alive_in_insert.
+ + iLeft. rewrite lft_inv_alive_insert //. iFrame "HA".
+ iPureIntro. by apply lft_alive_in_insert.
+ iRight. iFrame "HA". iPureIntro. by apply lft_dead_in_insert.
- iModIntro. iExists A, (<[κ:=γs]> I).
iSplit; first rewrite lookup_insert; eauto.
@@ -99,12 +100,13 @@ Lemma raw_bor_fake' E κ P :
Proof.
iIntros (?) "#LFT H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
- iDestruct "Hκ" as %Hκ. rewrite /lft_dead. iDestruct "H†" as (Λ) "[% #H†]".
- iDestruct (own_alft_auth_agree A' Λ false with "HA H†") as %EQAΛ.
+ iDestruct "Hκ" as %Hκ. rewrite /lft_dead. iDestruct "H†" as (Λ E') "[% #H†]".
+ iDestruct (own_alft_auth_agree with "HA H†") as %EQAΛ.
iDestruct (@big_sepS_elem_of_acc with "Hinv")
as "[Hinv Hclose']"; first by apply elem_of_dom.
- rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
- { unfold lft_alive_in in *; naive_solver. }
+ rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >Hal]|[Hinv >%]]".
+ { iDestruct "Hal" as %[F HF]; first done.
+ eapply eq_trans in HF; last by symmetry; apply EQAΛ. done. }
rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
iFrame. iApply "Hclose". iExists A', I'. iFrame. iNext. iApply "Hclose'".
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index e6df1d52529270ef3295cf28820cec75a997ae39..56e4826885e3df28a9afe4805bbacb08f288adf3 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -42,15 +42,20 @@ Proof.
destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
Qed.
-Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
+Lemma own_alft_auth_agree (A : gmap atomic_lft (bool * coPset)) Λ st E :
own_alft_auth A -∗
- own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
+ own alft_name (◯ {[Λ := (Some st, to_agree E)]}) -∗
+ ⌜A !! Λ = Some (match st with Cinl _ => true | _ => false end, E)⌝.
Proof.
iIntros "HA HΛ".
iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_valid_discrete_2.
- iPureIntro. move: HA=> /singleton_included [qs [/leibniz_equiv_iff]].
- rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
- move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
+ iPureIntro. move: HA=> /singleton_included [qs []].
+ rewrite lookup_fmap fmap_Some_equiv=> -[[b E'] [-> ->]] /Some_included /=.
+ move=> [[? /(inj to_agree) ?]|
+ /prod_included[/Some_included Hst /to_agree_included ?]]; setoid_subst.
+ - by destruct b.
+ - destruct Hst as [Hst|Hst]. setoid_subst. by destruct b.
+ apply csum_included in Hst. destruct b; naive_solver.
Qed.
Lemma own_bor_auth I κ x : own_ilft_auth I -∗ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
@@ -158,15 +163,21 @@ Qed.
(** Alive and dead *)
Global Instance lft_alive_in_dec A κ : Decision (lft_alive_in A κ).
Proof.
- refine (cast_if (decide (set_Forall (λ Λ, A !! Λ = Some true)
- (dom (gset atomic_lft) κ))));
- rewrite /lft_alive_in; by setoid_rewrite <-gmultiset_elem_of_dom.
+ destruct (decide (set_Forall (λ Λ, from_option fst false (A !! Λ))
+ (dom (gset atomic_lft) κ))) as [Hκ|Hκ];
+ [left|right; contradict Hκ]; move=> Λ /gmultiset_elem_of_dom HΛ;
+ specialize (Hκ Λ HΛ); simpl in Hκ.
+ - by destruct (A!!Λ) as [[[]]|]; eauto.
+ - by destruct Hκ as [? ->].
Qed.
Global Instance lft_dead_in_dec A κ : Decision (lft_dead_in A κ).
Proof.
- refine (cast_if (decide (set_Exists (λ Λ, A !! Λ = Some false)
- (dom (gset atomic_lft) κ))));
- rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
+ destruct (decide ((set_Exists (λ Λ, ¬from_option fst true (A !! Λ))
+ (dom (gset atomic_lft) κ)))) as [Hκ|Hκ]; [left|right; contradict Hκ].
+ - destruct Hκ as [Λ [?%gmultiset_elem_of_dom Hκ]]. exists Λ.
+ destruct (A!!Λ) as [[[]]|]; naive_solver.
+ - destruct Hκ as (Λ & E & ?%gmultiset_elem_of_dom & EQ). exists Λ.
+ rewrite EQ /=. naive_solver.
Qed.
Lemma lft_alive_or_dead_in A κ :
@@ -175,73 +186,87 @@ Proof.
rewrite /lft_alive_in /lft_dead_in.
destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom (gset _) κ)))
as [(Λ & ?%gmultiset_elem_of_dom & HAΛ)|HA%(not_set_Exists_Forall _)]; first eauto.
- destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom (gset _) κ)))
- as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)]; first eauto.
- right; left. intros Λ HΛ%gmultiset_elem_of_dom.
- move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[]|]; naive_solver.
+ destruct (decide (set_Exists (λ Λ, ¬from_option fst true (A !! Λ)) (dom (gset _) κ)))
+ as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)].
+ - right; right. exists Λ. by destruct (A !! Λ) as [[[]]|]; eauto.
+ - right; left. intros Λ HΛ%gmultiset_elem_of_dom.
+ move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[[]]|]; naive_solver.
Qed.
Lemma lft_alive_and_dead_in A κ : lft_alive_in A κ → lft_dead_in A κ → False.
-Proof. intros Halive (Λ&HΛ&?). generalize (Halive _ HΛ). naive_solver. Qed.
+Proof. intros Halive (Λ&E&HΛ&?). generalize (Halive _ HΛ). naive_solver. Qed.
Lemma lft_alive_in_subseteq A κ κ' :
lft_alive_in A κ → κ' ⊆ κ → lft_alive_in A κ'.
Proof. intros Halive ? Λ ?. by eapply Halive, gmultiset_elem_of_subseteq. Qed.
-Lemma lft_alive_in_insert A κ Λ b :
- A !! Λ = None → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
+Lemma lft_alive_in_insert_notin A κ Λ st :
+ Λ ∉ κ → lft_alive_in A κ → lft_alive_in (<[Λ:=st]> A) κ.
Proof.
intros HΛ Halive Λ' HΛ'.
- assert (Λ ≠ Λ') by (intros ->; move:(Halive _ HΛ'); by rewrite HΛ).
- rewrite lookup_insert_ne; eauto.
+ rewrite lookup_insert_ne; last (by intros ->); auto.
Qed.
-Lemma lft_alive_in_insert_false A κ Λ b :
- Λ ∉ κ → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
+Lemma lft_alive_in_insert A κ Λ st :
+ A !! Λ = None → lft_alive_in A κ → lft_alive_in (<[Λ:=st]> A) κ.
Proof.
- intros HΛ Halive Λ' HΛ'.
- rewrite lookup_insert_ne; last (by intros ->); auto.
+ intros ? Ha. apply lft_alive_in_insert_notin, Ha=>?. edestruct Ha; naive_solver.
+Qed.
+
+Lemma lft_inv_alive_insert_notin A κ Λ st :
+ Λ ∉ κ → lft_inv_alive A κ -∗ lft_inv_alive (<[Λ:=st]> A) κ.
+Proof.
+ intros ?. rewrite lft_inv_alive_A_proper=>// ??.
+ rewrite lookup_insert_ne //. naive_solver.
+Qed.
+Lemma lft_inv_alive_insert A κ Λ st :
+ A !! Λ = None → lft_alive_in A κ →
+ lft_inv_alive A κ -∗ lft_inv_alive (<[Λ:=st]> A) κ.
+Proof.
+ intros ? Halive. eapply lft_inv_alive_insert_notin=>HΛ.
+ edestruct Halive; naive_solver.
Qed.
-Lemma lft_dead_in_insert A κ Λ b :
- A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
+Lemma lft_dead_in_insert A κ Λ st :
+ A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=st]> A) κ.
Proof.
- intros HΛ (Λ'&?&HΛ').
+ intros HΛ (Λ'&E&?&HΛ').
assert (Λ ≠ Λ') by (intros ->; move:HΛ'; by rewrite HΛ).
- exists Λ'. by rewrite lookup_insert_ne.
+ exists Λ', E. by rewrite lookup_insert_ne.
Qed.
-Lemma lft_dead_in_insert_false A κ Λ :
- lft_dead_in A κ → lft_dead_in (<[Λ:=false]> A) κ.
+Lemma lft_dead_in_insert_None A κ Λ E :
+ lft_dead_in A κ → lft_dead_in (<[Λ:=(false, E)]> A) κ.
Proof.
- intros (Λ'&?&HΛ'). destruct (decide (Λ = Λ')) as [<-|].
- - exists Λ. by rewrite lookup_insert.
- - exists Λ'. by rewrite lookup_insert_ne.
+ intros (Λ'&E'&?&HΛ'). destruct (decide (Λ = Λ')) as [<-|].
+ - exists Λ, E. by rewrite lookup_insert.
+ - exists Λ',E'. by rewrite lookup_insert_ne.
Qed.
-Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
-Proof. exists Λ. by rewrite lookup_insert. Qed.
+Lemma lft_dead_in_insert_None' A κ Λ E : Λ ∈ κ → lft_dead_in (<[Λ:=(false,E)]> A) κ.
+Proof. exists Λ,E. 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.
+ intros (Λ & E & [Hin|Hin]%elem_of_union & HΛ) Halive.
+ - contradict HΛ. by destruct (Halive _ Hin) as [? ->].
+ - exists Λ, E. 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. }
+ iIntros ((Λ & E & HΛκ & EQΛ)) "HA". unfold own_alft_auth, lft_dead.
+ assert (({[Λ := (Some (Cinr ()), to_agree E)]} ⋅ to_alftUR A) ≡ to_alftUR A)
+ as HAinsert.
+ { move=>Λ'. rewrite lookup_op lookup_fmap. destruct (decide (Λ = Λ')) as [<-|Hne].
+ + by rewrite EQΛ lookup_singleton -Some_op pair_op agree_idemp.
+ + by rewrite !lookup_insert_ne // lookup_empty left_id -lookup_fmap. }
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.
+ { eapply (auth_update_alloc _ _ ({[Λ := (Some (Cinr ()), to_agree E)]}⋅∅)),
+ 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.
+Lemma lft_inv_alive_twice A κ : lft_inv_alive A κ -∗ lft_inv_alive A κ -∗ False.
Proof.
rewrite lft_inv_alive_unfold /lft_inh.
iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
@@ -249,7 +274,7 @@ Proof.
by iDestruct (own_inh_valid_2 with "HE HE'") as %?.
Qed.
-Lemma lft_inv_alive_in A κ : lft_alive_in A κ → lft_inv A κ -∗ lft_inv_alive κ.
+Lemma lft_inv_alive_in A κ : lft_alive_in A κ → lft_inv A κ -∗ lft_inv_alive A κ.
Proof.
rewrite /lft_inv. iIntros (?) "[[$ _]|[_ %]]".
by destruct (lft_alive_and_dead_in A κ).
@@ -261,37 +286,66 @@ Proof.
Qed.
(** Basic rules about lifetimes *)
-Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
-Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
+Lemma lft_tok_sep q κ1 κ2 E : q.[κ1,E] ∗ q.[κ2,E] ⊣⊢ q.[κ1 ∪ κ2,E].
+Proof.
+ rewrite /lft_tok big_sepMS_union. iSplit; first by iIntros "[[$$][_$]]".
+ iIntros "[%[$$]]". auto.
+Qed.
+
+Lemma lft_tok_combine q κ1 κ2 E1 E2 :
+ q.[κ1,E1] ∗ q.[κ2,E2] ⊢ q.[κ1 ∪ κ2, E1 ∩ E2].
+Proof.
+ rewrite <-(intersection_subseteq_r E1 E2), <-(intersection_subseteq_l E1 E2) at 1.
+ rewrite /lft_tok big_sepMS_union. iIntros "[[%$][%$]]!%". set_solver.
+Qed.
+
+Lemma lft_tok_frac_mask q1 q2 κ E1 E2 :
+ q1.[κ,E1] ∗ q2.[κ,E2] ⊢ (q1 + q2).[κ, E1 ∪ E2].
+Proof.
+ rewrite /lft_tok. iIntros "[[% H1][% H2]]". iCombine "H1" "H2" as "H".
+ iSplit; first by iPureIntro; set_solver. iApply (big_sepMS_mono _ _ κ κ with "H")=>// Λ ?.
+ iIntros "[H1 H2]". iDestruct "H1" as (E'1) "[% H1]". iDestruct "H2" as (E'2) "[% H2]".
+ iCombine "H1" "H2" as "H". rewrite -auth_frag_op op_singleton pair_op.
+ iDestruct (own_valid with "H") as %[_ Hag%to_agree_comp_valid]%singleton_valid.
+ setoid_subst. rewrite agree_idemp. iExists _. iIntros "{$H}!%". set_solver.
+Qed.
Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ∪ κ2].
Proof.
rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
- rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
+ rewrite -!sep_exist_l -sep_or_r -pure_or. do 2 f_equiv. set_solver.
Qed.
-Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False.
+Lemma lft_tok_dead q κ E : q.[κ,E] -∗ [† κ] -∗ False.
Proof.
- rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
- iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
+ rewrite /lft_tok /lft_dead. iIntros "[% H]"; iDestruct 1 as (Λ' E') "[% H']".
+ iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as (E'') "[_ H]"=> //.
iDestruct (own_valid_2 with "H H'") as %Hvalid.
- move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
+ move: Hvalid=> /auth_own_valid /=; rewrite op_singleton singleton_valid=>-[[]].
Qed.
-Lemma lft_tok_static q : q.[static]%I.
-Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
+Lemma lft_tok_static q E : E ⊥ ↑lftN → q.[static,E]%I.
+Proof. rewrite /lft_tok big_sepMS_empty. iIntros. iSplit; auto. Qed.
Lemma lft_dead_static : [† static] -∗ False.
-Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
+Proof. rewrite /lft_dead. iDestruct 1 as (Λ E) "[% H']". set_solver. Qed.
+
+Lemma lft_tok_mask_bound q κ E : q.[κ,E] -∗ ⌜E ⊥ ↑lftN⌝.
+Proof. rewrite /lft_tok. by iIntros "[$ _]". Qed.
(* Fractional and AsFractional instances *)
-Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
-Proof.
- intros p q. rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper.
- intros Λ ?. rewrite -Cinl_op -op_singleton auth_frag_op own_op //.
-Qed.
-Global Instance lft_tok_as_fractional κ q :
- AsFractional q.[κ] (λ q, q.[κ])%I q.
+Global Instance lft_tok_fractional κ E : Fractional (λ q, q.[κ,E])%I.
+Proof.
+ intros p q. iSplit; iIntros "H".
+ - rewrite /lft_tok. iDestruct "H" as "[% H]". iFrame "%".
+ rewrite -big_sepMS_sepMS big_sepMS_mono=>// Λ ?. iIntros "H".
+ iDestruct "H" as (E') "[% H]". rewrite -(agree_idemp (to_agree E')).
+ rewrite -frac_op' -Cinl_op Some_op -pair_op -op_singleton auth_frag_op own_op //.
+ iDestruct "H" as "[H1 H2]". iSplitL "H1"; eauto.
+ - rewrite -{3}(idemp_L union E). by iApply lft_tok_frac_mask.
+Qed.
+Global Instance lft_tok_as_fractional κ q E :
+ AsFractional q.[κ,E] (λ q, q.[κ,E])%I q.
Proof. split. done. apply _. Qed.
Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
Proof.
@@ -303,9 +357,8 @@ Global Instance idx_bor_own_as_fractional i q :
Proof. split. done. apply _. Qed.
(** Lifetime inclusion *)
-Lemma lft_incl_acc E κ κ' q :
- ↑lftN ⊆ E →
- κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+Lemma lft_incl_acc E F κ κ' q :
+ ↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ,F] ={E}=∗ ∃ q', q'.[κ',F] ∗ (q'.[κ',F] ={E}=∗ q.[κ,F]).
Proof.
rewrite /lft_incl.
iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
@@ -320,15 +373,15 @@ Proof.
Qed.
Lemma lft_incl_intro κ κ' :
- □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
- lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
+ □ ((∀ q E, q.[κ,E] ={↑lftN}=∗ ∃ q',
+ q'.[κ',E] ∗ (q'.[κ',E] ={↑lftN}=∗ q.[κ,E])) ∗
(lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
Proof. reflexivity. Qed.
Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
Proof.
iIntros (->%gmultiset_union_difference) "!#". iSplitR.
- - iIntros (q). rewrite <-lft_tok_sep. iIntros "[H Hf]". iExists q. iFrame.
+ - iIntros (q E). rewrite <-lft_tok_sep. iIntros "[H Hf]". iExists q. iFrame.
rewrite <-lft_tok_sep. by iIntros "!>{$Hf}$".
- iIntros "? !>". iApply lft_dead_or. auto.
Qed.
@@ -339,7 +392,7 @@ Proof. by apply lft_le_incl. Qed.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Proof.
rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†] !#". iSplitR.
- - iIntros (q) "Hκ".
+ - iIntros (q E) "Hκ".
iMod ("H1" with "Hκ") as (q') "[Hκ' Hclose]".
iMod ("H2" with "Hκ'") as (q'') "[Hκ'' Hclose']".
iExists q''. iIntros "{$Hκ''} !> Hκ''".
@@ -347,8 +400,9 @@ Proof.
- iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
Qed.
-Lemma lft_glb_acc κ κ' q q' :
- q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
+Lemma lft_glb_acc κ κ' q q' E:
+ q.[κ,E] -∗ q'.[κ',E] -∗
+ ∃ q'', q''.[κ ∪ κ', E] ∗ (q''.[κ ∪ κ', E] -∗ q.[κ,E] ∗ q'.[κ',E]).
Proof.
iIntros "Hκ Hκ'".
destruct (Qp_lower_bound q q') as (qq & q0 & q'0 & -> & ->).
@@ -359,7 +413,7 @@ Qed.
Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
Proof.
rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
- - iIntros (q) "[Hκ'1 Hκ'2]".
+ - iIntros (q E) "[Hκ'1 Hκ'2]".
iMod ("H1" with "Hκ'1") as (q') "[Hκ' Hclose']".
iMod ("H2" with "Hκ'2") as (q'') "[Hκ'' Hclose'']".
iDestruct (lft_glb_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
@@ -479,26 +533,29 @@ Proof.
Qed.
(* View shifts *)
-Lemma lft_vs_frame κ Pb Pi P :
- lft_vs κ Pb Pi -∗ lft_vs κ (P ∗ Pb) (P ∗ Pi).
+Lemma lft_vs_frame A κ Pb Pi P :
+ lft_vs A κ Pb Pi -∗ lft_vs A κ (P ∗ Pb) (P ∗ Pi).
Proof.
rewrite !lft_vs_unfold. iDestruct 1 as (n) "[Hcnt Hvs]".
- iExists n. iFrame "Hcnt". iIntros (I'') "Hinv [$ HPb] H†".
- iApply ("Hvs" $! I'' with "Hinv HPb H†").
+ iExists n. iFrame "Hcnt". iIntros (I'' E) "HE Hinv [$ HPb] H†".
+ iApply ("Hvs" $! I'' E with "HE 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.
+Lemma lft_vs_cons E q A κ Pb Pb' Pi :
+ (∀ Λ b EΛ, Λ ∈ κ → A !! Λ = Some (b, EΛ) → E ⊆ EΛ) →
+ (lft_bor_dead κ ∗ ▷ Pb' ={E ∪ ↑borN}=∗ lft_bor_dead κ ∗ ▷ Pb) -∗
+ ▷?q lft_vs A κ Pb Pi -∗ ▷?q lft_vs A κ Pb' Pi.
Proof.
- iIntros "Hcons Hvs". iNext. rewrite !lft_vs_unfold.
+ iIntros (HE) "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 (I E') "HE'". 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κ†").
+ iApply fupd_trans. iDestruct "HE'" as %HE'. iApply (fupd_mask_mono (E ∪ ↑borN));
+ first by auto using union_preserving_r.
+ iMod ("Hcons" with "[$Hdead $HPb]") as "[Hdead HPb]". iModIntro.
+ iApply ("Hvs" $! I with "[%] [Hdead Hinv Hκs] HPb Hκ†"); first done.
rewrite lft_vs_inv_unfold. by iFrame.
Qed.
End primitive.
diff --git a/theories/lifetime/model/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
index fadea3d20e6b368d8fdf776af22bd58109dc1f1d..202126448a97198f31804098f4f49243914ced76 100644
--- a/theories/lifetime/model/raw_reborrow.v
+++ b/theories/lifetime/model/raw_reborrow.v
@@ -20,8 +20,8 @@ Lemma raw_bor_unnest E q A I Pb Pi P κ i κ' :
κ ⊂ κ' →
lft_alive_in A κ' →
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.
+ ▷?q lft_vs A κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
+ Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs A κ' Pb' Pi.
Proof.
iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
@@ -71,7 +71,7 @@ Proof.
by rewrite /bor_cnt. }
clear dependent Iinv I.
iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hn●".
- iIntros (I) "Hinv [HP HPb] #Hκ†".
+ iIntros (I E') "% Hinv [HP HPb] #Hκ†".
rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
@@ -85,12 +85,12 @@ Proof.
(exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iMod (slice_fill _ _ false with "Hislice HP Hbox")
- as "Hbox"; first by solve_ndisj.
+ as "Hbox"; first set_solver.
{ by rewrite lookup_fmap HB. }
iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
rewrite /=; iDestruct "Hcnt" as "[% H1◯]".
- iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
- [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
+ iMod ("Hvs" $! I with "[] [Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
+ [$HPb Hi] Hκ†") as "($ & $ & Hcnt')"; first done.
{ rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
iIntros (_). rewrite lft_inv_alive_unfold.
@@ -110,15 +110,15 @@ Lemma raw_bor_unnest' E q A I Pb Pi P κ κ' :
κ ⊆ κ' →
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.
+ ▷?q lft_vs A κ' (raw_bor κ P ∗ Pb) Pi ={E}=∗ ∃ Pb',
+ Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs A κ' 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.
+ iApply (lft_vs_cons ∅ with "[]"); last done; first set_solver+.
iIntros "(Hdead & HPb)".
- iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
+ iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first set_solver.
by iFrame. }
assert (κ ⊂ κ') by (by apply strict_spec_alt).
iDestruct (raw_bor_inI with "HI Hraw") as %HI.
@@ -128,7 +128,7 @@ Proof.
iDestruct "Hislice" as (P') "[#HPP' 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.
+ { iApply (lft_vs_cons ∅ with "[]"); last done; first set_solver+.
iIntros "[$ [>? $]]". iModIntro. iNext. rewrite /raw_bor.
iExists i. iFrame. iExists _. iFrame "#". }
iExists Pb'. iModIntro. iFrame. iSplitL "Hclose Hκ". by iApply "Hclose".
@@ -183,11 +183,12 @@ Proof.
iDestruct ("HIlookup" with "HI") as %Hκ'.
iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
first by apply elem_of_dom.
- rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[Halive >%]|[Hdead >%]]".
+ rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[Halive >H]|[Hdead >%]]".
- (* the same proof is in bor_fake and bor_create *)
- rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
- iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
- unfold lft_alive_in in *. naive_solver.
+ rewrite /lft_dead; iDestruct "H†" as (Λ E') "[% #H†]".
+ iDestruct (own_alft_auth_agree with "HA H†") as %EQAΛ.
+ iDestruct "H" as %(E'' & HE''); first done.
+ eapply eq_trans in HE''; last by symmetry; apply EQAΛ. done.
- rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & Hcnt & Hinh)".
iMod ("Hinh_close" $! Pi with "Hinh") as (Pi') "(Heq & >Hbor & Hinh)".
iMod ("Hclose" with "[HA HI Hinv Hdead Hinh Hcnt]") as "_".
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 14b4c53de88002d58dfea60fa8e033eeccfd64e6..ff3e47cbf6575b3268eb409cbf636ae87cfbff92 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -92,7 +92,7 @@ Proof.
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 contractive rewriting. *)
- iApply (lft_vs_cons with "[]"); last done.
+ iApply (lft_vs_cons ∅ with "[]"); last done; first set_solver+.
iIntros "[$ [Hbor HPb']]". iModIntro. iNext. iRewrite "EQ". iFrame. by iApply "HPP'". }
iMod ("Hclose" with "[-HP]") as "_".
{ iNext. simpl. rewrite /lfts_inv. iExists A, I. iFrame.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 78a7bb2dffa60292af019ad00c038d53e4305a00..80a3e626ebac32bac1a36978a1d5c0563d3eb5e2 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -36,11 +36,11 @@ Section na_bor.
iExists i. iFrame "#". iApply (na_inv_alloc tid E N with "[Hown]"). auto.
Qed.
- Lemma na_bor_acc q κ E F :
+ Lemma na_bor_acc q κ E E' F :
↑lftN ⊆ E → ↑N ⊆ E → ↑N ⊆ F →
- lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ] -∗ na_own tid F ={E}=∗
+ lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ,E'] -∗ na_own tid F ={E}=∗
▷P ∗ na_own tid (F ∖ ↑N) ∗
- (▷P -∗ na_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ na_own tid F).
+ (▷P -∗ na_own tid (F ∖ ↑N) ={E}=∗ q.[κ,E'] ∗ na_own tid F).
Proof.
iIntros (???) "#LFT#HP Hκ Hnaown".
iDestruct "HP" as (i) "(#Hpers&#Hinv)".
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 8ab654ea2ca295cbc1408963f10e52cf60a6a10f..3c6b819bb4da7f36c8864e134875801a7479ce73 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -56,9 +56,9 @@ Section shared_bors.
+ iRight. iFrame. iIntros "!>". by iMod "Hclose".
Qed.
- Lemma shr_bor_acc_tok E q κ :
- ↑lftN ⊆ E → ↑N ⊆ E →
- lft_ctx -∗ &shr{κ,N}P -∗ q.[κ] ={E,E∖↑N}=∗ ▷P ∗ (▷P ={E∖↑N,E}=∗ q.[κ]).
+ Lemma shr_bor_acc_tok E F q κ :
+ ↑lftN ⊆ F → ↑N ⊆ F →
+ lft_ctx -∗ &shr{κ,N}P -∗ q.[κ,E] ={F,F∖↑N}=∗ ▷P ∗ (▷P ={F∖↑N,F}=∗ q.[κ,E]).
Proof.
iIntros (??) "#LFT #HP Hκ". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
- iInv N as ">Hi" "Hclose".
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index e7632f58b4f4713ef57beabb80e292d3dbe8eb57..d2055639ad0da8230a28fba561bea55ee77435a5 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -240,7 +240,8 @@ Section lft_contexts.
Lemma lctx_lft_alive_static : lctx_lft_alive static.
Proof.
- iIntros (F qE qL ?) "$$". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
+ iIntros (F qE qL ?) "$$". iExists 1%Qp. iSplitL; last auto.
+ iApply lft_tok_static. set_solver.
Qed.
Lemma lctx_lft_alive_local κ κs:
@@ -255,7 +256,7 @@ Section lft_contexts.
with ">[HE HL1]" as "H".
{ move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
- - iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
+ - iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static. set_solver.
- iDestruct "HL1" as "[HL1 HL2]". iDestruct "HE" as "[HE1 HE2]".
iMod (Hκ with "HE1 HL1") as (q') "[Htok' Hclose]". done.
iMod ("IH" with "HE2 HL2") as (q'') "[Htok'' Hclose']".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index e610b8bf381b46b06f85a023a777630a8cc343a5..a3336492d1b6eb41d9027dec20901eeeef6629d9 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -151,7 +151,7 @@ Section typing_rules.
typed_body E L C T (Newlft ;; e).
Proof.
iIntros (Hc) "He". iIntros (tid qE) "#LFT Htl HE HL HC HT".
- iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
+ iMod (lft_create ⊤ with "LFT") as (Λ) "[Htk #Hinh]"; try done.
set (κ' := foldr (∪) static κs). wp_seq.
iApply ("He" $! (κ' ∪ Λ) with "LFT Htl HE [HL Htk] HC HT").
rewrite /llctx_interp big_sepL_cons. iFrame "HL".
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 2101ab0ccd5fde03774ea4065e15403d0573431b..8713d718c9e9838c6024f88c56dcd244acded282 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -126,7 +126,7 @@ Section refcell.
iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
- iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ - iMod (lft_create ⊤ with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; try done.
iMod (own_alloc (● Some (to_agree ν, Cinr ((1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 5a12ad7f7a876cf68274f5030851e6ba20575ef4..5ac3d77e834135ee77c70a6707c59ea4be6a4343 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -199,7 +199,7 @@ Section refcell_functions.
iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _. iFrame.
iSplitR; first by rewrite /= Hag agree_idemp. iFrame "Hshr". iExists _. iFrame.
rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ - iMod (lft_create ⊤ with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; try done.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
@@ -277,7 +277,7 @@ Section refcell_functions.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
destruct st as [[?[|[]|]]|]; try done.
- iMod (lft_create with "LFT") as (ν) "[Htok #Hhν]". done.
+ iMod (lft_create ⊤ with "LFT") as (ν) "[Htok #Hhν]"; try done.
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc, (op_local_update_discrete _ _ (writing_st ν)). }
iMod (rebor _ _ (β ∪ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/unsafe/rwlock/rwlock.v
index dc70a67ca0f57a3f66cf6da29cf92638ddceaba2..5d06961185477661743ce9183bd9ff8e8ea5baaf 100644
--- a/theories/typing/unsafe/rwlock/rwlock.v
+++ b/theories/typing/unsafe/rwlock/rwlock.v
@@ -123,7 +123,7 @@ Section rwlock.
solve_ndisj. }
clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
- iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ - iMod (lft_create ⊤ with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; try done.
iMod (own_alloc (● Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
diff --git a/theories/typing/unsafe/rwlock/rwlock_code.v b/theories/typing/unsafe/rwlock/rwlock_code.v
index 620554ebdd72be3974a194b3292dc94c6e5a5bd6..271b7dbd73d91d27691ca942f77a2ff335bbefcd 100644
--- a/theories/typing/unsafe/rwlock/rwlock_code.v
+++ b/theories/typing/unsafe/rwlock/rwlock_code.v
@@ -206,7 +206,8 @@ Section rwlock_functions.
iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _.
iFrame "∗#". iSplitR; first by rewrite /= Hag agree_idemp.
rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". solve_ndisj.
+ - iMod (lft_create ⊤ with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]";
+ first done; first solve_ndisj. iSpecialize ("Hhν" $! _).
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".