Commit cce7faa3 authored by Robbert Krebbers's avatar Robbert Krebbers

Misc clean up.

- Put code and proofs of examples in a single file.
- Rename encode/decode to avoid conflicts with encode/decode (of the countable class) in stdpp.
- Remove useless imports.
parent 134c766d
-Q theories osiris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/base_logic/auth_excl.v
theories/utils/auth_excl.v
theories/proto/encodable.v
theories/proto/list.v
theories/proto/channel.v
......@@ -10,9 +10,7 @@ theories/proto/proto_def.v
theories/proto/proto_specs.v
theories/proto/proto_enc.v
theories/proto/branching.v
theories/examples/examples.v
theories/examples/proofs.v
theories/examples/proofs_enc.v
theories/examples/branching_examples.v
theories/examples/branching_proofs.v
theories/examples/list_sort.v
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic Require Import invariants.
From osiris.proto Require Import channel branching.
Section BranchingExamples.
Context `{!heapG Σ} (N : namespace).
Definition branch_example b : expr :=
(let: "c" := new_chan #() in
select "c" #Left #b;;
Fork(branch: "c" @ #Right
left send "c" #Right #5
right #());;
(if: #b then recv "c" #Left else #()))%E.
End BranchingExamples.
\ No newline at end of file
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic Require Import invariants.
From osiris.proto Require Import branching.
From osiris.examples Require Import branching_examples.
Definition branch_example b : expr :=
(let: "c" := new_chan #() in
select "c" #Left #b;;
Fork(branch: "c" @ #Right
left send "c" #Right #5
right #());;
(if: #b then recv "c" #Left else #()))%E.
Section BranchingExampleProofs.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Context `{!heapG Σ, !logrelG val Σ}.
Lemma branch_proof b :
{{{ True }}}
......@@ -17,29 +20,24 @@ Section BranchingExampleProofs.
| Right => v = #()
end }}}.
Proof.
iIntros (Φ H) "HΦ".
iIntros (Φ _) "HΦ".
rewrite /branch_example.
wp_apply (new_chan_st_spec N
((<?> v @ v = 5, TEnd) <+> (TEnd)))=> //;
wp_apply (new_chan_st_spec nroot ((<?> v @ v = 5, TEnd) <+> TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]".
wp_apply (select_st_spec with "Hstl");
iIntros "Hstl".
wp_apply (select_st_spec with "Hstl"); iIntros "Hstl".
wp_pures.
wp_apply (wp_fork with "[Hstr]").
- iNext.
simpl.
wp_apply (branch_st_spec with "Hstr")=> //;
iIntros (v) "[Hstr | Hstr]"; iDestruct "Hstr" as (->) "Hstr".
+ wp_pures.
wp_apply (send_st_spec N Z with "[$Hstr //]").
iIntros "Hstr". done.
+ wp_pures. done.
iIntros (v) "[[-> Hstr]|[-> Hstr]]".
+ wp_pures.
wp_apply (send_st_spec (A:=Z) with "[$Hstr //]"); auto.
+ by wp_pures.
- destruct b.
+ wp_apply (recv_st_spec N Z with "Hstl");
iIntros (v) "[Hstl HP]".
iDestruct "HP" as %->.
+ wp_apply (recv_st_spec (A:=Z) with "Hstl");
iIntros (v) "[Hstl ->]".
by iApply "HΦ".
+ wp_pures. by iApply "HΦ".
Qed.
End BranchingExampleProofs.
\ No newline at end of file
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic Require Import invariants.
From osiris.proto Require Import proto_specs.
Section Examples.
Context `{!heapG Σ} (N : namespace).
Definition seq_example : expr :=
(let: "c" := new_chan #() in
send "c" #Left #5;;
recv "c" #Right)%E.
Definition par_example : expr :=
(let: "c" := new_chan #() in
Fork(send "c" #Left #5);;
recv "c" #Right)%E.
Definition par_2_example : expr :=
(let: "c" := new_chan #() in
Fork(let: "v" := recv "c" #Right in send "c" #Right ("v"+#2));;
send "c" #Left #5;;recv "c" #Left)%E.
Definition heaplet_example : expr :=
(let: "c" := new_chan #() in
Fork(send "c" #Left (ref #5));;
!(recv "c" #Right))%E.
Definition channel_example : expr :=
(let: "c" := new_chan #() in
Fork(
let: "c'" := new_chan #() in
send "c" #Left ("c'");; send "c'" #Left #5);;
let: "c'" := recv "c" #Right in
recv "c'" #Right
)%E.
Definition bad_seq_example : expr :=
(let: "c" := new_chan #() in
let: "v" := recv "c" #Right in
send "c" #Left #5;; "v")%E.
Definition bad_par_example : expr :=
(let: "c" := new_chan #() in
Fork(#());;
recv "c" #Right)%E.
Definition bad_interleave_example : expr :=
(let: "c" := new_chan #() in
let: "c'" := new_chan #() in
Fork(recv "c" #Right;; send "c'" #Right #5);;
recv "c'" #Left;; send "c" #Left #5)%E.
End Examples.
\ No newline at end of file
From stdpp Require Import sorting.
Require Import Coq.Lists.List.
Require Import Omega.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic Require Import invariants.
From osiris.proto Require Import list channel proto_enc.
Section ListSortExample.
Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
Context `{!heapG Σ, !logrelG val Σ} (N : namespace).
Section SortService.
Context `{EncDec T}.
Context `{ValEncDec T}.
Context (R : relation T) `{!Total R} `{ x y, Decision (R x y)}.
Definition lsplit_ref : val :=
......@@ -19,13 +14,13 @@ Section ListSortExample.
(ref (Fst "ys_zs"), ref (Snd ("ys_zs"))).
Lemma lsplit_ref_spec lxs (x : T) (xs : list T) :
{{{ lxs encode (x::xs) }}}
{{{ lxs val_encode (x :: xs) }}}
lsplit_ref #lxs
{{{ lys lzs ys zs, RET (#lys,#lzs);
(x::xs) = ys++zs
lxs encode (x::xs)
lys encode ys
lzs encode zs }}}.
{{{ lys lzs ys zs, RET (#lys, #lzs);
x :: xs = ys ++ zs
lxs val_encode (x :: xs)
lys val_encode ys
lzs val_encode zs }}}.
Proof.
iIntros (Φ) "Hhd HΦ".
wp_lam. wp_load. wp_apply (lsplit_spec)=> //. iIntros (ys zs <-).
......@@ -60,14 +55,14 @@ Section ListSortExample.
Definition cmp_spec (cmp : val) : iProp Σ :=
( x y, {{{ True }}}
cmp (encode x) (encode y)
{{{ RET encode (bool_decide (R x y)); True}}})%I.
cmp (val_encode x) (val_encode y)
{{{ RET val_encode (bool_decide (R x y)); True}}})%I.
Lemma lmerge_spec (cmp : val) (ys zs : list T) :
cmp_spec cmp -
{{{ True }}}
lmerge cmp (encode ys) (encode zs)
{{{ RET (encode (list_merge (R) ys zs)); True }}}.
lmerge cmp (val_encode ys) (val_encode zs)
{{{ RET val_encode (list_merge R ys zs); True }}}.
Proof.
revert ys zs.
iLöb as "IH".
......@@ -103,8 +98,8 @@ Section ListSortExample.
Lemma lmerge_ref_spec (cmp : val) ldx tmp ys zs :
cmp_spec cmp -
{{{ ldx tmp }}}
lmerge_ref cmp #ldx (encode ys) (encode zs)
{{{ RET #(); ldx encode (list_merge R ys zs) }}}.
lmerge_ref cmp #ldx (val_encode ys) (val_encode zs)
{{{ RET #(); ldx val_encode (list_merge R ys zs) }}}.
Proof.
iIntros "#Hcmp_spec".
iIntros (Φ).
......@@ -139,12 +134,12 @@ Section ListSortExample.
Definition sort_protocol xs : proto val (iProp Σ) :=
(<?> cmp @ cmp_spec cmp,
<?> l @ l encode xs,
<?> l @ l val_encode xs,
<!> l' @ l = l'
( ys : list T,
l' encode ys
Sorted (R) ys
Permutation ys xs),
l' val_encode ys
Sorted R ys
Permutation ys xs),
TEnd).
Lemma list_sort_service_spec γ c xs :
......@@ -156,23 +151,22 @@ Section ListSortExample.
iLöb as "IH".
iIntros (γ c xs Φ) "Hstr HΦ".
wp_lam.
wp_apply (recv_st_spec N val with "Hstr").
wp_apply (recv_st_spec (A:=val) with "Hstr").
iIntros (cmp) "[Hstr #Hcmp_spec]".
wp_pures.
wp_apply (recv_st_spec N loc with "Hstr").
iIntros (v) "Hstr".
iDestruct "Hstr" as "[Hstr HP]".
wp_apply (recv_st_spec (A:=loc) with "Hstr").
iIntros (v) "[Hstr HP]".
wp_load.
destruct xs.
{
wp_apply (llength_spec)=> //; iIntros (_).
wp_apply (send_st_spec N loc with "[HP Hstr]")=> //. iFrame.
wp_apply (send_st_spec (A:=loc) with "[HP Hstr]")=> //. iFrame.
eauto 10 with iFrame.
}
destruct xs.
{
wp_apply (llength_spec)=> //; iIntros (_).
wp_apply (send_st_spec N loc with "[HP Hstr]")=> //. iFrame.
wp_apply (send_st_spec (A:=loc) with "[HP Hstr]")=> //. iFrame.
eauto 10 with iFrame.
}
wp_apply (llength_spec)=> //; iIntros (_).
......@@ -191,19 +185,19 @@ Section ListSortExample.
iIntros (cz γz) "[Hstlz Hstrz]".
wp_apply (wp_fork with "[Hstrz]").
{ iNext. iApply ("IH" with "Hstrz"). iNext. by iIntros "Hstrz". }
wp_apply (send_st_spec N val with "[Hstly]"). iFrame. done.
wp_apply (send_st_spec (A:=val) with "[Hstly]"). iFrame. done.
iIntros "Hstly".
wp_apply (send_st_spec N loc with "[Hhdy Hstly]"). iFrame.
wp_apply (send_st_spec (A:=loc) with "[Hhdy Hstly]"). iFrame.
iIntros "Hstly".
wp_apply (send_st_spec N val with "[Hstlz]"). iFrame. done.
wp_apply (send_st_spec (A:=val) with "[Hstlz]"). iFrame. done.
iIntros "Hstlz".
wp_apply (send_st_spec N loc with "[Hhdz Hstlz]"). iFrame.
wp_apply (send_st_spec (A:=loc) with "[Hhdz Hstlz]"). iFrame.
iIntros "Hstlz".
wp_apply (recv_st_spec N loc with "Hstly").
wp_apply (recv_st_spec (A:=loc) with "Hstly").
iIntros (ly') "[Hstly Hys']".
iDestruct "Hys'" as (<- ys') "(Hys' & Hys'_sorted_of)".
iDestruct "Hys'_sorted_of" as %[Hys'_sorted Hys'_perm].
wp_apply (recv_st_spec N loc with "Hstlz").
wp_apply (recv_st_spec (A:=loc) with "Hstlz").
iIntros (lz') "[Hstlz Hzs']".
iDestruct "Hzs'" as (<- zs') "(Hzs' & Hzs'_sorted_of)".
iDestruct "Hzs'_sorted_of" as %[Hzs'_sorted Hzs'_perm].
......@@ -211,7 +205,7 @@ Section ListSortExample.
wp_load.
wp_apply (lmerge_ref_spec with "Hcmp_spec Hhdx").
iIntros "Hhdx".
wp_apply (send_st_spec N loc with "[Hstr Hhdx]").
wp_apply (send_st_spec (A:=loc) with "[Hstr Hhdx]").
{
iFrame.
iSplit=> //.
......@@ -233,8 +227,8 @@ Section ListSortExample.
Lemma compare_vals_spec (x y : Z) :
{{{ True }}}
compare_vals (encode x) (encode y)
{{{ RET (encode (bool_decide (x y))); True }}}.
compare_vals (val_encode x) (val_encode y)
{{{ RET val_encode (bool_decide (x y)); True }}}.
Proof. iIntros (Φ) "_ HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Definition list_sort : val :=
......@@ -246,9 +240,9 @@ Section ListSortExample.
recv "c" #Left.
Lemma list_sort_spec l xs :
{{{ l encode xs }}}
{{{ l val_encode xs }}}
list_sort #l
{{{ ys, RET #l; l encode ys Sorted () ys Permutation ys xs }}}.
{{{ ys, RET #l; l val_encode ys Sorted () ys Permutation ys xs }}}.
Proof.
iIntros (Φ) "Hc HΦ".
wp_lam.
......@@ -259,15 +253,15 @@ Section ListSortExample.
iApply (list_sort_service_spec () γ c xs with "Hstr").
iNext. iNext. iIntros "Hstr". done.
}
wp_apply (send_st_spec N val with "[$Hstl]").
wp_apply (send_st_spec (A:=val) with "[$Hstl]").
{
iIntros (x y Φ').
iApply compare_vals_spec=> //.
}
iIntros "Hstl".
wp_apply (send_st_spec N loc with "[Hc $Hstl]"). iFrame.
wp_apply (send_st_spec (A:=loc) with "[Hc $Hstl]"). iFrame.
iIntros "Hstl".
wp_apply (recv_st_spec N loc with "Hstl").
wp_apply (recv_st_spec (A:=loc) with "Hstl").
iIntros (v) "[Hstl HP]".
iDestruct "HP" as (<- ys) "[Hys Hys_sorted_of]".
iApply "HΦ". iFrame.
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
From osiris.proto Require Import proto_enc.
From osiris.examples Require Import examples.
Definition seq_example : expr :=
(let: "c" := new_chan #() in
send "c" #Left #5;;
recv "c" #Right)%E.
Definition par_example : expr :=
(let: "c" := new_chan #() in
Fork(send "c" #Left #5);;
recv "c" #Right)%E.
Definition par_2_example : expr :=
(let: "c" := new_chan #() in
Fork(let: "v" := recv "c" #Right in send "c" #Right ("v"+#2));;
send "c" #Left #5;;recv "c" #Left)%E.
Definition heaplet_example : expr :=
(let: "c" := new_chan #() in
Fork(send "c" #Left (ref #5));;
!(recv "c" #Right))%E.
Definition channel_example : expr :=
(let: "c" := new_chan #() in
Fork(
let: "c'" := new_chan #() in
send "c" #Left ("c'");; send "c'" #Left #5);;
let: "c'" := recv "c" #Right in
recv "c'" #Right
)%E.
Definition bad_seq_example : expr :=
(let: "c" := new_chan #() in
let: "v" := recv "c" #Right in
send "c" #Left #5;; "v")%E.
Definition bad_par_example : expr :=
(let: "c" := new_chan #() in
Fork(#());;
recv "c" #Right)%E.
Definition bad_interleave_example : expr :=
(let: "c" := new_chan #() in
let: "c'" := new_chan #() in
Fork(recv "c" #Right;; send "c'" #Right #5);;
recv "c'" #Left;; send "c" #Left #5)%E.
Section ExampleProofsEnc.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Context `{!heapG Σ, !logrelG val Σ}.
Lemma seq_proof :
{{{ True }}} seq_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
iIntros (Φ _) "HΦ".
rewrite /seq_example.
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_spec N Z with "[$Hstl //]");
iIntros "Hstl".
wp_apply (recv_st_spec N Z with "[Hstr]"). iApply "Hstr".
iIntros (v) "[Hstr HP]".
wp_apply (new_chan_st_spec nroot (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_spec (A:=Z) with "[$Hstl //]"); iIntros "Hstl".
wp_apply (recv_st_spec (A:=Z) with "Hstr").
iIntros (v) "[Hstr ->]".
iApply "HΦ".
iDestruct "HP" as %->.
eauto.
Qed.
......@@ -31,44 +68,34 @@ Section ExampleProofsEnc.
par_2_example
{{{ (v:Z), RET #v; 7 v }}}.
Proof.
iIntros (Φ H) "HΦ".
iIntros (Φ _) "HΦ".
rewrite /par_2_example.
wp_apply (new_chan_st_spec N
(<!> v @ 5 v,
<?> v' @ v+2 v',
TEnd))=> //;
wp_apply (new_chan_st_spec nroot
(<!> v @ 5 v, <?> v' @ v+2 v', TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstr]").
- iNext.
wp_apply (recv_st_spec N Z with "Hstr");
iIntros (v) "[Hstr HP]".
wp_apply (send_st_spec N Z with "[$Hstr //]");
iIntros "Hstr".
wp_apply (recv_st_spec (A:=Z) with "Hstr"); iIntros (v) "[Hstr HP]".
wp_apply (send_st_spec (A:=Z) with "[$Hstr //]"); iIntros "Hstr".
eauto.
- wp_apply (send_st_spec N Z with "[$Hstl //]");
iIntros "Hstl".
wp_apply (recv_st_spec N Z with "Hstl");
iIntros (v) "[Hstl HP]".
iApply "HΦ".
iDestruct "HP" as %HP.
iPureIntro. lia.
- wp_apply (send_st_spec (A:=Z) with "[$Hstl //]"); iIntros "Hstl".
wp_apply (recv_st_spec (A:=Z) with "Hstl"); iIntros (v) "[Hstl %]".
iApply "HΦ". iPureIntro. lia.
Qed.
Lemma heaplet_proof :
{{{ True }}} heaplet_example {{{ v l, RET v; v = #5 l v }}}.
Proof.
rewrite /heaplet_example.
iIntros (Φ H) "HΦ".
wp_apply (new_chan_st_spec N (<!> v @ (v #5), TEnd))=> //;
iIntros (Φ _) "HΦ".
wp_apply (new_chan_st_spec nroot (<!> v @ (v #5), TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
wp_alloc l as "HP".
wp_apply (send_st_spec N loc with "[$Hstl HP]")=> //;
iIntros "Hstl".
wp_apply (send_st_spec (A:=loc) with "[$Hstl HP]")=> //; iIntros "Hstl".
eauto.
- wp_apply (recv_st_spec N loc with "Hstr");
iIntros (v) "[Hstr HP]".
- wp_apply (recv_st_spec (A:=loc) with "Hstr"); iIntros (v) "[Hstr HP]".
wp_load.
iApply "HΦ".
by iFrame.
......@@ -77,43 +104,36 @@ Section ExampleProofsEnc.
Lemma channel_proof :
{{{ True }}} channel_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
iIntros (Φ _) "HΦ".
rewrite /channel_example.
wp_apply (new_chan_st_spec N
(<!> v @ ( γ, v @ Right : <?> v @ v = 5, TEnd {N,γ}),
wp_apply (new_chan_st_spec nroot
(<!> v @ ( γ, v @ Right : <?> v @ v = 5, TEnd {nroot,γ}),
TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (send_st_spec N val with "[Hstl Hstr']");
wp_apply (new_chan_st_spec nroot (<!> v @ v = 5, TEnd))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (send_st_spec (A:=val) with "[Hstl Hstr']");
first by eauto 10 with iFrame.
iIntros "Hstl".
wp_apply (send_st_spec N Z with "[$Hstl' //]");
iIntros "Hstl'".
wp_apply (send_st_spec (A:=Z) with "[$Hstl' //]"); iIntros "Hstl'".
eauto.
- wp_apply (recv_st_spec N val with "Hstr");
iIntros (v) "[Hstr Hstr']".
- wp_apply (recv_st_spec (A:=val) with "Hstr"); iIntros (v) "[Hstr Hstr']".
iDestruct "Hstr'" as (γ') "Hstr'".
wp_apply (recv_st_spec N Z with "Hstr'");
iIntros (v') "[Hstr' HP]".
iDestruct "HP" as %<-.
wp_apply (recv_st_spec (A:=Z) with "Hstr'"); iIntros (v') "[Hstr' <-]".
by iApply "HΦ".
Qed.
Lemma bad_seq_proof :
{{{ True }}} bad_seq_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
iIntros (Φ _) "HΦ".
rewrite /bad_seq_example.
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
wp_apply (new_chan_st_spec nroot (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (recv_st_spec N Z with "Hstr");
iIntros (v) "[Hstr HP]".
wp_apply (send_st_spec N Z with "[$Hstl //]");
iIntros "Hstl".
iDestruct "HP" as %->.
wp_apply (recv_st_spec (A:=Z) with "Hstr"); iIntros (v) "[Hstr ->]".
wp_apply (send_st_spec (A:=Z) with "[$Hstl //]"); iIntros "Hstl".
wp_pures.
by iApply "HΦ".
Qed.
......@@ -121,36 +141,30 @@ Section ExampleProofsEnc.
Lemma bad_par_proof :
{{{ True }}} bad_par_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
iIntros (Φ _) "HΦ".
rewrite /bad_par_example.
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
wp_apply (new_chan_st_spec nroot (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext. by wp_finish.
- wp_apply (recv_st_spec _ with "Hstr");
iIntros (v) "[Hstr HP]".
iDestruct "HP" as %->.
- wp_apply (recv_st_spec (A:=Z) with "Hstr"); iIntros (v) "[Hstr ->]".
by iApply "HΦ".
Qed.
Lemma bad_interleave_proof :
{{{ True }}} bad_interleave_example {{{ v, RET v; v = #() }}}.
Proof.
iIntros (Φ H) "HΦ".
iIntros (Φ _) "HΦ".
rewrite /bad_interleave_example.
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
wp_apply (new_chan_st_spec nroot (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (new_chan_st_spec N (<?> v @ v = 5, TEnd))=> //;
wp_apply (new_chan_st_spec nroot (<?> v @ v = 5, TEnd))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (wp_fork with "[Hstr Hstr']").
- iNext. wp_apply (recv_st_spec _ with "Hstr");
iIntros (v) "[Hstr HP]".
wp_apply (send_st_spec _ Z with "[$Hstr' //]"). eauto.
- wp_apply (recv_st_spec _ Z with "[$Hstl' //]");
iIntros (v) "[Hstl' HP]".