Commit 62664ef4 authored by Janno's avatar Janno

Merge branch 'no_more_C_scopes' into 'master'

Get rid of `%C` scopes.

See merge request !14
parents 180b660b dac06892
Pipeline #5285 failed with stage
in 3 minutes and 17 seconds
......@@ -22,7 +22,7 @@ Section Accessors.
(INFO : AuthType foundationG_info).
Lemma PSInv_Info_update E l v v':
physN E ( v')%C
physN E v'
PSCtx Info l 1 v
={E}=> Info l 1 v'.
Proof.
......
......@@ -469,7 +469,7 @@ Proof.
apply Qcle_ngt in Hle. by destruct q.
Qed.
Lemma frac_invalid_plus_1: (q: Qp), (¬ (1 + q)%Qp)%C.
Lemma frac_invalid_plus_1: (q: Qp), ¬ (1 + q)%Qp.
Proof.
intros q H.
by apply (Qp_ge_1 q).
......@@ -482,7 +482,6 @@ Section UpdateGhosts.
Local Set Default Proof Using "level1".
Implicit Types (π ρ : thread) (l : loc) (V : View) (h : History) (v: dec_agreeR InfoT).
Local Open Scope I.
Lemma Views_update_override π V (VIEW: Views) V'
: own VN ( VIEW {[π := Excl V]})
......@@ -528,7 +527,7 @@ Section UpdateGhosts.
Qed.
Lemma Infos_update_override l v v' (INFO: Infos)
: ( v')%C
: v'
own IN ( INFO {[l := (1%Qp, v)]})
(|==> own IN ( <[l := (1%Qp, v')]>INFO {[l := (1%Qp, v')]})).
Proof.
......@@ -543,7 +542,7 @@ Section UpdateGhosts.
Lemma Infos_alloc (INFO: Infos) l v
(New: INFO !! l = None)
: ( v)%C
: v
own IN ( INFO)
(|==> own IN ( (<[l := (1%Qp, v)]> INFO) {[l := (1%Qp, v)]})).
Proof.
......@@ -583,8 +582,6 @@ Section UpdateGhosts.
iIntros (?) "%". by iFrame "HInfo".
Qed.
Close Scope I.
Lemma IInv_update
ς INFO l zv zv'
(Inv: IInv ς INFO)
......
......@@ -36,8 +36,6 @@ Section proof.
Context `{fG : !foundationG Σ}.
Set Default Proof Using "Type*".
Local Open Scope I.
Lemma alloc (E : coPset) :
physN E
{{{{ True }}}}
......@@ -55,7 +53,7 @@ Section proof.
Lemma dealloc l :
{{{{ l ? }}}}
(Dealloc #l) @ physN
{{{{ RET (#()); True }}}}%C.
{{{{ RET (#()); True }}}}.
Proof.
intros. iViewUp. iIntros "#kI kS oL Post".
iDestruct "oL" as (h i) "(Alloc & oH & oI)".
......@@ -77,7 +75,7 @@ Section proof.
rewrite [in X in _ X]Eqmax.
have Lemaxn: (n max)%Z by omega.
move Eqz: {-}(0) => z.
rewrite [in X in WP (_ X,_) @ _ {{ _ }}]Eqz.
rewrite [in X in WP (_ X,_) @ _ {{ _ }}%I]Eqz.
have Eqzn : (z + n = max)%Z by omega.
have Le0z : 0 z by omega.
rewrite (_ : 0%nat = Z.to_nat z); last by rewrite -Eqz.
......
......@@ -57,12 +57,10 @@ Section proof.
Local Notation iProp := (iProp Σ).
Local Notation vPred := (@vPred Σ).
Open Scope vPred_scope.
Lemma message_passing_spec:
{{{{ PersistorCtx }}}}
(message_passing)
{{{{ (v: Z), RET #v; (v = 37) }}}}%C.
{{{{ (v: Z), RET #v; (v = 37) }}}}.
Proof.
intros. iViewUp; iIntros "#kI kS #kIp Post". rewrite /message_passing.
wp_bind Alloc.
......@@ -92,7 +90,7 @@ Section proof.
wp_bind (Fork _)%E.
iApply (wp_mask_mono (physN)); first done.
iCombine "Nax" "yPRT" as "SndT".
iApply (f_fork _ ((x 0) V_l [PP y in false @ () | mpInt x γ ] V_l)%I
iApply (f_fork _ ((x 0)%VP V_l [PP y in false @ () | mpInt x γ ] V_l)%I
with "[$kI $kS $SndT Post Tok]").
iSplitL "Post Tok".
- iNext. iViewUp. iIntros "kS".
......@@ -141,7 +139,7 @@ Section proof.
iDestruct (fupd_mask_mono _ with "XE") as ">XE"; first auto.
(* write release to final state *)
iApply (GPS_PP_Write (p:=()) (mpInt x γ) true (XE x γ) (λ _, True)
iApply (GPS_PP_Write (p:=()) (mpInt x γ) true (XE x γ) (λ _, True%VP)
with "[%] kI kS [yPRT' XE]"); [done|done|move=>[|]; done|done|..].
{ iSplitL ""; [|by iFrame "XE"].
iNext. iViewUp; iIntros "[oL _]". iModIntro.
......
......@@ -61,7 +61,7 @@ Section Fractional.
Lemma GPS_FPs_agree l s1 s2 q1 q2 (E : coPset) (HE: fracN .@ l E):
(vGPS_FP l s1 q1 vGPS_FP l s2 q2
={E}=> (s1 s2 s2 s1) vGPS_FP l s1 q1 vGPS_FP l s2 q2)%VP%C.
={E}=> (s1 s2 s2 s1) vGPS_FP l s1 q1 vGPS_FP l s2 q2)%VP.
Proof.
constructor => V.
iViewUp; iIntros "RP".
......@@ -93,7 +93,7 @@ Section Fractional.
(HEN : physN E):
{{{{ own_loc l F l s v F_past l s v }}}}
#l <~ #v @ E
{{{{ RET #() ; vGPS_FP l s 1%Qp }}}}%C.
{{{{ RET #() ; vGPS_FP l s 1%Qp }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (oL & F & Fp) Post".
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
......@@ -122,7 +122,7 @@ Section Fractional.
P vGPS_FP l s q }}}}
!ᵃᵗ #l @ E
{{{{ s' v, RET #v ;
(s s') vGPS_FP l s' q Q s' v }}}}%C.
(s s') vGPS_FP l s' q Q s' v }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & VSDup & oP & oR) Post".
iMod (fractor_open with "[$oR]")
......@@ -159,7 +159,7 @@ Section Fractional.
P vGPS_FP l s q β aSeen β }}}}
!ᵃᵗ #l @ E
{{{{ s' v, RET #v ;
(s s') vGPS_FP l s q β Q s' v }}}}%C.
(s s') vGPS_FP l s q β Q s' v }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & VSDup & oP & oR & Seen) Post".
iDestruct "oR" as (V0) "(abs & oR)".
......@@ -196,7 +196,7 @@ Section Fractional.
P vGPS_FP l s q }}}}
#l <~ᵃᵗ #v @ E
{{{{ RET #() ;
Q s' }}}}%C.
Q s' }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & oP & oW) Post".
iMod (fractor_open' with "[$oW]")
......@@ -241,7 +241,7 @@ Section Fractional.
P vGPS_FP l s q }}}}
(FAI C #l) @ E
{{{{ s'' (v: Z), RET #v ;
(s s'') vGPS_FP l s'' q Q s'' v }}}}%C.
(s s'') vGPS_FP l s'' q Q s'' v }}}}.
Proof.
iIntros (mod1C Φ). intros; iViewUp; iIntros "#kI kS (VS & oP & oW) Post".
iMod ((fractor_open) with "[$oW]")
......@@ -285,7 +285,7 @@ Section Fractional.
(CAS #l #v_o #v_n) @ E
{{{{ s'' (b: bool) v, RET #b ;
(s s'')
vGPS_FP l s'' q (if b then Q s'' else R s'' v) }}}}%C.
vGPS_FP l s'' q (if b then Q s'' else R s'' v) }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & VSF & VSDup & oP & oW) Post".
iMod ((fractor_open) with "[$oW]")
......
......@@ -95,7 +95,7 @@ Section Plain.
(HEN : physN E) (HNp : persistN E):
{{{{ PersistorCtx own_loc l F l s v F_past l s v }}}}
#l <~ #v @ E
{{{{ RET #() ; vGPS_PP l p s }}}}%C.
{{{{ RET #() ; vGPS_PP l p s }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (#kIp & oL & F & Fp) Post".
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
......@@ -127,7 +127,7 @@ Section Plain.
={E persist_locN .@ l}= F_past l s' v F_past l s' v )
P vGPS_PP l p s }}}}
!ᵃᵗ #l @ E
{{{{ s' v, RET #v ; (s s') vGPS_PP l p s' Q s' v }}}}%C.
{{{{ s' v, RET #v ; (s s') vGPS_PP l p s' Q s' v }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & VSDup & oP & oR) Post".
iMod (persistor_open with "[$oR]")
......@@ -164,7 +164,7 @@ Section Plain.
Q s' (F l s' v) F_past l s' v)
P vGPS_PP l p s }}}}
#l <~ᵃᵗ #v @ E
{{{{ RET #() ; vGPS_PP l p s' Q s' }}}}%C.
{{{{ RET #() ; vGPS_PP l p s' Q s' }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & oP & oW) Post".
iMod ((persistor_open') with "oW")
......@@ -213,7 +213,7 @@ Section Plain.
P vGPS_PP l p s }}}}
(CAS #l #v_o #v_n) @ E
{{{{ s'' (b: bool) v, RET #b ;
(s s'') vGPS_PP l p s'' (if b then Q s'' else R s'' v )}}}}%C.
(s s'') vGPS_PP l p s'' (if b then Q s'' else R s'' v )}}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & VSF & VSDup & oP & oW) Post".
iMod ((persistor_open) with "[$oW]")
......@@ -260,7 +260,7 @@ Section Plain.
P vGPS_PP l p s }}}}
(FAI C #l) @ E
{{{{ s'' (v: Z), RET #v ;
(s s'') vGPS_PP l p s'' Q s'' v }}}}%C.
(s s'') vGPS_PP l p s'' Q s'' v }}}}.
Proof.
iIntros (mod1C Φ). intros; iViewUp; iIntros "#kI kS (VS & oP & oW) Post".
iMod ((persistor_open) with "[$oW]")
......@@ -311,7 +311,7 @@ Section Plain_Default.
(HEN : physN E) (HNp : persistN E):
{{{{ PersistorCtx own_loc l F l s v F_past l s v }}}}
#l <~ #v @ E
{{{{ RET #() ; vGPS_PP (IP := IP) l () s }}}}%C.
{{{{ RET #() ; vGPS_PP (IP := IP) l () s }}}}.
Proof. by apply GPS_PP_Init. Qed.
End Plain_Default.
......
......@@ -100,7 +100,7 @@ Section Setup.
Definition sBE ζ := block_ends (rel_of (st_time l) (adj_opt)) ζ.
Definition sEx ζ (e_x: state_sort) : gset state_sort
:= {[ e <- ζ | st_view e_x !! l st_view e !! l]}%C.
:= {[ e <- ζ | st_view e_x !! l st_view e !! l]}.
Definition BE_Inv ζ e_x :=
([ set] b sEx (sBE ζ) e_x, F (st_prst b) (st_val b) (st_view b))%I.
......
......@@ -87,7 +87,7 @@ Section Gname_StrongSW.
( γ,
|={E persist_locN.@l}=> F γ l (s γ) v F_past γ l (s γ) v Q γ) }}}}
#l <~ #v @ E
{{{{ γ, RET #() ; Q γ vGPS_nFWP γ l (s γ) 1%Qp }}}}%C.
{{{{ γ, RET #() ; Q γ vGPS_nFWP γ l (s γ) 1%Qp }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (oL & F) Post".
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
......@@ -407,7 +407,7 @@ Section Gname_StrongSW.
P vGPS_nFRP γ l s q }}}}
!ᵃᵗ #l @ E
{{{{ s' v, RET #v ;
(s s') vGPS_nFRP γ l s' q Q s' v }}}}%C.
(s s') vGPS_nFRP γ l s' q Q s' v }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & VSDup & oP & oR) Post".
iMod (fractor_open with "[$oR]")
......@@ -440,7 +440,7 @@ Section Gname_StrongSW.
P aSeen β vGPS_nFRP γ l s1 q β PrtSeen γ s2 }}}}
!ᵃᵗ #l @ E
{{{{ s' v, RET #v ;
(s1 s' s2 s') vGPS_nFRP γ l s1 q β Q s' v }}}}%C.
(s1 s' s2 s') vGPS_nFRP γ l s1 q β Q s' v }}}}.
Proof.
intros. iViewUp. iIntros "#kI kS (VS & VSDup & oP & #aS & oR & oS2) Post".
......@@ -510,7 +510,7 @@ Section Gname_StrongSW.
P aSeen β vGPS_nFRP γ l s q β }}}}
!ᵃᵗ #l @ E
{{{{ s' v, RET #v ;
(s s') vGPS_nFRP γ l s q β Q s' v }}}}%C.
(s s') vGPS_nFRP γ l s q β Q s' v }}}}.
Proof.
intros. iViewUp. iIntros "#kI kS (VS & VSDup & oP & #aS & oR) Post".
......@@ -966,7 +966,7 @@ Section SingleWriter.
Proof. intros. unfold Frame. iIntros "[? _]". iExists _, _. by iFrame "∗". Qed.
Lemma GPS_SW_Readers_agree l s1 s2 (E : coPset) (HE: persist_locN .@ l E):
(vGPS_RSP l s1 vGPS_RSP l s2 ={E}=> (s1 s2 s2 s1))%VP%C.
(vGPS_RSP l s1 vGPS_RSP l s2 ={E}=> (s1 s2 s2 s1))%VP.
Proof.
constructor => V_l V' HV.
iIntros "#RP".
......@@ -993,7 +993,7 @@ Section SingleWriter.
Qed.
Lemma GPS_SW_Writer_max l s s' (E : coPset) (HE: persist_locN .@ l E):
(vGPS_RSP l s vGPS_WSP l s' ={E}=> vGPS_WSP l s' (s s'))%VP%C.
(vGPS_RSP l s vGPS_WSP l s' ={E}=> vGPS_WSP l s' (s s'))%VP.
Proof.
constructor => V_l V HV.
iIntros "oRW".
......@@ -1173,7 +1173,7 @@ Section SingleWriter.
Lemma GPS_FRPs_agree l s1 s2 q1 q2 (E : coPset) (HE: fracN .@ l E):
(vGPS_FRP l s1 q1 vGPS_FRP l s2 q2
={E}=> (s1 s2 s2 s1) vGPS_FRP l s1 q1 vGPS_FRP l s2 q2)%VP%C.
={E}=> (s1 s2 s2 s1) vGPS_FRP l s1 q1 vGPS_FRP l s2 q2)%VP.
Proof.
constructor => V.
iViewUp; iIntros "RP".
......@@ -1207,7 +1207,7 @@ Section SingleWriter.
(HEN : physN E):
{{{{ own_loc l F l s v F_past l s v }}}}
#l <~ #v @ E
{{{{ RET #() ; vGPS_FWP l s 1%Qp }}}}%C.
{{{{ RET #() ; vGPS_FWP l s 1%Qp }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (oL & F & Fp) Post".
iDestruct "oL" as (h i) "(Alloc & Hist & Info)".
......@@ -1239,7 +1239,7 @@ Section SingleWriter.
P vGPS_FRP l s q }}}}
!ᵃᵗ #l @ E
{{{{ s' v, RET #v ;
(s s') vGPS_FRP l s' q Q s' v }}}}%C.
(s s') vGPS_FRP l s' q Q s' v }}}}.
Proof.
intros; iViewUp; iIntros "#kI kS (VS & VSDup & oP & oR) Post".
iMod (fractor_open with "[$oR]")
......@@ -1296,7 +1296,7 @@ Section SingleWriter.
Lemma GPS_FWP_Writer_max l s s' q1 q2 (E : coPset) (HE: fracN .@ l E):
(vGPS_FRP l s q1 vGPS_FWP l s' q2 ={E}=>
vGPS_FRP l s q1 vGPS_FWP l s' q2 (s s'))%VP%C.
vGPS_FRP l s q1 vGPS_FWP l s' q2 (s s'))%VP.
Proof.
constructor => V_l V HV.
iIntros "oRW".
......
......@@ -247,7 +247,7 @@ Lemma difference_subseteq `{Collection A C} (X Y: C):
Proof. by move => ? /elem_of_difference [? _]. Qed.
Lemma difference_twice_union `{Collection A C} (X Y Z: C):
(X Y Z X (Y Z))%C.
X Y Z X (Y Z).
Proof. abstract set_solver. Qed.
Section Filter_Help.
......
......@@ -40,8 +40,8 @@ Context `{!foundationG Σ, !rslG Σ}.
Local Notation iProp := (iProp Σ).
Implicit Types (Ψ: gname Z View iProp) (φ: Z View iProp).
Section defs.
Local Open Scope I.
Definition conv φ φ' : iProp := v V, φ v V φ' v V.
Definition slicesA Γ φ Ψ := vbox Γ φ Ψ.
Definition slicesC Γ Ψ := vslices Γ Ψ i v V, i Γ⌝ (Ψ i v V True).
......@@ -95,6 +95,7 @@ Definition InitRaw V jγ : iProp
:= s (j γ: gname), jγ = encode (j,γ)
sts_own γ s
isInit s init_local (rhist s) V.
End defs.
Instance RelRaw_persistent V (φ: Z vPred) φR jγ
: Persistent (RelRaw V φ φR jγ) := _.
......@@ -106,7 +107,7 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
(* Helpers *)
Lemma big_sepS_gblock_ends_ins_update
l (h: History) p0 (Ψ: Val * View iProp)
(Disj: (h ## {[p0]})%C)
(Disj: h ## {[p0]})
(GB: gblock_ends_ins l h p0 (gblock_ends l h) (gblock_ends l ({[p0]} h)))
: Ψ p0 ([ set] p gblock_ends l h, Ψ p)
([ set] p gblock_ends l ({[p0]} h), Ψ p).
......@@ -162,7 +163,7 @@ Lemma RelRaw_write l (φ φd φR: Z → vPred) v V n E π:
(#l <~ᵃᵗ #v, V)%E @ E
{{{ V', RET (#(), V') ;
V V'⌝ Seen π V'
RSLInv φR φd l n RelRaw V' φ φR n InitRaw V' n}}}%C.
RSLInv φR φd l n RelRaw V' φ φR n InitRaw V' n}}}.
Proof.
iIntros (??) "(#kI & Seen & Itpr &ItprD & oI & Rel) Post".
iDestruct "Rel" as (s j γ) "(% & Own & % & #Conv & #Stored)".
......@@ -226,7 +227,7 @@ Proof.
as (i') "(Hi' & #slice' & #slices')"; [exact INi|].
iExists i'. iDestruct "Hi'" as %NIn'. iFrame (NIn') "slice'".
iModIntro. iSplitR "Hφ conv".
+ iExists (<[i':=<[v:=λ _, True]> Ψi]> Ψ). iFrame "slices'".
+ iExists (<[i':=<[v:=λ _, True%I]> Ψi]> Ψ). iFrame "slices'".
iNext. rewrite (big_sepS_delete _ _ _ IN).
iSplitL "res1".
* rewrite (big_sepS_fn_insert (λ _ (f: Z View iProp), f v V));
......@@ -253,7 +254,7 @@ Proof.
as (i') "(Hi' & #slice' & #slices')"; [exact INi|..].
+ unfold vbox. iFrame "slices". iNext. iNext.
iIntros "!#" (v2 V2) "_".
iApply (big_sepS_impl (λ _, True) _ Γ with "[]"). iSplit.
iApply (big_sepS_impl (λ _, True%I) _ Γ with "[]"). iSplit.
* iIntros "!#" (i0) "IN _". by iApply ("EqT" $! i0 v2 V2 with "IN").
* by rewrite big_sepS_forall.
+ iExists i'. iDestruct "Hi'" as %NIn'. iFrame (NIn') "slice'".
......@@ -281,7 +282,7 @@ Lemma AcqRaw_read l (φ φd φR: Z → vPred) V n E π:
V V'⌝ Seen π V'
RSLInv φR φd l n
AcqRaw V' (<[v:=True%VP]>φ) n InitRaw V' n
φ v V' φd v V'}}}%C.
φ v V' φd v V'}}}.
Proof.
iIntros (? Φ) "(#kI & kS & Dup & oI & AR & IR) Post".
iDestruct "AR" as (s1 j γ i Ψi) "(% & Own1 & Hs1 & Alloc & #Conv & #SΨi)".
......@@ -353,10 +354,10 @@ Lemma rsl_slicesC_insert Γ (q: bool) :
i, i Γ⌝ vslice i (λ _ _, True) ?q Ψ, slicesC ({[i]} Γ) Ψ.
Proof.
iDestruct 1 as (Ψ) "(slices & #True)".
iMod (vslices_insert2 _ Γ _ (λ _ _, True) q with "slices")
iMod (vslices_insert2 _ Γ _ (λ _ _, True%I) q with "slices")
as (i) "(% & slice & slices)"; [done|].
iExists i. iIntros "!> {$%}".
iFrame "slice". iExists (<[i:= (λ _ _, True)]> Ψ). iFrame "slices".
iFrame "slice". iExists (<[i:= (λ _ _, True%I)]> Ψ). iFrame "slices".
do 2 iNext. iIntros "!#" (??).
iDestruct 1 as %[->%elem_of_singleton_1|?]%elem_of_union.
- by rewrite fn_lookup_insert.
......@@ -443,7 +444,7 @@ Proof.
iDestruct (vslices_agree with "slice2 slices") as "#Eq2"; [done|].
iDestruct (vslices_mono _ (Γ {[i1; i2]}) with "slices") as "slices";
[exact LE|].
iMod (vslices_insert2 _ Γ _ (λ v V, Ψi1 v V Ψi2 v V) q LE with "slices")
iMod (vslices_insert2 _ Γ _ (λ v V, Ψi1 v V Ψi2 v V)%I q LE with "slices")
as (i) "(#Hi & slice & slices)".
iModIntro. iExists (i). iFrame "Hi slice".
iExists _. iFrame "slices".
......@@ -472,7 +473,7 @@ Proof.
destruct s as [[] Γ h]; iFrame "Hist"; simpl in *;
iDestruct "Inv" as "[$ Inv]".
- iDestruct "Inv" as (Ψ) "slices".
iMod (vslice_merge _ _ _ _ (λ v V, Ψi1 v V Ψi2 v V) _ _ _ q
iMod (vslice_merge _ _ _ _ (λ v V, Ψi1 v V Ψi2 v V)%I _ _ _ q
with "slice1 slice2 [] slices") as (i) "(#Hi & slice & slices)";
[done|done|done|..].
{ do 2 iNext. iIntros "!#" (??) "[$$]". }
......@@ -480,7 +481,7 @@ Proof.
- iDestruct "Inv" as "[$ Inv]". iDestruct "Inv" as (Ψ) "[slices res]".
iDestruct (vbox_agree with "slice1 slices") as "#Eq1"; [done|].
iDestruct (vbox_agree with "slice2 slices") as "#Eq2"; [done|].
iMod (vslice_merge _ _ _ _ (λ v V, Ψi1 v V Ψi2 v V) _ _ _ q
iMod (vslice_merge _ _ _ _ (λ v V, Ψi1 v V Ψi2 v V)%I _ _ _ q
with "slice1 slice2 [] slices") as (i) "(#Hi & slice & slices)";
[done|done|done|..].
{ do 2 iNext. iIntros "!#" (??) "[$$]". }
......@@ -672,7 +673,7 @@ Proof.
assert (sts.closed (sts.up s'' {[Change i2]}) {[Change i2]}).
{ apply sts.closed_up, state_rset_split_token_disj_2. }
iAssert (|==> sts_own γ s'' {[Change i1]} sts_own γ s'' {[Change i2]})
iAssert (|==> sts_own γ s'' {[Change i1]} sts_own γ s'' {[Change i2]})%I
with "[Own]" as ">(O1 & O2)".
{ rewrite -sts_ownS_op; [..|auto|auto].
- iApply (sts_own_weaken with "Own"); [auto| |by apply sts.closed_op].
......@@ -726,7 +727,7 @@ Lemma AcqRaw_alloc (φ φd: Z → vPred) E π V:
(Alloc, V) @ E
{{{ (l: loc) V' n X, RET (#l, V');
V V'⌝ Seen π V' Info l 1 X
RSLInv φ φd l n RelRaw V' φ φ n AcqRaw V' φ n }}}%C.
RSLInv φ φd l n RelRaw V' φ φ n AcqRaw V' φ n }}}.
Proof.
iIntros (? Φ) "(kI & kS) Post".
iApply (wp_mask_mono (physN)); first auto. iApply wp_fupd.
......@@ -747,7 +748,7 @@ Proof.
set s: state := (mkRST rcUn h).
iAssert (rsl_inv l φ φd s) with "[Hist SΨi]" as "Inv".
{ iFrame "Hist UNI". iExists (λ _ _ _,True). iSplit.
{ iFrame "Hist UNI". iExists (λ _ _ _,True%I). iSplit.
- by rewrite /vslices big_sepS_empty.
- iNext. by iIntros "!#" (????). }
......@@ -769,7 +770,7 @@ Lemma RMWAcqRaw_alloc (φ φd: Z → vPred) E π V:
(Alloc, V) @ E
{{{ (l: loc) V' n X, RET (#l, V');
V V'⌝ Seen π V' Info l 1 X
RSLInv φ φd l n RelRaw V' φ φ n RMWAcqRaw V' n }}}%C.
RSLInv φ φd l n RelRaw V' φ φ n RMWAcqRaw V' n }}}.
Proof.
iIntros (? Φ) "(kI & kS) Post".
iApply (wp_mask_mono (physN)); [done|]. iApply wp_fupd.
......@@ -830,7 +831,7 @@ Proof.
iApply (big_sepS_mono _ _ ({[VInj v, V]} : History) with "[Hφ]");
[by apply subseteq_gset_filter|reflexivity
|by rewrite big_sepS_singleton].
- iExists (λ _ _ _,True). iSplit; [by rewrite /vslices big_sepS_empty|].
- iExists (λ _ _ _,True%I). iSplit; [by rewrite /vslices big_sepS_empty|].
iNext. by iIntros "!#" (???) "_". }
iMod (own_alloc (sts_auth s )) as (γ) "Own".
......@@ -858,7 +859,7 @@ Lemma AcqRaw_init l v h (φ φd: Z → vPred) E π V:
(#l <~ #v, V) @ E
{{{ V' n, RET (#(), V');
V V'⌝ Seen π V' RSLInv φ φd l n
RelRaw V' φ φ n AcqRaw V' φ n InitRaw V' n }}}%C.
RelRaw V' φ φ n AcqRaw V' φ n InitRaw V' n }}}.
Proof.
iIntros (? Φ) "(#kI & kS & Hist & #Alloc & Hφ & Hφd) Post".
iApply wp_fupd. iApply (wp_mask_mono (physN)); first done.
......@@ -880,7 +881,7 @@ Lemma RMWAcqRaw_init l v h (φ φd: Z → vPred) E π V:
(#l <~ #v, V) @ E
{{{ V' n, RET (#(), V');
V V'⌝ Seen π V' RSLInv φ φd l n
RelRaw V' φ φ n RMWAcqRaw V' n InitRaw V' n }}}%C.
RelRaw V' φ φ n RMWAcqRaw V' n InitRaw V' n }}}.
Proof.
iIntros (? Φ) "(#kI & kS & Hist & #Alloc & Hφ & Hφd) Post".
iApply wp_fupd. iApply (wp_mask_mono (physN)); first done.
......@@ -971,7 +972,7 @@ Proof.
(* get full interpretation *)
rewrite /res (big_sepS_delete _ _ _ Hp').
iDestruct "res" as "(Hφ & res)".
iAssert ( (φ v_r) V') with "[Hφ]" as "Hφ".
iAssert ( (φ v_r) V')%I with "[Hφ]" as "Hφ".
{ iNext. by iApply (vPred_mono V1). }
iMod ("CSucc" $! V' with "[] [$P $Hφ $Hφd]") as "(Hφ & Hφd & R)"; [auto|].
......
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