Commit 9b52923f authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Squashed commit of the following:

commit 32f5885b5083c6052251a266b0ec4b6f0cd01bcc
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Jun 11 11:54:32 2019 +0200

    Full bump

commit 3fdf913129ee6c1081e947de48e71ca6411f33da
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Tue Jun 11 11:31:22 2019 +0200

    More cleanup.

commit 46be8c0184d5a9e7de42022e389e23df99f73f6d
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Mon Jun 10 22:50:02 2019 +0200

    Some cleanup.

commit 2dc17e2cafc0b33e5ef0d2a6f6862b0938f68b18
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Mon Jun 10 16:33:46 2019 +0200

    WIP

commit 9427aa2ddd4fecb49b8e1c02eccc954fdb8af554
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Mon Jun 10 15:02:21 2019 +0200

    iRewrite Bug inspection

commit 40393f8800ab1a587f49f9ad479f5dc94b2bf2bc
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Mon Jun 10 14:56:08 2019 +0200

    Bumped Iris

commit 660218ca36e148b7270fd0044a2401fa553373d1
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Mon Jun 3 11:31:11 2019 +0200

    Add type.

commit 54214779390c19b1f9c8b293ac26f36efda95f4d
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Fri May 31 16:24:05 2019 +0200

    Coinductive version of stype.

commit b0fe9afb
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Fri May 31 13:19:13 2019 +0200

    Bump Iris.
