From e0d1432e4b8a70e51eafa289088e4078eabd05e0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 3 Jul 2020 17:28:07 +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/logic/gps.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 | 4 ++--
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 ++++----
22 files changed, 37 insertions(+), 37 deletions(-)
diff --git a/opam b/opam
index 866ad3bd..e4b0f02e 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-06-19.2.6c60d47a") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-07-03.0.ce4c6d6b") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index cef8a16d..e87fcc14 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -149,7 +149,7 @@ Proof.
Qed.
Lemma bor_later `{LatBottom Lat} E κ P :
- ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.
+ ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ &{κ}(▷ P) ={E}[E∖↑lftN]▷=∗ &{κ}P.
Proof.
iIntros (?) "#LFT Hb".
iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|H]"; first done.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 9c3fca84..765bb4b5 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -109,7 +109,7 @@ Module Type lifetime_sig.
Parameter lft_dead_static : [†static] -∗ False.
Parameter lft_create : ∀ `{LatBottom Lat} E, ↑lftN ⊆ E →
- ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ E0, E0}▷=∗ [†κ]).
+ ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ E0}[E0]▷=∗ [†κ]).
Parameter bor_create : ∀ `{LatBottom Lat} E κ P,
↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ ▷ P ={E}=∗ &{κ}P ∗ ([†κ] ={E}=∗ ▷ P).
Parameter bor_fake : ∀ `{LatBottom Lat} E κ P,
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index df30fe50..6e71e3e0 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -152,7 +152,7 @@ Proof.
Qed.
Lemma lft_create E :
- ↑lftN ⊆ E → ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ E0,E0}▷=∗ [†κ]).
+ ↑lftN ⊆ E → ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ E0}[E0]▷=∗ [†κ]).
Proof.
iIntros (?) "#LFT".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -176,7 +176,7 @@ Proof.
iDestruct (monPred_in_intro True%I with "[//]") as (V) "[H _]".
by rewrite -(lat_bottom_sqsubseteq V). }
clear I A HΛ. iIntros "!# HΛ".
- iApply (step_fupd_mask_mono (↑lftN ∪ E0) _ _ ((↑lftN ∪ E0)∖↑mgmtN)); [|done|].
+ iApply (step_fupd_mask_mono (↑lftN ∪ E0) _ ((↑lftN ∪ E0)∖↑mgmtN)); [|done|].
{ assert (↑mgmtN ## E0) by (pose proof E0_lftN_disj; solve_ndisj). set_solver. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
{ rewrite <-union_subseteq_l. solve_ndisj. }
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index ce337cab..68c5d13a 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -133,7 +133,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_weak
(∀ t'' , ⌜(t' < t'')%positive⌠-∗
▷ GPS_SWSharedWriter l t'' s'' vw γ ={E ∖ ↑N}=∗
(<obj> (▷ Q1 t' s' ={E ∖ ↑N}=∗ ▷ IP false l γ t' s' #vr)) ∗
- |={E ∖ ↑N,E'}▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw))) ) ∧
+ |={E ∖ ↑N}[E']▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw))) ) ∧
▷ (∀ (v: lit), ⌜lit_neq vr v⌠-∗
<obj> ((IP false l γ t' s' #v ={E ∖ ↑N}=∗ IP false l γ t' s' #v ∗ R t' s' v) ∧
(IP true l γ t' s' #v ={E ∖ ↑N}=∗ IP true l γ t' s' #v ∗ R t' s' v) ∧
@@ -183,7 +183,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_strong
(∀ t'' , ⌜(t' < t'')%positive⌠-∗ ▷ GPS_SWSharedWriter l t'' s'' vw γ -∗
(if dropR then ▷ GPS_SWSharedReader l t'' s'' vw qs γ else True) ={E ∖ ↑N}=∗
(<obj> (▷ Q1 t' s' ={E ∖ ↑N}=∗ ▷ IP false l γ t' s' #vr)) ∗
- |={E ∖ ↑N,E'}▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw)) ) ∧
+ |={E ∖ ↑N}[E']▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw)) ) ∧
▷ (∀ (v: lit), ⌜lit_neq vr v⌠-∗
<obj> ((IP false l γ t' s' #v ={E ∖ ↑N}=∗ IP false l γ t' s' #v ∗ R t' s' v) ∧
(IP true l γ t' s' #v ={E ∖ ↑N}=∗ IP true l γ t' s' #v ∗ R t' s' v))))%I in
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 9c695f63..055af496 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) : vProp Σ :=
let κ' := lft_intersect_list (x.2) in
- (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†κ0]))%I.
+ (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†κ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 3cc26d38..c4335c6b 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -34,7 +34,7 @@ Section arc.
(* because [weak_new] cannot prove ty_shr, even for a dead *)
(* lifetime. *)
(ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
- □ (1.[ν] ={↑lftN ∪ ↑histN ∪ ↑arc_endN,↑histN}▷=∗
+ □ (1.[ν] ={↑lftN ∪ ↑histN ∪ ↑arc_endN}[↑histN]▷=∗
[†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ ⎡ †l…(2 + ty.(ty_size)) ⎤))%I.
Global Instance arc_persist_ne tid ν γi γs γw γsw l n :
@@ -152,7 +152,7 @@ Section arc.
ty_shr κ tid l :=
∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ]
- ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν, κ ⊑ ν ∗
+ ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν, κ ⊑ ν ∗
arc_persist tid ν γi γs γw γsw l' ty ∗
∃ q' ts tw, shared_arc_local l' γs γw ts tw ∗
&at{κ, arc_shrN}(strong_arc ts q' l' γi γs γw γsw)
@@ -291,7 +291,7 @@ Section arc.
ty_shr κ tid l :=
∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ]
- ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν,
+ ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν,
arc_persist tid ν γi γs γw γsw l' ty ∗
∃ q' ts tw, shared_arc_local l' γs γw ts tw ∗
&at{κ, arc_shrN}(weak_arc tw q' l' γi γs γw γsw)
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 0834d1ed..28f36d79 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -38,7 +38,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 a098f55a..e1f93314 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -86,7 +86,7 @@ Section rc.
because [weak_new] cannot prove ty_shr, even for a dead
lifetime. *)
(ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
- □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]))%I.
+ □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]))%I.
Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
Proof. unfold rc_persist, tc_opaque. apply _. Qed.
@@ -124,7 +124,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.
@@ -254,16 +254,16 @@ Section code.
(((⌜strong = 1%positive⌠∗
(∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
((⌜weak = 1⌠∗
- |={⊤,↑histN}▷=> ⎡†l…(2 + ty.(ty_size))⎤ ∗
+ |={⊤}[↑histN]▷=> ⎡†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)
- ={⊤,↑histN}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
+ ={⊤}[↑histN]▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
((l +â‚— 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)âŒ)
={⊤}=∗ na_own tid F)))))) ∧
- (l ↦ #0 ={⊤,↑histN}▷=∗
+ (l ↦ #0 ={⊤}[↑histN]▷=∗
▷ (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 77586f49..7f441063 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 4a42835e..81ac8abd 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -14,7 +14,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 ∪ ↑histN,↑histN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
+ ((1).[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
(∃ q'', ⌜(q' + q'' = 1)%Qp⌠∗ q''.[ν]) ∗
ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1).
Proof.
@@ -161,7 +161,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 ∪ ↑histN,↑histN}▷=> refcell_inv tid lrc γ β ty')%I
+ iAssert (|={↑lftN ∪ ↑histN}[↑histN]▷=> 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 1341fca8..ec39aa1f 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -48,7 +48,7 @@ Section refcell_inv.
(* Not borrowed. *)
&{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
| Some (ν, rw, q, _) =>
- (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ &{α}((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 9161ac9d..0f51cf44 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -33,7 +33,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 bc776aba..7b7b7785 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -126,7 +126,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 ∪ ↑histN,↑histN}▷=> refcell_inv tid lrc γ β ty')%I
+ iAssert (|={↑lftN ∪ ↑histN}[↑histN]▷=> 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 248132e6..2dab818e 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -178,7 +178,7 @@ Section rwlock_inv.
GPS_SWSharedReader l t () #0 1%Qp γ
| Some (inr (ν, q, n)) => (* Locked for read. *)
GPS_SWSharedWriter l t () #(Z.pos n) γ ∗
- ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+ ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]) ∗
([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
(□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌠∗
q'.[ν] ∗
@@ -277,7 +277,7 @@ Section rwlock_inv.
| None => (* Not locked. *)
&{α}tyO
| Some (inr (ν, q, n)) => (* Locked for read. *)
- ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+ ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]) ∗
([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
(□ tyS (α ⊓ ν)) ∗ ⌜(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 7acb5a20..227757d1 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -210,7 +210,7 @@ Section rwlock_functions.
(∃ qν ν, (qν).[ν] ∗
(□ tyS (β ⊓ ν)) ∗
rwown γs (reading_st qν ν) ∗
- (□ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν])) ∗
+ (□ ((1).[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν])) ∗
GPS_SWSharedReader lx t (() : unitProtocol) #(Z_of_rwlock_st st' + 1) qν γ))%I.
set Q1: time → () → vProp Σ :=
(λ t _, rwlock_interp γs β tyO tyS false lx γ t () #(Z_of_rwlock_st st'))%I.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 2f9d709e..d7b5b5fd 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -23,7 +23,7 @@ Section rwlockreadguard.
| [ #(LitLoc l) ] =>
∃ ν q γs β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
α ⊑ β ∗ q.[ν] ∗ rwown γs (reading_st q ν) ∗
- □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+ □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]) ∗
(∃ γ tyO tyS, (∃ t n, GPS_SWSharedReader l t () #n q γ) ∗
rwlock_proto l γ γs β tyO tyS tid ty)
| _ => False
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index ecd96a97..f76e7f02 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -125,7 +125,7 @@ Section rwlockreadguard_functions.
{ rewrite /Q1 Eqst. by iIntros "!> $". }
destruct CASE as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
- rewrite Hqrq'. iMod (rwown_update_read_dealloc_1 with "Hâ— Hâ—¯") as "Hâ—".
- iApply (step_fupd_mask_mono (↑lftN ∪ ↑histN) _ _ (↑histN));
+ iApply (step_fupd_mask_mono (↑lftN ∪ ↑histN) _ (↑histN));
[solve_ndisj|apply union_least; solve_ndisj|..].
iMod ("H†" with "Hν") as "Hν". iIntros "!> !>". iMod "Hν".
iMod ("Hh" with "Hν") as "Hb". iModIntro.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index fbf90449..baa57227 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -31,7 +31,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 3372eab6..0677b433 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -62,7 +62,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.
@@ -81,7 +81,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 522d5d80..e0cde6e6 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -16,7 +16,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.
@@ -33,7 +33,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 092d9384..1adf126a 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -20,15 +20,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 (monPred_in_intro with "Hbor") as (V) "[#Hin Hbor]".
@@ -58,7 +58,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.
iCombine "Hincl Hbor" as "Hinclbor".
--
GitLab