diff --git a/_CoqProject b/_CoqProject
index 5c69bc04d79f359dd109c4fe59fa04ade6b8245e..86b78cf9e64a125158e1245f22dc07842bb12ae8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,15 +1,12 @@
 -Q theories osiris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/utils/auth_excl.v
-theories/proto/encodable.v
-theories/proto/list.v
-theories/proto/channel.v
-theories/proto/involutive.v
-theories/proto/side.v
-theories/proto/proto_def.v
-theories/proto/proto_specs.v
-theories/proto/proto_enc.v
-theories/proto/branching.v
+theories/utils/encodable.v
+theories/utils/list.v
+theories/channel/channel.v
+theories/channel/proto_model.v
+theories/channel/proto_channel.v
+theories/channel/branching.v
 theories/examples/proofs_enc.v
 theories/examples/branching_proofs.v
 theories/examples/list_sort.v
diff --git a/theories/proto/branching.v b/theories/channel/branching.v
similarity index 98%
rename from theories/proto/branching.v
rename to theories/channel/branching.v
index 57a88d96b8a48282de408f370d95a6d637aa7395..d2781686e498beed1d9f8e40b12f4f2927541146 100644
--- a/theories/proto/branching.v
+++ b/theories/channel/branching.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Import proofmode notation.
-From osiris.proto Require Export proto_enc.
+From osiris.channel Require Export proto_channel.
 
 Definition TSB {PROP : bi} (a : action)
     (prot1 prot2 : proto val PROP) : proto val PROP :=
diff --git a/theories/proto/channel.v b/theories/channel/channel.v
similarity index 52%
rename from theories/proto/channel.v
rename to theories/channel/channel.v
index 2680930d4cc590e82549f446a31a1b0f54153746..a6acf89bf2b9fc377ae0e81a8c41fee59d39621e 100644
--- a/theories/proto/channel.v
+++ b/theories/channel/channel.v
@@ -1,44 +1,34 @@
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import excl auth list.
-From osiris.utils Require Import auth_excl.
-From osiris.proto Require Export side.
-From osiris.proto Require Import list.
+From osiris.utils Require Import auth_excl list.
 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.
