From 1fa2c070aa1fd3f4b0df04ae79aaaaefdef32c26 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Jul 2019 14:33:27 +0200
Subject: [PATCH] Some renaming.

---
 _CoqProject                                   |   8 +-
 theories/examples/loop_sort.v                 |   6 +-
 theories/examples/mapper.v                    |   2 +-
 theories/examples/producer_consumer.v         |  98 +++++++-------
 theories/examples/{list_sort.v => sort.v}     |  20 +--
 .../{list_sort_instances.v => sort_client.v}  |  12 +-
 .../{list_sort_elem.v => sort_elem.v}         | 123 +++++++++---------
 ..._sort_elem_client.v => sort_elem_client.v} |  26 ++--
 8 files changed, 150 insertions(+), 145 deletions(-)
 rename theories/examples/{list_sort.v => sort.v} (93%)
 rename theories/examples/{list_sort_instances.v => sort_client.v} (79%)
 rename theories/examples/{list_sort_elem.v => sort_elem.v} (65%)
 rename theories/examples/{list_sort_elem_client.v => sort_elem_client.v} (78%)

diff --git a/_CoqProject b/_CoqProject
index 0ce2b93..9f9f2c7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,8 +10,8 @@ theories/channel/channel.v
 theories/channel/proto_model.v
 theories/channel/proto_channel.v
 theories/channel/proofmode.v
-theories/examples/list_sort.v
-theories/examples/list_sort_instances.v
-theories/examples/list_sort_elem.v
+theories/examples/sort.v
+theories/examples/sort_client.v
+theories/examples/sort_elem.v
 theories/examples/loop_sort.v
-theories/examples/list_sort_elem_client.v
+theories/examples/sort_elem_client.v
diff --git a/theories/examples/loop_sort.v b/theories/examples/loop_sort.v
index ff403fb..a779c92 100644
--- a/theories/examples/loop_sort.v
+++ b/theories/examples/loop_sort.v
@@ -2,11 +2,11 @@ From stdpp Require Import sorting.
 From osiris.channel Require Import proto_channel.
 From iris.heap_lang Require Import proofmode notation.
 From osiris.utils Require Import list.
-From osiris.examples Require Import list_sort.
+From osiris.examples Require Import sort.
 
 Definition loop_sort_service : val :=
   rec: "go" "c" :=
-    if: recv "c" then list_sort_service "c";; "go" "c"
+    if: recv "c" then sort_service "c";; "go" "c"
     else if: recv "c" then
       let: "d" := start_chan "go" in
       send "c" "d";;
@@ -33,7 +33,7 @@ Section loop_sort.
   Proof.
     iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
     wp_rec. wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.
