diff --git a/_CoqProject b/_CoqProject
index bdcd5f1a7c161e6eba7b5f7f4575254cf5ce9952..330aec8252d15ca5be2cdef987318cd0b9f9f047 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -16,6 +16,8 @@ theories/utils/cofe_solver_2.v
theories/utils/switch.v
theories/channel/proto_model.v
theories/channel/proto.v
+theories/channel/multi_proto_model.v
+theories/channel/multi_proto.v
theories/channel/channel.v
theories/channel/proofmode.v
theories/examples/basics.v
diff --git a/theories/channel/multi_proto.v b/theories/channel/multi_proto.v
new file mode 100644
index 0000000000000000000000000000000000000000..c2fbacb380eb605069f03f7fb828646d8f6d39f3
--- /dev/null
+++ b/theories/channel/multi_proto.v
@@ -0,0 +1,1724 @@
+(** This file defines the core of the Actris logic: It defines dependent
+separation protocols and the various operations on it like dual, append, and
+branching.
+
+Dependent separation protocols [iProto] are defined by instantiating the
+parameterized version in [proto_model] with the type of propositions [iProp] of Iris.
+We define ways of constructing instances of the instantiated type via two
+constructors:
+- [iProto_end], which is identical to [proto_end].
+- [iProto_message], which takes an [action] and an [iMsg]. The type [iMsg] is a
+ sequence of binders [iMsg_exist], terminated by the payload constructed with
+ [iMsg_base] based on arguments [v], [P] and [prot], which are the value, the
+ carried proposition and the [iProto] tail, respectively.
+
+For convenience sake, we provide the following notations:
+- [END], which is simply [iProto_end].
+- [∃ x, m], which is [iMsg_exist] with argument [m].
+- [MSG v {{ P }}; prot], which is [iMsg_Base] with arguments [v], [P] and [prot].
+- [<a> m], which is [iProto_message] with arguments [a] and [m].
+
+We also include custom notation to more easily construct complete constructions:
+- [<a x1 .. xn> m], which is [<a> ∃ x1, .. ∃ xn, m].
+- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol.
+
+Futhermore, we define the following operations:
+- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa.
+- [iProto_app], which appends two protocols.
+
+In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
+the following inductive definition for asynchronous subtyping on session types:
+
+ p1 <: p2 p1 <: p2 p1 <: !B.p3 ?A.p3 <: p2
+---------- ---------------- ---------------- ----------------------------
+end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2 ?A.p1 <: !B.p2
+
+Example:
+
+!R <: !R ?Q <: ?Q ?Q <: ?Q
+------------------- --------------
+?Q.!R <: !R.?Q ?P.?Q <: ?P.?Q
+------------------------------------
+ ?P.?Q.!R <: !R.?P.?Q
+
+Lastly, relevant type classes instances are defined for each of the above
+notions, such as contractiveness and non-expansiveness, after which the
+specifications of the message-passing primitives are defined in terms of the
+protocol connectives. *)
+From iris.algebra Require Import gmap excl_auth.
+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 actris.channel Require Import multi_proto_model.
+Set Default Proof Using "Type".
+Export action.
+
+(** * Setup of Iris's cameras *)
+Class protoG Σ V :=
+ protoG_authG ::
+ inG Σ (excl_authR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))).
+
+Definition protoΣ V := #[
+ GFunctor (authRF (optionURF (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.
+
+Notation "<!> m" := (<Send> m) (at level 200, m at level 200) : proto_scope.
+Notation "<! x1 .. xn > m" := (<!> ∃ x1, .. (∃ xn, m) ..)
+ (at level 200, x1 closed binder, xn closed binder, m at level 200,
+ format "<! x1 .. xn > m") : proto_scope.
+Notation "<!.. x1 .. xn > m" := (<!> ∃.. x1, .. (∃.. xn, m) ..)
+ (at level 200, x1 closed binder, xn closed binder, m at level 200,
+ format "<!.. x1 .. xn > m") : proto_scope.
+
+Notation "<?> m" := (<Recv> m) (at level 200, m at level 200) : proto_scope.
+Notation "<? x1 .. xn > m" := (<?> ∃ x1, .. (∃ xn, m) ..)
+ (at level 200, x1 closed binder, xn closed binder, m at level 200,
+ format "<? x1 .. xn > m") : proto_scope.
+Notation "<?.. x1 .. xn > m" := (<?> ∃.. x1, .. (∃.. xn, m) ..)
+ (at level 200, x1 closed binder, xn closed binder, m at level 200,
+ format "<?.. 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 ∨ ∃ a m, p ≡ <a> m.
+ Proof.
+ rewrite iProto_message_eq iProto_end_eq.
+ destruct (proto_case p) as [|(a&m&?)]; [by left|right].
+ by exists a, (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&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&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&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&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&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.
+
+Definition can_step {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
+ (ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ :=
+ (∀ a1 a2 m1 m2,
+ (ps !!! i ≡ <a1> m1) -∗ (ps !!! j ≡ <a2> m2) -∗
+ match a1,a2 with
+ | Send j, Recv i => ∀ v p1, iMsg_car m1 v (Next p1) -∗
+ ∃ p2, iMsg_car m2 v (Next p2) ∗
+ â–· (rec (<[i:=p1]>(<[j:=p2]>ps)))
+ | Recv j, Send i => ∀ v p2, iMsg_car m2 v (Next p2) -∗
+ ∃ p1, iMsg_car m1 v (Next p1) ∗
+ â–· (rec (<[i:=p1]>(<[j:=p2]>ps)))
+ | _, _ => True
+ end).
+
+Definition iProto_consistent_pre {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
+ (ps : gmap nat (iProto Σ V)) : iProp Σ :=
+ ∀ i j, ⌜i ∈ dom ps⌠-∗ ⌜j ∈ dom ps⌠-∗ can_step rec ps i j.
+
+Global Instance iProto_consistent_pre_ne {Σ V}
+ (rec : gmapO natO (iProto Σ V) -n> iPropO Σ) :
+ NonExpansive (iProto_consistent_pre (λ ps, rec ps)).
+Proof. Admitted.
+
+Program Definition iProto_consistent_pre' {Σ V}
+ (rec : gmapO natO (iProto Σ V) -n> iPropO Σ) :
+ gmapO natO (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. Admitted.
+
+Definition iProto_consistent {Σ V} (ps : gmap nat (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 : gmap nat (iProto Σ V)) :
+ iProto_consistent ps ≡ (iProto_consistent_pre iProto_consistent) ps.
+Proof.
+ apply: (fixpoint_unfold iProto_consistent_pre').
+Qed.
+(* Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ := *)
+(* ∀ p3, iProto_consistent p1 p3 -∗ iProto_consistent p2 p3. *)
+(* 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. *)
+
+Definition iProto_example1 {Σ V} : gmap nat (iProto Σ V) :=
+ ∅.
+
+Lemma iProto_example1_consistent {Σ V} :
+ ⊢ iProto_consistent (@iProto_example1 Σ V).
+Proof.
+ rewrite iProto_consistent_unfold.
+ iIntros (i j Hi Hj). set_solver.
+Qed.
+
+Definition iProto_example2 `{!invGS Σ} (P : iProp Σ) : gmap nat (iProto Σ Z) :=
+ <[0 := (<(Send 1) @ (x:Z)> MSG x {{ P }} ; END)%proto ]>
+ (<[1 := (<(Recv 0) @ (x:Z)> MSG x {{ P }} ; END)%proto ]>
+ ∅).
+
+Lemma iProto_example2_consistent `{!invGS Σ} (P : iProp Σ) :
+ ⊢ iProto_consistent (@iProto_example2 _ Σ invGS0 P).
+Proof.
+ rewrite iProto_consistent_unfold.
+ rewrite /iProto_example2.
+ iIntros (i j Hi Hj).
+ iIntros (a1 a2 m1 m2) "Hm1 Hm2".
+ destruct i, j.
+ - rewrite !lookup_total_insert.
+ rewrite !iProto_message_equivI.
+ iDestruct "Hm1" as (<-) "#Hm1".
+ iDestruct "Hm2" as (<-) "#Hm2".
+ done.
+ - destruct j; [|set_solver].
+ rewrite !lookup_total_insert.
+ rewrite lookup_total_insert_ne; [|done].
+ rewrite !lookup_total_insert.
+ rewrite !iProto_message_equivI.
+ iDestruct "Hm1" as (<-) "#Hm1".
+ iDestruct "Hm2" as (<-) "#Hm2".
+ iIntros (v p1) "Hm1'".
+ iSpecialize ("Hm1" $!v (Next p1)).
+ rewrite iMsg_base_eq. simpl.
+ rewrite iMsg_exist_eq. simpl.
+ iRewrite -"Hm1" in "Hm1'".
+ iExists END.
+ iSpecialize ("Hm2" $!v (Next END)).
+ iRewrite -"Hm2".
+ simpl.
+ iDestruct "Hm1'" as (x Heq) "[#Heq HP]".
+ iSplitL.
+ { iExists x. iSplit; [done|]. iFrame. done. }
+ iNext. iRewrite -"Heq".
+ rewrite insert_commute; [|done].
+ rewrite insert_insert.
+ rewrite insert_commute; [|done].
+ rewrite insert_insert.
+ rewrite iProto_consistent_unfold.
+ iIntros (i' j' Hi' Hj').
+ iIntros (a1 a2 m1' m2') "Hm1' Hm2'".
+ destruct i'.
+ { rewrite lookup_total_insert.
+ iDestruct (iProto_end_message_equivI with "Hm1'") as "H".
+ done. }
+ destruct i'.
+ { rewrite lookup_total_insert_ne; [|done].
+ rewrite lookup_total_insert.
+ iDestruct (iProto_end_message_equivI with "Hm1'") as "H".
+ done. }
+ set_solver.
+ - destruct i; [|set_solver].
+ rewrite !lookup_total_insert.
+ rewrite lookup_total_insert_ne; [|done].
+ rewrite !lookup_total_insert.
+ rewrite !iProto_message_equivI.
+ iDestruct "Hm1" as (<-) "#Hm1".
+ iDestruct "Hm2" as (<-) "#Hm2".
+ iIntros (v p1) "Hm1'".
+ iSpecialize ("Hm2" $!v (Next p1)).
+ rewrite iMsg_base_eq. simpl.
+ rewrite iMsg_exist_eq. simpl.
+ iRewrite -"Hm2" in "Hm1'".
+ iExists END.
+ iSpecialize ("Hm1" $!v (Next END)).
+ iRewrite -"Hm1".
+ simpl.
+ iDestruct "Hm1'" as (x Heq) "[#Heq HP]".
+ iSplitL.
+ { iExists x. iSplit; [done|]. iFrame. done. }
+ iNext. iRewrite -"Heq".
+ rewrite insert_insert.
+ rewrite insert_commute; [|done].
+ rewrite insert_insert.
+ rewrite iProto_consistent_unfold.
+ iIntros (i' j' Hi' Hj').
+ iIntros (a1 a2 m1' m2') "Hm1' Hm2'".
+ destruct i'.
+ { rewrite lookup_total_insert.
+ iDestruct (iProto_end_message_equivI with "Hm1'") as "H".
+ done. }
+ destruct i'.
+ { rewrite lookup_total_insert_ne; [|done].
+ rewrite lookup_total_insert.
+ iDestruct (iProto_end_message_equivI with "Hm1'") as "H".
+ done. }
+ set_solver.
+ - destruct i; [|set_solver].
+ destruct j; [|set_solver].
+ rewrite lookup_total_insert_ne; [|done].
+ rewrite lookup_total_insert.
+ rewrite !iProto_message_equivI.
+ iDestruct "Hm1" as (<-) "Hm1".
+ iDestruct "Hm2" as (<-) "Hm2".
+ done.
+Qed.
+
+(* Lemma iProto_consistent_step {Σ V} (ps : gmap nat (iProto Σ V)) : *)
+(* (∀ i j m1 m2, *)
+(* ⌜ps !! i = Some (<(Send j)> m1)%proto⌠-∗ *)
+(* ⌜ps !! j = Some (<(Recv i)> m2)⌠-∗ *)
+(* iProto_consistent (ps))%I -∗ *)
+(* iProto_consistent ps. *)
+
+Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
+Global Instance proto_name_inhabited : Inhabited proto_name :=
+ populate (ProtName inhabitant 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 γl γr), (γl,γr))
+ (λ '(γl, γr), Some (ProtName γl γr)) _); by intros [].
+Qed.
+
+Inductive side := Left | Right.
+Global Instance side_inhabited : Inhabited side := populate Left.
+Global Instance side_eq_dec : EqDecision side.
+Proof. solve_decision. Qed.
+Global Instance side_countable : Countable side.
+Proof.
+ refine (inj_countable (λ s, if s is Left then true else false)
+ (λ b, Some (if b then Left else Right)) _); by intros [].
+Qed.
+Definition side_elim {A} (s : side) (l r : A) : A :=
+ match s with Left => l | Right => r end.
+
+Definition iProto_own_frag `{!protoG Σ V} (γ : proto_name) (s : side)
+ (p : iProto Σ V) : iProp Σ :=
+ own (side_elim s proto_l_name proto_r_name γ) (◯E (Next p)).
+Definition iProto_own_auth `{!protoG Σ V} (γ : proto_name) (s : side)
+ (p : iProto Σ V) : iProp Σ :=
+ own (side_elim s proto_l_name proto_r_name γ) (â—E (Next p)).
+
+(* Definition iProto_ctx `{protoG Σ V} *)
+(* (γ : proto_name) : iProp Σ := *)
+(* ∃ ps, *)
+(* iProto_own_auth γ Left pl ∗ *)
+(* iProto_own_auth γ Right pr ∗ *)
+(* â–· iProto_consistent ps. *)
+
+(* (** * The connective for ownership of channel ends *) *)
+(* Definition iProto_own `{!protoG Σ V} *)
+(* (γ : proto_name) (s : side) (p : iProto Σ V) : iProp Σ := *)
+(* ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ s p'. *)
+(* Arguments iProto_own {_ _ _} _ _%proto. *)
+(* Global Instance: Params (@iProto_own) 3 := {}. *)
+
+(* Global Instance iProto_own_contractive `{protoG Σ V} γ s : *)
+(* Contractive (iProto_own γ s). *)
+(* Proof. solve_contractive. Qed. *)
+
+(** * 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 ∨ ∃ a m, p ≡ <a> m.
+ Proof.
+ rewrite iProto_message_eq iProto_end_eq.
+ destruct (proto_case p) as [|(a&m&?)]; [by left|right].
+ by exists a, (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&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&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&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&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&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.
+
+ Lemma iProto_consistent_flip p1 p2 :
+ iProto_consistent p2 p1 -∗
+ iProto_consistent p1 p2.
+ Proof.
+ iLöb as "IH" forall (p1 p2).
+ iIntros "Hprot".
+ rewrite iProto_consistent_unfold /iProto_consistent_pre.
+ rewrite iProto_consistent_unfold /iProto_consistent_pre.
+ iIntros (a1 a2 m1 m2) "Hm1 Hm2".
+ iDestruct ("Hprot" with "Hm2 Hm1") as "Hprot".
+ destruct a1, a2; [done| | |done].
+ - iIntros (v p1') "Hm1".
+ iDestruct ("Hprot" with "Hm1") as (p2') "[Hprot Hrec]".
+ iExists p2'. iFrame. by iApply "IH".
+ - iIntros (v p2') "Hm2".
+ iDestruct ("Hprot" with "Hm2") as (p1') "[Hprot Hrec]".
+ iExists p1'. iFrame. by iApply "IH".
+ Qed.
+
+ Lemma iProto_consistent_step m1 m2 v p1 :
+ iProto_consistent (<!> m1) (<?> m2) -∗
+ iMsg_car m1 v (Next p1) -∗
+ ∃ p2, iMsg_car m2 v (Next p2) ∗ ▷ iProto_consistent p1 p2.
+ Proof.
+ iIntros "Hprot Hm1".
+ rewrite iProto_consistent_unfold /iProto_consistent_pre.
+ iDestruct ("Hprot" with "[//] [//] Hm1") as (p2) "[Hm2 Hprot]".
+ iExists p2. iFrame.
+ Qed.
+
+ Lemma iProto_consistent_dual p :
+ ⊢ iProto_consistent p (iProto_dual p).
+ Proof.
+ iLöb as "IH" forall (p).
+ rewrite iProto_consistent_unfold.
+ iIntros (a1 a2 m1 m2) "#Hmeq1 #Hmeq2".
+ destruct a1, a2; [done| | |done].
+ - iIntros (v p') "Hm1".
+ iRewrite "Hmeq1" in "Hmeq2".
+ rewrite iProto_dual_message. simpl.
+ rewrite iProto_message_equivI.
+ iDestruct "Hmeq2" as (_) "Hmeq2".
+ iSpecialize ("Hmeq2" $! v (Next (iProto_dual p'))).
+ iExists (iProto_dual p').
+ iRewrite -"Hmeq2".
+ iSplitL; [|iNext; by iApply "IH"].
+ simpl. iExists p'. iFrame. done.
+ - iIntros (v p') "Hm2".
+ iRewrite "Hmeq1" in "Hmeq2".
+ rewrite iProto_dual_message. simpl.
+ rewrite iProto_message_equivI.
+ iDestruct "Hmeq2" as (_) "Hmeq2".
+ iSpecialize ("Hmeq2" $! v (Next p')).
+ iRewrite -"Hmeq2" in "Hm2".
+ simpl.
+ iDestruct "Hm2" as (p'') "[Hm2 Hmeq']".
+ iExists p''. iFrame.
+ iNext. iRewrite "Hmeq'".
+ iApply "IH".
+ Qed.
+
+ Lemma iProto_consistent_le_l pl pl' pr :
+ iProto_consistent pl pr -∗ pl ⊑ pl' -∗ iProto_consistent pl' pr.
+ Proof. iIntros "Hprot Hle". by iApply "Hle". Qed.
+ Lemma iProto_consistent_le_r pl pr pr' :
+ iProto_consistent pl pr -∗ pr ⊑ pr' -∗ iProto_consistent pl pr'.
+ Proof.
+ iIntros "H Hle". iApply iProto_consistent_flip.
+ iApply "Hle". by iApply iProto_consistent_flip.
+ Qed.
+
+ Lemma iProto_le_refl p : ⊢ p ⊑ p.
+ Proof. iIntros (p') "$". Qed.
+
+ Lemma iProto_le_end : ⊢ END ⊑ (END : iProto Σ V).
+ Proof. iApply iProto_le_refl. Qed.
+
+ (* Lemma iProto_le_send m1 m2 : *)
+ (* (∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1', *)
+ (* ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')) -∗ *)
+ (* (<!> m1) ⊑ (<!> m2). *)
+ (* Proof. *)
+ (* iLöb as "IH" forall (m1 m2). *)
+ (* iIntros "Hle". *)
+ (* repeat (unfold iProto_le at 3). *)
+ (* iIntros (p) "Hprot". *)
+ (* repeat rewrite iProto_consistent_unfold; unfold iProto_consistent_pre. *)
+ (* iSplit; [iDestruct "Hprot" as "[Hprot _]"|iDestruct "Hprot" as "[_ Hprot]"]. *)
+ (* { iIntros (a m) "H". *)
+ (* iDestruct (iProto_message_equivI with "H") as (Heq) "{H} #Hmeq"; subst. *)
+ (* iIntros (v p') "Hm". *)
+ (* iSpecialize ("Hprot" with "[//]"). *)
+ (* iSpecialize ("Hmeq" $! v (Next p')). iRewrite -"Hmeq" in "Hm". *)
+ (* iSpecialize ("Hle" $! _ _ with "Hm"). iDestruct "Hle" as (p'') "[Hle Hm]". *)
+ (* iApply "Hle". iApply "Hprot". iApply "Hm". } *)
+ (* { iIntros (a m) "H". *)
+ (* iSpecialize ("Hprot" $! _ _ with "H"). *)
+ (* destruct a. *)
+ (* - iIntros (v p') "Hm". *)
+ (* iApply ("IH" with "[Hle]"). *)
+ (* { iNext. iIntros (v' p'') "Hm". *)
+ (* iSpecialize ("Hle" with "Hm"). *)
+ (* iDestruct "Hle" as (p''') "[Hle Hm]". *)
+ (* iExists p'''. iSplitR "Hm"; [iApply "Hle" | iApply "Hm"]. } *)
+ (* iApply "Hprot". iApply "Hm". *)
+ (* - iIntros (v vs Heq); subst. *)
+ (* iSpecialize ("Hprot" $! _ _ eq_refl). *)
+ (* iDestruct "Hprot" as (p') "[Hm Hprot]". *)
+ (* iExists (p'). iFrame "Hm". *)
+ (* iApply ("IH" with "[Hle] [Hprot]"); [|iApply "Hprot"]. *)
+ (* iNext. iIntros (v' p'') "Hm". *)
+ (* iSpecialize ("Hle" with "Hm"). iDestruct "Hle" as (p''') "[Hle Hm]". *)
+ (* iExists p'''; iSplitR "Hm"; [iApply "Hle" |iApply "Hm"]. } *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_recv m1 m2 : *)
+ (* (∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2', *)
+ (* ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2')) -∗ *)
+ (* (<?> m1) ⊑ (<?> m2). *)
+ (* Proof. *)
+ (* iIntros "H" (vsl vsr p) "Hprot". *)
+ (* iLöb as "IH" forall (vsl vsr m2 p). *)
+ (* iEval (rewrite iProto_consistent_unfold). *)
+ (* rewrite /iProto_consistent_pre. *)
+ (* rewrite iProto_consistent_unfold /iProto_consistent_pre. *)
+ (* iSplit; last first. *)
+ (* { *)
+ (* iDestruct "Hprot" as "[_ Hprot]". *)
+ (* iIntros ([] m) "Heq". *)
+ (* { iIntros (v vs) "Hm". *)
+ (* iDestruct ("Hprot" with "Heq Hm") as "Hprot". *)
+ (* iIntros "!>". *)
+ (* by iApply ("IH" with "H"). } *)
+ (* { iIntros (v vs) "Hm". *)
+ (* iDestruct ("Hprot" with "Heq Hm") as (p') "[Hm Hprot]". *)
+ (* iExists p'. iFrame. *)
+ (* iIntros "!>". *)
+ (* by iApply ("IH" with "H"). } *)
+ (* } *)
+ (* destruct vsr. *)
+ (* { iIntros (a m) "Heq". rewrite iProto_message_equivI. *)
+ (* iDestruct "Heq" as (<-) "Heq". *)
+ (* iIntros (v vs Heq). done. } *)
+ (* iIntros (a m) "Heq". rewrite iProto_message_equivI. *)
+ (* iDestruct "Heq" as (<-) "Heq". *)
+ (* iIntros (w vs Heq). *)
+ (* assert (v = w) as <- by set_solver. *)
+ (* assert (vsr = vs) as <- by set_solver. *)
+ (* iDestruct "Hprot" as "[Hprot _]". *)
+ (* iDestruct ("Hprot" with "[//] [//]") as (p') "[Hm Hprot]". *)
+ (* iDestruct ("H" with "Hm") as (p'') "[Hle H]". *)
+ (* iExists p''. *)
+ (* iSpecialize ("Heq" $! v (Next p'')). iRewrite -"Heq". *)
+ (* iFrame. iIntros "!>". *)
+ (* iApply (iProto_consistent_le_l with "Hprot Hle"). *)
+ (* 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. *)
+ (* - 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_end_inv_l 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_r 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 p1 m2 : *)
+ (* p1 ⊑ (<!> m2) -∗ ∃ a1 m1, *)
+ (* (p1 ≡ <a1> m1) ∗ *)
+ (* match a1 with *)
+ (* | Send => ∀ v p2', *)
+ (* iMsg_car m2 v (Next p2') -∗ ∃ p1', *)
+ (* ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1') *)
+ (* | Recv => ∀ v1 v2 p1' p2', *)
+ (* iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt, *)
+ (* ▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2') *)
+ (* end. *)
+ (* 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)". *)
+ (* iExists _, _; iSplit; [done|]. destruct a1, a2. *)
+ (* - iIntros (v p2') "Hm2". *)
+ (* iDestruct (iProto_message_equivI with "Hp2") as (_) "{Hp2} #Hm". *)
+ (* iApply "H". by iRewrite -("Hm" $! v (Next p2')). *)
+ (* - done. *)
+ (* - iIntros (v1 v2 p1' p2') "Hm1 Hm2". *)
+ (* iDestruct (iProto_message_equivI with "Hp2") as (_) "{Hp2} #Hm". *)
+ (* iApply ("H" with "Hm1"). by iRewrite -("Hm" $! v2 (Next p2')). *)
+ (* - iDestruct (iProto_message_equivI with "Hp2") as ([=]) "_". *)
+ (* Qed. *)
+ (* Lemma iProto_le_send_send_inv m1 m2 v p2' : *)
+ (* (<!> m1) ⊑ (<!> 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 (a m1') "[Hm1 H]". *)
+ (* iDestruct (iProto_message_equivI with "Hm1") as (<-) "Hm1". *)
+ (* iDestruct ("H" with "Hm2") as (p1') "[Hle Hm]". *)
+ (* iRewrite -("Hm1" $! v (Next p1')) in "Hm". auto with iFrame. *)
+ (* Qed. *)
+ (* Lemma iProto_le_recv_send_inv m1 m2 v1 v2 p1' p2' : *)
+ (* (<?> m1) ⊑ (<!> m2) -∗ *)
+ (* iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt, *)
+ (* ▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2'). *)
+ (* Proof. *)
+ (* iIntros "H Hm1 Hm2". iDestruct (iProto_le_send_inv with "H") as (a m1') "[Hm H]". *)
+ (* iDestruct (iProto_message_equivI with "Hm") as (<-) "{Hm} #Hm". *)
+ (* iApply ("H" with "[Hm1] Hm2"). by iRewrite -("Hm" $! v1 (Next p1')). *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_recv_inv p1 m2 : *)
+ (* p1 ⊑ (<?> m2) -∗ ∃ m1, *)
+ (* (p1 ≡ <?> 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)". *)
+ (* iExists m1. *)
+ (* iDestruct (iProto_message_equivI with "Hp2") as (<-) "{Hp2} #Hm2". *)
+ (* destruct a1; [done|]. iSplit; [done|]. *)
+ (* iIntros (v p1') "Hm". iDestruct ("H" with "Hm") as (p2') "[Hle Hm]". *)
+ (* iExists p2'. iIntros "{$Hle}". by iRewrite ("Hm2" $! v (Next p2')). *)
+ (* Qed. *)
+ (* Lemma iProto_le_recv_recv_inv m1 m2 v p1' : *)
+ (* (<?> m1) ⊑ (<?> 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 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_refl p : ⊢ p ⊑ p. *)
+ (* Proof. *)
+ (* iLöb as "IH" forall (p). destruct (iProto_case p) as [->|([]&m&->)]. *)
+ (* - iApply iProto_le_end. *)
+ (* - iApply iProto_le_send. auto 10 with iFrame. *)
+ (* - iApply iProto_le_recv. auto 10 with iFrame. *)
+ (* Qed. *)
+
+ Lemma iProto_le_trans p1 p2 p3 : p1 ⊑ p2 -∗ p2 ⊑ p3 -∗ p1 ⊑ p3.
+ Proof.
+ iIntros "H1 H2" (p) "Hprot".
+ iApply "H2". iApply "H1". done.
+ Qed.
+
+ (* Lemma iProto_le_payload_elim_l a m v P p : *)
+ (* (P -∗ (<?> MSG v; p) ⊑ (<a> m)) -∗ *)
+ (* (<?> MSG v {{ P }}; p) ⊑ (<a> m). *)
+ (* Proof. *)
+ (* rewrite iMsg_base_eq. iIntros "H". destruct a. *)
+ (* - iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= (#?&#?&HP) Hm2 /=". *)
+ (* iApply (iProto_le_recv_send_inv with "(H HP)"); simpl; auto. *)
+ (* - 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 a m v P p : *)
+ (* (P -∗ (<a> m) ⊑ (<!> MSG v; p)) -∗ *)
+ (* (<a> m) ⊑ (<!> MSG v {{ P }}; p). *)
+ (* Proof. *)
+ (* rewrite iMsg_base_eq. iIntros "H". destruct a. *)
+ (* - iApply iProto_le_send. iIntros (v' p') "(->&Hp&HP)". *)
+ (* iApply (iProto_le_send_send_inv with "(H HP)"); simpl; auto. *)
+ (* - iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 (->&#?&HP) /=". *)
+ (* iApply (iProto_le_recv_send_inv with "(H HP) Hm1"); simpl; auto. *)
+ (* Qed. *)
+ (* Lemma iProto_le_payload_intro_l v P p : *)
+ (* P -∗ (<!> MSG v {{ P }}; p) ⊑ (<!> 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 v P p : *)
+ (* P -∗ (<?> MSG v; p) ⊑ (<?> 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} (m1 : A → iMsg Σ V) a m2 : *)
+ (* (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗ *)
+ (* (<? x> m1 x) ⊑ (<a> m2). *)
+ (* Proof. *)
+ (* rewrite iMsg_exist_eq. iIntros "H". destruct a. *)
+ (* - iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=". *)
+ (* iDestruct "Hm1" as (x) "Hm1". *)
+ (* iApply (iProto_le_recv_send_inv with "H Hm1 Hm2"). *)
+ (* - 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_l_inhabited `{!Inhabited A} (m : A → iMsg Σ V) p : *)
+ (* (∀ x, (<?> m x) ⊑ p) -∗ *)
+ (* (<? x> m x) ⊑ p. *)
+ (* Proof. *)
+ (* rewrite iMsg_exist_eq. iIntros "H". *)
+ (* destruct (iProto_case p) as [Heq | [a [m' Heq]]]. *)
+ (* - unshelve iSpecialize ("H" $!inhabitant); first by apply _. *)
+ (* rewrite Heq. *)
+ (* iDestruct (iProto_le_end_inv_l with "H") as "H". *)
+ (* rewrite iProto_end_eq iProto_message_eq. *)
+ (* iDestruct (proto_message_end_equivI with "H") as "[]". *)
+ (* - iEval (rewrite Heq). destruct a. *)
+ (* + iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=". *)
+ (* iDestruct "Hm1" as (x) "Hm1". *)
+ (* iSpecialize ("H" $! x). rewrite Heq. *)
+ (* iApply (iProto_le_recv_send_inv with "H Hm1 Hm2"). *)
+ (* + iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm". *)
+ (* iSpecialize ("H" $! x). rewrite Heq. *)
+ (* by iApply (iProto_le_recv_recv_inv with "H"). *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_exist_elim_r {A} a m1 (m2 : A → iMsg Σ V) : *)
+ (* (∀ x, (<a> m1) ⊑ (<!> m2 x)) -∗ *)
+ (* (<a> m1) ⊑ (<! x> m2 x). *)
+ (* Proof. *)
+ (* rewrite iMsg_exist_eq. iIntros "H". destruct a. *)
+ (* - iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm". *)
+ (* by iApply (iProto_le_send_send_inv with "H"). *)
+ (* - iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1". *)
+ (* iDestruct 1 as (x) "Hm2". *)
+ (* iApply (iProto_le_recv_send_inv with "H Hm1 Hm2"). *)
+ (* Qed. *)
+ (* Lemma iProto_le_exist_elim_r_inhabited `{Hinh : Inhabited A} p (m : A → iMsg Σ V) : *)
+ (* (∀ x, p ⊑ (<!> m x)) -∗ *)
+ (* p ⊑ (<! x> m x). *)
+ (* Proof. *)
+ (* rewrite iMsg_exist_eq. iIntros "H". *)
+ (* destruct (iProto_case p) as [Heq | [a [m' Heq]]]. *)
+ (* - unshelve iSpecialize ("H" $!inhabitant); first by apply _. *)
+ (* rewrite Heq. *)
+ (* iDestruct (iProto_le_end_inv_r with "H") as "H". *)
+ (* rewrite iProto_end_eq iProto_message_eq. *)
+ (* iDestruct (proto_message_end_equivI with "H") as "[]". *)
+ (* - iEval (rewrite Heq). destruct a. *)
+ (* + iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm". *)
+ (* iSpecialize ("H" $! x). rewrite Heq. *)
+ (* by iApply (iProto_le_send_send_inv with "H"). *)
+ (* + iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1". *)
+ (* iDestruct 1 as (x) "Hm2". *)
+ (* iSpecialize ("H" $! x). rewrite Heq. *)
+ (* iApply (iProto_le_recv_send_inv with "H Hm1 Hm2"). *)
+ (* Qed. *)
+ (* Lemma iProto_le_exist_intro_l {A} (m : A → iMsg Σ V) a : *)
+ (* ⊢ (<! x> m x) ⊑ (<!> 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} (m : A → iMsg Σ V) a : *)
+ (* ⊢ (<?> m a) ⊑ (<? 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} (m1 : TT → iMsg Σ V) a m2 : *)
+ (* (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗ *)
+ (* (<?.. x> m1 x) ⊑ (<a> 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} a m1 (m2 : TT → iMsg Σ V) : *)
+ (* (∀ x, (<a> m1) ⊑ (<!> m2 x)) -∗ *)
+ (* (<a> m1) ⊑ (<!.. 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} (m : TT → iMsg Σ V) x : *)
+ (* ⊢ (<!.. x> m 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_l|]. iApply IH. *)
+ (* Qed. *)
+ (* Lemma iProto_le_texist_intro_r {TT : tele} (m : TT → iMsg Σ V) x : *)
+ (* ⊢ (<?> m x) ⊑ (<?.. 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_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. *)
+ (* - 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_base_swap v1 v2 P1 P2 p : *)
+ (* ⊢ (<?> MSG v1 {{ P1 }}; <!> MSG v2 {{ P2 }}; p) *)
+ (* ⊑ (<!> MSG v2 {{ P2 }}; <?> MSG v1 {{ P1 }}; p). *)
+ (* Proof. *)
+ (* rewrite {1 3}iMsg_base_eq. iApply iProto_le_swap. *)
+ (* iIntros (v1' v2' p1' p2') "/= (->&#Hp1&HP1) (->&#Hp2&HP2)". iExists p. *)
+ (* iSplitL "HP2". *)
+ (* - iIntros "!>". iRewrite -"Hp1". by iApply iProto_le_payload_intro_l. *)
+ (* - iIntros "!>". iRewrite -"Hp2". by iApply iProto_le_payload_intro_r. *)
+ (* 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 [->|([]&m1&->)]. *)
+ (* - iDestruct (iProto_le_end_inv_l with "H") as "H". *)
+ (* iRewrite "H". iApply iProto_le_refl. *)
+ (* - iDestruct (iProto_le_send_inv with "H") as (a2 m2) "[Hp2 H]". *)
+ (* iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message). *)
+ (* destruct a2; simpl. *)
+ (* + 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. *)
+ (* + iApply iProto_le_swap. iIntros (v1 v2 p1d p2d). *)
+ (* iDestruct 1 as (p1') "[Hm1 #Hp1d]". iDestruct 1 as (p2') "[Hm2 #Hp2d]". *)
+ (* iDestruct ("H" with "Hm2 Hm1") as (pt) "[H1 H2]". *)
+ (* iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}". *)
+ (* rewrite !iProto_dual_message /=. iExists (iProto_dual pt). iSplitL "H2". *)
+ (* * iIntros "!>". iRewrite "Hp1d". by rewrite -iMsg_dual_base. *)
+ (* * iIntros "!>". iRewrite "Hp2d". by rewrite -iMsg_dual_base. *)
+ (* - iDestruct (iProto_le_recv_inv 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_amber_internal (p1 p2 : iProto Σ V → iProto Σ V) *)
+ (* `{Contractive p1, Contractive p2}: *)
+ (* □ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) -∗ *)
+ (* fixpoint p1 ⊑ fixpoint p2. *)
+ (* Proof. *)
+ (* iIntros "#H". iLöb as "IH". *)
+ (* iEval (rewrite (fixpoint_unfold p1)). *)
+ (* iEval (rewrite (fixpoint_unfold p2)). *)
+ (* iApply "H". iApply "IH". *)
+ (* Qed. *)
+ (* Lemma iProto_le_amber_external (p1 p2 : iProto Σ V → iProto Σ V) *)
+ (* `{Contractive p1, Contractive p2}: *)
+ (* (∀ rec1 rec2, (⊢ rec1 ⊑ rec2) → ⊢ p1 rec1 ⊑ p2 rec2) → *)
+ (* ⊢ fixpoint p1 ⊑ fixpoint p2. *)
+ (* Proof. *)
+ (* intros IH. apply fixpoint_ind. *)
+ (* - by intros p1' p2' -> ?. *)
+ (* - exists (fixpoint p2). iApply iProto_le_refl. *)
+ (* - intros p' ?. rewrite (fixpoint_unfold p2). by apply IH. *)
+ (* - apply bi.limit_preserving_entails; [done|solve_proper]. *)
+ (* 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 [->|([]&m2&->)]. *)
+ (* - iDestruct (iProto_le_end_inv_l with "H1") as "H1". *)
+ (* iRewrite "H1". by rewrite !left_id. *)
+ (* - iDestruct (iProto_le_send_inv with "H1") as (a1 m1) "[Hp1 H1]". *)
+ (* iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. destruct a1; simpl. *)
+ (* + 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"). *)
+ (* + iApply iProto_le_swap. iIntros (v1 v2 p13 p24). *)
+ (* iDestruct 1 as (p1') "[Hm1 #Hp13]". iDestruct 1 as (p2') "[Hm2 #Hp24]". *)
+ (* iSpecialize ("H1" with "Hm1 Hm2"). *)
+ (* iDestruct "H1" as (pt) "[H1 H1']". *)
+ (* iExists (pt <++> p3). iSplitL "H1". *)
+ (* * iIntros "!>". iRewrite "Hp13". *)
+ (* rewrite /= -iMsg_app_base -iProto_app_message. *)
+ (* iApply ("IH" with "H1"). iApply iProto_le_refl. *)
+ (* * iIntros "!>". iRewrite "Hp24". *)
+ (* rewrite /= -iMsg_app_base -iProto_app_message. *)
+ (* iApply ("IH" with "H1' H2"). *)
+ (* - iDestruct (iProto_le_recv_inv 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. *)
+
+ (** ** Lemmas about the auxiliary definitions and invariants *)
+ Global Instance iProto_app_recvs_ne vs :
+ NonExpansive (iProto_app_recvs (Σ:=Σ) (V:=V) vs).
+ Proof. induction vs; solve_proper. Qed.
+ Global Instance iProto_app_recvs_proper vs :
+ Proper ((≡) ==> (≡)) (iProto_app_recvs (Σ:=Σ) (V:=V) vs).
+ Proof. induction vs; solve_proper. Qed.
+
+ Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
+ Proof. solve_proper. Qed.
+
+ Lemma iProto_own_auth_agree γ s p p' :
+ iProto_own_auth γ s p -∗ iProto_own_frag γ s p' -∗ ▷ (p ≡ p').
+ Proof.
+ iIntros "H◠H◯". iDestruct (own_valid_2 with "H◠H◯") as "H✓".
+ iDestruct (excl_auth_agreeI with "H✓") as "H✓".
+ iApply (later_equivI_1 with "H✓").
+ Qed.
+
+ Lemma iProto_own_auth_update γ s p p' p'' :
+ iProto_own_auth γ s p -∗ iProto_own_frag γ s p' ==∗
+ iProto_own_auth γ s p'' ∗ iProto_own_frag γ s p''.
+ Proof.
+ iIntros "Hâ— Hâ—¯". iDestruct (own_update_2 with "Hâ— Hâ—¯") as "H".
+ { eapply (excl_auth_update _ _ (Next p'')). }
+ by rewrite own_op.
+ Qed.
+
+ Global Instance iProto_own_ne γ s : NonExpansive (iProto_own γ s).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_own_proper γ s : Proper ((≡) ==> (≡)) (iProto_own γ s).
+ Proof. apply (ne_proper _). 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_init p :
+ ⊢ |==> ∃ γ,
+ iProto_ctx γ ∗ iProto_own γ Left p ∗ iProto_own γ Right (iProto_dual p).
+ Proof.
+ iMod (own_alloc (â—E (Next p) â‹… â—¯E (Next p))) as (lγ) "[Hâ—l Hâ—¯l]".
+ { by apply excl_auth_valid. }
+ iMod (own_alloc (â—E (Next (iProto_dual p)) â‹…
+ â—¯E (Next (iProto_dual p)))) as (rγ) "[Hâ—r Hâ—¯r]".
+ { by apply excl_auth_valid. }
+ pose (ProtName lγ rγ) as γ. iModIntro. iExists γ. iSplitL "Hâ—l Hâ—r".
+ { iExists p, (iProto_dual p). iFrame. iApply iProto_consistent_dual. }
+ iSplitL "Hâ—¯l"; iExists _; iFrame; iApply iProto_le_refl.
+ Qed.
+
+ Definition side_dual s :=
+ match s with
+ | Left => Right
+ | Right => Left
+ end.
+
+ Lemma iProto_step_l γ m1 m2 p1 v :
+ iProto_ctx γ -∗ iProto_own γ Left (<!> m1) -∗ iProto_own γ Right (<?> m2) -∗
+ iMsg_car m1 v (Next p1) ==∗
+ ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ ▷ iProto_ctx γ ∗
+ iProto_own γ Left p1 ∗ iProto_own γ Right p2.
+ Proof.
+ iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hconsistent)".
+ iDestruct 1 as (pl') "[Hlel Hâ—¯l]".
+ iDestruct 1 as (pr') "[Hler Hâ—¯r]".
+ iIntros "Hm".
+ iDestruct (iProto_own_auth_agree with "Hâ—l Hâ—¯l") as "#Hpl".
+ iDestruct (iProto_own_auth_agree with "Hâ—r Hâ—¯r") as "#Hpr".
+ iAssert (▷ (pl ⊑ <!> m1))%I
+ with "[Hlel]" as "{Hpl} Hlel"; first (iNext; by iRewrite "Hpl").
+ iAssert (▷ (pr ⊑ <?> m2))%I
+ with "[Hler]" as "{Hpr} Hler"; first (iNext; by iRewrite "Hpr").
+ iDestruct (iProto_consistent_le_l with "Hconsistent Hlel") as "Hconsistent".
+ iDestruct (iProto_consistent_le_r with "Hconsistent Hler") as "Hconsistent".
+ iDestruct (iProto_consistent_step with "Hconsistent [Hm //]") as
+ (p2) "[Hm2 Hconsistent]".
+ iMod (iProto_own_auth_update _ _ _ _ p1 with "Hâ—l Hâ—¯l") as "[Hâ—l Hâ—¯l]".
+ iMod (iProto_own_auth_update _ _ _ _ p2 with "Hâ—r Hâ—¯r") as "[Hâ—r Hâ—¯r]".
+ iIntros "!>!>".
+ iExists p2. iFrame.
+ iSplitL "Hconsistent Hâ—l Hâ—r".
+ - iExists _, _. iFrame.
+ - iSplitL "Hâ—¯l".
+ + iExists _. iFrame. iApply iProto_le_refl.
+ + iExists _. iFrame. iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_step_r γ m1 m2 p2 v :
+ iProto_ctx γ -∗ iProto_own γ Left (<?> m1) -∗ iProto_own γ Right (<!> m2) -∗
+ iMsg_car m2 v (Next p2) ==∗
+ ▷ ∃ p1, iMsg_car m1 v (Next p1) ∗ ▷ iProto_ctx γ ∗
+ iProto_own γ Left p1 ∗ iProto_own γ Right p2.
+ Proof.
+ iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hconsistent)".
+ iDestruct 1 as (pl') "[Hlel Hâ—¯l]".
+ iDestruct 1 as (pr') "[Hler Hâ—¯r]".
+ iIntros "Hm".
+ iDestruct (iProto_own_auth_agree with "Hâ—l Hâ—¯l") as "#Hpl".
+ iDestruct (iProto_own_auth_agree with "Hâ—r Hâ—¯r") as "#Hpr".
+ iAssert (▷ (pl ⊑ <?> m1))%I
+ with "[Hlel]" as "{Hpl} Hlel"; first (iNext; by iRewrite "Hpl").
+ iAssert (▷ (pr ⊑ <!> m2))%I
+ with "[Hler]" as "{Hpr} Hler"; first (iNext; by iRewrite "Hpr").
+ iDestruct (iProto_consistent_le_l with "Hconsistent Hlel") as "Hconsistent".
+ iDestruct (iProto_consistent_le_r with "Hconsistent Hler") as "Hconsistent".
+ iDestruct (iProto_consistent_flip with "Hconsistent") as
+ "Hconsistent".
+ iDestruct (iProto_consistent_step with "Hconsistent [Hm //]") as
+ (p1) "[Hm1 Hconsistent]".
+ iMod (iProto_own_auth_update _ _ _ _ p1 with "Hâ—l Hâ—¯l") as "[Hâ—l Hâ—¯l]".
+ iMod (iProto_own_auth_update _ _ _ _ p2 with "Hâ—r Hâ—¯r") as "[Hâ—r Hâ—¯r]".
+ iIntros "!>!>".
+ iExists p1. iFrame.
+ iSplitL "Hconsistent Hâ—l Hâ—r".
+ - iExists _, _. iFrame. iApply iProto_consistent_flip. iFrame.
+ - iSplitL "Hâ—¯l".
+ + iExists _. iFrame. iApply iProto_le_refl.
+ + iExists _. iFrame. iApply iProto_le_refl.
+ 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} a (m1 : A → iMsg Σ V) m2 name : *)
+ (* AsIdentName m1 name → *)
+ (* FromForall (iProto_message Recv (iMsg_exist m1) ⊑ (<a> m2)) *)
+ (* (λ x, (<?> m1 x) ⊑ (<a> m2))%I name | 10. *)
+ (* Proof. intros _. apply iProto_le_exist_elim_l. Qed. *)
+ (* Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A → iMsg Σ V) name : *)
+ (* AsIdentName m2 name → *)
+ (* FromForall ((<a> m1) ⊑ iProto_message Send (iMsg_exist m2)) *)
+ (* (λ x, (<a> m1) ⊑ (<!> m2 x))%I name | 11. *)
+ (* Proof. intros _. apply iProto_le_exist_elim_r. Qed. *)
+
+ (* Global Instance iProto_le_from_wand_l a m v P p : *)
+ (* TCIf (TCEq P True%I) False TCTrue → *)
+ (* FromWand ((<?> MSG v {{ P }}; p) ⊑ (<a> m)) P ((<?> MSG v; p) ⊑ (<a> m)) | 10. *)
+ (* Proof. intros _. apply iProto_le_payload_elim_l. Qed. *)
+ (* Global Instance iProto_le_from_wand_r a m v P p : *)
+ (* FromWand ((<a> m) ⊑ (<!> MSG v {{ P }}; p)) P ((<a> m) ⊑ (<!> MSG v; p)) | 11. *)
+ (* Proof. apply iProto_le_payload_elim_r. Qed. *)
+
+ (* Global Instance iProto_le_from_exist_l {A} (m : A → iMsg Σ V) p : *)
+ (* FromExist ((<! x> m x) ⊑ p) (λ a, (<!> 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} (m : A → iMsg Σ V) p : *)
+ (* FromExist (p ⊑ <? x> m x) (λ a, p ⊑ (<?> 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 m v P p : *)
+ (* FromSep ((<!> MSG v {{ P }}; p) ⊑ (<!> m)) P ((<!> MSG v; p) ⊑ (<!> 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 m v P p : *)
+ (* FromSep ((<?> m) ⊑ (<?> MSG v {{ P }}; p)) P ((<?> m) ⊑ (<?> 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 q m v R P Q p : *)
+ (* Frame q R P Q → *)
+ (* Frame q R ((<!> MSG v {{ P }}; p) ⊑ (<!> m)) *)
+ (* ((<!> MSG v {{ Q }}; p) ⊑ (<!> 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 q m v R P Q p : *)
+ (* Frame q R P Q → *)
+ (* Frame q R ((<?> m) ⊑ (<?> MSG v {{ P }}; p)) *)
+ (* ((<?> m) ⊑ (<?> 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 _. apply iProto_le_base. Qed. *)
+
+End proto.
+
+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/theories/channel/multi_proto_model.v b/theories/channel/multi_proto_model.v
new file mode 100644
index 0000000000000000000000000000000000000000..9c6c8be4b1f3c89e141245f03062d1db3e9786a4
--- /dev/null
+++ b/theories/channel/multi_proto_model.v
@@ -0,0 +1,307 @@
+(** 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 an inductively defined datatype with two constructors [Send] and
+[Recv]. 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 actris.utils Require Import cofe_solver_2.
+Set Default Proof Using "Type".
+
+Module Export action.
+ Inductive action := Send (n:nat) | Recv (n: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.