Commit 4e268989 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Dynamic masks for lifetimes.

parent e7e16b65
......@@ -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κ' _]".
......
......@@ -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.
......@@ -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}=
......
......@@ -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".
......
......@@ -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.