diff --git a/_CoqProject b/_CoqProject
index 04256a8e63d51c4619561378ef3b57803a63b4b7..90943e2e0e285d6e8b05847cb5cb24375d656cc6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,6 @@
 -Q theories osiris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-theories/base_logic/auth_excl.v
+theories/utils/auth_excl.v
 theories/proto/encodable.v
 theories/proto/list.v
 theories/proto/channel.v
@@ -10,9 +10,7 @@ theories/proto/proto_def.v
 theories/proto/proto_specs.v
 theories/proto/proto_enc.v
 theories/proto/branching.v
-theories/examples/examples.v
 theories/examples/proofs.v
 theories/examples/proofs_enc.v
-theories/examples/branching_examples.v
 theories/examples/branching_proofs.v
 theories/examples/list_sort.v
diff --git a/theories/examples/branching_examples.v b/theories/examples/branching_examples.v
deleted file mode 100644
index 7fbe0c815da30ee5c76d1d33b8ae6b9fff10d700..0000000000000000000000000000000000000000
--- a/theories/examples/branching_examples.v
+++ /dev/null
@@ -1,18 +0,0 @@
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Import proofmode notation.
-From iris.base_logic Require Import invariants.
-From osiris.proto Require Import channel branching.
-
-Section BranchingExamples.
-  Context `{!heapG Σ} (N : namespace).
-
-  Definition branch_example b : expr :=
-    (let: "c" := new_chan #() in
-     select "c" #Left #b;;
-     Fork(branch: "c" @ #Right
-      left  send "c" #Right #5
-      right #());;
-     (if: #b then recv "c" #Left else #()))%E.
-
-End BranchingExamples.
\ No newline at end of file
diff --git a/theories/examples/branching_proofs.v b/theories/examples/branching_proofs.v
index 16fcaaa0731d9b23114548396e72e7c5d2235455..ab29ac04cb4c2ee2cb73fa4985eff1edf8a997db 100644
--- a/theories/examples/branching_proofs.v
+++ b/theories/examples/branching_proofs.v
@@ -1,13 +1,16 @@
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From iris.base_logic Require Import invariants.
 From osiris.proto Require Import branching.
-From osiris.examples Require Import branching_examples.
+
+Definition branch_example b : expr :=
+  (let: "c" := new_chan #() in
+   select "c" #Left #b;;
+   Fork(branch: "c" @ #Right
+    left  send "c" #Right #5
+    right #());;
+   (if: #b then recv "c" #Left else #()))%E.
 
 Section BranchingExampleProofs.
-  Context `{!heapG Σ} (N : namespace).
-  Context `{!logrelG val Σ}.
+  Context `{!heapG Σ, !logrelG val Σ}.
 
   Lemma branch_proof b :
     {{{ True }}}
@@ -17,29 +20,24 @@ Section BranchingExampleProofs.
                   | Right => ⌜v = #()⌝
                   end }}}.
   Proof.
-    iIntros (Φ H) "HΦ".
+    iIntros (Φ _) "HΦ".
     rewrite /branch_example.
