diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v index 0e21a9807ddd3e961068f171bf310dfbf875f906..56ed0432524d70a176ae66629fcb0b5a16321e17 100644 --- a/theories/typing/lib/arc.v +++ b/theories/typing/lib/arc.v @@ -105,7 +105,7 @@ Section arc. | _ => False end; ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗ - â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] + â–¡ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌠-∗ q.[κ] ={F}[F∖↑shrN]â–·=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗ arc_persist tid ν γ l' ty ∗ &at{κ, arc_shrN}(arc_tok γ q') @@ -227,7 +227,7 @@ Section arc. | _ => False end; ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗ - â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] + â–¡ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌠-∗ q.[κ] ={F}[F∖↑shrN]â–·=∗ q.[κ] ∗ ∃ γ ν, arc_persist tid ν γ l' ty ∗ &at{κ, arc_shrN}(weak_tok γ) |}%I. diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v index acc66566aa9f646ab61f7103a0a76d4ad2c59570..2ca7e007c293353579d63266da7192d11a9b7c07 100644 --- a/theories/typing/lib/mutex/mutexguard.v +++ b/theories/typing/lib/mutex/mutexguard.v @@ -38,7 +38,7 @@ Section mguard. | _ => False end; ty_shr κ tid l := ∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗ - â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α⊓κ] + â–¡ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌠-∗ q.[α⊓κ] ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) (α⊓κ) tid (l' +â‚— 1) ∗ q.[α⊓κ] |}%I. Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed. diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v index 38f7b51a9aec4418f101b6969ecd401d80edf71e..84266a6d561488238c6678760d0a11e50e1eef9b 100644 --- a/theories/typing/lib/rc/rc.v +++ b/theories/typing/lib/rc/rc.v @@ -121,7 +121,7 @@ Section rc. | _ => False end; ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗ - â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] + â–¡ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌠-∗ q.[κ] ={F}[F∖↑shrN]â–·=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗ rc_persist tid ν γ l' ty ∗ &na{κ, tid, rc_shrN}(own γ (rc_tok q')) diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v index c7f3a8b02fad971c489099dca5fbd60d72ed301e..5f2f3df241ec6ec6e1eba6011dcfe6c7daa25ade 100644 --- a/theories/typing/lib/rc/weak.v +++ b/theories/typing/lib/rc/weak.v @@ -18,7 +18,7 @@ Section weak. | _ => False end; ty_shr κ tid l := ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗ - â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] + â–¡ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌠-∗ q.[κ] ={F}[F∖↑shrN]â–·=∗ q.[κ] ∗ ∃ γ ν, rc_persist tid ν γ l' ty ∗ &na{κ, tid, rc_shrN}(own γ weak_tok) |}%I. diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v index a435bbda977aeb50a7b858c5e2f5d4d2a9e6432b..ff6e32e052f9d43d741d7d1e185d144127816dd7 100644 --- a/theories/typing/lib/refcell/refmut.v +++ b/theories/typing/lib/refcell/refmut.v @@ -33,7 +33,7 @@ Section refmut. ty_shr κ tid l := ∃ (lv lrc : loc), &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗ - â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ⊓ κ] + â–¡ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌠-∗ q.[α ⊓ κ] ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I. Next Obligation. iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_". diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v index 7bffa2d3c7fba3e3ed8a8721ab25d5382dbff156..f6ba19e93bf3689907f4c15b46cc800d6764e2c4 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 ∪ ↑lftN ⊆ 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 0c345c96f72b6ef25c38384ffdb50be8a51adef1..a03beedfe019966daaf34404c563faf4553d7a4f 100644 --- a/theories/typing/own.v +++ b/theories/typing/own.v @@ -60,7 +60,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 ∪ ↑lftN ⊆ F⌠-∗ q.[κ] ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I |}. Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed. Next Obligation. diff --git a/theories/typing/programs.v b/theories/typing/programs.v index 8b387f12b8574e4d4653f89359fe99a5ceb6e9e6..1a5e14ff67cafa173ec02f69fb38a98b53d13825 100644 --- a/theories/typing/programs.v +++ b/theories/typing/programs.v @@ -65,7 +65,7 @@ Section typing. (** Writing and Reading **) Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ := - (â–¡ ∀ v tid F qmax qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌠→ + (â–¡ ∀ v tid F qmax qL, ⌜↑lftN ∪ (↑lrustN) ⊆ F⌠→ lft_ctx -∗ elctx_interp E -∗ llctx_interp_noend qmax L qL -∗ ty1.(ty_own) tid [v] ={F}=∗ ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌠∗ l ↦∗ vl ∗ (â–· l ↦∗: ty.(ty_own) tid ={F}=∗ @@ -85,7 +85,7 @@ Section typing. that nobody could possibly have changed the vl (because only half the fraction was given). So we go with the definition that is easier to prove. *) Definition typed_read_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ := - (â–¡ ∀ v tid F qmax qL, ⌜lftE ∪ ↑lrustN ⊆ F⌠→ + (â–¡ ∀ v tid F qmax qL, ⌜↑lftN ∪ ↑lrustN ⊆ F⌠→ lft_ctx -∗ elctx_interp E -∗ na_own tid F -∗ llctx_interp_noend qmax L qL -∗ ty1.(ty_own) tid [v] ={F}=∗ ∃ (l : loc) vl q, ⌜v = #l⌠∗ l ↦∗{q} vl ∗ â–· ty.(ty_own) tid vl ∗ diff --git a/theories/typing/type.v b/theories/typing/type.v index 627b5111825200b1cd34bd5763b147881bcbec2b..61c8cf75822784ba847840cf5d3fcd6f67ce42e0 100644 --- a/theories/typing/type.v +++ b/theories/typing/type.v @@ -13,7 +13,6 @@ Class typeG Σ := TypeG { type_frac_borrowG :> frac_borG Σ }. -Definition lftE : coPset := ↑lftN. Definition lrustN := nroot .@ "lrust". Definition shrN := lrustN .@ "shr". @@ -40,7 +39,7 @@ Record type `{!typeG Σ} := nicer (they would otherwise require a "∨ â–¡|=>[†κ]"), and (b) so that we can have emp == sum []. *) - ty_share E κ l tid q : lftE ⊆ E → + ty_share E κ l tid q : ↑lftN ⊆ E → lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid l ∗ q.[κ]; ty_shr_mono κ κ' tid l : @@ -175,7 +174,7 @@ Section ofe. Let P (x : T) : Prop := (∀ κ tid l, Persistent (x.2 κ tid l)) ∧ (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1âŒ) ∧ - (∀ E κ l tid q, lftE ⊆ E → + (∀ E κ l tid q, ↑lftN ⊆ E → lft_ctx -∗ &{κ} (l ↦∗: λ vs, x.1.2 tid vs) -∗ q.[κ] ={E}=∗ x.2 κ tid l ∗ q.[κ]) ∧ (∀ κ κ' tid l, κ' ⊑ κ -∗ x.2 κ tid l -∗ x.2 κ' tid l). @@ -395,7 +394,7 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset := Class Copy `{!typeG Σ} (t : type) := { copy_persistent tid vl : Persistent (t.(ty_own) tid vl); copy_shr_acc κ tid E F l q : - lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F → + ↑lftN ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F → lft_ctx -∗ t.(ty_shr) κ tid l -∗ na_own tid F -∗ q.[κ] ={E}=∗ ∃ q', na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗ â–·(l ↦∗{q'}: t.(ty_own) tid) ∗ diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v index 674d69f5d833fcd74fd0c8a66e8afaa50b02b56e..f5ca1e03f8ffc49013949cb00ec17684d77db220 100644 --- a/theories/typing/uniq_bor.v +++ b/theories/typing/uniq_bor.v @@ -16,7 +16,7 @@ Section uniq_bor. end; ty_shr κ' tid l := ∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗ - â–¡ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ⊓κ'] + â–¡ ∀ F q, ⌜↑shrN ∪ ↑lftN ⊆ F⌠-∗ q.[κ⊓κ'] ={F}[F∖↑shrN]â–·=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ'] |}%I. Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed. diff --git a/theories/typing/util.v b/theories/typing/util.v index 857d6a4297ecfe38027801671b1c65840fa9c652..6bf47379bbe0c32b3a0703a7064fbe2cfa12efa0 100644 --- a/theories/typing/util.v +++ b/theories/typing/util.v @@ -25,10 +25,10 @@ Section util. *) Lemma delay_sharing_later N κ l ty tid : - lftE ⊆ N → + ↑lftN ⊆ 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 ∪ ↑lftN ⊆ 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)". @@ -47,10 +47,10 @@ Section util. Qed. Lemma delay_sharing_nested N κ κ' κ'' l ty tid : - lftE ⊆ N → + ↑lftN ⊆ 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 ∪ ↑lftN ⊆ 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)".