+
 Definition new_chan : val :=
   λ: <>,
      let: "l" := ref (lnil #()) in
      let: "r" := ref (lnil #()) in
      let: "lk" := newlock #() in
-     (("l","r"),"lk").
-
-Coercion side_to_bool (s : side) : bool :=
-  match s with Left => true | Right => false end.
-Arguments side_to_bool : simpl never.
-Definition side_elim {A} (s : side) (l r : A) : A :=
-  match s with Left => l | Right => r end.
-
-Definition get_side : val := λ: "c" "s",
-  (if: "s" = #Left then Fst (Fst "c") else Snd (Fst "c"))%E.
-Definition get_lock : val := λ: "c", Snd "c".
-
-Definition get_dual_side : val := λ: "s",
-  (if: "s" = #Left then #Right else #Left)%E.
+     ((("l","r"),"lk"), (("r","l"),"lk")).
 
 Definition send : val :=
-  λ: "c" "s" "v",
-    let: "lk" := get_lock "c" in
+  λ: "c" "v",
+    let: "lk" := Snd "c" in
     acquire "lk";;
-    let: "l" := get_side "c" "s" in
+    let: "l" := Fst (Fst "c") in
     "l" <- lsnoc !"l" "v";;
     release "lk".
 
 Definition try_recv : val :=
-  λ: "c" "s",
-    let: "lk" := get_lock "c" in
+  λ: "c",
+    let: "lk" := Snd "c" in
     acquire "lk";;
-    let: "l" := get_side "c" (get_dual_side "s") in
+    let: "l" := Snd (Fst "c") in
     let: "ret" :=
       match: !"l" with
         SOME "p" => "l" <- Snd "p";; SOME (Fst "p")
@@ -47,10 +37,10 @@ Definition try_recv : val :=
     release "lk";; "ret".
 
 Definition recv : val :=
-  rec: "go" "c" "s" :=
-    match: try_recv "c" "s" with
+  rec: "go" "c" :=
+    match: try_recv "c" with
       SOME "p" => "p"
-    | NONE => "go" "c" "s"
+    | NONE => "go" "c"
     end.
 
 Class chanG Σ := {
@@ -80,12 +70,12 @@ Section channel.
       is_list_ref r rs ∗ own (chan_r_name γ) (● to_auth_excl rs))%I.
   Typeclasses Opaque chan_inv.
 
-  Definition is_chan (γ : chan_name) (c : val) : iProp Σ :=
+  Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
     (∃ l r lk : val,
-      ⌜c = ((l, r), lk)%V⌝ ∧
+      ⌜ 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 γ c).
+  Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
   Proof. by apply _. Qed.
 
   Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
@@ -94,24 +84,10 @@ Section channel.
   Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
   Proof. by apply _. Qed.
 
-  Lemma get_side_spec Φ s (l r lk : val) :
-    Φ (side_elim s l r) -∗
-    WP get_side ((l, r), lk)%V #s {{ Φ }}.
-  Proof. iIntros "?". wp_lam. by destruct s; wp_pures. Qed.
-
-  Lemma get_lock_spec Φ (l r lk : val) :
-    Φ lk -∗
-    WP get_lock ((l, r), lk)%V {{ Φ }}.
-  Proof. iIntros "?". wp_lam. by wp_pures. Qed.
-
-  Lemma dual_side_spec Φ s :
-    Φ #(dual_side s) -∗ WP get_dual_side #s {{ Φ }}.
-  Proof. iIntros "?". wp_lam. by destruct s; wp_pures. Qed.
-
   Lemma new_chan_spec :
     {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c; is_chan γ c ∗ chan_own γ Left [] ∗ chan_own γ Right [] }}}.
+    {{{ c1 c2 γ, RET (c1,c2); is_chan γ c1 c2 ∗ chan_own γ Left [] ∗ chan_own γ Right [] }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
     wp_lam.
@@ -131,7 +107,7 @@ Section channel.
                 with "[Hl Hr Hls Hrs]").
     { eauto 10 with iFrame. }
     iIntros (lk γlk) "#Hlk". wp_pures.
-    iApply ("HΦ" $! _ (Chan_name γlk lsγ rsγ)); simpl.
+    iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
     rewrite /chan_inv /=. eauto 20 with iFrame.
   Qed.
 
@@ -146,22 +122,23 @@ Section channel.
     iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
   Qed.
 
-  Lemma send_spec Φ E γ c v s :
-    is_chan γ c -∗
+  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 c #s v {{ Φ }}.
+      ▷ (chan_own γ s (vs ++ [v]) ={E,⊤}=∗ ▷ ▷ Φ #())) -∗
+    WP send (side_elim s c1 c2) v {{ Φ }}.
   Proof.
     iIntros "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (l r lk ->) "#Hlock"; wp_pures.
-    wp_apply get_lock_spec; 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]".
-    wp_apply get_side_spec; wp_pures.
+    wp_pures.
     iDestruct (chan_inv_alt s with "Hinv") as
-        (vs ws) "(Href & Hvs & Href' & Hws)".
+      (vs ws) "(Href & Hvs & Href' & Hws)".
     iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
-    wp_load. 
+    wp_load.
     wp_apply (lsnoc_spec (A:=val))=> //; iIntros (_).
     wp_bind (_ <- _)%E.
     iMod "HΦ" as (vs') "[Hchan HΦ]".
@@ -174,76 +151,56 @@ Section channel.
     rewrite /is_list_ref. eauto 20 with iFrame.
   Qed.
 
-  Lemma try_recv_spec Φ E γ c s :
-    is_chan γ c -∗
-    (|={⊤,E}=> ∃ vs,
-      chan_own γ (dual_side s) vs ∗
-      ▷ ((⌜vs = []⌝ -∗ chan_own γ (dual_side s) vs ={E,⊤}=∗ Φ NONEV) ∧
-         (∀ v vs', ⌜vs = v :: vs'⌝ -∗
-                   chan_own γ (dual_side s) vs' ={E,⊤}=∗ Φ (SOMEV v)))) -∗
-    WP try_recv c #s {{ Φ }}.
+  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) {{ Φ }}.
   Proof.
     iIntros "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (l r lk ->) "#Hlock"; wp_pures.
-    wp_apply get_lock_spec; wp_pures.
-    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]". wp_pures.
-    wp_apply dual_side_spec. wp_apply get_side_spec; wp_pures.
-    iDestruct (chan_inv_alt (dual_side s) with "Hinv") as
-        (vs ws) "(Href & Hvs & Href' & Hws)".
-    iDestruct "Href" as (ll Hslr) "Hll"; rewrite Hslr.
-    wp_bind (! _)%E.
-    iMod "HΦ" as (vs') "[Hchan HΦ]".
-    wp_load.
-    iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
-    destruct vs as [|v vs]; simpl.
-    - iDestruct "HΦ" as "[HΦ _]".
-      iMod ("HΦ" with "[//] Hchan") as "HΦ".
-      iModIntro.
+    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]".
+    wp_pures.
+    iDestruct (chan_inv_alt s with "Hinv")
+      as (vs ws) "(Href & Hvs & Href' & Hws)".
+    iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
+    wp_bind (! _)%E. destruct vs as [|v vs]; simpl.
+    - iDestruct "HΦ" as "[>HΦ _]". wp_load. iMod "HΦ"; iModIntro.
       wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
-      { iApply (chan_inv_alt (dual_side s)).
+      { iApply (chan_inv_alt s).
         rewrite /is_list_ref. eauto 10 with iFrame. }
-      iIntros (_). wp_pures. by iApply "HΦ".
-    - iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
-      iDestruct "HΦ" as "[_ HΦ]".
-      iMod ("HΦ" with "[//] Hchan") as "HΦ".
-      iModIntro. wp_store.
+      iIntros (_). by wp_pures.
+    - iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]".
+      iDestruct (excl_eq with "Hvs Hvs'") as %<-%leibniz_equiv.
+      iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']".
+      wp_load.
+      iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
+      wp_store; wp_pures.
       wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
-      { iApply (chan_inv_alt (dual_side s)).
+      { iApply (chan_inv_alt s).
         rewrite /is_list_ref. eauto 10 with iFrame. }
-      iIntros (_). wp_pures. by iApply "HΦ".
+      iIntros (_). by wp_pures.
   Qed.
 
-  Lemma recv_spec Φ E γ c s :
-    is_chan γ c -∗
-    (□ (|={⊤,E}=> ∃ vs,
-      chan_own γ (dual_side s) vs ∗
-        ▷ ((⌜vs = []⌝ -∗ chan_own γ (dual_side s) vs ={E,⊤}=∗ True) ∗
-          (∀ v vs', ⌜vs = v :: vs'⌝ -∗
-                    chan_own γ (dual_side s) vs' ={E,⊤}=∗ Φ v)))) -∗
-    WP recv c #s {{ Φ }}.
+  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) {{ Φ }}.
   Proof.
-    iIntros "#Hc #HΦ".
-    rewrite /recv.
-    iLöb as "IH".
-    wp_apply (try_recv_spec with "Hc")=> //.
-    iMod "HΦ" as (vs) "[Hchan [HΦfail HΦsucc]]".
-    iModIntro.
-    iExists _.
-    iFrame.
-    iNext.
-    iSplitL "HΦfail".
-    - iIntros "Hvs Hown".
-      iRename ("HΦfail") into "HΦ".
-      iDestruct ("HΦ" with "Hvs Hown") as "HΦ".
-      iMod ("HΦ") as "HΦ".
-      iModIntro.
-      wp_match.
-      by iApply ("IH").
-    - iRename ("HΦsucc") into "HΦ".
-      iIntros (v vs') "Hvs Hown".
-      iMod ("HΦ" with "Hvs Hown") as "HΦ".
-      iModIntro.
-      by wp_pures.
+    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 "!> !> !>". by wp_pures.
   Qed.
-
-End channel.
\ No newline at end of file
+End channel.
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
new file mode 100644
index 0000000000000000000000000000000000000000..24507560e51a55471a194db7a64d93a445e6800e
--- /dev/null
+++ b/theories/channel/proto_channel.v
@@ -0,0 +1,475 @@
+From osiris.channel Require Export channel.
+From osiris.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 auth excl.
+From osiris.utils Require Import auth_excl.
+
+(** Camera setup *)
+Class proto_chanG Σ := {
+  proto_chanG_chanG :> chanG Σ;
+  proto_chanG_authG :> auth_exclG (laterO (proto val (iPreProp Σ) (iPreProp Σ))) Σ;
+}.
+
+Definition proto_chanΣ := #[
+  chanΣ;
+  GFunctor (authRF(optionURF (exclRF (laterOF (protoOF val idOF idOF)))))
+].
+Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ → proto_chanG Σ.
+Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
+
+(** Types and constructors *)
+Definition iProto Σ := proto val (iProp Σ) (iProp Σ).
+Definition iProto_cont Σ X := X -t> val * iProp Σ * iProto Σ.
+
+Delimit Scope proto_scope with proto.
+Bind Scope proto_scope with iProto.
+Delimit Scope proto_cont_scope with proto_cont.
+Bind Scope proto_cont_scope with iProto_cont.
+
+Definition iProto_end {Σ} : iProto Σ := proto_end.
+Program Definition iProto_message {Σ X} (a : action) (pc : iProto_cont Σ X) : iProto Σ :=
+  proto_message a (λ v, λne f, ∃ x : X,
+    ⌜ (tele_app pc x).1.1 = v ⌝ ∗ (tele_app pc x).1.2 ∗ f (Next (tele_app pc x).2))%I.
+Next Obligation. solve_proper. Qed.
+Arguments iProto_message {_ _} _ _%proto_cont.
+
+Definition proto_exist {Σ A} {X : A → tele}
+  (pc : ∀ x : A, iProto_cont Σ (X x)) : iProto_cont Σ (TeleS X) := pc.
+Arguments proto_exist {_ _ _} _%proto.
+Definition proto_payload {Σ} (w : val) (P : iProp Σ)
+  (p : iProto Σ) : iProto_cont Σ TeleO := (w,P,p).
+Arguments proto_payload {_} _%V _%I _%proto.
+
+Notation "<!> pc" := (iProto_message Send pc)
+  (at level 20, pc at level 200) : proto_scope.
+Notation "<?> pc" := (iProto_message Receive pc)
+  (at level 20, pc at level 200) : proto_scope.
+Notation "∃ x .. y , pc" :=
+  (proto_exist (λ x, .. (proto_exist (λ y, pc)) ..)%proto_cont) : proto_cont_scope.
+
+Notation "'MSG' v {{ P }}; p" :=
+  (proto_payload v P p) (at level 20, v at level 20, P, p at level 200) : proto_cont_scope.
+Notation "'MSG' v ; p" :=
+  (proto_payload v True p) (at level 20, v at level 20, p at level 200) : proto_cont_scope.
+
+Definition proto_dual {Σ} (p : iProto Σ) : iProto Σ :=
+  proto_map action_dual cid cid p.
+Arguments proto_dual {_} _%proto.
+
+Class IsActionDual (a1 a2 : action) :=
+  is_action_dual : action_dual a1 = a2.
+Instance is_action_dual_default a : IsActionDual a (action_dual a) | 100 := eq_refl.
+Instance is_action_dual_Send : IsActionDual Send Receive := eq_refl.
+Instance is_action_dual_Receive : IsActionDual Receive Send := eq_refl.
+
+Class IsProtoDual {Σ} (p1 p2 : iProto Σ) :=
+  is_dual_proto : proto_dual p1 ≡ p2.
+Class IsProtoContDual {Σ X} (pc1 pc2 : iProto_cont Σ X) :=
+  is_dual_proto_cont x : prod_map id proto_dual (tele_app pc1 x) ≡ tele_app pc2 x.
+
+(** Invariants *)
+Fixpoint proto_eval `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
+  match vs with
+  | [] => p1 ≡ proto_dual p2
+  | v :: vs => ∃ pc p2',
+     p2 ≡ (proto_message Receive pc)%proto ∗
+     (∀ f : laterO (iProto Σ) -n> iProp Σ, f (Next p2') -∗ pc v f) ∗
+     â–· proto_eval vs p1 p2'
+  end%I.
+Arguments proto_eval {_ _} _ _%proto _%proto : simpl nomatch.
+
+Record proto_name := ProtName {
+  proto_c_name : chan_name;
+  proto_l_name : gname;
+  proto_r_name : gname
+}.
+
+Definition to_proto_auth_excl `{!proto_chanG Σ} (p : iProto Σ) :=
+  to_auth_excl (Next (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 γ) (◯ to_proto_auth_excl p)%I.
+
+Definition proto_own_auth `{!proto_chanG Σ} (γ : proto_name) (s : side)
+    (p : iProto Σ) : iProp Σ :=
+  own (side_elim s proto_l_name proto_r_name γ) (● to_proto_auth_excl p)%I.
+
+Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
+  (∃ l r pl pr,
+    chan_own (proto_c_name γ) Left l ∗
+    chan_own (proto_c_name γ) Right r ∗
+    proto_own_auth γ Left pl ∗
+    proto_own_auth γ Right pr ∗
+    ▷ ((⌜r = []⌝ ∗ proto_eval l pl pr) ∨
+       (⌜l = []⌝ ∗ proto_eval r pr pl)))%I.
+
+Definition proto_interp `{!proto_chanG Σ, !heapG Σ} (N : namespace)
+    (c : val) (p : iProto Σ) : iProp Σ :=
+  (∃ s (c1 c2 : val) γ,
+    ⌜ c = side_elim s c1 c2 ⌝ ∗
+    proto_own_frag γ s p ∗ is_chan N (proto_c_name γ) c1 c2 ∗ inv N (proto_inv γ))%I.
+Arguments proto_interp {_ _ _} _ _ _%proto.
+Instance: Params (@proto_interp) 5 := {}.
+
+Notation "c ↣ p @ N" := (proto_interp N c p)
+  (at level 20, N at level 50, format "c  ↣  p  @  N").
+
+Section proto.
+  Context `{!proto_chanG Σ, !heapG Σ} (N : namespace).
+
+  Global Instance proto_dual_ne : NonExpansive (@proto_dual Σ).
+  Proof. solve_proper. Qed.
+  Global Instance proto_dual_proper : Proper ((≡) ==> (≡)) (@proto_dual Σ).
+  Proof. apply (ne_proper _). Qed.
+  Global Instance proto_dual_involutive : Involutive (≡) (@proto_dual Σ).
+  Proof.
+    intros p. rewrite /proto_dual -proto_map_compose -{2}(proto_map_id p).
+    apply: proto_map_ext=> //. by intros [].
+  Qed.
+  Lemma proto_dual_end : proto_dual (Σ:=Σ) proto_end ≡ proto_end.
+  Proof. by rewrite /proto_dual proto_map_end. Qed.
+  Lemma proto_dual_message a pc :
+    proto_dual (Σ:=Σ) (proto_message a pc)
+    ≡ proto_message (action_dual a) (ofe_morO_map (ofe_morO_map
+        (laterO_map (proto_map action_dual cid cid)) cid) cid ∘ pc).
+  Proof. by rewrite /proto_dual proto_map_message. Qed.
+
+  Global Instance is_proto_dual_default (p : iProto Σ) :
+    IsProtoDual p (proto_dual p) | 100.
+  Proof. by rewrite /IsProtoDual. Qed.
+  Global Instance is_proto_dual_end : IsProtoDual (@iProto_end Σ) iProto_end.
+  Proof. by rewrite /IsProtoDual /iProto_end proto_dual_end. Qed.
+  Global Instance is_proto_dual_message {X} a1 a2 (pc1 pc2 : iProto_cont Σ X) :
+    IsActionDual a1 a2 →
+    IsProtoContDual pc1 pc2 →
+    IsProtoDual (iProto_message a1 pc1) (iProto_message a2 pc2).
+  Proof.
+    rewrite /IsActionDual /IsProtoContDual /IsProtoDual=> <- Hpc.
+    rewrite /iProto_message proto_dual_message. f_equiv=> v f /=. f_equiv=> x.
+    by destruct (Hpc x) as [[-> ->] <-].
+ Qed.
+
+  Global Instance is_proto_cont_dual_payload v P (p1 p2 : iProto Σ) :
+    IsProtoDual p1 p2 →
+    IsProtoContDual (proto_payload v P p1) (proto_payload v P p2).
+  Proof.
+    rewrite /IsProtoDual /IsProtoContDual=> Hp.
+    apply tforall_forall. by rewrite /= Hp.
+  Qed.
+  Global Instance is_proto_cont_dual_exist {A} {X : A → tele}
+      (pc1 pc2 : ∀ x : A, iProto_cont Σ (X x)) :
+    (∀ x, IsProtoContDual (pc1 x) (pc2 x)) →
+    IsProtoContDual (proto_exist pc1) (proto_exist pc2).
+  Proof.
+    rewrite /IsProtoContDual=> Hpc. apply tforall_forall=> /= x'.
+    apply tforall_forall. apply Hpc.
+  Qed.
+
+  Global Instance proto_eval_ne : NonExpansive2 (proto_eval vs).
+  Proof. induction vs; solve_proper. Qed.
+  Global Instance proto_eval_proper vs : Proper ((≡) ==> (≡) ==> (≡)) (proto_eval vs).
+  Proof. apply (ne_proper_2 _). Qed.
+
+  Global Instance to_proto_auth_excl_ne : NonExpansive to_proto_auth_excl.
+  Proof. solve_proper. Qed.
+  Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
+  Proof. solve_proper. Qed.
+  Global Instance proto_interp_ne c : NonExpansive (proto_interp N c).
+  Proof. solve_proper. Qed.
+  Global Instance proto_interp_proper c : Proper ((≡) ==> (≡)) (proto_interp N 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').
+  Proof.
+    iIntros "Hauth Hfrag".
+    iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
+    iDestruct (to_auth_excl_valid with "Hvalid") as "Hvalid".
+    iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext.
+    assert (∀ p : iProto Σ,
+      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.
+  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''.
+  Proof.
+    iIntros "Hauth Hfrag".
+    iDestruct (own_update_2 with "Hauth Hfrag") as "H".
+    { eapply (auth_update _ _ (to_proto_auth_excl p'') (to_proto_auth_excl p'')).
+      apply option_local_update. by apply exclusive_local_update. }
+    by rewrite own_op.
+  Qed.
+
+  Lemma proto_eval_send v vs pc p1 p2 :
+    proto_eval vs (proto_message Send pc) p2 -∗
+    (∀ f : laterO (iProto Σ) -n> iProp Σ, f (Next p1) -∗ pc v f) -∗
+    proto_eval (vs ++ [v]) p1 p2.
+  Proof.
+    iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
+    - iDestruct "Heval" as "#Heval".
+      iExists _, (proto_dual p1). iSplit.
+      { rewrite -{2}(involutive proto_dual p2). iRewrite -"Heval".
+        by rewrite proto_dual_message. }
+      iSplit.
+      { iIntros (f) "Hf /=". by iApply "Hc". }
+      by rewrite involutive.
+    - iDestruct "Heval" as (pc' p2') "(Heq & Hc' & Heval)".
+      iExists pc', p2'. iFrame "Heq Hc'". iNext. iApply ("IH" with "Heval Hc").
+  Qed.
+
+  Lemma proto_eval_recv v vs p1 pc :
+     proto_eval (v :: vs) p1 (proto_message Receive pc) -∗ ∃ p2,
+       (∀ f : laterO (iProto Σ) -n> iProp Σ, f (Next p2) -∗ pc v f) ∗
+       â–· proto_eval vs p1 p2.
+  Proof.
+    simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2".
+    iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]".
+    iSpecialize ("Heq" $! v). rewrite bi.ofe_morO_equivI.
+    iIntros (f) "Hfp2". iRewrite ("Heq" $! f). by iApply "Hc".
+  Qed.
+
+  Lemma proto_eval_False p pc v vs :
+    proto_eval (v :: vs) p (proto_message Send pc) -∗ False.
+  Proof.
+    simpl. iDestruct 1 as (pc' p2') "[Heq _]".
+    by iDestruct (@proto_message_equivI with "Heq") as "[% _]".
+  Qed.
+
+  Lemma proto_eval_nil p1 p2 : proto_eval [] p1 p2 -∗ p1 ≡ proto_dual p2.
+  Proof. done. Qed.
+
+  Arguments proto_eval : simpl never.
+
+  Lemma proto_init E cγ c1 c2 p :
+    is_chan N cγ c1 c2 -∗
+    chan_own cγ Left [] -∗ chan_own cγ Right [] ={E}=∗
+    c1 ↣ p @ N ∗ c2 ↣ proto_dual p @ N.
+  Proof.
+    iIntros "#Hcctx Hcol Hcor".
+    iMod (own_alloc (● (to_proto_auth_excl p) ⋅
+                     ◯ (to_proto_auth_excl p))) as (lγ) "[Hlsta Hlstf]".
+    { by apply auth_both_valid_2. }
+    iMod (own_alloc (● (to_proto_auth_excl (proto_dual p)) ⋅
+                     ◯ (to_proto_auth_excl (proto_dual p)))) as (rγ) "[Hrsta Hrstf]".
+    { by apply auth_both_valid_2. }
+    pose (ProtName cγ lγ rγ) as pγ.
+    iMod (inv_alloc N _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
+    { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
+    iModIntro. iSplitL "Hlstf".
+    - iExists Left, c1, c2, pγ; iFrame; auto.
+    - iExists Right, c1, c2, pγ; iFrame; auto.
+  Qed.
+
+  Lemma proto_send_acc {X} E c (pc : iProto_cont Σ X) :
+    ↑N ⊆ E →
+    c ↣ <!> pc @ N -∗ ∃ s c1 c2 γ,
+      ⌜ c = side_elim s c1 c2 ⌝ ∗
+      is_chan N (proto_c_name γ) c1 c2 ∗ |={E,E∖↑N}=> ∃ vs,
+        chan_own (proto_c_name γ) s vs ∗
+        ▷ ∀ (x : X),
+           (tele_app pc x).1.2 -∗
+           chan_own (proto_c_name γ) s (vs ++ [(tele_app pc x).1.1]) ={E∖↑N,E}=∗
+           c ↣ (tele_app pc x).2 @ N.
+  Proof.
+    iIntros (?). iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]".
+    iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
+    iInv N as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
+    (* TODO: refactor to avoid twice nearly the same proof *)
+    iModIntro. destruct s.
+    - iExists _.
+      iIntros "{$Hclf} !>" (x) "HP Hclf".
+      iRename "Hstf" into "Hstlf".
+      iDestruct (proto_own_auth_agree with "Hstla Hstlf") as "#Heq".
+      iMod (proto_own_auth_update _ _ _ _ (tele_app pc x).2
+        with "Hstla Hstlf") as "[Hstla Hstlf]".
+      iMod ("Hclose" with "[-Hstlf]") as "_".
+      { iNext. iExists _,_,_,_. iFrame "Hcrf Hstra Hstla Hclf". iLeft.
+        iRewrite "Heq" in "Hinv'".
+        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
+        { iSplit=> //. iApply (proto_eval_send with "Heval [HP]").
+          iIntros (f) "Hf /=". iExists x. by iFrame. }
+        destruct r as [|vr r]; last first.
+        { iDestruct (proto_eval_False with "Heval") as %[]. }
+        iSplit; first done; simpl. iRewrite (proto_eval_nil with "Heval").
+        iApply (proto_eval_send _ [] with "[] [HP]").
+        { by rewrite /proto_eval involutive. }
+        iIntros (f) "Hf /=". iExists x. by iFrame. }
+      iModIntro. iExists Left, c1, c2, γ. iFrame; auto.
+    - iExists _.
+      iIntros "{$Hcrf} !>" (x) "HP Hcrf".
+      iRename "Hstf" into "Hstrf".
+      iDestruct (proto_own_auth_agree with "Hstra Hstrf") as "#Heq".
+      iMod (proto_own_auth_update _ _ _ _ (tele_app pc x).2
+        with "Hstra Hstrf") as "[Hstra Hstrf]".
+      iMod ("Hclose" with "[-Hstrf]") as "_".
+      { iNext. iExists _, _, _, _. iFrame "Hcrf Hstra Hstla Hclf". iRight.
+        iRewrite "Heq" in "Hinv'".
+        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last first.
+        { iSplit=> //. iApply (proto_eval_send with "Heval [HP]").
+          iIntros (f) "Hf /=". iExists x. by iFrame. }
+        destruct l as [|vl l]; last first.
+        { iDestruct (proto_eval_False with "Heval") as %[]. }
+        iSplit; first done; simpl. iRewrite (proto_eval_nil with "Heval").
+        iApply (proto_eval_send _ [] with "[] [HP]").
+        { by rewrite /proto_eval involutive. }
+        iIntros (f) "Hf /=". iExists x. by iFrame. }
+      iModIntro. iExists Right, c1, c2, γ. iFrame; auto.
+  Qed.
+
+  Lemma proto_recv_acc {X} E c (pc : iProto_cont Σ X) :
+    ↑N ⊆ E →
+    c ↣ <?> pc @ N -∗ ∃ s c1 c2 γ,
+      ⌜ c = side_elim s c2 c1 ⌝ ∗
+      is_chan N (proto_c_name γ) c1 c2 ∗ |={E,E∖↑N}=> ∃ vs,
+        chan_own (proto_c_name γ) s vs ∗
+        ▷ ((chan_own (proto_c_name γ) s vs ={E∖↑N,E}=∗
+             c ↣ <?> pc @ N) ∧
+           (∀ v vs',
+             ⌜ vs = v :: vs' ⌝ -∗
+             chan_own (proto_c_name γ) s vs' ={E∖↑N,E}=∗ ▷ ∃ x : X,
+             ⌜ v = (tele_app pc x).1.1 ⌝ ∗
+             ▷ c ↣ (tele_app pc x).2 @ N ∗
+             (tele_app pc x).1.2)).
+  Proof.
+    iIntros (?). iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]".
+    iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
+    iFrame "Hcctx".
+    iInv N as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
+    iExists (side_elim s r l). iModIntro.
+    (* TODO: refactor to avoid twice nearly the same proof *)
+    destruct s; simpl.
+    - iIntros "{$Hcrf} !>".
+      iRename "Hstf" into "Hstlf".
+      iDestruct (proto_own_auth_agree with "Hstla Hstlf") as "#Heq".
+      iSplit.
+      + iIntros "Hown".
+        iMod ("Hclose" with "[-Hstlf]") as "_".
+        { iNext. iExists l, r, _, _. iFrame. }
+        iModIntro. iExists Left, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
+      + iIntros (v vs ->) "Hown".
+        iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
+        iAssert (â–· proto_eval (v :: vs) pr (<?> pc))%I with "[Heval]" as "Heval".
+        { iNext. by iRewrite "Heq" in "Heval". }
+        iDestruct (proto_eval_recv with "Heval") as (q) "[Hf Heval]".
+        iMod (proto_own_auth_update _ _ _ _ q with "Hstla Hstlf") as "[Hstla Hstlf]".
+        iMod ("Hclose" with "[-Hstlf Hf]") as %_.
+        { iExists _, _,_ ,_. eauto 10 with iFrame. }
+        iIntros "!> !>".
+        set (f p := (∃ q, p ≡ Next q ∧ c1 ↣ q @ N)%I).
+        assert (NonExpansive f) by solve_proper.
+        iDestruct ("Hf" $! (OfeMor f) with "[Hstlf]") as (x <-) "[HP Hf] /=".
+        { iExists q. iSplit; first done. iExists Left, c1, c2, γ. iFrame; auto. }
+        iExists x. iSplit; first done. iFrame "HP".
+        iDestruct "Hf" as (q') "[#Hq Hc]". iModIntro. by iRewrite "Hq".
+    - iIntros "{$Hclf} !>".
+      iRename "Hstf" into "Hstrf".
+      iDestruct (proto_own_auth_agree with "Hstra Hstrf") as "#Heq".
+      iSplit.
+      + iIntros "Hown".
+        iMod ("Hclose" with "[-Hstrf]") as "_".
+        { iNext. iExists l, r, _, _. iFrame. }
+        iModIntro. iExists Right, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
+      + iIntros (v vs ->) "Hown".
+        iDestruct "Hinv'" as "[[>-> Heval]|[>% _]]"; last done.
+        iAssert (â–· proto_eval (v :: vs) pl (<?> pc))%I with "[Heval]" as "Heval".
+        { iNext. by iRewrite "Heq" in "Heval". }
+        iDestruct (proto_eval_recv with "Heval") as (q) "[Hf Heval]".
+        iMod (proto_own_auth_update _ _ _ _ q with "Hstra Hstrf") as "[Hstra Hstrf]".
+        iMod ("Hclose" with "[-Hstrf Hf]") as %_.
+        { iExists _, _, _, _. eauto 10 with iFrame. }
+        iIntros "!> !>".
+        set (f p := (∃ q, p ≡ Next q ∧ c2 ↣ q @ N)%I).
+        assert (NonExpansive f) by solve_proper.
+        iDestruct ("Hf" $! (OfeMor f) with "[Hstrf]") as (x <-) "[HP Hf] /=".
+        { iExists q. iSplit; first done. iExists Right, c1, c2, γ. iFrame; auto. }
+        iExists x. iSplit; first done. iFrame "HP".
+        iDestruct "Hf" as (q') "[#Hq Hc]". iModIntro. by iRewrite "Hq".
+  Qed.
+
+  Lemma new_chan_proto_spec p1 p2 :
+    IsProtoDual p1 p2 →
+    {{{ True }}}
+      new_chan #()
+    {{{ c1 c2, RET (c1,c2); c1 ↣ p1 @ N ∗ c2 ↣ p2 @ N }}}.
+  Proof.
+    rewrite /IsProtoDual.
+    iIntros (Hp2 Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
+    iIntros (c1 c2 γ) "(Hc & Hl & Hr)".
+    iMod (proto_init ⊤ γ c1 c2 p1 with "Hc Hl Hr") as "[Hp Hdp]".
+    iApply "HΨ". rewrite -Hp2. by iFrame.
+  Qed.
+
+  Lemma send_proto_spec_packed {X} c (pc : iProto_cont Σ X) (x : X) :
+    {{{ c ↣ <!> pc @ N ∗ (tele_app pc x).1.2 }}}
+      send c (tele_app pc x).1.1
+    {{{ RET #(); c ↣ (tele_app pc x).2 @ N }}}.
+  Proof.
+    iIntros (Ψ) "[Hp Hf] HΨ".
+    iDestruct (proto_send_acc ⊤ with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
+    iApply (send_spec with "[$]"). iMod "Hvs" as (vs) "[Hch H]".
+    iModIntro. iExists vs. iFrame "Hch".
+    iIntros "!> Hvs". iApply "HΨ".
+    iMod ("H" $! x with "Hf Hvs"); auto.
+  Qed.
+
+  Lemma send_proto_spec {X} Ψ c v (pc : iProto_cont Σ X) :
+    c ↣ <!> pc @ N -∗
+    (∃.. x : X,
+      ⌜ v = (tele_app pc x).1.1 ⌝ ∗
+      (tele_app pc x).1.2 ∗
+      (c ↣ (tele_app pc x).2 @ N -∗ Ψ #())) -∗
+    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 {X} c (pc : iProto_cont Σ X) :
+    {{{ c ↣ <?> pc @ N }}}
+      try_recv c
+    {{{ v, RET v; (⌜v = NONEV⌝ ∧ c ↣ <?> pc @ N) ∨
+                  (∃ x : X, ⌜v = SOMEV ((tele_app pc x).1.1)⌝ ∗
+                            c ↣ (tele_app pc x).2 @ N ∗ (tele_app pc x).1.2) }}}.
+  Proof.
+    iIntros (Ψ) "Hp HΨ".
+    iDestruct (proto_recv_acc ⊤ with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
+    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". iIntros "!>". iApply "HΨ"; auto.
+  Qed.
+
+  Lemma recv_proto_spec_packed {X} c (pc : iProto_cont Σ X) :
+    {{{ c ↣ <?> pc @ N }}}
+      recv c
+    {{{ x, RET (tele_app pc x).1.1;
+        c ↣ (tele_app pc x).2 @ N ∗ (tele_app pc x).1.2 }}}.
+  Proof.
+    iIntros (Ψ) "Hp HΨ".
+    iDestruct (proto_recv_acc ⊤ with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
+    wp_apply (recv_spec with "[$]"). iMod "Hvs" as (vs) "[Hch [_ H]]".
+    iModIntro. iExists vs. iFrame "Hch". iIntros "!>" (v vs' ->) "Hvs'".
+    iMod ("H" with "[//] Hvs'") as "H"; iIntros "!> !>".
+    iDestruct "H" as (x ->) "H". iIntros "!>". by iApply "HΨ".
+  Qed.
+
+  Lemma recv_proto_spec {X} Ψ c (pc : iProto_cont Σ X) :
+    c ↣ <?> pc @ N -∗
+    (∀.. x : X, c ↣ (tele_app pc x).2 @ N -∗
+                (tele_app pc x).1.2 -∗ Ψ (tele_app 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.
+End proto. 
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
new file mode 100644
index 0000000000000000000000000000000000000000..7e0d463d40857decc6e3f4cc6a25187886741739
--- /dev/null
+++ b/theories/channel/proto_model.v
@@ -0,0 +1,216 @@
+From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import cofe_solver.
+Set Default Proof Using "Type".
+
+Inductive action := Send | Receive.
+Instance action_inhabited : Inhabited action := populate Send.
+Definition action_dual (a : action) : action :=
+  match a with Send => Receive | Receive => Send end.
+Instance action_dual_involutive : Involutive (=) action_dual.
+Proof. by intros []. Qed.
+Canonical Structure actionO := leibnizO action.
+
+Definition protoOF_helper (V : Type) (PROPn PROP : ofeT) : oFunctor :=
+  optionOF (actionO * (V -d> (▶ ∙ -n> PROPn) -n> PROP)).
+Definition proto_result (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} :
+  solution (protoOF_helper V PROPn PROP) := solver.result _.
+Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
+  proto_result V PROPn PROP.
+Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
+Proof. apply _. Qed.
+
+Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
+    protoOF_helper V PROPn PROP (proto V PROPn PROP) _ -n> proto V PROPn PROP :=
+  solution_fold (proto_result V PROPn PROP).
+Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
+    proto V PROPn PROP -n> protoOF_helper V PROPn PROP (proto V PROPn PROP) _ :=
+  solution_unfold (proto_result V PROPn PROP).
+
+Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
+  proto_fold (proto_unfold p) ≡ p.
+Proof. apply solution_fold_unfold. Qed.
+Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
+    (p : protoOF_helper V PROPn PROP (proto V PROPn PROP) _) :
+  proto_unfold (proto_fold p) ≡ p.
+Proof. apply solution_unfold_fold. 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)
+    (pc : V → (laterO (proto V PROPn PROP) -n> PROPn) -n> PROP) : proto V PROPn PROP :=
+  proto_fold (Some (a, pc)).
+
+Lemma proto_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 pc1 pc2 :
+  proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 pc1 ≡ proto_message a2 pc2
+  ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v, pc1 v ≡ pc2 v).
+Proof.
+  trans (proto_unfold (proto_message a1 pc1) ≡ proto_unfold (proto_message a2 pc2) : 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 bi.option_equivI bi.prod_equivI /=.
+  by rewrite bi.discrete_fun_equivI bi.discrete_eq.
+Qed.
+
+Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
+  p ≡ proto_end ∨ ∃ a pc, p ≡ proto_message a pc.
+Proof.
+  destruct (proto_unfold p) as [[a pc]|] eqn:E; simpl in *; last first.
+  - left. by rewrite -(proto_fold_unfold p) E.
+  - right. exists a, pc. by rewrite -(proto_fold_unfold p) E.
+Qed.
+Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
+  Inhabited (proto V PROPn PROP) := populate proto_end.
+
+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.
+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.
+
+Definition proto_cont_map
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, Cofe PROP', !Cofe A, !Cofe B}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') (h : A -n> B) :
+    ((laterO A -n> PROPn) -n> PROP) -n> (laterO B -n> PROPn') -n> PROP' :=
+  ofe_morO_map (ofe_morO_map (laterO_map h) gn) g.
+
+Program Definition proto_map_aux {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (f : action → action) (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' := λne p,
+  match proto_unfold p return _ with
+  | None => proto_end
+  | Some (a, c) => proto_message (f a) (proto_cont_map gn g rec ∘ c)
+  end.
+Next Obligation.
+  intros V PROPn ? PROPn' ? PROP ? PROP' ? f g1 g2 rec n p1 p2 Hp.
+  apply (ofe_mor_ne _ _ proto_unfold) in Hp.
+  destruct Hp as [[??][??] [-> ?]|]; simplify_eq/=; last done.
+  f_equiv=> v /=. by f_equiv.
+Qed.
+
+Instance proto_map_aux_contractive {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+  Contractive (proto_map_aux (V:=V) f gn g).
+Proof.
+  intros n rec1 rec2 Hrec p. simpl.
+  destruct (proto_unfold p) as [[a c]|]; last done.
+  f_equiv=> v /=. do 2 f_equiv.
+  intros=> p'. apply Next_contractive. destruct n as [|n]=> //=.
+Qed.
+
+Definition proto_map {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+    proto V PROPn PROP -n> proto V PROPn' PROP' :=
+  fixpoint (proto_map_aux f gn g).
+
+Lemma proto_map_unfold {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
+  proto_map (V:=V) f gn g p ≡ proto_map_aux f gn g (proto_map f gn g) p.
+Proof. apply (fixpoint_unfold (proto_map_aux f gn g)). Qed.
+Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, Cofe PROP'}
+    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+  proto_map (V:=V) f gn g proto_end ≡ proto_end.
+Proof.
+  rewrite proto_map_unfold /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; rewrite E; inversion Hfold.
+Qed.
+Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a c :
+  proto_map (V:=V) f gn g (proto_message a c) ≡ proto_message (f a) (proto_cont_map gn g (proto_map f gn g) ∘ c).
+Proof.
+  rewrite proto_map_unfold /proto_message /=.
+  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) (Some (a, c))) as Hfold.
+  destruct (proto_unfold (proto_fold (Some (a, c))))
+    as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
+  rewrite /proto_message. do 3 f_equiv. intros v=> /=.
+  apply equiv_dist=> n. f_equiv. by apply equiv_dist.
+Qed.
+
+Lemma proto_map_ne {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (f1 f2 : action → action) (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
+  (∀ a, f1 a = f2 a) → (∀ x, gn1 x ≡{n}≡ gn2 x) → (∀ x, g1 x ≡{n}≡ g2 x) →
+  proto_map (V:=V) f1 gn1 g1 p ≡{n}≡ proto_map (V:=V) f2 gn2 g2 p.
+Proof.
+  intros Hf. revert p. induction (lt_wf n) as [n _ IH]=> p Hgn Hg /=.
+  destruct (proto_case p) as [->|(a & c & ->)].
+  - by rewrite !proto_map_end.
+  - rewrite !proto_map_message /= Hf. f_equiv=> v /=. do 2 (f_equiv; last done).
+    intros p'. apply Next_contractive. destruct n as [|n]=> //=.
+    apply IH; first lia; auto using dist_S.
+Qed.
+Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (f1 f2 : action → action) (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
+  (∀ a, f1 a = f2 a) → (∀ x, gn1 x ≡ gn2 x) → (∀ x, g1 x ≡ g2 x) →
+  proto_map (V:=V) f1 gn1 g1 p ≡ proto_map (V:=V) f2 gn2 g2 p.
+Proof.
+  intros Hf Hgn Hg. apply equiv_dist=> n.
+  apply proto_map_ne=> // ?; by apply equiv_dist.
+Qed.
+Lemma proto_map_id {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
+  proto_map id cid cid p ≡ p.
+Proof.
+  apply equiv_dist=> n. revert p. induction (lt_wf n) as [n _ IH]=> p /=.
+  destruct (proto_case p) as [->|(a & c & ->)].
+  - by rewrite !proto_map_end.
+  - rewrite !proto_map_message /=. f_equiv=> v c' /=. f_equiv=> p' /=. f_equiv.
+    apply Next_contractive. destruct n as [|n]=> //=.
+    apply IH; first lia; auto using dist_S.
+Qed.
+Lemma proto_map_compose {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROPn'', !Cofe PROP, !Cofe PROP', !Cofe PROP''}
+    (f1 f2 : action → action)
+    (gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
+    (g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
+  proto_map (f2 ∘ f1) (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map f2 gn1 g2 (proto_map f1 gn2 g1 p).
+Proof.
+  apply equiv_dist=> n. revert p. induction (lt_wf n) as [n _ IH]=> p /=.
+  destruct (proto_case p) as [->|(a & c & ->)].
+  - by rewrite !proto_map_end.
+  - rewrite !proto_map_message /=. f_equiv=> v c' /=. do 3 f_equiv. move=> p' /=.
+    do 3 f_equiv. apply Next_contractive. destruct n as [|n]=> //=.
+    apply IH; first lia; auto using dist_S.
+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 id (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_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_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 oFunctor_compose.
+Qed.
+
+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 ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
+  apply proto_map_ne=> //= y.
+  - destruct n; [|destruct Hfg]; by apply oFunctor_contractive.
+  - destruct n; [|destruct Hfg]; by apply oFunctor_contractive.
+Qed.
diff --git a/theories/examples/branching_proofs.v b/theories/examples/branching_proofs.v
index ab29ac04cb4c2ee2cb73fa4985eff1edf8a997db..83e20a7673feb1f5315ba5cdf120bc45ce235c0b 100644
--- a/theories/examples/branching_proofs.v
+++ b/theories/examples/branching_proofs.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Import proofmode notation.
-From osiris.proto Require Import branching.
+From osiris.channel Require Import branching.
 
 Definition branch_example b : expr :=
   (let: "c" := new_chan #() in
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index fd0a3f1194e77b4af675d2d719aa242d33821560..7aafed16e80e36932403213105ef2200d232739f 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -1,227 +1,151 @@
 From stdpp Require Import sorting.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.proto Require Import list channel proto_enc.
-
-Section ListSortExample.
-  Context `{!heapG Σ, !logrelG val Σ} (N : namespace).
-
-  Section SortService.
-    Context `{ValEncDec T}.
-    Context (R : relation T) `{!Total R} `{∀ x y, Decision (R x y)}.
-
-    Definition lsplit_ref : val :=
-      λ: "xs", let: "ys_zs" := lsplit !"xs" in
-               (ref (Fst "ys_zs"), ref (Snd ("ys_zs"))).
-
-    Lemma lsplit_ref_spec lxs (x : T) (xs : list T) :
-      {{{ lxs ↦ val_encode (x :: xs) }}}
-        lsplit_ref #lxs
-      {{{ lys lzs ys zs, RET (#lys, #lzs);
-          ⌜ x :: xs = ys ++ zs⌝ ∗
-          lxs ↦ val_encode (x :: xs) ∗
-          lys ↦ val_encode ys ∗
-          lzs ↦ val_encode zs }}}.
-    Proof.
-      iIntros (Φ) "Hhd HΦ".
-      wp_lam. wp_load. wp_apply (lsplit_spec)=> //. iIntros (ys zs <-).
-      wp_alloc lzs as "Hlzs".
-      wp_alloc lys as "Hlys".
-      wp_pures.
-      iApply "HΦ".
-      eauto 10 with iFrame.
-    Qed.
-
-    Definition lmerge : val :=
-      rec: "go" "cmp" "hys" "hzs" :=
-        match: "hys" with
-          NONE => "hzs"
-        | SOME "_" =>
-          match: "hzs" with
-            NONE => "hys"
-          | SOME "_" =>
-            let: "y" := lhead "hys" in
-            let: "z" := lhead "hzs" in
-            if: ("cmp" "y" "z")
-            then lcons "y" ("go" "cmp" (ltail "hys") "hzs")
-            else lcons "z" ("go" "cmp" "hys" (ltail "hzs"))
-          end
-        end.
-
-    Lemma list_merge_emp1 (ys : list T) : list_merge (R) [] ys = ys.
-    Proof. induction ys; eauto. Qed.
-
-    Lemma list_merge_emp2 (xs : list T) : list_merge (R) xs [] = xs.
-    Proof. induction xs; eauto. Qed.
-
-    Definition cmp_spec (cmp : val) : iProp Σ :=
-      (∀ x y, {{{ True }}}
-                cmp (val_encode x) (val_encode y)
-              {{{ RET val_encode (bool_decide (R x y)); True}}})%I.
-
-    Lemma lmerge_spec  (cmp : val) (ys zs : list T) :
-      cmp_spec cmp -∗
-      {{{ True }}}
-        lmerge cmp (val_encode ys) (val_encode zs)
-      {{{ RET val_encode (list_merge R ys zs); True }}}.
-    Proof.
-      revert ys zs.
-      iLöb as "IH".
-      iIntros (ys zs).
-      iIntros "#Hcmp_spec".
-      iIntros (Φ).
-      iModIntro.
-      iIntros (_) "HΦ".
-      wp_lam.
-      destruct ys as [|y ys].
-      { wp_pures. rewrite list_merge_emp1. by iApply ("HΦ"). }
-      destruct zs as [|z zs].
-      { wp_pures. rewrite list_merge_emp2. by iApply ("HΦ"). }
-      wp_apply (lhead_spec)=> //; iIntros "_".
-      wp_apply (lhead_spec)=> //; iIntros "_".
-      wp_apply ("Hcmp_spec")=> //; iIntros "_".
-      rewrite list_merge_cons.
-      destruct (decide (R y z)).
-      - rewrite bool_decide_true=> //.
-        wp_apply (ltail_spec)=> //; iIntros (_).
-        wp_apply ("IH")=> //; iIntros (_).
-        wp_apply (lcons_spec)=> //.
-      - rewrite bool_decide_false=> //.
-        wp_apply (ltail_spec)=> //; iIntros (_).
-        wp_apply ("IH")=> //; iIntros (_).
-        wp_apply (lcons_spec)=> //.
-    Qed.
-
-    Definition lmerge_ref : val :=
-      λ: "cmp" "lxs" "hys" "hzs",
-      "lxs" <- lmerge "cmp" "hys" "hzs".
-
-    Lemma lmerge_ref_spec (cmp : val) ldx tmp ys zs :
-      cmp_spec cmp -∗
-      {{{ ldx ↦ tmp }}}
-        lmerge_ref cmp #ldx (val_encode ys) (val_encode zs)
-      {{{ RET #(); ldx ↦ val_encode (list_merge R ys zs) }}}.
-    Proof.
-      iIntros "#Hcmp_spec".
-      iIntros (Φ).
-      iModIntro.
-      iIntros "Hldx HΦ".
-      wp_lam.
-      wp_apply (lmerge_spec cmp ys zs with "Hcmp_spec")=> //.
-      iIntros (_).
-      wp_store.
-      by iApply ("HΦ").
-    Qed.
-
-    Definition list_sort_service : val :=
-      rec: "go" "c" :=
-        let: "cmp" := recv "c" #Right in
-        let: "xs" := recv "c" #Right in
-        if: llength (!"xs") ≤ #1
-        then send "c" #Right "xs"
-        else let: "ys_zs" := lsplit_ref "xs" in
-             let: "ys" := Fst "ys_zs" in
-             let: "zs" := Snd "ys_zs" in
-             let: "cy" := new_chan #() in Fork("go" "cy");;
-             let: "cz" := new_chan #() in Fork("go" "cz");;
-             send "cy" #Left "cmp";;
-             send "cy" #Left "ys";;
-             send "cz" #Left "cmp";;
-             send "cz" #Left "zs";;
-             let: "ys" := recv "cy" #Left in
-             let: "zs" := recv "cz" #Left in
-             lmerge_ref "cmp" "xs" !"ys" !"zs";;
-             send "c" #Right "xs".
-
-    Definition sort_protocol xs : proto val (iProp Σ) :=
-      (<?> cmp @ cmp_spec cmp,
-       <?> l @ l ↦ val_encode xs,
-       <!> l' @ ⌜l = l'⌝ ∗
-                (∃ ys : list T,
-                    l' ↦ val_encode ys ∗
-                    ⌜Sorted R ys⌝ ∗
-                    ⌜Permutation ys xs⌝),
-       TEnd).
+From osiris.utils Require Import list.
+From osiris.channel Require Import proto_channel.
+
+Definition lmerge : val :=
+  rec: "go" "cmp" "hys" "hzs" :=
+    match: "hys" with
+      NONE => "hzs"
+    | SOME "_" =>
+      match: "hzs" with
+        NONE => "hys"
+      | SOME "_" =>
+        let: "y" := lhead "hys" in
+        let: "z" := lhead "hzs" in
+        if: ("cmp" "y" "z")
+        then lcons "y" ("go" "cmp" (ltail "hys") "hzs")
+        else lcons "z" ("go" "cmp" "hys" (ltail "hzs"))
+      end
+    end.
+
+Definition list_sort_service : val :=
+  rec: "go" "c" :=
+    let: "cmp" := recv "c" in
+    let: "xs" := recv "c" in
+    if: llength !"xs" ≤ #1 then
+      send "c" #() else
+    let: "ys_zs" := lsplit !"xs" in
+    let: "ys" := ref (Fst "ys_zs") in
+    let: "zs" := ref (Snd "ys_zs") in
+    let: "cy" := new_chan #() in Fork("go" (Fst "cy"));;
+    let: "cz" := new_chan #() in Fork("go" (Fst "cz"));;
+    send (Snd "cy") "cmp";;
+    send (Snd "cy") "ys";;
+    send (Snd "cz") "cmp";;
+    send (Snd "cz") "zs";;
+    recv (Snd "cy");;
+    recv (Snd "cz");;
+    "xs" <- lmerge "cmp" !"ys" !"zs";;
+    send "c" #().
+
+Section list_sort.
+  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+
+  Definition cmp_spec {A} (I : A → val → iProp Σ)
+      (R : A → A → Prop) `{!RelDecision R} (cmp : val) : iProp Σ :=
+    (∀ x x' v v',
+      {{{ I x v ∗ I x' v' }}}
+        cmp v v'
+      {{{ RET #(bool_decide (R x x')); I x v ∗ I x' v' }}})%I.
+
+  Definition sort_protocol : iProto Σ :=
+    (<?> ∃ A (I : A → val → iProp Σ) (R : A → A → Prop)
+         `{!RelDecision R, !TotalOrder R} (cmp : val),
+       MSG cmp {{ cmp_spec I R cmp }};
+     <?> ∃ (xs : list A) (l : loc) (vs : list val),
+       MSG #l {{ l ↦ val_encode vs ∗ [∗ list] x;v ∈ xs;vs, I x v }};
+     <!> ∃ (xs' : list A) (vs' : list val),
+       MSG #() {{ ⌜ Sorted R xs' ⌝ ∗ ⌜ xs' ≡ₚ xs ⌝ ∗
+                  l ↦ val_encode vs' ∗ [∗ list] x;v ∈ xs';vs', I x v }};
+     iProto_end)%proto.
+
+  Lemma lmerge_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
+      `{!RelDecision R, !TotalOrder R} (cmp : val) xs1 xs2 vs1 vs2 :
+    cmp_spec I R cmp -∗
+    {{{ ([∗ list] x;v ∈ xs1;vs1, I x v) ∗ ([∗ list] x;v ∈ xs2;vs2, I x v) }}}
+      lmerge cmp (val_encode vs1) (val_encode vs2)
+    {{{ ws, RET val_encode ws; [∗ list] x;v ∈ list_merge R xs1 xs2;ws, I x v }}}.
+  Proof.
+    iIntros "#Hcmp" (Ψ) "!> [HI1 HI2] HΨ". iLöb as "IH" forall (xs1 xs2 vs1 vs2 Ψ).
+    destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; try done.
+    { wp_lam. wp_pures. iApply "HΨ". by rewrite list_merge_nil_l. }
+    wp_lam; wp_pures.
+    destruct xs2 as [|x2 xs2], vs2 as [|v2 vs2]; simpl; try done.
+    { wp_pures. iApply "HΨ". iFrame. }
+    wp_pures.
+    wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
+    wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
+    iDestruct "HI1" as "[HI1 HI1']"; iDestruct "HI2" as "[HI2 HI2']".
+    wp_apply ("Hcmp" with "[$HI1 $HI2]"); iIntros "[HI1 HI2]".
+    case_bool_decide; wp_pures.
+    - rewrite decide_True //.
+      wp_apply (ltail_spec (A:=val) with "[//]"); iIntros (_).
+      wp_apply ("IH" $! _ (x2 :: _) with "HI1'[HI2 HI2']"); [simpl; iFrame|].
+      iIntros (ws) "HI".
+      wp_apply (lcons_spec (A:=val) with "[//]"); iIntros (_).
+      iApply "HΨ". iFrame.
+    - rewrite decide_False //.
+      wp_apply (ltail_spec (A:=val) with "[//]"); iIntros (_).
+      wp_apply ("IH" $! (x1 :: _) with "[HI1 HI1'] HI2'"); [simpl; iFrame|].
+      iIntros (ws) "HI".
+      wp_apply (lcons_spec (A:=val) with "[//]"); iIntros (_).
+      iApply "HΨ". iFrame.
+  Qed.
 
-    Lemma list_sort_service_spec γ c xs :
-      {{{ ⟦ c @ Right : sort_protocol xs ⟧{N,γ} }}}
-        list_sort_service c
-      {{{ RET #(); ⟦ c @ Right : TEnd ⟧{N,γ} }}}.
-    Proof.
-      revert γ c xs.
-      iLöb as "IH".
-      iIntros (γ c xs Φ) "Hstr HΦ".
-      wp_lam.
-      wp_apply (recv_st_spec (A:=val) with "Hstr").
-      iIntros (cmp) "[Hstr #Hcmp_spec]".
-      wp_pures.
-      wp_apply (recv_st_spec (A:=loc) with "Hstr").
-      iIntros (v) "[Hstr HP]".
-      wp_load.
-      destruct xs.
-      {
-        wp_apply (llength_spec)=> //; iIntros (_).
-        wp_apply (send_st_spec (A:=loc) with "[HP Hstr]")=> //. iFrame.
-        eauto 10 with iFrame.
-      }
-      destruct xs.
-      {
-        wp_apply (llength_spec)=> //; iIntros (_).
-        wp_apply (send_st_spec (A:=loc) with "[HP Hstr]")=> //. iFrame.
-        eauto 10 with iFrame.
-      }
-      wp_apply (llength_spec)=> //; iIntros (_).
-      wp_pures.
-      assert (bool_decide (S (S (length xs)) ≤ 1) = false) as HSS.
-      { apply bool_decide_false. lia. }
-      rewrite HSS.
-      wp_apply (lsplit_ref_spec with "HP");
-        iIntros (hdy hdz ys zs) "(Heq & Hhdx & Hhdy & Hhdz)".
-      iDestruct "Heq" as %->.
-      wp_apply (new_chan_st_spec N _ (sort_protocol ys))=> //.
-      iIntros (cy γy) "[Hstly Hstry]".
-      wp_apply (wp_fork with "[Hstry]").
-      { iNext. iApply ("IH" with "Hstry"). iNext. by iIntros "Hstry". }
-      wp_apply (new_chan_st_spec N _ (sort_protocol zs))=> //.
-      iIntros (cz γz) "[Hstlz Hstrz]".
-      wp_apply (wp_fork with "[Hstrz]").
-      { iNext. iApply ("IH" with "Hstrz"). iNext. by iIntros "Hstrz". }
-      wp_apply (send_st_spec (A:=val) with "[Hstly]"). iFrame. done.
-      iIntros "Hstly".
-      wp_apply (send_st_spec (A:=loc) with "[Hhdy Hstly]"). iFrame.
-      iIntros "Hstly".
-      wp_apply (send_st_spec (A:=val) with "[Hstlz]"). iFrame. done.
-      iIntros "Hstlz".
-      wp_apply (send_st_spec (A:=loc) with "[Hhdz Hstlz]"). iFrame.
-      iIntros "Hstlz".
-      wp_apply (recv_st_spec (A:=loc) with "Hstly").
-      iIntros (ly') "[Hstly Hys']".
-      iDestruct "Hys'" as (<- ys') "(Hys' & Hys'_sorted_of)".
-      iDestruct "Hys'_sorted_of" as %[Hys'_sorted Hys'_perm].
-      wp_apply (recv_st_spec (A:=loc) with "Hstlz").
-      iIntros (lz') "[Hstlz Hzs']".
-      iDestruct "Hzs'" as (<- zs') "(Hzs' & Hzs'_sorted_of)".
-      iDestruct "Hzs'_sorted_of" as %[Hzs'_sorted Hzs'_perm].
-      wp_load.
-      wp_load.
-      wp_apply (lmerge_ref_spec with "Hcmp_spec Hhdx").
-      iIntros "Hhdx".
-      wp_apply (send_st_spec (A:=loc) with "[Hstr Hhdx]").
-      {
-        iFrame.
-        iSplit=> //.
-        iExists (list_merge R ys' zs').
-        iSplit=> //.
-        iPureIntro.
-        split.
-        - apply Sorted_list_merge=> //.
-        - rewrite merge_Permutation.
-            by apply Permutation_app.
-      }
-      iIntros "Hstr".
-      by iApply "HΦ".
-    Qed.
-  End SortService.
+  Lemma list_sort_service_spec c :
+    {{{ c ↣ sort_protocol @ N }}}
+      list_sort_service c
+    {{{ RET #(); c ↣ iProto_end @ N }}}.
+  Proof.
+    iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
+    wp_lam.
+    wp_apply (recv_proto_spec with "Hc"); simpl.
+    iIntros (A I R ?? cmp) "/= Hc #Hcmp".
+    wp_apply (recv_proto_spec with "Hc"); simpl.
+    iIntros (xs l vs) "/= Hc [Hl HI]".
+    wp_load. wp_apply (llength_spec (A:=val) with "[//]"); iIntros (_).
+    iDestruct (big_sepL2_length with "HI") as %<-.
+    wp_op; case_bool_decide as Hlen; wp_if.
+    { assert (Sorted R xs).
+      { destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
+      wp_apply (send_proto_spec with "Hc"); simpl.
+      iExists xs, vs; iSplit; first done. eauto 10 with iFrame. }
+    wp_load. wp_apply (lsplit_spec (A:=val) with "[//]"); iIntros (vs1 vs2 <-).
+    wp_alloc l1 as "Hl1"; wp_alloc l2 as "Hl2".
+    iDestruct (big_sepL2_app_inv_r with "HI") as (xs1 xs2 ->) "[HI1 HI2]".
+    wp_apply (new_chan_proto_spec N sort_protocol)=> //.
+    iIntros (cy1 cy2) "[Hcy1 Hcy2]".
+    wp_apply (wp_fork with "[Hcy1]").
+    { iNext. wp_apply ("IH" with "Hcy1"); auto. }
+    wp_apply (new_chan_proto_spec N sort_protocol)=> //.
+    iIntros (cz1 cz2) "[Hcz1 Hcz2]".
+    wp_apply (wp_fork with "[Hcz1]").
+    { iNext. wp_apply ("IH" with "Hcz1"); auto. }
+    wp_apply (send_proto_spec with "Hcy2"); simpl.
+    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} Hcy2".
+    wp_apply (send_proto_spec with "Hcy2"); simpl.
+    iExists xs1, l1, vs1. iSplit; first done. iIntros "{$Hl1 $HI1} Hcy2".
+    wp_apply (send_proto_spec with "Hcz2"); simpl.
+    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} Hcz2".
+    wp_apply (send_proto_spec with "Hcz2"); simpl.
+    iExists xs2, l2, vs2. iSplit; first done. iIntros "{$Hl2 $HI2} Hcz2".
+    wp_apply (recv_proto_spec with "Hcy2"); simpl.
+    iIntros (ys1 ws1) "_". iDestruct 1 as (??) "[Hl1 HI1]".
+    wp_apply (recv_proto_spec with "Hcz2"); simpl.
+    iIntros (ys2 ws2) "_". iDestruct 1 as (??) "[Hl2 HI2]".
+    do 2 wp_load.
+    wp_apply (lmerge_spec with "Hcmp [$HI1 $HI2]"); iIntros (ws) "HI".
+    wp_store.
+    wp_apply (send_proto_spec with "Hc"); simpl.
+    iExists (list_merge R ys1 ys2), ws.
+    iSplit; first done. iFrame. iSplit; iPureIntro.
+    - by apply (Sorted_list_merge _).
+    - rewrite (merge_Permutation R). by f_equiv.
+  Qed.
+End list_sort.
 
+(*
   Definition compare_vals : val :=
     λ: "x" "y", "x" ≤ "y".
 
@@ -266,4 +190,4 @@ Section ListSortExample.
      iDestruct "HP" as (<- ys) "[Hys Hys_sorted_of]".
      iApply "HΦ". iFrame.
   Qed.
-End ListSortExample.
+*)
diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index f1b490d634a9b2460380ea3b276fac363150970e..11cf51a5551d8d55c8c0089a44e5358cf9a39d07 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Import proofmode notation.
-From osiris.proto Require Import proto_enc.
+From osiris.channel Require Import proto_channel.
 
 Definition seq_example : expr :=
   (let: "c" := new_chan #() in
diff --git a/theories/proto/involutive.v b/theories/proto/involutive.v
deleted file mode 100644
index 506925a667451c4ff0989b608046b790c5982681..0000000000000000000000000000000000000000
--- a/theories/proto/involutive.v
+++ /dev/null
@@ -1,4 +0,0 @@
-From iris.heap_lang Require Import proofmode notation.
-
-Class Involutive {A} (R : relation A) (f : A → A) :=
-  involutive x : R (f (f x)) x.
diff --git a/theories/proto/proto_def.v b/theories/proto/proto_def.v
deleted file mode 100644
index 881050352fda23113db8805052f8a79941dec108..0000000000000000000000000000000000000000
--- a/theories/proto/proto_def.v
+++ /dev/null
@@ -1,317 +0,0 @@
-From iris.base_logic Require Import base_logic.
-From osiris.proto Require Import involutive.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-
-Inductive action := Send | Receive.
-Instance action_inhabited : Inhabited action := populate Send.
-Definition dual_action (a : action) : action :=
-  match a with Send => Receive | Receive => Send end.
-Instance dual_action_involutive : Involutive (=) dual_action.
-Proof. by intros []. Qed.
-
-CoInductive proto (V PROP : Type) :=
-  | TEnd
-  | TSR (a : action) (P : V → PROP) (prot : V → proto V PROP).
-Arguments TEnd {_ _}.
-Arguments TSR {_ _} _ _ _.
-Instance: Params (@TSR) 3.
-
-Instance proto_inhabited V PROP : Inhabited (proto V PROP) := populate TEnd.
-
-CoFixpoint dual_proto {V PROP} (prot : proto V PROP) : proto V PROP :=
-  match prot with
-  | TEnd => TEnd
-  | TSR a Φ prot => TSR (dual_action a) Φ (λ v, dual_proto (prot v))
-  end.
-Instance: Params (@dual_proto) 2.
-
-Delimit Scope proto_scope with proto.
-Bind Scope proto_scope with proto.
-
-Notation "<!> x @ P , prot" :=
-  (TSR Send (λ x, P%I) (λ x, prot%proto))
-  (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<?> x @ P , prot" :=
-  (TSR Receive (λ x, P%I) (λ x, prot%proto))
-  (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<!> x , prot" := (<!> x @ True, prot%proto)%proto
-  (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<?> x , prot" := (<?> x @ True, prot%proto)%proto
-  (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<!> @ Φ , prot" := (TSR Send Φ prot)%proto
-  (at level 200, prot at level 200) : proto_scope.
-Notation "<?> @ Φ , prot" := (TSR Receive Φ prot)%proto
-  (at level 200, prot at level 200) : proto_scope.
-
-Section proto_ofe.
-  Context {V : Type}.
-  Context {PROP : ofeT}.
-
-  CoInductive proto_equiv : Equiv (proto V PROP) :=
-    | TEnd_equiv : TEnd ≡ TEnd
-    | TSR_equiv a Φ1 Φ2 prot1 prot2 :
-       pointwise_relation V (≡) Φ1 Φ2 →
-       pointwise_relation V (≡) prot1 prot2 →
-       TSR a Φ1 prot1 ≡ TSR a Φ2 prot2.
-  Existing Instance proto_equiv.
-
-  CoInductive proto_dist : Dist (proto V PROP) :=
-    | TEnd_dist n : TEnd ≡{n}≡ TEnd
-    | TSR_dist_0 a Φ1 Φ2 prot1 prot2 :
-       pointwise_relation V (dist 0) Φ1 Φ2 →
-       TSR a Φ1 prot1 ≡{0}≡ TSR a Φ2 prot2
-    | TSR_dist_S n a Φ1 Φ2 prot1 prot2 :
-       pointwise_relation V (dist (S n)) Φ1 Φ2 →
-       pointwise_relation V (dist n) prot1 prot2 →
-       TSR a Φ1 prot1 ≡{S n}≡ TSR a Φ2 prot2.
-  Existing Instance proto_dist.
-
-  Lemma TSR_dist n a Φ1 Φ2 prot1 prot2 :
-    pointwise_relation V (dist n) Φ1 Φ2 →
-    pointwise_relation V (dist_later n) prot1 prot2 →
-    TSR a Φ1 prot1 ≡{n}≡ TSR a Φ2 prot2.
-  Proof. destruct n; by constructor. Defined.
-
-  Definition proto_ofe_mixin : OfeMixin (proto V PROP).
-  Proof.
-    split.
-    - intros prot1 prot2. split.
-      + revert prot1 prot2. cofix IH; destruct 1 as [|a Φ1 Φ2 prot1' prot2' HΦ]=> n.
-        { constructor. }
-        destruct n as [|n].
-        * constructor=> v. apply equiv_dist, HΦ.
-        * constructor=> v. apply equiv_dist, HΦ. by apply IH.
-      + revert prot1 prot2. cofix IH=> -[|a1 Φ1 prot1] -[|a2 Φ2 prot2] Hprot;
-          feed inversion (Hprot O); subst; constructor=> v.
-        * apply equiv_dist=> n. feed inversion (Hprot n); auto.
-        * apply IH=> n. feed inversion (Hprot (S n)); auto.
-    - intros n. split.
-      + revert n. cofix IH=> -[|n] [|a Φ prot]; constructor=> v; auto.
-      + revert n. cofix IH; destruct 1; constructor=> v; symmetry; auto.
-      + revert n. cofix IH; destruct 1; inversion 1; constructor=> v; etrans; eauto.
-    - cofix IH=> -[|n]; inversion 1; constructor=> v; try apply dist_S; auto.
-  Qed.
-  Canonical Structure protoO : ofeT := OfeT (proto V PROP) proto_ofe_mixin.
-
-  Definition proto_head (dΦ : V -d> PROP) (prot : proto V PROP) : V -d> PROP :=
-    match prot with TEnd => dΦ | TSR a Φ prot => Φ end.
-  Definition proto_tail (v : V) (prot : protoO) : later protoO :=
-    match prot with TEnd => Next TEnd | TSR a P prot => Next (prot v) end.
-  Global Instance proto_head_ne d : NonExpansive (proto_head d).
-  Proof. by destruct 1. Qed.
-  Global Instance proto_tail_ne v : NonExpansive (proto_tail v).
-  Proof. destruct 1; naive_solver. Qed.
-
-  Definition proto_force (prot : proto V PROP) : proto V PROP :=
-    match prot with
-    | TEnd => TEnd
-    | TSR a Φ prot => TSR a Φ prot
-    end.
-  Lemma proto_force_eq prot : proto_force prot = prot.
-  Proof. by destruct prot. Defined.
-
-  CoFixpoint proto_compl_go `{!Cofe PROP} (c : chain protoO) : protoO :=
-    match c O with
-    | TEnd => TEnd
-    | TSR a Φ prot => TSR a
-       (compl (chain_map (proto_head Φ) c) : V → PROP)
-       (λ v, proto_compl_go (later_chain (chain_map (proto_tail v) c)))
-    end.
-
-  Global Program Instance proto_cofe `{!Cofe PROP} : Cofe protoO :=
-    {| compl c := proto_compl_go c |}.
-  Next Obligation.
-    intros ? n c; rewrite /compl. revert c n. cofix IH=> c n.
-    rewrite -(proto_force_eq (proto_compl_go c)) /=.
-    destruct (c O) as [|a Φ prot'] eqn:Hc0.
-    - assert (c n ≡{0}≡ TEnd) as Hcn.
-      { rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
-      by inversion Hcn.
-    - assert (c n ≡{0}≡ TSR a Φ prot') as Hcn.
-      { rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
-      inversion Hcn as [|? P' ? prot'' ? HΦ|]; subst.
-      destruct n as [|n]; constructor.
-      + intros v. by rewrite (conv_compl 0 (chain_map (proto_head Φ) c) v) /= -H.
-      + intros v. by rewrite (conv_compl _ (chain_map (proto_head Φ) c) v) /= -H.
-      + intros v. assert (prot'' v = later_car (proto_tail v (c (S n)))) as ->.
-        { by rewrite -H /=. }
-        apply IH.
-  Qed.
-
-  Global Instance TSR_proto_contractive a n :
-    Proper (pointwise_relation _ (dist n) ==>
-            pointwise_relation _ (dist_later n) ==> dist n) (TSR a).
-  Proof. destruct n; by constructor. Qed.
-  Global Instance TSR_proto_ne a n :
-    Proper (pointwise_relation _ (dist n) ==>
-            pointwise_relation _ (dist n) ==> dist n) (TSR a).
-  Proof.
-    intros Φ1 Φ2 HΦ prot1 prot2 Hst. apply TSR_proto_contractive=> //.
-    destruct n as [|n]=> // v /=. by apply dist_S.
-  Qed.
-  Global Instance TSR_proto_proper a :
-    Proper (pointwise_relation _ (≡) ==>
-            pointwise_relation _ (≡) ==> (≡)) (TSR a).
-  Proof. by constructor. Qed.
-
-  Global Instance dual_proto_ne : NonExpansive dual_proto.
-  Proof.
-    cofix IH=> n prot1 prot2 Hst.
-    rewrite -(proto_force_eq (dual_proto prot1)) -(proto_force_eq (dual_proto prot2)).
-    destruct Hst; constructor=> v; auto; by apply IH.
-  Qed.
-  Global Instance dual_proto_proper : Proper ((≡) ==> (≡)) dual_proto.
-  Proof. apply (ne_proper _). Qed.
-
-  Global Instance dual_proto_involutive : Involutive (≡) dual_proto.
-  Proof.
-    cofix IH=> prot. rewrite -(proto_force_eq (dual_proto (dual_proto _))).
-    destruct prot as [|a P prot]; first done.
-    rewrite /= involutive. constructor=> v; auto.
-  Qed.
-
-  Lemma proto_equivI {M} prot1 prot2 :
-    prot1 ≡ prot2 ⊣⊢@{uPredI M}
-        match prot1, prot2 with
-        | TEnd, TEnd => True
-        | TSR a1 Φ1 prot1, TSR a2 Φ2 prot2 =>
-          ⌜ a1 = a2 ⌝ ∧ (∀ v, Φ1 v ≡ Φ2 v) ∧ ▷ (∀ v, prot1 v ≡ prot2 v)
-        | _, _ => False
-        end.
-  Proof.
-    uPred.unseal; constructor=> n x ?. split; first by destruct 1.
-    destruct prot1, prot2=> //=; [constructor|].
-    by intros [[= ->] [??]]; destruct n; constructor.
-  Qed.
-
-  Lemma proto_later_equiv M prot a Φ2 prot2 :
-    ▷ (prot ≡ TSR a Φ2 prot2) -∗
-    ◇ (∃ Φ1 prot1, prot ≡ TSR a Φ1 prot1 ∗
-                 ▷ (∀ v, Φ1 v ≡ Φ2 v) ∗
-                 ▷ ▷ (∀ v, prot1 v ≡ prot2 v) : uPred M).
-  Proof.
-    iIntros "Heq". destruct prot as [|a' Φ1 prot1].
-    - iDestruct (proto_equivI with "Heq") as ">[]".
-    - iDestruct (proto_equivI with "Heq") as "(>-> & HΦeq & Hsteq)".
-      iExists Φ1, prot1. auto.
-  Qed.
-
-  Lemma dual_proto_flip {M} prot1 prot2 :
-    dual_proto prot1 ≡ prot2 ⊣⊢@{uPredI M} prot1 ≡ dual_proto prot2.
-  Proof.
-    iSplit.
-    - iIntros "Heq". iRewrite -"Heq". by rewrite dual_proto_involutive.
-    - iIntros "Heq". iRewrite "Heq". by rewrite dual_proto_involutive.
-  Qed.
-End proto_ofe.
-
-Arguments protoO : clear implicits.
-
-CoFixpoint proto_map {V PROP PROP'} (f : PROP → PROP')
-    (prot : proto V PROP) : proto V PROP' :=
-  match prot with
-  | TEnd => TEnd
-  | TSR a Φ prot => TSR a (λ v, f (Φ v)) (λ v, proto_map f (prot v))
-  end.
-Lemma proto_map_ext_ne {V PROP} {PROP' : ofeT}
-    (f g : PROP → PROP') (prot : proto V PROP) n :
-  (∀ x, f x ≡{n}≡ g x) → proto_map f prot ≡{n}≡ proto_map g prot.
-Proof.
-  revert n prot. cofix IH=> n prot Hf.
-  rewrite -(proto_force_eq (proto_map f prot)) -(proto_force_eq (proto_map g prot)).
-  destruct prot as [|a Φ prot], n as [|n]; constructor=> v //. apply IH; auto using dist_S.
-Qed.
-Lemma proto_map_ext {V PROP} {B : ofeT} (f g : PROP → B) (prot : proto V PROP) :
-  (∀ x, f x ≡ g x) → proto_map f prot ≡ proto_map g prot.
-Proof.
-  intros Hf. apply equiv_dist=> n. apply proto_map_ext_ne=> v.
-  apply equiv_dist, Hf.
-Qed.
-Instance proto_map_ne {V} {PROP PROP' : ofeT} (f : PROP → PROP') n :
-  (∀ n, Proper (dist n ==> dist n) f) →
-  Proper (dist n ==> dist n) (@proto_map V _ _ f).
-Proof.
-  intros Hf. revert n. cofix IH=> n prot1 prot2 Hst.
-  rewrite -(proto_force_eq (proto_map _ prot1)) -(proto_force_eq (proto_map _ prot2)).
-  destruct Hst; constructor=> v; apply Hf || apply IH; auto.
-Qed.
-Lemma proto_fmap_id {V} {PROP : ofeT} (prot : proto V PROP) :
-  proto_map id prot ≡ prot.
-Proof.
-  revert prot. cofix IH=> prot. rewrite -(proto_force_eq (proto_map _ _)).
-  destruct prot; constructor=> v; auto.
-Qed.
-Lemma proto_fmap_compose {V} {PROP PROP' PROP'' : ofeT}
-    (f : PROP → PROP') (g : PROP' → PROP'') prot :
-  proto_map (g ∘ f) prot ≡ proto_map g (@proto_map V _ _ f prot).
-Proof.
-  revert prot. cofix IH=> prot.
-  rewrite -(proto_force_eq (proto_map _ _)) -(proto_force_eq (proto_map g _)).
-  destruct prot; constructor=> v; auto.
-Qed.
-
-Definition protoO_map {V PROP PROP'}
-    (f : PROP -n> PROP') : protoO V PROP -n> protoO V PROP' :=
-  OfeMor (proto_map f : protoO V PROP → protoO V PROP').
-Instance protoO_map_ne {V} PROP B : NonExpansive (@protoO_map V PROP B).
-Proof. intros n f g ? prot. by apply proto_map_ext_ne. Qed.
-
-Program Definition protoOF {V} (F : oFunctor) : oFunctor := {|
-  oFunctor_car PROP _ B _ := protoO V (oFunctor_car F PROP _ B _);
-  oFunctor_map PROP1 _ PROP2 _ PROP1' _ PROP2' _ fg := protoO_map (oFunctor_map F fg)
-|}.
-Next Obligation. done. Qed.
-Next Obligation.
-  intros V F PROP1 ? PROP2 ? PROP1' ? PROP2' ? n f g Hfg.
-  by apply protoO_map_ne, oFunctor_ne.
-Qed.
-Next Obligation.
-  intros V F PROP ? PROP' ? x. rewrite /= -{2}(proto_fmap_id x).
-  apply proto_map_ext=>y. apply oFunctor_id.
-Qed.
-Next Obligation.
-  intros V F PROP1 ? PROP2 ? PROP3 ? PROP1' ? PROP2' ? PROP3' ? f g f' g' x.
-  rewrite /= -proto_fmap_compose.
-  apply proto_map_ext=>y; apply oFunctor_compose.
-Qed.
-
-Instance protoOF_contractive {V} F :
-  oFunctorContractive F → oFunctorContractive (@protoOF V F).
-Proof.
-  intros ? PROP1 ? PROP2 ? PROP1' ? PROP2' ? n f g Hfg.
-  by apply protoO_map_ne, oFunctor_contractive.
-Qed.
-
-Class IsDualAction (a1 a2 : action) :=
-  is_dual_action : dual_action a1 = a2.
-Instance is_dual_action_default : IsDualAction a (dual_action a) | 100.
-Proof. done. Qed.
-Instance is_dual_action_Send : IsDualAction Send Receive.
-Proof. done. Qed.
-Instance is_dual_action_Receive : IsDualAction Receive Send.
-Proof. done. Qed.
-
-Section DualProto.
-  Context {V : Type} {PROP : ofeT}.
-
-  Class IsDualProto (prot1 prot2 : proto V PROP) :=
-  is_dual_proto : dual_proto prot1 ≡ prot2.
-
-  Global Instance is_dual_default (prot : proto V PROP) :
-    IsDualProto prot (dual_proto prot) | 100.
-  Proof. by rewrite /IsDualProto. Qed.
-
-  Global Instance is_dual_end : IsDualProto (TEnd : proto V PROP) TEnd.
-  Proof. by rewrite /IsDualProto -(proto_force_eq (dual_proto _)). Qed.
-
-  Global Instance is_dual_tsr a1 a2 Φ (prot1 prot2 : V → proto V PROP) :
-    IsDualAction a1 a2 →
-    (∀ x, IsDualProto (prot1 x) (prot2 x)) →
-    IsDualProto (TSR a1 Φ prot1) (TSR a2 Φ prot2).
-  Proof.
-    rewrite /IsDualAction /IsDualProto. intros <- Hst.
-    rewrite /IsDualProto -(proto_force_eq (dual_proto _)) /=.
-    by constructor=> v.
-  Qed.
-End DualProto.
diff --git a/theories/proto/proto_enc.v b/theories/proto/proto_enc.v
deleted file mode 100644
index f9e5bd1491aee343a27dacf396db2626b940323b..0000000000000000000000000000000000000000
--- a/theories/proto/proto_enc.v
+++ /dev/null
@@ -1,71 +0,0 @@
-From iris.heap_lang Require Import proofmode notation.
-From osiris.proto Require Export encodable proto_specs.
-
-Section DualProtoEnc.
-  Context `{ValEncDec V} {PROP: bi} .
-
-  Definition TSR'
-      (a : action) (Φ : V → PROP) (prot : V → proto val PROP) : proto val PROP :=
-    TSR a
-      (λ v, if val_decode v is Some x then Φ x else False)%I
-      (λ v, if val_decode v is Some x then prot x else TEnd (* dummy *)).
-  Global Instance: Params (@TSR') 3.
-
-  Global Instance is_dual_tsr' a1 a2 Φ (st1 st2 : V → proto val PROP) :
-    IsDualAction a1 a2 →
-    (∀ x, IsDualProto (st1 x) (st2 x)) →
-    IsDualProto (TSR' a1 Φ st1) (TSR' a2 Φ st2).
-  Proof.
-    rewrite /IsDualAction /IsDualProto. intros <- Hst.
-    rewrite -(proto_force_eq (dual_proto _)).
-    constructor=> x. done. destruct (val_decode x)=> //.
-    apply is_dual_end.
-  Qed.
-End DualProtoEnc.
-
-Notation "<!> x @ P , prot" :=
-  (TSR' Send (λ x, P%I) (λ x, prot%proto))
-  (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<?> x @ P , prot" :=
-  (TSR' Receive (λ x, P%I) (λ x, prot%proto))
-  (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<!> x , prot" := (<!> x @ True, (prot x))%proto
-  (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<?> x , prot" := (<?> x @ True, (prot x))%proto
-  (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<!> @ Φ , prot" := (TSR' Send Φ prot)
-  (at level 200, prot at level 200) : proto_scope.
-Notation "<?> @ Φ , prot" := (TSR' Receive Φ prot)
-  (at level 200, prot at level 200) : proto_scope.
-
-Section proto_enc_specs.
-  Context `{!heapG Σ, !logrelG val Σ} `{ValEncDec A} (N : namespace).
-
-  Lemma send_st_spec prot γ c s (Φ : A → iProp Σ) w :
-    {{{ Φ w ∗ ⟦ c @ s : <!> @ Φ, prot ⟧{N,γ} }}}
-      send c #s (val_encode w)
-    {{{ RET #(); ⟦ c @ s : prot w ⟧{N,γ} }}}.
-  Proof.
-    iIntros (Ψ) "[HΦ Hsend] HΨ".
-    iApply (send_st_spec with "[HΦ $Hsend]").
-    { by rewrite val_encode_decode. }
-    iNext. rewrite val_encode_decode.
-    by iApply "HΨ".
-  Qed.
-
-  Lemma recv_st_spec prot γ c s (Φ : A → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ Φ, prot ⟧{N,γ} }}}
-      recv c #s
-    {{{ v, RET (val_encode v); ⟦ c @ s : prot v ⟧{N,γ} ∗ Φ v }}}.
-  Proof.
-    iIntros (Ψ) "Hrecv HΨ".
-    iApply (recv_st_spec with "Hrecv").
-    iIntros "!>" (v) "[H HΦ]".
-    iAssert (∃ w, ⌜val_decode v = Some w⌝ ∗ Φ w)%I with "[HΦ]" as (w Hw) "HΦ".
-    { destruct (val_decode v) as [x|]; last done.
-      iExists x. by iFrame. }
-    apply val_decode_encode in Hw as <-.
-    iApply ("HΨ" $!w). iFrame "HΦ".
-    by rewrite val_encode_decode.
-  Qed.
-End proto_enc_specs.
diff --git a/theories/proto/proto_specs.v b/theories/proto/proto_specs.v
deleted file mode 100644
index 968e21debe172058c8f1083c4939314eaa82f91f..0000000000000000000000000000000000000000
--- a/theories/proto/proto_specs.v
+++ /dev/null
@@ -1,338 +0,0 @@
-From osiris.proto Require Export proto_def.
-From osiris.proto Require Export channel.
-From iris.base_logic.lib Require Import invariants.
-From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import list auth excl.
-From osiris.utils Require Import auth_excl.
-
-Class logrelG A Σ := {
-  logrelG_channelG :> chanG Σ;
-  logrelG_authG :> auth_exclG (laterO (protoO A (iPreProp Σ))) Σ;
-}.
-
-Definition logrelΣ A :=
-  #[ chanΣ ; GFunctor (authRF(optionURF (exclRF
-                       (laterOF (@protoOF A idOF))))) ].
-Instance subG_chanΣ {A Σ} : subG (logrelΣ A) Σ → logrelG A Σ.
-Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
-
-Fixpoint prot_eval `{!logrelG val Σ} (vs : list val) (prot1 prot2 : proto val (iProp Σ)) : iProp Σ :=
-  match vs with
-  | [] => prot1 ≡ dual_proto prot2
-  | v::vs => match prot2 with
-             | TSR Receive Φ prot2  => Φ v ∗ ▷ prot_eval vs prot1 (prot2 v)
-             | _ => False
-             end
-  end%I.
-Arguments prot_eval : simpl nomatch.
-
-Record prot_name := ProtName {
-  prot_c_name : chan_name;
-  prot_l_name : gname;
-  prot_r_name : gname
-}.
-
-Definition to_proto_auth_excl `{!logrelG val Σ} (prot : proto val (iProp Σ)) :=
-  to_auth_excl (Next (proto_map iProp_unfold prot)).
-
-Definition prot_own `{!logrelG val Σ} (γ : prot_name) (s : side)
-    (prot : proto val (iProp Σ)) : iProp Σ :=
-  own (side_elim s prot_l_name prot_r_name γ) (◯ to_proto_auth_excl prot)%I.
-
-Definition prot_ctx `{!logrelG val Σ} (γ : prot_name) (s : side)
-    (prot : proto val (iProp Σ)) : iProp Σ :=
-  own (side_elim s prot_l_name prot_r_name γ) (● to_proto_auth_excl prot)%I.
-
-Definition inv_prot `{!logrelG val Σ} (γ : prot_name) (c : val) : iProp Σ :=
-  (∃ l r protl protr,
-    chan_own (prot_c_name γ) Left l ∗
-    chan_own (prot_c_name γ) Right r ∗
-    prot_ctx γ Left protl  ∗
-    prot_ctx γ Right protr ∗
-    ▷ ((⌜r = []⌝ ∗ prot_eval l protl protr) ∨
-       (⌜l = []⌝ ∗ prot_eval r protr protl)))%I.
-
-Definition interp_prot `{!logrelG val Σ, !heapG Σ} (N : namespace) (γ : prot_name)
-    (c : val) (s : side) (prot : proto val (iProp Σ)) : iProp Σ :=
-  (prot_own γ s prot ∗ is_chan N (prot_c_name γ) c ∗ inv N (inv_prot γ c))%I.
-Instance: Params (@interp_prot) 7.
-
-Notation "⟦ c @ s : prot ⟧{ N , γ }" := (interp_prot N γ c s prot)
-  (at level 10, s at next level, prot at next level, γ at next level,
-   format "⟦  c  @  s  :  prot  ⟧{ N , γ }").
-
-Section proto.
-  Context `{!logrelG val Σ, !heapG Σ} (N : namespace).
-
-  Global Instance prot_eval_ne : NonExpansive2 (prot_eval vs).
-  Proof.
-    induction vs as [|v vs IH];
-      destruct 2 as [n|[] Φ1 Φ2 prot1 prot2|n [] Φ1 Φ2 prot1 prot2]=> //=.
-    - by repeat f_equiv.
-    - f_equiv. done. f_equiv. by constructor.
-    - f_equiv. done. f_equiv. by constructor.
-    - f_equiv. done. f_equiv. by constructor.
-    - f_equiv. done. f_equiv. by constructor.
-    - f_equiv. done. by f_contractive.
-    - f_equiv. done. f_contractive. apply IH. by apply dist_S. done.
-  Qed.
-  Global Instance prot_eval_proper vs : Proper ((≡) ==> (≡) ==> (≡)) (prot_eval vs).
-  Proof. apply (ne_proper_2 _). Qed.
-
-  Global Instance to_proto_auth_excl_ne : NonExpansive to_proto_auth_excl.
-  Proof. solve_proper. Qed.
-  Global Instance prot_own_ne γ s : NonExpansive (prot_own γ s).
-  Proof. solve_proper. Qed.
-  Global Instance interp_st_ne γ c s : NonExpansive (interp_prot N γ c s).
-  Proof. solve_proper. Qed.
-  Global Instance interp_st_proper γ c s : Proper ((≡) ==> (≡)) (interp_prot N γ c s).
-  Proof. apply (ne_proper _). Qed.
-
-  Lemma prot_excl_eq γ s prot prot' :
-    prot_ctx γ s prot -∗ prot_own γ s prot' -∗ ▷ (prot ≡ prot').
-  Proof.
-    iIntros "Hauth Hfrag".
-    iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
-    iDestruct (to_auth_excl_valid with "Hvalid") as "Hvalid".
-    iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext.
-    assert (∀ prot : proto val (iProp Σ),
-      proto_map iProp_fold (proto_map iProp_unfold prot) ≡ prot) as help.
-    { intros prot''. rewrite -proto_fmap_compose -{2}(proto_fmap_id prot'').
-      apply proto_map_ext=> P. by rewrite /= iProp_fold_unfold. }
-    rewrite -{2}(help prot). iRewrite "Hvalid". by rewrite help.
-  Qed.
-
-  Lemma prot_excl_update γ s prot prot' prot'' :
-    prot_ctx γ s prot -∗ prot_own γ s prot' ==∗ prot_ctx γ s prot'' ∗ prot_own γ s prot''.
-  Proof.
-    iIntros "Hauth Hfrag".
-    iDestruct (own_update_2 with "Hauth Hfrag") as "H".
-    { eapply (auth_update _ _ (to_proto_auth_excl prot'')
-                              (to_proto_auth_excl prot'')).
-      eapply option_local_update.
-      eapply exclusive_local_update. done. }
-    by rewrite own_op.
-  Qed.
-
-  Lemma prot_eval_send (Φ : val → iProp Σ) prot vs v protr :
-    Φ v -∗ prot_eval vs (<!> @ Φ, prot) protr -∗ prot_eval (vs ++ [v]) (prot v) protr.
-  Proof.
-    iIntros "HΦ".
-    iRevert (protr).
-    iInduction vs as [|v' vs] "IH"; iIntros (protr) "Heval".
-    - iDestruct (dual_proto_flip with "Heval") as "Heval".
-      iRewrite -"Heval"; simpl.
-      rewrite dual_proto_involutive.
-      by iFrame.
-    - destruct protr as [|[] Φ' protr]=> //=.
-      iDestruct "Heval" as "[$ Heval]".
-      by iApply ("IH" with "HΦ").
-  Qed.
-
-  Lemma prot_eval_recv (Φ : val → iProp Σ) prot1 l prot2 v :
-     prot_eval (v :: l) prot1 (<?> @ Φ, prot2) -∗ ▷ prot_eval l prot1 (prot2 v) ∗ Φ v.
-  Proof. iDestruct 1 as "[HΦ Heval]". iFrame. Qed.
-
-  Lemma new_chan_vs prot E c cγ :
-    is_chan N cγ c ∗
-    chan_own cγ Left [] ∗
-    chan_own cγ Right [] ={E}=∗ ∃ lγ rγ,
-      let γ := ProtName cγ lγ rγ in
-      ⟦ c @ Left : prot ⟧{N,γ} ∗ ⟦ c @ Right : dual_proto prot ⟧{N,γ}.
-  Proof.
-    iIntros "[#Hcctx [Hcol Hcor]]".
-    iMod (own_alloc (● (to_proto_auth_excl prot) ⋅
-                     ◯ (to_proto_auth_excl prot))) as (lγ) "[Hlsta Hlstf]".
-    { by apply auth_both_valid_2. }
-    iMod (own_alloc (● (to_proto_auth_excl (dual_proto prot)) ⋅
-                     ◯ (to_proto_auth_excl (dual_proto prot)))) as (rγ) "[Hrsta Hrstf]".
-    { by apply auth_both_valid_2. }
-    pose (ProtName cγ lγ rγ) as protγ.
-    iMod (inv_alloc N _ (inv_prot protγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
-    { iNext. rewrite /inv_prot. eauto 10 with iFrame. }
-    iModIntro.
-    iExists _, _.
-    iFrame "Hlstf Hrstf Hcctx Hinv".
-  Qed.
-
-  Lemma new_chan_st_spec prot1 prot2 :
-    IsDualProto prot1 prot2 →
-    {{{ True }}}
-      new_chan #()
-    {{{ c γ, RET c; ⟦ c @ Left : prot1 ⟧{N,γ} ∗ ⟦ c @ Right : prot2 ⟧{N,γ} }}}.
-  Proof.
-    rewrite /IsDualProto.
-    iIntros (Hprot Φ _) "HΦ".
-    iApply (wp_fupd).
-    iApply (new_chan_spec)=> //.
-    iModIntro.
-    iIntros (c γ) "[Hc Hctx]".
-    iMod (new_chan_vs prot1 ⊤ c γ with "[-HΦ]") as "H".
-    { rewrite /is_chan. eauto with iFrame. }
-    iDestruct "H" as (lγ rγ) "[Hl Hr]".
-    iApply "HΦ".
-    rewrite Hprot.
-    by iFrame.
-  Qed.
-
-  Lemma send_vs c γ s (Φ : val → iProp Σ) prot E :
-    ↑N ⊆ E →
-    ⟦ c @ s : <!> @ Φ, prot ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
-      chan_own (prot_c_name γ) s vs ∗
-      ▷ ∀ v, Φ v -∗
-             chan_own (prot_c_name γ) s (vs ++ [v]) ={E∖↑N,E}=∗
-             ⟦ c @ s : prot v ⟧{N,γ}.
-  Proof.
-    iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
-    iInv N as (l r protl protr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
-    iModIntro.
-    destruct s.
-    - iExists _.
-      iIntros "{$Hclf} !>" (v) "HΦ Hclf".
-      iRename "Hstf" into "Hstlf".
-      iDestruct (prot_excl_eq with "Hstla Hstlf") as "#Heq".
-      iMod (prot_excl_update _ _ _ _ (prot v) with "Hstla Hstlf") as "[Hstla Hstlf]".
-      iMod ("Hclose" with "[-Hstlf]") as "_".
-      { iNext.
-        iExists _,_,_,_. iFrame.
-        iLeft.
-        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
-        - iSplit=> //.
-          iApply (prot_eval_send with "HΦ").
-          by iRewrite "Heq" in "Heval".
-        - iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //=.
-          iSplit; first done.
-          iRewrite "Heval". simpl. iFrame "HΦ". by rewrite dual_proto_involutive. }
-      iModIntro. iFrame. auto.
-    - iExists _.
-      iIntros "{$Hcrf} !>" (v) "HΦ Hcrf".
-      iRename "Hstf" into "Hstrf".
-      iDestruct (prot_excl_eq with "Hstra Hstrf") as "#Heq".
-      iMod (prot_excl_update _ _ _ _ (prot v) with "Hstra Hstrf") as "[Hstra Hstrf]".
-      iMod ("Hclose" with "[-Hstrf]") as "_".
-      { iNext.
-        iExists _, _, _, _. iFrame.
-        iRight.
-        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
-        - iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
-          iSplit; first done. simpl.
-          iRewrite "Heval". simpl. iFrame "HΦ". by rewrite dual_proto_involutive.
-        - iSplit=> //.
-          iApply (prot_eval_send with "HΦ").
-          by iRewrite "Heq" in "Heval". }
-      iModIntro. iFrame. auto.
-  Qed.
-
-  Lemma send_st_spec prot γ c s (Φ : val → iProp Σ) v :
-    {{{ Φ v ∗ ⟦ c @ s : <!> @ Φ, prot ⟧{N,γ} }}}
-      send c #s v
-    {{{ RET #(); ⟦ c @ s : prot v ⟧{N,γ} }}}.
-  Proof.
-    iIntros (Ψ) "[HΦ Hsend] HΨ".
-    iApply (send_spec with "[#]").
-    { iDestruct "Hsend" as "[? [$ ?]]". }
-    iMod (send_vs with "Hsend") as (vs) "[Hch H]"; first done.
-    iModIntro. iExists vs. iFrame "Hch".
-    iIntros "!> Hupd". iApply "HΨ".
-    iApply ("H" $! v with "HΦ"). by destruct s.
-  Qed.
-
-  Lemma try_recv_vs c γ s (Φ : val → iProp Σ) prot E :
-    ↑N ⊆ E →
-    ⟦ c @ s : TSR Receive Φ prot ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
-      chan_own (prot_c_name γ) (dual_side s) vs ∗
-      ▷ ((⌜vs = []⌝ -∗
-           chan_own (prot_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
-           ⟦ c @ s : <?> @ Φ, prot ⟧{N,γ}) ∧
-         (∀ v vs',
-           ⌜vs = v :: vs'⌝ -∗
-           chan_own (prot_c_name γ) (dual_side s) vs' ={E∖↑N,E}=∗
-           ⟦ c @ s : prot v ⟧{N,γ} ∗ ▷ Φ v)).
-  Proof.
-    iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
-    iInv N as (l r protl protr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
-    iExists (side_elim s r l). iModIntro.
-    destruct s; simpl.
-    - iIntros "{$Hcrf} !>".
-      iRename "Hstf" into "Hstlf".
-      iDestruct (prot_excl_eq with "Hstla Hstlf") as "#Heq".
-      iSplit.
-      + iIntros (->) "Hown".
-        iMod ("Hclose" with "[-Hstlf]") as "_".
-        { iNext. iExists l, [], _, _. iFrame. }
-        iModIntro. iFrame "Hcctx ∗ Hinv".
-      + iIntros (v vs ->) "Hown".
-        iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
-        iMod (prot_excl_update _ _ _ _ (prot v) with "Hstla Hstlf") as "[Hstla Hstlf]".
-        iDestruct (proto_later_equiv with "Heq") as ">Hleq".
-        iDestruct "Hleq" as (P1 prot1) "(Hsteq & HPeq & Hsteq')".
-        iRewrite "Hsteq" in "Heval".
-        iDestruct (prot_eval_recv with "Heval") as "[Heval HP]".
-        iMod ("Hclose" with "[-Hstlf HP]") as "H".
-        { iExists _, _,_ ,_. iFrame. iRight.
-          iNext. iSplit=> //. iNext. by iRewrite -("Hsteq'" $! v). }
-        iModIntro. iFrame "Hstlf Hcctx Hinv".
-        iNext. by iRewrite -("HPeq" $! v).
-    - iIntros "{$Hclf} !>".
-      iRename "Hstf" into "Hstrf".
-      iDestruct (prot_excl_eq with "Hstra Hstrf") as "#Heq".
-      iSplit=> //.
-      + iIntros (->) "Hown".
-        iMod ("Hclose" with "[-Hstrf]") as "_".
-        { iNext. iExists [], r, _, _. iFrame. }
-        iModIntro. iFrame "Hcctx ∗ Hinv".
-      + iIntros (v vs' ->) "Hown".
-        iDestruct "Hinv'" as "[[>-> Heval]|[>% Heval]]"; last done.
-        iMod (prot_excl_update _ _ _ _ (prot v) with "Hstra Hstrf") as "[Hstra Hstrf]".
-        iDestruct (proto_later_equiv with "Heq") as ">Hleq".
-        iDestruct "Hleq" as (P1 prot1) "(Hsteq & HPeq & Hsteq')".
-        iRewrite "Hsteq" in "Heval".
-        iDestruct (prot_eval_recv with "Heval") as "[Heval HP]".
-        iMod ("Hclose" with "[-Hstrf HP]") as "_".
-        { iExists _, _, _, _. iFrame. iLeft.
-          iNext. iSplit=> //. iNext. by iRewrite -("Hsteq'" $! v). }
-        iModIntro. iFrame "Hstrf Hcctx Hinv".
-        iNext. by iRewrite -("HPeq" $! v).
-  Qed.
-
-  Lemma try_recv_st_spec prot γ c s (Φ : val → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ Φ, prot ⟧{N,γ} }}}
-      try_recv c #s
-    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : <?> @ Φ, prot ⟧{N,γ}) ∨
-                  (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : prot w ⟧{N,γ} ∗ ▷ Φ w)}}}.
-  Proof.
-    iIntros (Ψ) "Hrecv HΨ".
-    iApply (try_recv_spec with "[#]").
-    { iDestruct "Hrecv" as "[? [$ ?]]". }
-    iMod (try_recv_vs with "Hrecv") as (vs) "[Hch H]"; first done.
-    iModIntro. iExists vs. iFrame "Hch".
-    iIntros "!>".
-    iSplit.
-    - iIntros (Hvs) "Hown".
-      iDestruct "H" as "[H _]".
-      iMod ("H" $!Hvs with "Hown") as "H".
-      iModIntro.
-      iApply "HΨ"=> //.
-      eauto with iFrame.
-    - iIntros (v vs' Hvs) "Hown".
-      iDestruct "H" as "[_ H]".
-      iMod ("H" $!v vs' Hvs with "Hown") as "H".
-      iModIntro.
-      iApply "HΨ"; eauto with iFrame.
-  Qed.
-
-  Lemma recv_st_spec prot γ c s (Φ : val → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ Φ,  prot ⟧{N,γ} }}}
-      recv c #s
-    {{{ v, RET v; ⟦ c @ s : prot v ⟧{N,γ} ∗ Φ v }}}.
-  Proof.
-    iIntros (Ψ) "Hrecv HΨ".
-    iLöb as "IH". wp_rec.
-    wp_apply (try_recv_st_spec with "Hrecv").
-    iIntros (v) "H".
-    iDestruct "H" as "[[-> H]| H]".
-    - wp_pures. by iApply ("IH" with "[H]").
-    - iDestruct "H" as (w ->) "[H HΦ]".
-      wp_pures. iApply "HΨ". iFrame.
-  Qed.
-End proto. 
diff --git a/theories/proto/side.v b/theories/proto/side.v
deleted file mode 100644
index f7e7698b65838a4a6f0fd3587765935eb6c44fa2..0000000000000000000000000000000000000000
--- a/theories/proto/side.v
+++ /dev/null
@@ -1,9 +0,0 @@
-From iris.heap_lang Require Import proofmode notation.
-From osiris.proto Require Export involutive.
-
-Inductive side := Left | Right.
-Instance side_inhabited : Inhabited side := populate Left.
-Definition dual_side (s : side) : side :=
-  match s with Left => Right | Right => Left end.
-Instance dual_side_involutive : Involutive (=) dual_side.
-Proof. by intros []. Qed.
\ No newline at end of file
diff --git a/theories/utils/auth_excl.v b/theories/utils/auth_excl.v
index 8bc93b575086a00eb0c053e4c3438dce7a4e5f2d..c51d82c71de71c8bed9b952e3c25eb4e224e53bd 100644
--- a/theories/utils/auth_excl.v
+++ b/theories/utils/auth_excl.v
@@ -1,7 +1,6 @@
-From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl auth.
-From iris.base_logic.lib Require Import auth.
+From iris.base_logic.lib Require Import own.
 Set Default Proof Using "Type".
 
 Class auth_exclG (A : ofeT) (Σ : gFunctors) := AuthExclG {
diff --git a/theories/proto/encodable.v b/theories/utils/encodable.v
similarity index 100%
rename from theories/proto/encodable.v
rename to theories/utils/encodable.v
diff --git a/theories/proto/list.v b/theories/utils/list.v
similarity index 99%
rename from theories/proto/list.v
rename to theories/utils/list.v
index 2764ce3d76225c212af1058e7b113fd7a6135491..58fe05e39ed3098eb0dfd556543478d963f17a12 100644
--- a/theories/proto/list.v
+++ b/theories/utils/list.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.
-From osiris Require Export encodable.
+From osiris.utils Require Export encodable.
 
 (** Immutable ML-style functional lists *)
 Instance list_val_enc `{ValEnc A} : ValEnc (list A) :=
@@ -148,6 +148,7 @@ Proof.
   by wp_apply (lcons_spec with "[//]").
 Qed.
 
+(*
 Lemma llist_member_spec `{EqDecision A} (xs : list A) (x : A) :
   {{{ True }}}
     llist_member (val_encode x) (val_encode xs)
@@ -164,6 +165,7 @@ Proof.
   - by rewrite bool_decide_true; last by right.
   - by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
 Qed.
+*)
 
 Lemma lreplicate_spec i x :
   {{{ True }}}