parent c8a2d68b
......@@ -12,7 +12,7 @@ Definition auth_exclΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
#[GFunctor (authRF (optionURF (exclRF F)))].
Instance subG_auth_exclG (F : cFunctor) `{!cFunctorContractive F} {Σ} :
subG (auth_exclΣ F) Σ auth_exclG (F (iPreProp Σ)) Σ.
subG (auth_exclΣ F) Σ auth_exclG (F (iPreProp Σ) _) Σ.
Proof. solve_inG. Qed.
Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
......@@ -38,11 +38,11 @@ Section auth_excl.
( to_auth_excl x to_auth_excl y) - (x y : iProp Σ).
Proof.
iIntros "Hvalid".
iDestruct (auth_validI with "Hvalid") as "[Hy Hvalid]"; simpl.
iDestruct "Hy" as ([z|]) "Hy"; last first.
- by rewrite left_id right_id_L bi.option_equivI /= excl_equivI.
iDestruct (auth_both_validI with "Hvalid") as "[_ [Hle Hvalid]]"; simpl.
iDestruct "Hle" as ([z|]) "Hy"; last first.
- by rewrite bi.option_equivI /= excl_equivI.
- iRewrite "Hy" in "Hvalid".
by rewrite left_id uPred.option_validI /= excl_validI /=.
by rewrite uPred.option_validI /= excl_validI /=.
Qed.
Lemma excl_eq γ x y :
......@@ -64,4 +64,4 @@ Section auth_excl.
eapply exclusive_local_update. done. }
by rewrite own_op.
Qed.
End auth_excl.
\ No newline at end of file
End auth_excl.
......@@ -22,20 +22,22 @@ Section DualBranch.
intros Ha Hst1 Hst2.
destruct a1.
- simpl.
simpl in Ha. rewrite Ha.
simpl in Ha. rewrite -Ha.
rewrite -(stype_force_eq (dual_stype _)).
constructor.
f_equiv.
f_equiv.
destruct (decode a).
by destruct b. done.
by destruct b. apply is_dual_end.
- simpl.
simpl in Ha. rewrite Ha.
simpl in Ha. rewrite -Ha.
rewrite -(stype_force_eq (dual_stype _)).
constructor.
f_equiv.
f_equiv.
destruct (decode a).
by destruct b.
done.
by destruct b.
apply is_dual_end.
Qed.
End DualBranch.
Global Typeclasses Opaque TSB.
......
......@@ -121,10 +121,10 @@ Section channel.
wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl [])))
as (lsγ) "[Hls Hls']"; first done.
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl [])))
as (rsγ) "[Hrs Hrs']"; first done.
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (lsγ) "[Hls Hls']".
{ by apply auth_both_valid. }
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
{ by apply auth_both_valid. }
iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
{ rewrite /is_list_ref; eauto. }
iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
......
......@@ -20,28 +20,77 @@ Definition logrelΣ A :=
Instance subG_chanΣ {A Σ} : subG (logrelΣ A) Σ logrelG A Σ.
Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
Section stype_interp.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Fixpoint st_eval `{!logrelG val Σ} (vs : list val) (st1 st2 : stype val (iProp Σ)) : iProp Σ :=
match vs with
| [] => st1 dual_stype st2
| v::vs => match st2 with
| TSR Receive P st2 => P v st_eval vs st1 (st2 v)
| _ => False
end
end%I.
Arguments st_eval : simpl nomatch.
Record st_name := SessionType_name {
st_c_name : chan_name;
st_l_name : gname;
st_r_name : gname
}.
Record st_name := STName {
st_c_name : chan_name;
st_l_name : gname;
st_r_name : gname
}.
Definition to_stype_auth_excl `{!logrelG val Σ} (st : stype val (iProp Σ)) :=
to_auth_excl (Next (stype_map iProp_unfold st)).
Definition st_own `{!logrelG val Σ} (γ : st_name) (s : side)
(st : stype val (iProp Σ)) : iProp Σ :=
own (side_elim s st_l_name st_r_name γ) ( to_stype_auth_excl st)%I.
Definition to_stype_auth_excl (st : stype val (iProp Σ)) :=
to_auth_excl (Next (stype_map iProp_unfold st)).
Definition st_ctx `{!logrelG val Σ} (γ : st_name) (s : side)
(st : stype val (iProp Σ)) : iProp Σ :=
own (side_elim s st_l_name st_r_name γ) ( to_stype_auth_excl st)%I.
Definition st_own (γ : st_name) (s : side)
(st : stype val (iProp Σ)) : iProp Σ :=
own (side_elim s st_l_name st_r_name γ)
( to_stype_auth_excl st)%I.
Definition inv_st `{!logrelG val Σ} (γ : st_name) (c : val) : iProp Σ :=
( l r stl str,
chan_own (st_c_name γ) Left l
chan_own (st_c_name γ) Right r
st_ctx γ Left stl
st_ctx γ Right str
((r = [] st_eval l stl str)
(l = [] st_eval r str stl)))%I.
Definition st_ctx (γ : st_name) (s : side)
(st : stype val (iProp Σ)) : iProp Σ :=
own (side_elim s st_l_name st_r_name γ)
( to_stype_auth_excl st)%I.
Definition interp_st `{!logrelG val Σ, !heapG Σ} (N : namespace) (γ : st_name)
(c : val) (s : side) (st : stype val (iProp Σ)) : iProp Σ :=
(st_own γ s st is_chan N (st_c_name γ) c inv N (inv_st γ c))%I.
Instance: Params (@interp_st) 7.
Notation "⟦ c @ s : st ⟧{ N , γ }" := (interp_st N γ c s st)
(at level 10, s at next level, st at next level, γ at next level,
format "⟦ c @ s : st ⟧{ N , γ }").
Section stype.
Context `{!logrelG val Σ, !heapG Σ} (N : namespace).
Global Instance st_eval_ne : NonExpansive2 (st_eval vs).
Proof.
induction vs as [|v vs IH];
destruct 2 as [n|[] P1 P2 st1 st2|n [] P1 P2 st1 st2]=> //=.
- by repeat f_equiv.
- f_equiv. done. f_equiv. by constructor.
- f_equiv. done. f_equiv. by constructor.
- f_equiv. done. f_equiv. by constructor.
- f_equiv. done. f_equiv. by constructor.
- f_equiv. done. by f_contractive.
- f_equiv. done. f_contractive. apply IH. by apply dist_S. done.
Qed.
Global Instance st_eval_proper vs : Proper (() ==> () ==> ()) (st_eval vs).
Proof. apply (ne_proper_2 _). Qed.
Global Instance to_stype_auth_excl_ne : NonExpansive to_stype_auth_excl.
Proof. solve_proper. Qed.
Global Instance st_own_ne γ s : NonExpansive (st_own γ s).
Proof. solve_proper. Qed.
Global Instance interp_st_ne γ c s : NonExpansive (interp_st N γ c s).
Proof. solve_proper. Qed.
Global Instance interp_st_proper γ c s : Proper (() ==> ()) (interp_st N γ c s).
Proof. apply (ne_proper _). Qed.
Lemma st_excl_eq γ s st st' :
st_ctx γ s st - st_own γ s st' - (st st').
......@@ -58,8 +107,7 @@ Section stype_interp.
Qed.
Lemma st_excl_update γ s st st' st'' :
st_ctx γ s st - st_own γ s st' ==
st_ctx γ s st'' st_own γ s st''.
st_ctx γ s st - st_own γ s st' == st_ctx γ s st'' st_own γ s st''.
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_update_2 with "Hauth Hfrag") as "H".
......@@ -67,130 +115,43 @@ Section stype_interp.
(to_stype_auth_excl st'')).
eapply option_local_update.
eapply exclusive_local_update. done. }
rewrite own_op.
done.
Qed.
Fixpoint st_eval (vs : list val) (st1 st2 : stype val (iProp Σ)) : iProp Σ :=
match vs with
| [] => st1 dual_stype st2
| v::vs => match st2 with
| TSR Receive P st2 => P v st_eval vs st1 (st2 v)
| _ => False
end
end%I.
Global Arguments st_eval : simpl nomatch.
Lemma st_later_eq a P2 (st : stype val (iProp Σ)) st2 :
( (st TSR a P2 st2) -
( P1 st1, st TSR a P1 st1
(( v, P1 v P2 v))
(( v, st1 v st2 v))) : iProp Σ).
Proof.
destruct st.
- iIntros "Heq".
iDestruct (stype_equivI with "Heq") as ">Heq".
done.
- iIntros "Heq".
iDestruct (stype_equivI with "Heq") as "Heq".
iDestruct ("Heq") as "[>Haeq [HPeq Hsteq]]".
iDestruct "Haeq" as %Haeq.
subst.
iExists P, st.
iSplit=> //.
by iSplitL "HPeq".
by rewrite own_op.
Qed.
Global Instance st_eval_ne : NonExpansive2 (st_eval vs).
Proof.
intros vs n. induction vs as [|v vs IH]; [solve_proper|].
destruct 2 as [|[] ????? Hst]=> //=. f_equiv. solve_proper.
by apply IH, Hst.
Qed.
Lemma st_eval_send (P : val -> iProp Σ) st l str v :
P v - st_eval l (TSR Send P st) str - st_eval (l ++ [v]) (st v) str.
Lemma st_eval_send (P : val iProp Σ) st vs v str :
P v - st_eval vs (<!> @ P, st) str - st_eval (vs ++ [v]) (st v) str.
Proof.
iIntros "HP".
iRevert (str).
iInduction l as [|l] "IH"; iIntros (str) "Heval".
- simpl.
iDestruct (dual_stype_flip with "Heval") as "Heval".
iRewrite -"Heval". simpl.
iInduction vs as [|v' vs] "IH"; iIntros (str) "Heval".
- iDestruct (dual_stype_flip with "Heval") as "Heval".
iRewrite -"Heval"; simpl.
rewrite dual_stype_involutive.
by iFrame.
- simpl.
destruct str; auto.
destruct a; auto.
iDestruct "Heval" as "[HP0 Heval]".
iFrame.
- destruct str as [|[] P' str]=> //=.
iDestruct "Heval" as "[$ Heval]".
by iApply ("IH" with "HP").
Qed.
Lemma st_eval_recv (P : val iProp Σ) st1 l st2 v :
st_eval (v :: l) st1 (TSR Receive P st2) - st_eval l st1 (st2 v) P v.
st_eval (v :: l) st1 (<?> @ P, st2) - st_eval l st1 (st2 v) P v.
Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed.
Definition inv_st (γ : st_name) (c : val) : iProp Σ :=
( l r stl str,
chan_own (st_c_name γ) Left l
chan_own (st_c_name γ) Right r
st_ctx γ Left stl
st_ctx γ Right str
((r = [] st_eval l stl str)
(l = [] st_eval r str stl)))%I.
Definition is_st (γ : st_name) (st : stype val (iProp Σ))
(c : val) : iProp Σ :=
(is_chan N (st_c_name γ) c inv N (inv_st γ c))%I.
Definition interp_st (γ : st_name) (st : stype val (iProp Σ))
(c : val) (s : side) : iProp Σ :=
(st_own γ s st is_st γ st c)%I.
Global Instance interp_st_proper γ :
Proper (() ==> (=) ==> (=) ==> ()) (interp_st γ).
Proof.
intros st1 st2 Heq v1 v2 <- s1 s2 <-.
iSplit;
iIntros "[Hown Hctx]";
iFrame;
unfold st_own;
iApply (own_mono with "Hown");
apply (auth_frag_mono);
apply Some_included;
left;
f_equiv;
f_equiv;
apply stype_map_equiv=> //.
Qed.
End stype_interp.
Notation "⟦ c @ s : st ⟧{ N , γ }" := (interp_st N γ st c s)
(at level 10, s at next level, st at next level, γ at next level,
format "⟦ c @ s : st ⟧{ N , γ }").
Section stype_specs.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Lemma new_chan_vs st E c cγ :
is_chan N cγ c
chan_own cγ Left []
chan_own cγ Right []
={E}=
lγ rγ,
let γ := SessionType_name cγ lγ rγ in
c @ Left : st {N,γ} c @ Right : dual_stype st {N,γ}.
chan_own cγ Right [] ={E}= lγ rγ,
let γ := STName cγ lγ rγ in
c @ Left : st {N,γ} c @ Right : dual_stype st {N,γ}.
Proof.
iIntros "[#Hcctx [Hcol Hcor]]".
iMod (own_alloc ( (to_stype_auth_excl st)
(to_stype_auth_excl st)))
as (lγ) "[Hlsta Hlstf]"; first done.
(to_stype_auth_excl st))) as (lγ) "[Hlsta Hlstf]".
{ by apply auth_both_valid_2. }
iMod (own_alloc ( (to_stype_auth_excl (dual_stype st))
(to_stype_auth_excl (dual_stype st))))
as (rγ) "[Hrsta Hrstf]"; first done.
pose (SessionType_name cγ lγ rγ) as stγ.
(to_stype_auth_excl (dual_stype st)))) as (rγ) "[Hrsta Hrstf]".
{ by apply auth_both_valid_2. }
pose (STName cγ lγ rγ) as stγ.
iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
{ iNext. rewrite /inv_st. eauto 10 with iFrame. }
iModIntro.
......@@ -202,8 +163,7 @@ Section stype_specs.
IsDualStype st1 st2
{{{ True }}}
new_chan #()
{{{ c γ, RET c; c @ Left : st1 {N,γ}
c @ Right : st2 {N,γ} }}}.
{{{ c γ, RET c; c @ Left : st1 {N,γ} c @ Right : st2 {N,γ} }}}.
Proof.
rewrite /IsDualStype.
iIntros (Hst Φ _) "HΦ".
......@@ -221,49 +181,41 @@ Section stype_specs.
Lemma send_vs c γ s (P : val iProp Σ) st E :
N E
c @ s : TSR Send P st {N,γ} ={E,E∖↑N}=
vs, chan_own (st_c_name γ) s vs
( v, P v -
chan_own (st_c_name γ) s (vs ++ [v])
={E N,E}= c @ s : st v {N,γ}).
c @ s : TSR Send P st {N,γ} ={E,E∖↑N}= vs,
chan_own (st_c_name γ) s vs
v, P v -
chan_own (st_c_name γ) s (vs ++ [v]) ={E∖↑N,E}=
c @ s : st v {N,γ}.
Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
iMod (inv_open with "Hinv") as "Hinv'"=> //.
iDestruct "Hinv'" as "[Hinv' Hinvstep]".
iDestruct "Hinv'" as
(l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')".
iInv N as (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
iModIntro.
destruct s.
- iExists _.
iIntros "{$Hclf} !>" (v) "HP Hclf".
iRename "Hstf" into "Hstlf".
iDestruct (st_excl_eq with "Hstla Hstlf") as "#Heq".
iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf")
as "[Hstla Hstlf]".
iMod ("Hinvstep" with "[-Hstlf]") as "_".
{
iNext.
iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
iMod ("Hclose" with "[-Hstlf]") as "_".
{ iNext.
iExists _,_,_,_. iFrame.
iLeft.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iSplit=> //.
iApply (st_eval_send with "HP").
by iRewrite -"Heq".
- iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //.
iSplit; first done. simpl.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
}
iModIntro. iFrame. rewrite /is_st. auto.
by iRewrite "Heq" in "Heval".
- iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //=.
iSplit; first done.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive. }
iModIntro. iFrame. auto.
- iExists _.
iIntros "{$Hcrf} !>" (v) "HP Hcrf".
iRename "Hstf" into "Hstrf".
iDestruct (st_excl_eq with "Hstra Hstrf") as "#Heq".
iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf")
as "[Hstra Hstrf]".
iMod ("Hinvstep" with "[-Hstrf]") as "_".
{
iNext.
iExists _,_,_,_. iFrame.
iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
iMod ("Hclose" with "[-Hstrf]") as "_".
{ iNext.
iExists _, _, _, _. iFrame.
iRight.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
......@@ -271,9 +223,8 @@ Section stype_specs.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
- iSplit=> //.
iApply (st_eval_send with "HP").
by iRewrite -"Heq".
}
iModIntro. iFrame. rewrite /is_st. auto.
by iRewrite "Heq" in "Heval". }
iModIntro. iFrame. auto.
Qed.
Lemma send_st_spec st γ c s (P : val iProp Σ) v :
......@@ -292,75 +243,60 @@ Section stype_specs.
Lemma try_recv_vs c γ s (P : val iProp Σ) st E :
N E
c @ s : TSR Receive P st {N,γ}
={E,E∖↑N}=
vs, chan_own (st_c_name γ) (dual_side s) vs
( ((vs = [] - chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=
c @ s : TSR Receive P st {N,γ} ={E,E∖↑N}= vs,
chan_own (st_c_name γ) (dual_side s) vs
((vs = [] -
chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=
c @ s : TSR Receive P st {N,γ})
( v vs', vs = v :: vs' -
chan_own (st_c_name γ) (dual_side s) vs' - |={E∖↑N,E}=>
c @ s : (st v) {N,γ} P v))).
( v vs',
vs = v :: vs' -
chan_own (st_c_name γ) (dual_side s) vs' ={E∖↑N,E}=
c @ s : (st v) {N,γ} P v)).
Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
iMod (inv_open with "Hinv") as "Hinv'"=> //.
iDestruct "Hinv'" as "[Hinv' Hinvstep]".
iDestruct "Hinv'" as
(l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')".
iInv N as (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
iExists (side_elim s r l). iModIntro.
destruct s.
- simpl. iIntros "{$Hcrf} !>".
destruct s; simpl.
- iIntros "{$Hcrf} !>".
iRename "Hstf" into "Hstlf".
iDestruct (st_excl_eq with "Hstla Hstlf") as "#Heq".
iSplit=> //.
+ iIntros "Hvs Hown".
iMod ("Hinvstep" with "[-Hstlf]") as "_".
{ iNext. iExists l,r,_,_. iFrame. }
iSplit.
+ iIntros (->) "Hown".
iMod ("Hclose" with "[-Hstlf]") as "_".
{ iNext. iExists l, [], _, _. iFrame. }
iModIntro. iFrame "Hcctx ∗ Hinv".
+ iIntros (v vs Hvs) "Hown".
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; first inversion Hvs.
iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf")
as "[Hstla Hstlf]".
subst.
iDestruct (st_later_eq with "Heq") as ">Hleq".
iDestruct "Hleq" as (P1 st1) "[Hsteq [HPeq Hsteq']]".
iSpecialize ("HPeq" $!v).
iSpecialize ("Hsteq'" $!v).
+ iIntros (v vs ->) "Hown".
iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
iDestruct (stype_later_equiv with "Heq") as ">Hleq".
iDestruct "Hleq" as (P1 st1) "(Hsteq & HPeq & Hsteq')".
iRewrite "Hsteq" in "Heval".
subst.
iDestruct (st_eval_recv with "Heval") as "[Heval HP]".
iMod ("Hinvstep" with "[-Hstlf HP]") as "H".
{ iExists _,_,_,_. iFrame. iRight=> //.
iNext. iSplit=> //. by iRewrite -"Hsteq'". }
iModIntro.
iSplitR "HP".
* iFrame "Hstlf Hcctx Hinv".
* iNext. by iRewrite -"HPeq".
- simpl. iIntros "{$Hclf} !>".
iMod ("Hclose" with "[-Hstlf HP]") as "H".
{ iExists _, _,_ ,_. iFrame. iRight.
iNext. iSplit=> //. iNext. by iRewrite -("Hsteq'" $! v). }
iModIntro. iFrame "Hstlf Hcctx Hinv".
iNext. by iRewrite -("HPeq" $! v).
- iIntros "{$Hclf} !>".
iRename "Hstf" into "Hstrf".
iDestruct (st_excl_eq with "Hstra Hstrf") as "#Heq".
iSplit=> //.
+ iIntros "Hvs Hown".
iMod ("Hinvstep" with "[-Hstrf]") as "_".
{ iNext. iExists l,r,_,_. iFrame. }
+ iIntros (->) "Hown".
iMod ("Hclose" with "[-Hstrf]") as "_".
{ iNext. iExists [], r, _, _. iFrame. }
iModIntro. iFrame "Hcctx ∗ Hinv".
+ iIntros (v vs' Hvs) "Hown".
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last inversion Hvs.
iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf")
as "[Hstra Hstrf]".
subst.
iDestruct (st_later_eq with "Heq") as ">Hleq".
iDestruct "Hleq" as (P1 st1) "[Hsteq [HPeq Hsteq']]".
iSpecialize ("HPeq" $!v).
iSpecialize ("Hsteq'" $!v).
+ iIntros (v vs' ->) "Hown".
iDestruct "Hinv'" as "[[>-> Heval]|[>% Heval]]"; last done.
iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
iDestruct (stype_later_equiv with "Heq") as ">Hleq".
iDestruct "Hleq" as (P1 st1) "(Hsteq & HPeq & Hsteq')".
iRewrite "Hsteq" in "Heval".
iDestruct (st_eval_recv with "Heval") as "[Heval HP]".
iMod ("Hinvstep" with "[-Hstrf HP]") as "_".
{ iExists _,_,_,_. iFrame. iLeft=> //.
iNext. iSplit=> //. by iRewrite -"Hsteq'". }
iModIntro.
iSplitR "HP".
* iFrame "Hstrf Hcctx Hinv".
* iNext. by iRewrite -"HPeq".
iMod ("Hclose" with "[-Hstrf HP]") as "_".
{ iExists _, _, _, _. iFrame. iLeft.
iNext. iSplit=> //. iNext. by iRewrite -("Hsteq'" $! v). }