diff --git a/_CoqProject b/_CoqProject
index 858ff55ee9aece47f01b08660ec974a8b57f4cf7..1041167075f165b0329e09d7065ccf3ed9d76600 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,52 +1,64 @@
--Q theories actris
+-Q actris actris
+-Q multris multris
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-theories/utils/llist.v
-theories/utils/compare.v
-theories/utils/contribution.v
-theories/utils/group.v
-theories/utils/cofe_solver_2.v
-theories/utils/switch.v
-theories/channel/proto_model.v
-theories/channel/proto.v
-theories/channel/channel.v
-theories/channel/proofmode.v
-theories/examples/basics.v
-theories/examples/equivalence.v
-theories/examples/sort.v
-theories/examples/sort_br_del.v
-theories/examples/sort_fg.v
-theories/examples/par_map.v
-theories/examples/map_reduce.v
-theories/examples/swap_mapper.v
-theories/examples/subprotocols.v
-theories/examples/list_rev.v
-theories/examples/rpc.v
-theories/examples/pizza.v
-theories/logrel/model.v
-theories/logrel/telescopes.v
-theories/logrel/subtyping.v
-theories/logrel/contexts.v
-theories/logrel/term_types.v
-theories/logrel/session_types.v
-theories/logrel/operators.v
-theories/logrel/term_typing_judgment.v
-theories/logrel/subtyping_rules.v
-theories/logrel/term_typing_rules.v
-theories/logrel/session_typing_rules.v
-theories/logrel/napp.v
-theories/logrel/lib/mutex.v
-theories/logrel/lib/list.v
-theories/logrel/lib/par_start.v
-theories/logrel/examples/pair.v
-theories/logrel/examples/par_recv.v
-theories/logrel/examples/rec_subtyping.v
-theories/logrel/examples/choice_subtyping.v
-theories/logrel/examples/mapper.v
-theories/logrel/examples/mapper_list.v
-theories/logrel/examples/compute_service.v
-theories/logrel/examples/compute_client_list.v
+actris/utils/llist.v
+actris/utils/compare.v
+actris/utils/contribution.v
+actris/utils/group.v
+actris/utils/cofe_solver_2.v
+actris/utils/switch.v
+actris/channel/proto_model.v
+actris/channel/proto.v
+actris/channel/channel.v
+actris/channel/proofmode.v
+actris/examples/basics.v
+actris/examples/equivalence.v
+actris/examples/sort.v
+actris/examples/sort_br_del.v
+actris/examples/sort_fg.v
+actris/examples/par_map.v
+actris/examples/map_reduce.v
+actris/examples/swap_mapper.v
+actris/examples/subprotocols.v
+actris/examples/list_rev.v
+actris/examples/rpc.v
+actris/examples/pizza.v
+actris/logrel/model.v
+actris/logrel/telescopes.v
+actris/logrel/subtyping.v
+actris/logrel/contexts.v
+actris/logrel/term_types.v
+actris/logrel/session_types.v
+actris/logrel/operators.v
+actris/logrel/term_typing_judgment.v
+actris/logrel/subtyping_rules.v
+actris/logrel/term_typing_rules.v
+actris/logrel/session_typing_rules.v
+actris/logrel/napp.v
+actris/logrel/lib/mutex.v
+actris/logrel/lib/list.v
+actris/logrel/lib/par_start.v
+actris/logrel/examples/pair.v
+actris/logrel/examples/par_recv.v
+actris/logrel/examples/rec_subtyping.v
+actris/logrel/examples/choice_subtyping.v
+actris/logrel/examples/mapper.v
+actris/logrel/examples/mapper_list.v
+actris/logrel/examples/compute_service.v
+actris/logrel/examples/compute_client_list.v
+
+multris/utils/cofe_solver_2.v
+multris/utils/matrix.v
+multris/channel/proto_model.v
+multris/channel/proto.v
+multris/channel/channel.v
+multris/channel/proofmode.v
+multris/examples/basics.v
+multris/examples/two_buyer.v
+multris/examples/three_buyer.v
+multris/examples/leader_election.v
diff --git a/theories/channel/channel.v b/actris/channel/channel.v
similarity index 100%
rename from theories/channel/channel.v
rename to actris/channel/channel.v
diff --git a/theories/channel/proofmode.v b/actris/channel/proofmode.v
similarity index 100%
rename from theories/channel/proofmode.v
rename to actris/channel/proofmode.v
diff --git a/theories/channel/proto.v b/actris/channel/proto.v
similarity index 100%
rename from theories/channel/proto.v
rename to actris/channel/proto.v
diff --git a/theories/channel/proto_model.v b/actris/channel/proto_model.v
similarity index 100%
rename from theories/channel/proto_model.v
rename to actris/channel/proto_model.v
diff --git a/theories/examples/basics.v b/actris/examples/basics.v
similarity index 100%
rename from theories/examples/basics.v
rename to actris/examples/basics.v
diff --git a/theories/examples/equivalence.v b/actris/examples/equivalence.v
similarity index 100%
rename from theories/examples/equivalence.v
rename to actris/examples/equivalence.v
diff --git a/theories/examples/list_rev.v b/actris/examples/list_rev.v
similarity index 100%
rename from theories/examples/list_rev.v
rename to actris/examples/list_rev.v
diff --git a/theories/examples/map_reduce.v b/actris/examples/map_reduce.v
similarity index 100%
rename from theories/examples/map_reduce.v
rename to actris/examples/map_reduce.v
diff --git a/theories/examples/par_map.v b/actris/examples/par_map.v
similarity index 100%
rename from theories/examples/par_map.v
rename to actris/examples/par_map.v
diff --git a/theories/examples/pizza.v b/actris/examples/pizza.v
similarity index 100%
rename from theories/examples/pizza.v
rename to actris/examples/pizza.v
diff --git a/theories/examples/rpc.v b/actris/examples/rpc.v
similarity index 100%
rename from theories/examples/rpc.v
rename to actris/examples/rpc.v
diff --git a/theories/examples/sort.v b/actris/examples/sort.v
similarity index 100%
rename from theories/examples/sort.v
rename to actris/examples/sort.v
diff --git a/theories/examples/sort_br_del.v b/actris/examples/sort_br_del.v
similarity index 100%
rename from theories/examples/sort_br_del.v
rename to actris/examples/sort_br_del.v
diff --git a/theories/examples/sort_fg.v b/actris/examples/sort_fg.v
similarity index 100%
rename from theories/examples/sort_fg.v
rename to actris/examples/sort_fg.v
diff --git a/theories/examples/subprotocols.v b/actris/examples/subprotocols.v
similarity index 100%
rename from theories/examples/subprotocols.v
rename to actris/examples/subprotocols.v
diff --git a/theories/examples/swap_mapper.v b/actris/examples/swap_mapper.v
similarity index 100%
rename from theories/examples/swap_mapper.v
rename to actris/examples/swap_mapper.v
diff --git a/theories/logrel/contexts.v b/actris/logrel/contexts.v
similarity index 100%
rename from theories/logrel/contexts.v
rename to actris/logrel/contexts.v
diff --git a/theories/logrel/examples/choice_subtyping.v b/actris/logrel/examples/choice_subtyping.v
similarity index 100%
rename from theories/logrel/examples/choice_subtyping.v
rename to actris/logrel/examples/choice_subtyping.v
diff --git a/theories/logrel/examples/compute_client_list.v b/actris/logrel/examples/compute_client_list.v
similarity index 100%
rename from theories/logrel/examples/compute_client_list.v
rename to actris/logrel/examples/compute_client_list.v
diff --git a/theories/logrel/examples/compute_service.v b/actris/logrel/examples/compute_service.v
similarity index 100%
rename from theories/logrel/examples/compute_service.v
rename to actris/logrel/examples/compute_service.v
diff --git a/theories/logrel/examples/mapper.v b/actris/logrel/examples/mapper.v
similarity index 100%
rename from theories/logrel/examples/mapper.v
rename to actris/logrel/examples/mapper.v
diff --git a/theories/logrel/examples/mapper_list.v b/actris/logrel/examples/mapper_list.v
similarity index 100%
rename from theories/logrel/examples/mapper_list.v
rename to actris/logrel/examples/mapper_list.v
diff --git a/theories/logrel/examples/pair.v b/actris/logrel/examples/pair.v
similarity index 100%
rename from theories/logrel/examples/pair.v
rename to actris/logrel/examples/pair.v
diff --git a/theories/logrel/examples/par_recv.v b/actris/logrel/examples/par_recv.v
similarity index 100%
rename from theories/logrel/examples/par_recv.v
rename to actris/logrel/examples/par_recv.v
diff --git a/theories/logrel/examples/rec_subtyping.v b/actris/logrel/examples/rec_subtyping.v
similarity index 100%
rename from theories/logrel/examples/rec_subtyping.v
rename to actris/logrel/examples/rec_subtyping.v
diff --git a/theories/logrel/lib/list.v b/actris/logrel/lib/list.v
similarity index 100%
rename from theories/logrel/lib/list.v
rename to actris/logrel/lib/list.v
diff --git a/theories/logrel/lib/mutex.v b/actris/logrel/lib/mutex.v
similarity index 100%
rename from theories/logrel/lib/mutex.v
rename to actris/logrel/lib/mutex.v
diff --git a/theories/logrel/lib/par_start.v b/actris/logrel/lib/par_start.v
similarity index 100%
rename from theories/logrel/lib/par_start.v
rename to actris/logrel/lib/par_start.v
diff --git a/theories/logrel/model.v b/actris/logrel/model.v
similarity index 100%
rename from theories/logrel/model.v
rename to actris/logrel/model.v
diff --git a/theories/logrel/napp.v b/actris/logrel/napp.v
similarity index 100%
rename from theories/logrel/napp.v
rename to actris/logrel/napp.v
diff --git a/theories/logrel/operators.v b/actris/logrel/operators.v
similarity index 100%
rename from theories/logrel/operators.v
rename to actris/logrel/operators.v
diff --git a/theories/logrel/session_types.v b/actris/logrel/session_types.v
similarity index 100%
rename from theories/logrel/session_types.v
rename to actris/logrel/session_types.v
diff --git a/theories/logrel/session_typing_rules.v b/actris/logrel/session_typing_rules.v
similarity index 100%
rename from theories/logrel/session_typing_rules.v
rename to actris/logrel/session_typing_rules.v
diff --git a/theories/logrel/subtyping.v b/actris/logrel/subtyping.v
similarity index 100%
rename from theories/logrel/subtyping.v
rename to actris/logrel/subtyping.v
diff --git a/theories/logrel/subtyping_rules.v b/actris/logrel/subtyping_rules.v
similarity index 100%
rename from theories/logrel/subtyping_rules.v
rename to actris/logrel/subtyping_rules.v
diff --git a/theories/logrel/telescopes.v b/actris/logrel/telescopes.v
similarity index 100%
rename from theories/logrel/telescopes.v
rename to actris/logrel/telescopes.v
diff --git a/theories/logrel/term_types.v b/actris/logrel/term_types.v
similarity index 100%
rename from theories/logrel/term_types.v
rename to actris/logrel/term_types.v
diff --git a/theories/logrel/term_typing_judgment.v b/actris/logrel/term_typing_judgment.v
similarity index 100%
rename from theories/logrel/term_typing_judgment.v
rename to actris/logrel/term_typing_judgment.v
diff --git a/theories/logrel/term_typing_rules.v b/actris/logrel/term_typing_rules.v
similarity index 100%
rename from theories/logrel/term_typing_rules.v
rename to actris/logrel/term_typing_rules.v
diff --git a/theories/utils/cofe_solver_2.v b/actris/utils/cofe_solver_2.v
similarity index 100%
rename from theories/utils/cofe_solver_2.v
rename to actris/utils/cofe_solver_2.v
diff --git a/theories/utils/compare.v b/actris/utils/compare.v
similarity index 100%
rename from theories/utils/compare.v
rename to actris/utils/compare.v
diff --git a/theories/utils/contribution.v b/actris/utils/contribution.v
similarity index 100%
rename from theories/utils/contribution.v
rename to actris/utils/contribution.v
diff --git a/theories/utils/group.v b/actris/utils/group.v
similarity index 100%
rename from theories/utils/group.v
rename to actris/utils/group.v
diff --git a/theories/utils/llist.v b/actris/utils/llist.v
similarity index 100%
rename from theories/utils/llist.v
rename to actris/utils/llist.v
diff --git a/theories/utils/switch.v b/actris/utils/switch.v
similarity index 100%
rename from theories/utils/switch.v
rename to actris/utils/switch.v
diff --git a/coq-actris.opam b/coq-actris.opam
index 0f0153afb1d1c9ef7fc76cdd2870f19ced3da274..c94b261865047855963029dcb7945d0c1f5f420e 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -11,5 +11,5 @@ depends: [
"coq-iris-heap-lang" { (= "dev.2024-10-30.0.27f837c1") | (= "dev") }
]
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "actris" "-j%{jobs}%"]
+install: ["./make-package" "actris" "install"]
diff --git a/make-package b/make-package
new file mode 100755
index 0000000000000000000000000000000000000000..5bf541bca26c231313c0343bccda663d665c11e9
--- /dev/null
+++ b/make-package
@@ -0,0 +1,32 @@
+#!/bin/bash
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
+ echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+ exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+make -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*
diff --git a/multris/channel/channel.v b/multris/channel/channel.v
new file mode 100644
index 0000000000000000000000000000000000000000..46083fd3404a9e94628bdfc0f46728904be3c34f
--- /dev/null
+++ b/multris/channel/channel.v
@@ -0,0 +1,370 @@
+(** This file contains the definition of the channels,
+and their primitive proof rules. Moreover:
+
+- It defines the connective [c ↣ prot] for ownership of channel endpoints,
+ which describes that channel endpoint [c] adheres to protocol [prot].
+- It proves Actris's specifications of [send] and [recv] w.r.t.
+ multiparty dependent separation protocols.
+
+In this file we define the three message-passing connectives:
+
+- [new_chan] creates an n*n matrix of references where [i,j] is the singleton
+ buffer from participant i to participant j
+- [send] takes an endpoint, a participant id, and a value, and puts the value in
+ the reference corresponding to the participant id, and waits until recv takes
+ it out.
+- [recv] takes an endpoint, and a participant id, and waits until a value is put
+ into the corresponding reference.
+
+It is additionaly shown that the channel ownership [c ↣ prot] is closed under
+the subprotocol relation [⊑] *)
+From iris.algebra Require Import gmap excl_auth gmap_view.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Export primitive_laws notation proofmode.
+From multris.utils Require Import matrix.
+From multris.channel Require Import proto_model.
+From multris.channel Require Export proto.
+Set Default Proof Using "Type".
+
+(** * The definition of the message-passing connectives *)
+Definition new_chan : val :=
+ λ: "n", new_matrix "n" "n" NONEV.
+
+Definition get_chan : val :=
+ λ: "cs" "i", ("cs","i").
+
+Definition wait : val :=
+ rec: "go" "c" :=
+ match: !"c" with
+ NONE => #()
+ | SOME <> => "go" "c"
+ end.
+
+Definition send : val :=
+ λ: "c" "j" "v",
+ let: "m" := Fst "c" in
+ let: "i" := Snd "c" in
+ let: "l" := matrix_get "m" "i" "j" in
+ "l" <- SOME "v";; wait "l".
+
+Definition recv : val :=
+ rec: "go" "c" "j" :=
+ let: "m" := Fst "c" in
+ let: "i" := Snd "c" in
+ let: "l" := matrix_get "m" "j" "i" in
+ let: "v" := Xchg "l" NONEV in
+ match: "v" with
+ NONE => "go" "c" "j"
+ | SOME "v" => "v"
+ end.
+
+(** * Setup of Iris's cameras *)
+Class proto_exclG Σ V :=
+ protoG_exclG ::
+ inG Σ (excl_authR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))).
+
+Definition proto_exclΣ V := #[
+ GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
+].
+
+Class chanG Σ := {
+ chanG_proto_exclG :: proto_exclG Σ val;
+ chanG_tokG :: inG Σ (exclR unitO);
+ chanG_protoG :: protoG Σ val;
+}.
+Definition chanΣ : gFunctors := #[ proto_exclΣ val; protoΣ val; GFunctor (exclR unitO) ].
+Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
+Proof. solve_inG. Qed.
+
+(** * Definition of the pointsto connective *)
+Notation iProto Σ := (iProto Σ val).
+Notation iMsg Σ := (iMsg Σ val).
+
+Definition tok `{!chanG Σ} (γ : gname) : iProp Σ := own γ (Excl ()).
+
+Definition chan_inv `{!heapGS Σ, !chanG Σ} γ γE γt i j (l:loc) : iProp Σ :=
+ (l ↦ NONEV ∗ tok γt)%I ∨
+ (∃ v p, l ↦ SOMEV v ∗
+ iProto_own γ i (<(Send, j)> MSG v ; p)%proto ∗ own γE (â—E (Next p))) ∨
+ (∃ p, l ↦ NONEV ∗
+ iProto_own γ i p ∗ own γE (â—E (Next p))).
+
+Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
+ (c : val) (p : iProto Σ) : iProp Σ :=
+ ∃ γ (γEs : list gname) (m:val) (i:nat) (n:nat) p',
+ ⌜ c = (m,#i)%V ⌠∗
+ inv (nroot.@"ctx") (iProto_ctx γ n) ∗
+ is_matrix m n n
+ (λ i j l, ∃ γt, inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j l)) ∗
+ ▷ (p' ⊑ p) ∗
+ own (γEs !!! i) (â—E (Next p')) ∗ own (γEs !!! i) (â—¯E (Next p')) ∗
+ iProto_own γ i p'.
+Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
+Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
+Definition iProto_pointsto_eq :
+ @iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
+Arguments iProto_pointsto {_ _ _} _ _%_proto.
+Global Instance: Params (@iProto_pointsto) 5 := {}.
+Notation "c ↣ p" := (iProto_pointsto c p)
+ (at level 20, format "c ↣ p").
+
+Definition chan_pool `{!heapGS Σ, !chanG Σ}
+ (m : val) (i':nat) (ps : list (iProto Σ)) : iProp Σ :=
+ ∃ γ (γEs : list gname) (n:nat),
+ ⌜(i' + length ps = n)%nat⌠∗
+ inv (nroot.@"ctx") (iProto_ctx γ n) ∗
+ is_matrix m n n (λ i j l,
+ ∃ γt, inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j l)) ∗
+ [∗ list] i ↦ p ∈ ps,
+ (own (γEs !!! (i+i')) (â—E (Next p)) ∗
+ own (γEs !!! (i+i')) (◯E (Next p)) ∗
+ iProto_own γ (i+i') p).
+
+Section channel.
+ Context `{!heapGS Σ, !chanG Σ}.
+ Implicit Types p : iProto Σ.
+ Implicit Types TT : tele.
+
+ Global Instance iProto_pointsto_ne c : NonExpansive (iProto_pointsto c).
+ Proof. rewrite iProto_pointsto_eq. solve_proper. Qed.
+ Global Instance iProto_pointsto_proper c : Proper ((≡) ==> (≡)) (iProto_pointsto c).
+ Proof. apply (ne_proper _). Qed.
+
+ Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
+ Proof.
+ rewrite iProto_pointsto_eq.
+ iDestruct 1 as (?????? ->) "(#IH & Hls & Hle & Hâ— & Hâ—¯ & Hown)".
+ iIntros "Hle'". iExists _,_,_,_,_,p'.
+ iSplit; [done|]. iFrame "#∗".
+ iApply (iProto_le_trans with "Hle Hle'").
+ Qed.
+
+ (** ** Specifications of [send] and [recv] *)
+ Lemma new_chan_spec (ps:list (iProto Σ)) :
+ 0 < length ps →
+ {{{ iProto_consistent ps }}}
+ new_chan #(length ps)
+ {{{ cs, RET cs; chan_pool cs 0 ps }}}.
+ Proof.
+ iIntros (Hle Φ) "Hps HΦ". wp_lam.
+ iMod (iProto_init with "Hps") as (γ) "[Hps Hps']".
+ iAssert (|==> ∃ (γEs : list gname),
+ ⌜length γEs = length ps⌠∗
+ [∗ list] i ↦ p ∈ ps,
+ own (γEs !!! i) (â—E (Next (ps !!! i))) ∗
+ own (γEs !!! i) (◯E (Next (ps !!! i))) ∗
+ iProto_own γ i (ps !!! i))%I with "[Hps']" as "H".
+ { clear Hle.
+ iInduction ps as [|p ps] "IHn" using rev_ind.
+ { iExists []. iModIntro. simpl. done. }
+ iDestruct "Hps'" as "[Hps' Hp]".
+ iMod (own_alloc (â—E (Next p) â‹… â—¯E (Next p))) as (γE) "[Hauth Hfrag]".
+ { apply excl_auth_valid. }
+ iMod ("IHn" with "Hps'") as (γEs Hlen) "H".
+ iModIntro. iExists (γEs++[γE]).
+ rewrite !length_app Hlen.
+ iSplit; [iPureIntro=>/=;lia|]=> /=.
+ iSplitL "H".
+ { iApply (big_sepL_impl with "H").
+ iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
+ assert (i < length ps) as Hle.
+ { by apply lookup_lt_is_Some_1. }
+ rewrite !lookup_total_app_l; [|lia..]. iFrame. }
+ rewrite Nat.add_0_r.
+ simpl. rewrite right_id_L.
+ rewrite !lookup_total_app_r; [|lia..]. rewrite !Hlen.
+ rewrite Nat.sub_diag. simpl. iFrame.
+ iDestruct "Hp" as "[$ _]". }
+ iMod "H" as (γEs Hlen) "H".
+ iMod (inv_alloc with "Hps") as "#IHp".
+ wp_smart_apply (new_matrix_spec _ _ _ _
+ (λ i j l, ∃ γt,
+ inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j
+ l))%I); [done..| |].
+ { iApply (big_sepL_intro). iIntros "!>" (k tt Hin). iApply (big_sepL_intro).
+ iIntros "!>" (k' tt' Hin'). iIntros (l) "Hl".
+ iMod (own_alloc (Excl ())) as (γ') "Hγ'"; [done|].
+ iExists γ'. iApply inv_alloc. iNext. iLeft. iFrame. }
+ iIntros (mat) "Hmat". iApply "HΦ".
+ iExists _, _, _. iFrame "#∗".
+ rewrite left_id. iSplit; [done|].
+ iApply (big_sepL_impl with "H").
+ iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)". iFrame.
+ rewrite (list_lookup_total_alt ps).
+ simpl. rewrite right_id_L. rewrite HSome'. iFrame.
+ Qed.
+
+ Lemma get_chan_spec cs i ps p :
+ {{{ chan_pool cs i (p::ps) }}}
+ get_chan cs #i
+ {{{ c, RET c; c ↣ p ∗ chan_pool cs (i+1) ps }}}.
+ Proof.
+ iIntros (Φ) "Hcs HΦ".
+ iDestruct "Hcs" as (γp γEs n <-) "(#IHp & #Hm & Hl)".
+ wp_lam. wp_pures.
+ iDestruct "Hl" as "[Hl Hls]".
+ iModIntro.
+ iApply "HΦ".
+ iSplitL "Hl".
+ { rewrite iProto_pointsto_eq. iExists _, _, _, _, _, _.
+ iSplit; [done|].
+ iFrame. iFrame "#∗". iNext. done. }
+ iExists γp, γEs, _. iSplit; [done|].
+ iFrame. iFrame "#∗".
+ simpl.
+ replace (i + 1 + length ps) with (i + (S $ length ps))%nat by lia.
+ iFrame "#".
+ iApply (big_sepL_impl with "Hls").
+ iIntros "!>" (k x HSome) "(H1 & H2 & H3)".
+ replace (S (k + i)) with (k + (i + 1)) by lia.
+ iFrame.
+ Qed.
+
+ Lemma send_spec c j v p :
+ {{{ c ↣ <(Send, j)> MSG v; p }}}
+ send c #j v
+ {{{ RET #(); c ↣ p }}}.
+ Proof.
+ rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+ iDestruct "Hc" as
+ (γ γE l i n p' ->) "(#IH & #Hls & Hle & H◠& H◯ & Hown)".
+ wp_bind (Fst _).
+ iInv "IH" as "Hctx".
+ iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
+ iRewrite "Heq" in "Hown".
+ iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
+ iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
+ iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
+ wp_pures.
+ iDestruct "Hi" as %Hi.
+ iDestruct "Hj" as %Hj.
+ wp_smart_apply (matrix_get_spec with "Hls"); [done..|].
+ iIntros (l') "[Hl' _]".
+ iDestruct "Hl'" as (γt) "#IHl1".
+ wp_pures. wp_bind (Store _ _).
+ iInv "IHl1" as "HIp".
+ iDestruct "HIp" as "[HIp|HIp]"; last first.
+ { iDestruct "HIp" as "[HIp|HIp]".
+ - iDestruct "HIp" as (? p'') "(>Hl & Hown' & HIp)".
+ wp_store.
+ iDestruct (iProto_own_excl with "Hown Hown'") as %[].
+ - iDestruct "HIp" as (p'') "(>Hl' & Hown' & HIp)".
+ wp_store.
+ iDestruct (iProto_own_excl with "Hown Hown'") as %[]. }
+ iDestruct "HIp" as "[>Hl' Htok]".
+ wp_store.
+ iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]"; [by apply excl_auth_update|].
+ iModIntro.
+ iSplitL "Hl' Hâ— Hown Hle".
+ { iRight. iLeft. iIntros "!>". iExists _, _. iFrame.
+ iDestruct (iProto_own_le with "Hown Hle") as "Hown".
+ by rewrite iMsg_base_eq. }
+ wp_pures.
+ iLöb as "HL".
+ wp_lam.
+ wp_bind (Load _).
+ iInv "IHl1" as "HIp".
+ iDestruct "HIp" as "[HIp|HIp]".
+ { iDestruct "HIp" as ">[Hl' Htok']".
+ iDestruct (own_valid_2 with "Htok Htok'") as %[]. }
+ iDestruct "HIp" as "[HIp|HIp]".
+ - iDestruct "HIp" as (? p'') "(>Hl' & Hown & HIp)".
+ wp_load. iModIntro.
+ iSplitL "Hl' Hown HIp".
+ { iRight. iLeft. iExists _,_. iFrame. }
+ wp_pures. iApply ("HL" with "HΦ Htok H◯").
+ - iDestruct "HIp" as (p'') "(>Hl' & Hown & Hâ—)".
+ wp_load.
+ iModIntro.
+ iSplitL "Hl' Htok".
+ { iLeft. iFrame. }
+ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as "#Hagree".
+ iDestruct (excl_auth_agreeI with "Hagree") as "Hagree'".
+ wp_pures.
+ iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]".
+ { apply excl_auth_update. }
+ iModIntro.
+ iApply "HΦ".
+ iExists _, _, _, _, _, _.
+ iSplit; [done|]. iFrame "#∗".
+ iRewrite -"Hagree'". iApply iProto_le_refl.
+ Qed.
+
+ Lemma send_spec_tele {TT} c i (tt : TT)
+ (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+ {{{ c ↣ (<(Send,i) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+ send c #i (v tt)
+ {{{ RET #(); c ↣ (p tt) }}}.
+ Proof.
+ iIntros (Φ) "[Hc HP] HΦ".
+ iDestruct (iProto_pointsto_le _ _ (<(Send,i)> MSG v tt; p tt)%proto
+ with "Hc [HP]") as "Hc".
+ { iIntros "!>". iApply iProto_le_trans. iApply iProto_le_texist_intro_l.
+ by iApply iProto_le_payload_intro_l. }
+ by iApply (send_spec with "Hc").
+ Qed.
+
+ Lemma recv_spec {TT} c j (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+ {{{ c ↣ <(Recv, j) @.. x> MSG v x {{ ▷ P x }}; p x }}}
+ recv c #j
+ {{{ x, RET v x; c ↣ p x ∗ P x }}}.
+ Proof.
+ iIntros (Φ) "Hc HΦ". iLöb as "HL". wp_lam.
+ rewrite iProto_pointsto_eq.
+ iDestruct "Hc" as
+ (γ γE l i n p' ->) "(#IH & #Hls & Hle & H◠& H◯ & Hown)".
+ do 5 wp_pure _.
+ wp_bind (Snd _).
+ iInv "IH" as "Hctx".
+ iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
+ iRewrite "Heq" in "Hown".
+ iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
+ iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
+ iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
+ wp_pure _.
+ iDestruct "Hi" as %Hi.
+ iDestruct "Hj" as %Hj.
+ wp_smart_apply (matrix_get_spec with "Hls"); [done..|].
+ iIntros (l') "[Hl' _]".
+ iDestruct "Hl'" as (γt) "#IHl2".
+ wp_pures.
+ wp_bind (Xchg _ _).
+ iInv "IHl2" as "HIp".
+ iDestruct "HIp" as "[HIp|HIp]".
+ { iDestruct "HIp" as ">[Hl' Htok]".
+ wp_xchg. iModIntro.
+ iSplitL "Hl' Htok".
+ { iLeft. iFrame. }
+ wp_pures. iApply ("HL" with "[H◠H◯ Hown Hle] HΦ").
+ iExists _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+ iDestruct "HIp" as "[HIp|HIp]"; last first.
+ { iDestruct "HIp" as (p'') "[>Hl' [Hown' Hâ—¯']]".
+ wp_xchg.
+ iModIntro.
+ iSplitL "Hl' Hown' Hâ—¯'".
+ { iRight. iRight. iExists _. iFrame. }
+ wp_pures. iApply ("HL" with "[H◠H◯ Hown Hle] HΦ").
+ iExists _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+ iDestruct "HIp" as (w p'') "(>Hl' & Hown' & Hp')".
+ iInv "IH" as "Hctx".
+ wp_xchg.
+ iDestruct (iProto_own_le with "Hown Hle") as "Hown".
+ iMod (iProto_step with "Hctx Hown' Hown []") as
+ (p''') "(Hm & Hctx & Hown & Hown')".
+ { by rewrite iMsg_base_eq. }
+ iModIntro.
+ iSplitL "Hctx"; [done|].
+ iModIntro.
+ iSplitL "Hl' Hown Hp'".
+ { iRight. iRight. iExists _. iFrame. }
+ wp_pure _.
+ rewrite iMsg_base_eq.
+ iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
+ wp_pures.
+ iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]";
+ [apply (excl_auth_update _ _ (Next p'''))|].
+ iModIntro. iApply "HΦ". rewrite /iProto_pointsto_def. iFrame "IH Hls ∗".
+ iSplit; [done|]. iRewrite "Hp". iApply iProto_le_refl.
+ Qed.
+
+End channel.
diff --git a/multris/channel/proofmode.v b/multris/channel/proofmode.v
new file mode 100644
index 0000000000000000000000000000000000000000..d3da00dfa7c332861580263f6c83a75ed8b1e16f
--- /dev/null
+++ b/multris/channel/proofmode.v
@@ -0,0 +1,405 @@
+(** This file contains the definitions of Actris's tactics for symbolic
+execution of message-passing programs. The API of these tactics is documented
+in the [README.md] file. The implementation follows the same pattern for the
+implementation of these tactics that is used in Iris. In addition, it uses a
+standard pattern using type classes to perform the normalization.
+
+In addition to the tactics for symbolic execution, this file defines the tactic
+[solve_proto_contractive], which can be used to automatically prove that
+recursive protocols are contractive. *)
+From iris.algebra Require Import gmap.
+From iris.proofmode Require Import coq_tactics reduction spec_patterns.
+From iris.heap_lang Require Export proofmode notation.
+From multris.channel Require Import proto_model.
+From multris.channel Require Export channel.
+Set Default Proof Using "Type".
+
+(** * Tactics for proving contractiveness of protocols *)
+Ltac f_dist_le :=
+ match goal with
+ | H : _ ≡{?n}≡ _ |- _ ≡{?n'}≡ _ => apply (dist_le n); [apply H|lia]
+ end.
+
+Ltac solve_proto_contractive :=
+ solve_proper_core ltac:(fun _ =>
+ first [f_contractive; simpl in * | f_equiv | f_dist_le]).
+
+(** * Normalization of protocols *)
+Class ActionDualIf (d : bool) (a1 a2 : action) :=
+ dual_action_if : a2 = if d then action_dual a1 else a1.
+Global Hint Mode ActionDualIf ! ! - : typeclass_instances.
+
+Global Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
+Global Instance action_dual_if_true_send i : ActionDualIf true (Send,i) (Recv,i) := eq_refl.
+Global Instance action_dual_if_true_recv i : ActionDualIf true (Recv,i) (Send,i) := eq_refl.
+
+Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
+ (pas : list (bool * iProto Σ)) (q : iProto Σ) :=
+ proto_normalize :
+ ⊢ iProto_dual_if d p <++>
+ foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
+Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
+Arguments ProtoNormalize {_} _ _%_proto _%_proto _%_proto.
+
+Notation ProtoUnfold p1 p2 := (∀ d pas q,
+ ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
+
+Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
+ (pas : list (bool * iProto Σ)) (m2 : iMsg Σ) :=
+ msg_normalize a :
+ ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
+Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
+Arguments MsgNormalize {_} _ _%_msg _%_msg _%_msg.
+
+Section classes.
+ Context `{!chanG Σ, !heapGS Σ}.
+ Implicit Types TT : tele.
+ Implicit Types p : iProto Σ.
+ Implicit Types m : iMsg Σ.
+ Implicit Types P : iProp Σ.
+
+ Lemma proto_unfold_eq p1 p2 : p1 ≡ p2 → ProtoUnfold p1 p2.
+ Proof. rewrite /ProtoNormalize=> Hp d pas q. by rewrite Hp. Qed.
+
+ Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0.
+ Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
+ Global Instance proto_normalize_done_dual p :
+ ProtoNormalize true p [] (iProto_dual p) | 0.
+ Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
+ Global Instance proto_normalize_done_dual_end :
+ ProtoNormalize (Σ:=Σ) true END [] END | 0.
+ Proof. rewrite /ProtoNormalize /= right_id iProto_dual_end. auto. Qed.
+
+ Global Instance proto_normalize_dual d p pas q :
+ ProtoNormalize (negb d) p pas q →
+ ProtoNormalize d (iProto_dual p) pas q.
+ Proof. rewrite /ProtoNormalize. by destruct d; rewrite /= ?involutive. Qed.
+
+ Global Instance proto_normalize_app_l d p1 p2 pas q :
+ ProtoNormalize d p1 ((d,p2) :: pas) q →
+ ProtoNormalize d (p1 <++> p2) pas q.
+ Proof.
+ rewrite /ProtoNormalize /=. rewrite assoc.
+ by destruct d; by rewrite /= ?iProto_dual_app.
+ Qed.
+
+ Global Instance proto_normalize_end d d' p pas q :
+ ProtoNormalize d p pas q →
+ ProtoNormalize d' END ((d,p) :: pas) q | 0.
+ Proof.
+ rewrite /ProtoNormalize /=.
+ destruct d'; by rewrite /= ?iProto_dual_end left_id.
+ Qed.
+
+ Global Instance proto_normalize_app_r d p1 p2 pas q :
+ ProtoNormalize d p2 pas q →
+ ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 0.
+ Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
+
+ Global Instance proto_normalize_app_r_dual d p1 p2 pas q :
+ ProtoNormalize d p2 pas q →
+ ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 0.
+ Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
+
+ Global Instance msg_normalize_base d v P p q pas :
+ ProtoNormalize d p pas q →
+ MsgNormalize d (MSG v {{ P }}; p) pas (MSG v {{ P }}; q).
+ Proof.
+ rewrite /MsgNormalize /ProtoNormalize=> H a.
+ iApply iProto_le_trans; [|by iApply iProto_le_base].
+ destruct d; by rewrite /= ?iProto_dual_message ?iMsg_dual_base
+ iProto_app_message iMsg_app_base.
+ Qed.
+
+ Global Instance msg_normalize_exist {A} d (m1 m2 : A → iMsg Σ) pas :
+ (∀ x, MsgNormalize d (m1 x) pas (m2 x)) →
+ MsgNormalize d (∃ x, m1 x) pas (∃ x, m2 x).
+ Proof.
+ rewrite /MsgNormalize /ProtoNormalize=> H a.
+ destruct d, a as [[|]];
+ simpl in *; rewrite ?iProto_dual_message ?iMsg_dual_exist
+ ?iProto_app_message ?iMsg_app_exist /=; iIntros (x); iExists x; first
+ [move: (H x (Send,n)); by rewrite ?iProto_dual_message ?iProto_app_message
+ |move: (H x (Recv,n)); by rewrite ?iProto_dual_message ?iProto_app_message].
+ Qed.
+
+ Global Instance proto_normalize_message d a1 a2 m1 m2 pas :
+ ActionDualIf d a1 a2 →
+ MsgNormalize d m1 pas m2 →
+ ProtoNormalize d (<a1> m1) pas (<a2> m2).
+ Proof. by rewrite /ActionDualIf /MsgNormalize /ProtoNormalize=> ->. Qed.
+
+ (** Automatically perform normalization of protocols in the proof mode when
+ using [iAssumption] and [iFrame]. *)
+ Global Instance pointsto_proto_from_assumption q c p1 p2 :
+ ProtoNormalize false p1 [] p2 →
+ FromAssumption q (c ↣ p1) (c ↣ p2).
+ Proof.
+ rewrite /FromAssumption /ProtoNormalize /= right_id.
+ rewrite bi.intuitionistically_if_elim.
+ iIntros (?) "H". by iApply (iProto_pointsto_le with "H").
+ Qed.
+ Global Instance pointsto_proto_from_frame q c p1 p2 :
+ ProtoNormalize false p1 [] p2 →
+ Frame q (c ↣ p1) (c ↣ p2) True.
+ Proof.
+ rewrite /Frame /ProtoNormalize /= right_id.
+ rewrite bi.intuitionistically_if_elim.
+ iIntros (?) "[H _]". by iApply (iProto_pointsto_le with "H").
+ Qed.
+End classes.
+
+(** * Symbolic execution tactics *)
+(* TODO: Maybe strip laters from other hypotheses in the future? *)
+Lemma tac_wp_recv `{!chanG Σ, !heapGS Σ} {TT : tele} Δ i j K v (n:nat) c p m tv tP tP' tp Φ :
+ v = #n →
+ envs_lookup i Δ = Some (false, c ↣ p)%I →
+ ProtoNormalize false p [] (<(Recv,n)> m) →
+ MsgTele m tv tP tp →
+ (∀.. x, MaybeIntoLaterN false 1 (tele_app tP x) (tele_app tP' x)) →
+ let Δ' := envs_delete false i false Δ in
+ (∀.. x : TT,
+ match envs_app false
+ (Esnoc (Esnoc Enil j (tele_app tP' x)) i (c ↣ tele_app tp x)) Δ' with
+ | Some Δ'' => envs_entails Δ'' (WP fill K (of_val (tele_app tv x)) {{ Φ }})
+ | None => False
+ end) →
+ envs_entails Δ (WP fill K (recv c v) {{ Φ }}).
+Proof.
+ intros ->.
+ rewrite envs_entails_unseal /ProtoNormalize /MsgTele /MaybeIntoLaterN /=.
+ rewrite !tforall_forall right_id.
+ intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl.
+ assert (c ↣ p ⊢ c ↣ <(Recv,n) @.. x>
+ MSG tele_app tv x {{ â–· tele_app tP' x }}; tele_app tp x) as ->.
+ { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"). iIntros "!>".
+ iApply iProto_le_trans; [iApply Hp|rewrite Hm].
+ iApply iProto_le_texist_elim_l; iIntros (x).
+ iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ _ x)]; simpl.
+ iIntros "H". by iDestruct (HP with "H") as "$". }
+ rewrite -wp_bind. eapply bi.wand_apply;
+ [by eapply bi.wand_entails, (recv_spec _ n (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
+ rewrite -bi.later_intro; apply bi.forall_intro=> x.
+ specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
+ rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
+Qed.
+
+Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
+ let solve_pointsto _ :=
+ let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
+ iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
+ wp_pures;
+ let Hnew := iFresh in
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
+ |fail 1 "wp_recv: cannot find 'recv' in" e];
+ [|solve_pointsto ()
+ |tc_solve || fail 1 "wp_recv: protocol not of the shape <?>"
+ |tc_solve || fail 1 "wp_recv: cannot convert to telescope"
+ |tc_solve
+ |pm_reduce; simpl; tac_intros;
+ tac Hnew;
+ wp_finish];[try done|]
+ | _ => fail "wp_recv: not a 'wp'"
+ end.
+
+
+Tactic Notation "wp_recv" "as" constr(pat) :=
+ wp_recv_core (idtac) as (fun H => iDestructHyp H as pat).
+Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" constr(pat) :=
+ wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
+Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as"
+ "(" ne_simple_intropattern_list(ys) ")" constr(pat) :=
+ wp_recv_core (intros xs) as (fun H => _iDestructHyp H ys pat).
+
+Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K (n:nat) w c v p m tv tP tp Φ :
+ w = #n →
+ envs_lookup i Δ = Some (false, c ↣ p)%I →
+ ProtoNormalize false p [] (<(Send,n)> m) →
+ MsgTele m tv tP tp →
+ let Δ' := envs_delete false i false Δ in
+ (∃.. x : TT,
+ match envs_split (if neg is true then base.Right else base.Left) js Δ' with
+ | Some (Δ1,Δ2) =>
+ match envs_app false (Esnoc Enil i (c ↣ tele_app tp x)) Δ2 with
+ | Some Δ2' =>
+ v = tele_app tv x ∧
+ envs_entails Δ1 (tele_app tP x) ∧
+ envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
+ | None => False
+ end
+ | None => False
+ end) →
+ envs_entails Δ (WP fill K (send c w v) {{ Φ }}).
+Proof.
+ intros ->.
+ rewrite envs_entails_unseal /ProtoNormalize /MsgTele /= right_id texist_exist.
+ intros ? Hp Hm [x HΦ]. rewrite envs_lookup_sound //; simpl.
+ destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
+ destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
+ rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
+ destruct HΦ as (-> & -> & ->). rewrite right_id assoc.
+ assert (c ↣ p ⊢
+ c ↣ <(Send,n) @.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->.
+ { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"); iIntros "!>".
+ iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. }
+ eapply bi.wand_apply; [rewrite -wp_bind; by eapply bi.wand_entails, send_spec_tele|].
+ by rewrite -bi.later_intro.
+Qed.
+
+Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
+ let solve_pointsto _ :=
+ let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
+ iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
+ let solve_done d :=
+ lazymatch d with
+ | true =>
+ done ||
+ let Q := match goal with |- envs_entails _ ?Q => Q end in
+ fail "wp_send: cannot solve" Q "using done"
+ | false => idtac
+ end in
+ lazymatch spec_pat.parse pat with
+ | [SGoal (SpecGoal GSpatial ?neg ?Hs_frame ?Hs ?d)] =>
+ let Hs' := eval cbv in (if neg then Hs else Hs_frame ++ Hs) in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
+ |fail 1 "wp_send: cannot find 'send' in" e];
+ [|solve_pointsto ()
+ |tc_solve || fail 1 "wp_send: protocol not of the shape <!>"
+ |tc_solve || fail 1 "wp_send: cannot convert to telescope"
+ |pm_reduce; simpl; tac_exist;
+ repeat lazymatch goal with
+ | |- ∃ _, _ => eexists _
+ end;
+ lazymatch goal with
+ | |- False => fail "wp_send:" Hs' "not found"
+ | _ => notypeclasses refine (conj (eq_refl _) (conj _ _));
+ [iFrame Hs_frame; solve_done d
+ |wp_finish]
+ end]; [try done|..]
+ | _ => fail "wp_send: not a 'wp'"
+ end
+ | _ => fail "wp_send: only a single goal spec pattern supported"
+ end.
+
+Tactic Notation "wp_send" "with" constr(pat) :=
+ wp_send_core (idtac) with pat.
+Tactic Notation "wp_send" "(" ne_uconstr_list(xs) ")" "with" constr(pat) :=
+ wp_send_core (ltac1_list_iter ltac:(fun x => eexists x) xs) with pat.
+
+Lemma iProto_consistent_equiv_proof {Σ} (ps : list (iProto Σ)) :
+ (∀ i j, valid_target ps i j) ∗
+ (∀ i j m1 m2,
+ (ps !!! i ≡ (<(Send, j)> m1)%proto) -∗
+ (ps !!! j ≡ (<(Recv, i)> m2)%proto) -∗
+ ∃ m1' m2' (TT1:tele) (TT2:tele) tv1 tP1 tp1 tv2 tP2 tp2,
+ (<(Send, j)> m1')%proto ≡ (<(Send, j)> m1)%proto ∗
+ (<(Recv, i)> m2')%proto ≡ (<(Recv, i)> m2)%proto ∗
+ ⌜MsgTele (TT:=TT1) m1' tv1 tP1 tp1⌠∗
+ ⌜MsgTele (TT:=TT2) m2' tv2 tP2 tp2⌠∗
+ ∀.. (x : TT1), tele_app tP1 x -∗
+ ∃.. (y : TT2), ⌜tele_app tv1 x = tele_app tv2 y⌠∗
+ tele_app tP2 y ∗
+ â–· (iProto_consistent
+ (<[i:=tele_app tp1 x]>(<[j:=tele_app tp2 y]>ps)))) -∗
+ iProto_consistent ps.
+Proof.
+ iIntros "[H' H]".
+ rewrite iProto_consistent_unfold.
+ iFrame.
+ iIntros (i j m1 m2) "Hm1 Hm2".
+ iDestruct ("H" with "Hm1 Hm2")
+ as (m1' m2' TT1 TT2 tv1 tP1 tp1 tv2 tP2 tp2)
+ "(Heq1 & Heq2& %Hm1' & %Hm2' & H)".
+ rewrite !iProto_message_equivI.
+ iDestruct "Heq1" as "[_ Heq1]".
+ iDestruct "Heq2" as "[_ Heq2]".
+ iIntros (v p1) "Hm1".
+ iSpecialize ("Heq1" $! v (Next p1)).
+ iRewrite -"Heq1" in "Hm1".
+ rewrite Hm1'.
+ rewrite iMsg_base_eq. rewrite iMsg_texist_exist.
+ iDestruct "Hm1" as (x Htv1) "[Hp1 HP1]".
+ iDestruct ("H" with "HP1") as (y Htv2) "[HP2 H]".
+ iExists (tele_app tp2 y).
+ iSpecialize ("Heq2" $! v (Next (tele_app tp2 y))).
+ iRewrite -"Heq2".
+ rewrite Hm2'. rewrite iMsg_base_eq. rewrite iMsg_texist_exist.
+ iSplitL "HP2".
+ { iExists y. iFrame.
+ iSplit; [|done].
+ iPureIntro. subst. done. }
+ iNext. iRewrite -"Hp1". done.
+Qed.
+
+Tactic Notation "iProto_consistent_take_step_step" :=
+ let i := fresh in
+ let j := fresh in
+ let m1 := fresh in
+ let m2 := fresh in
+ iIntros (i j m1 m2) "#Hm1 #Hm2";
+ repeat (destruct i as [|i]=> /=;
+ [try (by rewrite iProto_end_message_equivI);
+ iDestruct (iProto_message_equivI with "Hm1")
+ as "[%Heq1 Hm1']";simplify_eq=> /=|
+ try (by rewrite iProto_end_message_equivI)]);
+ try (by rewrite iProto_end_message_equivI);
+ iDestruct (iProto_message_equivI with "Hm2")
+ as "[%Heq2 Hm2']";simplify_eq=> /=;
+ try (iClear "Hm1' Hm2'";
+ iExists _,_,_,_,_,_,_,_,_,_;
+ iSplitL "Hm1"; [iFrame "#"|];
+ iSplitL "Hm2"; [iFrame "#"|];
+ iSplit; [iPureIntro; tc_solve|];
+ iSplit; [iPureIntro; tc_solve|];
+ simpl; iClear "Hm1 Hm2"; clear m1 m2).
+
+Tactic Notation "iProto_consistent_take_step_target" :=
+ let i := fresh in
+ iIntros (i j a m); rewrite /valid_target;
+ iIntros "#Hm1";
+ repeat (destruct i as [|i]=> /=;
+ [try (by rewrite iProto_end_message_equivI);
+ by iDestruct (iProto_message_equivI with "Hm1")
+ as "[%Heq1 _]" ; simplify_eq=> /=|
+ try (by rewrite iProto_end_message_equivI)]).
+
+Tactic Notation "iProto_consistent_take_step" :=
+ try iNext;
+ iApply iProto_consistent_equiv_proof;
+ iSplitR; [iProto_consistent_take_step_target|
+ iProto_consistent_take_step_step].
+
+Tactic Notation "iProto_consistent_resolve_step" :=
+ repeat iIntros (?); repeat iIntros "?";
+ repeat iExists _; repeat (iSplit; [done|]); try iFrame.
+
+Tactic Notation "iProto_consistent_take_steps" :=
+ repeat (iProto_consistent_take_step; iProto_consistent_resolve_step).
+
+Tactic Notation "wp_get_chan" "(" simple_intropattern(c) ")" constr(pat) :=
+ wp_smart_apply (get_chan_spec with "[$]"); iIntros (c) "[_TMP ?]";
+ iRevert "_TMP"; iIntros pat.
+
+Ltac ltac1_list_iter2 tac l1 l2 :=
+ let go := ltac2:(tac l1 l2 |- List.iter2 (ltac1:(tac x y |- tac x y) tac)
+ (of_ltac1_list l1) (of_ltac1_list l2)) in
+ go 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 (?) "?"];
+ [|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 (?) "?"];
+ ltac1_list_iter2 ltac:(fun x y => wp_get_chan (x) y) xs pats.
diff --git a/multris/channel/proto.v b/multris/channel/proto.v
new file mode 100644
index 0000000000000000000000000000000000000000..56522bb410f4f5ac41da6c02117cdeccd9c6b5f4
--- /dev/null
+++ b/multris/channel/proto.v
@@ -0,0 +1,1377 @@
+(** This file defines the core of the Multiparty Actris logic:
+It defines multiparty dependent separation protocols, and the Multiparty Actris
+ghost theory. *)
+From iris.algebra Require Import gmap excl_auth gmap_view.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic Require Export lib.iprop.
+From iris.base_logic Require Import lib.own.
+From iris.program_logic Require Import language.
+From multris.channel Require Import proto_model.
+Set Default Proof Using "Type".
+Export action.
+
+(** * Setup of Iris's cameras *)
+Class protoG Σ V :=
+ protoG_authG ::
+ inG Σ (gmap_viewR natO
+ (optionUR (exclR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))))).
+
+Definition protoΣ V := #[
+ GFunctor ((gmap_viewRF natO (optionRF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF))))))
+].
+Global Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
+Proof. solve_inG. Qed.
+
+(** * Types *)
+Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
+Declare Scope proto_scope.
+Delimit Scope proto_scope with proto.
+Bind Scope proto_scope with iProto.
+Local Open Scope proto.
+
+(** * Messages *)
+Section iMsg.
+ Set Primitive Projections.
+ Record iMsg Σ V := IMsg { iMsg_car : V → laterO (iProto Σ V) -n> iPropO Σ }.
+End iMsg.
+Arguments IMsg {_ _} _.
+Arguments iMsg_car {_ _} _.
+
+Declare Scope msg_scope.
+Delimit Scope msg_scope with msg.
+Bind Scope msg_scope with iMsg.
+Global Instance iMsg_inhabited {Σ V} : Inhabited (iMsg Σ V) := populate (IMsg inhabitant).
+
+Section imsg_ofe.
+ Context {Σ : gFunctors} {V : Type}.
+
+ Instance iMsg_equiv : Equiv (iMsg Σ V) := λ m1 m2,
+ ∀ w p, iMsg_car m1 w p ≡ iMsg_car m2 w p.
+ Instance iMsg_dist : Dist (iMsg Σ V) := λ n m1 m2,
+ ∀ w p, iMsg_car m1 w p ≡{n}≡ iMsg_car m2 w p.
+
+ Lemma iMsg_ofe_mixin : OfeMixin (iMsg Σ V).
+ Proof. by apply (iso_ofe_mixin (iMsg_car : _ → V -d> _ -n> _)). Qed.
+ Canonical Structure iMsgO := Ofe (iMsg Σ V) iMsg_ofe_mixin.
+
+ Global Instance iMsg_cofe : Cofe iMsgO.
+ Proof. by apply (iso_cofe (IMsg : (V -d> _ -n> _) → _) iMsg_car). Qed.
+End imsg_ofe.
+
+Program Definition iMsg_base_def {Σ V}
+ (v : V) (P : iProp Σ) (p : iProto Σ V) : iMsg Σ V :=
+ IMsg (λ v', λne p', ⌜ v = v' ⌠∗ Next p ≡ p' ∗ P)%I.
+Next Obligation. solve_proper. Qed.
+Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
+Definition iMsg_base := iMsg_base_aux.(unseal).
+Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
+Arguments iMsg_base {_ _} _%_V _%_I _%_proto.
+Global Instance: Params (@iMsg_base) 3 := {}.
+
+Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
+ IMsg (λ v', λne p', ∃ x, iMsg_car (m x) v' p')%I.
+Next Obligation. solve_proper. Qed.
+Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
+Definition iMsg_exist := iMsg_exist_aux.(unseal).
+Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
+Arguments iMsg_exist {_ _ _} _%_msg.
+Global Instance: Params (@iMsg_exist) 3 := {}.
+
+Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
+ tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
+Arguments iMsg_texist {_ _ !_} _%_msg /.
+
+Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
+ (at level 200, v at level 20, right associativity,
+ format "MSG v {{ P } } ; p") : msg_scope.
+Notation "'MSG' v ; p" := (iMsg_base v True p)
+ (at level 200, v at level 20, right associativity,
+ format "MSG v ; p") : msg_scope.
+Notation "∃ x .. y , m" :=
+ (iMsg_exist (λ x, .. (iMsg_exist (λ y, m)) ..)%msg) : msg_scope.
+Notation "'∃..' x .. y , m" :=
+ (iMsg_texist (λ x, .. (iMsg_texist (λ y, m)) .. )%msg)
+ (at level 200, x binder, y binder, right associativity,
+ format "∃.. x .. y , m") : msg_scope.
+
+Lemma iMsg_texist_exist {Σ V} {TT : tele} w lp (m : TT → iMsg Σ V) :
+ iMsg_car (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, iMsg_car (m x) w lp).
+Proof.
+ rewrite /iMsg_texist iMsg_exist_eq.
+ induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH.
+Qed.
+
+(** * Operators *)
+Definition iProto_end_def {Σ V} : iProto Σ V := proto_end.
+Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
+Definition iProto_end := iProto_end_aux.(unseal).
+Definition iProto_end_eq : @iProto_end = @iProto_end_def := iProto_end_aux.(seal_eq).
+Arguments iProto_end {_ _}.
+
+Definition iProto_message_def {Σ V} (a : action) (m : iMsg Σ V) : iProto Σ V :=
+ proto_message a (iMsg_car m).
+Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
+Definition iProto_message := iProto_message_aux.(unseal).
+Definition iProto_message_eq :
+ @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
+Arguments iProto_message {_ _} _ _%_msg.
+Global Instance: Params (@iProto_message) 3 := {}.
+
+Notation "'END'" := iProto_end : proto_scope.
+
+Notation "< a > m" := (iProto_message a m)
+ (at level 200, a at level 10, m at level 200,
+ format "< a > m") : proto_scope.
+Notation "< a @ x1 .. xn > m" := (iProto_message a (∃ x1, .. (∃ xn, m) ..))
+ (at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
+ format "< a @ x1 .. xn > m") : proto_scope.
+Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m) ..))
+ (at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
+ format "< a @.. x1 .. xn > m") : proto_scope.
+
+Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
+ (tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
+ msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
+Global Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
+
+(** * Operations *)
+Program Definition iMsg_map {Σ V}
+ (rec : iProto Σ V → iProto Σ V) (m : iMsg Σ V) : iMsg Σ V :=
+ IMsg (λ v, λne p1', ∃ p1, iMsg_car m v (Next p1) ∗ p1' ≡ Next (rec p1))%I.
+Next Obligation. solve_proper. Qed.
+
+Program Definition iProto_map_app_aux {Σ V}
+ (f : action → action) (p2 : iProto Σ V)
+ (rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p,
+ proto_elim p2 (λ a m,
+ proto_message (f a) (iMsg_car (iMsg_map rec (IMsg m)))) p.
+Next Obligation.
+ intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a m1 m2 Hm.
+ apply proto_message_ne=> v p' /=. by repeat f_equiv.
+Qed.
+
+Global Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
+ Contractive (iProto_map_app_aux f p2).
+Proof.
+ intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a m1 m2 Hm.
+ apply proto_message_ne=> v p' /=. by repeat (f_contractive || f_equiv).
+Qed.
+
+Definition iProto_map_app {Σ V} (f : action → action)
+ (p2 : iProto Σ V) : iProto Σ V -n> iProto Σ V :=
+ fixpoint (iProto_map_app_aux f p2).
+
+Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
+ iProto_map_app id p2 p1.
+Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
+Definition iProto_app := iProto_app_aux.(unseal).
+Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
+Arguments iProto_app {_ _} _%_proto _%_proto.
+Global Instance: Params (@iProto_app) 2 := {}.
+Infix "<++>" := iProto_app (at level 60) : proto_scope.
+Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
+
+Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V :=
+ iProto_map_app action_dual proto_end p.
+Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
+Definition iProto_dual := iProto_dual_aux.(unseal).
+Definition iProto_dual_eq :
+ @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
+Arguments iProto_dual {_ _} _%_proto.
+Global Instance: Params (@iProto_dual) 2 := {}.
+Notation iMsg_dual := (iMsg_map iProto_dual).
+
+Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
+ if d then iProto_dual p else p.
+Arguments iProto_dual_if {_ _} _ _%_proto.
+Global Instance: Params (@iProto_dual_if) 3 := {}.
+
+(** * Proofs *)
+Section proto.
+ Context `{!protoG Σ V}.
+ Implicit Types v : V.
+ Implicit Types p pl pr : iProto Σ V.
+ Implicit Types m : iMsg Σ V.
+
+ (** ** Equality *)
+ Lemma iProto_case p : p ≡ END ∨ ∃ t n m, p ≡ <(t,n)> m.
+ Proof.
+ rewrite iProto_message_eq iProto_end_eq.
+ destruct (proto_case p) as [|([a n]&m&?)]; [by left|right].
+ by exists a, n, (IMsg m).
+ Qed.
+ Lemma iProto_message_equivI `{!BiInternalEq SPROP} a1 a2 m1 m2 :
+ (<a1> m1) ≡ (<a2> m2) ⊣⊢@{SPROP} ⌜ a1 = a2 ⌠∧
+ (∀ v lp, iMsg_car m1 v lp ≡ iMsg_car m2 v lp).
+ Proof. rewrite iProto_message_eq. apply proto_message_equivI. Qed.
+
+ Lemma iProto_message_end_equivI `{!BiInternalEq SPROP} a m :
+ (<a> m) ≡ END ⊢@{SPROP} False.
+ Proof. rewrite iProto_message_eq iProto_end_eq. apply proto_message_end_equivI. Qed.
+ Lemma iProto_end_message_equivI `{!BiInternalEq SPROP} a m :
+ END ≡ (<a> m) ⊢@{SPROP} False.
+ Proof. by rewrite internal_eq_sym iProto_message_end_equivI. Qed.
+
+ (** ** Non-expansiveness of operators *)
+ Global Instance iMsg_car_proper :
+ Proper (iMsg_equiv ==> (=) ==> (≡) ==> (≡)) (iMsg_car (Σ:=Σ) (V:=V)).
+ Proof.
+ intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
+ f_equiv; [ by f_equiv | done ].
+ Qed.
+ Global Instance iMsg_car_ne n :
+ Proper (iMsg_dist n ==> (=) ==> (dist n) ==> (dist n)) (iMsg_car (Σ:=Σ) (V:=V)).
+ Proof.
+ intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
+ f_equiv; [ by f_equiv | done ].
+ Qed.
+
+ Global Instance iMsg_contractive v n :
+ Proper (dist n ==> dist_later n ==> dist n) (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_contractive. Qed.
+ Global Instance iMsg_ne v : NonExpansive2 (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_proper. Qed.
+ Global Instance iMsg_proper v :
+ Proper ((≡) ==> (≡) ==> (≡)) (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. apply (ne_proper_2 _). Qed.
+
+ Global Instance iMsg_exist_ne A n :
+ Proper (pointwise_relation _ (dist n) ==> (dist n)) (@iMsg_exist Σ V A).
+ Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
+ Global Instance iMsg_exist_proper A :
+ Proper (pointwise_relation _ (≡) ==> (≡)) (@iMsg_exist Σ V A).
+ Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
+
+ Global Instance msg_tele_base (v:V) (P : iProp Σ) (p : iProto Σ V) :
+ MsgTele (TT:=TeleO) (MSG v {{ P }}; p) v P p.
+ Proof. done. Qed.
+ Global Instance msg_tele_exist {A} {TT : A → tele} (m : A → iMsg Σ V) tv tP tp :
+ (∀ x, MsgTele (TT:=TT x) (m x) (tv x) (tP x) (tp x)) →
+ MsgTele (TT:=TeleS TT) (∃ x, m x) tv tP tp.
+ Proof. intros Hm. rewrite /MsgTele /=. f_equiv=> x. apply Hm. Qed.
+
+ Global Instance iProto_message_ne a :
+ NonExpansive (iProto_message (Σ:=Σ) (V:=V) a).
+ Proof. rewrite iProto_message_eq. solve_proper. Qed.
+ Global Instance iProto_message_proper a :
+ Proper ((≡) ==> (≡)) (iProto_message (Σ:=Σ) (V:=V) a).
+ Proof. apply (ne_proper _). Qed.
+
+ Lemma iProto_message_equiv {TT1 TT2 : tele} a1 a2
+ (m1 m2 : iMsg Σ V)
+ (v1 : TT1 -t> V) (v2 : TT2 -t> V)
+ (P1 : TT1 -t> iProp Σ) (P2 : TT2 -t> iProp Σ)
+ (prot1 : TT1 -t> iProto Σ V) (prot2 : TT2 -t> iProto Σ V) :
+ MsgTele m1 v1 P1 prot1 →
+ MsgTele m2 v2 P2 prot2 →
+ ⌜ a1 = a2 ⌠-∗
+ (■∀.. (xs1 : TT1), tele_app P1 xs1 -∗
+ ∃.. (xs2 : TT2), ⌜tele_app v1 xs1 = tele_app v2 xs2⌠∗
+ ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
+ tele_app P2 xs2) -∗
+ (■∀.. (xs2 : TT2), tele_app P2 xs2 -∗
+ ∃.. (xs1 : TT1), ⌜tele_app v1 xs1 = tele_app v2 xs2⌠∗
+ ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
+ tele_app P1 xs1) -∗
+ (<a1> m1) ≡ (<a2> m2).
+ Proof.
+ iIntros (Hm1 Hm2 Heq) "#Heq1 #Heq2".
+ unfold MsgTele in Hm1. rewrite Hm1. clear Hm1.
+ unfold MsgTele in Hm2. rewrite Hm2. clear Hm2.
+ rewrite iProto_message_eq proto_message_equivI.
+ iSplit; [ done | ].
+ iIntros (v p').
+ do 2 rewrite iMsg_texist_exist.
+ rewrite iMsg_base_eq /=.
+ iApply prop_ext.
+ iIntros "!>". iSplit.
+ - iDestruct 1 as (xs1 Hveq1) "[Hrec1 HP1]".
+ iDestruct ("Heq1" with "HP1") as (xs2 Hveq2) "[Hrec2 HP2]".
+ iExists xs2. rewrite -Hveq1 Hveq2.
+ iSplitR; [ done | ]. iSplitR "HP2"; [ | done ].
+ iRewrite -"Hrec1". iApply later_equivI. iIntros "!>". by iRewrite "Hrec2".
+ - iDestruct 1 as (xs2 Hveq2) "[Hrec2 HP2]".
+ iDestruct ("Heq2" with "HP2") as (xs1 Hveq1) "[Hrec1 HP1]".
+ iExists xs1. rewrite -Hveq2 Hveq1.
+ iSplitR; [ done | ]. iSplitR "HP1"; [ | done ].
+ iRewrite -"Hrec2". iApply later_equivI. iIntros "!>". by iRewrite "Hrec1".
+ Qed.
+
+ (** Helpers *)
+ Lemma iMsg_map_base f v P p :
+ NonExpansive f →
+ iMsg_map f (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; f p)%msg.
+ Proof.
+ rewrite iMsg_base_eq. intros ? v' p'; simpl. iSplit.
+ - iDestruct 1 as (p'') "[(->&Hp&$) Hp']". iSplit; [done|].
+ iRewrite "Hp'". iIntros "!>". by iRewrite "Hp".
+ - iIntros "(->&Hp'&$)". iExists p. iRewrite -"Hp'". auto.
+ Qed.
+ Lemma iMsg_map_exist {A} f (m : A → iMsg Σ V) :
+ iMsg_map f (∃ x, m x) ≡ (∃ x, iMsg_map f (m x))%msg.
+ Proof.
+ rewrite iMsg_exist_eq. intros v' p'; simpl. iSplit.
+ - iDestruct 1 as (p'') "[H Hp']". iDestruct "H" as (x) "H"; auto.
+ - iDestruct 1 as (x p'') "[Hm Hp']". auto.
+ Qed.
+
+ (** ** Dual *)
+ Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
+ Proof. rewrite iProto_dual_eq. solve_proper. Qed.
+ Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ V).
+ Proof. apply (ne_proper _). Qed.
+ Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_dual_if_proper d :
+ Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
+ Proof. apply (ne_proper _). Qed.
+
+ Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END.
+ Proof.
+ rewrite iProto_end_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
+ etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
+ by rewrite proto_elim_end.
+ Qed.
+ Lemma iProto_dual_message a m :
+ iProto_dual (<a> m) ≡ <action_dual a> iMsg_dual m.
+ Proof.
+ rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
+ etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
+ rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
+ intros a' m1 m2 Hm; f_equiv; solve_proper.
+ Qed.
+ Lemma iMsg_dual_base v P p :
+ iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg.
+ Proof. apply iMsg_map_base, _. Qed.
+ Lemma iMsg_dual_exist {A} (m : A → iMsg Σ V) :
+ iMsg_dual (∃ x, m x) ≡ (∃ x, iMsg_dual (m x))%msg.
+ Proof. apply iMsg_map_exist. Qed.
+
+ Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
+ Proof.
+ intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+ iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&n&m&->)].
+ { by rewrite !iProto_dual_end. }
+ rewrite !iProto_dual_message involutive.
+ iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
+ iApply prop_ext; iIntros "!>"; iSplit.
+ - iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'".
+ iDestruct "H" as (pdd) "[H #Hpd]".
+ iApply (internal_eq_rewrite); [|done]; iIntros "!>".
+ iRewrite "Hpd". by iRewrite ("IH" $! pdd).
+ - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists _.
+ rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
+ Qed.
+
+ (** ** Append *)
+ Global Instance iProto_app_end_l : LeftId (≡) END (@iProto_app Σ V).
+ Proof.
+ intros p. rewrite iProto_end_eq iProto_app_eq /iProto_app_def /iProto_map_app.
+ etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
+ by rewrite proto_elim_end.
+ Qed.
+ Lemma iProto_app_message a m p2 : (<a> m) <++> p2 ≡ <a> m <++> p2.
+ Proof.
+ rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app.
+ etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
+ rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
+ intros a' m1 m2 Hm. f_equiv; solve_proper.
+ Qed.
+
+ Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
+ Proof.
+ assert (∀ n, Proper (dist n ==> (=) ==> dist n) (@iProto_app Σ V)).
+ { intros n p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
+ assert (Proper ((≡) ==> (=) ==> (≡)) (@iProto_app Σ V)).
+ { intros p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
+ intros n p1 p1' Hp1 p2 p2' Hp2. rewrite Hp1. clear p1 Hp1.
+ revert p1'. induction (lt_wf n) as [n _ IH]; intros p1.
+ destruct (iProto_case p1) as [->|(a&i&m&->)].
+ { by rewrite !left_id. }
+ rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
+ f_contractive. apply IH; eauto using dist_le with lia.
+ Qed.
+ Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
+ Proof. apply (ne_proper_2 _). Qed.
+
+ Lemma iMsg_app_base v P p1 p2 :
+ ((MSG v {{ P }}; p1) <++> p2)%msg ≡ (MSG v {{ P }}; p1 <++> p2)%msg.
+ Proof. apply: iMsg_map_base. Qed.
+ Lemma iMsg_app_exist {A} (m : A → iMsg Σ V) p2 :
+ ((∃ x, m x) <++> p2)%msg ≡ (∃ x, m x <++> p2)%msg.
+ Proof. apply iMsg_map_exist. Qed.
+
+ Global Instance iProto_app_end_r : RightId (≡) END (@iProto_app Σ V).
+ Proof.
+ intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+ iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&i&m&->)].
+ { by rewrite left_id. }
+ rewrite iProto_app_message.
+ iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
+ iApply prop_ext; iIntros "!>". iSplit.
+ - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'".
+ iApply (internal_eq_rewrite); [|done]; iIntros "!>".
+ by iRewrite ("IH" $! p1').
+ - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists p''.
+ rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
+ Qed.
+ Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
+ Proof.
+ intros p1 p2 p3. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+ iLöb as "IH" forall (p1). destruct (iProto_case p1) as [->|(a&i&m&->)].
+ { by rewrite !left_id. }
+ rewrite !iProto_app_message.
+ iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=".
+ iApply prop_ext; iIntros "!>". iSplit.
+ - iDestruct 1 as (p1') "[H #Hp']".
+ iExists (p1' <++> p2). iSplitL; [by auto|].
+ iRewrite "Hp'". iIntros "!>". iApply "IH".
+ - iDestruct 1 as (p12) "[H #Hp123]". iDestruct "H" as (p1') "[H #Hp12]".
+ iExists p1'. iFrame "H". iRewrite "Hp123".
+ iIntros "!>". iRewrite "Hp12". by iRewrite ("IH" $! p1').
+ Qed.
+
+ Lemma iProto_dual_app p1 p2 :
+ iProto_dual (p1 <++> p2) ≡ iProto_dual p1 <++> iProto_dual p2.
+ Proof.
+ apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+ iLöb as "IH" forall (p1 p2). destruct (iProto_case p1) as [->|(a&i&m&->)].
+ { by rewrite iProto_dual_end !left_id. }
+ rewrite iProto_dual_message !iProto_app_message iProto_dual_message /=.
+ iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p12) "/=".
+ iApply prop_ext; iIntros "!>". iSplit.
+ - iDestruct 1 as (p12d) "[H #Hp12]". iDestruct "H" as (p1') "[H #Hp12d]".
+ iExists (iProto_dual p1'). iSplitL; [by auto|].
+ iRewrite "Hp12". iIntros "!>". iRewrite "Hp12d". iApply "IH".
+ - iDestruct 1 as (p1') "[H #Hp12]". iDestruct "H" as (p1d) "[H #Hp1']".
+ iExists (p1d <++> p2). iSplitL; [by auto|].
+ iRewrite "Hp12". iIntros "!>". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
+ Qed.
+
+End proto.
+
+Global Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate END.
+
+Definition can_step {Σ V} (rec : list (iProto Σ V) → iProp Σ)
+ (ps : list (iProto Σ V)) (i j : nat) : iProp Σ :=
+ ∀ m1 m2,
+ (ps !!! i ≡ (<(Send, j)> m1)) -∗
+ (ps !!! j ≡ (<(Recv, i)> m2)) -∗
+ ∀ v p1, iMsg_car m1 v (Next p1) -∗
+ ∃ p2, iMsg_car m2 v (Next p2) ∗
+ â–· (rec (<[i:=p1]>(<[j:=p2]>ps))).
+
+Definition valid_target {Σ V} (ps : list (iProto Σ V)) (i j : nat) : iProp Σ :=
+ ∀ a m, (ps !!! i ≡ (<(a, j)> m)) -∗ ⌜is_Some (ps !! j)âŒ.
+
+Definition iProto_consistent_pre {Σ V} (rec : list (iProto Σ V) → iProp Σ)
+ (ps : list (iProto Σ V)) : iProp Σ :=
+ (∀ i j, valid_target ps i j) ∗ (∀ i j, can_step rec ps i j).
+
+Global Instance iProto_consistent_pre_ne {Σ V}
+ (rec : listO (iProto Σ V) -n> iPropO Σ) :
+ NonExpansive (iProto_consistent_pre rec).
+Proof. rewrite /iProto_consistent_pre /can_step /valid_target. solve_proper. Qed.
+
+Program Definition iProto_consistent_pre' {Σ V}
+ (rec : listO (iProto Σ V) -n> iPropO Σ) :
+ listO (iProto Σ V) -n> iPropO Σ :=
+ λne ps, iProto_consistent_pre (λ ps, rec ps) ps.
+
+Local Instance iProto_consistent_pre_contractive {Σ V} : Contractive (@iProto_consistent_pre' Σ V).
+Proof.
+ rewrite /iProto_consistent_pre' /iProto_consistent_pre /can_step.
+ solve_contractive.
+Qed.
+
+Definition iProto_consistent {Σ V} (ps : list (iProto Σ V)) : iProp Σ :=
+ fixpoint iProto_consistent_pre' ps.
+
+Arguments iProto_consistent {_ _} _%_proto.
+Global Instance: Params (@iProto_consistent) 1 := {}.
+
+Global Instance iProto_consistent_ne {Σ V} : NonExpansive (@iProto_consistent Σ V).
+Proof. solve_proper. Qed.
+Global Instance iProto_consistent_proper {Σ V} : Proper ((≡) ==> (⊣⊢)) (@iProto_consistent Σ V).
+Proof. solve_proper. Qed.
+
+Lemma iProto_consistent_unfold {Σ V} (ps : list (iProto Σ V)) :
+ iProto_consistent ps ≡ (iProto_consistent_pre iProto_consistent) ps.
+Proof.
+ apply: (fixpoint_unfold iProto_consistent_pre').
+Qed.
+
+(** * Protocol entailment *)
+Definition iProto_le_pre {Σ V}
+ (rec : iProto Σ V → iProto Σ V → iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
+ (p1 ≡ END ∗ p2 ≡ END) ∨
+ ∃ a1 a2 m1 m2,
+ (p1 ≡ <a1> m1) ∗ (p2 ≡ <a2> m2) ∗
+ match a1, a2 with
+ | (Recv,i), (Recv,j) => ⌜i = j⌠∗ ∀ v p1',
+ iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ rec p1' p2' ∗ iMsg_car m2 v (Next p2')
+ | (Send,i), (Send,j) => ⌜i = j⌠∗ ∀ v p2',
+ iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ rec p1' p2' ∗ iMsg_car m1 v (Next p1')
+ | _, _ => False
+ end.
+Global Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
+ NonExpansive2 (iProto_le_pre rec).
+Proof. solve_proper. Qed.
+
+Program Definition iProto_le_pre' {Σ V}
+ (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
+ iProto Σ V -n> iProto Σ V -n> iPropO Σ := λne p1 p2,
+ iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
+Solve Obligations with solve_proper.
+Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V).
+Proof.
+ intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
+ by repeat (f_contractive || f_equiv).
+Qed.
+Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
+ fixpoint iProto_le_pre' p1 p2.
+Arguments iProto_le {_ _} _%_proto _%_proto.
+Global Instance: Params (@iProto_le) 2 := {}.
+Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
+
+Global Instance iProto_le_ne {Σ V} : NonExpansive2 (@iProto_le Σ V).
+Proof. solve_proper. Qed.
+Global Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
+Proof. solve_proper. Qed.
+
+Record proto_name := ProtName { proto_names : gmap nat gname }.
+Global Instance proto_name_inhabited : Inhabited proto_name :=
+ populate (ProtName inhabitant).
+Global Instance proto_name_eq_dec : EqDecision proto_name.
+Proof. solve_decision. Qed.
+Global Instance proto_name_countable : Countable proto_name.
+Proof.
+ refine (inj_countable (λ '(ProtName γs), (γs))
+ (λ '(γs), Some (ProtName γs)) _); by intros [].
+Qed.
+
+Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
+ (i : nat) (p : iProto Σ V) : iProp Σ :=
+ own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p))).
+
+Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
+ (ps : list (iProto Σ V)) : iProp Σ :=
+ own γ (gmap_view_auth (DfracOwn 1) ((λ p, Excl' (Next p)) <$> map_seq 0 ps)).
+
+Definition iProto_ctx `{protoG Σ V}
+ (γ : gname) (ps_len : nat) : iProp Σ :=
+ ∃ ps, ⌜length ps = ps_len⌠∗ iProto_own_auth γ ps ∗ ▷ iProto_consistent ps.
+
+(** * The connective for ownership of channel ends *)
+Definition iProto_own `{!protoG Σ V}
+ (γ : gname) (i : nat) (p : iProto Σ V) : iProp Σ :=
+ ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ i p'.
+Arguments iProto_own {_ _ _} _ _ _%_proto.
+Global Instance: Params (@iProto_own) 3 := {}.
+
+Global Instance iProto_own_frag_contractive `{protoG Σ V} γ i :
+ Contractive (iProto_own_frag γ i).
+Proof. solve_contractive. Qed.
+
+Global Instance iProto_own_contractive `{protoG Σ V} γ i :
+ Contractive (iProto_own γ i).
+Proof. solve_contractive. Qed.
+Global Instance iProto_own_ne `{protoG Σ V} γ s : NonExpansive (iProto_own γ s).
+Proof. solve_proper. Qed.
+Global Instance iProto_own_proper `{protoG Σ V} γ s :
+ Proper ((≡) ==> (≡)) (iProto_own γ s).
+Proof. apply (ne_proper _). Qed.
+
+(** * Proofs *)
+Section proto.
+ Context `{!protoG Σ V}.
+ Implicit Types v : V.
+ Implicit Types p pl pr : iProto Σ V.
+ Implicit Types m : iMsg Σ V.
+
+ Lemma own_prot_idx γ i j (p1 p2 : iProto Σ V) :
+ own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p1))) -∗
+ own γ (gmap_view_frag j (DfracOwn 1) (Excl' (Next p2))) -∗
+ ⌜i ≠jâŒ.
+ Proof.
+ iIntros "Hown Hown'" (->).
+ iDestruct (own_valid_2 with "Hown Hown'") as "H".
+ rewrite uPred.cmra_valid_elim.
+ by iDestruct "H" as %[]%gmap_view_frag_op_validN.
+ Qed.
+
+ Lemma own_prot_excl γ i (p1 p2 : iProto Σ V) :
+ own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p1))) -∗
+ own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p2))) -∗
+ False.
+ Proof. iIntros "Hi Hj". by iDestruct (own_prot_idx with "Hi Hj") as %?. Qed.
+
+ (** ** Protocol entailment **)
+ Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2 ≡ iProto_le_pre iProto_le p1 p2.
+ Proof. apply: (fixpoint_unfold iProto_le_pre'). Qed.
+
+ Lemma iProto_le_end : ⊢ END ⊑ (END : iProto Σ V).
+ Proof. rewrite iProto_le_unfold. iLeft. auto 10. Qed.
+
+ Lemma iProto_le_end_inv_r p : p ⊑ END -∗ (p ≡ END).
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
+ iDestruct "H" as (a1 a2 m1 m2) "(_ & Heq & _)".
+ by iDestruct (iProto_end_message_equivI with "Heq") as %[].
+ Qed.
+
+ Lemma iProto_le_end_inv_l p : END ⊑ p -∗ (p ≡ END).
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[_ Hp]|H] //".
+ iDestruct "H" as (a1 a2 m1 m2) "(Heq & _ & _)".
+ iDestruct (iProto_end_message_equivI with "Heq") as %[].
+ Qed.
+
+ Lemma iProto_le_send_inv i p1 m2 :
+ p1 ⊑ (<(Send,i)> m2) -∗ ∃ m1,
+ (p1 ≡ <(Send,i)> m1) ∗
+ ∀ v p2', iMsg_car m2 v (Next p2') -∗
+ ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
+ Proof.
+ rewrite iProto_le_unfold.
+ iIntros "[[_ Heq]|H]".
+ { by iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
+ rewrite iProto_message_equivI. iDestruct "Hp2" as "[%Heq Hm2]".
+ simplify_eq.
+ destruct a1 as [[]]; [|done].
+ iDestruct "H" as (->) "H". iExists m1. iFrame "Hp1".
+ iIntros (v p2). iSpecialize ("Hm2" $! v (Next p2)). by iRewrite "Hm2".
+ Qed.
+
+ Lemma iProto_le_send_send_inv i m1 m2 v p2' :
+ (<(Send,i)> m1) ⊑ (<(Send,i)> m2) -∗
+ iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
+ Proof.
+ iIntros "H Hm2". iDestruct (iProto_le_send_inv with "H") as (m1') "[Hm1 H]".
+ iDestruct (iProto_message_equivI with "Hm1") as (Heq) "Hm1".
+ iDestruct ("H" with "Hm2") as (p1') "[Hle Hm]".
+ iRewrite -("Hm1" $! v (Next p1')) in "Hm". auto with iFrame.
+ Qed.
+
+ Lemma iProto_le_recv_inv_l i m1 p2 :
+ (<(Recv,i)> m1) ⊑ p2 -∗ ∃ m2,
+ (p2 ≡ <(Recv,i)> m2) ∗
+ ∀ v p1', iMsg_car m1 v (Next p1') -∗
+ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
+ Proof.
+ rewrite iProto_le_unfold.
+ iIntros "[[Heq _]|H]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 m1' m2) "(Hp1 & Hp2 & H)".
+ rewrite iProto_message_equivI. iDestruct "Hp1" as "[%Heq Hm1]".
+ simplify_eq.
+ destruct a2 as [[]]; [done|].
+ iDestruct "H" as (->) "H". iExists m2. iFrame "Hp2".
+ iIntros (v p1). iSpecialize ("Hm1" $! v (Next p1)). by iRewrite "Hm1".
+ Qed.
+
+ Lemma iProto_le_recv_inv_r i p1 m2 :
+ (p1 ⊑ <(Recv,i)> m2) -∗ ∃ m1,
+ (p1 ≡ <(Recv,i)> m1) ∗
+ ∀ v p1', iMsg_car m1 v (Next p1') -∗
+ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
+ Proof.
+ rewrite iProto_le_unfold.
+ iIntros "[[_ Heq]|H]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
+ rewrite iProto_message_equivI.
+ iDestruct "Hp2" as "[%Heq Hm2]".
+ simplify_eq.
+ destruct a1 as [[]]; [done|].
+ iDestruct "H" as (->) "H".
+ iExists m1. iFrame.
+ iIntros (v p2).
+ iIntros "Hm1". iDestruct ("H" with "Hm1") as (p2') "[Hle H]".
+ iSpecialize ("Hm2" $! v (Next p2')).
+ iExists p2'. iFrame.
+ iRewrite "Hm2". iApply "H".
+ Qed.
+
+ Lemma iProto_le_recv_recv_inv i m1 m2 v p1' :
+ (<(Recv, i)> m1) ⊑ (<(Recv, i)> m2) -∗
+ iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
+ Proof.
+ iIntros "H Hm2". iDestruct (iProto_le_recv_inv_r with "H") as (m1') "[Hm1 H]".
+ iApply "H". iDestruct (iProto_message_equivI with "Hm1") as (_) "Hm1".
+ by iRewrite -("Hm1" $! v (Next p1')).
+ Qed.
+
+ Lemma iProto_le_msg_inv_l i a m1 p2 :
+ (<(a,i)> m1) ⊑ p2 -∗ ∃ m2, p2 ≡ <(a,i)> m2.
+ Proof.
+ rewrite iProto_le_unfold /iProto_le_pre.
+ iIntros "[[Heq _]|H]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 m1' m2) "(Hp1 & Hp2 & H)".
+ destruct a1 as [t1 ?], a2 as [t2 ?].
+ destruct t1,t2; [|done|done|].
+ - rewrite iProto_message_equivI.
+ iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
+ iDestruct "H" as (->) "H". by iExists _.
+ - rewrite iProto_message_equivI.
+ iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
+ iDestruct "H" as (->) "H". by iExists _.
+ Qed.
+
+ Lemma iProto_le_msg_inv_r j a p1 m2 :
+ (p1 ⊑ <(a,j)> m2) -∗ ∃ m1, p1 ≡ <(a,j)> m1.
+ Proof.
+ rewrite iProto_le_unfold /iProto_le_pre.
+ iIntros "[[_ Heq]|H]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
+ destruct a1 as [t1 ?], a2 as [t2 ?].
+ destruct t1,t2; [|done|done|].
+ - rewrite iProto_message_equivI.
+ iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
+ iDestruct "H" as (->) "H". by iExists _.
+ - rewrite iProto_message_equivI.
+ iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
+ iDestruct "H" as (->) "H". by iExists _.
+ Qed.
+
+ Lemma iProto_le_send i m1 m2 :
+ (∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1',
+ ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')) -∗
+ (<(Send,i)> m1) ⊑ (<(Send,i)> m2).
+ Proof.
+ iIntros "Hle". rewrite iProto_le_unfold.
+ iRight. iExists (Send, i), (Send, i), m1, m2. by eauto.
+ Qed.
+
+ Lemma iProto_le_recv i m1 m2 :
+ (∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2',
+ ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2')) -∗
+ (<(Recv,i)> m1) ⊑ (<(Recv,i)> m2).
+ Proof.
+ iIntros "Hle". rewrite iProto_le_unfold.
+ iRight. iExists (Recv, i), (Recv, i), m1, m2. by eauto.
+ Qed.
+
+ Lemma iProto_le_base a v P p1 p2 :
+ ▷ (p1 ⊑ p2) -∗
+ (<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
+ Proof.
+ rewrite iMsg_base_eq. iIntros "H". destruct a as [[]].
+ - iApply iProto_le_send. iIntros (v' p') "(->&Hp&$)".
+ iExists p1. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
+ - iApply iProto_le_recv. iIntros (v' p') "(->&Hp&$)".
+ iExists p2. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
+ Qed.
+
+ Lemma iProto_le_trans p1 p2 p3 : p1 ⊑ p2 -∗ p2 ⊑ p3 -∗ p1 ⊑ p3.
+ Proof.
+ iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
+ destruct (iProto_case p3) as [->|([]&i&m3&->)].
+ - iDestruct (iProto_le_end_inv_r with "H2") as "H2". by iRewrite "H2" in "H1".
+ - iDestruct (iProto_le_send_inv with "H2") as (m2) "[Hp2 H2]".
+ iRewrite "Hp2" in "H1"; clear p2.
+ iDestruct (iProto_le_send_inv with "H1") as (m1) "[Hp1 H1]".
+ iRewrite "Hp1"; clear p1.
+ iApply iProto_le_send. iIntros (v p3') "Hm3".
+ iDestruct ("H2" with "Hm3") as (p2') "[Hle Hm2]".
+ iDestruct ("H1" with "Hm2") as (p1') "[Hle' Hm1]".
+ iExists p1'. iIntros "{$Hm1} !>". by iApply ("IH" with "Hle'").
+ - iDestruct (iProto_le_recv_inv_r with "H2") as (m2) "[Hp2 H3]".
+ iRewrite "Hp2" in "H1".
+ iDestruct (iProto_le_recv_inv_r with "H1") as (m1) "[Hp1 H2]".
+ iRewrite "Hp1". iApply iProto_le_recv. iIntros (v p1') "Hm1".
+ iDestruct ("H2" with "Hm1") as (p2') "[Hle Hm2]".
+ iDestruct ("H3" with "Hm2") as (p3') "[Hle' Hm3]".
+ iExists p3'. iIntros "{$Hm3} !>". by iApply ("IH" with "Hle").
+ Qed.
+
+ Lemma iProto_le_refl p : ⊢ p ⊑ p.
+ Proof.
+ iLöb as "IH" forall (p). destruct (iProto_case p) as [->|([]&i&m&->)].
+ - iApply iProto_le_end.
+ - iApply iProto_le_send. auto 10 with iFrame.
+ - iApply iProto_le_recv. auto 10 with iFrame.
+ Qed.
+
+
+ Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
+ Proof. solve_proper. Qed.
+
+ Lemma iProto_own_auth_agree γ ps i p :
+ iProto_own_auth γ ps -∗ iProto_own_frag γ i p -∗ ▷ (ps !! i ≡ Some p).
+ Proof.
+ iIntros "Hâ— Hâ—¯".
+ iDestruct (own_valid_2 with "H◠H◯") as "H✓".
+ rewrite gmap_view_both_validI.
+ iDestruct "H✓" as "[_ [H1 H2]]".
+ rewrite lookup_fmap.
+ simpl.
+ rewrite lookup_map_seq_0.
+ destruct (ps !! i) eqn:Heqn; last first.
+ { rewrite Heqn. rewrite !option_equivI. done. }
+ rewrite Heqn.
+ simpl. rewrite !option_equivI excl_equivI. by iNext.
+ Qed.
+
+ Lemma iProto_own_auth_agree_Some γ ps i p :
+ iProto_own_auth γ ps -∗ iProto_own_frag γ i p -∗ ⌜is_Some (ps !! i)âŒ.
+ Proof.
+ iIntros "Hâ— Hâ—¯".
+ iDestruct (own_valid_2 with "H◠H◯") as "H✓".
+ rewrite gmap_view_both_validI.
+ iDestruct "H✓" as "[_ [H1 H2]]".
+ rewrite lookup_fmap.
+ simpl.
+ rewrite lookup_map_seq_0.
+ destruct (ps !! i) eqn:Heqn; last first.
+ { rewrite Heqn. rewrite !option_equivI. done. }
+ rewrite Heqn.
+ simpl. rewrite !option_equivI excl_equivI. done.
+ Qed.
+
+ Lemma iProto_own_auth_update γ ps i p p' :
+ iProto_own_auth γ ps -∗ iProto_own_frag γ i p ==∗
+ iProto_own_auth γ (<[i := p']>ps) ∗ iProto_own_frag γ i p'.
+ Proof.
+ iIntros "Hâ— Hâ—¯".
+ iDestruct (iProto_own_auth_agree_Some with "Hâ— Hâ—¯") as %HSome.
+ iMod (own_update_2 with "Hâ— Hâ—¯") as "[H1 H2]"; [|iModIntro].
+ { eapply (gmap_view_replace _ _ _ (Excl' (Next p'))). done. }
+ iFrame. rewrite -fmap_insert.
+ rewrite /iProto_own_auth.
+ rewrite insert_map_seq_0; [done|].
+ by apply lookup_lt_is_Some_1.
+ Qed.
+
+ Lemma iProto_own_auth_alloc ps :
+ ⊢ |==> ∃ γ, iProto_own_auth γ ps ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
+ Proof.
+ iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γ) "Hauth".
+ { apply gmap_view_auth_valid. }
+ iExists γ.
+ iInduction ps as [|p ps] "IH" using rev_ind.
+ { iModIntro. iFrame. done. }
+ iMod ("IH" with "Hauth") as "[Hauth Hfrags]".
+ iFrame "Hfrags".
+ iMod (own_update with "Hauth") as "[Hauth Hfrag]".
+ { apply (gmap_view_alloc _ (length ps) (DfracOwn 1) (Excl' (Next p))); [|done|done].
+ rewrite fmap_map_seq.
+ rewrite lookup_map_seq_0.
+ apply lookup_ge_None_2. rewrite length_fmap. done. }
+ simpl.
+ iModIntro.
+ rewrite right_id_L.
+ rewrite -fmap_insert. iFrame.
+ iSplitL "Hauth".
+ - rewrite /iProto_own_auth.
+ rewrite map_seq_snoc. simpl. done.
+ - by iApply iProto_le_refl.
+ Qed.
+
+ Lemma list_lookup_Some_le (ps : list $ iProto Σ V) (i : nat) (p1 : iProto Σ V) :
+ ⊢@{iProp Σ} ps !! i ≡ Some p1 -∗ ⌜i < length psâŒ.
+ Proof.
+ iIntros "HSome".
+ rewrite option_equivI.
+ destruct (ps !! i) eqn:Heqn; [|done].
+ iPureIntro.
+ by apply lookup_lt_is_Some_1.
+ Qed.
+
+ Lemma valid_target_le ps i p1 p2 :
+ (∀ i' j', valid_target ps i' j') -∗
+ ps !! i ≡ Some p1 -∗
+ p1 ⊑ p2 -∗
+ (∀ i' j', valid_target (<[i := p2]>ps) i' j') ∗ p1 ⊑ p2.
+ Proof.
+ iIntros "Hprot #HSome Hle".
+ iDestruct (list_lookup_Some_le with "HSome") as %Hi.
+ pose proof (iProto_case p1) as [Hend|Hmsg].
+ { rewrite Hend. iDestruct (iProto_le_end_inv_l with "Hle") as "#H".
+ iFrame "Hle".
+ iIntros (i' j' a m) "Hm".
+ destruct (decide (i = j')) as [->|Hneqj].
+ { rewrite list_lookup_insert; [done|]. done. }
+ rewrite (list_lookup_insert_ne _ i j'); [|done].
+ destruct (decide (i = i')) as [->|Hneqi].
+ { rewrite list_lookup_total_insert; [|done]. iRewrite "H" in "Hm".
+ by iDestruct (iProto_end_message_equivI with "Hm") as "Hm". }
+ rewrite list_lookup_total_insert_ne; [|done].
+ by iApply "Hprot". }
+ destruct Hmsg as (t & n & m & Hmsg).
+ setoid_rewrite Hmsg.
+ iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq". iFrame "Hle".
+ iIntros (i' j' a m') "Hm".
+ destruct (decide (i = j')) as [->|Hneqj].
+ { by rewrite list_lookup_insert. }
+ rewrite (list_lookup_insert_ne _ i j'); [|done].
+ destruct (decide (i = i')) as [->|Hneqi].
+ { rewrite list_lookup_total_insert; [|done]. iRewrite "Heq" in "Hm".
+ iDestruct (iProto_message_equivI with "Hm") as (Heq) "Hm".
+ simplify_eq. iApply ("Hprot" $! i').
+ rewrite list_lookup_total_alt. iRewrite "HSome". done. }
+ rewrite list_lookup_total_insert_ne; [|done].
+ by iApply "Hprot".
+ Qed.
+
+ Lemma iProto_consistent_le ps i p1 p2 :
+ iProto_consistent ps -∗
+ ps !! i ≡ Some p1 -∗
+ p1 ⊑ p2 -∗
+ iProto_consistent (<[i := p2]>ps).
+ Proof.
+ iIntros "Hprot #HSome Hle".
+ iRevert "HSome".
+ iLöb as "IH" forall (p1 p2 ps).
+ iIntros "#HSome".
+ iDestruct (list_lookup_Some_le with "HSome") as %Hi.
+ rewrite !iProto_consistent_unfold.
+ iDestruct "Hprot" as "(Htar & Hprot)".
+ iDestruct (valid_target_le with "Htar HSome Hle") as "[Htar Hle]".
+ iFrame.
+ iIntros (i' j' m1 m2) "#Hm1 #Hm2".
+ destruct (decide (i = i')) as [<-|Hneq].
+ { rewrite list_lookup_total_insert; [|done].
+ pose proof (iProto_case p2) as [Hend|Hmsg].
+ { setoid_rewrite Hend.
+ rewrite !option_equivI. rewrite iProto_end_message_equivI. done. }
+ destruct Hmsg as (a&?&m&Hmsg).
+ setoid_rewrite Hmsg.
+ destruct a; last first.
+ { rewrite !option_equivI. rewrite iProto_message_equivI.
+ iDestruct "Hm1" as "[%Htag Hm1]". done. }
+ rewrite iProto_message_equivI.
+ iDestruct "Hm1" as "[%Htag Hm1]".
+ inversion Htag. simplify_eq.
+ iIntros (v p) "Hm1'".
+ iSpecialize ("Hm1" $! v (Next p)).
+ iDestruct (iProto_le_send_inv with "Hle") as "Hle".
+ iRewrite -"Hm1" in "Hm1'".
+ iDestruct "Hle" as (m') "[#Heq H]".
+ iDestruct ("H" with "Hm1'") as (p') "[Hle H]".
+ destruct (decide (i = j')) as [<-|Hneq].
+ { rewrite list_lookup_total_insert; [|done].
+ rewrite iProto_message_equivI.
+ iDestruct "Hm2" as "[%Heq _]". done. }
+ iDestruct ("Hprot" $!i j' with "[] [] H") as "Hprot".
+ { iRewrite -"Heq". iEval (rewrite list_lookup_total_alt).
+ iRewrite "HSome". done. }
+ { rewrite list_lookup_total_insert_ne; [|done]. done. }
+ iDestruct "Hprot" as (p'') "[Hm Hprot]".
+ iExists p''. iFrame.
+ iNext.
+ iDestruct ("IH" with "Hprot Hle [HSome]") as "HI".
+ { rewrite list_lookup_insert; [done|].
+ by rewrite length_insert. }
+ iClear "IH Hm1 Hm2 Heq".
+ rewrite list_insert_insert.
+ rewrite (list_insert_commute _ j' i); [|done].
+ rewrite list_insert_insert. done. }
+ rewrite list_lookup_total_insert_ne; [|done].
+ destruct (decide (i = j')) as [<-|Hneq'].
+ { rewrite list_lookup_total_insert; [|done].
+ pose proof (iProto_case p2) as [Hend|Hmsg].
+ { setoid_rewrite Hend.
+ rewrite !option_equivI.
+ rewrite iProto_end_message_equivI. done. }
+ destruct Hmsg as (a&?&m&Hmsg).
+ setoid_rewrite Hmsg.
+ destruct a.
+ { rewrite !option_equivI.
+ rewrite iProto_message_equivI.
+ iDestruct "Hm2" as "[%Htag Hm2]". done. }
+ rewrite iProto_message_equivI.
+ iDestruct "Hm2" as "[%Htag Hm2]".
+ inversion Htag. simplify_eq.
+ iIntros (v p) "Hm1'".
+ iDestruct (iProto_le_recv_inv_r with "Hle") as "Hle".
+ iDestruct "Hle" as (m') "[#Heq Hle]".
+ iDestruct ("Hprot" $!i' with "[] [] Hm1'") as "Hprot".
+ { done. }
+ { iEval (rewrite list_lookup_total_alt). iRewrite "HSome". done. }
+ iDestruct ("Hprot") as (p') "[Hm1' Hprot]".
+ iDestruct ("Hle" with "Hm1'") as (p2') "[Hle Hm']".
+ iSpecialize ("Hm2" $! v (Next p2')).
+ iExists p2'.
+ iRewrite -"Hm2". iFrame.
+ iDestruct ("IH" with "Hprot Hle []") as "HI".
+ { iPureIntro. rewrite list_lookup_insert_ne; [|done].
+ by rewrite list_lookup_insert. }
+ rewrite list_insert_commute; [|done].
+ rewrite !list_insert_insert. done. }
+ rewrite list_lookup_total_insert_ne; [|done].
+ iIntros (v p) "Hm1'".
+ iDestruct ("Hprot" $!i' j' with "[//] [//] Hm1'") as "Hprot".
+ iDestruct "Hprot" as (p') "[Hm2' Hprot]".
+ iExists p'. iFrame.
+ iNext.
+ rewrite (list_insert_commute _ j' i); [|done].
+ rewrite (list_insert_commute _ i' i); [|done].
+ iApply ("IH" with "Hprot Hle []").
+ rewrite list_lookup_insert_ne; [|done].
+ rewrite list_lookup_insert_ne; [|done].
+ done.
+ Qed.
+
+ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
+ Proof.
+ iIntros "H". iLöb as "IH" forall (p1 p2).
+ destruct (iProto_case p1) as [->|([]&i&m1&->)].
+ - iDestruct (iProto_le_end_inv_r with "H") as "H".
+ iRewrite "H". iApply iProto_le_refl.
+ - iDestruct (iProto_le_send_inv with "H") as (m2) "[Hp2 H]".
+ iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message).
+ iApply iProto_le_recv. iIntros (v p1d).
+ iDestruct 1 as (p1') "[Hm1 #Hp1d]".
+ iDestruct ("H" with "Hm1") as (p2') "[H Hm2]".
+ iDestruct ("IH" with "H") as "H". iExists (iProto_dual p2').
+ iSplitL "H"; [iIntros "!>"; by iRewrite "Hp1d"|]. simpl; auto.
+ - iDestruct (iProto_le_recv_inv_r with "H") as (m2) "[Hp2 H]".
+ iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message /=).
+ iApply iProto_le_send. iIntros (v p2d).
+ iDestruct 1 as (p2') "[Hm2 #Hp2d]".
+ iDestruct ("H" with "Hm2") as (p1') "[H Hm1]".
+ iDestruct ("IH" with "H") as "H". iExists (iProto_dual p1').
+ iSplitL "H"; [iIntros "!>"; by iRewrite "Hp2d"|]. simpl; auto.
+ Qed.
+
+ Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 ⊢ iProto_dual p1 ⊑ p2.
+ Proof.
+ iIntros "H". iEval (rewrite -(involutive iProto_dual p2)).
+ by iApply iProto_le_dual.
+ Qed.
+ Lemma iProto_le_dual_r p1 p2 : p2 ⊑ iProto_dual p1 ⊢ p1 ⊑ iProto_dual p2.
+ Proof.
+ iIntros "H". iEval (rewrite -(involutive iProto_dual p1)).
+ by iApply iProto_le_dual.
+ Qed.
+
+ Lemma iProto_le_app p1 p2 p3 p4 :
+ p1 ⊑ p2 -∗ p3 ⊑ p4 -∗ p1 <++> p3 ⊑ p2 <++> p4.
+ Proof.
+ iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3 p4).
+ destruct (iProto_case p2) as [->|([]&i&m2&->)].
+ - iDestruct (iProto_le_end_inv_r with "H1") as "H1".
+ iRewrite "H1". by rewrite !left_id.
+ - iDestruct (iProto_le_send_inv with "H1") as (m1) "[Hp1 H1]".
+ iRewrite "Hp1"; clear p1. rewrite !iProto_app_message.
+ iApply iProto_le_send. iIntros (v p24).
+ iDestruct 1 as (p2') "[Hm2 #Hp24]".
+ iDestruct ("H1" with "Hm2") as (p1') "[H1 Hm1]".
+ iExists (p1' <++> p3). iSplitR "Hm1"; [|by simpl; eauto].
+ iIntros "!>". iRewrite "Hp24". by iApply ("IH" with "H1").
+ - iDestruct (iProto_le_recv_inv_r with "H1") as (m1) "[Hp1 H1]".
+ iRewrite "Hp1"; clear p1. rewrite !iProto_app_message.
+ iApply iProto_le_recv.
+ iIntros (v p13). iDestruct 1 as (p1') "[Hm1 #Hp13]".
+ iDestruct ("H1" with "Hm1") as (p2'') "[H1 Hm2]".
+ iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto].
+ iIntros "!>". iRewrite "Hp13". by iApply ("IH" with "H1").
+ Qed.
+
+ Lemma iProto_le_payload_elim_l i m v P p :
+ (P -∗ (<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> m)) ⊢
+ (<(Recv,i)> MSG v {{ P }}; p) ⊑ <(Recv,i)> m.
+ Proof.
+ rewrite iMsg_base_eq. iIntros "H".
+ iApply iProto_le_recv. iIntros (v' p') "(->&Hp&HP)".
+ iApply (iProto_le_recv_recv_inv with "(H HP)"); simpl; auto.
+ Qed.
+ Lemma iProto_le_payload_elim_r i m v P p :
+ (P -∗ (<(Send, i)> m) ⊑ (<(Send, i)> MSG v; p)) ⊢
+ (<(Send,i)> m) ⊑ (<(Send,i)> MSG v {{ P }}; p).
+ Proof.
+ rewrite iMsg_base_eq. iIntros "H".
+ iApply iProto_le_send. iIntros (v' p') "(->&Hp&HP)".
+ iApply (iProto_le_send_send_inv with "(H HP)"); simpl; auto.
+ Qed.
+ Lemma iProto_le_payload_intro_l i v P p :
+ P -∗ (<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> MSG v; p).
+ Proof.
+ rewrite iMsg_base_eq.
+ iIntros "HP". iApply iProto_le_send. iIntros (v' p') "(->&Hp&_) /=".
+ iExists p'. iSplitR; [iApply iProto_le_refl|]. auto.
+ Qed.
+ Lemma iProto_le_payload_intro_r i v P p :
+ P -∗ (<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> MSG v {{ P }}; p).
+ Proof.
+ rewrite iMsg_base_eq.
+ iIntros "HP". iApply iProto_le_recv. iIntros (v' p') "(->&Hp&_) /=".
+ iExists p'. iSplitR; [iApply iProto_le_refl|]. auto.
+ Qed.
+ Lemma iProto_le_exist_elim_l {A} i (m1 : A → iMsg Σ V) m2 :
+ (∀ x, (<(Recv,i)> m1 x) ⊑ (<(Recv,i)> m2)) ⊢
+ (<(Recv,i) @ x> m1 x) ⊑ (<(Recv,i)> m2).
+ Proof.
+ rewrite iMsg_exist_eq. iIntros "H".
+ iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
+ by iApply (iProto_le_recv_recv_inv with "H").
+ Qed.
+ Lemma iProto_le_exist_elim_r {A} i m1 (m2 : A → iMsg Σ V) :
+ (∀ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x)) ⊢
+ (<(Send,i)> m1) ⊑ (<(Send,i) @ x> m2 x).
+ Proof.
+ rewrite iMsg_exist_eq. iIntros "H".
+ iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
+ by iApply (iProto_le_send_send_inv with "H").
+ Qed.
+ Lemma iProto_le_exist_intro_l {A} i (m : A → iMsg Σ V) a :
+ ⊢ (<(Send,i) @ x> m x) ⊑ (<(Send,i)> m a).
+ Proof.
+ rewrite iMsg_exist_eq. iApply iProto_le_send. iIntros (v p') "Hm /=".
+ iExists p'. iSplitR; last by auto. iApply iProto_le_refl.
+ Qed.
+ Lemma iProto_le_exist_intro_r {A} i (m : A → iMsg Σ V) a :
+ ⊢ (<(Recv,i)> m a) ⊑ (<(Recv,i) @ x> m x).
+ Proof.
+ rewrite iMsg_exist_eq. iApply iProto_le_recv. iIntros (v p') "Hm /=".
+ iExists p'. iSplitR; last by auto. iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_le_texist_elim_l {TT : tele} i (m1 : TT → iMsg Σ V) m2 :
+ (∀ x, (<(Recv,i)> m1 x) ⊑ (<(Recv,i)> m2)) ⊢
+ (<(Recv,i) @.. x> m1 x) ⊑ (<(Recv,i)> m2).
+ Proof.
+ iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
+ iApply iProto_le_exist_elim_l; iIntros (x).
+ iApply "IH". iIntros (xs). iApply "H".
+ Qed.
+ Lemma iProto_le_texist_elim_r {TT : tele} i m1 (m2 : TT → iMsg Σ V) :
+ (∀ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x)) -∗
+ (<(Send,i)> m1) ⊑ (<(Send,i) @.. x> m2 x).
+ Proof.
+ iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
+ iApply iProto_le_exist_elim_r; iIntros (x).
+ iApply "IH". iIntros (xs). iApply "H".
+ Qed.
+
+ Lemma iProto_le_texist_intro_l {TT : tele} i (m : TT → iMsg Σ V) x :
+ ⊢ (<(Send,i) @.. x> m x) ⊑ (<(Send,i)> m x).
+ Proof.
+ induction x as [|T TT x xs IH] using tele_arg_ind; simpl.
+ { iApply iProto_le_refl. }
+ iApply iProto_le_trans; [by iApply iProto_le_exist_intro_l|]. iApply IH.
+ Qed.
+ Lemma iProto_le_texist_intro_r {TT : tele} i (m : TT → iMsg Σ V) x :
+ ⊢ (<(Recv,i)> m x) ⊑ (<(Recv,i) @.. x> m x).
+ Proof.
+ induction x as [|T TT x xs IH] using tele_arg_ind; simpl.
+ { iApply iProto_le_refl. }
+ iApply iProto_le_trans; [|by iApply iProto_le_exist_intro_r]. iApply IH.
+ Qed.
+
+ Lemma iProto_consistent_target ps m a i j :
+ iProto_consistent ps -∗
+ ps !! i ≡ Some (<(a, j)> m) -∗
+ ⌜is_Some (ps !! j)âŒ.
+ Proof.
+ rewrite iProto_consistent_unfold. iDestruct 1 as "[Htar _]".
+ iIntros "H". iApply ("Htar" $! i).
+ rewrite list_lookup_total_alt. iRewrite "H". done.
+ Qed.
+
+ Lemma iProto_consistent_step ps m1 m2 i j v p1 :
+ iProto_consistent ps -∗
+ ps !! i ≡ Some (<(Send, j)> m1) -∗
+ ps !! j ≡ Some (<(Recv, i)> m2) -∗
+ iMsg_car m1 v (Next p1) -∗
+ ∃ p2, iMsg_car m2 v (Next p2) ∗
+ â–· iProto_consistent (<[i := p1]>(<[j := p2]>ps)).
+ Proof.
+ iIntros "Hprot #Hi #Hj Hm1".
+ rewrite iProto_consistent_unfold /iProto_consistent_pre.
+ iDestruct "Hprot" as "[_ Hprot]".
+ iDestruct ("Hprot" $! i j with "[Hi] [Hj] Hm1") as (p2) "[Hm2 Hprot]".
+ { rewrite list_lookup_total_alt. iRewrite "Hi". done. }
+ { rewrite list_lookup_total_alt. iRewrite "Hj". done. }
+ iExists p2. iFrame.
+ Qed.
+
+ Lemma iProto_own_le γ s p1 p2 :
+ iProto_own γ s p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ s p2.
+ Proof.
+ iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
+ iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
+ Qed.
+
+ Lemma iProto_own_excl γ i (p1 p2 : iProto Σ V) :
+ iProto_own γ i p1 -∗ iProto_own γ i p2 -∗ False.
+ Proof.
+ rewrite /iProto_own.
+ iDestruct 1 as (p1') "[_ Hp1]".
+ iDestruct 1 as (p2') "[_ Hp2]".
+ iDestruct (own_prot_excl with "Hp1 Hp2") as %[].
+ Qed.
+
+ Lemma iProto_ctx_agree γ n i p :
+ iProto_ctx γ n -∗
+ iProto_own γ i p -∗
+ ⌜i < nâŒ.
+ Proof.
+ iIntros "Hctx Hown".
+ rewrite /iProto_ctx /iProto_own.
+ iDestruct "Hctx" as (ps <-) "[Hauth Hps]".
+ iDestruct "Hown" as (p') "[Hle Hown]".
+ iDestruct (iProto_own_auth_agree_Some with "Hauth Hown") as %HSome.
+ iPureIntro.
+ by apply lookup_lt_is_Some_1.
+ Qed.
+
+ Lemma iProto_init ps :
+ ▷ iProto_consistent ps -∗
+ |==> ∃ γ, iProto_ctx γ (length ps) ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
+ Proof.
+ iIntros "Hconsistent".
+ iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
+ iExists γ. by iFrame.
+ Qed.
+
+ Lemma iProto_step γ ps_dom i j m1 m2 p1 v :
+ iProto_ctx γ ps_dom -∗
+ iProto_own γ i (<(Send, j)> m1) -∗
+ iProto_own γ j (<(Recv, i)> m2) -∗
+ iMsg_car m1 v (Next p1) ==∗
+ ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ iProto_ctx γ ps_dom ∗
+ iProto_own γ i p1 ∗ iProto_own γ j p2.
+ Proof.
+ iIntros "Hctx Hi Hj Hm".
+ iDestruct (iProto_ctx_agree with "Hctx Hi") as %Hi.
+ iDestruct (iProto_ctx_agree with "Hctx Hj") as %Hij.
+ iDestruct "Hi" as (pi) "[Hile Hi]".
+ iDestruct "Hj" as (pj) "[Hjle Hj]".
+ iDestruct "Hctx" as (ps Hdom) "[Hauth Hconsistent]".
+ iDestruct (iProto_own_auth_agree with "Hauth Hi") as "#Hpi".
+ iDestruct (iProto_own_auth_agree with "Hauth Hj") as "#Hpj".
+ iDestruct (own_prot_idx with "Hi Hj") as %Hneq.
+ iAssert (▷ (<[i:=<(Send, j)> m1]>ps !! j ≡ Some pj))%I as "Hpj'".
+ { by rewrite list_lookup_insert_ne. }
+ iAssert (▷ (⌜is_Some (ps !! i)⌠∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]"
+ as "[Hi' Hile]".
+ { iNext. iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#Heq".
+ iFrame. iRewrite "Heq" in "Hpi". destruct (ps !! i); [done|].
+ by rewrite option_equivI. }
+ iAssert (▷ (⌜is_Some (ps !! j)⌠∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]"
+ as "[Hj' Hjle]".
+ { iNext. iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#Heq".
+ iFrame. iRewrite "Heq" in "Hpj".
+ destruct (ps !! j); [done|]. by rewrite !option_equivI. }
+ iDestruct (iProto_consistent_le with "Hconsistent Hpi Hile") as "Hconsistent".
+ iDestruct (iProto_consistent_le with "Hconsistent Hpj' Hjle") as "Hconsistent".
+ iDestruct (iProto_consistent_step _ _ _ i j with "Hconsistent [] [] [Hm //]") as
+ (p2) "[Hm2 Hconsistent]".
+ { rewrite list_lookup_insert_ne; [|done].
+ rewrite list_lookup_insert_ne; [|done].
+ rewrite list_lookup_insert; [done|]. lia. }
+ { rewrite list_lookup_insert_ne; [|done].
+ rewrite list_lookup_insert; [done|]. rewrite length_insert. lia. }
+ iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
+ iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
+ iIntros "!>!>". iExists p2. iFrame "Hm2".
+ iDestruct "Hi'" as %Hi'. iDestruct "Hj'" as %Hj'.
+ iSplitL "Hconsistent Hauth".
+ { iExists (<[i:=p1]> (<[j:=p2]> ps)).
+ iSplit.
+ { iPureIntro. rewrite !length_insert. done. }
+ iFrame. rewrite list_insert_insert.
+ rewrite list_insert_commute; [|done]. rewrite list_insert_insert.
+ by rewrite list_insert_commute; [|done]. }
+ iSplitL "Hi"; iExists _; iFrame; iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_target γ ps_dom i a j m :
+ iProto_ctx γ ps_dom -∗
+ iProto_own γ i (<(a, j)> m) -∗
+ â–· (⌜j < ps_domâŒ).
+ Proof.
+ iIntros "Hctx Hown".
+ rewrite /iProto_ctx /iProto_own.
+ iDestruct "Hctx" as (ps Hdom) "[Hauth Hps]".
+ iDestruct "Hown" as (p') "[Hle Hown]".
+ iDestruct (iProto_own_auth_agree with "Hauth Hown") as "#Hi".
+ iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
+ iDestruct (iProto_consistent_target with "Hps []") as "#H".
+ { iNext. iRewrite "Heq" in "Hi". done. }
+ iNext. iDestruct "H" as %HSome.
+ iPureIntro. subst. by apply lookup_lt_is_Some_1.
+ Qed.
+
+ (* (** The instances below make it possible to use the tactics [iIntros], *)
+ (* [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [iProto_le] goals. *) *)
+ Global Instance iProto_le_from_forall_l {A} i (m1 : A → iMsg Σ V) m2 name :
+ AsIdentName m1 name →
+ FromForall (iProto_message (Recv,i) (iMsg_exist m1) ⊑ (<(Recv,i)> m2))
+ (λ x, (<(Recv, i)> m1 x) ⊑ (<(Recv, i)> m2))%I name | 10.
+ Proof. intros _. apply iProto_le_exist_elim_l. Qed.
+ Global Instance iProto_le_from_forall_r {A} i m1 (m2 : A → iMsg Σ V) name :
+ AsIdentName m2 name →
+ FromForall ((<(Send,i)> m1) ⊑ iProto_message (Send,i) (iMsg_exist m2))
+ (λ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x))%I name | 11.
+ Proof. intros _. apply iProto_le_exist_elim_r. Qed.
+
+ Global Instance iProto_le_from_wand_l i m v P p :
+ TCIf (TCEq P True%I) False TCTrue →
+ FromWand ((<(Recv,i)> MSG v {{ P }}; p) ⊑ (<(Recv,i)> m)) P ((<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> m)) | 10.
+ Proof. intros _. apply iProto_le_payload_elim_l. Qed.
+ Global Instance iProto_le_from_wand_r i m v P p :
+ FromWand ((<(Send,i)> m) ⊑ (<(Send,i)> MSG v {{ P }}; p)) P ((<(Send,i)> m) ⊑ (<(Send,i)> MSG v; p)) | 11.
+ Proof. apply iProto_le_payload_elim_r. Qed.
+
+ Global Instance iProto_le_from_exist_l {A} i (m : A → iMsg Σ V) p :
+ FromExist ((<(Send,i) @ x> m x) ⊑ p) (λ a, (<(Send,i)> m a) ⊑ p)%I | 10.
+ Proof.
+ rewrite /FromExist. iDestruct 1 as (x) "H".
+ iApply (iProto_le_trans with "[] H"). iApply iProto_le_exist_intro_l.
+ Qed.
+ Global Instance iProto_le_from_exist_r {A} i (m : A → iMsg Σ V) p :
+ FromExist (p ⊑ <(Recv,i) @ x> m x) (λ a, p ⊑ (<(Recv,i)> m a))%I | 11.
+ Proof.
+ rewrite /FromExist. iDestruct 1 as (x) "H".
+ iApply (iProto_le_trans with "H"). iApply iProto_le_exist_intro_r.
+ Qed.
+
+ Global Instance iProto_le_from_sep_l i m v P p :
+ FromSep ((<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> m)) P ((<(Send,i)> MSG v; p) ⊑ (<(Send,i)> m)) | 10.
+ Proof.
+ rewrite /FromSep. iIntros "[HP H]".
+ iApply (iProto_le_trans with "[HP] H"). by iApply iProto_le_payload_intro_l.
+ Qed.
+ Global Instance iProto_le_from_sep_r i m v P p :
+ FromSep ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ P }}; p)) P ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v; p)) | 11.
+ Proof.
+ rewrite /FromSep. iIntros "[HP H]".
+ iApply (iProto_le_trans with "H"). by iApply iProto_le_payload_intro_r.
+ Qed.
+
+ Global Instance iProto_le_frame_l i q m v R P Q p :
+ Frame q R P Q →
+ Frame q R ((<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> m))
+ ((<(Send,i)> MSG v {{ Q }}; p) ⊑ (<(Send,i)> m)) | 10.
+ Proof.
+ rewrite /Frame /=. iIntros (HP) "[HR H]".
+ iApply (iProto_le_trans with "[HR] H"). iApply iProto_le_payload_elim_r.
+ iIntros "HQ". iApply iProto_le_payload_intro_l. iApply HP; iFrame.
+ Qed.
+ Global Instance iProto_le_frame_r i q m v R P Q p :
+ Frame q R P Q →
+ Frame q R ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ P }}; p))
+ ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ Q }}; p)) | 11.
+ Proof.
+ rewrite /Frame /=. iIntros (HP) "[HR H]".
+ iApply (iProto_le_trans with "H"). iApply iProto_le_payload_elim_l.
+ iIntros "HQ". iApply iProto_le_payload_intro_r. iApply HP; iFrame.
+ Qed.
+
+ Global Instance iProto_le_from_modal a v p1 p2 :
+ FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+ ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
+ Proof. intros _. iApply iProto_le_base. Qed.
+
+End proto.
+
+Global Typeclasses Opaque iProto_ctx iProto_own.
+
+Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
+ first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
diff --git a/multris/channel/proto_model.v b/multris/channel/proto_model.v
new file mode 100644
index 0000000000000000000000000000000000000000..3dc4bf07c21e40703e2794619ffa28b80ededef3
--- /dev/null
+++ b/multris/channel/proto_model.v
@@ -0,0 +1,309 @@
+(** This file defines the model of dependent separation protocols as the
+solution of a recursive domain equation, along with various primitive
+operations, such as append and map.
+
+Important: This file should not be used directly, but rather the wrappers in
+[proto] should be used.
+
+Dependent Separation Protocols are modeled as the solution of the following
+recursive domain equation:
+
+[proto = 1 + (action * (V → ▶ proto → PROP))]
+
+Here, the left-hand side of the sum is used for the terminated process, while
+the right-hand side is used for the communication constructors. The type
+[action] is a pair of a an inductively defined datatype [tag] with two
+constructors [Send] and [Recv], and a synchronosation id of [nat].
+Compared to having an additional sum in [proto], this makes it
+possible to factorize the code in a better way.
+
+The remainder [V → ▶ proto → PROP] is a predicate that ranges over the
+communicated value [V] and the tail protocol [proto]. Note that to solve this
+recursive domain equation using Iris's COFE solver, the recursive occurrence
+of [proto] appear under the later [â–¶].
+
+On top of the type [proto], we define the constructors:
+
+- [proto_end], which constructs the left-side of the sum.
+- [proto_msg], which takes an action and a predicate and constructs the
+ right-hand side of the sum accordingly.
+
+The defined functions on the type [proto] are:
+
+- [proto_map], which can be used to map the actions and the propositions of
+ a given protocol.
+- [proto_app], which appends two protocols [p1] and [p2], by substituting
+ all terminations [END] in [p1] with [p2]. *)
+From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import proofmode.
+From multris.utils Require Import cofe_solver_2.
+Set Default Proof Using "Type".
+
+Module Export action.
+ Inductive tag := Send | Recv.
+ Definition action : Set := tag * nat.
+ Global Instance action_inhabited : Inhabited action := populate (Send,0).
+ Definition action_dual (a : action) : action :=
+ match a with (Send, n) => (Recv, n) | (Recv, n) => (Send, n) end.
+ Global Instance action_dual_involutive : Involutive (=) action_dual.
+ Proof. by intros [[]]. Qed.
+ Canonical Structure actionO := leibnizO action.
+End action.
+
+Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe :=
+ optionO (prodO actionO (V -d> laterO A -n> PROP)).
+Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
+ optionOF (actionO * (V -d> ▶ ∙ -n> PROP)).
+
+Definition proto_result (V : Type) := result_2 (proto_auxOF V).
+Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
+ solution_2_car (proto_result V) PROPn _ PROP _.
+Global Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
+Proof. apply _. Qed.
+Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
+ ofe_iso (proto_auxO V PROP (proto V PROP PROPn)) (proto V PROPn PROP).
+Proof. apply proto_result. Qed.
+
+Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
+ proto_auxO V PROP (proto V PROP PROPn) -n> proto V PROPn PROP := ofe_iso_1 proto_iso.
+Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
+ proto V PROPn PROP -n> proto_auxO V PROP (proto V PROP PROPn) := ofe_iso_2 proto_iso.
+Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
+ proto_fold (proto_unfold p) ≡ p.
+Proof. apply (ofe_iso_12 proto_iso). Qed.
+Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
+ (p : proto_auxO V PROP (proto V PROP PROPn)) :
+ proto_unfold (proto_fold p) ≡ p.
+Proof. apply (ofe_iso_21 proto_iso). Qed.
+
+Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
+ proto_fold None.
+Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
+ (m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
+ proto_fold (Some (a, m)).
+
+Global Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
+ Proper (pointwise_relation V (dist n) ==> dist n)
+ (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
+Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
+Global Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
+ Proper (pointwise_relation V (≡) ==> (≡))
+ (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
+Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
+
+Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
+ p ≡ proto_end ∨ ∃ a m, p ≡ proto_message a m.
+Proof.
+ destruct (proto_unfold p) as [[a m]|] eqn:E; simpl in *; last first.
+ - left. by rewrite -(proto_fold_unfold p) E.
+ - right. exists a, m. by rewrite /proto_message -E proto_fold_unfold.
+Qed.
+Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
+ Inhabited (proto V PROPn PROP) := populate proto_end.
+
+Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
+ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
+ ⊣⊢@{SPROP} ⌜ a1 = a2 ⌠∧ (∀ v p', m1 v p' ≡ m2 v p').
+Proof.
+ trans (proto_unfold (proto_message a1 m1) ≡ proto_unfold (proto_message a2 m2) : SPROP)%I.
+ { iSplit.
+ - iIntros "Heq". by iRewrite "Heq".
+ - iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
+ iRewrite "Heq". by rewrite proto_fold_unfold. }
+ rewrite /proto_message !proto_unfold_fold option_equivI prod_equivI /=.
+ rewrite discrete_eq discrete_fun_equivI.
+ by setoid_rewrite ofe_morO_equivI.
+Qed.
+Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{SPROP} False.
+Proof.
+ trans (proto_unfold (proto_message a m) ≡ proto_unfold proto_end : SPROP)%I.
+ { iIntros "Heq". by iRewrite "Heq". }
+ by rewrite /proto_message !proto_unfold_fold option_equivI.
+Qed.
+Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+ proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
+Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
+
+(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
+is contractive *)
+Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
+ (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
+ (p : proto V PROPn PROP) : A :=
+ match proto_unfold p with None => x | Some (a, m) => f a m end.
+
+Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
+ (x : A) (f1 f2 : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n :
+ (∀ a m1 m2, (∀ v, m1 v ≡{n}≡ m2 v) → f1 a m1 ≡{n}≡ f2 a m2) →
+ p1 ≡{n}≡ p2 →
+ proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2.
+Proof.
+ intros Hf Hp. rewrite /proto_elim.
+ apply (_ : NonExpansive proto_unfold) in Hp
+ as [[a1 m1] [a2 m2] [-> ?]|]; simplify_eq/=; [|done].
+ apply Hf. destruct n; by simpl.
+Qed.
+
+Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
+ (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) :
+ proto_elim x f proto_end ≡ x.
+Proof.
+ rewrite /proto_elim /proto_end.
+ pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
+ by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
+Qed.
+Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
+ (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
+ `{Hf : ∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)} a m :
+ proto_elim x f (proto_message a m) ≡ f a m.
+Proof.
+ rewrite /proto_elim /proto_message /=.
+ pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
+ (PROP:=PROP) (Some (a, m))) as Hfold.
+ destruct (proto_unfold (proto_fold (Some (a, m))))
+ as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
+ by f_equiv=> v.
+Qed.
+
+(** Functor *)
+Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+ (g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
+ proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
+ proto_elim proto_end (λ a m, proto_message a (λ v, g ◎ m v ◎ laterO_map rec)) p.
+Next Obligation.
+ intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
+ apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv.
+Qed.
+
+Global Instance proto_map_aux_contractive {V}
+ `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
+ Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
+Proof.
+ intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm.
+ f_equiv=> v p' /=. do 2 f_equiv; [done|].
+ apply Next_contractive; by dist_later_intro as n' Hn'.
+Qed.
+
+Definition proto_map_aux_2 {V}
+ `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+ (gn : PROPn' -n> PROPn) (g : PROP -n> PROP')
+ (rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
+ proto V PROPn PROP -n> proto V PROPn' PROP' :=
+ proto_map_aux g (proto_map_aux gn rec).
+Global Instance proto_map_aux_2_contractive {V}
+ `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+ (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+ Contractive (proto_map_aux_2 (V:=V) gn g).
+Proof.
+ intros n rec1 rec2 Hrec. rewrite /proto_map_aux_2.
+ f_equiv. by apply proto_map_aux_contractive.
+Qed.
+Definition proto_map {V}
+ `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+ (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+ proto V PROPn PROP -n> proto V PROPn' PROP' :=
+ fixpoint (proto_map_aux_2 gn g).
+
+Lemma proto_map_unfold {V}
+ `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
+ (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
+ proto_map (V:=V) gn g p ≡ proto_map_aux g (proto_map g gn) p.
+Proof.
+ apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
+ induction (lt_wf n) as [n _ IH]=>
+ PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
+ etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
+ apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
+Qed.
+Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+ (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+ proto_map (V:=V) gn g proto_end ≡ proto_end.
+Proof. by rewrite proto_map_unfold /proto_map_aux /= proto_elim_end. Qed.
+Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+ (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
+ proto_map (V:=V) gn g (proto_message a m)
+ ≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
+Proof.
+ rewrite proto_map_unfold /proto_map_aux /=.
+ rewrite ->proto_elim_message; [done|].
+ intros a' m1 m2 Hm. f_equiv; solve_proper.
+Qed.
+
+Lemma proto_map_ne {V}
+ `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
+ (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
+ gn1 ≡{n}≡ gn2 → g1 ≡{n}≡ g2 →
+ proto_map (V:=V) gn1 g1 p ≡{n}≡ proto_map (V:=V) gn2 g2 p.
+Proof.
+ revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn1 gn2 g1 g2 p.
+ induction (lt_wf n) as [n _ IH]=>
+ PROPn ? PROPn' ? PROP ? PROP' ? gn1 gn2 g1 g2 p Hgn Hg /=.
+ destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
+ rewrite !proto_map_message /=.
+ apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
+ apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_le with lia.
+Qed.
+Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+ (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
+ gn1 ≡ gn2 → g1 ≡ g2 → proto_map (V:=V) gn1 g1 p ≡ proto_map (V:=V) gn2 g2 p.
+Proof.
+ intros Hgn Hg. apply equiv_dist=> n.
+ apply proto_map_ne=> // ?; by apply equiv_dist.
+Qed.
+Lemma proto_map_id {V} `{Hcn:!Cofe PROPn, Hc:!Cofe PROP} (p : proto V PROPn PROP) :
+ proto_map cid cid p ≡ p.
+Proof.
+ apply equiv_dist=> n. revert PROPn Hcn PROP Hc p.
+ induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
+ destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
+ rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
+ apply Next_contractive; dist_later_intro as n' Hn'; auto.
+Qed.
+Lemma proto_map_compose {V}
+ `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
+ Hc:!Cofe PROP, Hc':!Cofe PROP', Hc'':!Cofe PROP''}
+ (gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
+ (g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
+ proto_map (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map gn1 g2 (proto_map gn2 g1 p).
+Proof.
+ apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROPn'' Hcn''
+ PROP Hc PROP' Hc' PROP'' Hc'' gn1 gn2 g1 g2 p.
+ induction (lt_wf n) as [n _ IH]=> PROPn ? PROPn' ? PROPn'' ?
+ PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
+ destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
+ rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
+ do 3 f_equiv. apply Next_contractive; dist_later_intro as n' Hn'; simpl; auto.
+Qed.
+
+Program Definition protoOF (V : Type) (Fn F : oFunctor)
+ `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
+ `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} : oFunctor := {|
+ oFunctor_car A _ B _ := proto V (oFunctor_car Fn B A) (oFunctor_car F A B);
+ oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+ proto_map (oFunctor_map Fn (fg.2, fg.1)) (oFunctor_map F fg)
+|}.
+Next Obligation.
+ intros V Fn F ?? A1 ? A2 ? B1 ? B2 ? n f g [??] p; simpl in *.
+ apply proto_map_ne=> // y; by apply oFunctor_map_ne.
+Qed.
+Next Obligation.
+ intros V Fn F ?? A ? B ? p; simpl in *. rewrite /= -{2}(proto_map_id p).
+ apply proto_map_ext=> //= y; by rewrite oFunctor_map_id.
+Qed.
+Next Obligation.
+ intros V Fn F ?? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' p; simpl in *.
+ rewrite -proto_map_compose.
+ apply proto_map_ext=> //= y; by rewrite ofe.oFunctor_map_compose.
+Qed.
+
+Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
+ `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
+ `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
+ oFunctorContractive Fn → oFunctorContractive F →
+ oFunctorContractive (protoOF V Fn F).
+Proof.
+ intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
+ apply proto_map_ne=> y //=.
+ + apply HFn. dist_later_intro as n' Hn'. f_equiv; apply Hfg.
+ + apply HF. by dist_later_intro as n' Hn'.
+Qed.
diff --git a/multris/examples/basics.v b/multris/examples/basics.v
new file mode 100644
index 0000000000000000000000000000000000000000..53ad44ad83e4699babe78a1c9486aa151c27b40a
--- /dev/null
+++ b/multris/examples/basics.v
@@ -0,0 +1,431 @@
+From multris.channel Require Import proofmode.
+Set Default Proof Using "Type".
+
+Definition iProto_empty {Σ} : list (iProto Σ) := [].
+
+Lemma iProto_consistent_empty {Σ} :
+ ⊢ iProto_consistent (@iProto_empty Σ).
+Proof. iProto_consistent_take_steps. Qed.
+
+Definition iProto_binary `{!heapGS Σ} : list (iProto Σ) :=
+ [(<(Send, 1) @ (x:Z)> MSG #x ; END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ; END)%proto].
+
+Lemma iProto_binary_consistent `{!heapGS Σ} :
+ ⊢ iProto_consistent iProto_binary.
+Proof. rewrite /iProto_binary. iProto_consistent_take_steps. Qed.
+
+Definition roundtrip_prog : val :=
+ λ: <>,
+ let: "cs" := new_chan #3 in
+ let: "c0" := get_chan "cs" #0 in
+ let: "c1" := get_chan "cs" #1 in
+ let: "c2" := get_chan "cs" #2 in
+ Fork (let: "x" := recv "c1" #0 in send "c1" #2 "x");;
+ Fork (let: "x" := recv "c2" #1 in send "c2" #0 "x");;
+ send "c0" #1 #42;; recv "c0" #2.
+
+Section channel.
+ Context `{!heapGS Σ, !chanG Σ}.
+
+ Definition iProto_roundtrip : list (iProto Σ) :=
+ [(<(Send, 1) @ (x:Z)> MSG #x ; <(Recv, 2)> MSG #x; END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ; <(Send, 2)> MSG #x; END)%proto;
+ (<(Recv, 1) @ (x:Z)> MSG #x ; <(Send, 0)> MSG #x; END)%proto].
+
+ Lemma iProto_roundtrip_consistent :
+ ⊢ iProto_consistent iProto_roundtrip.
+ Proof. rewrite /iProto_roundtrip. iProto_consistent_take_steps. Qed.
+
+ Lemma roundtrip_prog_spec :
+ {{{ True }}} roundtrip_prog #() {{{ RET #42 ; True }}}.
+ Proof using chanG0 heapGS0 Σ.
+ iIntros (Φ) "_ HΦ". wp_lam.
+ wp_new_chan iProto_roundtrip with iProto_roundtrip_consistent
+ as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
+ wp_smart_apply (wp_fork with "[Hc1]").
+ { iIntros "!>". wp_recv (x) as "_". wp_send with "[//]". done. }
+ wp_smart_apply (wp_fork with "[Hc2]").
+ { iIntros "!>". wp_recv (x) as "_". wp_send with "[//]". done. }
+ wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
+ Qed.
+
+End channel.
+
+Definition roundtrip_ref_prog : val :=
+ λ: <>,
+ let: "cs" := new_chan #3 in
+ let: "c0" := get_chan "cs" #0 in
+ let: "c1" := get_chan "cs" #1 in
+ let: "c2" := get_chan "cs" #2 in
+ Fork (let: "l" := recv "c1" #0 in "l" <- !"l" + #1;; send "c1" #2 "l");;
+ Fork (let: "l" := recv "c2" #1 in "l" <- !"l" + #1;; send "c2" #0 #());;
+ let: "l" := ref #40 in send "c0" #1 "l";; recv "c0" #2;; !"l".
+
+Section roundtrip_ref.
+ Context `{!heapGS Σ, !chanG Σ}.
+
+ Definition iProto_roundtrip_ref : list (iProto Σ) :=
+ [(<(Send, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Recv, 2)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto;
+ (<(Recv, 0) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Send, 2)> MSG #l {{ l ↦ #(x+1) }}; END)%proto;
+ (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Send, 0)> MSG #() {{ l ↦ #(x+1) }}; END)%proto].
+
+ Lemma iProto_roundtrip_ref_consistent :
+ ⊢ iProto_consistent iProto_roundtrip_ref.
+ Proof.
+ rewrite /iProto_roundtrip_ref.
+ iProto_consistent_take_steps.
+ replace (x0 + 1 + 1)%Z with (x0+2)%Z by lia. iFrame.
+ iProto_consistent_take_step.
+ Qed.
+
+ Lemma roundtrip_ref_prog_spec :
+ {{{ True }}} roundtrip_ref_prog #() {{{ RET #42 ; True }}}.
+ Proof using chanG0.
+ iIntros (Φ) "_ HΦ". wp_lam.
+ wp_new_chan iProto_roundtrip_ref with iProto_roundtrip_ref_consistent
+ as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
+ wp_smart_apply (wp_fork with "[Hc1]").
+ { iIntros "!>".
+ wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[$Hl]". }
+ wp_smart_apply (wp_fork with "[Hc2]").
+ { iIntros "!>".
+ wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[$Hl]". }
+ wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
+ by iApply "HΦ".
+ Qed.
+
+End roundtrip_ref.
+
+Definition roundtrip_ref_rec_prog : val :=
+ λ: <>,
+ let: "cs" := new_chan #3 in
+ let: "c0" := get_chan "cs" #0 in
+ let: "c1" := get_chan "cs" #1 in
+ let: "c2" := get_chan "cs" #2 in
+ Fork ((rec: "go" "c1" :=
+ let: "l" := recv "c1" #0 in "l" <- !"l" + #1;; send "c1" #2 "l";;
+ "go" "c1") "c1");;
+ Fork ((rec: "go" "c2" :=
+ let: "l" := recv "c2" #1 in "l" <- !"l" + #1;; send "c2" #0 #();;
+ "go" "c2") "c2");;
+ let: "l" := ref #38 in
+ send "c0" #1 "l";; recv "c0" #2;;
+ send "c0" #1 "l";; recv "c0" #2;; !"l".
+
+Section roundtrip_ref_rec.
+ Context `{!heapGS Σ, !chanG Σ}.
+
+ Definition iProto_roundtrip_ref_rec1_aux (rec : iProto Σ) : iProto Σ :=
+ (<(Send, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Recv, 2)> MSG #() {{ l ↦ #(x+2) }} ; rec)%proto.
+ Instance iProto_roundtrip_ref_rec1_contractive :
+ Contractive iProto_roundtrip_ref_rec1_aux.
+ Proof. solve_proto_contractive. Qed.
+ Definition iProto_roundtrip_ref_rec1 :=
+ fixpoint iProto_roundtrip_ref_rec1_aux.
+ Lemma iProto_roundtrip_ref_rec1_unfold :
+ iProto_roundtrip_ref_rec1 ≡
+ (iProto_roundtrip_ref_rec1_aux iProto_roundtrip_ref_rec1).
+ Proof. apply (fixpoint_unfold _). Qed.
+ Global Instance iProto_roundtrip_ref_rec1_proto_unfold :
+ ProtoUnfold iProto_roundtrip_ref_rec1
+ (iProto_roundtrip_ref_rec1_aux iProto_roundtrip_ref_rec1).
+ Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
+
+ Definition iProto_roundtrip_ref_rec2_aux (rec : iProto Σ) : iProto Σ :=
+ (<(Recv, 0) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Send, 2)> MSG #l {{ l ↦ #(x+1) }}; rec)%proto.
+ Instance iProto_roundtrip_ref_rec2_contractive :
+ Contractive iProto_roundtrip_ref_rec2_aux.
+ Proof. solve_proto_contractive. Qed.
+ Definition iProto_roundtrip_ref_rec2 :=
+ fixpoint iProto_roundtrip_ref_rec2_aux.
+ Lemma iProto_roundtrip_ref_rec2_unfold :
+ iProto_roundtrip_ref_rec2 ≡
+ (iProto_roundtrip_ref_rec2_aux iProto_roundtrip_ref_rec2).
+ Proof. apply (fixpoint_unfold _). Qed.
+
+ Global Instance iProto_roundtrip_ref_rec2_proto_unfold :
+ ProtoUnfold iProto_roundtrip_ref_rec2
+ (iProto_roundtrip_ref_rec2_aux iProto_roundtrip_ref_rec2).
+ Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
+ Definition iProto_roundtrip_ref_rec3_aux (rec : iProto Σ) : iProto Σ :=
+ (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Send, 0)> MSG #() {{ l ↦ #(x+1) }}; rec)%proto.
+ Instance iProto_roundtrip_ref_rec3_contractive :
+ Contractive iProto_roundtrip_ref_rec3_aux.
+ Proof. solve_proto_contractive. Qed.
+ Definition iProto_roundtrip_ref_rec3 :=
+ fixpoint iProto_roundtrip_ref_rec3_aux.
+ Lemma iProto_roundtrip_ref_rec3_unfold :
+ iProto_roundtrip_ref_rec3 ≡
+ (iProto_roundtrip_ref_rec3_aux iProto_roundtrip_ref_rec3).
+ Proof. apply (fixpoint_unfold _). Qed.
+ Global Instance iProto_roundtrip_ref_rec3_proto_unfold :
+ ProtoUnfold iProto_roundtrip_ref_rec3
+ (iProto_roundtrip_ref_rec3_aux iProto_roundtrip_ref_rec3).
+ Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
+
+ Definition iProto_roundtrip_ref_rec : list (iProto Σ) :=
+ [iProto_roundtrip_ref_rec1;
+ iProto_roundtrip_ref_rec2;
+ iProto_roundtrip_ref_rec3].
+
+ Lemma iProto_roundtrip_ref_rec_consistent :
+ ⊢ iProto_consistent iProto_roundtrip_ref_rec.
+ Proof.
+ iLöb as "IH".
+ rewrite /iProto_roundtrip_ref_rec.
+ iEval (rewrite iProto_roundtrip_ref_rec1_unfold).
+ iEval (rewrite iProto_roundtrip_ref_rec2_unfold).
+ iEval (rewrite iProto_roundtrip_ref_rec3_unfold).
+ iProto_consistent_take_step.
+ iIntros (l x) "Hloc". iExists _, _. iSplit; [done|]. iFrame.
+ iProto_consistent_take_step.
+ iIntros "Hloc". iExists _, _. iSplit; [done|]. iFrame. iNext.
+ rewrite iProto_roundtrip_ref_rec2_unfold.
+ iProto_consistent_take_step.
+ iIntros "Hloc". iSplit; [done|].
+ replace (x + 1 + 1)%Z with (x+2)%Z by lia. iFrame.
+ rewrite -iProto_roundtrip_ref_rec2_unfold.
+ iApply "IH".
+ Qed.
+
+ Lemma roundtrip_ref_rec_prog_spec :
+ {{{ True }}} roundtrip_ref_rec_prog #() {{{ RET #42 ; True }}}.
+ Proof using chanG0.
+ iIntros (Φ) "_ HΦ". wp_lam.
+ wp_new_chan iProto_roundtrip_ref_rec with iProto_roundtrip_ref_rec_consistent
+ as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
+ wp_smart_apply (wp_fork with "[Hc1]").
+ { iIntros "!>". wp_pure _. iLöb as "IH".
+ wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
+ do 2 wp_pure _. by iApply "IH". }
+ wp_smart_apply (wp_fork with "[Hc2]").
+ { iIntros "!>". wp_pure _. iLöb as "IH".
+ wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
+ do 2 wp_pure _. by iApply "IH". }
+ wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl".
+ wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
+ by iApply "HΦ".
+ Qed.
+
+End roundtrip_ref_rec.
+
+Definition smuggle_ref_prog : val :=
+ λ: <>,
+ let: "cs" := new_chan #3 in
+ let: "c0" := get_chan "cs" #0 in
+ let: "c1" := get_chan "cs" #1 in
+ let: "c2" := get_chan "cs" #2 in
+ Fork (send "c1" #2 (recv "c1" #0);; send "c1" #0 (recv "c1" #2));;
+ Fork (let: "l" := recv "c2" #1 in "l" <- !"l" + #2;; send "c2" #1 #());;
+ let: "l" := ref #40 in
+ send "c0" #1 "l";; recv "c0" #1;; !"l".
+
+Section smuggle_ref.
+ Context `{!heapGS Σ, !chanG Σ}.
+
+ Definition iProto_smuggle_ref : list (iProto Σ) :=
+ [(<(Send, 1) @ (l:loc) (x:Z)> MSG #l {{ l ↦ #x }} ;
+ <(Recv,1)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto;
+ (<(Recv, 0) @ (v:val)> MSG v ; <(Send,2)> MSG v ;
+ <(Recv, 2)> MSG #(); <(Send,0)> MSG #() ; END)%proto;
+ (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ l ↦ #x }} ;
+ <(Send,1)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto].
+
+ Lemma iProto_smuggle_ref_consistent :
+ ⊢ iProto_consistent iProto_smuggle_ref.
+ Proof. rewrite /iProto_smuggle_ref. iProto_consistent_take_steps. Qed.
+
+ Lemma smuggle_ref_spec :
+ {{{ True }}} smuggle_ref_prog #() {{{ RET #42 ; True }}}.
+ Proof using chanG0 heapGS0 Σ.
+ iIntros (Φ) "_ HΦ". wp_lam.
+ wp_new_chan iProto_smuggle_ref with iProto_smuggle_ref_consistent
+ as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
+ wp_smart_apply (wp_fork with "[Hc1]").
+ { iIntros "!>". wp_recv (v) as "_". wp_send with "[//]".
+ wp_recv as "_". by wp_send with "[//]". }
+ wp_smart_apply (wp_fork with "[Hc2]").
+ { iIntros "!>". wp_recv (l x) as "Hl". wp_load. wp_store.
+ by wp_send with "[$Hl]". }
+ wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
+ by iApply "HΦ".
+ Qed.
+
+End smuggle_ref.
+
+Section parallel.
+ Context `{!heapGS Σ}.
+
+ (**
+ 0
+ / \
+ 1 2
+ | |
+ 3 4
+ \ /
+ 0
+ *)
+
+ Definition iProto_parallel : list (iProto Σ) :=
+ [(<(Send, 1) @ (x1:Z)> MSG #x1 ;
+ <(Send, 2) @ (x2:Z)> MSG #x2 ;
+ <(Recv, 3) @ (y1:Z)> MSG #(x1+y1);
+ <(Recv, 4) @ (y2:Z)> MSG #(x2+y2); END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ;
+ <(Send, 3) @ (y:Z)> MSG #(x+y); END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ;
+ <(Send, 4) @ (y:Z)> MSG #(x+y) ; END)%proto;
+ (<(Recv, 1) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x; END)%proto;
+ (<(Recv, 2) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x ; END)%proto].
+
+ Lemma iProto_parallel_consistent :
+ ⊢ iProto_consistent iProto_parallel.
+ Proof. rewrite /iProto_parallel. iProto_consistent_take_steps. Qed.
+
+End parallel.
+
+Section forwarder.
+ Context `{!heapGS Σ}.
+
+ (**
+
+ 0
+ / | \
+ / | \
+ | 1 |
+ \ / \ /
+ 2 3
+
+ *)
+
+ Definition iProto_forwarder : list (iProto Σ) :=
+ [(<(Send, 1) @ (x:Z)> MSG #x ;
+ <(Send, 1) @ (b:bool)> MSG #b ;
+ <(Recv, if b then 2 else 3) > MSG #x ; END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ;
+ <(Recv, 0) @ (b:bool)> MSG #b;
+ <(Send, if b then 2 else 3)> MSG #x ; END)%proto;
+ (<(Recv, 1) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x ; END)%proto;
+ (<(Recv, 1) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x ; END)%proto].
+
+ Lemma iProto_forwarder_consistent :
+ ⊢ iProto_consistent iProto_forwarder.
+ Proof.
+ rewrite /iProto_forwarder.
+ iProto_consistent_take_steps.
+ destruct x0; iProto_consistent_take_steps.
+ Qed.
+
+End forwarder.
+
+Section forwarder_rec.
+ Context `{!heapGS Σ}.
+
+ (**
+ 0
+ / | \
+ / | \
+ | 1 |
+ \ / \ /
+ 2 3
+ *)
+
+ Definition iProto_forwarder_rec_0_aux (rec : iProto Σ) : iProto Σ :=
+ (<(Send, 1) @ (x:Z)> MSG #x ;
+ <(Send, 1) @ (b:bool)> MSG #b ;
+ <(Recv, if b then 2 else 3) > MSG #x ; rec)%proto.
+ Instance iProto_forwarder_rec_0_contractive :
+ Contractive iProto_forwarder_rec_0_aux.
+ Proof. solve_proto_contractive. Qed.
+ Definition iProto_forwarder_rec_0 :=
+ fixpoint iProto_forwarder_rec_0_aux.
+ Lemma iProto_forwarder_rec_0_unfold :
+ iProto_forwarder_rec_0 ≡
+ (iProto_forwarder_rec_0_aux iProto_forwarder_rec_0).
+ Proof. apply (fixpoint_unfold _). Qed.
+
+ Definition iProto_forwarder_rec_1_aux (rec : iProto Σ) : iProto Σ :=
+ (<(Recv, 0) @ (x:Z)> MSG #x ;
+ <(Recv, 0) @ (b:bool)> MSG #b;
+ if b
+ then <(Send,2)> MSG #x ; rec
+ else <(Send,3)> MSG #x ; rec)%proto.
+ Instance iProto_forwarder_rec_1_contractive :
+ Contractive iProto_forwarder_rec_1_aux.
+ Proof. solve_proto_contractive. Qed.
+ Definition iProto_forwarder_rec_1 :=
+ fixpoint iProto_forwarder_rec_1_aux.
+ Lemma iProto_forwarder_rec_1_unfold :
+ iProto_forwarder_rec_1 ≡
+ (iProto_forwarder_rec_1_aux iProto_forwarder_rec_1).
+ Proof. apply (fixpoint_unfold _). Qed.
+
+ Definition iProto_forwarder_rec_n_aux (rec : iProto Σ) : iProto Σ :=
+ (<(Recv, 1) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x ; rec)%proto.
+ Instance iProto_forwarder_rec_n_contractive :
+ Contractive iProto_forwarder_rec_n_aux.
+ Proof. solve_proto_contractive. Qed.
+ Definition iProto_forwarder_rec_n :=
+ fixpoint iProto_forwarder_rec_n_aux.
+ Lemma iProto_forwarder_rec_n_unfold :
+ iProto_forwarder_rec_n ≡
+ (iProto_forwarder_rec_n_aux iProto_forwarder_rec_n).
+ Proof. apply (fixpoint_unfold _). Qed.
+
+ Definition iProto_forwarder_rec : list (iProto Σ) :=
+ [iProto_forwarder_rec_0;
+ iProto_forwarder_rec_1;
+ iProto_forwarder_rec_n;
+ iProto_forwarder_rec_n].
+
+ Lemma iProto_forwarder_rec_consistent :
+ ⊢ iProto_consistent iProto_forwarder_rec.
+ Proof.
+ iLöb as "IH".
+ rewrite /iProto_forwarder_rec.
+ iEval (rewrite iProto_forwarder_rec_0_unfold).
+ iEval (rewrite iProto_forwarder_rec_1_unfold).
+ iEval (rewrite iProto_forwarder_rec_n_unfold).
+ iProto_consistent_take_step.
+ iIntros (x) "_". iExists _. iSplit; [done|]. iSplit; [done|].
+ iProto_consistent_take_step.
+ iIntros ([]) "_".
+ - iExists _. iSplit; [done|]. iSplit; [done|].
+ iProto_consistent_take_step.
+ iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
+ iNext.
+ iEval (rewrite iProto_forwarder_rec_1_unfold).
+ iEval (rewrite iProto_forwarder_rec_n_unfold).
+ iProto_consistent_take_step.
+ iIntros "_". iSplit; [done|]. iSplit; [done|].
+ iEval (rewrite -iProto_forwarder_rec_1_unfold).
+ iEval (rewrite -iProto_forwarder_rec_n_unfold).
+ iEval (rewrite -iProto_forwarder_rec_n_unfold).
+ iApply "IH".
+ - iExists _. iSplit; [done|]. iSplit; [done|].
+ iProto_consistent_take_step.
+ iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
+ iNext.
+ iEval (rewrite iProto_forwarder_rec_1_unfold).
+ iEval (rewrite iProto_forwarder_rec_n_unfold).
+ iProto_consistent_take_step.
+ iIntros "_". iSplit; [done|]. iSplit; [done|].
+ iEval (rewrite -iProto_forwarder_rec_1_unfold).
+ iEval (rewrite -iProto_forwarder_rec_n_unfold).
+ iEval (rewrite -iProto_forwarder_rec_n_unfold).
+ iApply "IH".
+ Qed.
+
+End forwarder_rec.
diff --git a/multris/examples/leader_election.v b/multris/examples/leader_election.v
new file mode 100644
index 0000000000000000000000000000000000000000..c8336954d574ac07c7e479e00232b4c9d1164078
--- /dev/null
+++ b/multris/examples/leader_election.v
@@ -0,0 +1,356 @@
+From iris.heap_lang Require Import adequacy.
+From iris.heap_lang.lib Require Import assert.
+From multris.channel Require Import proofmode.
+
+(** Inspired by https://en.wikipedia.org/wiki/Chang_and_Roberts_algorithm *)
+
+Definition process : val :=
+ rec: "go" "c" "idl" "id" "idr" "isp" :=
+ if: recv "c" "idr"
+ then let: "id'" := recv "c" "idr" in
+ if: "id" < "id'" (** Case 1 *)
+ then send "c" "idl" #true;; send "c" "idl" "id'";;
+ "go" "c" "idl" "id" "idr" #true
+ else if: "id" = "id'" (** Case 4 *)
+ then send "c" "idl" #false;; send "c" "idl" "id";;
+ "go" "c" "idl" "id" "idr" #false
+ else if: "isp" (** Case 3 *)
+ then "go" "c" "idl" "id" "idr" "isp" (** Case 2 *)
+ else send "c" "idl" #true;; send "c" "idl" "id";;
+ "go" "c" "idl" "id" "idr" #true
+ else let: "id'" := recv "c" "idr" in
+ if: "id" = "id'" then "id'"
+ else send "c" "idl" #false;; send "c" "idl" "id'";; "id'".
+
+Definition init : val :=
+ λ: "c" "idl" "id" "idr",
+ send "c" "idl" #true;; send "c" "idl" "id";;
+ process "c" "idl" "id" "idr" #true.
+
+Notation iProto_choice a p1 p2 :=
+ (<a @ (b : bool)> MSG #b; if b then p1 else p2)%proto.
+
+Section ring_leader_election_protocols.
+ Context `{!heapGS Σ, chanG Σ}.
+
+ Definition my_recv_prot (il i ir : nat) (P : iProp Σ) (p : nat → iProto Σ)
+ (rec : bool -d> iProto Σ) : bool -d> iProto Σ :=
+ λ (isp:bool),
+ iProto_choice (Recv,ir)
+ (<(Recv,ir) @ (i':nat)> MSG #i';
+ if bool_decide (i < i')
+ then <(Send,il)> MSG #true ; <(Send,il)> MSG #i' ; rec true
+ else if bool_decide (i = i')
+ then <(Send,il)> MSG #false ; <(Send, il)> MSG #i ; rec false
+ else if isp then rec isp
+ else <(Send,il)> MSG #true ; <(Send,il)> MSG #i ; rec true)%proto
+ (<(Recv,ir) @ (i':nat)> MSG #i'
+ {{ if bool_decide (i = i') then P else True%I }};
+ if (bool_decide (i = i')) then p i
+ else <(Send,il)> MSG #false; <(Send,il)> MSG #i'; p i')%proto.
+
+ Instance rle_prot_aux_contractive il i ir P p :
+ Contractive (my_recv_prot il i ir P p).
+ Proof. rewrite /my_recv_prot. solve_proto_contractive. Qed.
+ Definition rle_prot il i ir P p := fixpoint (my_recv_prot il i ir P p).
+ Instance rle_prot_unfold il i ir isp P p :
+ ProtoUnfold (rle_prot il i ir P p isp)
+ (my_recv_prot il i ir P p (rle_prot il i ir P p) isp).
+ Proof. apply proto_unfold_eq, (fixpoint_unfold (my_recv_prot il i ir P p)). Qed.
+ Lemma rle_prot_unfold' il i ir isp P p :
+ (rle_prot il i ir P p isp) ≡
+ (my_recv_prot il i ir P p (rle_prot il i ir P p) isp).
+ Proof. apply (fixpoint_unfold (my_recv_prot il i ir P p)). Qed.
+
+ Definition rle_preprot (il i ir : nat) P p : iProto Σ :=
+ (<(Send, il)> MSG #true; <(Send, il)> MSG #i {{ P }} ;
+ rle_prot il i ir P p true)%proto.
+
+ Lemma process_spec il i ir P p c (isp:bool) :
+ {{{ c ↣ (rle_prot il i ir P p isp) }}}
+ process c #il #i #ir #isp
+ {{{ i', RET #i'; c ↣ p i' ∗ if (bool_decide (i = i')) then P else True%I }}}.
+ Proof.
+ iIntros (Φ) "Hc HΦ".
+ iLöb as "IH" forall (Φ isp).
+ wp_lam. wp_recv (b) as "_".
+ destruct b.
+ - wp_recv (i') as "_".
+ wp_pures. case_bool_decide as Hlt.
+ { case_bool_decide; [|lia].
+ wp_send with "[//]". wp_send with "[//]".
+ wp_smart_apply ("IH" with "Hc HΦ"). }
+ case_bool_decide as Hlt2.
+ { case_bool_decide; [lia|]. wp_pures. case_bool_decide; [|simplify_eq;lia].
+ wp_send with "[//]". wp_send with "[//]".
+ wp_smart_apply ("IH" with "Hc HΦ"). }
+ case_bool_decide; [lia|].
+ wp_pures. case_bool_decide; [simplify_eq;lia|]. wp_pures.
+ destruct isp; [by wp_smart_apply ("IH" with "Hc HΦ")|].
+ wp_send with "[//]". wp_send with "[//]".
+ wp_smart_apply ("IH" with "Hc HΦ").
+ - wp_recv (id') as "HP". wp_pures.
+ case_bool_decide as Hlt.
+ { case_bool_decide; [|simplify_eq;lia].
+ wp_pures. subst. iApply "HΦ". iFrame. by case_bool_decide. }
+ case_bool_decide; [simplify_eq;lia|].
+ wp_send with "[//]". wp_send with "[//]". wp_pures. iApply "HΦ".
+ iFrame. by case_bool_decide; [simplify_eq;lia|].
+ Qed.
+
+ Lemma init_spec c il i ir p P :
+ {{{ c ↣ rle_preprot il i ir P p ∗ P }}}
+ init c #il #i #ir
+ {{{ i', RET #i'; c ↣ p i' ∗ if (bool_decide (i = i')) then P else True%I }}}.
+ Proof.
+ iIntros (Φ) "[Hc HP] HΦ". wp_lam. wp_send with "[//]". wp_send with "[HP//]".
+ wp_smart_apply (process_spec with "Hc HΦ").
+ Qed.
+
+End ring_leader_election_protocols.
+
+Definition rle_ref_prog : val :=
+ λ: <>,
+ let: "l" := ref #42 in
+ let: "cs" := new_chan #4 in
+ let: "c0" := get_chan "cs" #0 in
+ let: "c1" := get_chan "cs" #1 in
+ let: "c2" := get_chan "cs" #2 in
+ let: "c3" := get_chan "cs" #3 in
+ Fork (let: "id_max" := process "c1" #0 #1 #2 #false in
+ if: "id_max" = #1 then Free "l" else #());;
+ Fork (let: "id_max" := process "c2" #1 #2 #3 #false in
+ if: "id_max" = #2 then Free "l" else #());;
+ Fork (let: "id_max" := process "c3" #2 #3 #0 #false in
+ if: "id_max" = #3 then Free "l" else #());;
+ let: "id_max" := init "c0" #3 #0 #1 in
+ if: "id_max" = #0 then Free "l" else #().
+
+Section rle_ref_prog_proof.
+ Context `{!heapGS Σ, chanG Σ}.
+
+ Definition rle_ref_prog_prot_pool P : list (iProto Σ) :=
+ [rle_preprot 3 0 1 P (λ id_max, END)%proto;
+ rle_prot 0 1 2 P (λ id_max, END)%proto false;
+ rle_prot 1 2 3 P (λ id_max, END)%proto false;
+ rle_prot 2 3 0 P (λ id_max, END)%proto false].
+
+ Lemma rle_ref_prog_prot_pool_consistent P :
+ ⊢ iProto_consistent (rle_ref_prog_prot_pool P).
+ Proof.
+ rewrite /rle_ref_prog_prot_pool /rle_preprot.
+ rewrite !rle_prot_unfold'.
+ iProto_consistent_take_steps.
+ case_bool_decide; try lia.
+ rewrite !rle_prot_unfold'.
+ iProto_consistent_take_steps.
+ case_bool_decide; try lia.
+ rewrite !rle_prot_unfold'.
+ iProto_consistent_take_steps.
+ case_bool_decide; try lia.
+ rewrite !rle_prot_unfold'.
+ iProto_consistent_take_steps.
+ Qed.
+
+ Lemma rle_ref_prog_spec :
+ {{{ True }}} rle_ref_prog #() {{{ RET #(); True }}}.
+ Proof.
+ iIntros (Φ) "_ HΦ". wp_lam.
+ wp_alloc l as "Hl".
+ wp_new_chan (rle_ref_prog_prot_pool (l ↦ #42))
+ with rle_ref_prog_prot_pool_consistent
+ as (c0 c1 c2 c3) "Hc0" "Hc1" "Hc2" "Hc3".
+ wp_smart_apply (wp_fork with "[Hc1]").
+ { iIntros "!>". wp_smart_apply (process_spec with "Hc1").
+ iIntros (i') "[_ Hl]". wp_pures. case_bool_decide.
+ - case_bool_decide; [|simplify_eq; lia]. by wp_free.
+ - case_bool_decide; [simplify_eq; lia|]. by wp_pures. }
+ wp_smart_apply (wp_fork with "[Hc2]").
+ { iIntros "!>". wp_smart_apply (process_spec with "Hc2").
+ iIntros (i') "[_ Hl]". wp_pures. case_bool_decide.
+ - case_bool_decide; [|simplify_eq; lia]. by wp_free.
+ - case_bool_decide; [simplify_eq; lia|]. by wp_pures. }
+ wp_smart_apply (wp_fork with "[Hc3]").
+ { iIntros "!>". wp_smart_apply (process_spec with "Hc3").
+ iIntros (i') "[_ Hl]". wp_pures. case_bool_decide.
+ - case_bool_decide; [|simplify_eq; lia]. by wp_free.
+ - case_bool_decide; [simplify_eq; lia|]. by wp_pures. }
+ wp_smart_apply (init_spec with "[$Hc0 $Hl]").
+ iIntros (i') "[_ Hl]". wp_pures. case_bool_decide.
+ - case_bool_decide; [|simplify_eq; lia]. wp_free. by iApply "HΦ".
+ - case_bool_decide; [simplify_eq; lia|]. wp_pures. by iApply "HΦ".
+ Qed.
+
+End rle_ref_prog_proof.
+
+Lemma rle_ref_prog_adequate :
+ adequate NotStuck (rle_ref_prog #()) ({|heap := ∅; used_proph_id := ∅|})
+ (λ _ _, True).
+Proof.
+ apply (heap_adequacy #[heapΣ; chanΣ]).
+ iIntros (Σ) "H". by iApply rle_ref_prog_spec.
+Qed.
+
+Definition relay : val :=
+ λ: "c" "c'" "idl" "id" "idr" "id_max",
+ if: "id" = "id_max" then
+ send "c'" #0 "id_max";; send "c" "idl" #();; recv "c" "idr"
+ else
+ recv "c" "idr";; send "c'" #0 "id_max";; send "c" "idl" #().
+
+Definition rle_del_prog : val :=
+ λ: <>,
+ let: "cs'" := new_chan #2 in
+ let: "c0'" := get_chan "cs'" #0 in
+ let: "c1'" := get_chan "cs'" #1 in
+ Fork (let: "id_max" := recv "c0'" #1 in
+ (rec: "f" <> :=
+ let: "id'" := recv "c0'" #1 in
+ assert: ("id'" = "id_max");; "f" #()) #());;
+ let: "cs" := new_chan #4 in
+ let: "c0" := get_chan "cs" #0 in
+ let: "c1" := get_chan "cs" #1 in
+ let: "c2" := get_chan "cs" #2 in
+ let: "c3" := get_chan "cs" #3 in
+ Fork (let: "id_max" := process "c1" #0 #1 #2 #false in
+ relay "c1" "c1'" #0 #1 #2 "id_max");;
+ Fork (let: "id_max" := process "c2" #1 #2 #3 #false in
+ relay "c2" "c1'" #1 #2 #3 "id_max");;
+ Fork (let: "id_max" := process "c3" #2 #3 #0 #false in
+ relay "c3" "c1'" #2 #3 #0 "id_max");;
+ let: "id_max" := init "c0" #3 #0 #1 in
+ relay "c0" "c1'" #3 #0 #1 "id_max".
+
+Section rle_del_prog_proof.
+ Context `{!heapGS Σ, chanG Σ}.
+
+ Definition relay_del_prot (P:iProp Σ) (il i ir i_max : nat) : iProto Σ :=
+ if bool_decide (i = i_max) then
+ (<(Send,il)> MSG #() {{ P }} ; <(Recv,ir)> MSG #() {{ P }}; END)%proto
+ else
+ (<(Recv,ir)> MSG #() {{ P }} ; <(Send,il)> MSG #() {{ P }}; END)%proto.
+
+ Definition relay_send_aux (id : nat) (rec : iProto Σ) : iProto Σ :=
+ (<(Send,0)> MSG #id ; rec)%proto.
+ Instance relay_send_aux_contractive i : Contractive (relay_send_aux i).
+ Proof. solve_proto_contractive. Qed.
+ Definition relay_send_prot i := fixpoint (relay_send_aux i).
+ Instance relay_send_prot_unfold i :
+ ProtoUnfold (relay_send_prot i) (relay_send_aux i (relay_send_prot i)).
+ Proof. apply proto_unfold_eq, (fixpoint_unfold (relay_send_aux i)). Qed.
+ Lemma relay_send_prot_unfold' i :
+ (relay_send_prot i) ≡
+ (relay_send_aux i (relay_send_prot i)).
+ Proof. apply (fixpoint_unfold (relay_send_aux i)). Qed.
+
+ Definition relay_send_preprot : iProto Σ :=
+ (<(Send,0) @ (i_max:nat)> MSG #i_max ; relay_send_prot i_max)%proto.
+
+ Definition relay_recv_aux (id : nat) (rec : iProto Σ) : iProto Σ :=
+ (<(Recv,1)> MSG #id ; rec)%proto.
+ Instance relay_recv_aux_contractive i : Contractive (relay_recv_aux i).
+ Proof. solve_proto_contractive. Qed.
+ Definition relay_recv_prot i := fixpoint (relay_recv_aux i).
+ Instance relay_recv_prot_unfold i :
+ ProtoUnfold (relay_recv_prot i) (relay_recv_aux i (relay_recv_prot i)).
+ Proof. apply proto_unfold_eq, (fixpoint_unfold (relay_recv_aux i)). Qed.
+ Lemma relay_recv_prot_unfold' i :
+ (relay_recv_prot i) ≡
+ (relay_recv_aux i (relay_recv_prot i)).
+ Proof. apply (fixpoint_unfold (relay_recv_aux i)). Qed.
+ Definition relay_recv_preprot : iProto Σ :=
+ (<(Recv,1) @ (i_max:nat)> MSG #i_max ; relay_recv_prot i_max)%proto.
+
+ Definition rle_del_prog_prot_pool P Φ : list (iProto Σ) :=
+ [rle_preprot 3 0 1 P (λ id_max, relay_del_prot (Φ id_max) 3 0 1 id_max);
+ rle_prot 0 1 2 P (λ id_max, relay_del_prot (Φ id_max) 0 1 2 id_max) false;
+ rle_prot 1 2 3 P (λ id_max, relay_del_prot (Φ id_max) 1 2 3 id_max) false;
+ rle_prot 2 3 0 P (λ id_max, relay_del_prot (Φ id_max) 2 3 0 id_max) false].
+
+ Lemma rle_del_prog_prot_pool_consistent P Φ :
+ ⊢ iProto_consistent (rle_del_prog_prot_pool P Φ).
+ Proof.
+ rewrite /rle_del_prog_prot_pool /rle_preprot.
+ rewrite !rle_prot_unfold'.
+ iProto_consistent_take_steps.
+ case_bool_decide; try lia.
+ rewrite !rle_prot_unfold'.
+ iProto_consistent_take_steps.
+ case_bool_decide; try lia.
+ rewrite !rle_prot_unfold'.
+ iProto_consistent_take_steps.
+ case_bool_decide; try lia.
+ rewrite !rle_prot_unfold'.
+ iProto_consistent_take_steps.
+ Qed.
+
+ Definition rle_del_prog_prot_pool' : list (iProto Σ) :=
+ [relay_recv_preprot; relay_send_preprot].
+
+ Lemma rle_del_prog_prot_pool_consistent' :
+ ⊢ iProto_consistent (rle_del_prog_prot_pool').
+ Proof.
+ rewrite /rle_del_prog_prot_pool'.
+ iProto_consistent_take_steps.
+ iLöb as "IH".
+ iEval (rewrite relay_recv_prot_unfold').
+ iEval (rewrite relay_send_prot_unfold').
+ iProto_consistent_take_steps.
+ done.
+ Qed.
+
+ Lemma relay_spec c c' il i ir i_max :
+ {{{ c ↣ relay_del_prot (c' ↣ relay_send_prot i_max) il i ir i_max ∗
+ if (bool_decide (i = i_max)) then c' ↣ relay_send_preprot else True%I }}}
+ relay c c' #il #i #ir #i_max
+ {{{ RET #(); True }}}.
+ Proof.
+ iIntros (Φ) "[Hc Hc'] HΦ". wp_lam.
+ rewrite /relay_del_prot.
+ wp_pures. case_bool_decide.
+ - simplify_eq. wp_pures.
+ case_bool_decide; [|simplify_eq;lia].
+ wp_send with "[//]". wp_send with "[Hc'//]". wp_recv as "Hc'".
+ by iApply "HΦ".
+ - case_bool_decide; [simplify_eq;lia|].
+ iClear "Hc'". wp_recv as "Hc'".
+ wp_send with "[//]". wp_send with "[Hc'//]". by iApply "HΦ".
+ Qed.
+
+ Lemma rle_del_prog_spec :
+ {{{ True }}} rle_del_prog #() {{{ RET #(); True }}}.
+ Proof.
+ iIntros (Φ) "_ HΦ". wp_lam.
+ wp_new_chan rle_del_prog_prot_pool' with rle_del_prog_prot_pool_consistent'
+ as (c0' c1') "Hc0'" "Hc1'".
+ wp_smart_apply (wp_fork with "[Hc0']").
+ { iIntros "!>". wp_recv (i_max) as "_". wp_pures.
+ iLöb as "IH". wp_recv as "_". wp_smart_apply wp_assert.
+ wp_pures. iModIntro. iSplit; [iPureIntro; f_equiv; by case_bool_decide|].
+ iIntros "!>". wp_pures. by iApply "IH". }
+ wp_new_chan (rle_del_prog_prot_pool (c1' ↣ relay_send_preprot)
+ (λ i_max, c1' ↣ relay_send_prot i_max))
+ with rle_del_prog_prot_pool_consistent
+ as (c0 c1 c2 c3) "Hc0" "Hc1" "Hc2" "Hc3".
+ wp_smart_apply (wp_fork with "[Hc1]").
+ { iIntros "!>". wp_smart_apply (process_spec with "Hc1").
+ iIntros (i') "Hc1". by wp_smart_apply (relay_spec with "[$Hc1]"). }
+ wp_smart_apply (wp_fork with "[Hc2]").
+ { iIntros "!>". wp_smart_apply (process_spec with "Hc2").
+ iIntros (i') "Hc2". by wp_smart_apply (relay_spec with "[$Hc2]"). }
+ wp_smart_apply (wp_fork with "[Hc3]").
+ { iIntros "!>". wp_smart_apply (process_spec with "Hc3").
+ iIntros (i') "Hc3". by wp_smart_apply (relay_spec with "[$Hc3]"). }
+ wp_smart_apply (init_spec with "[$Hc0 $Hc1']").
+ iIntros (i') "Hc0". by wp_smart_apply (relay_spec with "[$Hc0]").
+ Qed.
+
+End rle_del_prog_proof.
+
+Lemma rle_del_prog_adequate :
+ adequate NotStuck (rle_del_prog #()) ({|heap := ∅; used_proph_id := ∅|})
+ (λ _ _, True).
+Proof.
+ apply (heap_adequacy #[heapΣ; chanΣ]).
+ iIntros (Σ) "H". by iApply rle_del_prog_spec.
+Qed.
diff --git a/multris/examples/three_buyer.v b/multris/examples/three_buyer.v
new file mode 100644
index 0000000000000000000000000000000000000000..a4d24c465e5d4874d88f5b56a71e8717715e1efa
--- /dev/null
+++ b/multris/examples/three_buyer.v
@@ -0,0 +1,198 @@
+From multris.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" "cb2'" "b3",
+ 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 send "cb2'" "b3" "quote";;
+ send "cb2'" "b3" ("contrib" + #100);;
+ send "cb2'" "b3" "cb2".
+
+Definition buyer3_prog : val :=
+ λ: "cb3" "b1" "b2'" "s",
+ let: "quote" := recv "cb3" "b2'" in
+ let: "contrib" := recv "cb3" "b2'" in
+ let: "cb2" := recv "cb3" "b2'" in
+ if: ("quote" - "contrib" < #100)
+ then send "cb2" "s" #true;; send "cb2" "b1" #true;;
+ recv "cb2" "s"
+ else #().
+
+Definition three_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
+ let: "cs'" := new_chan #2 in
+ let: "b2'" := get_chan "cs'" #0 in
+ let: "b3" := get_chan "cs'" #1 in
+ Fork (seller_prog "s" #0 #2);;
+ Fork (buyer2_prog "b2" #0 #1 "b2'" #1);;
+ Fork (buyer3_prog "b3" #0 #1 #0);;
+ buyer1_prog "b1" #1 #2.
+
+Section three_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.
+
+ Definition buyer2_prot' b3 b1 s : iProto Σ :=
+ (<(Send, b3) @ (quote:Z)> MSG #quote ;
+ <(Send, b3) @ (contrib:Z)> MSG #contrib ;
+ <(Send, b3) @ (c:val)> MSG c
+ {{ c ↣ (<(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 }} ;
+ END)%proto.
+
+ Lemma buyer2_spec c b1 s c' b3 :
+ {{{ c ↣ buyer2_prot b1 s ∗ c' ↣ buyer2_prot' b3 b1 s }}}
+ buyer2_prog c #b1 #s c' #b3
+ {{{ b, RET #b; True }}}.
+ Proof.
+ iIntros (Φ) "[Hc 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_send with "[//]". wp_send with "[//]". wp_send with "[Hc//]".
+ by iApply "HΦ".
+ Qed.
+
+ Definition buyer3_prot b1 b2' s : iProto Σ :=
+ (<(Recv, b2') @ (quote:Z)> MSG #quote ;
+ <(Recv, b2') @ (contrib:Z)> MSG #contrib ;
+ <(Recv, b2') @ (c:val)> MSG c
+ {{ c ↣ (<(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 }} ;
+ END)%proto.
+
+ Lemma buyer3_spec c b1 b2' s :
+ {{{ c ↣ buyer3_prot b1 b2' s }}}
+ buyer3_prog c #b1 #b2' #s
+ {{{ b, RET #b; True }}}.
+ Proof.
+ iIntros (Φ) "Hc HΦ". wp_lam. wp_pures.
+ wp_recv (quote) as "_".
+ wp_recv (contrib) as "_".
+ wp_recv (c') as "Hc'".
+ 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.
+
+ Definition three_buyer_prot : list (iProto Σ) :=
+ [buyer2_prot' 1 0 1; buyer3_prot 0 1 0].
+
+ Lemma three_buyer_prot_consistent :
+ ⊢ iProto_consistent three_buyer_prot.
+ Proof. rewrite /three_buyer_prot. iProto_consistent_take_steps. Qed.
+
+ Lemma three_buyer_spec :
+ {{{ True }}}
+ three_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_pures.
+ wp_new_chan three_buyer_prot with three_buyer_prot_consistent
+ as (??) "Hcb2'" "Hcb3".
+ wp_smart_apply (wp_fork with "[Hcs]").
+ { by iApply (seller_spec with "Hcs"). }
+ wp_smart_apply (wp_fork with "[Hcb2 Hcb2']").
+ { by iApply (buyer2_spec with "[$Hcb2 $Hcb2']"). }
+ wp_smart_apply (wp_fork with "[Hcb3]").
+ { by iApply (buyer3_spec with "Hcb3"). }
+ wp_smart_apply (buyer1_spec with "Hcb1").
+ by iApply "HΦ".
+ Qed.
+
+End three_buyer.
diff --git a/multris/examples/two_buyer.v b/multris/examples/two_buyer.v
new file mode 100644
index 0000000000000000000000000000000000000000..a3179243a0ed5368fc6195835f639951775e7ff9
--- /dev/null
+++ b/multris/examples/two_buyer.v
@@ -0,0 +1,133 @@
+From multris.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.
diff --git a/multris/utils/cofe_solver_2.v b/multris/utils/cofe_solver_2.v
new file mode 100644
index 0000000000000000000000000000000000000000..7a2425ba1241530b55ba7d0572cb276d271f7728
--- /dev/null
+++ b/multris/utils/cofe_solver_2.v
@@ -0,0 +1,88 @@
+From iris.algebra Require Import cofe_solver.
+
+(** Version of the cofe_solver for a parametrized functor. Generalize and move
+to Iris. *)
+Record solution_2 (F : ofe → oFunctor) := Solution2 {
+ solution_2_car : ∀ An `{!Cofe An} A `{!Cofe A}, ofe;
+ solution_2_cofe `{!Cofe An, !Cofe A} : Cofe (solution_2_car An A);
+ solution_2_iso `{!Cofe An, !Cofe A} :>
+ ofe_iso (oFunctor_apply (F A) (solution_2_car A An)) (solution_2_car An A);
+}.
+Arguments solution_2_car {F}.
+Global Existing Instance solution_2_cofe.
+
+Section cofe_solver_2.
+ Context (F : ofe → oFunctor).
+ Context `{Fcontr : !∀ T, oFunctorContractive (F T)}.
+ Context `{Fcofe : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
+ Context `{Finh : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
+ Notation map := (oFunctor_map (F _)).
+
+ Definition F_2 (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : oFunctor :=
+ oFunctor_oFunctor_compose (F A) (F An).
+
+ Definition T_result `{!Cofe An, !Cofe A} : solution (F_2 An A) := solver.result _.
+ Definition T (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : ofe :=
+ T_result (An:=An) (A:=A).
+ Instance T_cofe `{!Cofe An, !Cofe A} : Cofe (T An A) := _.
+ Instance T_inhabited `{!Cofe An, !Cofe A} : Inhabited (T An A) :=
+ populate (ofe_iso_1 T_result inhabitant).
+
+ Definition T_iso_fun_aux `{!Cofe An, !Cofe A}
+ (rec : prodO (oFunctor_apply (F An) (T An A) -n> T A An)
+ (T A An -n> oFunctor_apply (F An) (T An A))) :
+ prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+ (T An A -n> oFunctor_apply (F A) (T A An)) :=
+ (ofe_iso_1 T_result â—Ž map (rec.1,rec.2), map (rec.2,rec.1) â—Ž ofe_iso_2 T_result).
+ Instance T_iso_aux_fun_contractive `{!Cofe An, !Cofe A} :
+ Contractive (T_iso_fun_aux (An:=An) (A:=A)).
+ Proof. solve_contractive. Qed.
+
+ Definition T_iso_fun_aux_2 `{!Cofe An, !Cofe A}
+ (rec : prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+ (T An A -n> oFunctor_apply (F A) (T A An))) :
+ prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+ (T An A -n> oFunctor_apply (F A) (T A An)) :=
+ T_iso_fun_aux (T_iso_fun_aux rec).
+ Instance T_iso_fun_aux_2_contractive `{!Cofe An, !Cofe A} :
+ Contractive (T_iso_fun_aux_2 (An:=An) (A:=A)).
+ Proof.
+ intros n rec1 rec2 Hrec. rewrite /T_iso_fun_aux_2.
+ f_equiv. by apply T_iso_aux_fun_contractive.
+ Qed.
+
+ Definition T_iso_fun `{!Cofe An, !Cofe A} :
+ prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+ (T An A -n> oFunctor_apply (F A) (T A An)) :=
+ fixpoint T_iso_fun_aux_2.
+ Definition T_iso_fun_unfold_1 `{!Cofe An, !Cofe A} y :
+ T_iso_fun (An:=An) (A:=A).1 y ≡ (T_iso_fun_aux (T_iso_fun_aux T_iso_fun)).1 y.
+ Proof. apply (fixpoint_unfold T_iso_fun_aux_2). Qed.
+ Definition T_iso_fun_unfold_2 `{!Cofe An, !Cofe A} y :
+ T_iso_fun (An:=An) (A:=A).2 y ≡ (T_iso_fun_aux (T_iso_fun_aux T_iso_fun)).2 y.
+ Proof. apply (fixpoint_unfold T_iso_fun_aux_2). Qed.
+
+ Lemma result_2 : solution_2 F.
+ Proof using Fcontr Fcofe Finh.
+ apply (Solution2 F T _)=> An Hcn A Hc.
+ apply (OfeIso (T_iso_fun.1) (T_iso_fun.2)).
+ - intros y. apply equiv_dist=> n. revert An Hcn A Hc y.
+ induction (lt_wf n) as [n _ IH]; intros An ? A ? y.
+ rewrite T_iso_fun_unfold_1 T_iso_fun_unfold_2 /=.
+ rewrite -{2}(ofe_iso_12 T_result y). f_equiv.
+ rewrite -(oFunctor_map_id (F _) (ofe_iso_2 T_result y))
+ -!oFunctor_map_compose.
+ f_equiv; apply Fcontr; dist_later_intro as n' Hn'; split=> x /=;
+ rewrite ofe_iso_21 -{2}(oFunctor_map_id (F _) x)
+ -!oFunctor_map_compose; do 2 f_equiv; split=> z /=; auto.
+ - intros y. apply equiv_dist=> n. revert An Hcn A Hc y.
+ induction (lt_wf n) as [n _ IH]; intros An ? A ? y.
+ rewrite T_iso_fun_unfold_1 T_iso_fun_unfold_2 /= ofe_iso_21.
+ rewrite -(oFunctor_map_id (F _) y) -!oFunctor_map_compose.
+ f_equiv; apply Fcontr; dist_later_intro as n' Hn'; split=> x /=;
+ rewrite -{2}(ofe_iso_12 T_result x); f_equiv;
+ rewrite -{2}(oFunctor_map_id (F _) (ofe_iso_2 T_result x))
+ -!oFunctor_map_compose;
+ do 2 f_equiv; split=> z /=; auto.
+ Qed.
+End cofe_solver_2.
diff --git a/multris/utils/matrix.v b/multris/utils/matrix.v
new file mode 100644
index 0000000000000000000000000000000000000000..6a643600b5123217ab3561ba789c983692ad161e
--- /dev/null
+++ b/multris/utils/matrix.v
@@ -0,0 +1,159 @@
+From iris.bi Require Import big_op.
+From iris.heap_lang Require Export primitive_laws notation proofmode.
+
+Definition new_matrix : val :=
+ λ: "m" "n" "v", (AllocN ("m"*"n") "v","m","n").
+
+Definition pos (n i j : nat) : nat := i * n + j.
+Definition vpos : val := λ: "n" "i" "j", "i"*"n" + "j".
+
+Definition matrix_get : val :=
+ λ: "m" "i" "j",
+ let: "l" := Fst (Fst "m") in
+ let: "n" := Snd "m" in
+ "l" +â‚— vpos "n" "i" "j".
+
+Section with_Σ.
+ Context `{heapGS Σ}.
+
+ Definition is_matrix (v : val) (m n : nat)
+ (P : nat → nat → loc → iProp Σ) : iProp Σ :=
+ ∃ (l:loc),
+ ⌜v = PairV (PairV #l #m) #n⌠∗
+ [∗ list] i ↦ _ ∈ replicate m (),
+ [∗ list] j ↦ _ ∈ replicate n (),
+ P i j (l +â‚— pos n i j).
+
+ Lemma array_to_matrix_pre l n m v :
+ l ↦∗ replicate (n * m) v -∗
+ [∗ list] i ↦ _ ∈ replicate n (), (l +ₗ i*m) ↦∗ replicate m v.
+ Proof.
+ iIntros "Hl".
+ iInduction n as [|n] "IHn"; [done|].
+ replace (S n) with (n + 1) by lia.
+ replace ((n + 1) * m) with (n * m + m) by lia.
+ rewrite !replicate_add /= array_app=> /=.
+ iDestruct "Hl" as "[Hl Hls]".
+ iDestruct ("IHn" with "Hl") as "Hl".
+ iFrame=> /=.
+ rewrite Nat.add_0_r !length_replicate.
+ replace (Z.of_nat (n * m)) with (Z.of_nat n * Z.of_nat m)%Z by lia.
+ by iFrame.
+ Qed.
+
+ Lemma big_sepL_replicate_type {A B} n (x1 : A) (x2 : B) (P : nat → iProp Σ) :
+ ([∗ list] i ↦ _ ∈ replicate n x1, P i) ⊢
+ ([∗ list] i ↦ _ ∈ replicate n x2, P i).
+ Proof.
+ iIntros "H".
+ iInduction n as [|n] "IHn"; [done|].
+ replace (S n) with (n + 1) by lia.
+ rewrite !replicate_add /=. iDestruct "H" as "[H1 H2]".
+ iSplitL "H1"; [by iApply "IHn"|]=> /=.
+ by rewrite !length_replicate.
+ Qed.
+
+ Lemma array_to_matrix l m n v :
+ l ↦∗ replicate (m * n) v -∗
+ [∗ list] i ↦ _ ∈ replicate m (),
+ [∗ list] j ↦ _ ∈ replicate n (),
+ (l +ₗ pos n i j) ↦ v.
+ Proof.
+ iIntros "Hl".
+ iDestruct (array_to_matrix_pre with "Hl") as "Hl".
+ iApply (big_sepL_impl with "Hl").
+ iIntros "!>" (i ? _) "Hl".
+ iApply big_sepL_replicate_type.
+ iApply (big_sepL_impl with "Hl").
+ iIntros "!>" (j ? HSome) "Hl".
+ rewrite Loc.add_assoc.
+ replace (Z.of_nat i * Z.of_nat n + Z.of_nat j)%Z with
+ (Z.of_nat (i * n + j))%Z by lia.
+ by apply lookup_replicate in HSome as [-> _].
+ Qed.
+
+ Lemma new_matrix_spec E m n v P :
+ 0 < m → 0 < n →
+ {{{ [∗ list] i ↦ _ ∈ replicate m (), [∗ list] j ↦ _ ∈ replicate n (),
+ ∀ l, l ↦ v ={E}=∗ P i j l }}}
+ new_matrix #m #n v @ E
+ {{{ mat, RET mat; is_matrix mat m n P }}}.
+ Proof.
+ iIntros (Hm Hn Φ) "HP HΦ".
+ wp_lam. wp_pures.
+ wp_smart_apply wp_allocN; [lia|done|].
+ iIntros (l) "[Hl _]".
+ wp_pures. iApply "HΦ".
+ iExists _. iSplitR; [done|].
+ replace (Z.to_nat (Z.of_nat m * Z.of_nat n)) with (m * n) by lia.
+ iDestruct (array_to_matrix with "Hl") as "Hl".
+ iCombine "HP Hl" as "HPl".
+ rewrite -big_sepL_sep.
+ iApply big_sepL_fupd.
+ iApply (big_sepL_impl with "HPl").
+ iIntros "!>" (k x Hin) "H".
+ rewrite -big_sepL_sep.
+ iApply big_sepL_fupd.
+ iApply (big_sepL_impl with "H").
+ iIntros "!>" (k' x' Hin') "[HP Hl]".
+ by iApply "HP".
+ Qed.
+
+ Lemma matrix_sep m n l (P : _ → _ → _ → iProp Σ) i j :
+ i < m → j < n →
+ ([∗ list] i ↦ _ ∈ replicate m (),
+ [∗ list] j ↦ _ ∈ replicate n (),
+ P i j (l +ₗ pos n i j)) -∗
+ (P i j (l +ₗ pos n i j) ∗
+ (P i j (l +ₗ pos n i j) -∗
+ ([∗ list] i ↦ _ ∈ replicate m (),
+ [∗ list] j ↦ _ ∈ replicate n (),
+ P i j (l +â‚— pos n i j)))).
+ Proof.
+ iIntros (Hm Hn) "Hm".
+ iDestruct (big_sepL_impl with "Hm []") as "Hm".
+ { iIntros "!>" (k x HIn).
+ iApply (big_sepL_lookup_acc _ _ j ()).
+ by apply lookup_replicate. }
+ rewrite {1}(big_sepL_lookup_acc _ (replicate m ()) i ());
+ [|by apply lookup_replicate].
+ iDestruct "Hm" as "[[Hij Hi] Hm]".
+ iFrame.
+ iIntros "HP".
+ iDestruct ("Hm" with "[$Hi $HP]") as "Hm".
+ iApply (big_sepL_impl with "Hm").
+ iIntros "!>" (k x Hin).
+ iIntros "[Hm Hm']". iApply "Hm'". done.
+ Qed.
+
+ Lemma vpos_spec (n i j : nat) :
+ {{{ True }}} vpos #n #i #j {{{ RET #(pos n i j); True }}}.
+ Proof.
+ iIntros (Φ) "_ HΦ". wp_lam. wp_pures. rewrite /pos.
+ replace (Z.of_nat i * Z.of_nat n + Z.of_nat j)%Z with
+ (Z.of_nat (i * n + j)) by lia.
+ by iApply "HΦ".
+ Qed.
+
+ Lemma matrix_get_spec m n i j v P :
+ i < m → j < n →
+ {{{ is_matrix v m n P }}}
+ matrix_get v #i #j
+ {{{ l, RET #l; P i j l ∗ (P i j l -∗ is_matrix v m n P) }}}.
+ Proof.
+ iIntros (Hm Hn Φ) "Hm HΦ".
+ wp_lam.
+ iDestruct "Hm" as (l ->) "Hm".
+ wp_pures.
+ wp_smart_apply vpos_spec; [done|].
+ iIntros "_".
+ wp_pures.
+ iApply "HΦ".
+ iModIntro.
+ iDestruct (matrix_sep _ _ _ _ i j with "Hm") as "[$ Hm]"; [lia|lia|].
+ iIntros "H".
+ iDestruct ("Hm" with "H") as "Hm".
+ iExists _. iSplit; [done|]. iFrame.
+ Qed.
+
+End with_Σ.