-    wp_apply (new_chan_st_spec N
-      ((<?> v @ ⌜v = 5⌝, TEnd) <+> (TEnd)))=> //;
+    wp_apply (new_chan_st_spec nroot ((<?> v @ ⌜v = 5⌝, TEnd) <+> TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]".
-    wp_apply (select_st_spec with "Hstl");
-    iIntros "Hstl".
+    wp_apply (select_st_spec with "Hstl"); iIntros "Hstl".
     wp_pures.
     wp_apply (wp_fork with "[Hstr]").
     - iNext.
       simpl.
       wp_apply (branch_st_spec with "Hstr")=> //;
-      iIntros (v) "[Hstr | Hstr]"; iDestruct "Hstr" as (->) "Hstr".
-      + wp_pures. 
-        wp_apply (send_st_spec N Z with "[$Hstr //]").
-        iIntros "Hstr". done.
-      + wp_pures. done.
+      iIntros (v) "[[-> Hstr]|[-> Hstr]]".
+      + wp_pures.
+        wp_apply (send_st_spec (A:=Z) with "[$Hstr //]"); auto.
+      + by wp_pures.
     - destruct b.
-      + wp_apply (recv_st_spec N Z with "Hstl");
-        iIntros (v) "[Hstl HP]".
-        iDestruct "HP" as %->.
+      + wp_apply (recv_st_spec (A:=Z) with "Hstl");
+        iIntros (v) "[Hstl ->]".
         by iApply "HΦ".
       + wp_pures. by iApply "HΦ".
   Qed.
-
 End BranchingExampleProofs.
\ No newline at end of file
diff --git a/theories/examples/examples.v b/theories/examples/examples.v
deleted file mode 100644
index bf596026775dbf589071a49f49de420e4d4fafb6..0000000000000000000000000000000000000000
--- a/theories/examples/examples.v
+++ /dev/null
@@ -1,55 +0,0 @@
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Import proofmode notation.
-From iris.base_logic Require Import invariants.
-From osiris.proto Require Import proto_specs.
-
-Section Examples.
-  Context `{!heapG Σ} (N : namespace).
-
-  Definition seq_example : expr :=
-    (let: "c" := new_chan #() in
-     send "c" #Left #5;;
-     recv "c" #Right)%E.
-
-  Definition par_example : expr :=
-    (let: "c" := new_chan #() in
-     Fork(send "c" #Left #5);;
-     recv "c" #Right)%E.
-
-  Definition par_2_example : expr :=
-    (let: "c" := new_chan #() in
-     Fork(let: "v" := recv "c" #Right in send "c" #Right ("v"+#2));;
-     send "c" #Left #5;;recv "c" #Left)%E.
-
-  Definition heaplet_example : expr :=
-    (let: "c" := new_chan #() in
-     Fork(send "c" #Left (ref #5));;
-     !(recv "c" #Right))%E.
-
-  Definition channel_example : expr :=
-    (let: "c" := new_chan #() in
-     Fork(
-         let: "c'" := new_chan #() in
-         send "c" #Left ("c'");; send "c'" #Left #5);;
-     let: "c'" := recv "c" #Right in
-     recv "c'" #Right
-    )%E.
-
-  Definition bad_seq_example : expr :=
-    (let: "c" := new_chan #() in
-     let: "v" := recv "c" #Right in
-     send "c" #Left #5;; "v")%E.
-
-  Definition bad_par_example : expr :=
-    (let: "c" := new_chan #() in
-     Fork(#());;
-     recv "c" #Right)%E.
-
-  Definition bad_interleave_example : expr :=
-    (let: "c" := new_chan #() in
-     let: "c'" := new_chan #() in
-     Fork(recv "c" #Right;; send "c'" #Right #5);;
-     recv "c'" #Left;; send "c" #Left #5)%E.
-  
-End Examples.
\ No newline at end of file
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 150ae9122a2ae87cdea4044d0e813d7a43843efc..fd0a3f1194e77b4af675d2d719aa242d33821560 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -1,17 +1,12 @@
 From stdpp Require Import sorting.
-Require Import Coq.Lists.List.
-Require Import Omega.
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From iris.base_logic Require Import invariants.
 From osiris.proto Require Import list channel proto_enc.
 
 Section ListSortExample.
-  Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
+  Context `{!heapG Σ, !logrelG val Σ} (N : namespace).
 
   Section SortService.
-    Context `{EncDec T}.
+    Context `{ValEncDec T}.
     Context (R : relation T) `{!Total R} `{∀ x y, Decision (R x y)}.
 
     Definition lsplit_ref : val :=
@@ -19,13 +14,13 @@ Section ListSortExample.
                (ref (Fst "ys_zs"), ref (Snd ("ys_zs"))).
 
     Lemma lsplit_ref_spec lxs (x : T) (xs : list T) :
-      {{{ lxs ↦ encode (x::xs) }}}
+      {{{ lxs ↦ val_encode (x :: xs) }}}
         lsplit_ref #lxs
-      {{{ lys lzs ys zs, RET (#lys,#lzs);
-          ⌜(x::xs) = ys++zs⌝ ∗
-                       lxs ↦ encode (x::xs) ∗
-                       lys ↦ encode ys ∗
-                       lzs ↦ encode zs }}}.
+      {{{ 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 <-).
@@ -60,14 +55,14 @@ Section ListSortExample.
 
     Definition cmp_spec (cmp : val) : iProp Σ :=
       (∀ x y, {{{ True }}}
-                cmp (encode x) (encode y)
-              {{{ RET encode (bool_decide (R x y)); True}}})%I.
+                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 (encode ys) (encode zs)
-      {{{ RET (encode (list_merge (R) ys zs)); 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".
@@ -103,8 +98,8 @@ Section ListSortExample.
     Lemma lmerge_ref_spec (cmp : val) ldx tmp ys zs :
       cmp_spec cmp -∗
       {{{ ldx ↦ tmp }}}
-        lmerge_ref cmp #ldx (encode ys) (encode zs)
-      {{{ RET #(); ldx ↦ encode (list_merge R ys zs) }}}.
+        lmerge_ref cmp #ldx (val_encode ys) (val_encode zs)
+      {{{ RET #(); ldx ↦ val_encode (list_merge R ys zs) }}}.
     Proof.
       iIntros "#Hcmp_spec".
       iIntros (Φ).
@@ -139,12 +134,12 @@ Section ListSortExample.
 
     Definition sort_protocol xs : proto val (iProp Σ) :=
       (<?> cmp @ cmp_spec cmp,
-       <?> l @ l ↦ encode xs,
+       <?> l @ l ↦ val_encode xs,
        <!> l' @ ⌜l = l'⌝ ∗
                 (∃ ys : list T,
-                    l' ↦ encode ys ∗
-                       ⌜Sorted (R) ys⌝ ∗
-                       ⌜Permutation ys xs⌝),
+                    l' ↦ val_encode ys ∗
+                    ⌜Sorted R ys⌝ ∗
+                    ⌜Permutation ys xs⌝),
        TEnd).
 
     Lemma list_sort_service_spec γ c xs :
@@ -156,23 +151,22 @@ Section ListSortExample.
       iLöb as "IH".
       iIntros (γ c xs Φ) "Hstr HΦ".
       wp_lam.
-      wp_apply (recv_st_spec N val with "Hstr").
+      wp_apply (recv_st_spec (A:=val) with "Hstr").
       iIntros (cmp) "[Hstr #Hcmp_spec]".
       wp_pures.
-      wp_apply (recv_st_spec N loc with "Hstr").
-      iIntros (v) "Hstr".
-      iDestruct "Hstr" as "[Hstr HP]".
+      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 N loc with "[HP Hstr]")=> //. iFrame.
+        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 N loc with "[HP Hstr]")=> //. iFrame.
+        wp_apply (send_st_spec (A:=loc) with "[HP Hstr]")=> //. iFrame.
         eauto 10 with iFrame.
       }
       wp_apply (llength_spec)=> //; iIntros (_).
@@ -191,19 +185,19 @@ Section ListSortExample.
       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 N val with "[Hstly]"). iFrame. done.
+      wp_apply (send_st_spec (A:=val) with "[Hstly]"). iFrame. done.
       iIntros "Hstly".
-      wp_apply (send_st_spec N loc with "[Hhdy Hstly]"). iFrame.
+      wp_apply (send_st_spec (A:=loc) with "[Hhdy Hstly]"). iFrame.
       iIntros "Hstly".
-      wp_apply (send_st_spec N val with "[Hstlz]"). iFrame. done.
+      wp_apply (send_st_spec (A:=val) with "[Hstlz]"). iFrame. done.
       iIntros "Hstlz".
-      wp_apply (send_st_spec N loc with "[Hhdz Hstlz]"). iFrame.
+      wp_apply (send_st_spec (A:=loc) with "[Hhdz Hstlz]"). iFrame.
       iIntros "Hstlz".
-      wp_apply (recv_st_spec N loc with "Hstly").
+      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 N loc with "Hstlz").
+      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].
@@ -211,7 +205,7 @@ Section ListSortExample.
       wp_load.
       wp_apply (lmerge_ref_spec with "Hcmp_spec Hhdx").
       iIntros "Hhdx".
-      wp_apply (send_st_spec N loc with "[Hstr Hhdx]").
+      wp_apply (send_st_spec (A:=loc) with "[Hstr Hhdx]").
       {
         iFrame.
         iSplit=> //.
@@ -233,8 +227,8 @@ Section ListSortExample.
 
   Lemma compare_vals_spec (x y : Z) :
     {{{ True }}}
-      compare_vals (encode x) (encode y)
-    {{{ RET (encode (bool_decide (x ≤ y))); True }}}.
+      compare_vals (val_encode x) (val_encode y)
+    {{{ RET val_encode (bool_decide (x ≤ y)); True }}}.
   Proof. iIntros (Φ) "_ HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
 
   Definition list_sort : val :=
@@ -246,9 +240,9 @@ Section ListSortExample.
         recv "c" #Left.
 
   Lemma list_sort_spec l xs :
-    {{{ l ↦ encode xs }}}
+    {{{ l ↦ val_encode xs }}}
       list_sort #l
-    {{{ ys, RET #l; l ↦ encode ys ∗ ⌜Sorted (≤) ys⌝ ∗ ⌜Permutation ys xs⌝ }}}.
+    {{{ ys, RET #l; l ↦ val_encode ys ∗ ⌜Sorted (≤) ys⌝ ∗ ⌜Permutation ys xs⌝ }}}.
   Proof.
      iIntros (Φ) "Hc HΦ".
      wp_lam.
@@ -259,15 +253,15 @@ Section ListSortExample.
        iApply (list_sort_service_spec (≤) γ c xs with "Hstr").
        iNext. iNext. iIntros "Hstr". done.
      }
-     wp_apply (send_st_spec N val with "[$Hstl]").
+     wp_apply (send_st_spec (A:=val) with "[$Hstl]").
      {
        iIntros (x y Φ').
        iApply compare_vals_spec=> //.
      }
      iIntros "Hstl".
-     wp_apply (send_st_spec N loc with "[Hc $Hstl]"). iFrame.
+     wp_apply (send_st_spec (A:=loc) with "[Hc $Hstl]"). iFrame.
      iIntros "Hstl".
-     wp_apply (recv_st_spec N loc with "Hstl").
+     wp_apply (recv_st_spec (A:=loc) with "Hstl").
      iIntros (v) "[Hstl HP]".
      iDestruct "HP" as (<- ys) "[Hys Hys_sorted_of]".
      iApply "HΦ". iFrame.
diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index 608ecfbf7b8eed9d77403ac786aa3b4dadeba40f..f1b490d634a9b2460380ea3b276fac363150970e 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -1,28 +1,65 @@
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import list auth excl.
-From iris.base_logic Require Import invariants.
 From osiris.proto Require Import proto_enc.
-From osiris.examples Require Import examples.
+
+Definition seq_example : expr :=
+  (let: "c" := new_chan #() in
+   send "c" #Left #5;;
+   recv "c" #Right)%E.
+
+Definition par_example : expr :=
+  (let: "c" := new_chan #() in
+   Fork(send "c" #Left #5);;
+   recv "c" #Right)%E.
+
+Definition par_2_example : expr :=
+  (let: "c" := new_chan #() in
+   Fork(let: "v" := recv "c" #Right in send "c" #Right ("v"+#2));;
+   send "c" #Left #5;;recv "c" #Left)%E.
+
+Definition heaplet_example : expr :=
+  (let: "c" := new_chan #() in
+   Fork(send "c" #Left (ref #5));;
+   !(recv "c" #Right))%E.
+
+Definition channel_example : expr :=
+  (let: "c" := new_chan #() in
+   Fork(
+       let: "c'" := new_chan #() in
+       send "c" #Left ("c'");; send "c'" #Left #5);;
+   let: "c'" := recv "c" #Right in
+   recv "c'" #Right
+  )%E.
+
+Definition bad_seq_example : expr :=
+  (let: "c" := new_chan #() in
+   let: "v" := recv "c" #Right in
+   send "c" #Left #5;; "v")%E.
+
+Definition bad_par_example : expr :=
+  (let: "c" := new_chan #() in
+   Fork(#());;
+   recv "c" #Right)%E.
+
+Definition bad_interleave_example : expr :=
+  (let: "c" := new_chan #() in
+   let: "c'" := new_chan #() in
+   Fork(recv "c" #Right;; send "c'" #Right #5);;
+   recv "c'" #Left;; send "c" #Left #5)%E.
 
 Section ExampleProofsEnc.
-  Context `{!heapG Σ} (N : namespace).
-  Context `{!logrelG val Σ}.
+  Context `{!heapG Σ, !logrelG val Σ}.
 
   Lemma seq_proof :
     {{{ True }}} seq_example {{{ v, RET v; ⌜v = #5⌝ }}}.
   Proof.
-    iIntros (Φ H) "HΦ".
+    iIntros (Φ _) "HΦ".
     rewrite /seq_example.
-    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
-    iIntros (c γ) "[Hstl Hstr]"=> /=.
-    wp_apply (send_st_spec N Z with "[$Hstl //]");
-    iIntros "Hstl".
-    wp_apply (recv_st_spec N Z with "[Hstr]"). iApply "Hstr".
-    iIntros (v) "[Hstr HP]".
+    wp_apply (new_chan_st_spec nroot (<!> v @ ⌜v = 5⌝, TEnd))=> //;
+      iIntros (c γ) "[Hstl Hstr]"=> /=.
+    wp_apply (send_st_spec (A:=Z) with "[$Hstl //]"); iIntros "Hstl".
+    wp_apply (recv_st_spec (A:=Z) with "Hstr").
+    iIntros (v) "[Hstr ->]".
     iApply "HΦ".
-    iDestruct "HP" as %->.
     eauto.
   Qed.
 
@@ -31,44 +68,34 @@ Section ExampleProofsEnc.
       par_2_example
     {{{ (v:Z), RET #v; ⌜7 ≤ v⌝ }}}.
   Proof.
-    iIntros (Φ H) "HΦ".
+    iIntros (Φ _) "HΦ".
     rewrite /par_2_example.
-    wp_apply (new_chan_st_spec N
-      (<!> v @ ⌜5 ≤ v⌝,
-               <?> v' @ ⌜v+2 ≤ v'⌝,
-                        TEnd))=> //;
+    wp_apply (new_chan_st_spec nroot
+      (<!> v @ ⌜5 ≤ v⌝, <?> v' @ ⌜v+2 ≤ v'⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstr]").
     - iNext.
-      wp_apply (recv_st_spec N Z with "Hstr");
-      iIntros (v) "[Hstr HP]".
-      wp_apply (send_st_spec N Z with "[$Hstr //]");
-      iIntros "Hstr".
+      wp_apply (recv_st_spec (A:=Z) with "Hstr"); iIntros (v) "[Hstr HP]".
+      wp_apply (send_st_spec (A:=Z) with "[$Hstr //]"); iIntros "Hstr".
       eauto.
-    - wp_apply (send_st_spec N Z with "[$Hstl //]");
-      iIntros "Hstl".
-      wp_apply (recv_st_spec N Z with "Hstl");
-      iIntros (v) "[Hstl HP]".
-      iApply "HΦ".
-      iDestruct "HP" as %HP.
-      iPureIntro. lia.
+    - wp_apply (send_st_spec (A:=Z) with "[$Hstl //]"); iIntros "Hstl".
+      wp_apply (recv_st_spec (A:=Z) with "Hstl"); iIntros (v) "[Hstl %]".
+      iApply "HΦ". iPureIntro. lia.
   Qed.
 
   Lemma heaplet_proof :
     {{{ True }}} heaplet_example {{{ v l, RET v; ⌜v = #5⌝ ∗ l ↦ v }}}.
   Proof.
     rewrite /heaplet_example.
-    iIntros (Φ H) "HΦ".
-    wp_apply (new_chan_st_spec N (<!> v @ (v ↦ #5), TEnd))=> //;
+    iIntros (Φ _) "HΦ".
+    wp_apply (new_chan_st_spec nroot (<!> v @ (v ↦ #5), TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext.
       wp_alloc l as "HP".
-      wp_apply (send_st_spec N loc with "[$Hstl HP]")=> //;
-      iIntros "Hstl".
+      wp_apply (send_st_spec (A:=loc) with "[$Hstl HP]")=> //; iIntros "Hstl".
       eauto.
-    - wp_apply (recv_st_spec N loc with "Hstr");
-      iIntros (v) "[Hstr HP]".
+    - wp_apply (recv_st_spec (A:=loc) with "Hstr"); iIntros (v) "[Hstr HP]".
       wp_load.
       iApply "HΦ".
       by iFrame.
@@ -77,43 +104,36 @@ Section ExampleProofsEnc.
   Lemma channel_proof :
     {{{ True }}} channel_example {{{ v, RET v; ⌜v = #5⌝ }}}.
   Proof.
-    iIntros (Φ H) "HΦ".
+    iIntros (Φ _) "HΦ".
     rewrite /channel_example.
-    wp_apply (new_chan_st_spec N
-      (<!> v @ (∃ γ, ⟦ v @ Right : <?> v @ ⌜v = 5⌝, TEnd ⟧{N,γ}),
+    wp_apply (new_chan_st_spec nroot
+      (<!> v @ (∃ γ, ⟦ v @ Right : <?> v @ ⌜v = 5⌝, TEnd ⟧{nroot,γ}),
                TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext.
-      wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
-      iIntros (c' γ') "[Hstl' Hstr']"=> /=.
-      wp_apply (send_st_spec N val with "[Hstl Hstr']");
+      wp_apply (new_chan_st_spec nroot (<!> v @ ⌜v = 5⌝, TEnd))=> //;
+        iIntros (c' γ') "[Hstl' Hstr']"=> /=.
+      wp_apply (send_st_spec (A:=val) with "[Hstl Hstr']");
         first by eauto 10 with iFrame.
       iIntros "Hstl".
-      wp_apply (send_st_spec N Z with "[$Hstl' //]");
-      iIntros "Hstl'".
+      wp_apply (send_st_spec (A:=Z) with "[$Hstl' //]"); iIntros "Hstl'".
       eauto.
-    - wp_apply (recv_st_spec N val with "Hstr");
-      iIntros (v) "[Hstr Hstr']".
+    - wp_apply (recv_st_spec (A:=val) with "Hstr"); iIntros (v) "[Hstr Hstr']".
       iDestruct "Hstr'" as (γ') "Hstr'".
-      wp_apply (recv_st_spec N Z with "Hstr'");
-      iIntros (v') "[Hstr' HP]".
-      iDestruct "HP" as %<-.
+      wp_apply (recv_st_spec (A:=Z) with "Hstr'"); iIntros (v') "[Hstr' <-]".
       by iApply "HΦ".
   Qed.
 
   Lemma bad_seq_proof :
     {{{ True }}} bad_seq_example {{{ v, RET v; ⌜v = #5⌝ }}}.
   Proof.
-    iIntros (Φ H) "HΦ".
+    iIntros (Φ _) "HΦ".
     rewrite /bad_seq_example.
-    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
+    wp_apply (new_chan_st_spec nroot (<!> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
-    wp_apply (recv_st_spec N Z with "Hstr");
-    iIntros (v) "[Hstr HP]".
-    wp_apply (send_st_spec N Z with "[$Hstl //]");
-    iIntros "Hstl".
-    iDestruct "HP" as %->.
+    wp_apply (recv_st_spec (A:=Z) with "Hstr"); iIntros (v) "[Hstr ->]".
+    wp_apply (send_st_spec (A:=Z) with "[$Hstl //]"); iIntros "Hstl".
     wp_pures.
     by iApply "HΦ".
   Qed.
@@ -121,36 +141,30 @@ Section ExampleProofsEnc.
   Lemma bad_par_proof :
     {{{ True }}} bad_par_example {{{ v, RET v; ⌜v = #5⌝ }}}.
   Proof.
-    iIntros (Φ H) "HΦ".
+    iIntros (Φ _) "HΦ".
     rewrite /bad_par_example.
-    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
+    wp_apply (new_chan_st_spec nroot (<!> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext. by wp_finish.
-    - wp_apply (recv_st_spec _ with "Hstr");
-      iIntros (v) "[Hstr HP]".
-      iDestruct "HP" as %->.
+    - wp_apply (recv_st_spec (A:=Z) with "Hstr"); iIntros (v) "[Hstr ->]".
       by iApply "HΦ".
   Qed.
 
   Lemma bad_interleave_proof :
     {{{ True }}} bad_interleave_example {{{ v, RET v; ⌜v = #()⌝ }}}.
   Proof.
-    iIntros (Φ H) "HΦ".
+    iIntros (Φ _) "HΦ".
     rewrite /bad_interleave_example.
-    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
+    wp_apply (new_chan_st_spec nroot (<!> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
-    wp_apply (new_chan_st_spec N (<?> v @ ⌜v = 5⌝, TEnd))=> //;
+    wp_apply (new_chan_st_spec nroot (<?> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c' γ') "[Hstl' Hstr']"=> /=.
     wp_apply (wp_fork with "[Hstr Hstr']").
-    - iNext. wp_apply (recv_st_spec _ with "Hstr");
-      iIntros (v) "[Hstr HP]".
-      wp_apply (send_st_spec _ Z with "[$Hstr' //]"). eauto.
-    - wp_apply (recv_st_spec _ Z with "[$Hstl' //]");
-      iIntros (v) "[Hstl' HP]".
-      wp_apply (send_st_spec _ Z with "[$Hstl //]");
-      iIntros "Hstl".
+    - iNext. wp_apply (recv_st_spec (A:=Z) with "Hstr"); iIntros (v) "[Hstr HP]".
+      wp_apply (send_st_spec (A:=Z) with "[$Hstr' //]"). eauto.
+    - wp_apply (recv_st_spec (A:=Z) with "[$Hstl' //]"); iIntros (v) "[Hstl' HP]".
+      wp_apply (send_st_spec (A:=Z) with "[$Hstl //]"); iIntros "Hstl".
       by iApply "HΦ".
   Qed.
-
-End ExampleProofsEnc.
\ No newline at end of file
+End ExampleProofsEnc.
diff --git a/theories/proto/branching.v b/theories/proto/branching.v
index 4380bcad7de12be56ab75c0615a45ee4dc0042e3..57a88d96b8a48282de408f370d95a6d637aa7395 100644
--- a/theories/proto/branching.v
+++ b/theories/proto/branching.v
@@ -1,57 +1,52 @@
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import list auth excl.
-From iris.base_logic Require Import invariants.
 From osiris.proto Require Export proto_enc.
 
-Section DualBranch.
-  Context `{PROP : bi}.
-
-  Definition TSB (a : action)
-             (prot1 prot2 : proto val PROP) : proto val PROP :=
-    TSR' a (λ _, True)%I (λ v, if v : bool then prot1 else prot2).
-
-  Global Instance is_dual_tsb a1 a2 proto1 proto1' proto2 proto2' :
-    IsDualAction a1 a2 →
-    IsDualProto proto1 proto1' → IsDualProto proto2 proto2' →
-    IsDualProto (TSB a1 proto1 proto2) (TSB a2 proto1' proto2').
-  Proof.
-    rewrite /IsDualAction.
-    rewrite /IsDualProto.
-    intros Ha Hst1 Hst2.
-    destruct a1.
-    - simpl.
-      simpl in Ha. rewrite -Ha.
-      rewrite -(proto_force_eq (dual_proto _)).
-      constructor.
-      f_equiv.
-      f_equiv.
-      destruct (decode a).
-      by destruct b. apply is_dual_end.
-    - simpl.
-      simpl in Ha. rewrite -Ha.
-      rewrite -(proto_force_eq (dual_proto _)).
-      constructor.
-      f_equiv.
-      f_equiv.
-      destruct (decode a).
-      by destruct b.
-      apply is_dual_end.
-  Qed.
-End DualBranch.
+Definition TSB {PROP : bi} (a : action)
+    (prot1 prot2 : proto val PROP) : proto val PROP :=
+  TSR' a (λ _, True)%I (λ v, if v : bool then prot1 else prot2).
 Global Typeclasses Opaque TSB.
-
 Infix "<+>" := (TSB Send) (at level 85) : proto_scope.
 Infix "<&>" := (TSB Receive) (at level 85) : proto_scope.
 
-Section branching_specs.
-  Context `{!heapG Σ} (N : namespace).
-  Context `{!logrelG val Σ}.
+Definition select : val := λ: "c" "s" "b", send "c" "s" "b".
+Definition branch : val := λ: "c" "s" "b1" "b2",
+  if: recv "c" "s" then "b1" else "b2".
+(* TODO: This notation should be fixed *)
+Notation "'branch:' c @ s 'left' e1 'right' e2" :=
+  (branch c s (λ: <>, e1)%E (λ: <>, e2)%E #())
+    (at level 200, c, s, e1, e2 at level 200) : expr_scope.
 
-  Definition select : val :=
-    λ: "c" "s" "b",
-      send "c" "s" "b".
+Global Instance is_dual_tsb {PROP : bi} a1 a2
+    (proto1 proto1' proto2 proto2' : proto val PROP) :
+  IsDualAction a1 a2 →
+  IsDualProto proto1 proto1' → IsDualProto proto2 proto2' →
+  IsDualProto (TSB a1 proto1 proto2) (TSB a2 proto1' proto2').
+Proof.
+  rewrite /IsDualAction.
+  rewrite /IsDualProto.
+  intros Ha Hst1 Hst2.
+  destruct a1.
+  - simpl.
+    simpl in Ha. rewrite -Ha.
+    rewrite -(proto_force_eq (dual_proto _)).
+    constructor.
+    f_equiv.
+    f_equiv.
+    destruct (val_decode a).
+    by destruct b. apply is_dual_end.
+  - simpl.
+    simpl in Ha. rewrite -Ha.
+    rewrite -(proto_force_eq (dual_proto _)).
+    constructor.
+    f_equiv.
+    f_equiv.
+    destruct (val_decode a).
+    by destruct b.
+    apply is_dual_end.
+Qed.
+
+Section branching_specs.
+  Context `{!heapG Σ, !logrelG val Σ} (N : namespace).
 
   Lemma select_st_spec proto1 proto2 γ c s (b : side) :
     {{{ ⟦ c @ s : proto1 <+> proto2 ⟧{N,γ} }}}
@@ -61,17 +56,9 @@ Section branching_specs.
     iIntros (Φ) "Hproto HΦ".
     wp_pures. wp_lam.
     wp_pures. rewrite /TSB.
-    wp_apply (send_st_spec N bool with "[$Hproto //]");
-    iIntros "Hstl".
-    iApply "HΦ".
-    by destruct b.
+    wp_apply (send_st_spec (A:=bool) with "[$Hproto //]"); iIntros "Hstl".
+    iApply "HΦ". by destruct b.
   Qed.
-  
-  Definition branch : val :=
-    λ: "c" "s" "b1" "b2",
-      if: recv "c" "s"
-       then "b1"
-       else "b2".
 
   Lemma branch_st_spec proto1 proto2 γ c s (b1 b2 : val) :
     {{{ ⟦ c @ s : proto1 <&> proto2 ⟧{N,γ} }}}
@@ -83,15 +70,9 @@ Section branching_specs.
     iIntros "Hproto HΦ'".
     wp_pures.
     wp_lam. rewrite /TSB. simpl.
-    wp_apply (recv_st_spec N bool with "[$Hproto //]").
-    iIntros (v) "[Hstl _]".
-    destruct v.
+    wp_apply (recv_st_spec (A:=bool) with "[$Hproto //]").
+    iIntros ([]) "[Hstl _]".
     - wp_pures. iApply ("HΦ'"). eauto with iFrame.
     - wp_pures. iApply ("HΦ'"). eauto with iFrame.
   Qed.
-
 End branching_specs.
-
-Notation "'branch:' c @ s 'left' e1 'right' e2" :=
-  (branch c s (λ: <>, e1)%E (λ: <>, e2)%E #())
-    (at level 200, c, s, e1, e2 at level 200) : expr_scope.
diff --git a/theories/proto/channel.v b/theories/proto/channel.v
index 146b46850ed206f47a25fbdea343136212b7836b..83bc2132c62e36acdd8c60b4abfc447062b9af57 100644
--- a/theories/proto/channel.v
+++ b/theories/proto/channel.v
@@ -1,15 +1,10 @@
-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl auth list.
-From iris.base_logic.lib Require Import auth.
 From iris.heap_lang.lib Require Import spin_lock.
-From osiris.base_logic Require Import auth_excl.
+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.
 Set Default Proof Using "Type".
-Import uPred.
 
 Definition new_chan : val :=
   λ: <>,
@@ -71,7 +66,7 @@ Section channel.
   Context `{!heapG Σ, !chanG Σ} (N : namespace).
 
   Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
-    (∃ l':loc, ⌜l = #l'⌝ ∧ l' ↦ encode xs)%I.
+    (∃ l' : loc, ⌜l = #l'⌝ ∧ l' ↦ val_encode xs)%I.
 
   Record chan_name := Chan_name {
     chan_lock_name : gname;
@@ -167,7 +162,7 @@ Section channel.
         (vs ws) "(Href & Hvs & Href' & Hws)".
     iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
     wp_load. 
-    wp_apply (lsnoc_spec (T:=val))=> //; iIntros (_).
+    wp_apply (lsnoc_spec (A:=val))=> //; iIntros (_).
     wp_bind (_ <- _)%E.
     iMod "HΦ" as (vs') "[Hchan HΦ]".
     iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
diff --git a/theories/proto/encodable.v b/theories/proto/encodable.v
index bebe9fd32a1361cc324338b3cf11f77c675e3cb5..d8528c1cab17b524396fa3cd0719ac9d39f015a7 100644
--- a/theories/proto/encodable.v
+++ b/theories/proto/encodable.v
@@ -1,151 +1,87 @@
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export notation.
 
-Class Encodable A := encode : A -> val.
-Class Decodable A := decode : val -> option A.
-Class EncDec (A : Type) {EA : Encodable A} {DA : Decodable A} :=
-{
-  encdec : ∀ v, decode (encode v) = Some v;
-  decenc : ∀ (v : val) (w : A) , decode v = Some w -> encode w = v
+Class ValEnc A := val_encode : A → val.
+Class ValDec A := val_decode : val → option A.
+Class ValEncDec A `{!ValEnc A, !ValDec A} := {
+  val_encode_decode v : val_decode (val_encode v) = Some v;
+  val_decode_encode v x : val_decode v = Some x → val_encode x = v;
 }.
 
-Ltac solve_encdec := intros v; by unfold decode, encode.
-Ltac solve_decenc :=
-  intros ?v ?w ?H;
-  destruct v as [?l | | | | ]; try by inversion H;
-  destruct l; try by inversion H.
-Ltac solve_encdec_decenc :=
-  split; [solve_encdec | solve_decenc].
+Local Arguments val_encode _ _ !_ /.
+Local Arguments val_decode _ _ !_ /.
 
-(* Instances *)
-Instance val_encodable : Encodable val := id.
-Instance val_decodable : Decodable val := id $ Some.
-Instance val_encdec : EncDec val.
+Lemma val_encode_decode_iff `{ValEncDec A} v x :
+  val_encode x = v ↔ val_decode v = Some x.
 Proof.
-  split.
-  - intros v. unfold decode, encode. eauto.
-  - intros v w H. by destruct v; inversion H.
+  split; last apply val_decode_encode. intros <-. by rewrite -val_encode_decode.
+Qed.
+Instance val_encode_inj `{ValEncDec A} : Inj (=) (=) val_encode.
+Proof.
+  intros x y Heq. apply (inj Some).
+  by rewrite -(val_encode_decode x) Heq val_encode_decode.
 Qed.
 
-Instance int_encodable : Encodable Z := λ n, #n.
-Instance int_decodable : Decodable Z :=
-  λ v, match v with
-       | LitV (LitInt z) => Some z
-       | _ => None
-       end.
-Instance int_encdec : EncDec Z.
-Proof. solve_encdec_decenc. Qed.
+(* Instances *)
+Instance val_val_enc : ValEnc val := id.
+Instance val_val_dec : ValDec val := id $ Some.
+Instance val_val_enc_dec : ValEncDec val.
+Proof. split. done. by intros ?? [= ->]. Qed.
 
-Instance bool_encodable : Encodable bool := λ b, #b.
-Instance bool_decodable : Decodable bool :=
-  λ v, match v with
-       | LitV (LitBool b) => Some b
-       | _ => None
-       end.
-Instance bool_encdec : EncDec bool.
-Proof. solve_encdec_decenc. Qed.
+Instance int_val_enc : ValEnc Z := λ n, #n.
+Instance int_val_dec : ValDec Z := λ v,
+  match v with LitV (LitInt z) => Some z | _ => None end.
+Instance int_val_enc_dec : ValEncDec Z.
+Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
 
-Instance loc_encodable : Encodable loc := λ l, #l.
-Instance loc_decodable : Decodable loc :=
-  λ v, match v with
-       | LitV (LitLoc l) => Some l
-       | _ => None
-       end.
-Instance loc_encdec : EncDec loc.
-Proof. solve_encdec_decenc. Qed.
+Instance bool_val_enc : ValEnc bool := λ b, #b.
+Instance bool_val_dec : ValDec bool := λ v,
+  match v with LitV (LitBool b) => Some b | _ => None end.
+Instance bool_val_enc_dec : ValEncDec bool.
+Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
 
-Instance unit_encodable : Encodable unit := λ _, #().
-Instance unit_decodable : Decodable unit :=
-  λ v, match v with
-       | LitV (LitUnit) => Some ()
-       | _ => None
-       end.
-Instance unit_encdec : EncDec unit.
-Proof.
-  split.
-  - intros v. destruct v. by unfold decode, encode.
-  - solve_decenc.
-Qed.
+Instance loc_val_enc : ValEnc loc := λ l, #l.
+Instance loc_val_dec : ValDec loc := λ v,
+  match v with LitV (LitLoc l) => Some l | _ => None end.
+Instance loc_val_enc_dec : ValEncDec loc.
+Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
 
-Instance pair_encodable `{Encodable A, Encodable B} : Encodable (A * B) :=
-  λ p, (encode p.1, encode p.2)%V.
-Instance pair_decodable `{Decodable A, Decodable B} : Decodable (A * B) :=
-  λ v, match v with
-       | PairV v1 v2 => match decode v1, decode v2 with
-                        | Some v1, Some v2 => Some (v1, v2)
-                        | _, _ => None
-                        end
-       | _ => None
-       end.
-Instance pair_encdec `{EncDec A, EncDec B} : EncDec (A * B).
-Proof.
-  split.
-  - intros v. destruct v. unfold decode, encode. simpl.
-    rewrite encdec. rewrite encdec. reflexivity.
-  - intros v w Heq. destruct w.
-    unfold decode, encode in *.
-    unfold pair_encodable, pair_decodable in *. simpl.
-    destruct v; inversion Heq.
-    by f_equiv;
-    apply decenc;
-    destruct (decode v1); inversion Heq;
-    destruct (decode v2); inversion Heq.
-Qed.
+Instance unit_val_enc : ValEnc unit := λ _, #().
+Instance unit_val_dec : ValDec unit := λ v,
+  match v with LitV LitUnit => Some () | _ => None end.
+Instance unit_val_enc_dec : ValEncDec unit.
+Proof. split. by intros []. by intros [[]| | | |] ? [= <-]. Qed.
 
-Instance option_encodable `{Encodable A} : Encodable (option A) := λ mx,
-  match mx with Some x => SOMEV (encode x) | None => NONEV end%V.
-Instance option_decodable `{Decodable A} : Decodable (option A) :=
-  λ v, match v with
-       | SOMEV v => match decode v with
-                    | Some v => Some (Some v)
-                    | None => None
-                    end
-       | NONEV => Some (None)
-       | _ => None
-       end.
-Instance option_encdec `{EncDec A} : EncDec (option A).
+Instance pair_val_enc `{ValEnc A, ValEnc B} : ValEnc (A * B) := λ p,
+  (val_encode p.1, val_encode p.2)%V.
+Instance pair_val_dec `{ValDec A, ValDec B} : ValDec (A * B) := λ v,
+  match v with
+  | PairV v1 v2 => x1 ← val_decode v1; x2 ← val_decode v2; Some (x1, x2)
+  | _ => None
+  end.
+Instance pair_val_enc_dec `{ValEncDec A, ValEncDec B} : ValEncDec (A * B).
 Proof.
   split.
-  - intros v. unfold decode, encode.
-    destruct v; simpl. rewrite encdec. eauto. eauto.
-  - intros v w Heq.
-    destruct w.
-    + unfold decode, encode in *.
-      unfold option_encodable, option_decodable in *.
-      destruct v; inversion Heq.
-      destruct v; inversion Heq.
-      destruct l; inversion Heq.
-      f_equiv.
-      apply decenc.
-        by destruct (decode v); inversion Heq.
-    + unfold decode, encode in *.
-      simpl.
-      unfold option_encodable, option_decodable in *.
-      destruct v; inversion Heq.
-      * destruct v; inversion Heq.
-        destruct l; inversion Heq.
-        eauto.
-      * destruct (decode v); inversion Heq.
+  - intros []. by rewrite /= val_encode_decode /= val_encode_decode.
+  - intros [] ??; simplify_option_eq;
+      by repeat match goal with
+      | H : val_decode _ = Some _ |- _ => apply val_decode_encode in H as <-
+      end.
 Qed.
 
-Lemma enc_dec {A : Type} `{ED : EncDec A}
-      v (w : A) : encode w = v <-> decode v = Some w.
+Instance option_val_enc `{ValEnc A} : ValEnc (option A) := λ mx,
+  match mx with Some x => SOMEV (val_encode x) | None => NONEV end%V.
+Instance option_val_dec `{ValDec A} : ValDec (option A) := λ v,
+  match v with
+  | SOMEV v => x ← val_decode v; Some (Some x)
+  | NONEV => Some None
+  | _ => None
+  end.
+Instance option_val_enc_dec `{ValEncDec A} : ValEncDec (option A).
 Proof.
   split.
-  - intros.
-    rewrite -encdec.
-    rewrite -H.
-    reflexivity.
-  - intros.
-    apply decenc. eauto.
+  - intros []=> //. by rewrite /= val_encode_decode.
+  - intros [] ??; repeat (simplify_option_eq || case_match);
+      by repeat match goal with
+      | H : val_decode _ = Some _ |- _ => apply val_decode_encode in H as <-
+      end.
 Qed.
-
-Lemma enc_inj {A : Type} `{ED : EncDec A}
-      x y : encode x = encode y -> x = y.
-Proof.
-  intros Heq.
-  assert (decode (encode x) = decode (encode y)).
-  { by f_equiv. }
-  erewrite encdec in H=> //.
-  erewrite encdec in H=> //.
-  by inversion H.
-Qed.
\ No newline at end of file
diff --git a/theories/proto/list.v b/theories/proto/list.v
index 92a87d8a830b18bf04757331cd575e84cfda5acc..2764ce3d76225c212af1058e7b113fd7a6135491 100644
--- a/theories/proto/list.v
+++ b/theories/proto/list.v
@@ -3,12 +3,12 @@ From iris.heap_lang Require Import assert.
 From osiris Require Export encodable.
 
 (** Immutable ML-style functional lists *)
-Instance list_encodable `{Encodable A} : Encodable (list A) :=
+Instance list_val_enc `{ValEnc A} : ValEnc (list A) :=
   fix go xs :=
-  let _ : Encodable _ := @go in
+  let _ : ValEnc _ := @go in
   match xs with
-  | [] => encode None
-  | x :: xs => encode (Some (x,xs))
+  | [] => val_encode None
+  | x :: xs => val_encode (Some (x,xs))
   end.
 
 Definition lnil : val := λ: <>, NONEV.
@@ -91,35 +91,34 @@ Definition lsplit : val :=
   λ: "l", lsplit_at "l" ((llength "l") `quot` #2).
 
 Section lists.
-Context `{heapG Σ}.
+Context `{heapG Σ} `{ValEncDec A}.
 Implicit Types i : nat.
-Context `{EncDec T}.
-Implicit Types x : T.
-Implicit Types xs : list T.
+Implicit Types x : A.
+Implicit Types xs : list A.
 
 Lemma lnil_spec :
-  {{{ True }}} lnil #() {{{ RET encode []; True }}}.
+  {{{ True }}} lnil #() {{{ RET val_encode []; True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
 
 Lemma lcons_spec x xs :
   {{{ True }}}
-    lcons (encode x) (encode xs)
-  {{{ RET (encode (x :: xs)); True }}}.
+    lcons (val_encode x) (val_encode xs)
+  {{{ RET val_encode (x :: xs); True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
 
 Lemma lhead_spec x xs:
-  {{{ True }}} lhead (encode (x::xs)) {{{ RET encode x; True }}}.
+  {{{ True }}} lhead (val_encode (x::xs)) {{{ RET val_encode x; True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
 
 Lemma ltail_spec x xs :
-  {{{ True }}} ltail (encode (x::xs)) {{{ RET encode xs; True }}}.
+  {{{ True }}} ltail (val_encode (x::xs)) {{{ RET val_encode xs; True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
 
 Lemma llookup_spec i xs x:
   xs !! i = Some x →
   {{{ True }}}
-    llookup #i (encode xs)
-  {{{ RET encode x; True }}}.
+    llookup #i (val_encode xs)
+  {{{ RET val_encode x; True }}}.
 Proof.
   iIntros (Hi Φ Hl) "HΦ".
   iInduction xs as [|x' xs] "IH" forall (i Hi Hl);
@@ -133,8 +132,8 @@ Qed.
 Lemma linsert_spec i xs x :
   is_Some (xs !! i) →
   {{{ True }}}
-    linsert #i (encode x) (encode xs)
-  {{{ RET encode (<[i:=x]>xs); True }}}.
+    linsert #i (val_encode x) (val_encode xs)
+  {{{ RET val_encode (<[i:=x]>xs); True }}}.
 Proof.
   iIntros ([w Hi] Φ Hl) "HΦ".
   iInduction xs as [|x' xs] "IH" forall (i Hi Hl Φ);
@@ -149,18 +148,17 @@ Proof.
   by wp_apply (lcons_spec with "[//]").
 Qed.
 
-Lemma llist_member_spec `{EqDecision T} (xs : list T) (x : T) :
+Lemma llist_member_spec `{EqDecision A} (xs : list A) (x : A) :
   {{{ True }}}
-    llist_member (encode x) (encode xs)
+    llist_member (val_encode x) (val_encode xs)
   {{{ RET #(bool_decide (x ∈ xs)); True }}}.
 Proof.
   iIntros (Φ Hl) "HΦ".
   iInduction xs as [|x' xs] "IH" forall (Hl); simplify_eq/=.
   { wp_lam; wp_pures. by iApply "HΦ". }
   wp_lam; wp_pures.
-  destruct (bool_decide_reflect (encode x' = encode x)) as [Heq|?]; wp_if.
-  { apply enc_inj in Heq. rewrite Heq.
-    rewrite (bool_decide_true (_ ∈ _ :: _)). by iApply "HΦ". by left. }
+  destruct (bool_decide_reflect (val_encode x' = val_encode x)); simplify_eq/=; wp_if.
+  { rewrite (bool_decide_true (_ ∈ _ :: _)); last by left. by iApply "HΦ". }
   wp_proj. wp_let. iApply ("IH" with "[//]").
   destruct (bool_decide_reflect (x ∈ xs)).
   - by rewrite bool_decide_true; last by right.
@@ -169,8 +167,8 @@ Qed.
 
 Lemma lreplicate_spec i x :
   {{{ True }}}
-    lreplicate #i (encode x)
-  {{{ RET encode (replicate i x); True }}}.
+    lreplicate #i (val_encode x)
+  {{{ RET val_encode (replicate i x); True }}}.
 Proof.
   iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
   { wp_lam; wp_pures.
@@ -181,20 +179,20 @@ Proof.
 Qed.
 
 Lemma llength_spec xs :
-  {{{ True }}} llength (encode xs) {{{ RET #(length xs); True }}}.
+  {{{ True }}} llength (val_encode xs) {{{ RET #(length xs); True }}}.
 Proof.
   iIntros (Φ Hl) "HΦ".
   iInduction xs as [|x' xs] "IH" forall (Hl Φ); simplify_eq/=.
   { wp_lam. wp_match. by iApply "HΦ". }
-wp_lam. wp_match. wp_proj.
+  wp_lam. wp_match. wp_proj.
   wp_apply ("IH" with "[//]"); iIntros "_ /=". wp_op.
   rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
 Qed.
 
 Lemma lsnoc_spec xs x :
   {{{ True }}}
-    lsnoc (encode xs) (encode x)
-  {{{ RET (encode (xs++[x])); True }}}.
+    lsnoc (val_encode xs) (val_encode x)
+  {{{ RET (val_encode (xs++[x])); True }}}.
 Proof.
   iIntros (Φ _) "HΦ".
   iInduction xs as [|x' xs] "IH" forall (Φ).
@@ -206,8 +204,8 @@ Qed.
 
 Lemma ltake_spec xs (n:Z) :
   {{{ True }}}
-    ltake (encode xs) #n
-  {{{ RET encode (take (Z.to_nat n) xs); True }}}.
+    ltake (val_encode xs) #n
+  {{{ RET val_encode (take (Z.to_nat n) xs); True }}}.
 Proof.
   iIntros (Φ _) "HΦ".
   iInduction xs as [|x' xs] "IH" forall (n Φ).
@@ -227,14 +225,10 @@ Proof.
       by iApply "HΦ".
 Qed.
 
-Lemma drop_cons x xs n :
-  drop (S n) (x::xs) = drop n xs.
-Proof. by destruct xs. Qed.
-
 Lemma ldrop_spec xs (n:Z) :
   {{{ True }}}
-    ldrop (encode xs) #n
-  {{{ RET encode (drop (Z.to_nat n) xs); True }}}.
+    ldrop (val_encode xs) #n
+  {{{ RET val_encode (drop (Z.to_nat n) xs); True }}}.
 Proof.
   iIntros (Φ _) "HΦ".
   iInduction xs as [|x' xs] "IH" forall (n Φ).
@@ -247,19 +241,16 @@ Proof.
       rewrite Z_to_nat_nonpos=> //. rewrite drop_0.
       by iApply "HΦ".
     + rewrite bool_decide_false=> //.
-      wp_apply ("IH").
-      rewrite -(drop_cons x' xs (Z.to_nat (n - 1))).
-      rewrite -Z2Nat.inj_succ; last lia.
-      rewrite Z.succ_pred.
-      iIntros (_).
+      wp_apply "IH"; iIntros (_).
+      rewrite -{1}(Z.succ_pred n) Z2Nat.inj_succ /= -Z.sub_1_r; last lia.
       by iApply "HΦ".
 Qed.
 
 Lemma lsplit_at_spec xs n :
   {{{ True }}}
-    lsplit_at (encode (xs)) #n
-  {{{ RET encode (encode (take (Z.to_nat n) xs),
-          encode (drop (Z.to_nat n) xs)); True }}}.
+    lsplit_at (val_encode (xs)) #n
+  {{{ RET val_encode (val_encode (take (Z.to_nat n) xs),
+          val_encode (drop (Z.to_nat n) xs)); True }}}.
 Proof.
   iIntros (Φ _) "HΦ".
   wp_lam.
@@ -269,28 +260,18 @@ Proof.
   by iApply "HΦ".
 Qed.
 
-Lemma take_drop xs n :
-  take n xs ++ drop n xs = xs.
-Proof.
-  revert n.
-  induction xs; intros n.
-  - by destruct n.
-  - destruct n=> //.
-    simpl. f_equiv. apply IHxs.
-Qed.
-
 Lemma lsplit_spec xs :
-  {{{ True }}} lsplit (encode xs) {{{ ys zs, RET (encode ys, encode zs);
-                                           ⌜ys++zs = xs⌝ }}}.
+  {{{ True }}}
+    lsplit (val_encode xs)
+  {{{ ys zs, RET (val_encode ys, val_encode zs); ⌜ ys++zs = xs ⌝ }}}.
 Proof.
   iIntros (Φ _) "HΦ".
   wp_lam.
   wp_apply (llength_spec)=>//; iIntros (_).
   wp_apply (lsplit_at_spec)=>//; iIntros (_).
   wp_pures.
-  iApply ("HΦ").
+  iApply "HΦ".
   iPureIntro.
   apply take_drop.
 Qed.
-
-End lists.
\ No newline at end of file
+End lists.
diff --git a/theories/proto/proto_def.v b/theories/proto/proto_def.v
index 17a5e6ff350ba41fef0e6445c179119bd0d269d0..3d33e67e975659185de541113c2c36a716923d6c 100644
--- a/theories/proto/proto_def.v
+++ b/theories/proto/proto_def.v
@@ -1,10 +1,6 @@
-From iris.heap_lang Require Export lang.
-From iris.algebra Require Export cmra.
-From stdpp Require Export list.
 From iris.base_logic Require Import base_logic.
-From iris.algebra Require Import updates local_updates.
-From iris.heap_lang Require Import proofmode notation.
 From osiris.proto Require Import involutive.
+From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Inductive action := Send | Receive.
diff --git a/theories/proto/proto_enc.v b/theories/proto/proto_enc.v
index 2989bb19d15acfc85bba0aaceb150f0917020be3..2ef46d56d9d0a4873df142323c1be00c2face169 100644
--- a/theories/proto/proto_enc.v
+++ b/theories/proto/proto_enc.v
@@ -1,18 +1,14 @@
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import list auth excl.
-From iris.base_logic Require Import invariants.
 From osiris.proto Require Export encodable proto_specs.
 
 Section DualProtoEnc.
-  Context `{EncDec V} `{PROP: bi} .
+  Context `{ValEncDec V} {PROP: bi} .
 
   Definition TSR'
-    (a : action) (P : V → PROP) (prot : V → proto val PROP) : proto val PROP :=
-  TSR a
-    (λ v, if decode v is Some x then P x else False)%I
-    (λ v, if decode v is Some x then prot x else TEnd (* dummy *)).
+      (a : action) (P : V → PROP) (prot : V → proto val PROP) : proto val PROP :=
+    TSR a
+      (λ v, if val_decode v is Some x then P 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 P (st1 st2 : V → proto val PROP) :
@@ -22,10 +18,9 @@ Section DualProtoEnc.
   Proof.
     rewrite /IsDualAction /IsDualProto. intros <- Hst.
     rewrite -(proto_force_eq (dual_proto _)).
-    constructor=> x. done. destruct (decode x)=> //.
+    constructor=> x. done. destruct (val_decode x)=> //.
     apply is_dual_end.
   Qed.
-
 End DualProtoEnc.
 
 Notation "<!> x @ P , prot" :=
@@ -44,46 +39,35 @@ Notation "<?> @ P , prot" := (<?> dummy__ @ P dummy__, prot dummy__)%proto
   (at level 200, prot at level 200) : proto_scope.
 
 Section proto_enc_specs.
-  Context `{!heapG Σ} (N : namespace).
-  Context `{!logrelG val Σ}.
+  Context `{!heapG Σ, !logrelG val Σ} `{ValEncDec A} (N : namespace).
 
-  Lemma send_st_spec (A : Type) `{EncDec A}
-        prot γ c s (P : A → iProp Σ) w :
+  Lemma send_st_spec prot γ c s (P : A → iProp Σ) w :
     {{{ P w ∗ ⟦ c @ s : <!> @ P, prot ⟧{N,γ} }}}
-      send c #s (encode w)
+      send c #s (val_encode w)
     {{{ RET #(); ⟦ c @ s : prot w ⟧{N,γ} }}}.
   Proof.
     iIntros (Φ) "[HP Hsend] HΦ".
-    iApply (send_st_spec with "[HP Hsend]").
-    simpl.
-    iFrame.
-    by rewrite encdec.
-    iNext.
-    rewrite encdec.
+    iApply (send_st_spec with "[HP $Hsend]").
+    { by rewrite val_encode_decode. }
+    iNext. rewrite val_encode_decode.
     by iApply "HΦ".
   Qed.
 
-  Lemma recv_st_spec (A : Type) `{EncDec A}
-        prot γ c s (P : A → iProp Σ) :
+  Lemma recv_st_spec prot γ c s (P : A → iProp Σ) :
     {{{ ⟦ c @ s : <?> @ P, prot ⟧{N,γ} }}}
       recv c #s
-    {{{ v, RET (encode v); ⟦ c @ s : prot v ⟧{N,γ} ∗ P v }}}.
+    {{{ v, RET (val_encode v); ⟦ c @ s : prot v ⟧{N,γ} ∗ P v }}}.
   Proof.
     iIntros (Φ) "Hrecv HΦ".
     iApply (recv_st_spec with "Hrecv").
     iNext. iIntros (v).
     iIntros "[H HP]".
-    iAssert ((∃ w, ⌜decode v = Some w⌝ ∗ P w)%I) with "[HP]" as (w Hw) "HP".
-    { destruct (decode v).
-      iExists a. by iFrame. iDestruct "HP" as %HP=>//. }
+    iAssert (∃ w, ⌜val_decode v = Some w⌝ ∗ P w)%I with "[HP]" as (w Hw) "HP".
+    { destruct (val_decode v) as [x|]; last done.
+      iExists x. by iFrame. }
     iSpecialize ("HΦ" $!w).
-    apply enc_dec in Hw. rewrite Hw.
-    iApply "HΦ".
-    iFrame.
-    apply enc_dec in Hw.
-    destruct (decode v).
-    - inversion Hw. subst. iApply "H".
-    - inversion Hw.
+    apply val_decode_encode in Hw as <-.
+    iApply "HΦ". iFrame "HP".
+    by rewrite val_encode_decode.
   Qed.
-
-End proto_enc_specs.
\ No newline at end of file
+End proto_enc_specs.
diff --git a/theories/proto/proto_specs.v b/theories/proto/proto_specs.v
index a0a3ea39b7d386cca17c9ec3db0ac437e2ede327..cd99fde41b7e75de3c03f19cdcc09b5abfca604e 100644
--- a/theories/proto/proto_specs.v
+++ b/theories/proto/proto_specs.v
@@ -1,13 +1,9 @@
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
-From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import list auth excl.
-From iris.base_logic Require Import invariants.
-From osiris.base_logic Require Import auth_excl.
 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 Σ;
diff --git a/theories/base_logic/auth_excl.v b/theories/utils/auth_excl.v
similarity index 100%
rename from theories/base_logic/auth_excl.v
rename to theories/utils/auth_excl.v