Commit a772befe authored by Ralf Jung's avatar Ralf Jung

update dependencies; fix for step_fupd notation change

parent bcf15e3d
Pipeline #30791 passed with stage
in 33 minutes and 26 seconds
......@@ -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}%"]
......
......@@ -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.
......
......@@ -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,
......
......@@ -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Λ")
......
......@@ -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.
......
......@@ -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.
......
......@@ -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. *)
......
......@@ -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
......
......@@ -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.
......
......@@ -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]
......
......@@ -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)
......
......@@ -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.
......
......@@ -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 _]
......
......@@ -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'.[ν]
......
......@@ -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.
......
......@@ -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 :=
......
......@@ -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])]
......
......@@ -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.
......
......@@ -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 "$".
......
......@@ -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 "$".
......
......@@ -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)".
......
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