Make everything work; lots of refactoring.

_CoqProject

@@ -5,9 +5,9 @@ theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v
 theories/utils/group.v
-theories/channel/channel.v
 theories/channel/proto_model.v
-theories/channel/proto_channel.v
+theories/channel/proto.v
+theories/channel/channel.v
 theories/channel/proofmode.v
 theories/examples/basics.v
 theories/examples/sort.v

theories/channel/channel.v

 (** This file contains the definition of the channels, encoded as a pair of
-lock-protected buffers, and their primitive proof rules. Actris's proof rules
-for channels in terms of dependent separation protocols can be found in the file
-[theories/channel/proto_channel.v].
+lock-protected buffers, 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 [receive] w.r.t. dependent
+  separation protocols.
+
+An encoding of the usual branching connectives [prot1 <{Q1}+{Q2}> prot2] and
+[prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in this
+file.
 
 In this file we define the three message-passing connectives:
 
@@ -10,32 +17,13 @@ In this file we define the three message-passing connectives:
   polarity of the endpoints.
 - [send] takes an endpoint and adds an element to the first buffer.
 - [recv] performs a busy loop until there is something in the second buffer,
-  which it pops and returns, locking during each peek.
-
-The logically-atomic basic (i.e. non dependent separation protocol)
-proof rules [new_chan_spec], [send_spec] and [recv_spec] are defined in terms
-of the logical connectives [is_chan] and [chan_own]:
-
-- [is_chan γ v1 v2] is a persistent proposition expressing that [v1] and [v2]
-  are the endpoints of a channel with logical name [γ].
-- [chan_own γ s vs] is an exclusive proposition expressing the buffer of side
-  [s] ([Left] or [Right]) has contents [vs].
-
-Note that the specifications include 3 laters [▷] to account for the three
-levels of indirection due to step-indexing in the model of dependent separation
-protocols. *)
+  which it pops and returns, locking during each peek.*)
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.heap_lang Require Import lifting.
-From iris.algebra Require Import excl_auth list.
-From actris.utils Require Import llist.
+From actris.channel Require Export proto.
+From actris.utils Require Import llist skip.
 Set Default Proof Using "Type".
 
-Inductive side := Left | Right.
-Instance side_inhabited : Inhabited side := populate Left.
-Definition side_elim {A} (s : side) (l r : A) : A :=
-  match s with Left => l | Right => r end.
-
 (** * The definition of the message-passing connectives *)
 Definition new_chan : val :=
   λ: <>,
@@ -44,12 +32,17 @@ Definition new_chan : val :=
      let: "lk" := newlock #() in
      ((("l","r"),"lk"), (("r","l"),"lk")).
 
+Definition start_chan : val := λ: "f",
+  let: "cc" := new_chan #() in
+  Fork ("f" (Snd "cc"));; Fst "cc".
+
 Definition send : val :=
   λ: "c" "v",
     let: "lk" := Snd "c" in
     acquire "lk";;
     let: "l" := Fst (Fst "c") in
     lsnoc "l" "v";;
+    skipN (llength (Snd (Fst "c")));; (* Later stripping *)
     release "lk".
 
 Definition try_recv : val :=
@@ -68,156 +61,251 @@ Definition recv : val :=
     end.
 
 (** * Setup of Iris's cameras *)
+Definition chanN := nroot .@ "chan".
+
 Class chanG Σ := {
   chanG_lockG :> lockG Σ;
-  chanG_authG :> inG Σ (excl_authR (listO valO));
+  chanG_protoG :> protoG Σ val;
 }.
-Definition chanΣ : gFunctors :=
-  #[ lockΣ; GFunctor (excl_authR (listO valO)) ].
+Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
 Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
+Record chan_name := ChanName {
+  chan_lock_name : gname;
+  chan_proto_name : proto_name;
+}.
+
+(** * Definition of the mapsto connective *)
+Notation iProto Σ := (iProto Σ val).
+
+Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
+    (c : val) (p : iProto Σ) : iProp Σ :=
+  ∃ γ s (l r : loc) (lk : val),
+    ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
+    is_lock chanN (chan_lock_name γ) lk (∃ vsl vsr,
+      llist sbi_internal_eq l vsl ∗
+      llist sbi_internal_eq r vsr ∗
+      iProto_ctx (chan_proto_name γ) vsl vsr) ∗
+    iProto_own (chan_proto_name γ) s p.
+Definition iProto_mapsto_aux : seal (@iProto_mapsto_def). by eexists. Qed.
+Definition iProto_mapsto := iProto_mapsto_aux.(unseal).
+Definition iProto_mapsto_eq :
+  @iProto_mapsto = @iProto_mapsto_def := iProto_mapsto_aux.(seal_eq).
+Arguments iProto_mapsto {_ _ _} _ _%proto.
+Instance: Params (@iProto_mapsto) 4 := {}.
+Notation "c ↣ p" := (iProto_mapsto c p)
+  (at level 20, format "c  ↣  p").
+
+Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
+    (p1 p2 : iProto Σ) : iProto Σ :=
+  (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
+Typeclasses Opaque iProto_branch.
+Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
+Instance: Params (@iProto_branch) 2 := {}.
+Infix "<{ P1 }+{ P2 }>" := (iProto_branch Send P1 P2) (at level 85) : proto_scope.
+Infix "<{ P1 }&{ P2 }>" := (iProto_branch Receive P1 P2) (at level 85) : proto_scope.
+Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
+Infix "<&{ P2 }>" := (iProto_branch Receive True P2) (at level 85) : proto_scope.
+Infix "<{ P1 }+>" := (iProto_branch Send P1 True) (at level 85) : proto_scope.
+Infix "<{ P1 }&>" := (iProto_branch Receive P1 True) (at level 85) : proto_scope.
+Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
+Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
+
 Section channel.
-  Context `{!heapG Σ, !chanG Σ} (N : namespace).
-
-  Record chan_name := Chan_name {
-    chan_lock_name : gname;
-    chan_l_name : gname;
-    chan_r_name : gname
-  }.
-
-  (** * The logical connectives *)
-  Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
-    (∃ ls rs,
-      llist sbi_internal_eq l ls ∗ own (chan_l_name γ) (●E ls) ∗
-      llist sbi_internal_eq r rs ∗ own (chan_r_name γ) (●E rs))%I.
-  Typeclasses Opaque chan_inv.
-
-  Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
-    (∃ (l r : loc) (lk : val),
-      ⌜ c1 = ((#l, #r), lk)%V ∧ c2 = ((#r, #l), lk)%V ⌝ ∗
-      is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
-
-  Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
-  Proof. by apply _. Qed.
-
-  Lemma chan_inv_alt s γ l r :
-    chan_inv γ l r ⊣⊢ ∃ ls rs,
-      llist sbi_internal_eq (side_elim s l r) ls ∗
-      own (side_elim s chan_l_name chan_r_name γ) (●E ls) ∗
-      llist sbi_internal_eq (side_elim s r l) rs ∗
-      own (side_elim s chan_r_name chan_l_name γ) (●E rs).
+  Context `{!heapG Σ, !chanG Σ}.
+  Implicit Types p : iProto Σ.
+  Implicit Types TT : tele.
+
+  Global Instance iProto_mapsto_ne c : NonExpansive (iProto_mapsto c).
+  Proof. rewrite iProto_mapsto_eq. solve_proper. Qed.
+  Global Instance iProto_mapsto_proper c : Proper ((≡) ==> (≡)) (iProto_mapsto c).
+  Proof. apply (ne_proper _). Qed.
+
+  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ iProto_le p1 p2 -∗ c ↣ p2.
   Proof.
-    destruct s; rewrite /chan_inv //=.
-    iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
+    rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
+    iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+    by iApply (iProto_own_le with "H").
   Qed.
 
-  Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
-    own (side_elim s chan_l_name chan_r_name γ) (◯E vs)%I.
+  Global Instance iProto_branch_contractive n a :
+    Proper (dist_later n ==> dist_later n ==>
+            dist_later n ==> dist_later n ==> dist n) (@iProto_branch Σ a).
+  Proof.
+    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
+    apply iProto_message_contractive=> /= -[] //.
+  Qed.
+  Global Instance iProto_branch_ne n a :
+    Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_branch Σ a).
+  Proof.
+    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
+    by apply iProto_message_ne=> /= -[].
+  Qed.
+  Global Instance iProto_branch_proper a :
+    Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_branch Σ a).
+  Proof.
+    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
+    by apply iProto_message_proper=> /= -[].
+  Qed.
 
