From 7175500980cf458698f43d1909e8b68b9adfbb03 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 11 Jun 2019 19:51:45 +0200
Subject: [PATCH] Refactoring: Definitions stype -> proto, st -> prot

---
 theories/examples/list_sort.v |   4 +-
 theories/proto/branching.v    |  42 ++---
 theories/proto/proto_def.v    | 318 +++++++++++++++++-----------------
 theories/proto/proto_enc.v    |  62 +++----
 theories/proto/proto_specs.v  | 244 +++++++++++++-------------
 5 files changed, 335 insertions(+), 335 deletions(-)

diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 630702e..150ae91 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -137,7 +137,7 @@ Section ListSortExample.
              lmerge_ref "cmp" "xs" !"ys" !"zs";;
              send "c" #Right "xs".
 
-    Definition sort_protocol xs :=
+    Definition sort_protocol xs : proto val (iProp Σ) :=
       (<?> cmp @ cmp_spec cmp,
        <?> l @ l ↦ encode xs,
        <!> l' @ ⌜l = l'⌝ ∗
@@ -145,7 +145,7 @@ Section ListSortExample.
                     l' ↦ encode ys ∗
                        ⌜Sorted (R) ys⌝ ∗
                        ⌜Permutation ys xs⌝),
-       TEnd)%stype.
+       TEnd).
 
     Lemma list_sort_service_spec γ c xs :
       {{{ ⟦ c @ Right : sort_protocol xs ⟧{N,γ} }}}
diff --git a/theories/proto/branching.v b/theories/proto/branching.v
index b511fa2..4380bca 100644
--- a/theories/proto/branching.v
+++ b/theories/proto/branching.v
@@ -9,21 +9,21 @@ Section DualBranch.
   Context `{PROP : bi}.
 
   Definition TSB (a : action)
-             (st1 st2 : stype val PROP) : stype val PROP :=
-    TSR' a (λ _, True)%I (λ v, if v : bool then st1 else st2).
+             (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 st1 st1' st2 st2' :
+  Global Instance is_dual_tsb a1 a2 proto1 proto1' proto2 proto2' :
     IsDualAction a1 a2 →
-    IsDualStype st1 st1' → IsDualStype st2 st2' →
-    IsDualStype (TSB a1 st1 st2) (TSB a2 st1' st2').
+    IsDualProto proto1 proto1' → IsDualProto proto2 proto2' →
+    IsDualProto (TSB a1 proto1 proto2) (TSB a2 proto1' proto2').
   Proof.
     rewrite /IsDualAction.
-    rewrite /IsDualStype.
+    rewrite /IsDualProto.
     intros Ha Hst1 Hst2.
     destruct a1.
     - simpl.
       simpl in Ha. rewrite -Ha.
-      rewrite -(stype_force_eq (dual_stype _)).
+      rewrite -(proto_force_eq (dual_proto _)).
       constructor.
       f_equiv.
       f_equiv.
@@ -31,7 +31,7 @@ Section DualBranch.
       by destruct b. apply is_dual_end.
     - simpl.
       simpl in Ha. rewrite -Ha.
-      rewrite -(stype_force_eq (dual_stype _)).
+      rewrite -(proto_force_eq (dual_proto _)).
       constructor.
       f_equiv.
       f_equiv.
@@ -42,8 +42,8 @@ Section DualBranch.
 End DualBranch.
 Global Typeclasses Opaque TSB.
 
-Infix "<+>" := (TSB Send) (at level 85) : stype_scope.
-Infix "<&>" := (TSB Receive) (at level 85) : stype_scope.
+Infix "<+>" := (TSB Send) (at level 85) : proto_scope.
+Infix "<&>" := (TSB Receive) (at level 85) : proto_scope.
 
 Section branching_specs.
   Context `{!heapG Σ} (N : namespace).
@@ -53,15 +53,15 @@ Section branching_specs.
     λ: "c" "s" "b",
       send "c" "s" "b".
 
-  Lemma select_st_spec st1 st2 γ c s (b : side) :
-    {{{ ⟦ c @ s : st1 <+> st2 ⟧{N,γ} }}}
+  Lemma select_st_spec proto1 proto2 γ c s (b : side) :
+    {{{ ⟦ c @ s : proto1 <+> proto2 ⟧{N,γ} }}}
       select c #s #b
