diff --git a/_CoqProject b/_CoqProject
index 843f066acc79b8e5e9b25720b75aa4983368a4ba..f187ca70e541a7470e6af79da9e937579ce20485 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -61,4 +61,5 @@ multi_actris/channel/proto.v
multi_actris/channel/channel.v
multi_actris/channel/proofmode.v
multi_actris/examples/basics.v
+multi_actris/examples/two_buyer.v
multi_actris/examples/leader_election.v
diff --git a/multi_actris/channel/proofmode.v b/multi_actris/channel/proofmode.v
index 5f9d7b8fb105122ee7dc64e208c6ecb50395aef1..319de3ca5ca601e6e0aeb357b7436c01aef211e1 100644
--- a/multi_actris/channel/proofmode.v
+++ b/multi_actris/channel/proofmode.v
@@ -396,11 +396,11 @@ Ltac ltac1_list_iter2 tac l1 l2 :=
Tactic Notation "wp_new_chan" constr(prot) "as"
"(" simple_intropattern_list(xs) ")" constr_list(pats) :=
wp_smart_apply (new_chan_spec prot);
- [set_solver| |iIntros (?) "?"];
+ [set_solver| |iIntros (_cs) "?"];
[|ltac1_list_iter2 ltac:(fun x y => wp_get_chan (x) y) xs pats].
Tactic Notation "wp_new_chan" constr(prot) "with" constr(lem) "as"
"(" simple_intropattern_list(xs) ")" constr_list(pats) :=
wp_smart_apply (new_chan_spec prot);
- [set_solver|by iApply lem|iIntros (?) "?"];
+ [set_solver|by iApply lem|iIntros (_cs) "?"];
ltac1_list_iter2 ltac:(fun x y => wp_get_chan (x) y) xs pats.
diff --git a/multi_actris/examples/basics.v b/multi_actris/examples/basics.v
index 36c500f5638399b41d1f224f642729436330879d..82a0173265dedc632b60bc59b6d3be84fa182d39 100644
--- a/multi_actris/examples/basics.v
+++ b/multi_actris/examples/basics.v
@@ -294,91 +294,6 @@ Section parallel.
End parallel.
-Section two_buyer.
- Context `{!heapGS Σ}.
-
- Definition two_buyer_prot : list (iProto Σ) :=
- [(<(Send, 1) @ (title:Z)> MSG #title ;
- <(Recv, 1) @ (quote:Z)> MSG #quote ;
- <(Send, 2) @ (contrib:Z)> MSG #contrib ; END)%proto;
- (<(Recv, 0) @ (title:Z)> MSG #title ;
- <(Send, 0) @ (quote:Z)> MSG #quote ;
- <(Send, 2)> MSG #quote ;
- <(Recv, 2) @ (b:bool)> MSG #b ;
- if b then
- <(Recv, 2) @ (address:Z)> MSG #address ;
- <(Send, 2) @ (date:Z)> MSG #date ; END
- else END)%proto;
- (<(Recv, 1) @ (quote:Z)> MSG #quote ;
- <(Recv, 0) @ (contrib:Z)> MSG #contrib ;
- if bool_decide (contrib >= quote/2)%Z then
- <(Send, 1)> MSG #true ;
- <(Send, 1) @ (address:Z)> MSG #address ;
- <(Recv, 1) @ (date:Z)> MSG #date ; END
- else
- <(Send, 1)> MSG #false ; END)%proto].
-
- Lemma two_buyer_prot_consistent :
- ⊢ iProto_consistent two_buyer_prot.
- Proof.
- rewrite /two_buyer_prot. iProto_consistent_take_steps.
- case_bool_decide; iProto_consistent_take_steps.
- Qed.
-
-End two_buyer.
-
-Section two_buyer_ref.
- Context `{!heapGS Σ}.
-
- Definition two_buyer_ref_b1_prot : iProto Σ :=
- (<(Send, 1) @ (title:Z)> MSG #title ;
- <(Recv, 1) @ (quote:Z)> MSG #quote ;
- <(Send, 2) @ (l : loc) (amount:Z) (contrib:Z)>
- MSG (#l,#contrib) {{ l ↦ #amount }} ;
- <(Recv, 2) @ (b : bool)>
- MSG #b {{ l ↦ #(if b then amount - contrib else amount) }};
- END)%proto.
-
- Definition two_buyer_ref_s_prot : iProto Σ :=
- (<(Recv, 0) @ (title:Z)> MSG #title ;
- <(Send, 0) @ (quote:Z)> MSG #quote ;
- <(Send, 2)> MSG #quote ;
- <(Recv, 2) @ (b:bool)> MSG #b ;
- if b then
- <(Recv, 2) @ (l2 : loc) (amount2:Z) (address:Z)>
- MSG (#l2,#address) {{ l2 ↦ #amount2 }} ;
- <(Send, 2) @ (date : Z)> MSG #date {{ l2 ↦ #(amount2-quote) }}; END
- else END)%proto.
-
- Definition two_buyer_ref_b2_prot : iProto Σ :=
- (<(Recv, 1) @ (quote:Z)> MSG #quote ;
- <(Recv, 0) @ (l1 : loc) (amount1:Z) (contrib:Z)>
- MSG (#l1,#contrib) {{ l1 ↦ #amount1 }};
- <(Send, 0) @ (b : bool)>
- MSG #b {{ l1 ↦ #(if b then amount1 - contrib else amount1) }};
- <(Send, 1)> MSG #b;
- if b then
- <(Send, 1) @ (l2 : loc) (amount2:Z) (address:Z)>
- MSG (#l2,#address) {{ l2 ↦ #amount2 }} ;
- <(Recv, 1) @ (date : Z)> MSG #date {{ l2 ↦ #(amount2-quote) }};
- END
- else END)%proto.
-
- Definition two_buyer_ref_prot : list (iProto Σ) :=
- [two_buyer_ref_b1_prot;
- two_buyer_ref_s_prot;
- two_buyer_ref_b2_prot].
-
- (* TODO: Anonymous variable in this is unsatisfactory *)
- Lemma two_buyer_ref_prot_consistent :
- ⊢ iProto_consistent two_buyer_ref_prot.
- Proof.
- rewrite /two_buyer_prot. iProto_consistent_take_steps.
- iNext. destruct x4; iProto_consistent_take_steps.
- Qed.
-
-End two_buyer_ref.
-
Section forwarder.
Context `{!heapGS Σ}.
diff --git a/multi_actris/examples/two_buyer.v b/multi_actris/examples/two_buyer.v
new file mode 100644
index 0000000000000000000000000000000000000000..15eef77c44bf1d0a46f101ecd2da09e3480877cf
--- /dev/null
+++ b/multi_actris/examples/two_buyer.v
@@ -0,0 +1,133 @@
+From multi_actris.channel Require Import proofmode.
+Set Default Proof Using "Type".
+
+Definition buyer1_prog : val :=
+ λ: "cb1" "s" "b2",
+ send "cb1" "s" #0;;
+ let: "quote" := recv "cb1" "s" in
+ send "cb1" "b2" ("quote" `rem` #2);;
+ recv "cb1" "b2";; #().
+
+Definition seller_prog : val :=
+ λ: "cs" "b1" "b2",
+ let: "title" := recv "cs" "b1" in
+ send "cs" "b1" #42;; send "cs" "b2" #42;;
+ let: "b" := recv "cs" "b2" in
+ if: "b" then
+ send "cs" "b2" #0
+ else #().
+
+Definition buyer2_prog : val :=
+ λ: "cb2" "b1" "s",
+ let: "quote" := recv "cb2" "s" in
+ let: "contrib" := recv "cb2" "b1" in
+ if: ("quote" - "contrib" < #100)
+ then send "cb2" "s" #true;; send "cb2" "b1" #true;;
+ recv "cb2" "s"
+ else #().
+
+Definition two_buyer_prog : val :=
+ λ: <>,
+ let: "cs" := new_chan #3 in
+ let: "b1" := get_chan "cs" #0 in
+ let: "s" := get_chan "cs" #1 in
+ let: "b2" := get_chan "cs" #2 in
+ Fork (seller_prog "s" #0 #2);;
+ Fork (buyer2_prog "b2" #0 #1);;
+ buyer1_prog "b1" #1 #2.
+
+Section two_buyer.
+ Context `{!heapGS Σ, !chanG Σ}.
+
+ Definition buyer1_prot s b2 : iProto Σ :=
+ (<(Send, s) @ (title:Z)> MSG #title ;
+ <(Recv, s) @ (quote:Z)> MSG #quote ;
+ <(Send, b2) @ (contrib:Z)> MSG #contrib ;
+ <(Recv, b2) @ (b:bool)> MSG #b; END)%proto.
+
+ Lemma buyer1_spec c s b2 :
+ {{{ c ↣ buyer1_prot s b2 }}}
+ buyer1_prog c #s #b2
+ {{{ RET #(); True }}}.
+ Proof.
+ iIntros (Φ) "Hc HΦ". wp_lam.
+ wp_send with "[//]".
+ wp_recv (quote) as "_".
+ wp_send with "[//]".
+ wp_recv (b) as "_". wp_pures.
+ by iApply "HΦ".
+ Qed.
+
+ Definition seller_prot b1 b2 : iProto Σ :=
+ (<(Recv, b1) @ (title:Z)> MSG #title ;
+ <(Send, b1) @ (quote:Z)> MSG #quote ;
+ <(Send, b2)> MSG #quote ;
+ <(Recv, b2) @ (b:bool)> MSG #b ;
+ if b then
+ <(Send, b2) @ (date:Z)> MSG #date ; END
+ else END)%proto.
+
+ Lemma seller_spec c b1 b2 :
+ {{{ c ↣ seller_prot b1 b2 }}}
+ seller_prog c #b1 #b2
+ {{{ b, RET #b; True }}}.
+ Proof.
+ iIntros (Φ) "Hc HΦ". wp_lam.
+ wp_recv (title) as "_".
+ wp_send with "[//]".
+ wp_send with "[//]".
+ wp_recv (b) as "_".
+ destruct b.
+ - wp_pures. wp_send with "[//]". by iApply "HΦ".
+ - wp_pures. by iApply "HΦ".
+ Qed.
+
+ Definition buyer2_prot b1 s : iProto Σ :=
+ (<(Recv, s) @ (quote:Z)> MSG #quote ;
+ <(Recv, b1) @ (contrib:Z)> MSG #contrib ;
+ <(Send, s) @ (b:bool)> MSG #b ;
+ <(Send, b1)> MSG #b ;
+ if b then <(Recv, s) @ (date:Z)> MSG #date ; END
+ else <(Send, s)> MSG #false ; END)%proto.
+
+ Lemma buyer2_spec c b1 s :
+ {{{ c ↣ buyer2_prot b1 s }}}
+ buyer2_prog c #b1 #s
+ {{{ b, RET #b; True }}}.
+ Proof.
+ iIntros (Φ) "Hc HΦ". wp_lam.
+ wp_recv (quote) as "_".
+ wp_recv (contrib) as "_".
+ wp_pures. case_bool_decide.
+ - wp_send with "[//]". wp_send with "[//]". wp_recv (date) as "_".
+ by iApply "HΦ".
+ - wp_pures. by iApply "HΦ".
+ Qed.
+
+ Definition two_buyer_prot : list (iProto Σ) :=
+ [buyer1_prot 1 2 ; seller_prot 0 2; buyer2_prot 0 1].
+
+ Lemma two_buyer_prot_consistent :
+ ⊢ iProto_consistent two_buyer_prot.
+ Proof.
+ rewrite /two_buyer_prot. iProto_consistent_take_steps.
+ destruct x2; iProto_consistent_take_steps.
+ Qed.
+
+ Lemma two_buyer_spec :
+ {{{ True }}}
+ two_buyer_prog #()
+ {{{ RET #(); True }}}.
+ Proof using chanG0 heapGS0 Σ.
+ iIntros (Φ) "Hc HΦ". wp_lam.
+ wp_new_chan two_buyer_prot with two_buyer_prot_consistent
+ as (???) "Hcb1" "Hcs" "Hcb2".
+ wp_smart_apply (wp_fork with "[Hcs]").
+ { by iApply (seller_spec with "Hcs"). }
+ wp_smart_apply (wp_fork with "[Hcb2]").
+ { by iApply (buyer2_spec with "Hcb2"). }
+ wp_smart_apply (buyer1_spec with "Hcb1").
+ by iApply "HΦ".
+ Qed.
+
+End two_buyer.