diff --git a/_CoqProject b/_CoqProject
index 15c320d40b62c44460de97b2402ee17b9132c631..5e5ad4f5c7fe9470ebb6457b38de40e2ad5aacf1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,15 +1,15 @@
 -Q theories osiris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/base_logic/auth_excl.v
-theories/encodings/involutive.v
-theories/encodings/side.v
-theories/encodings/stype_def.v
-theories/encodings/encodable.v
-theories/encodings/list.v
-theories/encodings/channel.v
-theories/encodings/stype.v
-theories/encodings/stype_enc.v
-theories/encodings/branching.v
+theories/proto/encodable.v
+theories/proto/list.v
+theories/proto/channel.v
+theories/proto/involutive.v
+theories/proto/side.v
+theories/proto/stype_def.v
+theories/proto/stype.v
+theories/proto/stype_enc.v
+theories/proto/branching.v
 theories/examples/examples.v
 theories/examples/proofs.v
 theories/examples/proofs_enc.v
diff --git a/theories/examples/branching_examples.v b/theories/examples/branching_examples.v
index 8b7431303224733e3acad7b901bff3fd9c9e64f3..7fbe0c815da30ee5c76d1d33b8ae6b9fff10d700 100644
--- a/theories/examples/branching_examples.v
+++ b/theories/examples/branching_examples.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.encodings Require Import channel branching.
 From iris.base_logic Require Import invariants.
+From osiris.proto Require Import channel branching.
 
 Section BranchingExamples.
   Context `{!heapG Σ} (N : namespace).
diff --git a/theories/examples/branching_proofs.v b/theories/examples/branching_proofs.v
index 5226ad6dba555dd93b1aad0038c151b6517e65a2..16fcaaa0731d9b23114548396e72e7c5d2235455 100644
--- a/theories/examples/branching_proofs.v
+++ b/theories/examples/branching_proofs.v
@@ -2,7 +2,7 @@ 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.encodings Require Import branching.
+From osiris.proto Require Import branching.
 From osiris.examples Require Import branching_examples.
 
 Section BranchingExampleProofs.
diff --git a/theories/examples/examples.v b/theories/examples/examples.v
index b40881be53765f31be873e98871b00936b0e8af3..4b6976d23ec8b1b3fb52eb17bb76cb6171acdf71 100644
--- a/theories/examples/examples.v
+++ b/theories/examples/examples.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.encodings Require Import stype.
 From iris.base_logic Require Import invariants.
+From osiris.proto Require Import stype.
 
 Section Examples.
   Context `{!heapG Σ} (N : namespace).
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index c235b9ab036806ccd6b68a39f7c30e7a85828e6f..9f492865d3b8e5340808c5ac8f33fcd0d6bd842f 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -1,11 +1,11 @@
+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 osiris.encodings Require Import list channel stype_enc.
+From osiris.proto Require Import list channel stype_enc.
 From iris.base_logic Require Import invariants.
-From stdpp Require Import sorting.
-Require Import Coq.Lists.List.
-Require Import Omega.
 
 Section ListSortExample.
   Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
diff --git a/theories/examples/proofs.v b/theories/examples/proofs.v
index 8254e5384473b0ebc8ac06f992e287ef5b70417d..dc679f7b9307b5cc0c04219fe002a3761d9806ca 100644
--- a/theories/examples/proofs.v
+++ b/theories/examples/proofs.v
@@ -2,7 +2,7 @@ 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.encodings Require Import stype.
+From osiris.proto Require Import stype.
 From osiris.examples Require Import examples.
 
 Section ExampleProofs.
diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index 521d2f2dd402cff60a5f909bc1c217805e896e36..186c70668c9cad66b5753b842b13737360d6aeab 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -3,7 +3,7 @@ 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.encodings Require Import stype_enc.
+From osiris.proto Require Import stype_enc.
 From osiris.examples Require Import examples.
 
 Section ExampleProofsEnc.