-    {{{ RET #(); ⟦ c @ s : (if b then st1 else st2) ⟧{N,γ} }}}.
+    {{{ RET #(); ⟦ c @ s : (if b then proto1 else proto2) ⟧{N,γ} }}}.
   Proof.
-    iIntros (Φ) "Hst HΦ".
+    iIntros (Φ) "Hproto HΦ".
     wp_pures. wp_lam.
     wp_pures. rewrite /TSB.
-    wp_apply (send_st_spec N bool with "[$Hst //]");
+    wp_apply (send_st_spec N bool with "[$Hproto //]");
     iIntros "Hstl".
     iApply "HΦ".
     by destruct b.
@@ -73,17 +73,17 @@ Section branching_specs.
        then "b1"
        else "b2".
 
-  Lemma branch_st_spec st1 st2 γ c s (b1 b2 : val) :
-    {{{ ⟦ c @ s : st1 <&> st2 ⟧{N,γ} }}}
+  Lemma branch_st_spec proto1 proto2 γ c s (b1 b2 : val) :
+    {{{ ⟦ c @ s : proto1 <&> proto2 ⟧{N,γ} }}}
       branch c #s b1 b2
-    {{{ v, RET v; (⌜v = b1%V⌝ ∧ ⟦ c @ s : st1 ⟧{N,γ}) ∨
-                  (⌜v = b2%V⌝ ∧ ⟦ c @ s : st2 ⟧{N,γ})}}}.
+    {{{ v, RET v; (⌜v = b1%V⌝ ∧ ⟦ c @ s : proto1 ⟧{N,γ}) ∨
+                  (⌜v = b2%V⌝ ∧ ⟦ c @ s : proto2 ⟧{N,γ})}}}.
   Proof.
     iIntros (Φ').
-    iIntros "Hst HΦ'".
+    iIntros "Hproto HΦ'".
     wp_pures.
     wp_lam. rewrite /TSB. simpl.
-    wp_apply (recv_st_spec N bool with "[$Hst //]").
+    wp_apply (recv_st_spec N bool with "[$Hproto //]").
     iIntros (v) "[Hstl _]".
     destruct v.
     - wp_pures. iApply ("HΦ'"). eauto with iFrame.
diff --git a/theories/proto/proto_def.v b/theories/proto/proto_def.v
index 156af33..72af0d6 100644
--- a/theories/proto/proto_def.v
+++ b/theories/proto/proto_def.v
@@ -14,273 +14,273 @@ Definition dual_action (a : action) : action :=
 Instance dual_action_involutive : Involutive (=) dual_action.
 Proof. by intros []. Qed.
 
-CoInductive stype (V A : Type) :=
+CoInductive proto (V A : Type) :=
   | TEnd
-  | TSR (a : action) (P : V → A) (st : V → stype V A).
+  | TSR (a : action) (P : V → A) (prot : V → proto V A).
 Arguments TEnd {_ _}.
 Arguments TSR {_ _} _ _ _.
 Instance: Params (@TSR) 3.
 
-Instance stype_inhabited V A : Inhabited (stype V A) := populate TEnd.
+Instance stype_inhabited V A : Inhabited (proto V A) := populate TEnd.
 
-CoFixpoint dual_stype {V A} (st : stype V A) : stype V A :=
-  match st with
+CoFixpoint dual_proto {V A} (prot : proto V A) : proto V A :=
+  match prot with
   | TEnd => TEnd
-  | TSR a P st => TSR (dual_action a) P (λ v, dual_stype (st v))
+  | TSR a P prot => TSR (dual_action a) P (λ v, dual_proto (prot v))
   end.
-Instance: Params (@dual_stype) 2.
-
-Delimit Scope stype_scope with stype.
-Bind Scope stype_scope with stype.
-
-Notation "<!> x @ P , st" :=
-  (TSR Send (λ x, P%I) (λ x, st%stype))
-  (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<?> x @ P , st" :=
-  (TSR Receive (λ x, P%I) (λ x, st%stype))
-  (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<!> x , st" := (<!> x @ True, st%stype)%stype
-  (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<?> x , st" := (<?> x @ True, st%stype)%stype
-  (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<!> @ P , st" := (<!> x @ P x, st x)%stype
-  (at level 200, st at level 200) : stype_scope.
-Notation "<?> @ P , st" := (<?> x @ P x, st x)%stype
-  (at level 200, st at level 200) : stype_scope.
-
-Section stype_ofe.
+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 "<!> @ P , prot" := (<!> x @ P x, prot x)%proto
+  (at level 200, prot at level 200) : proto_scope.
+Notation "<?> @ P , prot" := (<?> x @ P x, prot x)%proto
+  (at level 200, prot at level 200) : proto_scope.
+
+Section proto_ofe.
   Context {V : Type}.
   Context {A : ofeT}.
 
-  CoInductive stype_equiv : Equiv (stype V A) :=
+  CoInductive proto_equiv : Equiv (proto V A) :=
     | TEnd_equiv : TEnd ≡ TEnd
-    | TSR_equiv a P1 P2 st1 st2 :
+    | TSR_equiv a P1 P2 prot1 prot2 :
        pointwise_relation V (≡) P1 P2 →
-       pointwise_relation V (≡) st1 st2 →
-       TSR a P1 st1 ≡ TSR a P2 st2.
-  Existing Instance stype_equiv.
+       pointwise_relation V (≡) prot1 prot2 →
+       TSR a P1 prot1 ≡ TSR a P2 prot2.
+  Existing Instance proto_equiv.
 
-  CoInductive stype_dist : Dist (stype V A) :=
+  CoInductive proto_dist : Dist (proto V A) :=
     | TEnd_dist n : TEnd ≡{n}≡ TEnd
-    | TSR_dist_0 a P1 P2 st1 st2 :
+    | TSR_dist_0 a P1 P2 prot1 prot2 :
        pointwise_relation V (dist 0) P1 P2 →
-       TSR a P1 st1 ≡{0}≡ TSR a P2 st2
-    | TSR_dist_S n a P1 P2 st1 st2 :
+       TSR a P1 prot1 ≡{0}≡ TSR a P2 prot2
+    | TSR_dist_S n a P1 P2 prot1 prot2 :
        pointwise_relation V (dist (S n)) P1 P2 →
-       pointwise_relation V (dist n) st1 st2 →
-       TSR a P1 st1 ≡{S n}≡ TSR a P2 st2.
-  Existing Instance stype_dist.
+       pointwise_relation V (dist n) prot1 prot2 →
+       TSR a P1 prot1 ≡{S n}≡ TSR a P2 prot2.
+  Existing Instance proto_dist.
 
-  Lemma TSR_dist n a P1 P2 st1 st2 :
+  Lemma TSR_dist n a P1 P2 prot1 prot2 :
     pointwise_relation V (dist n) P1 P2 →
-    pointwise_relation V (dist_later n) st1 st2 →
-    TSR a P1 st1 ≡{n}≡ TSR a P2 st2.
+    pointwise_relation V (dist_later n) prot1 prot2 →
+    TSR a P1 prot1 ≡{n}≡ TSR a P2 prot2.
   Proof. destruct n; by constructor. Defined.
 
-  Definition stype_ofe_mixin : OfeMixin (stype V A).
+  Definition proto_ofe_mixin : OfeMixin (proto V A).
   Proof.
     split.
-    - intros st1 st2. split.
-      + revert st1 st2. cofix IH; destruct 1 as [|a P1 P2 st1' st2' HP]=> n.
+    - intros prot1 prot2. split.
+      + revert prot1 prot2. cofix IH; destruct 1 as [|a P1 P2 prot1' prot2' HP]=> n.
         { constructor. }
         destruct n as [|n].
         * constructor=> v. apply equiv_dist, HP.
         * constructor=> v. apply equiv_dist, HP. by apply IH.
-      + revert st1 st2. cofix IH=> -[|a1 P1 st1] -[|a2 P2 st2] Hst;
-          feed inversion (Hst O); subst; constructor=> v.
-        * apply equiv_dist=> n. feed inversion (Hst n); auto.
-        * apply IH=> n. feed inversion (Hst (S n)); auto.
+      + revert prot1 prot2. cofix IH=> -[|a1 P1 prot1] -[|a2 P2 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 P st]; constructor=> v; auto.
+      + revert n. cofix IH=> -[|n] [|a P 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 stypeC : ofeT := OfeT (stype V A) stype_ofe_mixin.
+  Canonical Structure protoC : ofeT := OfeT (proto V A) proto_ofe_mixin.
 
-  Definition stype_head (d : V -c> A) (st : stype V A) : V -c> A :=
-    match st with TEnd => d | TSR a P st => P end.
-  Definition stype_tail (v : V) (st : stypeC) : later stypeC :=
-    match st with TEnd => Next TEnd | TSR a P st => Next (st v) end.
-  Global Instance stype_head_ne d : NonExpansive (stype_head d).
+  Definition proto_head (d : V -c> A) (prot : proto V A) : V -c> A :=
+    match prot with TEnd => d | TSR a P prot => P end.
+  Definition proto_tail (v : V) (prot : protoC) : later protoC :=
+    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 stype_tail_ne v : NonExpansive (stype_tail v).
+  Global Instance proto_tail_ne v : NonExpansive (proto_tail v).
   Proof. destruct 1; naive_solver. Qed.
 
-  Definition stype_force (st : stype V A) : stype V A :=
-    match st with
+  Definition proto_force (prot : proto V A) : proto V A :=
+    match prot with
     | TEnd => TEnd
-    | TSR a P st => TSR a P st
+    | TSR a P prot => TSR a P prot
     end.
-  Lemma stype_force_eq st : stype_force st = st.
-  Proof. by destruct st. Defined.
+  Lemma proto_force_eq prot : proto_force prot = prot.
+  Proof. by destruct prot. Defined.
 
-  CoFixpoint stype_compl_go `{!Cofe A} (c : chain stypeC) : stypeC :=
+  CoFixpoint proto_compl_go `{!Cofe A} (c : chain protoC) : protoC :=
     match c O with
     | TEnd => TEnd
-    | TSR a P st => TSR a
-       (compl (chain_map (stype_head P) c) : V → A)
-       (λ v, stype_compl_go (later_chain (chain_map (stype_tail v) c)))
+    | TSR a P prot => TSR a
+       (compl (chain_map (proto_head P) c) : V → A)
+       (λ v, proto_compl_go (later_chain (chain_map (proto_tail v) c)))
     end.
 
-  Global Program Instance stype_cofe `{!Cofe A} : Cofe stypeC :=
-    {| compl c := stype_compl_go c |}.
+  Global Program Instance proto_cofe `{!Cofe A} : Cofe protoC :=
+    {| compl c := proto_compl_go c |}.
   Next Obligation.
     intros ? n c; rewrite /compl. revert c n. cofix IH=> c n.
-    rewrite -(stype_force_eq (stype_compl_go c)) /=.
-    destruct (c O) as [|a P st'] eqn:Hc0.
+    rewrite -(proto_force_eq (proto_compl_go c)) /=.
+    destruct (c O) as [|a P 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 P st') as Hcn.
+    - assert (c n ≡{0}≡ TSR a P prot') as Hcn.
       { rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
-      inversion Hcn as [|? P' ? st'' ? HP|]; subst.
+      inversion Hcn as [|? P' ? prot'' ? HP|]; subst.
       destruct n as [|n]; constructor.
-      + intros v. by rewrite (conv_compl 0 (chain_map (stype_head P) c) v) /= -H.
-      + intros v. by rewrite (conv_compl _ (chain_map (stype_head P) c) v) /= -H.
-      + intros v. assert (st'' v = later_car (stype_tail v (c (S n)))) as ->.
+      + intros v. by rewrite (conv_compl 0 (chain_map (proto_head P) c) v) /= -H.
+      + intros v. by rewrite (conv_compl _ (chain_map (proto_head P) 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_stype_contractive a n :
+  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_stype_ne a n :
+  Global Instance TSR_proto_ne a n :
     Proper (pointwise_relation _ (dist n) ==>
             pointwise_relation _ (dist n) ==> dist n) (TSR a).
   Proof.
-    intros P1 P2 HP st1 st2 Hst. apply TSR_stype_contractive=> //.
+    intros P1 P2 HP prot1 prot2 Hst. apply TSR_proto_contractive=> //.
     destruct n as [|n]=> // v /=. by apply dist_S.
   Qed.
-  Global Instance TSR_stype_proper a :
+  Global Instance TSR_proto_proper a :
     Proper (pointwise_relation _ (≡) ==>
             pointwise_relation _ (≡) ==> (≡)) (TSR a).
   Proof. by constructor. Qed.
 
-  Global Instance dual_stype_ne : NonExpansive dual_stype.
+  Global Instance dual_proto_ne : NonExpansive dual_proto.
   Proof.
-    cofix IH=> n st1 st2 Hst.
-    rewrite -(stype_force_eq (dual_stype st1)) -(stype_force_eq (dual_stype st2)).
+    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_stype_proper : Proper ((≡) ==> (≡)) dual_stype.
+  Global Instance dual_proto_proper : Proper ((≡) ==> (≡)) dual_proto.
   Proof. apply (ne_proper _). Qed.
 
-  Global Instance dual_stype_involutive : Involutive (≡) dual_stype.
+  Global Instance dual_proto_involutive : Involutive (≡) dual_proto.
   Proof.
-    cofix IH=> st. rewrite -(stype_force_eq (dual_stype (dual_stype _))).
-    destruct st as [|a P st]; first done.
+    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 stype_equivI {M} st1 st2 :
-    st1 ≡ st2 ⊣⊢@{uPredI M}
-        match st1, st2 with
+  Lemma proto_equivI {M} prot1 prot2 :
+    prot1 ≡ prot2 ⊣⊢@{uPredI M}
+        match prot1, prot2 with
         | TEnd, TEnd => True
-        | TSR a1 P1 st1, TSR a2 P2 st2 =>
-          ⌜ a1 = a2 ⌝ ∧ (∀ v, P1 v ≡ P2 v) ∧ ▷ (∀ v, st1 v ≡ st2 v)
+        | TSR a1 P1 prot1, TSR a2 P2 prot2 =>
+          ⌜ a1 = a2 ⌝ ∧ (∀ v, P1 v ≡ P2 v) ∧ ▷ (∀ v, prot1 v ≡ prot2 v)
         | _, _ => False
         end.
   Proof.
     uPred.unseal; constructor=> n x ?. split; first by destruct 1.
-    destruct st1, st2=> //=; [constructor|].
+    destruct prot1, prot2=> //=; [constructor|].
     by intros [[= ->] [??]]; destruct n; constructor.
   Qed.
 
-  Lemma stype_later_equiv M st a P2 st2 :
-    ▷ (st ≡ TSR a P2 st2) -∗
-    ◇ (∃ P1 st1, st ≡ TSR a P1 st1 ∗
+  Lemma proto_later_equiv M prot a P2 prot2 :
+    ▷ (prot ≡ TSR a P2 prot2) -∗
+    ◇ (∃ P1 prot1, prot ≡ TSR a P1 prot1 ∗
                  ▷ (∀ v, P1 v ≡ P2 v) ∗
-                 ▷ ▷ (∀ v, st1 v ≡ st2 v) : uPred M).
+                 ▷ ▷ (∀ v, prot1 v ≡ prot2 v) : uPred M).
   Proof.
-    iIntros "Heq". destruct st as [|a' P1 st1].
-    - iDestruct (stype_equivI with "Heq") as ">[]".
-    - iDestruct (stype_equivI with "Heq") as "(>-> & HPeq & Hsteq)".
-      iExists P1, st1. auto.
+    iIntros "Heq". destruct prot as [|a' P1 prot1].
+    - iDestruct (proto_equivI with "Heq") as ">[]".
+    - iDestruct (proto_equivI with "Heq") as "(>-> & HPeq & Hsteq)".
+      iExists P1, prot1. auto.
   Qed.
 
-  Lemma dual_stype_flip {M} st1 st2 :
-    dual_stype st1 ≡ st2 ⊣⊢@{uPredI M} st1 ≡ dual_stype st2.
+  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_stype_involutive.
-    - iIntros "Heq". iRewrite "Heq". by rewrite dual_stype_involutive.
+    - iIntros "Heq". iRewrite -"Heq". by rewrite dual_proto_involutive.
+    - iIntros "Heq". iRewrite "Heq". by rewrite dual_proto_involutive.
   Qed.
-End stype_ofe.
+End proto_ofe.
 
-Arguments stypeC : clear implicits.
+Arguments protoC : clear implicits.
 
-CoFixpoint stype_map {V A B} (f : A → B) (st : stype V A) : stype V B :=
-  match st with
+CoFixpoint proto_map {V A B} (f : A → B) (prot : proto V A) : proto V B :=
+  match prot with
   | TEnd => TEnd
-  | TSR a P st => TSR a (λ v, f (P v)) (λ v, stype_map f (st v))
+  | TSR a P prot => TSR a (λ v, f (P v)) (λ v, proto_map f (prot v))
   end.
-Lemma stype_map_ext_ne {V A} {B : ofeT} (f g : A → B) (st : stype V A) n :
-  (∀ x, f x ≡{n}≡ g x) → stype_map f st ≡{n}≡ stype_map g st.
+Lemma proto_map_ext_ne {V A} {B : ofeT} (f g : A → B) (prot : proto V A) n :
+  (∀ x, f x ≡{n}≡ g x) → proto_map f prot ≡{n}≡ proto_map g prot.
 Proof.
-  revert n st. cofix IH=> n st Hf.
-  rewrite -(stype_force_eq (stype_map f st)) -(stype_force_eq (stype_map g st)).
-  destruct st as [|a P st], n as [|n]; constructor=> v //. apply IH; auto using dist_S.
+  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 P prot], n as [|n]; constructor=> v //. apply IH; auto using dist_S.
 Qed.
-Lemma stype_map_ext {V A} {B : ofeT} (f g : A → B) (st : stype V A) :
-  (∀ x, f x ≡ g x) → stype_map f st ≡ stype_map g st.
+Lemma proto_map_ext {V A} {B : ofeT} (f g : A → B) (prot : proto V A) :
+  (∀ x, f x ≡ g x) → proto_map f prot ≡ proto_map g prot.
 Proof.
-  intros Hf. apply equiv_dist=> n. apply stype_map_ext_ne=> v.
+  intros Hf. apply equiv_dist=> n. apply proto_map_ext_ne=> v.
   apply equiv_dist, Hf.
 Qed.
-Instance stype_map_ne {V : Type} {A B : ofeT} (f : A → B) n :
+Instance proto_map_ne {V : Type} {A B : ofeT} (f : A → B) n :
   (∀ n, Proper (dist n ==> dist n) f) →
-  Proper (dist n ==> dist n) (@stype_map V _ _ f).
+  Proper (dist n ==> dist n) (@proto_map V _ _ f).
 Proof.
-  intros Hf. revert n. cofix IH=> n st1 st2 Hst.
-  rewrite -(stype_force_eq (stype_map _ st1)) -(stype_force_eq (stype_map _ st2)).
+  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 stype_fmap_id {V : Type} {A : ofeT} (st : stype V A) :
-  stype_map id st ≡ st.
+Lemma proto_fmap_id {V : Type} {A : ofeT} (prot : proto V A) :
+  proto_map id prot ≡ prot.
 Proof.
-  revert st. cofix IH=> st. rewrite -(stype_force_eq (stype_map _ _)).
-  destruct st; constructor=> v; auto.
+  revert prot. cofix IH=> prot. rewrite -(proto_force_eq (proto_map _ _)).
+  destruct prot; constructor=> v; auto.
 Qed.
-Lemma stype_fmap_compose {V : Type} {A B C : ofeT} (f : A → B) (g : B → C) st :
-  stype_map (g ∘ f) st ≡ stype_map g (@stype_map V _ _ f st).
+Lemma proto_fmap_compose {V : Type} {A B C : ofeT} (f : A → B) (g : B → C) prot :
+  proto_map (g ∘ f) prot ≡ proto_map g (@proto_map V _ _ f prot).
 Proof.
-  revert st. cofix IH=> st.
-  rewrite -(stype_force_eq (stype_map _ _)) -(stype_force_eq (stype_map g _)).
-  destruct st; constructor=> v; auto.
+  revert prot. cofix IH=> prot.
+  rewrite -(proto_force_eq (proto_map _ _)) -(proto_force_eq (proto_map g _)).
+  destruct prot; constructor=> v; auto.
 Qed.
 
-Definition stypeC_map {V A B} (f : A -n> B) : stypeC V A -n> stypeC V B :=
-  CofeMor (stype_map f : stypeC V A → stypeC V B).
-Instance stypeC_map_ne {V} A B : NonExpansive (@stypeC_map V A B).
-Proof. intros n f g ? st. by apply stype_map_ext_ne. Qed.
+Definition protoC_map {V A B} (f : A -n> B) : protoC V A -n> protoC V B :=
+  CofeMor (proto_map f : protoC V A → protoC V B).
+Instance protoC_map_ne {V} A B : NonExpansive (@protoC_map V A B).
+Proof. intros n f g ? prot. by apply proto_map_ext_ne. Qed.
 
-Program Definition stypeCF {V} (F : cFunctor) : cFunctor := {|
-  cFunctor_car A _ B _ := stypeC V (cFunctor_car F A _ B _);
-  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := stypeC_map (cFunctor_map F fg)
+Program Definition protoCF {V} (F : cFunctor) : cFunctor := {|
+  cFunctor_car A _ B _ := protoC V (cFunctor_car F A _ B _);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := protoC_map (cFunctor_map F fg)
 |}.
 Next Obligation. done. Qed.
 Next Obligation.
   by intros V F A1 ? A2 ? B1 ? B2 ? n f g Hfg;
-  apply stypeC_map_ne, cFunctor_ne.
+  apply protoC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros V F A ? B ? x. rewrite /= -{2}(stype_fmap_id x).
-  apply stype_map_ext=>y. apply cFunctor_id.
+  intros V F A ? B ? x. rewrite /= -{2}(proto_fmap_id x).
+  apply proto_map_ext=>y. apply cFunctor_id.
 Qed.
 Next Obligation.
   intros V F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x.
-  rewrite /= -stype_fmap_compose.
-  apply stype_map_ext=>y; apply cFunctor_compose.
+  rewrite /= -proto_fmap_compose.
+  apply proto_map_ext=>y; apply cFunctor_compose.
 Qed.
 
-Instance stypeCF_contractive {V} F :
-  cFunctorContractive F → cFunctorContractive (@stypeCF V F).
+Instance protoCF_contractive {V} F :
+  cFunctorContractive F → cFunctorContractive (@protoCF V F).
 Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
-  apply stypeC_map_ne, cFunctor_contractive.
+  apply protoC_map_ne, cFunctor_contractive.
 Qed.
 
 Class IsDualAction (a1 a2 : action) :=
@@ -292,26 +292,26 @@ Proof. done. Qed.
 Instance is_dual_action_Receive : IsDualAction Receive Send.
 Proof. done. Qed.
 
-Section DualStype.
+Section DualProto.
   Context {V : Type} {A : ofeT}.
 
-  Class IsDualStype (st1 st2 : stype V A) :=
-  is_dual_stype : dual_stype st1 ≡ st2.
+  Class IsDualProto (prot1 prot2 : proto V A) :=
+  is_dual_proto : dual_proto prot1 ≡ prot2.
 
-  Global Instance is_dual_default (st : stype V A) :
-    IsDualStype st (dual_stype st) | 100.
-  Proof. by rewrite /IsDualStype. Qed.
+  Global Instance is_dual_default (prot : proto V A) :
+    IsDualProto prot (dual_proto prot) | 100.
+  Proof. by rewrite /IsDualProto. Qed.
 
-  Global Instance is_dual_end : IsDualStype (TEnd : stype V A) TEnd.
-  Proof. by rewrite /IsDualStype -(stype_force_eq (dual_stype _)). Qed.
+  Global Instance is_dual_end : IsDualProto (TEnd : proto V A) TEnd.
+  Proof. by rewrite /IsDualProto -(proto_force_eq (dual_proto _)). Qed.
 
-  Global Instance is_dual_tsr a1 a2 P (st1 st2 : V → stype V A) :
+  Global Instance is_dual_tsr a1 a2 P (prot1 prot2 : V → proto V A) :
     IsDualAction a1 a2 →
-    (∀ x, IsDualStype (st1 x) (st2 x)) →
-    IsDualStype (TSR a1 P st1) (TSR a2 P st2).
+    (∀ x, IsDualProto (prot1 x) (prot2 x)) →
+    IsDualProto (TSR a1 P prot1) (TSR a2 P prot2).
   Proof.
-    rewrite /IsDualAction /IsDualStype. intros <- Hst.
-    rewrite /IsDualStype -(stype_force_eq (dual_stype _)) /=.
+    rewrite /IsDualAction /IsDualProto. intros <- Hst.
+    rewrite /IsDualProto -(proto_force_eq (dual_proto _)) /=.
     by constructor=> v.
   Qed.
-End DualStype.
+End DualProto.
diff --git a/theories/proto/proto_enc.v b/theories/proto/proto_enc.v
index 05a775e..2989bb1 100644
--- a/theories/proto/proto_enc.v
+++ b/theories/proto/proto_enc.v
@@ -5,53 +5,53 @@ From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
 From osiris.proto Require Export encodable proto_specs.
 
-Section DualStypeEnc.
+Section DualProtoEnc.
   Context `{EncDec V} `{PROP: bi} .
 
   Definition TSR'
-    (a : action) (P : V → PROP) (st : V → stype val PROP) : stype val PROP :=
+    (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 st x else TEnd (* dummy *)).
+    (λ v, if 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 → stype val PROP) :
+  Global Instance is_dual_tsr' a1 a2 P (st1 st2 : V → proto val PROP) :
     IsDualAction a1 a2 →
-    (∀ x, IsDualStype (st1 x) (st2 x)) →
-    IsDualStype (TSR' a1 P st1) (TSR' a2 P st2).
+    (∀ x, IsDualProto (st1 x) (st2 x)) →
+    IsDualProto (TSR' a1 P st1) (TSR' a2 P st2).
   Proof.
-    rewrite /IsDualAction /IsDualStype. intros <- Hst.
-    rewrite -(stype_force_eq (dual_stype _)).
+    rewrite /IsDualAction /IsDualProto. intros <- Hst.
+    rewrite -(proto_force_eq (dual_proto _)).
     constructor=> x. done. destruct (decode x)=> //.
     apply is_dual_end.
   Qed.
 
-End DualStypeEnc.
+End DualProtoEnc.
 
-Notation "<!> x @ P , st" :=
-  (TSR' Send (λ x, P%I) (λ x, st%stype))
-  (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<?> x @ P , st" :=
-  (TSR' Receive (λ x, P%I) (λ x, st%stype))
-  (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<!> x , st" := (<!> x @ True, (st x))%stype
-  (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<?> x , st" := (<?> x @ True, (st x))%stype
-  (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<!> @ P , st" := (<!> dummy__ @ P dummy__, st dummy__)%stype
-  (at level 200, st at level 200) : stype_scope.
-Notation "<?> @ P , st" := (<?> dummy__ @ P dummy__, st dummy__)%stype
-  (at level 200, st at level 200) : stype_scope.
+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 "<!> @ P , prot" := (<!> dummy__ @ P dummy__, prot dummy__)%proto
+  (at level 200, prot at level 200) : proto_scope.
+Notation "<?> @ P , prot" := (<?> dummy__ @ P dummy__, prot dummy__)%proto
+  (at level 200, prot at level 200) : proto_scope.
 
-Section stype_enc_specs.
+Section proto_enc_specs.
   Context `{!heapG Σ} (N : namespace).
   Context `{!logrelG val Σ}.
 
   Lemma send_st_spec (A : Type) `{EncDec A}
-        st γ c s (P : A → iProp Σ) w :
-    {{{ P w ∗ ⟦ c @ s : <!> @ P, st ⟧{N,γ} }}}
+        prot γ c s (P : A → iProp Σ) w :
+    {{{ P w ∗ ⟦ c @ s : <!> @ P, prot ⟧{N,γ} }}}
       send c #s (encode w)
-    {{{ RET #(); ⟦ c @ s : st w ⟧{N,γ} }}}.
+    {{{ RET #(); ⟦ c @ s : prot w ⟧{N,γ} }}}.
   Proof.
     iIntros (Φ) "[HP Hsend] HΦ".
     iApply (send_st_spec with "[HP Hsend]").
@@ -64,10 +64,10 @@ Section stype_enc_specs.
   Qed.
 
   Lemma recv_st_spec (A : Type) `{EncDec A}
-        st γ c s (P : A → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ P, st ⟧{N,γ} }}}
+        prot γ c s (P : A → iProp Σ) :
+    {{{ ⟦ c @ s : <?> @ P, prot ⟧{N,γ} }}}
       recv c #s
-    {{{ v, RET (encode v); ⟦ c @ s : st v ⟧{N,γ} ∗ P v }}}.
+    {{{ v, RET (encode v); ⟦ c @ s : prot v ⟧{N,γ} ∗ P v }}}.
   Proof.
     iIntros (Φ) "Hrecv HΦ".
     iApply (recv_st_spec with "Hrecv").
@@ -86,4 +86,4 @@ Section stype_enc_specs.
     - inversion Hw.
   Qed.
 
-End stype_enc_specs.
\ No newline at end of file
+End proto_enc_specs.
\ No newline at end of file
diff --git a/theories/proto/proto_specs.v b/theories/proto/proto_specs.v
index c6d1277..a0a3ea3 100644
--- a/theories/proto/proto_specs.v
+++ b/theories/proto/proto_specs.v
@@ -11,67 +11,67 @@ From osiris.proto Require Export channel.
 
 Class logrelG A Σ := {
   logrelG_channelG :> chanG Σ;
-  logrelG_authG :> auth_exclG (laterC (stypeC A (iPreProp Σ))) Σ;
+  logrelG_authG :> auth_exclG (laterC (protoC A (iPreProp Σ))) Σ;
 }.
 
 Definition logrelΣ A :=
   #[ chanΣ ; GFunctor (authRF(optionURF (exclRF
-                       (laterCF (@stypeCF A idCF))))) ].
+                       (laterCF (@protoCF A idCF))))) ].
 Instance subG_chanΣ {A Σ} : subG (logrelΣ A) Σ → logrelG A Σ.
 Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
 
-Fixpoint st_eval `{!logrelG val Σ} (vs : list val) (st1 st2 : stype val (iProp Σ)) : iProp Σ :=
+Fixpoint prot_eval `{!logrelG val Σ} (vs : list val) (prot1 prot2 : proto val (iProp Σ)) : iProp Σ :=
   match vs with
-  | [] => st1 ≡ dual_stype st2
-  | v::vs => match st2 with
-             | TSR Receive P st2  => P v ∗ ▷ st_eval vs st1 (st2 v)
+  | [] => prot1 ≡ dual_proto prot2
+  | v::vs => match prot2 with
+             | TSR Receive P prot2  => P v ∗ ▷ prot_eval vs prot1 (prot2 v)
              | _ => False
              end
   end%I.
-Arguments st_eval : simpl nomatch.
+Arguments prot_eval : simpl nomatch.
 
-Record st_name := STName {
-  st_c_name : chan_name;
-  st_l_name : gname;
-  st_r_name : gname
+Record prot_name := ProtName {
+  prot_c_name : chan_name;
+  prot_l_name : gname;
+  prot_r_name : gname
 }.
 
-Definition to_stype_auth_excl `{!logrelG val Σ} (st : stype val (iProp Σ)) :=
-  to_auth_excl (Next (stype_map iProp_unfold st)).
+Definition to_proto_auth_excl `{!logrelG val Σ} (prot : proto val (iProp Σ)) :=
+  to_auth_excl (Next (proto_map iProp_unfold prot)).
 
-Definition st_own `{!logrelG val Σ} (γ : st_name) (s : side)
-    (st : stype val (iProp Σ)) : iProp Σ :=
-  own (side_elim s st_l_name st_r_name γ) (◯ to_stype_auth_excl st)%I.
+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 st_ctx `{!logrelG val Σ} (γ : st_name) (s : side)
-    (st : stype val (iProp Σ)) : iProp Σ :=
-  own (side_elim s st_l_name st_r_name γ) (● to_stype_auth_excl st)%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_st `{!logrelG val Σ} (γ : st_name) (c : val) : iProp Σ :=
-  (∃ l r stl str,
-    chan_own (st_c_name γ) Left l ∗
-    chan_own (st_c_name γ) Right r ∗
-    st_ctx γ Left stl  ∗
-    st_ctx γ Right str ∗
-    ▷ ((⌜r = []⌝ ∗ st_eval l stl str) ∨
-       (⌜l = []⌝ ∗ st_eval r str stl)))%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_st `{!logrelG val Σ, !heapG Σ} (N : namespace) (γ : st_name)
-    (c : val) (s : side) (st : stype val (iProp Σ)) : iProp Σ :=
-  (st_own γ s st ∗ is_chan N (st_c_name γ) c ∗ inv N (inv_st γ c))%I.
-Instance: Params (@interp_st) 7.
+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 : st ⟧{ N , γ }" := (interp_st N γ c s st)
-  (at level 10, s at next level, st at next level, γ at next level,
-   format "⟦  c  @  s  :  st  ⟧{ N , γ }").
+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 stype.
+Section proto.
   Context `{!logrelG val Σ, !heapG Σ} (N : namespace).
 
-  Global Instance st_eval_ne : NonExpansive2 (st_eval vs).
+  Global Instance prot_eval_ne : NonExpansive2 (prot_eval vs).
   Proof.
     induction vs as [|v vs IH];
-      destruct 2 as [n|[] P1 P2 st1 st2|n [] P1 P2 st1 st2]=> //=.
+      destruct 2 as [n|[] P1 P2 prot1 prot2|n [] P1 P2 prot1 prot2]=> //=.
     - by repeat f_equiv.
     - f_equiv. done. f_equiv. by constructor.
     - f_equiv. done. f_equiv. by constructor.
@@ -80,139 +80,139 @@ Section stype.
     - f_equiv. done. by f_contractive.
     - f_equiv. done. f_contractive. apply IH. by apply dist_S. done.
   Qed.
-  Global Instance st_eval_proper vs : Proper ((≡) ==> (≡) ==> (≡)) (st_eval vs).
+  Global Instance prot_eval_proper vs : Proper ((≡) ==> (≡) ==> (≡)) (prot_eval vs).
   Proof. apply (ne_proper_2 _). Qed.
 
-  Global Instance to_stype_auth_excl_ne : NonExpansive to_stype_auth_excl.
+  Global Instance to_proto_auth_excl_ne : NonExpansive to_proto_auth_excl.
   Proof. solve_proper. Qed.
-  Global Instance st_own_ne γ s : NonExpansive (st_own γ s).
+  Global Instance prot_own_ne γ s : NonExpansive (prot_own γ s).
   Proof. solve_proper. Qed.
-  Global Instance interp_st_ne γ c s : NonExpansive (interp_st N γ c s).
+  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_st N γ c s).
+  Global Instance interp_st_proper γ c s : Proper ((≡) ==> (≡)) (interp_prot N γ c s).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma st_excl_eq γ s st st' :
-    st_ctx γ s st -∗ st_own γ s st' -∗ ▷ (st ≡ st').
+  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 (∀ st : stype val (iProp Σ),
-      stype_map iProp_fold (stype_map iProp_unfold st) ≡ st) as help.
-    { intros st''. rewrite -stype_fmap_compose -{2}(stype_fmap_id st'').
-      apply stype_map_ext=> P. by rewrite /= iProp_fold_unfold. }
-    rewrite -{2}(help st). iRewrite "Hvalid". by rewrite help.
+    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 st_excl_update γ s st st' st'' :
-    st_ctx γ s st -∗ st_own γ s st' ==∗ st_ctx γ s st'' ∗ st_own γ s st''.
+  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_stype_auth_excl st'')
-                              (to_stype_auth_excl st'')).
+    { 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 st_eval_send (P : val →iProp Σ) st vs v str :
-    P v -∗ st_eval vs (<!> @ P, st) str -∗ st_eval (vs ++ [v]) (st v) str.
+  Lemma prot_eval_send (P : val →iProp Σ) prot vs v protr :
+    P v -∗ prot_eval vs (<!> @ P, prot) protr -∗ prot_eval (vs ++ [v]) (prot v) protr.
   Proof.
     iIntros "HP".
-    iRevert (str).
-    iInduction vs as [|v' vs] "IH"; iIntros (str) "Heval".
-    - iDestruct (dual_stype_flip with "Heval") as "Heval".
+    iRevert (protr).
+    iInduction vs as [|v' vs] "IH"; iIntros (protr) "Heval".
+    - iDestruct (dual_proto_flip with "Heval") as "Heval".
       iRewrite -"Heval"; simpl.
-      rewrite dual_stype_involutive.
+      rewrite dual_proto_involutive.
       by iFrame.
-    - destruct str as [|[] P' str]=> //=.
+    - destruct protr as [|[] P' protr]=> //=.
       iDestruct "Heval" as "[$ Heval]".
       by iApply ("IH" with "HP").
   Qed.
 
-  Lemma st_eval_recv (P : val → iProp Σ) st1 l st2 v :
-     st_eval (v :: l) st1 (<?> @ P, st2) -∗ ▷ st_eval l st1 (st2 v) ∗ P v.
+  Lemma prot_eval_recv (P : val → iProp Σ) prot1 l prot2 v :
+     prot_eval (v :: l) prot1 (<?> @ P, prot2) -∗ ▷ prot_eval l prot1 (prot2 v) ∗ P v.
   Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed.
 
-  Lemma new_chan_vs st E c cγ :
+  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 γ := STName cγ lγ rγ in
-      ⟦ c @ Left : st ⟧{N,γ} ∗ ⟦ c @ Right : dual_stype st ⟧{N,γ}.
+      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_stype_auth_excl st) ⋅
-                     ◯ (to_stype_auth_excl st))) as (lγ) "[Hlsta Hlstf]".
+    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_stype_auth_excl (dual_stype st)) ⋅
-                     ◯ (to_stype_auth_excl (dual_stype st)))) as (rγ) "[Hrsta Hrstf]".
+    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 (STName cγ lγ rγ) as stγ.
-    iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
-    { iNext. rewrite /inv_st. eauto 10 with iFrame. }
+    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 st1 st2 :
-    IsDualStype st1 st2 →
+  Lemma new_chan_st_spec prot1 prot2 :
+    IsDualProto prot1 prot2 →
     {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c; ⟦ c @ Left : st1 ⟧{N,γ} ∗ ⟦ c @ Right : st2 ⟧{N,γ} }}}.
+    {{{ c γ, RET c; ⟦ c @ Left : prot1 ⟧{N,γ} ∗ ⟦ c @ Right : prot2 ⟧{N,γ} }}}.
   Proof.
-    rewrite /IsDualStype.
-    iIntros (Hst Φ _) "HΦ".
+    rewrite /IsDualProto.
+    iIntros (Hprot Φ _) "HΦ".
     iApply (wp_fupd).
     iApply (new_chan_spec)=> //.
     iModIntro.
     iIntros (c γ) "[Hc Hctx]".
-    iMod (new_chan_vs st1 ⊤ c γ with "[-HΦ]") as "H".
+    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 Hst.
+    rewrite Hprot.
     by iFrame.
   Qed.
 
-  Lemma send_vs c γ s (P : val → iProp Σ) st E :
+  Lemma send_vs c γ s (P : val → iProp Σ) prot E :
     ↑N ⊆ E →
-    ⟦ c @ s : TSR Send P st ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
-      chan_own (st_c_name γ) s vs ∗
+    ⟦ c @ s : TSR Send P prot ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
+      chan_own (prot_c_name γ) s vs ∗
       ▷ ∀ v, P v -∗
-             chan_own (st_c_name γ) s (vs ++ [v]) ={E∖↑N,E}=∗
-             ⟦ c @ s : st v ⟧{N,γ}.
+             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 stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
+    iInv N as (l r protl protr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
     iModIntro.
     destruct s.
     - iExists _.
       iIntros "{$Hclf} !>" (v) "HP Hclf".
       iRename "Hstf" into "Hstlf".
-      iDestruct (st_excl_eq with "Hstla Hstlf") as "#Heq".
-      iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf") as "[Hstla 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 (st_eval_send with "HP").
+          iApply (prot_eval_send with "HP").
           by iRewrite "Heq" in "Heval".
         - iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //=.
           iSplit; first done.
-          iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_stype_involutive. }
+          iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_proto_involutive. }
       iModIntro. iFrame. auto.
     - iExists _.
       iIntros "{$Hcrf} !>" (v) "HP Hcrf".
       iRename "Hstf" into "Hstrf".
-      iDestruct (st_excl_eq with "Hstra Hstrf") as "#Heq".
-      iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf") as "[Hstra 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.
@@ -220,17 +220,17 @@ Section stype.
         iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
         - iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
           iSplit; first done. simpl.
-          iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_stype_involutive.
+          iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_proto_involutive.
         - iSplit=> //.
-          iApply (st_eval_send with "HP").
+          iApply (prot_eval_send with "HP").
           by iRewrite "Heq" in "Heval". }
       iModIntro. iFrame. auto.
   Qed.
 
-  Lemma send_st_spec st γ c s (P : val → iProp Σ) v :
-    {{{ P v ∗ ⟦ c @ s : <!> @ P , st ⟧{N,γ} }}}
+  Lemma send_st_spec prot γ c s (P : val → iProp Σ) v :
+    {{{ P v ∗ ⟦ c @ s : <!> @ P , prot ⟧{N,γ} }}}
       send c #s v
-    {{{ RET #(); ⟦ c @ s : st v ⟧{N,γ} }}}.
+    {{{ RET #(); ⟦ c @ s : prot v ⟧{N,γ} }}}.
   Proof.
     iIntros (Φ) "[HP Hsend] HΦ".
     iApply (send_spec with "[#]").
@@ -241,25 +241,25 @@ Section stype.
     iApply ("H" $! v with "HP"). by destruct s.
   Qed.
 
-  Lemma try_recv_vs c γ s (P : val → iProp Σ) st E :
+  Lemma try_recv_vs c γ s (P : val → iProp Σ) prot E :
     ↑N ⊆ E →
-    ⟦ c @ s : TSR Receive P st ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
-      chan_own (st_c_name γ) (dual_side s) vs ∗
+    ⟦ c @ s : TSR Receive P prot ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
+      chan_own (prot_c_name γ) (dual_side s) vs ∗
       ▷ ((⌜vs = []⌝ -∗
-           chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
-           ⟦ c @ s : TSR Receive P st ⟧{N,γ}) ∧
+           chan_own (prot_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
+           ⟦ c @ s : TSR Receive P prot ⟧{N,γ}) ∧
          (∀ v vs',
            ⌜vs = v :: vs'⌝ -∗
-           chan_own (st_c_name γ) (dual_side s) vs' ={E∖↑N,E}=∗
-           ⟦ c @ s : (st v) ⟧{N,γ} ∗ ▷ P v)).
+           chan_own (prot_c_name γ) (dual_side s) vs' ={E∖↑N,E}=∗
+           ⟦ c @ s : (prot v) ⟧{N,γ} ∗ ▷ P v)).
   Proof.
     iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
-    iInv N as (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
+    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 (st_excl_eq with "Hstla Hstlf") as "#Heq".
+      iDestruct (prot_excl_eq with "Hstla Hstlf") as "#Heq".
       iSplit.
       + iIntros (->) "Hown".
         iMod ("Hclose" with "[-Hstlf]") as "_".
@@ -267,11 +267,11 @@ Section stype.
         iModIntro. iFrame "Hcctx ∗ Hinv".
       + iIntros (v vs ->) "Hown".
         iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
-        iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
-        iDestruct (stype_later_equiv with "Heq") as ">Hleq".
-        iDestruct "Hleq" as (P1 st1) "(Hsteq & HPeq & Hsteq')".
+        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 (st_eval_recv with "Heval") as "[Heval HP]".
+        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). }
@@ -279,7 +279,7 @@ Section stype.
         iNext. by iRewrite -("HPeq" $! v).
     - iIntros "{$Hclf} !>".
       iRename "Hstf" into "Hstrf".
-      iDestruct (st_excl_eq with "Hstra Hstrf") as "#Heq".
+      iDestruct (prot_excl_eq with "Hstra Hstrf") as "#Heq".
       iSplit=> //.
       + iIntros (->) "Hown".
         iMod ("Hclose" with "[-Hstrf]") as "_".
@@ -287,11 +287,11 @@ Section stype.
         iModIntro. iFrame "Hcctx ∗ Hinv".
       + iIntros (v vs' ->) "Hown".
         iDestruct "Hinv'" as "[[>-> Heval]|[>% Heval]]"; last done.
-        iMod (st_excl_update _ _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
-        iDestruct (stype_later_equiv with "Heq") as ">Hleq".
-        iDestruct "Hleq" as (P1 st1) "(Hsteq & HPeq & Hsteq')".
+        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 (st_eval_recv with "Heval") as "[Heval HP]".
+        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). }
@@ -299,11 +299,11 @@ Section stype.
         iNext. by iRewrite -("HPeq" $! v).
   Qed.
 
-  Lemma try_recv_st_spec st γ c s (P : val → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ P , st ⟧{N,γ} }}}
+  Lemma try_recv_st_spec prot γ c s (P : val → iProp Σ) :
+    {{{ ⟦ c @ s : <?> @ P , prot ⟧{N,γ} }}}
       try_recv c #s
-    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : <?> @ P, st ⟧{N,γ}) ∨
-                  (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : st w ⟧{N,γ} ∗ ▷ P w)}}}.
+    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : <?> @ P, prot ⟧{N,γ}) ∨
+                  (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : prot w ⟧{N,γ} ∗ ▷ P w)}}}.
   Proof.
     iIntros (Φ) "Hrecv HΦ".
     iApply (try_recv_spec with "[#]").
@@ -325,10 +325,10 @@ Section stype.
       iApply "HΦ"; eauto with iFrame.
   Qed.
 
-  Lemma recv_st_spec st γ c s (P : val → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ P ,  st ⟧{N,γ} }}}
+  Lemma recv_st_spec prot γ c s (P : val → iProp Σ) :
+    {{{ ⟦ c @ s : <?> @ P ,  prot ⟧{N,γ} }}}
       recv c #s
-    {{{ v, RET v; ⟦ c @ s : st v ⟧{N,γ} ∗ P v }}}.
+    {{{ v, RET v; ⟦ c @ s : prot v ⟧{N,γ} ∗ P v }}}.
   Proof.
     iIntros (Φ) "Hrecv HΦ".
     iLöb as "IH". wp_rec.
@@ -339,4 +339,4 @@ Section stype.
     - iDestruct "H" as (w ->) "[H HP]".
       wp_pures. iApply "HΦ". iFrame.
   Qed.
-End stype. 
+End proto. 
-- 
GitLab