-  (** * The proof rules *)
-  Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
-  Proof. by apply _. Qed.
+  Lemma iProto_dual_branch a P1 P2 p1 p2 :
+    iProto_dual (iProto_branch a P1 P2 p1 p2)
+    ≡ iProto_branch (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
+  Proof.
+    rewrite /iProto_branch iProto_dual_message /=.
+    by apply iProto_message_proper=> /= -[].
+  Qed.
+
+  Lemma iProto_app_branch a P1 P2 p1 p2 q :
+    (iProto_branch a P1 P2 p1 p2 <++> q)%proto
+    ≡ (iProto_branch a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
+  Proof.
+    rewrite /iProto_branch iProto_app_message.
+    by apply iProto_message_proper=> /= -[].
+  Qed.
 
-  Lemma new_chan_spec :
+  (** ** Specifications of [send] and [recv] *)
+  Lemma new_chan_spec p :
     {{{ True }}}
       new_chan #()
-    {{{ c1 c2 γ, RET (c1,c2); is_chan γ c1 c2 ∗ chan_own γ Left [] ∗ chan_own γ Right [] }}}.
+    {{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
+  Proof.
+    iIntros (Φ _) "HΦ". wp_lam.
+    wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (l) "Hl".
+    wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (r) "Hr".
+    iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
+    wp_apply (newlock_spec chanN (∃ vsl vsr,
+      llist sbi_internal_eq l vsl ∗ llist sbi_internal_eq r vsr ∗
+      iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
+    { iExists [], []. iFrame. }
+    iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
+    set (γ := ChanName γlk γp). iSplitL "Hcl".
+    - rewrite iProto_mapsto_eq. iExists γ, Left, l, r, lk. by iFrame "Hcl #".
+    - rewrite iProto_mapsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
+  Qed.
+
+  Lemma start_chan_spec p Φ (f : val) :
+    ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
+    ▷ (∀ c, c ↣ p -∗ Φ c) -∗
+    WP start_chan f {{ Φ }}.
+  Proof.
+    iIntros "Hfork HΦ". wp_lam.
+    wp_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
+    wp_apply (wp_fork with "[Hfork Hc2]").
+    { iNext. wp_apply ("Hfork" with "Hc2"). }
+    wp_pures. iApply ("HΦ" with "Hc1").
+  Qed.
+
+  Lemma send_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) (x : TT) :
+    {{{ c ↣ iProto_message Send pc ∗ (pc x).1.2 }}}
+      send c (pc x).1.1
+    {{{ RET #(); c ↣ (pc x).2 }}}.
+  Proof.
+    rewrite iProto_mapsto_eq. iIntros (Φ) "[Hc Hpc] HΦ". wp_lam; wp_pures.
+    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+    wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
+    - iMod (iProto_send_l with "Hctx H Hpc") as "[Hctx H]".
+      wp_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
+      wp_apply (llength_spec with "[$Hr //]"); iIntros "Hr".
+      wp_apply skipN_spec.
+      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
+    - iMod (iProto_send_r with "Hctx H Hpc") as "[Hctx H]".
+      wp_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
+      wp_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
+      wp_apply skipN_spec.
+      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
+  Qed.
+
+  (** A version written without Texan triples that is more convenient to use
+  (via [iApply] in Coq. *)
+  Lemma send_proto_spec {TT} Φ c v (pc : TT → val * iProp Σ * iProto Σ) :
+    c ↣ iProto_message Send pc -∗
+    (∃.. x : TT,
+      ⌜ v = (pc x).1.1 ⌝ ∗ (pc x).1.2 ∗ ▷ (c ↣ (pc x).2 -∗ Φ #())) -∗
+    WP send c v {{ Φ }}.
+  Proof.
+    iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΦ]".
+    by iApply (send_spec_packed with "[$]").
+  Qed.
+
+  Lemma try_recv_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
+    {{{ c ↣ iProto_message Receive pc }}}
+      try_recv c
+    {{{ v, RET v; (⌜v = NONEV⌝ ∧ c ↣ iProto_message Receive pc) ∨
+                  (∃ x : TT, ⌜v = SOMEV ((pc x).1.1)⌝ ∗ c ↣ (pc x).2 ∗ (pc x).1.2) }}}.
+  Proof.
+    rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+    wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
+    - wp_apply (lisnil_spec with "Hr"); iIntros "Hr".
+      destruct vsr as [|vr vsr]; wp_pures.
+      { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+        iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
+        iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
+      wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
+      iMod (iProto_recv_l with "Hctx H") as "H". wp_pures.
+      iDestruct "H" as (x ->) "(Hctx & H & Hpc)".
+      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
+      iFrame "Hpc". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
+    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+      destruct vsl as [|vl vsl]; wp_pures.
+      { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+        iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
+        iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
+      wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
+      iMod (iProto_recv_r with "Hctx H") as "H". wp_pures.
+      iDestruct "H" as (x ->) "(Hctx & H & Hpc)".
+      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+      iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
+      iFrame "Hpc". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
+  Qed.
+
+  Lemma recv_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
+    {{{ c ↣ iProto_message Receive pc }}}
+      recv c
+    {{{ x, RET (pc x).1.1; c ↣ (pc x).2 ∗ (pc x).1.2 }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
-    wp_lam.
-    wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
-    wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
-    iMod (own_alloc (●E [] ⋅ ◯E [])) as (lsγ) "[Hls Hls']".
-    { by apply excl_auth_valid. }
-    iMod (own_alloc (●E [] ⋅ ◯E [])) as (rsγ) "[Hrs Hrs']".
-    { by apply excl_auth_valid. }
-    wp_apply (newlock_spec N (∃ ls rs,
-      llist sbi_internal_eq l ls ∗ own lsγ (●E ls) ∗
-      llist sbi_internal_eq r rs ∗ own rsγ (●E rs))%I with "[Hl Hr Hls Hrs]").
-    { eauto 10 with iFrame. }
-    iIntros (lk γlk) "#Hlk". wp_pures.
-    iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
-    rewrite /chan_inv /=. eauto 20 with iFrame.
+    iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
+    wp_apply (try_recv_spec_packed with "Hc"); iIntros (v) "[[-> H]|H]".
+    { wp_pures. by iApply ("IH" with "[$]"). }
+    iDestruct "H" as (x ->) "[Hc Hpc]". wp_pures. iApply "HΦ". iFrame.
   Qed.
 
-  Lemma send_spec Φ E γ c1 c2 v s :
-    is_chan γ c1 c2 -∗
-    (|={⊤,E}=> ∃ vs,
-      chan_own γ s vs ∗
-      ▷ (chan_own γ s (vs ++ [v]) ={E,⊤}=∗ ▷ ▷ Φ #())) -∗
-    WP send (side_elim s c1 c2) v {{ Φ }}.
+  (** A version written without Texan triples that is more convenient to use
+  (via [iApply] in Coq. *)
+  Lemma recv_proto_spec {TT} Φ c (pc : TT → val * iProp Σ * iProto Σ) :
+    c ↣ iProto_message Receive pc -∗
+    ▷ (∀.. x : TT, c ↣ (pc x).2 -∗ (pc x).1.2 -∗ Φ (pc x).1.1) -∗
+    WP recv c {{ Φ }}.
   Proof.
-    iIntros "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
-    assert (side_elim s (#l, #r, lk)%V (#r, #l, lk)%V =
-      ((#(side_elim s l r), #(side_elim s r l)), lk)%V) as -> by (by destruct s).
-    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
-    iDestruct (chan_inv_alt s with "Hinv") as
-      (vs ws) "(Hll & Hvs & Href' & Hws)".
-    wp_seq. wp_bind (Fst (_,_)%V)%E.
-    iMod "HΦ" as (vs') "[Hchan HΦ]".
-    iDestruct (own_valid_2 with "Hvs Hchan") as %<-%excl_auth_agreeL.
-    iMod (own_update_2 _ _ _ (●E (vs ++ [v]) ⋅ _) with "Hvs Hchan") as "[Hvs Hchan]".
-    { apply excl_auth_update. }
-    wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro.
-    wp_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll".
-    wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
-    iApply (chan_inv_alt s).
-    rewrite /llist. eauto 20 with iFrame.
+    iIntros "Hc H". iApply (recv_spec_packed with "[$]").
+    iIntros "!>" (x) "[Hc HP]". iDestruct (bi_tforall_forall with "H") as "H".
+    iApply ("H" with "[$] [$]").
   Qed.
 
-  Lemma try_recv_spec Φ E γ c1 c2 s :
-    is_chan γ c1 c2 -∗
-    ((|={⊤,E}▷=> ▷ Φ NONEV) ∧
-     (|={⊤,E}=> ∃ vs,
-       chan_own γ s vs ∗
-       ▷ (∀ v vs', ⌜ vs = v :: vs' ⌝ -∗
-                   chan_own γ s vs' ={E,⊤,⊤}▷=∗ ▷ Φ (SOMEV v)))) -∗
-    WP try_recv (side_elim s c2 c1) {{ Φ }}.
+  (** ** Specifications for branching *)
+  Lemma select_spec c (b : bool) P1 P2 p1 p2 :
+    {{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}
+      send c #b
+    {{{ RET #(); c ↣ (if b then p1 else p2) }}}.
   Proof.
-    iIntros "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
-    assert (side_elim s (#r, #l, lk)%V (#l, #r, lk)%V =
-      ((#(side_elim s r l), #(side_elim s l r)), lk)%V) as -> by (by destruct s).
-    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
-    iDestruct (chan_inv_alt s with "Hinv")
-      as (vs ws) "(Hll & Hvs & Href' & Hws)".
-    wp_seq. wp_bind (Fst (_,_)%V)%E. destruct vs as [|v vs]; simpl.
-    - iDestruct "HΦ" as "[>HΦ _]". wp_pures. iMod "HΦ"; iModIntro.
-      wp_apply (lisnil_spec with "Hll"); iIntros "Hll". wp_pures.
-      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
-      { iApply (chan_inv_alt s).
-        rewrite /llist. eauto 10 with iFrame. }
-      iIntros (_). by wp_pures.
-    - iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]".
-      iDestruct (own_valid_2 with "Hvs Hvs'") as %<-%excl_auth_agreeL.
-      iMod (own_update_2 _ _ _ (●E vs ⋅ _) with "Hvs Hvs'") as "[Hvs Hvs']".
-      { apply excl_auth_update. }
-      wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
-      wp_apply (lisnil_spec with "Hll"); iIntros "Hll". iMod "HΦ".
-      wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
-      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
-      { iApply (chan_inv_alt s).
-        rewrite /llist. eauto 10 with iFrame. }
-      iIntros (_). by wp_pures.
+    rewrite /iProto_branch. iIntros (Φ) "[Hc HP] HΦ".
+    iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
   Qed.
 
-  Lemma recv_spec Φ E γ c1 c2 s :
-    is_chan γ c1 c2 -∗
-    (|={⊤,E}=> ∃ vs,
-      chan_own γ s vs ∗
-      ▷ ∀ v vs', ⌜ vs = v :: vs' ⌝ -∗
-                 chan_own γ s vs' ={E,⊤,⊤}▷=∗ ▷ Φ v) -∗
-    WP recv (side_elim s c2 c1) {{ Φ }}.
+  Lemma branch_spec c P1 P2 p1 p2 :
+    {{{ c ↣ (p1 <{P1}&{P2}> p2) }}}
+      recv c
+    {{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}.
   Proof.
-    iIntros "#Hc HΦ". iLöb as "IH". wp_lam.
-    wp_apply (try_recv_spec _ E with "Hc")=> //. iSplit.
-    - iMod (fupd_intro_mask' _ E) as "Hclose"; first done. iIntros "!> !>".
-      iMod "Hclose" as %_; iIntros "!> !>". wp_pures. by iApply "IH".
-    - iMod "HΦ" as (vs) "[Hvs HΦ]". iExists vs; iFrame "Hvs".
-      iIntros "!> !>" (v vs' ->) "Hvs".
-      iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !>". iMod "HΦ".
-      iIntros "!> !>". by wp_pures.
+    rewrite /iProto_branch. iIntros (Φ) "Hc HΦ".
+    iApply (recv_proto_spec with "Hc"); simpl.
+    iIntros "!>" (b) "Hc HP". iApply "HΦ". iFrame.
   Qed.
 End channel.

theories/channel/proofmode.v

@@ -9,7 +9,7 @@ In addition to the tactics for symbolic execution, this file defines the tactic
 recursive protocols are contractive. *)
 From iris.heap_lang Require Export proofmode notation.
 From iris.proofmode Require Export tactics.
-From actris Require Export proto_channel.
+From actris Require Export channel.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 
 (** * Tactics for proving contractiveness of protocols *)
@@ -56,7 +56,7 @@ Notation ProtoUnfold p1 p2 := (∀ d pas q,
   ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
 
 Section classes.
-  Context `{!proto_chanG Σ, !heapG Σ}.
+  Context `{!chanG Σ, !heapG Σ}.
   Implicit Types p : iProto Σ.
   Implicit Types TT : tele.
 
@@ -163,7 +163,7 @@ End classes.
 
 (** * Symbolic execution tactics *)
 (* TODO: Maybe strip laters from other hypotheses in the future? *)
-Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K
+Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K
     c p (pc : TT → val * iProp Σ * iProto Σ) Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (iProto_message Receive pc) →
@@ -241,7 +241,7 @@ Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_i
     simple_intropattern(x8) ")" constr(pat) :=
   wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
-Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
+Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
     c v p (pc : TT → val * iProp Σ * iProto Σ) Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (iProto_message Send pc) →
@@ -337,7 +337,7 @@ Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")
   wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
                 eexists x6; eexists x7; eexists x8) with pat.
 
-Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K
+Lemma tac_wp_branch `{!chanG Σ, !heapG Σ} Δ i j K
     c p P1 P2 (p1 p2 : iProto Σ) Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (p1 <{P1}&{P2}> p2) →
@@ -385,7 +385,7 @@ Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" "%" simple_in
   wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
 Tactic Notation "wp_branch" := wp_branch as %_ | %_.
 
-Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K
+Lemma tac_wp_select `{!chanG Σ, !heapG Σ} Δ neg i js K
     c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
   ProtoNormalize false p [] (p1 <{P1}+{P2}> p2) →

theories/channel/proto_channel.v → theories/channel/proto.v

-(** 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.
-- It defines the connective [c ↣ prot] for ownership of channel endpoints.
-- It proves Actris's specifications of [send] and [receive] w.r.t. dependent
-  separation protocols.
+(** 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 are defined by instantiating the parameterized
-version in [proto_model] with type of values [val] of HeapLang and the
-propositions [iProp] of Iris.
-
-In doing so we define ways of constructing instances of the instantiated type
-via two constructors:
+version in [proto_model] with 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 a continuation to construct
   the corresponding message protocols.
@@ -26,57 +19,43 @@ 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 as described in proto_model.v
 
-An encoding of the usual branching connectives [prot1 <{Q1}+{Q2}> prot2] and
-[prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in this
-file.
-
-The logical connective for protocol ownership is denoted as [c ↣ prot]. It
-describes that channel endpoint [c] adheres to protocol [prot]. This connective
-is modeled using Iris invariants and ghost state along with the logical
-connectives of the channel encodings [is_chan] and [chan_own].
-
 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 actris.channel Require Export channel. 
-From actris.channel Require Import proto_model.
-From iris.base_logic.lib Require Import invariants.
-From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl_auth.
+From iris.bi Require Import telescopes.
+From iris.program_logic Require Import language.
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import lib.own.
+From actris.channel Require Import proto_model.
 Export action.
 
-Definition start_chan : val := λ: "f",
-  let: "cc" := new_chan #() in
-  Fork ("f" (Snd "cc"));; Fst "cc".
-
 (** * Setup of Iris's cameras *)
-Class proto_chanG Σ := {
-  proto_chanG_chanG :> chanG Σ;
-  proto_chanG_authG :> inG Σ (excl_authR (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))));
-}.
-
-Definition proto_chanΣ := #[
-  chanΣ;
-  GFunctor (authRF (optionURF (exclRF (laterOF (protoOF val idOF idOF)))))
+Class protoG Σ V :=
+  protoG_authG :>
+    inG Σ (excl_authR (laterO (proto (leibnizO V) (iPrePropO Σ) (iPrePropO Σ)))).
+
+Definition protoΣ V := #[
+  GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
 ].
-Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ → proto_chanG Σ.
-Proof. intros [??%subG_inG]%subG_inv. constructor; apply _. Qed.
+Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
+Proof. solve_inG. Qed.
 
 (** * Types *)
-Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
+Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
 Delimit Scope proto_scope with proto.
 Bind Scope proto_scope with iProto.
 
 (** * Operators *)
-Definition iProto_end_def {Σ} : iProto Σ := proto_end.
+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 {_}.
+Arguments iProto_end {_ _}.
 
-Program Definition iProto_message_def {Σ} {TT : tele} (a : action)
-    (pc : TT → val * iProp Σ * iProto Σ) : iProto Σ :=
+Program Definition iProto_message_def {Σ V} {TT : tele} (a : action)
+    (pc : TT → V * iProp Σ * iProto Σ V) : iProto Σ V :=
   proto_message a (λ v, λne f, ∃ x : TT,
     (** We need the later to make [iProto_message] contractive *)
     ⌜ v = (pc x).1.1 ⌝ ∗
@@ -87,8 +66,8 @@ 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 {_ _} _ _%proto.
-Instance: Params (@iProto_message) 3 := {}.
+Arguments iProto_message {_ _ _} _ _%proto.
+Instance: Params (@iProto_message) 4 := {}.
 
 Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
   (iProto_message
@@ -166,37 +145,22 @@ Notation "<?> 'MSG' v ; p" :=
 Notation "'END'" := iProto_end : proto_scope.
 
 (** * Operations *)
-Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
+Definition iProto_dual {Σ V} (p : iProto Σ V) : iProto Σ V :=
   proto_map action_dual cid cid p.
-Arguments iProto_dual {_} _%proto.
-Instance: Params (@iProto_dual) 1 := {}.
-Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ :=
+Arguments iProto_dual {_ _} _%proto.
+Instance: Params (@iProto_dual) 2 := {}.
+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.
-Instance: Params (@iProto_dual_if) 2 := {}.
-
-Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
-    (p1 p2 : iProto Σ) : iProto Σ :=
-  (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
-Typeclasses Opaque iProto_branch.
-Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
-Instance: Params (@iProto_branch) 2 := {}.
-Infix "<{ P1 }+{ P2 }>" := (iProto_branch Send P1 P2) (at level 85) : proto_scope.
-Infix "<{ P1 }&{ P2 }>" := (iProto_branch Receive P1 P2) (at level 85) : proto_scope.
-Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
-Infix "<&{ P2 }>" := (iProto_branch Receive True P2) (at level 85) : proto_scope.
-Infix "<{ P1 }+>" := (iProto_branch Send P1 True) (at level 85) : proto_scope.
-Infix "<{ P1 }&>" := (iProto_branch Receive P1 True) (at level 85) : proto_scope.
-Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
-Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
-
-Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2.
-Arguments iProto_app {_} _%proto _%proto.
-Instance: Params (@iProto_app) 1 := {}.
+Arguments iProto_dual_if {_ _} _ _%proto.
+Instance: Params (@iProto_dual_if) 3 := {}.
+
+Definition iProto_app {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V := proto_app p1 p2.
+Arguments iProto_app {_ _} _%proto _%proto.
+Instance: Params (@iProto_app) 2 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 
 (** * Auxiliary definitions and invariants *)
-Definition proto_eq_next {Σ} (p : iProto Σ) : laterO (iProto Σ) -n> iPropO Σ :=
+Definition proto_eq_next {Σ V} (p : iProto Σ V) : laterO (iProto Σ V) -n> iPropO Σ :=
   OfeMor (sbi_internal_eq (Next p)).
 
 (*
@@ -219,8 +183,8 @@ Example:
 ------------------------------------
    ?P.?Q.!R <: !R.?P.?Q
 *)
-Definition iProto_le_pre {Σ}
-    (rec : iProto Σ → iProto Σ → iProp Σ) (p1 p2 : iProto Σ) : iProp Σ :=
+Definition iProto_le_pre {Σ V}
+    (rec : iProto Σ V → iProto Σ V→ iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
   (p1 ≡ proto_end ∗ p2 ≡ proto_end) ∨
   ∃ a1 a2 pc1 pc2,
     p1 ≡ proto_message a1 pc1 ∗
@@ -242,25 +206,26 @@ Definition iProto_le_pre {Σ}
            pc2' v1 (proto_eq_next pt)
     | Send, Receive => False
     end.
-Instance iProto_le_pre_ne {Σ} (rec : iProto Σ → iProto Σ → iProp Σ) :
+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' {Σ}
-    (rec : iProto Σ -n> iProto Σ -n> iPropO Σ) : iProto Σ -n> iProto Σ -n> iPropO Σ :=
+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 {Σ} : Contractive (@iProto_le_pre' Σ).
+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 {Σ} (p1 p2 : iProto Σ) : iProp Σ := fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_} _%proto _%proto.
-Instance: Params (@iProto_le) 1 := {}.
+Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ := fixpoint iProto_le_pre' p1 p2.
+Arguments iProto_le {_ _} _%proto _%proto.
+Instance: Params (@iProto_le) 2 := {}.
 
-Fixpoint proto_interp_aux {Σ} (n : nat)
-    (vsl vsr : list val) (pl pr : iProto Σ) : iProp Σ :=
+Fixpoint iProto_interp_aux {Σ V} (n : nat)
+    (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
   match n with
   | 0 => ∃ p,
      ⌜ vsl = [] ⌝ ∗
@@ -272,73 +237,56 @@ Fixpoint proto_interp_aux {Σ} (n : nat)
        ⌜ vsl = vl :: vsl' ⌝ ∗
        iProto_le (proto_message Receive pc) pr ∗
        pc vl (proto_eq_next p2') ∗
-       proto_interp_aux n vsl' vsr pl p2') ∨
+       iProto_interp_aux n vsl' vsr pl p2') ∨
      (∃ vr vsr' pc p1',
        ⌜ vsr = vr :: vsr' ⌝ ∗
        iProto_le (proto_message Receive pc) pl ∗
        pc vr (proto_eq_next p1') ∗
-       proto_interp_aux n vsl vsr' p1' pr)
+       iProto_interp_aux n vsl vsr' p1' pr)
   end.
-Definition proto_interp {Σ} (vsl vsr : list val) (pl pr : iProto Σ) : iProp Σ :=
-  proto_interp_aux (length vsl + length vsr) vsl vsr pl pr.
-Arguments proto_interp {_} _ _ _%proto _%proto : simpl nomatch.
-
-Record proto_name := ProtName {
-  proto_c_name : chan_name;
-  proto_l_name : gname;
-  proto_r_name : gname
-}.
-
-Definition to_pre_proto {Σ} (p : iProto Σ) :
-    proto val (iPrePropO Σ) (iPrePropO Σ) :=
-  proto_map id iProp_fold iProp_unfold p.
-
-Definition proto_own_frag `{!proto_chanG Σ} (γ : proto_name) (s : side)
-    (p : iProto Σ) : iProp Σ :=
-  own (side_elim s proto_l_name proto_r_name γ) (◯E (Next (to_pre_proto p))).
+Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
+  iProto_interp_aux (length vsl + length vsr) vsl vsr pl pr.
+Arguments iProto_interp {_ _} _ _ _%proto _%proto : simpl nomatch.
 
-Definition proto_own_auth `{!proto_chanG Σ} (γ : proto_name) (s : side)
-    (p : iProto Σ) : iProp Σ :=
-  own (side_elim s proto_l_name proto_r_name γ) (●E (Next (to_pre_proto p))).
+Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
 
-Definition proto_inv `{!invG Σ, proto_chanG Σ} (γ : proto_name) : iProp Σ :=
-  ∃ vsl vsr pl pr,
-    chan_own (proto_c_name γ) Left vsl ∗
-    chan_own (proto_c_name γ) Right vsr ∗
-    proto_own_auth γ Left pl ∗
-    proto_own_auth γ Right pr ∗
-    ▷ proto_interp vsl vsr pl pr.
+Inductive side := Left | Right.
+Instance side_inhabited : Inhabited side := populate Left.
+Definition side_elim {A} (s : side) (l r : A) : A :=
+  match s with Left => l | Right => r end.
 
-Definition protoN := nroot .@ "proto".
+Definition iProto_unfold {Σ V} (p : iProto Σ V) : proto V (iPrePropO Σ) (iPrePropO Σ) :=
+  proto_map id iProp_fold iProp_unfold p.
+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 (iProto_unfold 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 (iProto_unfold p))).
+
+Definition iProto_ctx `{protoG Σ V}
+    (γ : proto_name) (vsl vsr : list V) : iProp Σ :=
+  ∃ pl pr,
+    iProto_own_auth γ Left pl ∗
+    iProto_own_auth γ Right pr ∗
+    ▷ iProto_interp vsl vsr pl pr.
 
 (** * The connective for ownership of channel ends *)
-Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
-    (c : val) (p : iProto Σ) : iProp Σ :=
-  ∃ s (c1 c2 : val) γ p',
-    ⌜ c = side_elim s c1 c2 ⌝ ∗
-    iProto_le p' p ∗
-    proto_own_frag γ s p' ∗
-    is_chan protoN (proto_c_name γ) c1 c2 ∗
-    inv protoN (proto_inv γ).
-Definition mapsto_proto_aux : seal (@mapsto_proto_def). by eexists. Qed.
-Definition mapsto_proto {Σ pΣ hΣ} := mapsto_proto_aux.(unseal) Σ pΣ hΣ.
-Definition mapsto_proto_eq :
-  @mapsto_proto = @mapsto_proto_def := mapsto_proto_aux.(seal_eq).
-Arguments mapsto_proto {_ _ _} _ _%proto.
-Instance: Params (@mapsto_proto) 4 := {}.
-
-Notation "c ↣ p" := (mapsto_proto c p)
-  (at level 20, format "c  ↣  p").
+Definition iProto_own `{!protoG Σ V}
+    (γ : proto_name) (s : side) (p : iProto Σ V) : iProp Σ :=
+  ∃ p', iProto_le p' p ∗ iProto_own_frag γ s p'.
+Arguments iProto_own {_ _ _} _ _%proto.
+Instance: Params (@iProto_own) 3 := {}.
 
 (** * Proofs *)
 Section proto.
-  Context `{!proto_chanG Σ, !heapG Σ}.
-  Implicit Types p pl pr : iProto Σ.
+  Context `{!protoG Σ V}.
+  Implicit Types p pl pr : iProto Σ V.
   Implicit Types TT : tele.
 
   (** ** Non-expansiveness of operators *)
   Lemma iProto_message_contractive {TT} a
-      (pc1 pc2 : TT → val * iProp Σ * iProto Σ) n :
+      (pc1 pc2 : TT → V * iProp Σ * iProto Σ V) n :
     (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
     (∀.. x, dist_later n ((pc1 x).1.2) ((pc2 x).1.2)) →
     (∀.. x, dist_later n ((pc1 x).2) ((pc2 x).2)) →
@@ -349,8 +297,7 @@ Section proto.
     f_equiv=> v f /=. apply bi.exist_ne=> x.
     repeat (apply Hv || apply HP || apply Hp || f_contractive || f_equiv).
   Qed.
-  Lemma iProto_message_ne {TT} a
-      (pc1 pc2 : TT → val * iProp Σ * iProto Σ) n :
+  Lemma iProto_message_ne {TT} a (pc1 pc2 : TT → V * iProp Σ * iProto Σ V) n :
     (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
     (∀.. x, (pc1 x).1.2 ≡{n}≡ (pc2 x).1.2) →
     (∀.. x, (pc1 x).2 ≡{n}≡ (pc2 x).2) →
@@ -359,8 +306,7 @@ Section proto.
     rewrite !tforall_forall=> Hv HP Hp.
     apply iProto_message_contractive; apply tforall_forall; eauto using dist_dist_later.
   Qed.
-  Lemma iProto_message_proper {TT} a
-      (pc1 pc2 : TT → val * iProp Σ * iProto Σ) :
+  Lemma iProto_message_proper {TT} a (pc1 pc2 : TT → V * iProp Σ * iProto Σ V) :
     (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
     (∀.. x, (pc1 x).1.2 ≡ (pc2 x).1.2) →
     (∀.. x, (pc1 x).2 ≡ (pc2 x).2) →
@@ -370,46 +316,26 @@ Section proto.
     apply iProto_message_ne; apply tforall_forall=> x; by try apply equiv_dist.
   Qed.
 
-  Global Instance iProto_branch_contractive n a :
-    Proper (dist_later n ==> dist_later n ==>
-            dist_later n ==> dist_later n ==> dist n) (@iProto_branch Σ a).
-  Proof.
-    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
-    apply iProto_message_contractive=> /= -[] //.
-  Qed.
-  Global Instance iProto_branch_ne n a :
-    Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_branch Σ a).
-  Proof.
-    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
-    by apply iProto_message_ne=> /= -[].
-  Qed.
-  Global Instance iProto_branch_proper a :
-    Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_branch Σ a).
-  Proof.
-    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
-    by apply iProto_message_proper=> /= -[].
-  Qed.
-
   (** ** Dual *)
-  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
+  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
   Proof. solve_proper. Qed.
-  Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ).
+  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 Σ d).
+  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 Σ d).
+  Global Instance iProto_dual_if_proper d : Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
   Proof. apply (ne_proper _). Qed.
 
-  Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ).
+  Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
   Proof.
     intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
     apply: proto_map_ext=> //. by intros [].
   Qed.
 
-  Lemma iProto_dual_end : iProto_dual (Σ:=Σ) END ≡ END%proto.
+  Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END%proto.
   Proof. by rewrite iProto_end_eq /iProto_dual proto_map_end. Qed.
 
-  Lemma iProto_dual_message {TT} a (pc : TT → val * iProp Σ * iProto Σ) :
+  Lemma iProto_dual_message {TT} a (pc : TT → V * iProp Σ * iProto Σ V) :
     iProto_dual (iProto_message a pc)
     ≡ iProto_message (action_dual a) (prod_map id iProto_dual ∘ pc).
   Proof.
@@ -417,23 +343,16 @@ Section proto.
     by f_equiv=> v f /=.
   Qed.
 
-  Lemma iProto_dual_branch a P1 P2 p1 p2 :
-    iProto_dual (iProto_branch a P1 P2 p1 p2)
-    ≡ iProto_branch (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
-  Proof.
-    rewrite /iProto_branch iProto_dual_message /=.
-    by apply iProto_message_proper=> /= -[].
-  Qed.
-
   (** Helpers for duals *)
-  Global Instance proto_eq_next_ne : NonExpansive (proto_eq_next (Σ:=Σ)).
+  Global Instance proto_eq_next_ne : NonExpansive (proto_eq_next (Σ:=Σ) (V:=V)).
   Proof. solve_proper. Qed.
-  Global Instance proto_eq_next_proper : Proper ((≡) ==> (≡)) (proto_eq_next (Σ:=Σ)).
+  Global Instance proto_eq_next_proper :
+    Proper ((≡) ==> (≡)) (proto_eq_next (Σ:=Σ) (V:=V)).
   Proof. solve_proper. Qed.
 
   Lemma proto_eq_next_dual p :
-    ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid (proto_eq_next (iProto_dual p)) ≡
-    proto_eq_next p.
+    ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid
+      (proto_eq_next (iProto_dual p)) ≡ proto_eq_next p.
   Proof.
     intros lp. iSplit; iIntros "Hlp /="; last by iRewrite -"Hlp".
     destruct (Next_uninj lp) as [p' ->].
@@ -451,12 +370,12 @@ Section proto.
   Qed.
 
   (** ** Append *)
-  Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ).
+  Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
   Proof. apply _. Qed.
-  Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ).
+  Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
   Proof. apply (ne_proper_2 _). Qed.
 
-  Lemma iProto_app_message {TT} a (pc : TT → val * iProp Σ * iProto Σ) p2 :
+  Lemma iProto_app_message {TT} a (pc : TT → V * iProp Σ * iProto Σ V) p2 :
     (iProto_message a pc <++> p2)%proto
     ≡ iProto_message a (prod_map id (flip iProto_app p2) ∘ pc).
   Proof.
@@ -464,33 +383,25 @@ Section proto.
     by f_equiv=> v f /=.
   Qed.
 
-  Global Instance iProto_app_end_l : LeftId (≡) END%proto (@iProto_app Σ).
+  Global Instance iProto_app_end_l : LeftId (≡) END%proto (@iProto_app Σ V).
   Proof.
     intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_l.
   Qed.
-  Global Instance iProto_app_end_r : RightId (≡) END%proto (@iProto_app Σ).
+  Global Instance iProto_app_end_r : RightId (≡) END%proto (@iProto_app Σ V).
   Proof.
     intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
   Qed.
-  Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ).
+  Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
   Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.
 
-  Lemma iProto_app_branch a P1 P2 p1 p2 q :
-    (iProto_branch a P1 P2 p1 p2 <++> q)%proto
-    ≡ (iProto_branch a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
-  Proof.
-    rewrite /iProto_branch iProto_app_message.
-    by apply iProto_message_proper=> /= -[].
-  Qed.
-
   Lemma iProto_dual_app p1 p2 :
     iProto_dual (p1 <++> p2) ≡ (iProto_dual p1 <++> iProto_dual p2)%proto.
   Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed.
 
   (** ** Protocol entailment **)
-  Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ).
+  Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ V).
   Proof. solve_proper. Qed.
-  Global Instance iProto_le_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ).
+  Global Instance iProto_le_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
   Proof. solve_proper. Qed.
 
   Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2 ≡ iProto_le_pre iProto_le p1 p2.
@@ -591,8 +502,8 @@ Section proto.
       iExists p3'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle").
   Qed.
 
-  Lemma iProto_send_le {TT1 TT2} (pc1 : TT1 → val * iProp Σ * iProto Σ)
-      (pc2 : TT2 → val * iProp Σ * iProto Σ) :
+  Lemma iProto_send_le {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+      (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
     (∀.. x2 : TT2, ▷ (pc2 x2).1.2 -∗ ∃.. x1 : TT1,
       ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌝ ∗
       ▷ (pc1 x1).1.2 ∗
@@ -608,8 +519,8 @@ Section proto.
     iExists x1. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
   Qed.
 
-  Lemma iProto_recv_le {TT1 TT2} (pc1 : TT1 → val * iProp Σ * iProto Σ)
-      (pc2 : TT2 → val * iProp Σ * iProto Σ) :
+  Lemma iProto_recv_le {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+      (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
     (∀.. x1 : TT1, ▷ (pc1 x1).1.2 -∗ ∃.. x2 : TT2,
       ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌝ ∗
       ▷ (pc2 x2).1.2 ∗
@@ -624,8 +535,8 @@ Section proto.
     iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
   Qed.
 
-  Lemma iProto_swap {TT1 TT2} (v1 : TT1 → val) (v2 : TT2 → val)
-      (P1 : TT1 → iProp Σ) (P2 : TT2 → iProp Σ) (p : TT1 → TT2 → iProto Σ) :
+  Lemma iProto_swap {TT1 TT2} (v1 : TT1 → V) (v2 : TT2 → V)
+      (P1 : TT1 → iProp Σ) (P2 : TT2 → iProp Σ) (p : TT1 → TT2 → iProto Σ V) :
     ⊢ iProto_le (iProto_message Receive (λ x1,
                   (v1 x1, P1 x1, iProto_message Send (λ x2, (v2 x2, P2 x2, p x1 x2)))))
                 (iProto_message Send (λ x2,
@@ -670,56 +581,44 @@ Section proto.
       iExists (iProto_dual p2''). rewrite proto_eq_next_dual. iFrame.
   Qed.
 
-  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ iProto_le p1 p2 -∗ c ↣ p2.
-  Proof.
-    rewrite mapsto_proto_eq. iDestruct 1 as (s c1 c2 γ p1' ->) "[Hle H]".
-    iIntros "Hle'". iExists s, c1, c2, γ, p1'. iSplit; first done. iFrame "H".
-    by iApply (iProto_le_trans with "Hle").
-  Qed.
-
   (** ** Lemmas about the auxiliary definitions and invariants *)
-  Global Instance proto_interp_aux_ne n vsl vsr :
-    NonExpansive2 (proto_interp_aux (Σ:=Σ) n vsl vsr).
+  Global Instance iProto_interp_aux_ne n vsl vsr :
+    NonExpansive2 (iProto_interp_aux (Σ:=Σ) (V:=V) n vsl vsr).
   Proof. revert vsl vsr. induction n; solve_proper. Qed.
-  Global Instance proto_interp_aux_proper n vsl vsr :
-    Proper ((≡) ==> (≡) ==> (≡)) (proto_interp_aux (Σ:=Σ) n vsl vsr).
+  Global Instance iProto_interp_aux_proper n vsl vsr :
+    Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp_aux (Σ:=Σ) (V:=V) n vsl vsr).
   Proof. apply (ne_proper_2 _). Qed.
-  Global Instance proto_interp_ne vsl vsr : NonExpansive2 (proto_interp (Σ:=Σ) vsl vsr).
+  Global Instance iProto_interp_ne vsl vsr :
+    NonExpansive2 (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
   Proof. solve_proper. Qed.
-  Global Instance proto_interp_proper vsl vsr :
-    Proper ((≡) ==> (≡) ==> (≡)) (proto_interp (Σ:=Σ) vsl vsr).
+  Global Instance iProto_interp_proper vsl vsr :
+    Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
   Proof. apply (ne_proper_2 _). Qed.
 
-  Global Instance to_pre_proto_ne : NonExpansive (to_pre_proto (Σ:=Σ)).
+  Global Instance iProto_unfold_ne : NonExpansive (iProto_unfold (Σ:=Σ) (V:=V)).
   Proof. solve_proper. Qed.
-  Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
+  Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
   Proof. solve_proper. Qed.
-  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
-  Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
-  Global Instance mapsto_proto_proper c : Proper ((≡) ==> (≡)) (mapsto_proto c).
-  Proof. apply (ne_proper _). Qed.
 
-  Lemma proto_own_auth_agree γ s p p' :
-    proto_own_auth γ s p -∗ proto_own_frag γ s p' -∗ ▷ (p ≡ p').
+  Lemma iProto_own_auth_agree γ s p p' :
+    iProto_own_auth γ s p -∗ iProto_own_frag γ s p' -∗ ▷ (p ≡ p').
   Proof.
-    iIntros "Hauth Hfrag".
-    iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
-    iDestruct (excl_auth_agreeI with "Hvalid") as "Hvalid".
-    iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext.
-    rewrite /to_pre_proto. assert (∀ p,
+    iIntros "H● H◯". iDestruct (own_valid_2 with "H● H◯") as "H✓".
+    iDestruct (excl_auth_agreeI with "H✓") as "H✓".
+    iDestruct (bi.later_eq_1 with "H✓") as "H✓"; iNext.
+    rewrite /iProto_unfold. assert (∀ p,
       proto_map id iProp_unfold iProp_fold (proto_map id iProp_fold iProp_unfold p) ≡ p) as help.
     { intros p''. rewrite -proto_map_compose -{2}(proto_map_id p'').
       apply proto_map_ext=> // pc /=; by rewrite iProp_fold_unfold. }
-    rewrite -{2}(help p). iRewrite "Hvalid". by rewrite help.
+    rewrite -{2}(help p). iRewrite "H✓". by rewrite help.
   Qed.
 
-  Lemma proto_own_auth_update γ s p p' p'' :
-    proto_own_auth γ s p -∗ proto_own_frag γ s p' ==∗
-    proto_own_auth γ s p'' ∗ proto_own_frag γ s p''.
+  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 "Hauth Hfrag".
-    iDestruct (own_update_2 with "Hauth Hfrag") as "H".
-    { eapply (excl_auth_update _ _ (Next (to_pre_proto p''))). }
+    iIntros "H● H◯". iDestruct (own_update_2 with "H● H◯") as "H".
+    { eapply (excl_auth_update _ _ (Next (iProto_unfold p''))). }
     by rewrite own_op.
   Qed.
 
@@ -732,8 +631,8 @@ Section proto.
     (φ1 ↔ φ2) → (φ1 → φ2 → P1 ⊣⊢ P2) → (⌜φ1⌝ ∗ P1) ⊣⊢ (⌜φ2⌝ ∗ P2).
   Proof. intros -> HP. iSplit; iDestruct 1 as (Hϕ) "H"; rewrite HP; auto. Qed.
 
-  Lemma proto_interp_unfold vsl vsr pl pr :
-    proto_interp vsl vsr pl pr ⊣⊢
+  Lemma iProto_interp_unfold vsl vsr pl pr :
+    iProto_interp vsl vsr pl pr ⊣⊢
       (∃ p,
         ⌜ vsl = [] ⌝ ∗
         ⌜ vsr = [] ⌝ ∗
@@ -743,14 +642,14 @@ Section proto.
         ⌜ vsl = vl :: vsl' ⌝ ∗
         iProto_le (proto_message Receive pc) pr ∗
         pc vl (proto_eq_next pr') ∗
-        proto_interp vsl' vsr pl pr') ∨
+        iProto_interp vsl' vsr pl pr') ∨
       (∃ vr vsr' pc pl',
         ⌜ vsr = vr :: vsr' ⌝ ∗
         iProto_le (proto_message Receive pc) pl ∗
         pc vr (proto_eq_next pl') ∗
-        proto_interp vsl vsr' pl' pr).
+        iProto_interp vsl vsr' pl' pr).
   Proof.
-    rewrite {1}/proto_interp. destruct vsl as [|vl vsl]; simpl.
+    rewrite {1}/iProto_interp. destruct vsl as [|vl vsl]; simpl.
     - destruct vsr as [|vr vsr]; simpl.
       + iSplit; first by auto.
         iDestruct 1 as "[H | [H | H]]"; first by auto.
@@ -766,18 +665,18 @@ Section proto.
         by rewrite ?Nat.add_succ_r.
   Qed.
 
-  Lemma proto_interp_nil p : ⊢ proto_interp [] [] p (iProto_dual p).
+  Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
   Proof.
-    rewrite proto_interp_unfold. iLeft. iExists p. do 2 (iSplit; [done|]).
+    rewrite iProto_interp_unfold. iLeft. iExists p. do 2 (iSplit; [done|]).
     iSplitL; iApply iProto_le_refl.
   Qed.
 
-  Lemma proto_interp_flip vsl vsr pl pr :
-    proto_interp vsl vsr pl pr -∗ proto_interp vsr vsl pr pl.
+  Lemma iProto_interp_flip vsl vsr pl pr :
+    iProto_interp vsl vsr pl pr -∗ iProto_interp vsr vsl pr pl.
   Proof.
     remember (length vsl + length vsr) as n eqn:Hn.
     iInduction (lt_wf n) as [n _] "IH" forall (vsl vsr pl pr Hn); subst.
-    rewrite !proto_interp_unfold. iIntros "[H|[H|H]]".
+    rewrite !iProto_interp_unfold. iIntros "[H|[H|H]]".
     - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
       iLeft. iExists (iProto_dual p). rewrite involutive. iFrame; auto.
     - iDestruct "H" as (vl vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
@@ -788,12 +687,12 @@ Section proto.
       iApply ("IH" with "[%] [//] H"); simpl; lia.
   Qed.
 
-  Lemma proto_interp_le_l vsl vsr pl pl' pr :
-    proto_interp vsl vsr pl pr -∗ iProto_le pl pl' -∗ proto_interp vsl vsr pl' pr.
+  Lemma iProto_interp_le_l vsl vsr pl pl' pr :
+    iProto_interp vsl vsr pl pr -∗ iProto_le pl pl' -∗ iProto_interp vsl vsr pl' pr.
   Proof.
     remember (length vsl + length vsr) as n eqn:Hn.
     iInduction (lt_wf n) as [n _] "IH" forall (vsl vsr pl pr Hn); subst.
-    rewrite !proto_interp_unfold. iIntros "[H|[H|H]] Hle".
+    rewrite !iProto_interp_unfold. iIntros "[H|[H|H]] Hle".
     - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
       iLeft. iExists p. do 2 (iSplit; [done|]). iFrame "Hp'".
       by iApply (iProto_le_trans with "Hp").
@@ -804,34 +703,34 @@ Section proto.
       iRight; iRight. iExists vr, vsr', pc', pl''. iSplit; [done|]; iFrame.
       by iApply (iProto_le_trans with "Hpl").
   Qed.
-  Lemma proto_interp_le_r vsl vsr pl pr pr' :
-    proto_interp vsl vsr pl pr -∗ iProto_le pr pr' -∗ proto_interp vsl vsr pl pr'.
+  Lemma iProto_interp_le_r vsl vsr pl pr pr' :
+    iProto_interp vsl vsr pl pr -∗ iProto_le pr pr' -∗ iProto_interp vsl vsr pl pr'.
   Proof.
-    iIntros "H Hle". iApply proto_interp_flip.
-    iApply (proto_interp_le_l with "[H] Hle"). by iApply proto_interp_flip.
+    iIntros "H Hle". iApply iProto_interp_flip.
+    iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_flip.
   Qed.
 
-  Lemma proto_interp_send vl pcl vsl vsr pl pr pl' :
-    proto_interp vsl vsr pl pr -∗
+  Lemma iProto_interp_send vl pcl vsl vsr pl pr pl' :
+    iProto_interp vsl vsr pl pr -∗
     iProto_le pl (proto_message Send pcl) -∗
     pcl vl (proto_eq_next pl') -∗
-    ▷^(length vsr) proto_interp (vsl ++ [vl]) vsr pl' pr.
+    ▷^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
   Proof.
-    iIntros "H Hle". iDestruct (proto_interp_le_l with "H Hle") as "H".
+    iIntros "H Hle". iDestruct (iProto_interp_le_l with "H Hle") as "H".
     clear pl. iIntros "Hpcl". remember (length vsl + length vsr) as n eqn:Hn.
     iInduction (lt_wf n) as [n _] "IH" forall (pcl vsl vsr pr pl' Hn); subst.
-    rewrite {1}proto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
+    rewrite {1}iProto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
     - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
       iDestruct (iProto_dual_le with "Hp") as "Hp".
       iDestruct (iProto_le_trans with "Hp Hp'") as "Hp".
       rewrite /iProto_dual proto_map_message /=.
-      iApply proto_interp_unfold. iRight; iLeft.
+      iApply iProto_interp_unfold. iRight; iLeft.
       iExists vl, [], _, (iProto_dual pl'). iSplit; [done|]. iFrame "Hp"; simpl.
-      rewrite proto_eq_next_dual. iFrame "Hpcl". iApply proto_interp_nil.
+      rewrite proto_eq_next_dual. iFrame "Hpcl". iApply iProto_interp_nil.
     - iDestruct "H" as (vl' vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
       iDestruct ("IH" with "[%] [//] H Hpcl") as "H"; [simpl; lia|].
-      iNext. iApply (proto_interp_le_r with "[-Hpr] Hpr"); clear pr.
-      iApply proto_interp_unfold. iRight; iLeft.
+      iNext. iApply (iProto_interp_le_r with "[-Hpr] Hpr"); clear pr.
+      iApply iProto_interp_unfold. iRight; iLeft.
       iExists vl', (vsl' ++ [vl]), pc', pr'. iFrame.
       iSplit; [done|]. iApply iProto_le_refl.
     - iDestruct "H" as (vr' vsr' pc' pl'' ->) "(Hle & Hpcl' & H) /=".
@@ -840,271 +739,145 @@ Section proto.
       iRewrite ("Hpc" $! vr' (proto_eq_next pl'')) in "Hpcl'"; clear pc'.
       iDestruct ("Hle" with "Hpcl' Hpcl")
         as (pc1 pc2 pt) "(Hpl'' & Hpl' & Hpc1 & Hpc2)".
-      iNext. iDestruct (proto_interp_le_l with "H Hpl''") as "H".
+      iNext. iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
       iDestruct ("IH" with "[%] [//] H Hpc1") as "H"; [simpl; lia|..].
-      iNext. iApply proto_interp_unfold. iRight; iRight.
+      iNext. iApply iProto_interp_unfold. iRight; iRight.
       iExists vr', vsr', _, pt. iSplit; [done|]. by iFrame.
   Qed.
 
-  Lemma proto_interp_recv vl vsl vsr pl pr pcr :
-    proto_interp (vl :: vsl) vsr pl pr -∗
+  Lemma iProto_interp_recv vl vsl vsr pl pr pcr :
+    iProto_interp (vl :: vsl) vsr pl pr -∗
     iProto_le pr (proto_message Receive pcr) -∗
-    ∃ pr, pcr vl (proto_eq_next pr) ∗ ▷ proto_interp vsl vsr pl pr.
+    ∃ pr, pcr vl (proto_eq_next pr) ∗ ▷ iProto_interp vsl vsr pl pr.
   Proof.
-    iIntros "H Hle". iDestruct (proto_interp_le_r with "H Hle") as "H".
+    iIntros "H Hle". iDestruct (iProto_interp_le_r with "H Hle") as "H".
     clear pr. remember (length vsr) as n eqn:Hn.
     iInduction (lt_wf n) as [n _] "IH" forall (vsr pl Hn); subst.
-    rewrite !proto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
+    rewrite !iProto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
     - iClear "IH". iDestruct "H" as (p [=]) "_".
     - iClear "IH". iDestruct "H" as (vl' vsl' pc' pr' [= -> ->]) "(Hpr & Hpc' & Hinterp)".
       iDestruct (iProto_le_recv_inv with "Hpr") as (pc'') "[Hpc Hpr]".
       iDestruct (proto_message_equivI with "Hpc") as (_) "{Hpc} #Hpc".
       iDestruct ("Hpr" $! vl' pr' with "[Hpc']") as (pr'') "[Hler Hpr]".
       { by iRewrite -("Hpc" $! vl' (proto_eq_next pr')). }
-      iExists pr''. iFrame "Hpr". by iApply (proto_interp_le_r with "Hinterp").
+      iExists pr''. iFrame "Hpr". by iApply (iProto_interp_le_r with "Hinterp").
     - iDestruct "H" as (vr vsr' pc' pl'' ->) "(Hpl & Hpc' & Hinterp)".
       iDestruct ("IH" with "[%] [//] Hinterp") as (pr) "[Hpc Hinterp]"; [simpl; lia|].
       iExists pr. iFrame "Hpc".
-      iApply proto_interp_unfold. iRight; iRight. eauto 20 with iFrame.
+      iApply iProto_interp_unfold. iRight; iRight. eauto 20 with iFrame.
   Qed.
 
-  (** ** Helper lemma for initialization of a channel *)
-  Lemma proto_init E cγ c1 c2 p :
-    is_chan protoN cγ c1 c2 -∗
-    chan_own cγ Left [] -∗ chan_own cγ Right [] ={E}=∗
-    c1 ↣ p ∗ c2 ↣ iProto_dual p.
-  Proof.
-    iIntros "#? Hcol Hcor".
-    iMod (own_alloc (●E (Next (to_pre_proto p)) ⋅
-                     ◯E (Next (to_pre_proto p)))) as (lγ) "[Hlsta Hlstf]".
-    { by apply excl_auth_valid. }
-    iMod (own_alloc (●E (Next (to_pre_proto (iProto_dual p))) ⋅
-                     ◯E (Next (to_pre_proto (iProto_dual p))))) as (rγ) "[Hrsta Hrstf]".
-    { by apply excl_auth_valid. }
-    pose (ProtName cγ lγ rγ) as pγ.
-    iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf]") as "#?".
-    { iNext. iExists [], [], p, (iProto_dual p). iFrame.
-      iApply proto_interp_nil. }
-    iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
-    - iExists Left, c1, c2, pγ, p.
-      iFrame "Hlstf #". iSplit; [done|]. iApply iProto_le_refl.
-    - iExists Right, c1, c2, pγ, (iProto_dual p).
-      iFrame "Hrstf #". iSplit; [done|]. iApply iProto_le_refl.
-  Qed.
-
-  (** ** Accessor style lemmas, used as helpers to prove the specifications of
-  [send] and [recv]. *)
-  Lemma proto_send_acc {TT} c (pc : TT → val * iProp Σ * iProto Σ) (x : TT) :
-    c ↣ iProto_message Send pc -∗
-    (pc x).1.2 -∗
-    ∃ s c1 c2 γ,
-      ⌜ c = side_elim s c1 c2 ⌝ ∗
-      is_chan protoN (proto_c_name γ) c1 c2 ∗ |={⊤,⊤∖↑protoN}=> ∃ vs,
-        chan_own (proto_c_name γ) s vs ∗
-        ▷ (chan_own (proto_c_name γ) s (vs ++ [(pc x).1.1]) ={⊤∖↑protoN,⊤}=∗
-           c ↣ (pc x).2).
-  Proof.
-    rewrite {1}mapsto_proto_eq iProto_message_eq. iIntros "Hc Hpc".
-    iDestruct "Hc" as (s c1 c2 γ p ->) "(Hle & Hst & #[??])".
-    iExists s, c1, c2, γ. do 2 (iSplit; [done|]).
-    iInv protoN as (vsl vsr pl pr)
-      "(>Hcl & >Hcr & Hstla & Hstra & Hinterp)" "Hclose".
-    (* TODO: refactor to avoid twice nearly the same proof *)
-    iModIntro. destruct s.
-    - iExists _. iIntros "{$Hcl} !> Hcl".
-      iDestruct (proto_own_auth_agree with "Hstla Hst") as "#Hpl".
-      iAssert (▷ iProto_le pl (iProto_message_def Send pc))%I
-        with "[Hle]" as "{Hpl} Hlel"; first by (iNext; iRewrite "Hpl").
-      iDestruct (proto_interp_send ((pc x).1.1) with "Hinterp Hlel [Hpc]") as "Hinterp".
-      { iNext. iExists x. iFrame; auto. }
-      iMod (proto_own_auth_update _ _ _ _ (pc x).2 with "Hstla Hst") as "[Hstla Hst]".
-      iMod ("Hclose" with "[-Hst]") as "_".
-      { iNext. iExists _, _, _, _. iFrame. }
-      iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ, (pc x).2.
-      iFrame "Hst #". iSplit; [done|]. iApply iProto_le_refl.
-    - iExists _. iIntros "{$Hcr} !> Hcr".
-      iDestruct (proto_own_auth_agree with "Hstra Hst") as "#Hpr".
-      iAssert (▷ iProto_le pr (iProto_message_def Send pc))%I
-        with "[Hle]" as "{Hpr} Hler"; first by (iNext; iRewrite "Hpr").
-      iDestruct (proto_interp_flip with "Hinterp") as "Hinterp".
-      iDestruct (proto_interp_send ((pc x).1.1) with "Hinterp Hler [Hpc]") as "Hinterp".
-      { iNext. iExists x. iFrame; auto. }
-      iMod (proto_own_auth_update _ _ _ _ (pc x).2 with "Hstra Hst") as "[Hstra Hst]".
-      iMod ("Hclose" with "[-Hst]") as "_".
-      { iNext. iExists _, _, _, _. iFrame. by iApply proto_interp_flip. }
-      iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ, (pc x).2.
-      iFrame "Hst #". iSplit; [done|]. iApply iProto_le_refl.
-  Qed.
-
-  Lemma proto_recv_acc {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
-    c ↣ iProto_message Receive pc -∗
-    ∃ s c1 c2 γ,
-      ⌜ c = side_elim s c2 c1 ⌝ ∗
-      is_chan protoN (proto_c_name γ) c1 c2 ∗ |={⊤,⊤∖↑protoN}=> ∃ vs,
-        chan_own (proto_c_name γ) s vs ∗
-        ▷ ((chan_own (proto_c_name γ) s vs ={⊤∖↑protoN,⊤}=∗
-             c ↣ iProto_message Receive pc) ∧
-           (∀ v vs',
-             ⌜ vs = v :: vs' ⌝ -∗
-             chan_own (proto_c_name γ) s vs' ={⊤∖↑protoN,⊤}=∗ ▷ ▷ ∃ x : TT,
-             ⌜ v = (pc x).1.1 ⌝ ∗ c ↣ (pc x).2 ∗ (pc x).1.2)).
-  Proof.
-    rewrite {1}mapsto_proto_eq iProto_message_eq.
-    iDestruct 1 as (s c1 c2 γ p ->) "(Hle & Hst & #[??])".
-    iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
-    iSplit; [done|].
-    iInv protoN as (vsl vsr pl pr)
-      "(>Hcl & >Hcr & Hstla & Hstra & Hinterp)" "Hclose".
-    iExists (side_elim s vsr vsl). iModIntro.
-    (* TODO: refactor to avoid twice nearly the same proof *)
-    destruct s; simpl.
-    - iIntros "{$Hcr} !>".
-      iDestruct (proto_own_auth_agree with "Hstla Hst") as "#Hpl".
-      iSplit.
-      + iIntros "Hcr".
-        iMod ("Hclose" with "[-Hle Hst]") as "_".
-        { iNext. iExists vsl, vsr, _, _. iFrame. }
-        iModIntro. rewrite mapsto_proto_eq.
-        iExists Left, c1, c2, γ, p. iFrame; auto.
-      + iIntros (v vs ->) "Hcr".
-        iDestruct (proto_interp_flip with "Hinterp") as "Hinterp".
-        iDestruct (proto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
-        { iNext. by iRewrite "Hpl". }
-        iMod (proto_own_auth_update _ _ _ _ q with "Hstla Hst") as "[Hstla Hst]".
-        iMod ("Hclose" with "[-Hst Hpc]") as %_.
-        { iNext. iExists _, _, q, _. iFrame. by iApply proto_interp_flip. }
-        iIntros "!> !> !>". iDestruct "Hpc" as (x ->) "[Hpc #Hq'] /=".
-        iExists x. iSplit; [done|]. iFrame "Hpc". iRewrite -"Hq'".
-        rewrite mapsto_proto_eq. iExists Left, c1, c2, γ, q.
-        iFrame "Hst #". iSplit; [done|]. iApply iProto_le_refl.
-    - iIntros "{$Hcl} !>".
-      iDestruct (proto_own_auth_agree with "Hstra Hst") as "#Hpr".
-      iSplit.
-      + iIntros "Hcl".
-        iMod ("Hclose" with "[-Hle Hst]") as "_".
-        { iNext. iExists vsl, vsr, _, _. iFrame. }
-        iModIntro. rewrite mapsto_proto_eq.
-        iExists Right, c1, c2, γ, p. iFrame; auto.
-      + iIntros (v vs ->) "Hcl".
-        iDestruct (proto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
-        { iNext. by iRewrite "Hpr". }
-        iMod (proto_own_auth_update _ _ _ _ q with "Hstra Hst") as "[Hstra Hst]".
-        iMod ("Hclose" with "[-Hst Hpc]") as %_.
-        { iNext. iExists _, _, _, q. iFrame. }
-        iIntros "!> !> !>". iDestruct "Hpc" as (x ->) "[Hpc #Hq'] /=".
-        iExists x. iSplit; [done|]. iFrame "Hpc". iRewrite -"Hq'".
-        rewrite mapsto_proto_eq. iExists Right, c1, c2, γ, q.
-        iFrame "Hst #". iSplit; [done|]. iApply iProto_le_refl.
-  Qed.
-
-  (** ** Specifications of [send] and [recv] *)
-  Lemma new_chan_proto_spec :
-    {{{ True }}}
-      new_chan #()
-    {{{ c1 c2, RET (c1,c2); (∀ p, |={⊤}=> c1 ↣ p ∗ c2 ↣ iProto_dual p) }}}.
-  Proof.
-    iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
-    iIntros (c1 c2 γ) "(Hc & Hl & Hr)". iApply "HΨ"; iIntros "!>" (p).
-    iApply (proto_init ⊤ γ c1 c2 p with "Hc Hl Hr").
-  Qed.
-
-  Lemma start_chan_proto_spec p Ψ (f : val) :
-    ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
-    ▷ (∀ c, c ↣ p -∗ Ψ c) -∗
-    WP start_chan f {{ Ψ }}.
-  Proof.
-    iIntros "Hfork HΨ". wp_lam.
-    wp_apply (new_chan_proto_spec with "[//]"); iIntros (c1 c2) "Hc".
-    iMod ("Hc" $! p) as "[Hc1 Hc2]".
-    wp_apply (wp_fork with "[Hfork Hc2]").
-    { iNext. wp_apply ("Hfork" with "Hc2"). }
-    wp_pures. iApply ("HΨ" with "Hc1").
-  Qed.
-
-  Lemma send_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) (x : TT) :
-    {{{ c ↣ iProto_message Send pc ∗ (pc x).1.2 }}}
-      send c (pc x).1.1
-    {{{ RET #(); c ↣ (pc x).2 }}}.
-  Proof.
-    iIntros (Ψ) "[Hp HP] HΨ".
-    iDestruct (proto_send_acc with "Hp HP") as (γ s c1 c2 ->) "[#Hc Hvs]".
-    iApply (send_spec with "[$]"). iMod "Hvs" as (vs) "[Hch H]".
-    iModIntro. iExists vs. iFrame "Hch".
-    iIntros "!> Hvs". iApply "HΨ".
-    iMod ("H" with "Hvs"); auto.
-  Qed.
-
-  (** A version written without Texan triples that is more convenient to use
-  (via [iApply] in Coq. *)
-  Lemma send_proto_spec {TT} Ψ c v (pc : TT → val * iProp Σ * iProto Σ) :
-    c ↣ iProto_message Send pc -∗
-    (∃.. x : TT,
-      ⌜ v = (pc x).1.1 ⌝ ∗ (pc x).1.2 ∗ ▷ (c ↣ (pc x).2 -∗ Ψ #())) -∗
-    WP send c v {{ Ψ }}.
-  Proof.
-    iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΨ]".
-    by iApply (send_proto_spec_packed with "[$]").
-  Qed.
-
-  Lemma try_recv_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
-    {{{ c ↣ iProto_message Receive pc }}}
-      try_recv c
-    {{{ v, RET v; (⌜v = NONEV⌝ ∧ c ↣ iProto_message Receive pc) ∨
-                  (∃ x : TT, ⌜v = SOMEV ((pc x).1.1)⌝ ∗ c ↣ (pc x).2 ∗ (pc x).1.2) }}}.
-  Proof.
-    iIntros (Ψ) "Hp HΨ".
-    iDestruct (proto_recv_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]".
-    wp_apply (try_recv_spec with "[$]"). iSplit.
-    - iMod "Hvs" as (vs) "[Hch [H _]]".
-      iIntros "!> !>". iMod ("H" with "Hch") as "Hch". iApply "HΨ"; auto.
-    - iMod "Hvs" as (vs) "[Hch [_ H]]".
-      iIntros "!>". iExists vs. iIntros "{$Hch} !>" (v vs' ->) "Hch".
-      iMod ("H" with "[//] Hch") as "H". iIntros "!> !> !> !>".
-      iDestruct "H" as (x ->) "H". iApply "HΨ"; auto.
-  Qed.
-
-  Lemma recv_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
-    {{{ c ↣ iProto_message Receive pc }}}
-      recv c
-    {{{ x, RET (pc x).1.1; c ↣ (pc x).2 ∗ (pc x).1.2 }}}.
-  Proof.
-    iIntros (Ψ) "Hp HΨ".
-    iDestruct (proto_recv_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]".
-    wp_apply (recv_spec with "[$]"). iMod "Hvs" as (vs) "[Hch [_ H]]".
-    iModIntro. iExists vs. iIntros "{$Hch} !>" (v vs' ->) "Hvs'".
-    iMod ("H" with "[//] Hvs'") as "H"; iIntros "!> !> !> !>".
-    iDestruct "H" as (x ->) "H". by iApply "HΨ".
-  Qed.
-
-  (** A version written without Texan triples that is more convenient to use
-  (via [iApply] in Coq. *)
-  Lemma recv_proto_spec {TT} Ψ c (pc : TT → val * iProp Σ * iProto Σ) :
-    c ↣ iProto_message Receive pc -∗
-    ▷ (∀.. x : TT, c ↣ (pc x).2 -∗ (pc x).1.2 -∗ Ψ (pc x).1.1) -∗
-    WP recv c {{ Ψ }}.
-  Proof.
-    iIntros "Hc H". iApply (recv_proto_spec_packed with "[$]").
-    iIntros "!>" (x) "[Hc HP]". iDestruct (bi_tforall_forall with "H") as "H".
-    iApply ("H" with "[$] [$]").
-  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.
 
-  (** ** Specifications for branching *)
-  Lemma select_spec c (b : bool) P1 P2 p1 p2 :
-    {{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}
-      send c #b
-    {{{ RET #(); c ↣ (if b then p1 else p2) }}}.
+  Lemma iProto_own_le γ s p1 p2 :
+    iProto_own γ s p1 -∗ iProto_le p1 p2 -∗ iProto_own γ s p2.
   Proof.
-    rewrite /iProto_branch. iIntros (Ψ) "[Hc HP] HΨ".
-    iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
+    iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
+    iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
   Qed.
 
-  Lemma branch_spec c P1 P2 p1 p2 :
-    {{{ c ↣ (p1 <{P1}&{P2}> p2) }}}
-      recv c
-    {{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}.
+  Lemma iProto_init p :
+    ⊢ |==> ∃ γ,
+      iProto_ctx γ [] [] ∗
+      iProto_own γ Left p ∗ iProto_own γ Right (iProto_dual p).
   Proof.
-    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
-    iApply (recv_proto_spec with "Hc"); simpl.
-    iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
+    iMod (own_alloc (●E (Next (iProto_unfold p)) ⋅
+      ◯E (Next (iProto_unfold p)))) as (lγ) "[H●l H◯l]".
+    { by apply excl_auth_valid. }
+    iMod (own_alloc (●E (Next (iProto_unfold (iProto_dual p))) ⋅
+      ◯E (Next (iProto_unfold (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_interp_nil. }
+    iSplitL "H◯l"; iExists _; iFrame; iApply iProto_le_refl.
+  Qed.
+
+  Lemma iProto_send_l {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) (x : TT) vsr vsl :
+    iProto_ctx γ vsl vsr -∗
+    iProto_own γ Left (iProto_message Send pc) -∗
+    (pc x).1.2 ==∗
+      ▷^(length vsr) iProto_ctx γ (vsl ++ [(pc x).1.1]) vsr ∗
+      iProto_own γ Left (pc x).2.
+  Proof.
+    rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
+    iDestruct 1 as (p) "[Hle H◯]". iIntros "Hpc".
+    iDestruct (iProto_own_auth_agree with "H●l H◯") as "#Hp".
+    iAssert (▷ iProto_le pl (iProto_message_def Send pc))%I
+      with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
+    iDestruct (iProto_interp_send ((pc x).1.1) with "Hinterp Hle [Hpc]") as "Hinterp".
+    { simpl. auto. }
+    iMod (iProto_own_auth_update _ _ _ _ (pc x).2 with "H●l H◯") as "[H●l H◯]".
+    iIntros "!>". iSplitR "H◯".
+    - iIntros "!>". iExists (pc x).2, pr. iFrame.
+    - iExists (pc x).2. iFrame. iApply iProto_le_refl.
+  Qed.
+
+  Lemma iProto_send_r {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) (x : TT) vsr vsl :
+    iProto_ctx γ vsl vsr -∗
+    iProto_own γ Right (iProto_message Send pc) -∗
+    (pc x).1.2 ==∗
+      ▷^(length vsl) iProto_ctx γ vsl (vsr ++ [(pc x).1.1]) ∗
+      iProto_own γ Right (pc x).2.
+  Proof.
+    rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
+    iDestruct 1 as (p) "[Hle H◯]". iIntros "Hpc".
+    iDestruct (iProto_own_auth_agree with "H●r H◯") as "#Hp".
+    iAssert (▷ iProto_le pr (iProto_message_def Send pc))%I
+      with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
+    iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
+    iDestruct (iProto_interp_send ((pc x).1.1) with "Hinterp Hle [Hpc]") as "Hinterp".
+    { simpl. auto. }
+    iMod (iProto_own_auth_update _ _ _ _ (pc x).2 with "H●r H◯") as "[H●r H◯]".
+    iIntros "!>". iSplitR "H◯".
+    - iIntros "!>". iExists pl, (pc x).2. iFrame. by iApply iProto_interp_flip.
+    - iExists (pc x).2. iFrame. iApply iProto_le_refl.
+  Qed.
+
+  Lemma iProto_recv_l {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) vr vsr vsl :
+    iProto_ctx γ vsl (vr :: vsr) -∗
+    iProto_own γ Left (iProto_message Receive pc) ==∗
+    ▷ ▷ ∃ (x : TT),
+      ⌜ vr = (pc x).1.1 ⌝ ∗
+      iProto_ctx γ vsl vsr ∗
+      iProto_own γ Left (pc x).2 ∗
+      (pc x).1.2.
+  Proof.
+    rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
+    iDestruct 1 as (p) "[Hle H◯]".
+    iDestruct (iProto_own_auth_agree with "H●l H◯") as "#Hp".
+    iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
+    iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
+    { iNext. by iRewrite "Hp". }
+    iMod (iProto_own_auth_update _ _ _ _ q with "H●l H◯") as "[H●l H◯]".
+    iIntros "!> !> !>". iDestruct "Hpc" as (x ->) "[Hpc #Hq] /=".
+    iExists x. iSplit; [done|]. iFrame "Hpc". iSplitR "H◯".
+    - iExists q, pr. iFrame. by iApply iProto_interp_flip.
+    - iRewrite -"Hq". iExists q. iFrame. iApply iProto_le_refl.
+  Qed.
+
+  Lemma iProto_recv_r {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) vl vsr vsl :
+    iProto_ctx γ (vl :: vsl) vsr -∗
+    iProto_own γ Right (iProto_message Receive pc) ==∗
+    ▷ ▷ ∃ (x : TT),
+      ⌜ vl = (pc x).1.1 ⌝ ∗
+      iProto_ctx γ vsl vsr ∗
+      iProto_own γ Right (pc x).2 ∗
+      (pc x).1.2.
+  Proof.
+    rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
+    iDestruct 1 as (p) "[Hle H◯]".
+    iDestruct (iProto_own_auth_agree with "H●r H◯") as "#Hp".
+    iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
+    { iNext. by iRewrite "Hp". }
+    iMod (iProto_own_auth_update _ _ _ _ q with "H●r H◯") as "[H●r H◯]".
+    iIntros "!> !> !>". iDestruct "Hpc" as (x ->) "[Hpc #Hq] /=".
+    iExists x. iSplit; [done|]. iFrame "Hpc". iSplitR "H◯".
+    - iExists pl, q. iFrame.
+    - iRewrite -"Hq". iExists q. iFrame. iApply iProto_le_refl.
   Qed.
 End proto.
+
+Typeclasses Opaque iProto_ctx iProto_own.

theories/channel/proto_model.v

-(** This file defines the model of dependent separation protocols, along with
-various operations, such as append and map.
+(** 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_channel] should be used.
+[proto] should be used.
 
 Dependent Separation Protocols are modeled as the solution of the following
 recursive domain equation:

theories/examples/basics.v

 (** This file includes basic examples that each describe a unique feature of 
 dependent separation protocols. *)
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation lib.spin_lock.
+From actris.channel Require Import proofmode.
+From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import contribution.
 
 (** Basic *)
@@ -87,7 +87,7 @@ Definition prog_lock : val := λ: <>,
   recv "c" + recv "c".
 
 Section proofs.
-Context `{heapG Σ, proto_chanG Σ}.
+Context `{heapG Σ, chanG Σ}.
 
 (** Protocols for the respective programs *)
 Definition prot : iProto Σ :=
@@ -146,7 +146,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
 Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot); iIntros (c) "Hc".
+  wp_apply (start_chan_spec prot); iIntros (c) "Hc".
   - by wp_send with "[]".
   - wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -154,7 +154,7 @@ Qed.
 Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_ref); iIntros (c) "Hc".
+  wp_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
   - wp_alloc l as "Hl". by wp_send with "[$Hl]".
   - wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
 Qed.
@@ -162,17 +162,16 @@ Qed.
 Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_del); iIntros (c) "Hc".
-  - wp_apply (new_chan_proto_spec with "[//]").
-    iIntros (c2 c2') "Hcc2". iMod ("Hcc2" $! prot) as "[Hc2 Hc2']".
-    wp_send with "[$Hc2]". by wp_send with "[]".
+  wp_apply (start_chan_spec prot_del); iIntros (c) "Hc".
+  - wp_apply (new_chan_spec prot with "[//]").
+    iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
 Qed.
 
 Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_dep); iIntros (c) "Hc".
+  wp_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
   - wp_recv (x) as "_". by wp_send with "[]".
   - wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -180,7 +179,7 @@ Qed.
 Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_dep_ref); iIntros (c) "Hc".
+  wp_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
   - 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Φ".
@@ -189,9 +188,8 @@ Qed.
 Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_dep_del); iIntros (c) "Hc".
-  - wp_apply (new_chan_proto_spec with "[//]").
-    iIntros (c2 c2') "Hcc2". iMod ("Hcc2" $! prot_dep) as "[Hc2 Hc2']".
+  wp_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
+  - wp_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
     wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
     by iApply "HΦ".
@@ -200,9 +198,9 @@ Qed.
 Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_dep_del_2); iIntros (c) "Hc".
+  wp_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_apply (start_chan_proto_spec prot_dep); iIntros (c2) "Hc2".
+  wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -210,10 +208,10 @@ Qed.
 Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_dep_del_3); iIntros (c) "Hc".
+  wp_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_recv (y) as "_".
     wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_apply (start_chan_proto_spec prot_dep); iIntros (c2) "Hc2".
+  wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_send with "[//]".
   wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -222,7 +220,7 @@ Qed.
 Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_loop); iIntros (c) "Hc".
+  wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
   - iAssert (∀ Ψ, WP (rec: "go" <> := let: "x" := recv c in
       send c ("x" + #2) ;; "go" #())%V #() {{ Ψ }})%I with "[Hc]" as "H".
     { iIntros (Ψ). iLöb as "IH". wp_recv (x) as "_". wp_send with "[//]".
@@ -235,7 +233,7 @@ Qed.
 Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec prot_fun); iIntros (c) "Hc".
+  wp_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
   - wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
     iIntros "!>" (Ψ') "HP HΨ'". wp_apply ("Hf" with "HP"); iIntros (x) "HΨ".
     wp_pures. by iApply "HΨ'".
@@ -250,8 +248,8 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
   {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_proto_spec (prot_lock 2)); iIntros (c) "Hc".
-  - iMod (contribution_init) as (γ) "Hs".
+  wp_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
+  - iMod contribution_init as (γ) "Hs".
     iMod (alloc_client with "Hs") as "[Hs Hcl1]".
     iMod (alloc_client with "Hs") as "[Hs Hcl2]".
     wp_apply (newlock_spec nroot (∃ n, server γ n ε ∗

theories/examples/map.v

 (** This file implements a distributed mapper service, a specification thereof,
 and its proofs. *)
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation lib.spin_lock.
+From actris.channel Require Import proofmode.
+From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import llist contribution.
 From iris.algebra Require Import gmultiset.
 
@@ -60,7 +60,7 @@ Class mapG Σ A `{Countable A} := {
 
 Section map.
   Context `{Countable A} {B : Type}.
-  Context `{!heapG Σ, !proto_chanG Σ, !mapG Σ A}.
+  Context `{!heapG Σ, !chanG Σ, !mapG Σ A}.
   Context (IA : A → val → iProp Σ) (IB : B → val → iProp Σ) (map : A → list B).
   Local Open Scope nat_scope.
   Implicit Types n : nat.
@@ -202,7 +202,7 @@ Section map.
     {{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
   Proof.
     iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_apply (start_chan_proto_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
+    wp_apply (start_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
     { wp_apply (par_map_service_spec with "Hmap Hc"); auto. }
     wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
     wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.

theories/examples/map_reduce.v

 (** This file implements a simple distributed map-reduce function, a
 specification thereof, and its proofs. *)
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
 From actris.utils Require Import llist compare contribution group.
 From actris.examples Require Import map sort_fg.
 From iris.algebra Require Import gmultiset.
@@ -97,7 +96,7 @@ Class map_reduceG Σ A B `{Countable A, Countable B} := {
 
 Section mapper.
   Context `{Countable A, Countable B} {C : Type}.
-  Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B}.
+  Context `{!heapG Σ, !chanG Σ, !map_reduceG Σ A B}.
   Context (IA : A → val → iProp Σ) (IB : Z → B → val → iProp Σ) (IC : C → val → iProp Σ).
   Context (map : A → list (Z * B)) (red : Z → list B → list C).
   Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
@@ -282,10 +281,10 @@ Section mapper.
     {{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
   Proof.
     iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_apply (start_chan_proto_spec (par_map_protocol IA IZB map n ∅));
+    wp_apply (start_chan_spec (par_map_protocol IA IZB map n ∅));
       iIntros (cmap) "// Hcmap".
     { wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
-    wp_apply (start_chan_proto_spec (sort_fg_protocol IZB RZB <++> END)%proto);
+    wp_apply (start_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
       iIntros (csort) "Hcsort".
     { wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
       iApply RZB_cmp_spec. }
@@ -293,7 +292,7 @@ Section mapper.
     wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
     iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
     iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
-    wp_apply (start_chan_proto_spec (par_map_protocol IZBs IC (curry red) m ∅));
+    wp_apply (start_chan_spec (par_map_protocol IZBs IC (curry red) m ∅));
       iIntros (cred) "// Hcred".
     { wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
     wp_branch as %_|%Hnil; last first.

theories/examples/sort.v

@@ -6,8 +6,7 @@ thereof, and its proofs. There are two variants:
 - [sort_service_func]: a service that only takes a channel as its argument. The
   comparison function is sent over the channel. *)
 From stdpp Require Import sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
 From actris.utils Require Export llist compare.
 
 Definition lmerge : val :=
@@ -43,7 +42,7 @@ Definition sort_client_func : val := λ: "cmp" "xs",
   recv "c".
 
 Section sort.
-  Context `{!heapG Σ, !proto_chanG Σ}.
+  Context `{!heapG Σ, !chanG Σ}.
 
   Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop) : iProto Σ :=
     (<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
@@ -106,10 +105,10 @@ Section sort.
       wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
     wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
       iDestruct 1 as (->) "[Hl1 Hl2]".
-    wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cy) "Hcy".
+    wp_apply (start_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_apply ("IH" with "Hcy"); auto. }
-    wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cz) "Hcz".
+    wp_apply (start_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_apply ("IH" with "Hcz"); auto. }
     wp_send with "[$Hl1]".
@@ -142,7 +141,7 @@ Section sort.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_proto_spec sort_protocol_func); iIntros (c) "Hc".
+    wp_apply (start_chan_spec sort_protocol_func); iIntros (c) "Hc".
     { rewrite -(right_id END%proto _ (iProto_dual _)).
       wp_apply (sort_service_func_spec with "Hc"); auto. }
     wp_send with "[$Hcmp]".

theories/examples/sort_br_del.v

@@ -8,8 +8,7 @@ sort, demonstrating Actris's support for delegation and branching:
 - [sort_service_br_del]: a service that allows one to sort a series of list by
   forking itself. *)
 From stdpp Require Import sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
 From actris.examples Require Import sort.
 
 Definition sort_service_br : val :=
@@ -35,7 +34,7 @@ Definition sort_service_br_del : val :=
     else #().
 
 Section sort_service_br_del.
-  Context `{!heapG Σ, !proto_chanG Σ}.
+  Context `{!heapG Σ, !chanG Σ}.
   Context {A} (I : A → val → iProp Σ) (R : A → A → Prop) `{!RelDecision R, !Total R}.
 
   Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
@@ -77,8 +76,7 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_apply (start_chan_proto_spec (sort_protocol I R <++> END)%proto);
-        iIntros (c') "Hc'".
+    { wp_apply (start_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
       { wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
       wp_send with "[$Hc']". by wp_apply ("IH" with "Hc"). }
     by iApply "HΨ".
@@ -104,7 +102,7 @@ Section sort_service_br_del.
     { wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
       by wp_apply ("IH" with "Hc"). }
     wp_branch; wp_pures.
-    { wp_apply (start_chan_proto_spec sort_protocol_br_del); iIntros (c') "Hc'".
+    { wp_apply (start_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
       { wp_apply ("IH" with "Hc'"); auto. }
       wp_send with "[$Hc']".
       by wp_apply ("IH" with "Hc"). }

theories/examples/sort_fg.v

@@ -3,8 +3,7 @@ specification thereof, and its proofs. We call this version fine-grained because
 the lists are not transmitted using a single message, but using a series of
 messages. *)
 From stdpp Require Export sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
 From iris.heap_lang Require Import assert.
 From actris.utils Require Import llist compare.
 
@@ -73,7 +72,7 @@ Definition sort_client_fg : val := λ: "cmp" "xs",
   recv_all "c" "xs".
 
 Section sort_fg.
-  Context `{!heapG Σ, !proto_chanG Σ}.
+  Context `{!heapG Σ, !chanG Σ}.
 
   Section sort_fg_inner.
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
@@ -222,10 +221,10 @@ Section sort_fg.
     wp_rec; wp_pures. wp_branch; wp_pures.
     - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
       + wp_recv (x2 v2) as "HIx2".
-        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
+        wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
         { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
         iIntros (cy) "Hcy".
-        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
+        wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
         { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
         iIntros (cz) "Hcz". rewrite !right_id.
         wp_select. wp_send with "[$HIx1]".
@@ -241,7 +240,7 @@ Section sort_fg.
         wp_select. by iApply "HΨ".
     - wp_select. by iApply "HΨ".
   Qed.
-  
+
   Lemma send_all_spec c p xs' l xs :
     {{{ llist I l xs ∗ c ↣ (sort_fg_head_protocol xs' <++> p) }}}
       send_all c #l
@@ -282,8 +281,7 @@ Section sort_fg.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto);
-      iIntros (c) "Hc".
+    wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
     { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
     wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
     wp_select.