Commit 4aa2399d authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Finalised send proof

parent ae9857fc
......@@ -198,7 +198,8 @@ Section logrel.
iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf")
as "[Hstla Hstlf]".
iMod ("Hinvstep" with "[-Hstlf]") as "_".
{ iNext.
{
iNext.
iExists _,_,_,_. iFrame.
iLeft.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
......@@ -207,10 +208,30 @@ Section logrel.
by iRewrite -"Heq".
- iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //.
iSplit; first done. simpl.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive. }
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
}
iModIntro. iFrame. rewrite /is_st. auto.
-
Admitted.
- 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.
iRight.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
iSplit; first done. simpl.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
- iSplit=> //.
iApply (st_eval_send with "HP").
by iRewrite -"Heq".
}
iModIntro. iFrame. rewrite /is_st. auto.
Qed.
Lemma send_st_spec st γ c s (P : val iProp Σ) v :
{{{ P v c @ s : TSR Send P st {γ} }}}
......
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