-    { wp_apply (list_sort_service_spec with "Hc"); iIntros "Hc".
+    { wp_apply (sort_service_spec with "Hc"); iIntros "Hc".
       by wp_apply ("IH" with "Hc"). }
     wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.
     - wp_apply (start_chan_proto_spec N loop_sort_protocol); iIntros (d) "Hd".
diff --git a/theories/examples/mapper.v b/theories/examples/mapper.v
index 1f13162..1e5904a 100644
--- a/theories/examples/mapper.v
+++ b/theories/examples/mapper.v
@@ -3,7 +3,7 @@ From osiris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
 From osiris.utils Require Import list compare spin_lock contribution.
-From osiris.examples Require Import list_sort_elem.
+From osiris.examples Require Import sort_elem.
 From iris.algebra Require Import gmultiset.
 
 Definition mapper : val :=
diff --git a/theories/examples/producer_consumer.v b/theories/examples/producer_consumer.v
index 3b6d8fb..e0efb05 100644
--- a/theories/examples/producer_consumer.v
+++ b/theories/examples/producer_consumer.v
@@ -2,9 +2,7 @@ From stdpp Require Import sorting.
 From osiris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From iris.heap_lang.lib Require Import spin_lock.
-From osiris.utils Require Import list compare.
-
+From osiris.utils Require Import list compare spin_lock.
 
 Definition qnew : val := λ: <>, #().
 Definition qenqueue : val := λ: "q" "v", #().
@@ -20,55 +18,55 @@ Definition stop := false.
 Definition some := true.
 Definition none := false.
 
-Definition dist_queue : val :=
+Definition pd_loop : val :=
   rec: "go" "q" "pc" "cc" "c" :=
     if: "cc" ≤ #0 then #() else 
-    if: recv "c"                (* enq/deq *)
-    then if: recv "c"           (* cont/stop *)
-         then "go" (qenqueue "q" (recv "c")) "pc" "cc" "c"
-         else "go" "q" ("pc"-#1) "cc" "c"
-    else if: (qis_empty "q")
-         then if: "pc" ≤ #0
-              then send "c" #stop;; "go" "q" "pc" ("cc"-#1) "c"
-              else send "c" #cont;; send "c" #none;; "go" "q" "pc" "cc" "c"
-         else send "c" #cont;; send "c" #some;;
-              let: "qv" := qdequeue "q" in
-              send "c" (Snd "qv");; "go" (Fst "qv") "pc" "cc" "c".
-
-Definition producer : val :=
-  rec: "go" "c" "l" "produce" :=
-    (* acquire "l";; *)
-    match: "produce" #() with
-      SOME "v" =>
-        acquire "l";;
-        send "c" #enq;; send "c" #cont;; send "c" "v";;
-        release "l";;
-        "go" "c" "l" "produce"
-     | NONE =>
-        acquire "l";;
-        send "c" #enq;; send "c" #stop
-        release "l"
-    end.
-
-Definition consumer : val :=
-  rec: "go" "c" "l" "consume" :=
-    acquire "l";;
-    send "c" #deq;;
-    if: recv "c"             (* cont/stop *)
-    then if: recv "c"        (* some/none *)
-         then let: "v" := SOME (recv "c") in
-              release "l";; "consume" "v";; "go" "c" "l" "consume"
-              (* "consume" "v";; release "l";; "go" "c" "l" "consume" *)
-         else release "l";; "go" "c" "l" "consume"
-    else "consume" NONE;; release "l";; #().
-    (* else release "l";; "consume" NONE;; #(). *)
-
-(* Makes n producers and m consumers *)
-Definition produce_consume : val :=
-  λ: "produce" "consume" "pc" "cc",
-  #().
-
-Section list_sort_elem.
+    if: recv "c" then (* enq/deq *)
+      if: recv "c" then (* cont/stop *)
+        "go" (qenqueue "q" (recv "c")) "pc" "cc" "c"
+      else "go" "q" ("pc"-#1) "cc" "c"
+    else
+      if: (qis_empty "q") then
+        if: "pc" ≤ #0 then
+          send "c" #stop;;
+          "go" "q" "pc" ("cc"-#1) "c"
+        else
+          send "c" #cont;; send "c" #none;;
+          "go" "q" "pc" "cc" "c"
+      else
+        send "c" #cont;; send "c" #some;;
+        let: "qv" := qdequeue "q" in
+        send "c" (Snd "qv");;
+        "go" (Fst "qv") "pc" "cc" "c".
+
+Definition new_pd : val := λ: "pc" "cc",
+  let: "q" := qnew #() in
+  let: "c" := start_chan (λ: "c", pd_loop "q" "pc" "cc" "c") in
+  let: "l" := new_lock #() in
+  ("c", "l").
+
+Definition pd_send : val := λ: "cl" "x",
+  acquire (Snd "cl");;
+  send (Fst "cl") #enq;; send (Fst "cl") #cont;; send (Fst "cl") "x";;
+  release (Snd "cl").
+
+Definition pd_stop : val := λ: "cl",
+  acquire (Fst "cl");;
+  send (Snd "cl") #enq;; send (Snd "cl") #stop;;
+  release (Fst "cl").
+
+Definition pd_recv : val :=
+  rec: "go" "cl" :=
+    acquire (Fst "cl");;
+    send (Snd "cl") #deq;;
+    if: recv (Snd "cl") then    (* cont/stop *)
+       if: recv (Snd "cl") then (* some/none *)
+         let: "v" := recv (Snd "cl") in
+         release (Fst "cl");; SOME "v"
+       else release (Fst "cl");; "go" "c" "l"
+    else release (Fst "cl");; NONE.
+
+Section sort_elem.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
 
   Definition queue_prot : iProto Σ := (END)%proto.
diff --git a/theories/examples/list_sort.v b/theories/examples/sort.v
similarity index 93%
rename from theories/examples/list_sort.v
rename to theories/examples/sort.v
index aef3c25..ce043c8 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/sort.v
@@ -13,7 +13,7 @@ Definition lmerge : val :=
     then lcons "y" ("go" "cmp" (ltail "ys") "zs")
     else lcons "z" ("go" "cmp" "ys" (ltail "zs")).
 
-Definition list_sort_service : val :=
+Definition sort_service : val :=
   rec: "go" "c" :=
     let: "cmp" := recv "c" in
     let: "xs" := recv "c" in
@@ -30,12 +30,12 @@ Definition list_sort_service : val :=
     "xs" <- lmerge "cmp" !"ys" !"zs";;
     send "c" #().
 
-Definition list_sort_client : val := λ: "cmp" "xs",
-  let: "c" := start_chan list_sort_service in
+Definition sort_client : val := λ: "cmp" "xs",
+  let: "c" := start_chan sort_service in
   send "c" "cmp";; send "c" "xs";;
   recv "c".
 
-Section list_sort.
+Section sort.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
 
   Definition sort_protocol : iProto Σ :=
@@ -82,9 +82,9 @@ Section list_sort.
       iApply "HΨ". iFrame.
   Qed.
 
-  Lemma list_sort_service_spec p c :
+  Lemma sort_service_spec p c :
     {{{ c ↣ iProto_dual sort_protocol <++> p @ N }}}
-      list_sort_service c
+      sort_service c
     {{{ RET #(); c ↣ p @ N }}}.
   Proof.
     iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ).
@@ -122,21 +122,21 @@ Section list_sort.
     - by iApply "HΨ".
   Qed.
 
-  Lemma list_sort_client_spec {A} (I : A → val → iProp Σ) R
+  Lemma sort_client_spec {A} (I : A → val → iProp Σ) R
        `{!RelDecision R, !Total R} cmp l (vs : list val) (xs : list A) :
     cmp_spec I R cmp -∗
     {{{ l ↦ val_encode vs ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
-      list_sort_client cmp #l
+      sort_client cmp #l
     {{{ ys ws, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗
                l ↦ val_encode ws ∗ [∗ list] y;w ∈ ys;ws, I y w }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
     wp_apply (start_chan_proto_spec N sort_protocol); iIntros (c) "Hc".
     { rewrite -(right_id END%proto _ (iProto_dual _)).
-      wp_apply (list_sort_service_spec with "Hc"); auto. }
+      wp_apply (sort_service_spec with "Hc"); auto. }
     wp_send with "[$Hcmp]".
     wp_send with "[$Hl]".
     wp_recv (ys ws) as "(Hsorted & Hperm & Hl & HI)".
     wp_pures. iApply "HΦ"; iFrame.
   Qed.
-End list_sort.
+End sort.
diff --git a/theories/examples/list_sort_instances.v b/theories/examples/sort_client.v
similarity index 79%
rename from theories/examples/list_sort_instances.v
rename to theories/examples/sort_client.v
index c2ddd86..e52de6d 100644
--- a/theories/examples/list_sort_instances.v
+++ b/theories/examples/sort_client.v
@@ -2,22 +2,22 @@ From stdpp Require Import sorting.
 From osiris.channel Require Import proto_channel.
 From iris.heap_lang Require Import proofmode notation.
 From osiris.utils Require Import list compare.
-From osiris.examples Require Import list_sort.
+From osiris.examples Require Import sort.
 
-Section list_sort_instances.
+Section sort_client.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
 
   Local Arguments val_encode _ _ !_ /.
 
-  Lemma list_sort_client_le_spec l (xs : list Z) :
+  Lemma sort_client_le_spec l (xs : list Z) :
     {{{ l ↦ val_encode xs }}}
-      list_sort_client cmpZ #l
+      sort_client cmpZ #l
     {{{ ys, RET #(); ⌜Sorted (≤) ys⌝ ∗ ⌜ ys ≡ₚ xs⌝ ∗ l ↦ val_encode ys }}}.
   Proof.
     assert (∀ zs : list Z, val_encode zs = val_encode (LitV ∘ LitInt <$> zs)) as Henc.
     { intros zs. induction zs; f_equal/=; auto with f_equal. }
     iIntros (Φ) "Hl HΦ".
-    iApply (list_sort_client_spec N IZ (≤) _ _ (LitV ∘ LitInt <$> xs) xs with "[] [Hl] [HΦ]").
+    iApply (sort_client_spec N IZ (≤) _ _ (LitV ∘ LitInt <$> xs) xs with "[] [Hl] [HΦ]").
     { iApply cmpZ_spec. }
     { rewrite -Henc. iFrame "Hl".
       iInduction xs as [|x xs] "IH"; csimpl; first by iFrame.
@@ -30,4 +30,4 @@ Section list_sort_instances.
       by iDestruct ("IH" with "HI2") as %->. }
     rewrite -Henc. iApply ("HΦ" $! ys with "[$]").
   Qed.
-End list_sort_instances.
+End sort_client.
diff --git a/theories/examples/list_sort_elem.v b/theories/examples/sort_elem.v
similarity index 65%
rename from theories/examples/list_sort_elem.v
rename to theories/examples/sort_elem.v
index 1393810..6d4733a 100644
--- a/theories/examples/list_sort_elem.v
+++ b/theories/examples/sort_elem.v
@@ -7,25 +7,25 @@ From osiris.utils Require Import list compare.
 Definition cont := true.
 Definition stop := false.
 
-Definition list_sort_elem_service_split : val :=
+Definition sort_elem_service_split : val :=
   rec: "go" "c" "c1" "c2" :=
     if: ~(recv "c") then send "c1" #stop;; send "c2" #stop else
     let: "x" := recv "c" in
     send "c1" #cont;; send "c1" "x";;
     "go" "c" "c2" "c1".
 
-Definition list_sort_elem_service_move : val :=
+Definition sort_elem_service_move : val :=
   rec: "go" "c" "cin" :=
     if: ~(recv "cin") then send "c" #stop else
     let: "x" := recv "cin" in
     send "c" #cont;; send "c" "x";;
     "go" "c" "cin".
 
-Definition list_sort_elem_service_merge : val :=
+Definition sort_elem_service_merge : val :=
   rec: "go" "cmp" "c" "x1" "c1" "c2" :=
     if: ~recv "c2" then
       send "c" #cont;; send "c" "x1";;
-      list_sort_elem_service_move "c" "c1"
+      sort_elem_service_move "c" "c1"
     else
       let: "x2" := recv "c2" in
       if: "cmp" "x1" "x2" then
@@ -33,7 +33,7 @@ Definition list_sort_elem_service_merge : val :=
       else
         send "c" #cont;; send "c" "x2";; "go" "cmp" "c" "x1" "c1" "c2".
 
-Definition list_sort_elem_service : val :=
+Definition sort_elem_service : val :=
   rec: "go" "cmp" "c" :=
     if: ~(recv "c") then send "c" #stop else
     let: "x" := recv "c" in
@@ -45,59 +45,65 @@ Definition list_sort_elem_service : val :=
     let: "c2" := Fst "cc2" in let: "c2'" := Snd "cc2" in
     send "c1" #cont;; send "c1" "x";;
     send "c2" #cont;; send "c2" "y";;
-    list_sort_elem_service_split "c" "c1" "c2";;
+    sort_elem_service_split "c" "c1" "c2";;
     Fork ("go" "cmp" "c1'");; Fork ("go" "cmp" "c2'");;
     let: "x" := (if: recv "c1" then recv "c1" else assert #false) in
-    list_sort_elem_service_merge "cmp" "c" "x" "c1" "c2".
+    sort_elem_service_merge "cmp" "c" "x" "c1" "c2".
 
-Definition list_sort_elem_service_top : val := λ: "c",
+Definition sort_elem_service_top : val := λ: "c",
   let: "cmp" := recv "c" in
-  list_sort_elem_service "cmp" "c".
+  sort_elem_service "cmp" "c".
 
-Section list_sort_elem.
+Section sort_elem.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
 
-  Section list_sort_elem_inner.
+  Section sort_elem_inner.
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
 
-  Definition tail_protocol_aux (xs : list A)
+  Definition sort_elem_tail_protocol_aux (xs : list A)
       (rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ ys,
     ((<?> y v, MSG v {{ ⌜ TlRel R y ys ⌝ ∗ I y v }}; (rec : _ → iProto Σ) (ys ++ [y]))
      <&{⌜ ys ≡ₚ xs ⌝}> END)%proto.
 
-  Instance tail_protocol_aux_contractive xs : Contractive (tail_protocol_aux xs).
+  Instance sort_elem_tail_protocol_aux_contractive xs :
+    Contractive (sort_elem_tail_protocol_aux xs).
   Proof. solve_proto_contractive. Qed.
-  Definition tail_protocol (xs : list A) : list A → iProto Σ :=
-    fixpoint (tail_protocol_aux xs).
-  Global Instance tail_protocol_unfold xs ys :
-    ProtoUnfold (tail_protocol xs ys) (tail_protocol_aux xs (tail_protocol xs) ys).
-  Proof. apply proto_unfold_eq, (fixpoint_unfold (tail_protocol_aux _)). Qed.
-
-  Definition head_protocol_aux
+  Definition sort_elem_tail_protocol (xs : list A) : list A → iProto Σ :=
+    fixpoint (sort_elem_tail_protocol_aux xs).
+  Global Instance sort_elem_tail_protocol_unfold xs ys :
+    ProtoUnfold (sort_elem_tail_protocol xs ys)
+      (sort_elem_tail_protocol_aux xs (sort_elem_tail_protocol xs) ys).
+  Proof. apply proto_unfold_eq, (fixpoint_unfold (sort_elem_tail_protocol_aux _)). Qed.
+
+  Definition sort_elem_head_protocol_aux
       (rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ xs,
     ((<!> x v, MSG v {{ I x v }}; (rec : _ → iProto Σ) (xs ++ [x]))
-     <+> tail_protocol xs [])%proto.
+     <+> sort_elem_tail_protocol xs [])%proto.
 
-  Instance head_protocol_aux_contractive : Contractive head_protocol_aux.
+  Instance sort_elem_head_protocol_aux_contractive :
+    Contractive sort_elem_head_protocol_aux.
   Proof. solve_proto_contractive. Qed.
 
-  Definition head_protocol : list A → iProto Σ := fixpoint head_protocol_aux.
-  Global Instance head_protocol_unfold xs :
-    ProtoUnfold (head_protocol xs) (head_protocol_aux head_protocol xs) | 100.
-  Proof. apply proto_unfold_eq, (fixpoint_unfold head_protocol_aux). Qed.
+  Definition sort_elem_head_protocol : list A → iProto Σ :=
+    fixpoint sort_elem_head_protocol_aux.
+  Global Instance sort_elem_head_protocol_unfold xs :
+    ProtoUnfold (sort_elem_head_protocol xs)
+      (sort_elem_head_protocol_aux sort_elem_head_protocol xs).
+  Proof. apply proto_unfold_eq, (fixpoint_unfold sort_elem_head_protocol_aux). Qed.
 
-  Definition list_sort_elem_protocol : iProto Σ := head_protocol [].
+  Definition sort_elem_protocol : iProto Σ := sort_elem_head_protocol [].
 
-  Lemma list_sort_elem_service_split_spec c p c1 c2 xs xs1 xs2 :
+  Lemma sort_elem_service_split_spec c p c1 c2 xs xs1 xs2 :
     {{{
-      c ↣ iProto_dual (head_protocol xs) <++> p @ N ∗
-      c1 ↣ head_protocol xs1 @ N ∗ c2 ↣ head_protocol xs2 @ N
+      c ↣ iProto_dual (sort_elem_head_protocol xs) <++> p @ N ∗
+      c1 ↣ sort_elem_head_protocol xs1 @ N ∗ c2 ↣ sort_elem_head_protocol xs2 @ N
     }}}
-      list_sort_elem_service_split c c1 c2
+      sort_elem_service_split c c1 c2
     {{{ xs' xs1' xs2', RET #();
       ⌜xs' ≡ₚ xs1' ++ xs2'⌝ ∗
-      c ↣ iProto_dual (tail_protocol (xs ++ xs') []) <++> p @ N ∗
-      c1 ↣ tail_protocol (xs1 ++ xs1') [] @ N ∗ c2 ↣ tail_protocol (xs2 ++ xs2') [] @ N
+      c ↣ iProto_dual (sort_elem_tail_protocol (xs ++ xs') []) <++> p @ N ∗
+      c1 ↣ sort_elem_tail_protocol (xs1 ++ xs1') [] @ N ∗
+      c2 ↣ sort_elem_tail_protocol (xs2 ++ xs2') [] @ N
     }}}.
   Proof.
     iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
@@ -111,16 +117,16 @@ Section list_sort_elem.
       iApply ("HΨ" $! [] [] []). rewrite !right_id_L. by iFrame.
   Qed.
 
-  Lemma list_sort_elem_service_move_spec c p cin xs ys zs xs' ys' :
+  Lemma sort_elem_service_move_spec c p cin xs ys zs xs' ys' :
     xs ≡ₚ xs' ++ zs →
     ys ≡ₚ ys' ++ zs →
     Sorted R ys →
     (∀ x, TlRel R x ys' → TlRel R x ys) →
     {{{
-      c ↣ iProto_dual (tail_protocol xs ys) <++> p @ N ∗
-      cin ↣ tail_protocol xs' ys' @ N
+      c ↣ iProto_dual (sort_elem_tail_protocol xs ys) <++> p @ N ∗
+      cin ↣ sort_elem_tail_protocol xs' ys' @ N
     }}}
-      list_sort_elem_service_move c cin
+      sort_elem_service_move c cin
     {{{ RET #(); c ↣ p @ N ∗ cin ↣ END @ N }}}.
   Proof.
     iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
@@ -139,7 +145,7 @@ Section list_sort_elem.
       iApply "HΨ". iFrame.
   Qed.
 
-  Lemma list_sort_elem_service_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
+  Lemma sort_elem_service_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
     xs ≡ₚ xs1 ++ xs2 →
     ys ≡ₚ ys1 ++ ys2 →
     Sorted R ys →
@@ -147,11 +153,12 @@ Section list_sort_elem.
     (∀ x, TlRel R x ys2 → R x y1 → TlRel R x ys) →
     cmp_spec I R cmp -∗
     {{{
-      c ↣ iProto_dual (tail_protocol xs ys) <++> p @ N ∗
-      c1 ↣ tail_protocol xs1 (ys1 ++ [y1]) @ N ∗ c2 ↣ tail_protocol xs2 ys2 @ N ∗
+      c ↣ iProto_dual (sort_elem_tail_protocol xs ys) <++> p @ N ∗
+      c1 ↣ sort_elem_tail_protocol xs1 (ys1 ++ [y1]) @ N ∗
+      c2 ↣ sort_elem_tail_protocol xs2 ys2 @ N ∗
       I y1 w1
     }}}
-      list_sort_elem_service_merge cmp c w1 c1 c2
+      sort_elem_service_merge cmp c w1 c1 c2
     {{{ RET #(); c ↣ p @ N }}}.
   Proof.
     iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
@@ -178,7 +185,7 @@ Section list_sort_elem.
         * intros x'.
           inversion 1; discriminate_list || simplify_list_eq. by constructor.
     - wp_select. wp_send with "[$HIy1 //]".
-      wp_apply (list_sort_elem_service_move_spec with "[$Hc $Hc1]").
+      wp_apply (sort_elem_service_move_spec with "[$Hc $Hc1]").
       * done.
       * by rewrite Hys Hys2 -!assoc_L (comm _ xs2).
       * by apply Sorted_snoc.
@@ -187,10 +194,10 @@ Section list_sort_elem.
       * iIntros "[Hc Hc1]". iApply "HΨ". iFrame.
   Qed.
 
-  Lemma list_sort_elem_service_spec cmp c p :
+  Lemma sort_elem_service_spec cmp c p :
     cmp_spec I R cmp -∗
-    {{{ c ↣ iProto_dual list_sort_elem_protocol <++> p @ N }}}
-      list_sort_elem_service cmp c
+    {{{ c ↣ iProto_dual sort_elem_protocol <++> p @ N }}}
+      sort_elem_service cmp c
     {{{ RET #(); c ↣ p @ N }}}.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c p Ψ).
@@ -199,12 +206,12 @@ Section list_sort_elem.
       + wp_recv (x2 v2) as "HIx2".
         wp_apply (new_chan_proto_spec N with "[//]"); iIntros (cy1 cy2) "Hcy".
         wp_apply (new_chan_proto_spec N with "[//]"); iIntros (cz1 cz2) "Hcz".
-        iMod ("Hcy" $! (list_sort_elem_protocol <++> END)%proto) as "[Hcy1 Hcy2]".
-        iMod ("Hcz" $! (list_sort_elem_protocol <++> END)%proto) as "[Hcz1 Hcz2]".
+        iMod ("Hcy" $! (sort_elem_protocol <++> END)%proto) as "[Hcy1 Hcy2]".
+        iMod ("Hcz" $! (sort_elem_protocol <++> END)%proto) as "[Hcz1 Hcz2]".
         iEval (rewrite right_id) in "Hcy1 Hcz1".
         wp_select. wp_send with "[$HIx1]".
         wp_select. wp_send with "[$HIx2]".
-        wp_apply (list_sort_elem_service_split_spec with "[$Hc $Hcy1 $Hcz1]").
+        wp_apply (sort_elem_service_split_spec with "[$Hc $Hcy1 $Hcz1]").
         iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
         wp_apply (wp_fork with "[Hcy2]").
         { iNext. wp_apply ("IH" with "Hcy2"); auto. }
@@ -212,28 +219,28 @@ Section list_sort_elem.
         { iNext. wp_apply ("IH" with "Hcz2"); auto. }
         wp_branch as %_ | %[]%Permutation_nil_cons.
         wp_recv (x v) as "[_ HIx]".
-        wp_apply (list_sort_elem_service_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
+        wp_apply (sort_elem_service_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
           with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
         by rewrite Hxs' Permutation_middle.
       + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
         wp_select. by iApply "HΨ".
     - wp_select. by iApply "HΨ".
   Qed.
-  End list_sort_elem_inner.
+  End sort_elem_inner.
 
-  Definition list_sort_elem_top_protocol : iProto Σ :=
+  Definition sort_elem_top_protocol : iProto Σ :=
     (<!> A (I : A → val → iProp Σ) (R : A → A → Prop)
          `{!RelDecision R, !Total R} (cmp : val),
        MSG cmp {{ cmp_spec I R cmp }};
-     head_protocol I R [])%proto.
+     sort_elem_head_protocol I R [])%proto.
 
-  Lemma list_sort_elem_service_top_spec c p :
-    {{{ c ↣ iProto_dual list_sort_elem_top_protocol <++> p @ N }}}
-      list_sort_elem_service_top c
+  Lemma sort_elem_service_top_spec c p :
+    {{{ c ↣ iProto_dual sort_elem_top_protocol <++> p @ N }}}
+      sort_elem_service_top c
     {{{ RET #(); c ↣ p @ N }}}.
   Proof.
     iIntros (Ψ) "Hc HΨ". wp_lam.
-    wp_recv (? I R ? ? cmp) as "#Hcmp".
-    by wp_apply (list_sort_elem_service_spec with "Hcmp Hc").
+    wp_recv (A I R ? ? cmp) as "#Hcmp".
+    by wp_apply (sort_elem_service_spec with "Hcmp Hc").
   Qed.
-End list_sort_elem.
+End sort_elem.
diff --git a/theories/examples/list_sort_elem_client.v b/theories/examples/sort_elem_client.v
similarity index 78%
rename from theories/examples/list_sort_elem_client.v
rename to theories/examples/sort_elem_client.v
index e515e6f..28f384c 100644
--- a/theories/examples/list_sort_elem_client.v
+++ b/theories/examples/sort_elem_client.v
@@ -3,7 +3,7 @@ From osiris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
 From osiris.utils Require Import list compare.
-From osiris.examples Require Import list_sort_elem.
+From osiris.examples Require Import sort_elem.
 
 Definition send_all : val :=
   rec: "go" "c" "xs" :=
@@ -18,21 +18,21 @@ Definition recv_all : val :=
     then let: "x" := recv "c" in lcons "x" ("go" "c")
     else lnil #().
 
-Definition list_sort_elem_client : val :=
+Definition sort_elem_client : val :=
   λ: "cmp" "xs",
-    let: "c" := start_chan list_sort_elem_service_top in
+    let: "c" := start_chan sort_elem_service_top in
     send "c" "cmp";;
     send_all "c" "xs";;
     recv_all "c".
 
-Section list_sort_elem_client.
+Section sort_elem_client.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
 
   Lemma send_all_spec c p xs' xs vs :
-    {{{ c ↣ head_protocol I R xs' <++> p @ N ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
+    {{{ c ↣ sort_elem_head_protocol I R xs' <++> p @ N ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
       send_all c (val_encode vs)
-    {{{ RET #(); c ↣ tail_protocol I R (xs' ++ xs) [] <++> p @ N }}}.
+    {{{ RET #(); c ↣ sort_elem_tail_protocol I R (xs' ++ xs) [] <++> p @ N }}}.
   Proof.
     iIntros (Φ) "[Hc HI] HΦ".
     iInduction xs as [|x xs] "IH" forall (xs' vs); destruct vs as [|v vs]=>//.
@@ -44,7 +44,7 @@ Section list_sort_elem_client.
 
   Lemma recv_all_spec c p xs ys' :
     Sorted R ys' →
-    {{{ c ↣ tail_protocol I R xs ys' <++> p @ N }}}
+    {{{ c ↣ sort_elem_tail_protocol I R xs ys' <++> p @ N }}}
       recv_all c
     {{{ ys ws, RET (val_encode ws);
         ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗
@@ -63,22 +63,22 @@ Section list_sort_elem_client.
       iApply ("HΦ" $! [] []); rewrite /= right_id_L; by iFrame.
   Qed.
 
-  Lemma list_sort_client_spec cmp vs xs :
+  Lemma sort_client_spec cmp vs xs :
     cmp_spec I R cmp -∗
     {{{ [∗ list] x;v ∈ xs;vs, I x v }}}
-      list_sort_elem_client cmp (val_encode vs)
+      sort_elem_client cmp (val_encode vs)
     {{{ ys ws, RET (val_encode ws); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗
                [∗ list] y;w ∈ ys;ws, I y w }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "HI HΦ". wp_lam.
-    wp_apply (start_chan_proto_spec N (list_sort_elem_top_protocol <++> END)%proto);
+    wp_apply (start_chan_proto_spec N (sort_elem_top_protocol <++> END)%proto);
       iIntros (c) "Hc".
-    { wp_apply (list_sort_elem_service_top_spec N with "Hc"); auto. }
-    rewrite /list_sort_elem_top_protocol.
+    { wp_apply (sort_elem_service_top_spec N with "Hc"); auto. }
+    rewrite /sort_elem_top_protocol.
     wp_send (A I R) with "[$Hcmp]".
     wp_apply (send_all_spec with "[$HI $Hc]"); iIntros "Hc".
     wp_apply (recv_all_spec _ _ _ [] with "[$Hc]"); auto.
     iIntros (ys ws) "/=". iDestruct 1 as (??) "[_ HI]".
     iApply "HΦ"; auto.
   Qed.
-End list_sort_elem_client.
+End sort_elem_client.
-- 
GitLab