diff --git a/theories/encodings/branching.v b/theories/proto/branching.v
similarity index 98%
rename from theories/encodings/branching.v
rename to theories/proto/branching.v
index 4bdf43c9aa4bb5f8caeeec8b03393ff4f0211807..7c552dc1ee3a55996da966bf688d2c625a4e9451 100644
--- a/theories/encodings/branching.v
+++ b/theories/proto/branching.v
@@ -3,7 +3,7 @@ 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.encodings Require Export stype_enc.
+From osiris.proto Require Export stype_enc.
 
 Section DualBranch.
   Context `{PROP : bi}.
diff --git a/theories/encodings/channel.v b/theories/proto/channel.v
similarity index 99%
rename from theories/encodings/channel.v
rename to theories/proto/channel.v
index c9feffb00e066a8127a073bf1dbe2919f5e64665..146b46850ed206f47a25fbdea343136212b7836b 100644
--- a/theories/encodings/channel.v
+++ b/theories/proto/channel.v
@@ -6,8 +6,8 @@ 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 osiris.encodings Require Export side.
-From osiris.encodings Require Import list.
+From osiris.proto Require Export side.
+From osiris.proto Require Import list.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/encodings/encodable.v b/theories/proto/encodable.v
similarity index 100%
rename from theories/encodings/encodable.v
rename to theories/proto/encodable.v
diff --git a/theories/proto/involutive.v b/theories/proto/involutive.v
new file mode 100644
index 0000000000000000000000000000000000000000..506925a667451c4ff0989b608046b790c5982681
--- /dev/null
+++ b/theories/proto/involutive.v
@@ -0,0 +1,4 @@
+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/encodings/list.v b/theories/proto/list.v
similarity index 100%
rename from theories/encodings/list.v
rename to theories/proto/list.v
diff --git a/theories/encodings/side.v b/theories/proto/side.v
similarity index 86%
rename from theories/encodings/side.v
rename to theories/proto/side.v
index f58a57b7dc7de2062f07ac76cf66e06a01344b2a..f7e7698b65838a4a6f0fd3587765935eb6c44fa2 100644
--- a/theories/encodings/side.v
+++ b/theories/proto/side.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Import proofmode notation.
-From osiris.encodings Require Export involutive.
+From osiris.proto Require Export involutive.
 
 Inductive side := Left | Right.
 Instance side_inhabited : Inhabited side := populate Left.
diff --git a/theories/encodings/stype.v b/theories/proto/stype.v
similarity index 99%
rename from theories/encodings/stype.v
rename to theories/proto/stype.v
index 6cdfac0a34fc71302fbc0f2158c1130df2af3ad7..48df2098e58b6569117e90533943e8139f32857f 100644
--- a/theories/encodings/stype.v
+++ b/theories/proto/stype.v
@@ -6,8 +6,8 @@ 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.encodings Require Export stype_def.
-From osiris.encodings Require Export channel.
+From osiris.proto Require Export stype_def.
+From osiris.proto Require Export channel.
 
 Class logrelG A Σ := {
   logrelG_channelG :> chanG Σ;
diff --git a/theories/encodings/stype_def.v b/theories/proto/stype_def.v
similarity index 99%
rename from theories/encodings/stype_def.v
rename to theories/proto/stype_def.v
index 3a82661db9160c780acbcb853ab5259316b770d8..156af33f4e6a0bed7af72b46774a449c76c1426c 100644
--- a/theories/encodings/stype_def.v
+++ b/theories/proto/stype_def.v
@@ -4,7 +4,7 @@ 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.encodings Require Import involutive.
+From osiris.proto Require Import involutive.
 Set Default Proof Using "Type".
 
 Inductive action := Send | Receive.
diff --git a/theories/encodings/stype_enc.v b/theories/proto/stype_enc.v
similarity index 98%
rename from theories/encodings/stype_enc.v
rename to theories/proto/stype_enc.v
index 2429c8323e2b2f25d3181ca664f4ebbf862f6485..de6637fec83b1a062ca2f3959366f81fd3f0c9c5 100644
--- a/theories/encodings/stype_enc.v
+++ b/theories/proto/stype_enc.v
@@ -3,7 +3,7 @@ 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.encodings Require Export encodable stype.
+From osiris.proto Require Export encodable stype.
 
 Section DualStypeEnc.
   Context `{EncDec V} `{PROP: bi} .