From a772befe97d78e1ea401a958de73a6fa98e070d4 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 2 Jul 2020 09:25:48 +0200 Subject: [PATCH] update dependencies; fix for step_fupd notation change --- opam | 2 +- theories/lifetime/lifetime.v | 2 +- theories/lifetime/lifetime_sig.v | 2 +- theories/lifetime/model/creation.v | 4 ++-- theories/typing/lft_contexts.v | 2 +- theories/typing/lib/arc.v | 6 +++--- theories/typing/lib/mutex/mutexguard.v | 2 +- theories/typing/lib/rc/rc.v | 10 +++++----- theories/typing/lib/rc/weak.v | 2 +- theories/typing/lib/refcell/ref_code.v | 4 ++-- theories/typing/lib/refcell/refcell.v | 2 +- theories/typing/lib/refcell/refmut.v | 2 +- theories/typing/lib/refcell/refmut_code.v | 2 +- theories/typing/lib/rwlock/rwlock.v | 2 +- theories/typing/lib/rwlock/rwlock_code.v | 2 +- theories/typing/lib/rwlock/rwlockreadguard.v | 2 +- theories/typing/lib/rwlock/rwlockreadguard_code.v | 2 +- theories/typing/lib/rwlock/rwlockwriteguard.v | 2 +- theories/typing/own.v | 4 ++-- theories/typing/uniq_bor.v | 4 ++-- theories/typing/util.v | 8 ++++---- 21 files changed, 34 insertions(+), 34 deletions(-) diff --git a/opam b/opam index 2c0379ff..bfd5401d 100644 --- a/opam +++ b/opam @@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries. """ depends: [ - "coq-iris" { (= "dev.2020-06-19.0.80be7f21") | (= "dev") } + "coq-iris" { (= "dev.2020-07-02.0.59a1ad49") | (= "dev") } ] build: [make "-j%{jobs}%"] diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v index 26eee181..183cdd37 100644 --- a/theories/lifetime/lifetime.v +++ b/theories/lifetime/lifetime.v @@ -116,7 +116,7 @@ Qed. Lemma bor_later E κ P : ↑lftN ⊆ E → - lft_ctx -∗ &{κ}(â–· P) ={E,E∖↑lftN}â–·=∗ &{κ}P. + lft_ctx -∗ &{κ}(â–· P) ={E}[E∖↑lftN]â–·=∗ &{κ}P. Proof. iIntros (?) "#LFT Hb". iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H†Hclose]]"; first done. diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v index 5374ca71..b7b0abf7 100644 --- a/theories/lifetime/lifetime_sig.v +++ b/theories/lifetime/lifetime_sig.v @@ -96,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_userN}â–·=∗ [†κ]). + 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, diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v index 383ed012..92016023 100644 --- a/theories/lifetime/model/creation.v +++ b/theories/lifetime/model/creation.v @@ -110,7 +110,7 @@ Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed. Lemma lft_create E : ↑lftN ⊆ E → - lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ â–¡ (1.[κ] ={↑lftN,↑lft_userN}â–·=∗ [†κ]). + lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ â–¡ (1.[κ] ={↑lftN}[↑lft_userN]â–·=∗ [†κ]). Proof. iIntros (?) "#LFT". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". @@ -128,7 +128,7 @@ Proof. iModIntro; iExists {[ Λ ]}. rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ". clear I A HΛ. iIntros "!# HΛ". - iApply (step_fupd_mask_mono (↑lftN) _ _ (↑lftN∖↑mgmtN)); [solve_ndisj..|]. + iApply (step_fupd_mask_mono (↑lftN) _ (↑lftN∖↑mgmtN)); [solve_ndisj..|]. iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". rewrite /lft_tok big_sepMS_singleton. iDestruct (own_valid_2 with "HA HΛ") diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v index 033c00f6..3017ca81 100644 --- a/theories/typing/lft_contexts.v +++ b/theories/typing/lft_contexts.v @@ -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,↑lft_userN}â–·=∗ [†κ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. diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v index 7a0f07c2..09a3d763 100644 --- a/theories/typing/lib/arc.v +++ b/theories/typing/lib/arc.v @@ -27,7 +27,7 @@ Section arc. (* because [weak_new] cannot prove ty_shr, even for a dead *) (* lifetime. *) (ty.(ty_shr) ν tid (l +â‚— 2) ∨ [†ν]) ∗ - â–¡ (1.[ν] ={↑lftN ∪ ↑arc_endN,↑lft_userN}â–·=∗ + â–¡ (1.[ν] ={↑lftN ∪ ↑arc_endN}[↑lft_userN]â–·=∗ [†ν] ∗ â–· (l +â‚— 2) ↦∗: ty.(ty_own) tid ∗ †l…(2 + ty.(ty_size))))%I. Global Instance arc_persist_ne tid ν γ l n : @@ -103,7 +103,7 @@ Section arc. ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗ â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] - ={F, F∖↑shrN}â–·=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗ + ={F}[F∖↑shrN]â–·=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗ arc_persist tid ν γ l' ty ∗ &at{κ, arc_shrN}(arc_tok γ q') |}%I. @@ -225,7 +225,7 @@ Section arc. ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗ â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] - ={F, F∖↑shrN}â–·=∗ q.[κ] ∗ ∃ γ ν, + ={F}[F∖↑shrN]â–·=∗ q.[κ] ∗ ∃ γ ν, arc_persist tid ν γ l' ty ∗ &at{κ, arc_shrN}(weak_tok γ) |}%I. Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed. diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v index 1f30e5f0..d0f2e34e 100644 --- a/theories/typing/lib/mutex/mutexguard.v +++ b/theories/typing/lib/mutex/mutexguard.v @@ -40,7 +40,7 @@ Section mguard. ty_shr κ tid l := ∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗ â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α⊓κ] - ={F, F∖↑shrN}â–·=∗ ty.(ty_shr) (α⊓κ) tid (l' +â‚— 1) ∗ q.[α⊓κ] + ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) (α⊓κ) tid (l' +â‚— 1) ∗ q.[α⊓κ] |}%I. Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed. (* This is to a large extend copy-pasted from RWLock's write guard. *) diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v index ddf5a893..529b04c8 100644 --- a/theories/typing/lib/rc/rc.v +++ b/theories/typing/lib/rc/rc.v @@ -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,↑lft_userN}â–·=∗ [†ν]))%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. @@ -123,7 +123,7 @@ Section rc. ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗ â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] - ={F, F∖↑shrN}â–·=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗ + ={F}[F∖↑shrN]â–·=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗ rc_persist tid ν γ l' ty ∗ &na{κ, tid, rc_shrN}(own γ (rc_tok q')) |}%I. @@ -247,16 +247,16 @@ Section code. (((⌜strong = 1%positive⌠∗ (∃ weak : Z, (l +â‚— 1) ↦ #weak ∗ ((⌜weak = 1⌠∗ - |={⊤,↑lft_userN}â–·=> †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) - ={⊤,↑lft_userN}â–·=∗ â–· (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 ={⊤,↑lft_userN}â–·=∗ + (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 ∗ diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v index e79b7885..e7071607 100644 --- a/theories/typing/lib/rc/weak.v +++ b/theories/typing/lib/rc/weak.v @@ -20,7 +20,7 @@ Section weak. ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗ â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] - ={F, F∖↑shrN}â–·=∗ q.[κ] ∗ ∃ γ ν, rc_persist tid ν γ l' ty ∗ + ={F}[F∖↑shrN]â–·=∗ q.[κ] ∗ ∃ γ ν, rc_persist tid ν γ l' ty ∗ &na{κ, tid, rc_shrN}(own γ weak_tok) |}%I. Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed. diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v index 7dc10476..5ad3cb65 100644 --- a/theories/typing/lib/refcell/ref_code.v +++ b/theories/typing/lib/refcell/ref_code.v @@ -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,↑lft_userN}â–·=∗ &{α}((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,↑lft_userN}â–·=> 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] diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v index c8acaf22..27a92d38 100644 --- a/theories/typing/lib/refcell/refcell.v +++ b/theories/typing/lib/refcell/refcell.v @@ -49,7 +49,7 @@ Section refcell_inv. (* Not borrowed. *) &{α}((l +â‚— 1) ↦∗: ty.(ty_own) tid) | Some (ν, rw, q, _) => - (1.[ν] ={↑lftN,↑lft_userN}â–·=∗ &{α}((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) diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v index c8e0f46c..0ba4b8eb 100644 --- a/theories/typing/lib/refcell/refmut.v +++ b/theories/typing/lib/refcell/refmut.v @@ -34,7 +34,7 @@ Section refmut. ∃ (lv lrc : loc), &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗ â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ⊓ κ] - ={F, F∖↑shrN}â–·=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I. + ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I. Next Obligation. iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_". Qed. diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v index d793d41e..bffd384c 100644 --- a/theories/typing/lib/refcell/refmut_code.v +++ b/theories/typing/lib/refcell/refmut_code.v @@ -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,↑lft_userN}â–·=> 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 _] diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v index 7ed012d3..97fcea2a 100644 --- a/theories/typing/lib/rwlock/rwlock.v +++ b/theories/typing/lib/rwlock/rwlock.v @@ -39,7 +39,7 @@ Section rwlock_inv. | Some (Cinr (agν, q, n)) => (* Locked for read. *) ∃ (ν : lft) q', agν ≡ to_agree ν ∗ - â–¡ (1.[ν] ={↑lftN,↑lft_userN}â–·=∗ [†ν]) ∗ + â–¡ (1.[ν] ={↑lftN}[↑lft_userN]â–·=∗ [†ν]) ∗ ([†ν] ={↑lftN}=∗ &{α}((l +â‚— 1) ↦∗: ty.(ty_own) tid)) ∗ ty.(ty_shr) (α ⊓ ν) tid (l +â‚— 1) ∗ ⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν] diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v index 932987cc..cbb8f13c 100644 --- a/theories/typing/lib/rwlock/rwlock_code.v +++ b/theories/typing/lib/rwlock/rwlock_code.v @@ -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,↑lft_userN}â–·=∗ [†ν]))%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. diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v index 0967717b..2773fa07 100644 --- a/theories/typing/lib/rwlock/rwlockreadguard.v +++ b/theories/typing/lib/rwlock/rwlockreadguard.v @@ -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,↑lft_userN}â–·=∗ [†ν]) + (1.[ν] ={↑lftN}[↑lft_userN]â–·=∗ [†ν]) | _ => False end; ty_shr κ tid l := diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v index ebf0a8e7..b5698df1 100644 --- a/theories/typing/lib/rwlock/rwlockreadguard_code.v +++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v @@ -83,7 +83,7 @@ Section rwlockreadguard_functions. iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|]. iDestruct "INV" as (st') "(Hlx & >Hâ— & Hst)". destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]. - + iAssert (|={⊤ ∖ ↑rwlockN,⊤ ∖ ↑rwlockN ∖ ↑lftN}â–·=> + + iAssert (|={⊤ ∖ ↑rwlockN}[⊤ ∖ ↑rwlockN ∖ ↑lftN]â–·=> (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I with "[Hâ— Hâ—¯ Hx' Hν Hst H†]" as "INV". { iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])] diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v index ef2e9d2b..aabe30e7 100644 --- a/theories/typing/lib/rwlock/rwlockwriteguard.v +++ b/theories/typing/lib/rwlock/rwlockwriteguard.v @@ -29,7 +29,7 @@ Section rwlockwriteguard. ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l↦∗{q} [ #l']) ∗ - â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ⊓ κ] ={F, F∖↑shrN}â–·=∗ + â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ⊓ κ] ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) (α ⊓ κ) tid (l' +â‚— 1) ∗ q.[α ⊓ κ] |}%I. Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed. Next Obligation. diff --git a/theories/typing/own.v b/theories/typing/own.v index 3ac859d6..22cfa025 100644 --- a/theories/typing/own.v +++ b/theories/typing/own.v @@ -61,7 +61,7 @@ Section own. end%I; ty_shr κ tid l := (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗ - â–¡ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] ={F,F∖↑shrN}â–·=∗ + â–¡ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I |}. Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed. Next Obligation. @@ -80,7 +80,7 @@ Section own. intros _ ty κ κ' tid l. iIntros "#Hκ #H". iDestruct "H" as (l') "[Hfb #Hvs]". iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok". - iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)); [solve_ndisj..|]. + iApply (step_fupd_mask_mono F _ (F∖↑shrN)); [solve_ndisj..|]. iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first solve_ndisj. iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext. iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$". diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v index a84b95b4..d2c80811 100644 --- a/theories/typing/uniq_bor.v +++ b/theories/typing/uniq_bor.v @@ -17,7 +17,7 @@ Section uniq_bor. ty_shr κ' tid l := ∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗ â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ⊓κ'] - ={F, F∖↑shrN}â–·=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ'] + ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ'] |}%I. Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed. Next Obligation. @@ -34,7 +34,7 @@ Section uniq_bor. iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0". { iApply lft_intersect_mono. iApply lft_incl_refl. done. } iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). - iIntros "!# * % Htok". iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)); try solve_ndisj. + iIntros "!# * % Htok". iApply (step_fupd_mask_mono F _ (F∖↑shrN)); try solve_ndisj. iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj. iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext. iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$". diff --git a/theories/typing/util.v b/theories/typing/util.v index ce4cb571..3dab3ddc 100644 --- a/theories/typing/util.v +++ b/theories/typing/util.v @@ -21,15 +21,15 @@ Section util. Lemma delay_borrow_step : lfeE ⊆ N → (∀ x, Persistent (Post x)) → lft_ctx -∗ &{κ} P -∗ - â–¡ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1 x,F2 x}â–·=∗ Post x ∗ Frame x) ={N}=∗ - â–¡ (∀ x, Pre x -∗ Frame x ={F1 x,F2 x}â–·=∗ Post x ∗ Frame x). + â–¡ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1 x}[F2 x]â–·=∗ Post x ∗ Frame x) ={N}=∗ + â–¡ (∀ x, Pre x -∗ Frame x ={F1 x}[F2 x]â–·=∗ Post x ∗ Frame x). *) Lemma delay_sharing_later N κ l ty tid : lftE ⊆ N → lft_ctx -∗ &{κ}(â–· l ↦∗: ty_own ty tid) ={N}=∗ â–¡ ∀ (F : coPset) (q : Qp), - ⌜↑shrN ∪ lftE ⊆ F⌠-∗ (q).[κ] ={F,F ∖ ↑shrN}â–·=∗ ty.(ty_shr) κ tid l ∗ (q).[κ]. + ⌜↑shrN ∪ lftE ⊆ F⌠-∗ (q).[κ] ={F}[F ∖ ↑shrN]â–·=∗ ty.(ty_shr) κ tid l ∗ (q).[κ]. Proof. iIntros (?) "#LFT Hbor". rewrite bor_unfold_idx. iDestruct "Hbor" as (i) "(#Hpb&Hpbown)". @@ -51,7 +51,7 @@ Section util. lftE ⊆ N → lft_ctx -∗ â–· (κ'' ⊑ κ ⊓ κ') -∗ &{κ'}(&{κ}(l ↦∗: ty_own ty tid)) ={N}=∗ â–¡ ∀ (F : coPset) (q : Qp), - ⌜↑shrN ∪ lftE ⊆ F⌠-∗ (q).[κ''] ={F,F ∖ ↑shrN}â–·=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ'']. + ⌜↑shrN ∪ lftE ⊆ F⌠-∗ (q).[κ''] ={F}[F ∖ ↑shrN]â–·=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ'']. Proof. iIntros (?) "#LFT #Hincl Hbor". rewrite bor_unfold_idx. iDestruct "Hbor" as (i) "(#Hpb&Hpbown)". -- GitLab