Commit 757490f7 by Ralf Jung

### make a user-mask available inside lifetime logic view shifts

parent df39e04f
Pipeline #25962 passed with stage
in 30 minutes and 5 seconds
 ... ... @@ -29,7 +29,7 @@ Implicit Types κ : lft. Lemma bor_acc_atomic_cons E κ P : ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗ (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨ (▷ P ∗ ∀ Q, ▷ (▷ Q ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True). Proof. iIntros (?) "#LFT HP". ... ... @@ -55,7 +55,7 @@ Qed. Lemma bor_acc_cons E q κ P : ↑lftN ⊆ E → lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ} Q ∗ q.[κ]. ∀ Q, ▷ (▷ Q ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ} Q ∗ q.[κ]. Proof. iIntros (?) "#LFT HP Htok". iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & \$ & Hclose)"; first done. ... ...
 ... ... @@ -6,6 +6,9 @@ From iris.bi Require Import fractional. Set Default Proof Using "Type". Definition lftN : namespace := nroot .@ "lft". (** A mask inside the lifetime logic namespace that users may use. This is still available in the "consequence" view shift of borrow accessors. *) Definition lft_userN : namespace := nroot .@ "lft" .@ "usr". Module Type lifetime_sig. (** CMRAs needed by the lifetime logic *) ... ... @@ -93,7 +96,7 @@ Module Type lifetime_sig. Parameter lft_dead_static : [† static] -∗ False. Parameter lft_create : ∀ E, ↑lftN ⊆ E → lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,∅}▷=∗ [†κ]). lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,↑lft_userN}▷=∗ [†κ]). Parameter bor_create : ∀ E κ P, ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P). Parameter bor_fake : ∀ E κ P, ... ... @@ -123,11 +126,11 @@ Module Type lifetime_sig. ([†κ] ∗ |={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 -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ]. ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ]. Parameter bor_acc_atomic_strong : ∀ E κ P, ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗ (∃ κ', κ ⊑ κ' ∗ ▷ P ∗ ∀ Q, ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨ ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True). (* Because Coq's module system is horrible, we have to repeat properties of lft_incl here ... ...
 ... ... @@ -55,7 +55,7 @@ Proof. Qed. Lemma add_vs Pb Pb' P Q Pi κ : ▷ (Pb ≡ (P ∗ Pb')) -∗ lft_vs κ Pb Pi -∗ (▷ Q -∗ [†κ] ={∅}=∗ ▷ P) -∗ ▷ (Pb ≡ (P ∗ Pb')) -∗ lft_vs κ Pb Pi -∗ (▷ Q -∗ [†κ] ={↑lft_userN}=∗ ▷ P) -∗ lft_vs κ (Q ∗ Pb') Pi. Proof. iIntros "#HEQ Hvs HvsQ". iApply (lft_vs_cons with "[-Hvs] Hvs"). ... ... @@ -148,7 +148,7 @@ Qed. Lemma bor_acc_strong E q κ P : ↑lftN ⊆ E → lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗ ∀ Q, ▷(▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ]. ∀ Q, ▷(▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ]. Proof. unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok". iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)". ... ... @@ -215,7 +215,7 @@ Lemma bor_acc_atomic_strong E κ P : ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗ (∃ κ', κ ⊑ κ' ∗ ▷ P ∗ ∀ Q, ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨ ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True). Proof. iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor. ... ...
 ... ... @@ -4,9 +4,11 @@ From lrust.lifetime Require Export lifetime_sig. Set Default Proof Using "Type". Import uPred. Definition borN : namespace := lftN .@ "bor". Definition inhN : namespace := lftN .@ "inh". Definition mgmtN : namespace := lftN .@ "mgmt". (** We put borrows into the "user" namespace, so that they are available in [lft_vs]. *) Definition borN : namespace := lft_userN .@ "bor". Definition atomic_lft := positive. (* HACK : We need to make sure this is not in the top-level context, ... ... @@ -140,7 +142,7 @@ Section defs. own_cnt κ (● n) ∗ ∀ I : gmap lft lft_names, lft_vs_inv_go κ lft_inv_alive I -∗ ▷ Pb -∗ lft_dead κ ={↑borN}=∗ ={↑lft_userN}=∗ lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I. Definition lft_inv_alive_go (κ : lft) ... ... @@ -268,7 +270,7 @@ Lemma lft_vs_unfold κ Pb Pi : lft_vs κ Pb Pi ⊣⊢ ∃ n : nat, own_cnt κ (● n) ∗ ∀ I : gmap lft lft_names, lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={↑borN}=∗ lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={↑lft_userN}=∗ lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n). Proof. done. Qed. ... ...
 ... ... @@ -490,7 +490,7 @@ Proof. Qed. Lemma lft_vs_cons κ Pb Pb' Pi : (▷ Pb'-∗ [†κ] ={↑borN}=∗ ▷ Pb) -∗ (▷ Pb'-∗ [†κ] ={↑lft_userN}=∗ ▷ Pb) -∗ lft_vs κ Pb Pi -∗ lft_vs κ Pb' Pi. Proof. iIntros "Hcons Hvs". rewrite !lft_vs_unfold. ... ...
 ... ... @@ -41,7 +41,7 @@ Section lft_contexts. (* Local lifetime contexts. *) Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ := let κ' := lft_intersect_list (x.2) in (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,∅}▷=∗ [†κ0]))%I. (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,↑lft_userN}▷=∗ [†κ0]))%I. Global Instance llctx_elt_interp_fractional x : Fractional (llctx_elt_interp x). Proof. ... ...
 ... ... @@ -85,7 +85,7 @@ Section rc. because [weak_new] cannot prove ty_shr, even for a dead lifetime. *) (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗ □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))%I. □ (1.[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]))%I. Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty). Proof. unfold rc_persist, tc_opaque. apply _. Qed. ... ... @@ -247,16 +247,16 @@ Section code. (((⌜strong = 1%positive⌝ ∗ (∃ weak : Z, (l +ₗ 1) ↦ #weak ∗ ((⌜weak = 1⌝ ∗ |={⊤,∅}▷=> † l…(2 + ty.(ty_size)) ∗ |={⊤,↑lft_userN}▷=> † l…(2 + ty.(ty_size)) ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ na_own tid F) ∨ (⌜weak > 1⌝ ∗ ((l ↦ #1 -∗ (l +ₗ 1) ↦ #weak ={⊤}=∗ na_own tid F ∗ ty_own (rc ty) tid [ #l ]) ∧ (l ↦ #0 -∗ (l +ₗ 1) ↦ #(weak - 1) ={⊤,∅}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ ={⊤,↑lft_userN}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ ((l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝) ={⊤}=∗ na_own tid F)))))) ∧ (l ↦ #0 ={⊤,∅}▷=∗ (l ↦ #0 ={⊤,↑lft_userN}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size)) ∗ na_own tid F ∗ (na_own tid F ={⊤}=∗ ∃ weak : Z, (l +ₗ 1) ↦ #weak ∗ ... ... @@ -295,7 +295,7 @@ Section code. iMod (own_update_2 with "Hst Htok") as "Hst". { apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)). apply cancel_local_update_unit, _. } rewrite -[in (1).[ν]%I]Hqq' -[(|={∅,⊤}=>_)%I]fupd_trans. rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans. iApply step_fupd_mask_mono; last iMod ("Hνend" with "[\$Hν \$Hν1]") as "H†"; try done. iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro. ... ... @@ -307,7 +307,7 @@ Section code. iMod ("Hclose" with "[-Htok Hν1]") as "\$"; last by auto 10 with iFrame. iFrame. iExists _. auto with iFrame. ++ iIntros "Hl1 Hl2". rewrite -[in (1).[ν]%I]Hqq' -[(|={∅,⊤}=>_)%I]fupd_trans. rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans. iApply step_fupd_mask_mono; last iMod ("Hνend" with "[\$Hν \$Hν1]") as "H†"; try done. iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro. ... ... @@ -325,7 +325,7 @@ Section code. { apply auth_update. etrans. - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_unit, _. - apply (op_local_update _ _ (Some (Cinr (Excl tt)), 0%nat)). auto. } rewrite -[(|={∅,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'. rewrite -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'. iApply step_fupd_mask_mono; last iMod ("Hνend" with "[\$Hν \$Hν1]") as "H†"; try done. iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro. ... ...
 ... ... @@ -15,7 +15,7 @@ Section ref_functions. own γ (◯ reading_stR q ν) -∗ ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗ own γ (● (refcell_st_to_R \$ Some (ν, false, q', n)) ⋅ ◯ reading_stR q ν) ∗ ((1).[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗ ((1).[ν] ={↑lftN,↑lft_userN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗ (∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗ ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1). Proof. ... ... @@ -162,7 +162,7 @@ Section ref_functions. as (q' n) "(H↦lrc & >% & H●◯ & H† & Hq' & Hshr)". iDestruct "Hq'" as (q'') ">[% Hν']". wp_read. wp_let. wp_op. wp_write. iAssert (|={↑lftN,∅}▷=> refcell_inv tid lrc γ β ty')%I iAssert (|={↑lftN,↑lft_userN}▷=> refcell_inv tid lrc γ β ty')%I with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV". { iDestruct (own_valid with "H●◯") as %[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included] ... ... @@ -180,10 +180,10 @@ Section ref_functions. { apply auth_update_dealloc. rewrite -(agree_idemp (to_agree _)) !pair_op Some_op. apply (cancel_local_update_unit (reading_stR q ν)), _. } iApply step_fupd_intro; first set_solver. iExists (q+q'')%Qp. iFrame. iApply step_fupd_intro; first solve_ndisj. iExists (q+q'')%Qp. iFrame. by rewrite assoc (comm _ q0 q). } wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done. iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq. iApply (wp_step_fupd with "INV"); [solve_ndisj..|]. wp_seq. iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[\$INV] Hna") as "[Hβ Hna]". iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)] with "[] LFT HE Hna HL Hk"); ... ...
 ... ... @@ -49,7 +49,7 @@ Section refcell_inv. (* Not borrowed. *) &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid) | Some (ν, rw, q, _) => (1.[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗ (1.[ν] ={↑lftN,↑lft_userN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗ (∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]) ∗ if rw then (* Mutably borrowed. *) True else (* Immutably borrowed. *) ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ... ... @@ -155,7 +155,7 @@ Section refcell. - iMod (own_alloc (● (refcell_st_to_R \$ Some (static, true, (1/2)%Qp, n)))) as (γ) "Hst". { by apply auth_auth_valid. } iFrame "Htok'". iExists γ, _. iFrame. iSplitR. { rewrite -step_fupd_intro. auto. set_solver+. } { rewrite -step_fupd_intro. auto. solve_ndisj. } iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|]. iApply lft_tok_static. Qed. ... ...
 ... ... @@ -127,7 +127,7 @@ Section refmut_functions. iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done. iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|]. iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_read. wp_let. wp_op. wp_write. iAssert (|={↑lftN,∅}▷=> refcell_inv tid lrc γ β ty')%I iAssert (|={↑lftN,↑lft_userN}▷=> refcell_inv tid lrc γ β ty')%I with "[H↦lrc H● H◯ Hν INV]" as "INV". { iDestruct (own_valid_2 with "H● H◯") as %[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _] ... ... @@ -148,11 +148,11 @@ Section refmut_functions. iDestruct "INV" as "(H† & Hq & _)". rewrite /= (_:Z.neg (1%positive ⋅ n') + 1 = Z.neg n'); last (rewrite pos_op_plus; lia). iFrame. iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done]. iApply step_fupd_intro; [solve_ndisj|]. iSplitL; [|done]. iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame. rewrite assoc (comm _ q'' q) //. } wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done. iApply (wp_step_fupd with "INV"); [set_solver|]. wp_seq. iIntros "{Hb} Hb !>". iApply (wp_step_fupd with "INV"); [solve_ndisj|]. wp_seq. iIntros "{Hb} Hb !>". iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]". iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq. iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)] ... ...
 ... ... @@ -39,7 +39,7 @@ Section rwlock_inv. | Some (Cinr (agν, q, n)) => (* Locked for read. *) ∃ (ν : lft) q', agν ≡ to_agree ν ∗ □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗ □ (1.[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]) ∗ ([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗ ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ... ...
 ... ... @@ -183,7 +183,7 @@ Section rwlock_functions. iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗ ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗ own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗ ((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I ((1).[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]))%I with "[> Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)". { destruct st' as [[|[[agν q] n]|]|]; try done. ... ...
 ... ... @@ -23,7 +23,7 @@ Section rwlockreadguard. ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗ α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗ q.[ν] ∗ own γ (◯ reading_st q ν) ∗ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) (1.[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]) | _ => False end; ty_shr κ tid l := ... ...
 ... ... @@ -95,8 +95,9 @@ Section rwlockreadguard_functions. rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv. iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->. iApply (step_fupd_mask_mono (↑lftN ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN))); last iApply (step_fupd_mask_frame_r _ ∅); [try set_solver..|]; [apply union_least; solve_ndisj|]. last iApply (step_fupd_mask_frame_r _ (↑lft_userN)); [set_solver+ || solve_ndisj..| |]. { (* FIXME [solve_ndisj] fails. *) apply: disjoint_difference_r1. solve_ndisj. } iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†". iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame. iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc. ... ...
 ... ... @@ -182,7 +182,7 @@ Section typing_rules. iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)". iSpecialize ("Hend" with "Htok"). wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done. iApply (wp_step_fupd with "Hend"); first set_solver. wp_seq. iApply (wp_step_fupd with "Hend"); first solve_ndisj. wp_seq. iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]"). iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto. Qed. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment