.gitlab-ci.yml

@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.15.1:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.1"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
     OPAM_PKG: "1"
   tags:
@@ -42,7 +42,7 @@ trigger-iris.dev:
   variables:
     STDPP_REPO: "iris/stdpp"
     IRIS_REPO: "iris/iris"
-    OPAM_PINS: "coq version 8.15.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version $NIGHTLY_COQ   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   except:
   only:
   - triggers

README.md

@@ -10,7 +10,7 @@ the paper
 
 It has been built and tested with the following dependencies
 
- - Coq 8.15.1
+ - Coq 8.18.0
  - The version of Iris in the [opam file](opam)
 
 In order to build, install the above dependencies and then run
@@ -37,7 +37,7 @@ The individual types contain the following:
   bidirectional channels in terms of Iris's HeapLang language, with specifications
   defined in terms of the dependent separation protocols.
   The relevant definitions and proof rules are as follows:
-  + `iProto_mapsto`: endpoint ownership (notation `↣`).
+  + `iProto_pointsto`: endpoint ownership (notation `↣`).
   + `new_chan_spec`, `send_spec` and `recv_spec`: proof rule for `new_chan`,
 	`send`, and `recv`.
   + `select_spec` and `branch_spec`: proof rule for the derived (binary)

_CoqProject

--Q theories actris
+-Q actris actris
+-Q multris multris
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
-# Coq emits warnings when a custom entry is reimported, this is too noisy.
--arg -w -arg -custom-entry-overriden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
+-arg -w -arg -notation-incompatible-prefix
+# No common logical root, so we have to specify documentation root, to avoid warnings
+-docroot actris
 
-theories/utils/skip.v
-theories/utils/llist.v
-theories/utils/compare.v
-theories/utils/contribution.v
-theories/utils/group.v
-theories/utils/cofe_solver_2.v
-theories/utils/switch.v
-theories/channel/proto_model.v
-theories/channel/proto.v
-theories/channel/channel.v
-theories/channel/proofmode.v
-theories/examples/basics.v
-theories/examples/equivalence.v
-theories/examples/sort.v
-theories/examples/sort_br_del.v
-theories/examples/sort_fg.v
-theories/examples/par_map.v
-theories/examples/map_reduce.v
-theories/examples/swap_mapper.v
-theories/examples/subprotocols.v
-theories/examples/list_rev.v
-theories/examples/rpc.v
-theories/examples/pizza.v
-theories/logrel/model.v
-theories/logrel/telescopes.v
-theories/logrel/subtyping.v
-theories/logrel/contexts.v
-theories/logrel/term_types.v
-theories/logrel/session_types.v
-theories/logrel/operators.v
-theories/logrel/term_typing_judgment.v
-theories/logrel/subtyping_rules.v
-theories/logrel/term_typing_rules.v
-theories/logrel/session_typing_rules.v
-theories/logrel/napp.v
-theories/logrel/lib/mutex.v
-theories/logrel/lib/list.v
-theories/logrel/lib/par_start.v
-theories/logrel/examples/pair.v
-theories/logrel/examples/par_recv.v
-theories/logrel/examples/rec_subtyping.v
-theories/logrel/examples/choice_subtyping.v
-theories/logrel/examples/mapper.v
-theories/logrel/examples/mapper_list.v
-theories/logrel/examples/compute_service.v
-theories/logrel/examples/compute_client_list.v
+actris/utils/llist.v
+actris/utils/compare.v
+actris/utils/contribution.v
+actris/utils/group.v
+actris/utils/cofe_solver_2.v
+actris/utils/switch.v
+actris/channel/proto_model.v
+actris/channel/proto.v
+actris/channel/channel.v
+actris/channel/proofmode.v
+actris/examples/basics.v
+actris/examples/equivalence.v
+actris/examples/sort.v
+actris/examples/sort_br_del.v
+actris/examples/sort_fg.v
+actris/examples/par_map.v
+actris/examples/map_reduce.v
+actris/examples/swap_mapper.v
+actris/examples/subprotocols.v
+actris/examples/list_rev.v
+actris/examples/rpc.v
+actris/examples/pizza.v
+actris/logrel/model.v
+actris/logrel/telescopes.v
+actris/logrel/subtyping.v
+actris/logrel/contexts.v
+actris/logrel/term_types.v
+actris/logrel/session_types.v
+actris/logrel/operators.v
+actris/logrel/term_typing_judgment.v
+actris/logrel/subtyping_rules.v
+actris/logrel/term_typing_rules.v
+actris/logrel/session_typing_rules.v
+actris/logrel/napp.v
+actris/logrel/lib/mutex.v
+actris/logrel/lib/list.v
+actris/logrel/lib/par_start.v
+actris/logrel/examples/pair.v
+actris/logrel/examples/par_recv.v
+actris/logrel/examples/rec_subtyping.v
+actris/logrel/examples/choice_subtyping.v
+actris/logrel/examples/mapper.v
+actris/logrel/examples/mapper_list.v
+actris/logrel/examples/compute_service.v
+actris/logrel/examples/compute_client_list.v
+
+multris/utils/cofe_solver_2.v
+multris/utils/matrix.v
+multris/channel/proto_model.v
+multris/channel/proto.v
+multris/channel/channel.v
+multris/channel/proofmode.v
+multris/examples/basics.v
+multris/examples/two_buyer.v
+multris/examples/three_buyer.v
+multris/examples/leader_election.v

theories/channel/channel.v → actris/channel/channel.v

@@ -25,9 +25,11 @@ From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Export proofmode.
 From iris.heap_lang.lib Require Import spin_lock.
 From actris.channel Require Export proto.
-From actris.utils Require Import llist skip.
+From actris.utils Require Import llist.
 Set Default Proof Using "Type".
 
+Local Existing Instance spin_lock.
+
 (** * The definition of the message-passing connectives *)
 Definition new_chan : val :=
   λ: <>,
@@ -36,7 +38,7 @@ Definition new_chan : val :=
      let: "lk" := newlock #() in
      ((("l","r"),"lk"), (("r","l"),"lk")).
 
-Definition start_chan : val := λ: "f",
+Definition fork_chan : val := λ: "f",
   let: "cc" := new_chan #() in
   Fork ("f" (Snd "cc"));; Fst "cc".
 
@@ -66,59 +68,50 @@ Definition recv : val :=
 
 (** * Setup of Iris's cameras *)
 Class chanG Σ := {
-  chanG_lockG :> lockG Σ;
-  chanG_protoG :> protoG Σ val;
+  #[local] chanG_lockG :: lockG Σ;
+  #[local] chanG_protoG :: protoG Σ val;
 }.
-Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
+Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
 Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
-Record chan_name := ChanName {
-  chan_lock_name : gname;
-  chan_proto_name : proto_name;
-}.
-Global Instance chan_name_inhabited : Inhabited chan_name :=
-  populate (ChanName inhabitant inhabitant).
-Global Instance chan_name_eq_dec : EqDecision chan_name.
-Proof. solve_decision. Qed.
-Global Instance chan_name_countable : Countable chan_name.
-Proof.
- refine (inj_countable (λ '(ChanName γl γr), (γl,γr))
-   (λ '(γl, γr), Some (ChanName γl γr)) _); by intros [].
-Qed.
-
-(** * Definition of the mapsto connective *)
+(** * Definition of the pointsto connective *)
 Notation iProto Σ := (iProto Σ val).
 Notation iMsg Σ := (iMsg Σ val).
 
-Definition iProto_mapsto_def `{!heapGS Σ, !chanG Σ}
+Definition iProto_lock_inv `{!heapGS Σ, !chanG Σ}
+    (l r : loc) (γl γr : gname) : iProp Σ :=
+  ∃ vsl vsr,
+    llist internal_eq l vsl ∗
+    llist internal_eq r vsr ∗
+    steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
+    iProto_ctx γl γr vsl vsr.
+
+Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
     (c : val) (p : iProto Σ) : iProp Σ :=
-  ∃ γ s (l r : loc) (lk : val),
-    ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
-    is_lock (chan_lock_name γ) lk (∃ vsl vsr,
-      llist internal_eq l vsl ∗
-      llist internal_eq r vsr ∗
-      steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
-      iProto_ctx (chan_proto_name γ) vsl vsr) ∗
-    iProto_own (chan_proto_name γ) s p.
-Definition iProto_mapsto_aux : seal (@iProto_mapsto_def). by eexists. Qed.
-Definition iProto_mapsto := iProto_mapsto_aux.(unseal).
-Definition iProto_mapsto_eq :
-  @iProto_mapsto = @iProto_mapsto_def := iProto_mapsto_aux.(seal_eq).
-Arguments iProto_mapsto {_ _ _} _ _%proto.
-Global Instance: Params (@iProto_mapsto) 4 := {}.
-Notation "c ↣ p" := (iProto_mapsto c p)
+  ∃ γl γr γlk (l r : loc) (lk : val),
+    ⌜ c = ((#l, #r), lk)%V ⌝ ∗
+    is_lock γlk lk (iProto_lock_inv l r γl γr) ∗
+    iProto_own γl p.
+
+Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
+Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
+Definition iProto_pointsto_eq :
+  @iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
+Arguments iProto_pointsto {_ _ _} _ _%_proto.
+Global Instance: Params (@iProto_pointsto) 4 := {}.
+Notation "c ↣ p" := (iProto_pointsto c p)
   (at level 20, format "c  ↣  p").
 
-Global Instance iProto_mapsto_contractive `{!heapGS Σ, !chanG Σ} c :
-  Contractive (iProto_mapsto c).
-Proof. rewrite iProto_mapsto_eq. solve_contractive. Qed.
+Global Instance iProto_pointsto_contractive `{!heapGS Σ, !chanG Σ} c :
+  Contractive (iProto_pointsto c).
+Proof. rewrite iProto_pointsto_eq. solve_contractive. Qed.
 
 Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
   (<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
 Global Typeclasses Opaque iProto_choice.
-Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
+Arguments iProto_choice {_} _ _%_I _%_I _%_proto _%_proto.
 Global Instance: Params (@iProto_choice) 2 := {}.
 Infix "<{ P1 }+{ P2 }>" := (iProto_choice Send P1 P2) (at level 85) : proto_scope.
 Infix "<{ P1 }&{ P2 }>" := (iProto_choice Recv P1 P2) (at level 85) : proto_scope.
@@ -134,15 +127,15 @@ Section channel.
   Implicit Types p : iProto Σ.
   Implicit Types TT : tele.
 
-  Global Instance iProto_mapsto_ne c : NonExpansive (iProto_mapsto c).
-  Proof. rewrite iProto_mapsto_eq. solve_proper. Qed.
-  Global Instance iProto_mapsto_proper c : Proper ((≡) ==> (≡)) (iProto_mapsto c).
+  Global Instance iProto_pointsto_ne c : NonExpansive (iProto_pointsto c).
+  Proof. rewrite iProto_pointsto_eq. solve_proper. Qed.
+  Global Instance iProto_pointsto_proper c : Proper ((≡) ==> (≡)) (iProto_pointsto c).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
+  Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
   Proof.
-    rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
-    iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+    rewrite iProto_pointsto_eq. iDestruct 1 as (γl γr γlk l r lk ->) "[Hlk H]".
+    iIntros "Hle'". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
     by iApply (iProto_own_le with "H").
   Qed.
 
@@ -198,33 +191,42 @@ Section channel.
       iDestruct ("H" with "HP") as "[$ ?]"; by iModIntro.
   Qed.
 
+  Lemma iProto_lock_inv_sym l r γl γr :
+    iProto_lock_inv l r γl γr ⊢ iProto_lock_inv r l γr γl.
+  Proof.
+    iIntros "(%vsl & %vsr & Hlistl & Hlistr & Hstepsl & Hstepsr & Hctx)".
+    iExists vsr, vsl. iFrame. by iApply iProto_ctx_sym.
+  Qed.
+
   (** ** Specifications of [send] and [recv] *)
   Lemma new_chan_spec p :
     {{{ True }}}
       new_chan #()
     {{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
   Proof.
-    iIntros (Φ _) "HΦ". wp_lam.
-    wp_bind (lnil _).
-    iApply wp_lb_init; iIntros "#Hlb".
+    iIntros (Φ _) "HΦ". wp_lam. iMod (steps_lb_0) as "#Hlb".
     wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
     wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
-    iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
+    iMod (iProto_init p) as (γl γr) "(Hctx & Hcl & Hcr)".
     wp_smart_apply (newlock_spec (∃ vsl vsr,
       llist internal_eq l vsl ∗ llist internal_eq r vsr ∗
       steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
-      iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
+      iProto_ctx γl γr vsl vsr) with "[Hl Hr Hctx]").
     { iExists [], []. iFrame "#∗". }
     iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
-    set (γ := ChanName γlk γp). iSplitL "Hcl".
-    - rewrite iProto_mapsto_eq. iExists γ, Left, l, r, lk. by iFrame "Hcl #".
-    - rewrite iProto_mapsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
+    iSplitL "Hcl".
+    - rewrite iProto_pointsto_eq.
+      iExists γl, γr, γlk, l, r, lk. by iFrame "Hcl #".
+    - rewrite iProto_pointsto_eq.
+      iExists γr, γl, γlk, r, l, lk. iFrame "Hcr #".
+      iModIntro. iSplit; first done. iApply (is_lock_iff with "Hlk").
+      iIntros "!> !>". iSplit; iIntros; by iApply iProto_lock_inv_sym.
   Qed.
 
-  Lemma start_chan_spec p Φ (f : val) :
+  Lemma fork_chan_spec p Φ (f : val) :
     ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
     ▷ (∀ c, c ↣ p -∗ Φ c) -∗
-    WP start_chan f {{ Φ }}.
+    WP fork_chan f {{ Φ }}.
   Proof.
     iIntros "Hfork HΦ". wp_lam.
     wp_smart_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
@@ -238,51 +240,30 @@ Section channel.
       send c v
     {{{ RET #(); c ↣ p }}}.
   Proof.
-    rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+    rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+    iDestruct "Hc" as (γl γr γlk l r lk ->) "[#Hlk H]"; wp_pures.
     wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
     iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
-    destruct s; simpl.
-    - wp_pures. wp_bind (lsnoc _ _).
-      iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
-      { iApply fupd_mask_intro; [set_solver|]. simpl.
-        iIntros "Hclose !>!>".
-        iMod (iProto_send_l with "Hctx H []") as "[Hctx H]".
-        { rewrite iMsg_base_eq /=; auto. }
-        iModIntro.
-        iApply step_fupdN_intro; [done|].
-        iIntros "!>". iMod "Hclose".
-        iCombine ("Hctx H") as "H".
-        iExact "H". }
-      iApply (wp_lb_update with "Hlbl").
-      wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
-      iIntros "#Hlbl' [Hctx H] !>".
-      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
-      { iExists (vsl ++ [v]), vsr.
-        rewrite app_length /=.
-        replace (length vsl + 1) with (S (length vsl)) by lia.
-        iFrame "#∗". }
-      iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
-    - wp_pures. wp_bind (lsnoc _ _).
-      iApply (wp_step_fupdN_lb with "Hlbl [Hctx H]"); [done| |].
-      { iApply fupd_mask_intro; [set_solver|]. simpl.
-        iIntros "Hclose !>!>".
-        iMod (iProto_send_r with "Hctx H []") as "[Hctx H]".
-        { rewrite iMsg_base_eq /=; auto. }
-        iModIntro.
-        iApply step_fupdN_intro; [done|].
-        iIntros "!>". iMod "Hclose".
-        iCombine ("Hctx H") as "H".
-        iExact "H". }
-      iApply (wp_lb_update with "Hlbr").
-      wp_smart_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
-      iIntros "#Hlbr' [Hctx H] !>".
-      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
-      { iExists vsl, (vsr ++ [v]).
-        rewrite app_length /=.
-        replace (length vsr + 1) with (S (length vsr)) by lia.
-        iFrame "#∗". }
-      iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
+    wp_pures. wp_bind (lsnoc _ _).
+    iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
+    { iApply fupd_mask_intro; [set_solver|]. simpl.
+      iIntros "Hclose !>!>".
+      iMod (iProto_send with "Hctx H []") as "[Hctx H]".
+      { rewrite iMsg_base_eq /=; auto. }
+      iModIntro.
+      iApply step_fupdN_intro; [done|].
+      iIntros "!>". iMod "Hclose".
+      iCombine ("Hctx H") as "H".
+      iExact "H". }
+    iApply (wp_lb_update with "Hlbl").
+    wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
+    iIntros "#Hlbl' [Hctx H] !>".
+    wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
+    { iExists (vsl ++ [v]), vsr.
+      rewrite length_app /=.
+      replace (length vsl + 1) with (S (length vsl)) by lia.
+      iFrame "#∗". }
+    iIntros "_". iApply "HΦ". iExists γl, γr, γlk. eauto 10 with iFrame.
   Qed.
 
   Lemma send_spec_tele {TT} c (tt : TT)
@@ -292,7 +273,7 @@ Section channel.
     {{{ RET #(); c ↣ (p tt) }}}.
   Proof.
     iIntros (Φ) "[Hc HP] HΦ".
-    iDestruct (iProto_mapsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
+    iDestruct (iProto_pointsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
       as "Hc".
     { iIntros "!>".
       iApply iProto_le_trans.
@@ -307,37 +288,26 @@ Section channel.
     {{{ w, RET w; (⌜w = NONEV⌝ ∗ c ↣ <?.. x> MSG v x {{ P x }}; p x) ∨
                   (∃.. x, ⌜w = SOMEV (v x)⌝ ∗ c ↣ p x ∗ P x) }}}.
   Proof.
-    rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+    rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+    iDestruct "Hc" as (γl γr γlk l r lk ->) "[#Hlk H]"; wp_pures.
     wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
-    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)". destruct s; simpl.
-    - wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
-      destruct vsr as [|vr vsr]; wp_pures.
-      { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-        iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
-        iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
-      wp_smart_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
-      iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
+    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
+    wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
+    destruct vsr as [|vr vsr]; wp_pures.
+    - wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
+      { unfold iProto_lock_inv; by eauto with iFrame. }
+      iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
+      iExists γl, γr, γlk. eauto 10 with iFrame.
+    - wp_smart_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
+      iMod (iProto_recv with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
       rewrite iMsg_base_eq.
       iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
       iDestruct (steps_lb_le _ (length vsr) with "Hlbr") as "#Hlbr'"; [lia|].
-      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
-      iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
-      by iRewrite "Hp".
-    - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
-      destruct vsl as [|vl vsl]; wp_pures.
-      { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-        iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
-        iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
-      wp_smart_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
-      iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
-      rewrite iMsg_base_eq.
-      iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
-      iDestruct (steps_lb_le _ (length vsl) with "Hlbl") as "#Hlbl'"; [lia|].
-      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
-      iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+      wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
+      { unfold iProto_lock_inv; by eauto with iFrame. }
+      iIntros "_". wp_pures. iModIntro. iApply "HΦ".
+      iRight. iExists x. iSplit; [done|].
+      iFrame "HP". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
       by iRewrite "Hp".
   Qed.
 
@@ -360,7 +330,7 @@ Section channel.
   Proof.
     rewrite /iProto_choice. iIntros (Φ) "[Hc HP] HΦ".
     iApply (send_spec with "[Hc HP] HΦ").
-    iApply (iProto_mapsto_le with "Hc").
+    iApply (iProto_pointsto_le with "Hc").
     iIntros "!>". iExists b. by iFrame "HP".
   Qed.
 
@@ -373,7 +343,7 @@ Section channel.
     iApply (recv_spec _ (tele_app _)
       (tele_app (TT:=[tele _ : bool]) (λ b, if b then P1 else P2))%I
       (tele_app _) with "[Hc]").
-    { iApply (iProto_mapsto_le with "Hc").
+    { iApply (iProto_pointsto_le with "Hc").
       iIntros "!> /=" (b) "HP". iExists b. by iSplitL. }
     rewrite -bi_tforall_forall.
     iIntros "!>" (x) "[Hc H]". iApply "HΦ". iFrame.

theories/channel/proofmode.v → actris/channel/proofmode.v

@@ -36,7 +36,7 @@ Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
     ⊢ iProto_dual_if d p <++>
         foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
 Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
-Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
+Arguments ProtoNormalize {_} _ _%_proto _%_proto _%_proto.
 
 Notation ProtoUnfold p1 p2 := (∀ d pas q,
   ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
@@ -46,7 +46,7 @@ Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
   msg_normalize a :
     ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
 Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
-Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
+Arguments MsgNormalize {_} _ _%_msg _%_msg _%_msg.
 
 Section classes.
   Context `{!chanG Σ, !heapGS Σ}.
@@ -164,21 +164,21 @@ Section classes.
 
   (** Automatically perform normalization of protocols in the proof mode when
   using [iAssumption] and [iFrame]. *)
-  Global Instance mapsto_proto_from_assumption q c p1 p2 :
+  Global Instance pointsto_proto_from_assumption q c p1 p2 :
     ProtoNormalize false p1 [] p2 →
     FromAssumption q (c ↣ p1) (c ↣ p2).
   Proof.
     rewrite /FromAssumption /ProtoNormalize /= right_id.
     rewrite bi.intuitionistically_if_elim.
-    iIntros (?) "H". by iApply (iProto_mapsto_le with "H").
+    iIntros (?) "H". by iApply (iProto_pointsto_le with "H").
   Qed.
-  Global Instance mapsto_proto_from_frame q c p1 p2 :
+  Global Instance pointsto_proto_from_frame q c p1 p2 :
     ProtoNormalize false p1 [] p2 →
     Frame q (c ↣ p1) (c ↣ p2) True.
   Proof.
     rewrite /Frame /ProtoNormalize /= right_id.
     rewrite bi.intuitionistically_if_elim.
-    iIntros (?) "[H _]". by iApply (iProto_mapsto_le with "H").
+    iIntros (?) "[H _]". by iApply (iProto_pointsto_le with "H").
   Qed.
 End classes.
 
@@ -203,20 +203,20 @@ Proof.
   intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl.
   assert (c ↣ p ⊢ c ↣ <?.. x>
     MSG tele_app tv x {{ ▷ tele_app tP' x }}; tele_app tp x) as ->.
-  { iIntros "Hc". iApply (iProto_mapsto_le with "Hc"). iIntros "!>".
+  { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"). iIntros "!>".
     iApply iProto_le_trans; [iApply Hp|rewrite Hm].
     iApply iProto_le_texist_elim_l; iIntros (x).
     iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ x)]; simpl.
     iIntros "H". by iDestruct (HP with "H") as "$". }
   rewrite -wp_bind. eapply bi.wand_apply;
-    [by eapply (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
+    [by eapply bi.wand_entails, (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
   rewrite -bi.later_intro; apply bi.forall_intro=> x.
   specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
 Qed.
 
 Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
     iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
   wp_pures;
@@ -226,10 +226,10 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
       |fail 1 "wp_recv: cannot find 'recv' in" e];
-    [solve_mapsto ()
-       |iSolveTC || fail 1 "wp_recv: protocol not of the shape <?>"
-    |iSolveTC || fail 1 "wp_recv: cannot convert to telescope"
-    |iSolveTC
+    [solve_pointsto ()
+       |tc_solve || fail 1 "wp_recv: protocol not of the shape <?>"
+    |tc_solve || fail 1 "wp_recv: cannot convert to telescope"
+    |tc_solve
     |pm_reduce; simpl; tac_intros;
      tac Hnew;
      wp_finish]
@@ -241,37 +241,9 @@ Tactic Notation "wp_recv" "as" constr(pat) :=
 
 Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" constr(pat) :=
   wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")"
-    constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
-    simple_intropattern(x5) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
-    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
-    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
-    constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
-    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
-    simple_intropattern(x8) ")" constr(pat) :=
-  wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as"
+    "(" ne_simple_intropattern_list(ys) ")" constr(pat) :=
+  wp_recv_core (intros xs) as (fun H => _iDestructHyp H ys pat).
 
 Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K c v p m tv tP tp Φ :
   envs_lookup i Δ = Some (false, c ↣ p)%I →
@@ -300,14 +272,14 @@ Proof.
   destruct HΦ as (-> & -> & ->). rewrite right_id assoc.
   assert (c ↣ p ⊢
     c ↣ <!.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->.
-  { iIntros "Hc". iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
+  { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"); iIntros "!>".
     iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. }
-  eapply bi.wand_apply; [rewrite -wp_bind; by eapply send_spec_tele|].
+  eapply bi.wand_apply; [rewrite -wp_bind; by eapply bi.wand_entails, send_spec_tele|].
   by rewrite -bi.later_intro.
 Qed.
 
 Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
     iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
   let solve_done d :=
@@ -327,9 +299,9 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
        first
          [reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
          |fail 1 "wp_send: cannot find 'send' in" e];
-       [solve_mapsto ()
-       |iSolveTC || fail 1 "wp_send: protocol not of the shape <!>"
-       |iSolveTC || fail 1 "wp_send: cannot convert to telescope"
+       [solve_pointsto ()
+       |tc_solve || fail 1 "wp_send: protocol not of the shape <!>"
+       |tc_solve || fail 1 "wp_send: cannot convert to telescope"
        |pm_reduce; simpl; tac_exist;
         repeat lazymatch goal with
         | |- ∃ _, _ => eexists _
@@ -347,31 +319,8 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
 
 Tactic Notation "wp_send" "with" constr(pat) :=
   wp_send_core (idtac) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) ")"
-    "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
-    "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4)
-    uconstr(x5) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
-    uconstr(x5) uconstr(x6) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
-                eexists x6) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
-    uconstr(x5) uconstr(x6) uconstr(x7) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
-                eexists x6; eexists x7) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
-    uconstr(x5) uconstr(x6) uconstr(x7) uconstr(x8) ")" "with" constr(pat) :=
-  wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
-                eexists x6; eexists x7; eexists x8) with pat.
+Tactic Notation "wp_send" "(" ne_uconstr_list(xs) ")" "with" constr(pat) :=
+  wp_send_core (ltac1_list_iter ltac:(fun x => eexists x) xs) with pat.
 
 Lemma tac_wp_branch `{!chanG Σ, !heapGS Σ} Δ i j K
     c p P1 P2 (p1 p2 : iProto Σ) Φ :
@@ -388,15 +337,15 @@ Lemma tac_wp_branch `{!chanG Σ, !heapGS Σ} Δ i j K
 Proof.
   rewrite envs_entails_unseal /ProtoNormalize /= right_id=> ? Hp HΦ.
   rewrite envs_lookup_sound //; simpl.
-  rewrite (iProto_mapsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
-  rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv; first done].
+  rewrite (iProto_pointsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply bi.wand_entails, branch_spec|f_equiv; first done].
   rewrite -bi.later_intro; apply bi.forall_intro=> b.
   specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
 Qed.
 
 Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
     iAssumptionCore || fail "wp_branch: cannot find" c "↣ ? @ ?" in
   wp_pures;
@@ -406,8 +355,8 @@ Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_branch _ _ Hnew K))
       |fail 1 "wp_branch: cannot find 'recv' in" e];
-    [solve_mapsto ()
-       |iSolveTC || fail 1 "wp_send: protocol not of the shape <&>"
+    [solve_pointsto ()
+       |tc_solve || fail 1 "wp_send: protocol not of the shape <&>"
     |pm_reduce; intros []; [tac1 Hnew|tac2 Hnew]; wp_finish]
   | _ => fail "wp_branch: not a 'wp'"
   end.
@@ -420,7 +369,7 @@ Tactic Notation "wp_branch" "as" constr(pat1) "|" "%" simple_intropattern(pat2)
   wp_branch_core as (fun H => iDestructHyp H as pat1) (fun H => iPure H as pat2).
 Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" "%" simple_intropattern(pat2) :=
   wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2). 
-Tactic Notation "wp_branch" := wp_branch as %_ | %_.
+Tactic Notation "wp_branch" := wp_branch as % _ | % _.
 
 Lemma tac_wp_select `{!chanG Σ, !heapGS Σ} Δ neg i js K
     c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
@@ -441,8 +390,8 @@ Lemma tac_wp_select `{!chanG Σ, !heapGS Σ} Δ neg i js K
 Proof.
   rewrite envs_entails_unseal /ProtoNormalize /= right_id=> ? Hp HΦ.
   rewrite envs_lookup_sound //; simpl.
-  rewrite (iProto_mapsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
-  rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
+  rewrite (iProto_pointsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply bi.wand_entails, select_spec|].
   rewrite -assoc; f_equiv; first done.
   destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
   destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
@@ -451,7 +400,7 @@ Proof.
 Qed.
 
 Tactic Notation "wp_select" "with" constr(pat) :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
     iAssumptionCore || fail "wp_select: cannot find" c "↣ ? @ ?" in
   let solve_done d :=
@@ -471,8 +420,8 @@ Tactic Notation "wp_select" "with" constr(pat) :=
        first
          [reshape_expr e ltac:(fun K e' => eapply (tac_wp_select _ neg _ Hs' K))
          |fail 1 "wp_select: cannot find 'send' in" e];
-       [solve_mapsto ()
-       |iSolveTC || fail 1 "wp_select: protocol not of the shape <+>"
+       [solve_pointsto ()
+       |tc_solve || fail 1 "wp_select: protocol not of the shape <+>"
        |pm_reduce;
         lazymatch goal with
         | |- False => fail "wp_select:" Hs' "not fresh"
@@ -484,3 +433,21 @@ Tactic Notation "wp_select" "with" constr(pat) :=
   end.
 
 Tactic Notation "wp_select" := wp_select with "[//]".
+
+Tactic Notation "wp_new_chan" constr(prot) "as"
+       "(" simple_intropattern(c1) simple_intropattern(c2) ")" constr(pat) :=
+  wp_smart_apply (new_chan_spec prot); [done|];
+  iIntros (c1); iIntros (c2); iIntros pat.
+
+Tactic Notation "wp_fork_chan" constr(prot) "as"
+       simple_intropattern(c1) constr(pat1) "and"
+       simple_intropattern(c2) constr(pat2) :=
+  wp_smart_apply (fork_chan_spec prot); [iIntros (c2); iIntros pat2|
+                                         iIntros (c1); iIntros pat1].
+
+Tactic Notation "wp_fork_chan" constr(prot) "as"
+       simple_intropattern(c) constr(pat) :=
+  wp_fork_chan prot as c pat and c pat.
+
+Tactic Notation "wp_fork_chan" constr(prot) :=
+  wp_fork_chan prot as ? "?".

theories/channel/proto.v → actris/channel/proto.v

@@ -54,10 +54,17 @@ From actris.channel Require Import proto_model.
 Set Default Proof Using "Type".
 Export action.
 
+(** * Types *)
+Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
+Declare Scope proto_scope.
+Delimit Scope proto_scope with proto.
+Bind Scope proto_scope with iProto.
+Open Scope proto.
+
 (** * Setup of Iris's cameras *)
 Class protoG Σ V :=
-  protoG_authG :>
-    inG Σ (excl_authR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))).
+  protoG_authG ::
+    inG Σ (excl_authR (laterO (iProto Σ V))).
 
 Definition protoΣ V := #[
   GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
@@ -65,13 +72,6 @@ Definition protoΣ V := #[
 Global Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
 Proof. solve_inG. Qed.
 
-(** * Types *)
-Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
-Declare Scope proto_scope.
-Delimit Scope proto_scope with proto.
-Bind Scope proto_scope with iProto.
-Local Open Scope proto.
-
 (** * Messages *)
 Section iMsg.
   Set Primitive Projections.
@@ -108,7 +108,7 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
 Definition iMsg_base := iMsg_base_aux.(unseal).
 Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
-Arguments iMsg_base {_ _} _%V _%I _%proto.
+Arguments iMsg_base {_ _} _%_V _%_I _%_proto.
 Global Instance: Params (@iMsg_base) 3 := {}.
 
 Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
@@ -117,12 +117,12 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
 Definition iMsg_exist := iMsg_exist_aux.(unseal).
 Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
-Arguments iMsg_exist {_ _ _} _%msg.
+Arguments iMsg_exist {_ _ _} _%_msg.
 Global Instance: Params (@iMsg_exist) 3 := {}.
 
 Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
   tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
-Arguments iMsg_texist {_ _ !_} _%msg /.
+Arguments iMsg_texist {_ _ !_} _%_msg /.
 
 Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
   (at level 200, v at level 20, right associativity,
@@ -157,7 +157,7 @@ Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
 Definition iProto_message := iProto_message_aux.(unseal).
 Definition iProto_message_eq :
   @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
-Arguments iProto_message {_ _} _ _%msg.
+Arguments iProto_message {_ _} _ _%_msg.
 Global Instance: Params (@iProto_message) 3 := {}.
 
 Notation "'END'" := iProto_end : proto_scope.
@@ -225,7 +225,7 @@ Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
 Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
 Definition iProto_app := iProto_app_aux.(unseal).
 Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
-Arguments iProto_app {_ _} _%proto _%proto.
+Arguments iProto_app {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_app) 2 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
@@ -236,13 +236,13 @@ Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
 Definition iProto_dual := iProto_dual_aux.(unseal).
 Definition iProto_dual_eq :
   @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
-Arguments iProto_dual {_ _} _%proto.
+Arguments iProto_dual {_ _} _%_proto.
 Global Instance: Params (@iProto_dual) 2 := {}.
 Notation iMsg_dual := (iMsg_map iProto_dual).
 
 Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
   if d then iProto_dual p else p.
-Arguments iProto_dual_if {_ _} _ _%proto.
+Arguments iProto_dual_if {_ _} _ _%_proto.
 Global Instance: Params (@iProto_dual_if) 3 := {}.
 
 (** * Protocol entailment *)
@@ -277,7 +277,7 @@ Proof.
 Qed.
 Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
   fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_ _} _%proto _%proto.
+Arguments iProto_le {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_le) 2 := {}.
 Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
 
@@ -294,52 +294,33 @@ Fixpoint iProto_app_recvs {Σ V} (vs : list V) (p : iProto Σ V) : iProto Σ V :
 Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
   ∃ p, iProto_app_recvs vsr p ⊑ pl ∗ iProto_app_recvs vsl (iProto_dual p) ⊑ pr.
 
-Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
-Global Instance proto_name_inhabited : Inhabited proto_name :=
-  populate (ProtName inhabitant inhabitant).
-Global Instance proto_name_eq_dec : EqDecision proto_name.
-Proof. solve_decision. Qed.
-Global Instance proto_name_countable : Countable proto_name.
-Proof.
- refine (inj_countable (λ '(ProtName γl γr), (γl,γr))
-   (λ '(γl, γr), Some (ProtName γl γr)) _); by intros [].
-Qed.
-
-Inductive side := Left | Right.
-Global Instance side_inhabited : Inhabited side := populate Left.
-Global Instance side_eq_dec : EqDecision side.
-Proof. solve_decision. Qed.
-Global Instance side_countable : Countable side.
-Proof.
- refine (inj_countable (λ s, if s is Left then true else false)
-   (λ b, Some (if b then Left else Right)) _); by intros [].
-Qed.
-Definition side_elim {A} (s : side) (l r : A) : A :=
-  match s with Left => l | Right => r end.
-
-Definition iProto_own_frag `{!protoG Σ V} (γ : proto_name) (s : side)
+Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
     (p : iProto Σ V) : iProp Σ :=
-  own (side_elim s proto_l_name proto_r_name γ) (◯E (Next p)).
-Definition iProto_own_auth `{!protoG Σ V} (γ : proto_name) (s : side)
+  own γ (◯E (Next p)).
+Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
     (p : iProto Σ V) : iProp Σ :=
-  own (side_elim s proto_l_name proto_r_name γ) (●E (Next p)).
+  own γ (●E (Next p)).
 
+(** In the original Actris papers we a single ghost name for [iProto_ctx] and
+[iProto_own]. To distinguish the two [iProto_own]s for both sides, we used
+an enum [Left]/[Right]. This turned out to be cumbersome because at various
+places we need to case at this enum. The current version of [iProto_ctx] has two
+ghost names, one for each [iProto_own], enabling more uniform definitions. *)
 Definition iProto_ctx `{protoG Σ V}
-    (γ : proto_name) (vsl vsr : list V) : iProp Σ :=
+    (γl γr : gname) (vsl vsr : list V) : iProp Σ :=
   ∃ pl pr,
-    iProto_own_auth γ Left pl ∗
-    iProto_own_auth γ Right pr ∗
+    iProto_own_auth γl pl ∗
+    iProto_own_auth γr pr ∗
     ▷ iProto_interp vsl vsr pl pr.
 
 (** * The connective for ownership of channel ends *)
-Definition iProto_own `{!protoG Σ V}
-    (γ : proto_name) (s : side) (p : iProto Σ V) : iProp Σ :=
-  ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ s p'.
-Arguments iProto_own {_ _ _} _ _%proto.
-Global Instance: Params (@iProto_own) 3 := {}.
-
-Global Instance iProto_own_contractive `{protoG Σ V} γ s :
-  Contractive (iProto_own γ s).
+Definition iProto_own `{!protoG Σ V} (γ : gname) (p : iProto Σ V) : iProp Σ :=
+  ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ p'.
+Arguments iProto_own {_ _ _} _ _%_proto.
+Global Instance: Params (@iProto_own) 4 := {}.
+
+Global Instance iProto_own_contractive `{protoG Σ V} γ :
+  Contractive (iProto_own γ).
 Proof. solve_contractive. Qed.
 
 (** * Proofs *)
@@ -751,7 +732,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_payload_elim_l a m v P p :
-    (P -∗ (<?> MSG v; p) ⊑ (<a> m)) -∗
+    (P -∗ (<?> MSG v; p) ⊑ (<a> m)) ⊢
     (<?> MSG v {{ P }}; p) ⊑ (<a> m).
   Proof.
     rewrite iMsg_base_eq. iIntros "H". destruct a.
@@ -761,7 +742,7 @@ Section proto.
       iApply (iProto_le_recv_recv_inv with "(H HP)"); simpl; auto.
   Qed.
   Lemma iProto_le_payload_elim_r a m v P p :
-    (P -∗ (<a> m) ⊑ (<!> MSG v; p)) -∗
+    (P -∗ (<a> m) ⊑ (<!> MSG v; p)) ⊢
     (<a> m) ⊑ (<!> MSG v {{ P }}; p).
   Proof.
     rewrite iMsg_base_eq. iIntros "H". destruct a.
@@ -786,7 +767,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_exist_elim_l {A} (m1 : A → iMsg Σ V) a m2 :
-    (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗
+    (∀ x, (<?> m1 x) ⊑ (<a> m2)) ⊢
     (<? x> m1 x) ⊑ (<a> m2).
   Proof.
     rewrite iMsg_exist_eq. iIntros "H". destruct a.
@@ -798,7 +779,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_exist_elim_l_inhabited `{!Inhabited A} (m : A → iMsg Σ V) p :
-    (∀ x, (<?> m x) ⊑ p) -∗
+    (∀ x, (<?> m x) ⊑ p) ⊢
     (<? x> m x) ⊑ p.
   Proof.
     rewrite iMsg_exist_eq. iIntros "H".
@@ -819,7 +800,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_exist_elim_r {A} a m1 (m2 : A → iMsg Σ V) :
-    (∀ x, (<a> m1) ⊑ (<!> m2 x)) -∗
+    (∀ x, (<a> m1) ⊑ (<!> m2 x)) ⊢
     (<a> m1) ⊑ (<! x> m2 x).
   Proof.
     rewrite iMsg_exist_eq. iIntros "H". destruct a.
@@ -830,7 +811,7 @@ Section proto.
       iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
   Qed.
   Lemma iProto_le_exist_elim_r_inhabited `{Hinh : Inhabited A} p (m : A → iMsg Σ V) :
-    (∀ x, p ⊑ (<!> m x)) -∗
+    (∀ x, p ⊑ (<!> m x)) ⊢
     p ⊑ (<! x> m x).
   Proof.
     rewrite iMsg_exist_eq. iIntros "H".
@@ -863,7 +844,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_texist_elim_l {TT : tele} (m1 : TT → iMsg Σ V) a m2 :
-    (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗
+    (∀ x, (<?> m1 x) ⊑ (<a> m2)) ⊢
     (<?.. x> m1 x) ⊑ (<a> m2).
   Proof.
     iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
@@ -895,7 +876,7 @@ Section proto.
   Qed.
 
   Lemma iProto_le_base a v P p1 p2 :
-    ▷ (p1 ⊑ p2) -∗
+    ▷ (p1 ⊑ p2) ⊢
     (<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
   Proof.
     rewrite iMsg_base_eq. iIntros "H". destruct a.
@@ -948,7 +929,7 @@ Section proto.
 
   Lemma iProto_le_amber_internal (p1 p2 : iProto Σ V → iProto Σ V)
       `{Contractive p1, Contractive p2}:
-    □ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) -∗
+    □ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) ⊢
     fixpoint p1 ⊑ fixpoint p2.
   Proof.
     iIntros "#H". iLöb as "IH".
@@ -968,12 +949,12 @@ Section proto.
     - apply bi.limit_preserving_entails; [done|solve_proper].
   Qed.
 
-  Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 -∗ iProto_dual p1 ⊑ p2.
+  Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 ⊢ iProto_dual p1 ⊑ p2.
   Proof.
     iIntros "H". iEval (rewrite -(involutive iProto_dual p2)).
     by iApply iProto_le_dual.
   Qed.
-  Lemma iProto_le_dual_r p1 p2 : p2 ⊑ iProto_dual p1 -∗ p1 ⊑ iProto_dual p2.
+  Lemma iProto_le_dual_r p1 p2 : p2 ⊑ iProto_dual p1 ⊢ p1 ⊑ iProto_dual p2.
   Proof.
     iIntros "H". iEval (rewrite -(involutive iProto_dual p1)).
     by iApply iProto_le_dual.
@@ -1026,20 +1007,20 @@ Section proto.
     Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
   Proof. apply (ne_proper_2 _). Qed.
 
-  Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
+  Global Instance iProto_own_frag_ne γ : NonExpansive (iProto_own_frag γ).
   Proof. solve_proper. Qed.
 
-  Lemma iProto_own_auth_agree γ s p p' :
-    iProto_own_auth γ s p -∗ iProto_own_frag γ s p' -∗ ▷ (p ≡ p').
+  Lemma iProto_own_auth_agree γ p p' :
+    iProto_own_auth γ p -∗ iProto_own_frag γ p' -∗ ▷ (p ≡ p').
   Proof.
-    iIntros "H● H◯". iDestruct (own_valid_2 with "H● H◯") as "H✓".
-    iDestruct (excl_auth_agreeI with "H✓") as "H✓".
+    iIntros "H● H◯". iCombine "H● H◯" gives "H✓".
+    iDestruct (excl_auth_agreeI with "H✓") as "{H✓} H✓".
     iApply (later_equivI_1 with "H✓").
   Qed.
 
-  Lemma iProto_own_auth_update γ s p p' p'' :
-    iProto_own_auth γ s p -∗ iProto_own_frag γ s p' ==∗
-    iProto_own_auth γ s p'' ∗ iProto_own_frag γ s p''.
+  Lemma iProto_own_auth_update γ p p' p'' :
+    iProto_own_auth γ p -∗ iProto_own_frag γ p' ==∗
+    iProto_own_auth γ p'' ∗ iProto_own_frag γ p''.
   Proof.
     iIntros "H● H◯". iDestruct (own_update_2 with "H● H◯") as "H".
     { eapply (excl_auth_update _ _ (Next p'')). }
@@ -1049,8 +1030,8 @@ Section proto.
   Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
   Proof. iExists p; simpl. iSplitL; iApply iProto_le_refl. Qed.
 
-  Lemma iProto_interp_flip vsl vsr pl pr :
-    iProto_interp vsl vsr pl pr -∗ iProto_interp vsr vsl pr pl.
+  Lemma iProto_interp_sym vsl vsr pl pr :
+    iProto_interp vsl vsr pl pr ⊢ iProto_interp vsr vsl pr pl.
   Proof.
     iDestruct 1 as (p) "[Hp Hdp]". iExists (iProto_dual p).
     rewrite (involutive iProto_dual). iFrame.
@@ -1065,8 +1046,8 @@ Section proto.
   Lemma iProto_interp_le_r vsl vsr pl pr pr' :
     iProto_interp vsl vsr pl pr -∗ pr ⊑ pr' -∗ iProto_interp vsl vsr pl pr'.
   Proof.
-    iIntros "H Hle". iApply iProto_interp_flip.
-    iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_flip.
+    iIntros "H Hle". iApply iProto_interp_sym.
+    iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_sym.
   Qed.
 
   Lemma iProto_interp_send vl ml vsl vsr pr pl' :
@@ -1107,39 +1088,47 @@ Section proto.
     iExists pr''. iIntros "{$Hpr} !>". iExists p. iFrame.
   Qed.
 
-  Global Instance iProto_own_ne γ s : NonExpansive (iProto_own γ s).
+  Lemma iProto_ctx_sym γl γr vsl vsr :
+    iProto_ctx γl γr vsl vsr ⊢ iProto_ctx γr γl vsr vsl.
+  Proof.
+    iIntros "(%pl & %pr & Hauthl & Hauthr & Hinterp)".
+    iDestruct (iProto_interp_sym with "Hinterp") as "Hinterp".
+    iExists pr, pl; iFrame.
+  Qed.
+
+  Global Instance iProto_own_ne γ : NonExpansive (iProto_own γ).
   Proof. solve_proper. Qed.
-  Global Instance iProto_own_proper γ s : Proper ((≡) ==> (≡)) (iProto_own γ s).
+  Global Instance iProto_own_proper γ : Proper ((≡) ==> (≡)) (iProto_own γ).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma iProto_own_le γ s p1 p2 :
-    iProto_own γ s p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ s p2.
+  Lemma iProto_own_le γ p1 p2 :
+    iProto_own γ p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ p2.
   Proof.
     iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
     iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
   Qed.
 
   Lemma iProto_init p :
-    ⊢ |==> ∃ γ,
-      iProto_ctx γ [] [] ∗
-      iProto_own γ Left p ∗ iProto_own γ Right (iProto_dual p).
+    ⊢ |==> ∃ γl γr,
+      iProto_ctx γl γr [] [] ∗
+      iProto_own γl p ∗ iProto_own γr (iProto_dual p).
   Proof.
-    iMod (own_alloc (●E (Next p) ⋅ ◯E (Next p))) as (lγ) "[H●l H◯l]".
+    iMod (own_alloc (●E (Next p) ⋅ ◯E (Next p))) as (γl) "[H●l H◯l]".
     { by apply excl_auth_valid. }
     iMod (own_alloc (●E (Next (iProto_dual p)) ⋅
-      ◯E (Next (iProto_dual p)))) as (rγ) "[H●r H◯r]".
+      ◯E (Next (iProto_dual p)))) as (γr) "[H●r H◯r]".
     { by apply excl_auth_valid. }
-    pose (ProtName lγ rγ) as γ. iModIntro. iExists γ. iSplitL "H●l H●r".
+    iModIntro. iExists γl, γr. iSplitL "H●l H●r".
     { iExists p, (iProto_dual p). iFrame. iApply iProto_interp_nil. }
     iSplitL "H◯l"; iExists _; iFrame; iApply iProto_le_refl.
   Qed.
 
-  Lemma iProto_send_l γ m vsr vsl vl p :
-    iProto_ctx γ vsl vsr -∗
-    iProto_own γ Left (<!> m) -∗
+  Lemma iProto_send γl γr m vsr vsl vl p :
+    iProto_ctx γl γr vsl vsr -∗
+    iProto_own γl (<!> m) -∗
     iMsg_car m vl (Next p) ==∗
-      ▷^(length vsr) iProto_ctx γ (vsl ++ [vl]) vsr ∗
-      iProto_own γ Left p.
+      ▷^(length vsr) iProto_ctx γl γr (vsl ++ [vl]) vsr ∗
+      iProto_own γl p.
   Proof.
     iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
     iDestruct 1 as (pl') "[Hle H◯]". iIntros "Hm".
@@ -1148,39 +1137,18 @@ Section proto.
       with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
     iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
     iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
-    iMod (iProto_own_auth_update _ _ _ _ p with "H●l H◯") as "[H●l H◯]".
+    iMod (iProto_own_auth_update _ _ _ p with "H●l H◯") as "[H●l H◯]".
     iIntros "!>". iSplitR "H◯".
     - iIntros "!>". iExists p, pr. iFrame.
     - iExists p. iFrame. iApply iProto_le_refl.
   Qed.
 
-  Lemma iProto_send_r γ m vsr vsl vr p :
-    iProto_ctx γ vsl vsr -∗
-    iProto_own γ Right (<!> m) -∗
-    iMsg_car m vr (Next p) ==∗
-      ▷^(length vsl) iProto_ctx γ vsl (vsr ++ [vr]) ∗
-      iProto_own γ Right p.
-  Proof.
-    iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
-    iDestruct 1 as (pr') "[Hle H◯]". iIntros "Hm".
-    iDestruct (iProto_own_auth_agree with "H●r H◯") as "#Hp".
-    iAssert (▷ (pr ⊑ <!> m))%I
-      with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
-    iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
-    iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
-    iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
-    iMod (iProto_own_auth_update _ _ _ _ p with "H●r H◯") as "[H●r H◯]".
-    iIntros "!>". iSplitR "H◯".
-    - iIntros "!>". iExists pl, p. iFrame. by iApply iProto_interp_flip.
-    - iExists p. iFrame. iApply iProto_le_refl.
-  Qed.
-
-  Lemma iProto_recv_l γ m vr vsr vsl :
-    iProto_ctx γ vsl (vr :: vsr) -∗
-    iProto_own γ Left (<?> m) ==∗
+  Lemma iProto_recv γl γr m vr vsr vsl :
+    iProto_ctx γl γr vsl (vr :: vsr) -∗
+    iProto_own γl (<?> m) ==∗
     ▷ ∃ p,
-      iProto_ctx γ vsl vsr ∗
-      iProto_own γ Left p ∗
+      iProto_ctx γl γr vsl vsr ∗
+      iProto_own γl p ∗
       iMsg_car m vr (Next p).
   Proof.
     iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
@@ -1188,31 +1156,11 @@ Section proto.
     iDestruct (iProto_own_auth_agree with "H●l H◯") as "#Hp".
     iDestruct (iProto_interp_le_l with "Hinterp [Hle]") as "Hinterp".
     { iIntros "!>". by iRewrite "Hp". }
-    iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
-    iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
-    iMod (iProto_own_auth_update _ _ _ _ q with "H●l H◯") as "[H●l H◯]".
-    iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "H◯".
-    - iExists q, pr. iFrame. by iApply iProto_interp_flip.
-    - iExists q. iIntros "{$H◯} !>". iApply iProto_le_refl.
-  Qed.
-
-  Lemma iProto_recv_r γ m vl vsr vsl :
-    iProto_ctx γ (vl :: vsl) vsr -∗
-    iProto_own γ Right (<?> m) ==∗
-    ▷ ∃ p,
-      iProto_ctx γ vsl vsr ∗
-      iProto_own γ Right p ∗
-      iMsg_car m vl (Next p).
-  Proof.
-    iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
-    iDestruct 1 as (p) "[Hle H◯]".
-    iDestruct (iProto_own_auth_agree with "H●r H◯") as "#Hp".
-    iDestruct (iProto_interp_le_r with "Hinterp [Hle]") as "Hinterp".
-    { iIntros "!>". by iRewrite "Hp". }
+    iDestruct (iProto_interp_sym with "Hinterp") as "Hinterp".
     iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
-    iMod (iProto_own_auth_update _ _ _ _ q with "H●r H◯") as "[H●r H◯]".
+    iMod (iProto_own_auth_update _ _ _ q with "H●l H◯") as "[H●l H◯]".
     iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "H◯".
-    - iExists pl, q. iFrame.
+    - iExists q, pr. iFrame. by iApply iProto_interp_sym.
     - iExists q. iIntros "{$H◯} !>". iApply iProto_le_refl.
   Qed.
 

theories/channel/proto_model.v → actris/channel/proto_model.v

@@ -123,8 +123,6 @@ Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe P
   proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
 Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
 
-(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
-is contractive *)
 Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
     (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
     (p : proto V PROPn PROP) : A :=
@@ -151,11 +149,11 @@ Proof.
   by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
 Qed.
 Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
-    (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
-    `{Hf : ∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)} a m :
+    (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) a m :
+  (∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)) →
   proto_elim x f (proto_message a m) ≡ f a m.
 Proof.
-  rewrite /proto_elim /proto_message /=.
+  intros. rewrite /proto_elim /proto_message /=.
   pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
     (PROP:=PROP) (Some (a, m))) as Hfold.
   destruct (proto_unfold (proto_fold (Some (a, m))))
@@ -179,7 +177,7 @@ Global Instance proto_map_aux_contractive {V}
 Proof.
   intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm.
   f_equiv=> v p' /=. do 2 f_equiv; [done|].
-  apply Next_contractive; destruct n as [|n]=> //=.
+  apply Next_contractive; by dist_later_intro as n' Hn'.
 Qed.
 
 Definition proto_map_aux_2 {V}
@@ -211,8 +209,7 @@ Proof.
   induction (lt_wf n) as [n _ IH]=>
     PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
   etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
-  apply proto_map_aux_contractive; destruct n as [|n]; [done|]; simpl.
-  symmetry. apply: IH. lia.
+  apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
 Qed.
 Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
@@ -240,7 +237,7 @@ Proof.
   destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=.
   apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
-  apply Next_contractive; destruct n as [|n]=> //=; auto using dist_S with lia.
+  apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_le with lia.
 Qed.
 Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
@@ -256,7 +253,7 @@ Proof.
   induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
   destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
-  apply Next_contractive; destruct n as [|n]=> //=; auto.
+  apply Next_contractive; dist_later_intro as n' Hn'; auto.
 Qed.
 Lemma proto_map_compose {V}
    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
@@ -271,7 +268,7 @@ Proof.
     PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
   destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
-  do 3 f_equiv. apply Next_contractive; destruct n as [|n]=> //=; auto.
+  do 3 f_equiv. apply Next_contractive; dist_later_intro as n' Hn'; simpl; auto.
 Qed.
 
 Program Definition protoOF (V : Type) (Fn F : oFunctor)
@@ -301,7 +298,8 @@ Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
   oFunctorContractive Fn → oFunctorContractive F → 
   oFunctorContractive (protoOF V Fn F).
 Proof.
-  intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
-  apply proto_map_ne=> //= y;
-    [destruct n; [|destruct Hfg]; by apply oFunctor_map_contractive..].
+  intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
+  apply proto_map_ne=> y //=.
+  + apply HFn. dist_later_intro as n' Hn'. f_equiv; apply Hfg.
+  + apply HF. by dist_later_intro as n' Hn'.
 Qed.

theories/examples/basics.v → actris/examples/basics.v

@@ -4,19 +4,21 @@ From actris.channel Require Import proofmode.
 From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import contribution.
 
+Local Existing Instance spin_lock.
+
 (** Basic *)
 Definition prog : val := λ: <>,
-  let: "c" := start_chan (λ: "c'", send "c'" #42) in
+  let: "c" := fork_chan (λ: "c'", send "c'" #42) in
   recv "c".
 
 (** Tranfering References *)
 Definition prog_ref : val := λ: <>,
-  let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
+  let: "c" := fork_chan (λ: "c'", send "c'" (ref #42)) in
   ! (recv "c").
 
 (** Delegation, i.e. transfering channels *)
 Definition prog_del : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
     send "c1'" (Fst "cc2");;
     send (Snd "cc2") #42) in
@@ -24,42 +26,42 @@ Definition prog_del : val := λ: <>,
 
 (** Dependent protocols *)
 Definition prog_dep : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "x" := recv "c'" in send "c'" ("x" + #2)) in
   send "c" #40;;
   recv "c".
 
 Definition prog_dep_ref : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "l" := recv "c'" in "l" <- !"l" + #2;; send "c'" #()) in
   let: "l" := ref #40 in send "c" "l";; recv "c";; !"l".
 
 Definition prog_dep_del : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
     send "c1'" (Fst "cc2");;
     let: "x" := recv (Snd "cc2") in send (Snd "cc2") ("x" + #2)) in
   let: "c2'" := recv "c1" in send "c2'" #40;; recv "c2'".
 
 Definition prog_dep_del_2 : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     send (recv "c1'") #40;;
     send "c1'" #()) in
-  let: "c2" := start_chan (λ: "c2'",
+  let: "c2" := fork_chan (λ: "c2'",
     let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
   send "c1" "c2";; recv "c1";; recv "c2".
 
 Definition prog_dep_del_3 : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "c" := recv "c1'" in let: "y" := recv "c1'" in
     send "c" "y";; send "c1'" #()) in
-  let: "c2" := start_chan (λ: "c2'",
+  let: "c2" := fork_chan (λ: "c2'",
     let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
   send "c1" "c2";; send "c1" #40;; recv "c1";; recv "c2".
 
 (** Loops *)
 Definition prog_loop : val := λ: <>,
-  let: "c" := start_chan (rec: "go" "c'" :=
+  let: "c" := fork_chan (rec: "go" "c'" :=
     let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
   send "c" #18;;
   let: "x1" := recv "c" in
@@ -69,7 +71,7 @@ Definition prog_loop : val := λ: <>,
 
 (** Transfering higher-order functions *)
 Definition prog_fun : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
   let: "r" := ref #40 in
   send "c" (λ: <>, !"r");;
@@ -77,7 +79,7 @@ Definition prog_fun : val := λ: <>,
 
 (** Lock protected channel endpoints *)
 Definition prog_lock : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "l" := newlock #() in
     Fork (acquire "l";; send "c'" #21;; release "l");;
     acquire "l";; send "c'" #21;; release "l") in
@@ -85,7 +87,7 @@ Definition prog_lock : val := λ: <>,
 
 (** Swapping of sends *)
 Definition prog_swap : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     send "c'" #20;;
     let: "y" := recv "c'" in
     send "c'" ("y" + #2)) in
@@ -93,7 +95,7 @@ Definition prog_swap : val := λ: <>,
   recv "c" + recv "c".
 
 Definition prog_swap_twice : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     send "c'" #20;;
     let: "y1" := recv "c'" in
     let: "y2" := recv "c'" in
@@ -102,7 +104,7 @@ Definition prog_swap_twice : val := λ: <>,
   recv "c" + recv "c".
 
 Definition prog_swap_loop : val := λ: <>,
-  let: "c" := start_chan (rec: "go" "c'" :=
+  let: "c" := fork_chan (rec: "go" "c'" :=
     let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
   send "c" #18;;
   send "c" #20;;
@@ -111,7 +113,7 @@ Definition prog_swap_loop : val := λ: <>,
   "x1" + "x2".
 
 Definition prog_ref_swap_loop : val := λ: <>,
-  let: "c" := start_chan (rec: "go" "c'" :=
+  let: "c" := fork_chan (rec: "go" "c'" :=
      let: "l" := recv "c'" in
      "l" <- !"l" + #2;; send "c'" #();; "go" "c'") in
   let: "l1" := ref #18 in
@@ -207,7 +209,7 @@ Definition prot_swap_loop : iProto Σ :=
 Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot); iIntros (c) "Hc".
   - by wp_send with "[]".
   - wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -215,7 +217,7 @@ Qed.
 Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_ref); iIntros (c) "Hc".
   - wp_alloc l as "Hl". by wp_send with "[$Hl]".
   - wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
 Qed.
@@ -223,7 +225,7 @@ Qed.
 Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_del); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_del); iIntros (c) "Hc".
   - wp_smart_apply (new_chan_spec prot with "[//]").
     iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -232,7 +234,7 @@ Qed.
 Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c) "Hc".
   - wp_recv (x) as "_". by wp_send with "[]".
   - wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -240,7 +242,7 @@ Qed.
 Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_ref); iIntros (c) "Hc".
   - wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
   - wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
     by iApply "HΦ".
@@ -249,7 +251,7 @@ Qed.
 Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_del); iIntros (c) "Hc".
   - wp_smart_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
     wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
@@ -259,9 +261,9 @@ Qed.
 Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_del_2); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_smart_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -269,10 +271,10 @@ Qed.
 Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_del_3); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_recv (y) as "_".
     wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_smart_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_send with "[//]".
   wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -281,7 +283,7 @@ Qed.
 Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
   - iLöb as "IH".
     wp_recv (x) as "_". wp_send with "[//]".
     by wp_smart_apply "IH".
@@ -292,7 +294,7 @@ Qed.
 Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_fun); iIntros (c) "Hc".
   - wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
     iIntros "!>" (Ψ') "HP HΨ'". wp_smart_apply ("Hf" with "HP"); iIntros (x) "HΨ".
     wp_pures. by iApply "HΨ'".
@@ -307,7 +309,7 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
   {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec (prot_lock 2)); iIntros (c) "Hc".
   - iMod contribution_init as (γ) "Hs".
     iMod (alloc_client with "Hs") as "[Hs Hcl1]".
     iMod (alloc_client with "Hs") as "[Hs Hcl2]".
@@ -333,7 +335,7 @@ Qed.
 Lemma prog_swap_spec : {{{ True }}} prog_swap #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_swap); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_swap); iIntros (c) "Hc".
   - wp_send with "[//]". wp_recv (x) as "_". by wp_send with "[//]".
   - wp_send with "[//]". wp_recv as "_". wp_recv as "_".
     wp_pures. by iApply "HΦ".
@@ -342,7 +344,7 @@ Qed.
 Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_swap_twice); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_swap_twice); iIntros (c) "Hc".
   - wp_send with "[//]". wp_recv (x1) as "_". wp_recv (x2) as "_".
     by wp_send with "[//]".
   - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
@@ -352,7 +354,7 @@ Qed.
 Lemma prog_swap_loop_spec : {{{ True }}} prog_swap_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
   - iLöb as "IH".
     wp_recv (x) as "_". wp_send with "[//]".
     by wp_smart_apply "IH".
@@ -366,7 +368,7 @@ Actris journal paper *)
 Lemma prog_ref_swap_loop_spec : ∀ Φ, Φ #42 -∗ WP prog_ref_swap_loop #() {{ Φ }}.
 Proof.
   iIntros (Φ) "HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_ref_loop); iIntros (c) "Hc".
   - iLöb as "IH". wp_lam.
     wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
     by wp_smart_apply "IH".

theories/examples/list_rev.v → actris/examples/list_rev.v

@@ -9,7 +9,7 @@ Definition list_rev_service : val :=
 
 Definition list_rev_client : val :=
   λ: "l",
-    let: "c" := start_chan list_rev_service in
+    let: "c" := fork_chan list_rev_service in
     send "c" "l";; recv "c".
 
 Section list_rev_example.
@@ -39,8 +39,7 @@ Section list_rev_example.
       + iExists []. eauto.
       + iDestruct "Hl" as (v lcons) "[HIT [Hlcons Hrec]]".
         iDestruct ("IH" with "Hrec") as (vs) "[Hvs H]".
-        iExists (v::vs). iFrame.
-        iExists v, lcons. eauto with iFrame.
+        iExists (v::vs). by iFrame.
     - iDestruct 1 as (vs) "[Hvs HIT]".
       iInduction xs as [|x xs] "IH" forall (l vs).
       + by iDestruct (big_sepL2_nil_inv_l with "HIT") as %->.
@@ -75,10 +74,10 @@ Section list_rev_example.
     {{{ RET #(); llist IT l (reverse xs) }}}.
   Proof.
     iIntros (Φ) "Hl HΦ". wp_lam.
-    wp_smart_apply (start_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
+    wp_smart_apply (fork_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
     - rewrite -(iProto_app_end_r list_rev_prot).
       iApply (list_rev_service_spec with "Hc"). eauto.
-    - iDestruct (iProto_mapsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".
+    - iDestruct (iProto_pointsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".
       { iApply list_rev_subprot. }
       wp_send (l xs) with "[$Hl]". wp_recv as "Hl". by iApply "HΦ".
   Qed.

theories/examples/map_reduce.v → actris/examples/map_reduce.v

@@ -60,11 +60,11 @@ Definition par_map_reduce_reduce : val :=
 Definition cmpZfst : val := λ: "x" "y", Fst "x" ≤ Fst "y".
 
 Definition par_map_reduce : val := λ: "n" "m" "map" "red" "xs",
-  let: "cmap" := start_chan (λ: "c", par_map_service "n" "map" "c") in
-  let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in
+  let: "cmap" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
+  let: "csort" := fork_chan (λ: "c", sort_service_fg cmpZfst "c") in
   par_map_reduce_map "n" "cmap" "csort" "xs";;
   send "csort" #stop;;
-  let: "cred" := start_chan (λ: "c", par_map_service "m" "red" "c") in
+  let: "cred" := fork_chan (λ: "c", par_map_service "m" "red" "c") in
   (* We need the first sorted element in the loop to compare subsequent elements *)
   if: ~recv "csort" then #() else (* Handle the empty case *)
   let: "jy" := recv "csort" in
@@ -90,8 +90,8 @@ End map_reduce.
 
 (** * Correctness proofs of the distributed version *)
 Class map_reduceG Σ A B `{Countable A, Countable B} := {
-  map_reduce_mapG :> mapG Σ A;
-  map_reduce_reduceG :> mapG Σ (Z * list B);
+  map_reduce_mapG :: mapG Σ A;
+  map_reduce_reduceG :: mapG Σ (Z * list B);
 }.
 
 Section mapper.
@@ -142,7 +142,7 @@ Section mapper.
     case_bool_decide; wp_pures; simplify_eq/=.
     { destruct Hn as [-> ->]; first lia.
       iApply ("HΦ" $! []). rewrite right_id_L. auto with iFrame. }
-    destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
+    destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
     - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
       destruct xs as [|x xs]; csimpl; wp_pures.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
@@ -188,7 +188,7 @@ Section mapper.
   Proof.
     iIntros (acc accv Hys Hsort Hi Φ) "[Hl Hcsort] HΦ".
     iLöb as "IH" forall (ys Hys Hsort Hi Φ); wp_rec; wp_pures; simpl.
-    wp_branch as %_|%Hperm; last first; wp_pures.
+    wp_branch as % _|%Hperm; last first; wp_pures.
     { iApply ("HΦ" $! [] None with "[Hl $Hcsort]"); simpl.
      iEval (rewrite !right_id_L); auto with iFrame. }
     wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L.
@@ -211,7 +211,7 @@ Section mapper.
       inversion 1 as [|?? [? _]]; discriminate_list || simplify_list_eq.
       assert (RZB (j',y') (i,y'')) as [??]; last (simpl in *; lia).
       apply (Sorted_StronglySorted _) in Hsort.
-      eapply elem_of_StronglySorted_app; set_solver.
+      eapply StronglySorted_app; set_solver.
   Qed.
 
   Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred :
@@ -239,7 +239,7 @@ Section mapper.
     { destruct Hn as [-> ->]; first lia.
       iApply ("HΦ" $! [] with "[$Hl]"); iPureIntro; simpl.
       by rewrite gmultiset_elements_empty !right_id_L Hmiy. }
-    destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
+    destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
     - destruct miy as [[[i y] w]|]; simplify_eq/=; wp_pures; last first.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
         iApply ("IH" $! _ _ None
@@ -281,10 +281,10 @@ Section mapper.
     {{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
   Proof.
     iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_smart_apply (start_chan_spec (par_map_protocol IA IZB map n ∅));
+    wp_smart_apply (fork_chan_spec (par_map_protocol IA IZB map n ∅));
       iIntros (cmap) "// Hcmap".
     { wp_pures. wp_smart_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
-    wp_smart_apply (start_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
+    wp_smart_apply (fork_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
       iIntros (csort) "Hcsort".
     { wp_smart_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
       iApply RZB_cmp_spec. }
@@ -292,10 +292,10 @@ Section mapper.
     wp_smart_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
     iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
     iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
-    wp_smart_apply (start_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
+    wp_smart_apply (fork_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
       iIntros (cred) "// Hcred".
     { wp_pures. wp_smart_apply (par_map_service_spec with "Hred Hcred"); auto. }
-    wp_branch as %_|%Hnil; last first.
+    wp_branch as % _|%Hnil; last first.
     { wp_pures. iApply ("HΦ" $! [] with "[$Hl]"); simpl.
       by rewrite /map_reduce /= -Hiys -Hnil. }
     wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures.

theories/examples/par_map.v → actris/examples/par_map.v

@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import llist contribution.
 From iris.algebra Require Import gmultiset.
 
+Local Existing Instance spin_lock.
+
 (** * Distributed version (aka the implementation) *)
 Definition par_map_worker : val :=
   rec: "go" "map" "l" "c" :=
@@ -47,15 +49,15 @@ Definition par_map_client_loop : val :=
       "go" "n" "c" "xs" "ys".
 
 Definition par_map_client : val := λ: "n" "map" "xs",
-  let: "c" := start_chan (λ: "c", par_map_service "n" "map" "c") in
+  let: "c" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
   let: "ys" := lnil #() in
   par_map_client_loop "n" "c" "xs" "ys";;
   lapp "xs" "ys".
 
 (** * Correctness proofs of the distributed version *)
 Class mapG Σ A `{Countable A} := {
-  map_contributionG :> contributionG Σ (gmultisetUR A);
-  map_lockG :> lockG Σ;
+  map_contributionG :: contributionG Σ (gmultisetUR A);
+  map_lockG :: lockG Σ;
 }.
 
 Section map.
@@ -171,7 +173,7 @@ Section map.
     case_bool_decide; wp_pures; simplify_eq/=.
     { destruct Hn as [-> ->]; first lia.
       iApply ("HΦ" $! []); simpl; auto with iFrame. }
-    destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
+    destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
     - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
       destruct xs as [|x xs]; csimpl; wp_pures.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
@@ -201,7 +203,7 @@ Section map.
     {{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
   Proof.
     iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_smart_apply (start_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
+    wp_smart_apply (fork_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
     { wp_smart_apply (par_map_service_spec with "Hmap Hc"); auto. }
     wp_pures. wp_smart_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
     wp_smart_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.

theories/examples/pizza.v → actris/examples/pizza.v

@@ -3,6 +3,8 @@ From actris.utils Require Import llist.
 From actris.channel Require Import proofmode.
 From stdpp Require Import list.
 
+Local Existing Instance spin_lock.
+
 Inductive pizza :=
   | Margherita
   | Calzone.
@@ -127,7 +129,7 @@ Section example.
        "v2")
     ).
 
-  Lemma lock_example_spec jcc rcc c (x1 y1 : Z) :
+  Lemma lock_example_spec `{!lockG Σ} jcc rcc c (x1 y1 : Z) :
     {{{ c ↣ pizza_prot ∗ jcc ↦ #x1 ∗ rcc ↦ #y1 }}}
       lock_example #jcc #rcc c
     {{{ (x2 y2 : Z), RET ((#x2, #(x1 - x2)), (#y2, #(y1 - y2)))%V;

theories/examples/sort.v → actris/examples/sort.v

@@ -24,8 +24,8 @@ Definition sort_service : val :=
     let: "xs" := recv "c" in
     if: llength "xs" ≤ #1 then send "c" #() else
     let: "zs" := lsplit "xs" in
-    let: "cy" := start_chan (λ: "c", "go" "cmp" "c") in
-    let: "cz" := start_chan (λ: "c", "go" "cmp" "c") in
+    let: "cy" := fork_chan (λ: "c", "go" "cmp" "c") in
+    let: "cz" := fork_chan (λ: "c", "go" "cmp" "c") in
     send "cy" "xs";;
     send "cz" "zs";;
     recv "cy";; recv "cz";;
@@ -37,7 +37,7 @@ Definition sort_service_func : val := λ: "c",
   sort_service "cmp" "c".
 
 Definition sort_client_func : val := λ: "cmp" "xs",
-  let: "c" := start_chan sort_service_func in
+  let: "c" := fork_chan sort_service_func in
   send "c" "cmp";; send "c" "xs";;
   recv "c".
 
@@ -105,10 +105,10 @@ Section sort.
       wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
     wp_smart_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
       iDestruct 1 as (->) "[Hl1 Hl2]".
-    wp_smart_apply (start_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
+    wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_smart_apply ("IH" with "Hcy"); auto. }
-    wp_smart_apply (start_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
+    wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_smart_apply ("IH" with "Hcz"); auto. }
     wp_send with "[$Hl1]".
@@ -141,7 +141,7 @@ Section sort.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_smart_apply (start_chan_spec sort_protocol_func); iIntros (c) "Hc".
+    wp_smart_apply (fork_chan_spec sort_protocol_func); iIntros (c) "Hc".
     { rewrite -(right_id END%proto _ (iProto_dual _)).
       wp_smart_apply (sort_service_func_spec with "Hc"); auto. }
     wp_send with "[$Hcmp]".

theories/examples/sort_br_del.v → actris/examples/sort_br_del.v

@@ -20,7 +20,7 @@ Definition sort_service_br : val :=
 Definition sort_service_del : val :=
   rec: "go" "cmp" "c" :=
     if: ~recv "c" then #() else
-    send "c" (start_chan (λ: "c", sort_service "cmp" "c"));;
+    send "c" (fork_chan (λ: "c", sort_service "cmp" "c"));;
     "go" "cmp" "c".
 
 Definition sort_service_br_del : val :=
@@ -29,7 +29,7 @@ Definition sort_service_br_del : val :=
       sort_service "cmp" "c";;
       "go" "cmp" "c"
     else if: recv "c" then
-      send "c" (start_chan (λ: "c", "go" "cmp" "c"));;
+      send "c" (fork_chan (λ: "c", "go" "cmp" "c"));;
       "go" "cmp" "c"
     else #().
 
@@ -76,7 +76,7 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_smart_apply (start_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
+    { wp_smart_apply (fork_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
       { wp_pures. wp_smart_apply (sort_service_spec with "Hcmp Hc'"); auto. }
       wp_send with "[$Hc']". by wp_smart_apply ("IH" with "Hc"). }
     by iApply "HΨ".
@@ -102,7 +102,7 @@ Section sort_service_br_del.
     { wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
       by wp_smart_apply ("IH" with "Hc"). }
     wp_branch; wp_pures.
-    { wp_smart_apply (start_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
+    { wp_smart_apply (fork_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
       { wp_smart_apply ("IH" with "Hc'"); auto. }
       wp_send with "[$Hc']".
       by wp_smart_apply ("IH" with "Hc"). }

theories/examples/sort_fg.v → actris/examples/sort_fg.v

@@ -42,8 +42,8 @@ Definition sort_service_fg : val :=
     let: "x" := recv "c" in
     if: ~(recv "c") then send "c" #cont;; send "c" "x";; send "c" #stop else
     let: "y" := recv "c" in
-    let: "c1" := start_chan (λ: "c", "go" "cmp" "c") in
-    let: "c2" := start_chan (λ: "c", "go" "cmp" "c") in
+    let: "c1" := fork_chan (λ: "c", "go" "cmp" "c") in
+    let: "c2" := fork_chan (λ: "c", "go" "cmp" "c") in
     send "c1" #cont;; send "c1" "x";;
     send "c2" #cont;; send "c2" "y";;
     sort_service_fg_split "c" "c1" "c2";;
@@ -66,7 +66,7 @@ Definition recv_all : val :=
     "go" "c" "ys";; lcons "x" "ys".
 
 Definition sort_client_fg : val := λ: "cmp" "xs",
-  let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
+  let: "c" := fork_chan (λ: "c", sort_service_fg "cmp" "c") in
   send_all "c" "xs";;
   send "c" #stop;;
   recv_all "c" "xs".
@@ -148,7 +148,7 @@ Section sort_fg.
   Proof.
     iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
     iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
-    wp_rec. wp_branch as %_ | %Hys'.
+    wp_rec. wp_branch as % _ | %Hys'.
     - wp_recv (x v) as (Htl) "HI".
       wp_select. wp_send with "[$HI]"; first by auto.
       wp_smart_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
@@ -181,7 +181,7 @@ Section sort_fg.
     iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
     iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
     iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
-    wp_rec. wp_branch as %_ | %Hys2.
+    wp_rec. wp_branch as % _ | %Hys2.
     - wp_recv (x v) as (Htl2) "HIx".
       wp_pures. wp_smart_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
       case_bool_decide.
@@ -221,17 +221,17 @@ Section sort_fg.
     wp_rec; wp_pures. wp_branch; wp_pures.
     - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
       + wp_recv (x2 v2) as "HIx2".
-        wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
+        wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
         { iIntros (cy) "Hcy". wp_smart_apply ("IH" with "Hcy"). auto. }
         iIntros (cy) "Hcy".
-        wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
+        wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
         { iIntros (cz) "Hcz". wp_smart_apply ("IH" with "Hcz"); auto. }
         iIntros (cz) "Hcz". rewrite !right_id.
         wp_select. wp_send with "[$HIx1]".
         wp_select. wp_send with "[$HIx2]".
         wp_smart_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
         iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
-        wp_branch as %_ | %[]%Permutation_nil_cons.
+        wp_branch as % _ | %[]%Permutation_nil_cons.
         wp_recv (x v) as "[_ HIx]".
         wp_smart_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
           with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
@@ -265,7 +265,7 @@ Section sort_fg.
   Proof.
     iIntros (Hsort Φ) "[Hl Hc] HΦ".
     iLöb as "IH" forall (xs ys' Φ Hsort).
-    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
+    wp_lam. wp_branch as % _ | %Hperm; wp_pures.
     - wp_recv (y v) as (Htl) "HIx".
       wp_smart_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
       iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
@@ -281,7 +281,7 @@ Section sort_fg.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
+    wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
     { wp_smart_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
     wp_smart_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
     wp_select.

theories/examples/swap_mapper.v → actris/examples/swap_mapper.v

@@ -25,7 +25,7 @@ Definition recv_all : val :=
 
 Definition swap_mapper_client : val :=
   λ: "f" "xs",
-    let: "c" := start_chan (λ: "c", swap_mapper_service "f" "c") in
+    let: "c" := fork_chan (λ: "c", swap_mapper_service "f" "c") in
     let: "n" := llength "xs" in
     send_all "c" "xs";; recv_all "c" "xs" "n";; send "c" #false.
 
@@ -62,7 +62,7 @@ Section with_Σ.
     (send_once $ recv_once $ prot).
 
   Lemma send_once_mono prot1 prot2 :
-    ▷ (∀ x, prot1 x ⊑ prot2 x) -∗ send_once prot1 ⊑ send_once prot2.
+    ▷ (∀ x, prot1 x ⊑ prot2 x) ⊢ send_once prot1 ⊑ send_once prot2.
   Proof.
     iIntros "Hsub".
     iModIntro.
@@ -76,7 +76,7 @@ Section with_Σ.
   Proof. intros _. apply send_once_mono. Qed.
 
   Lemma recv_once_mono prot1 prot2 x :
-    ▷ (prot1 ⊑ prot2) -∗ recv_once prot1 x ⊑ recv_once prot2 x.
+    ▷ (prot1 ⊑ prot2) ⊢ recv_once prot1 x ⊑ recv_once prot2 x.
   Proof.
     iIntros "Hsub".
     iIntros (w) "Hw". iExists w. iFrame "Hw". iModIntro.
@@ -89,7 +89,7 @@ Section with_Σ.
   Proof. intros _. apply recv_once_mono. Qed.
 
   Lemma map_once_mono prot1 prot2 :
-    ▷ (prot1 ⊑ prot2) -∗ map_once prot1 ⊑ map_once prot2.
+    ▷ (prot1 ⊑ prot2) ⊢ map_once prot1 ⊑ map_once prot2.
   Proof. iIntros "Hsub". iModIntro. iIntros (x). iModIntro. eauto. Qed.
 
   Global Instance map_once_from_modal p1 p2 :
@@ -373,13 +373,13 @@ Section with_Σ.
   Proof.
     iIntros "#Hfspec !>" (Φ) "HIT HΦ".
     wp_lam.
-    wp_smart_apply (start_chan_spec mapper_prot); iIntros (c) "// Hc".
+    wp_smart_apply (fork_chan_spec mapper_prot); iIntros (c) "// Hc".
     { wp_lam. rewrite -(iProto_app_end_r (iProto_dual mapper_prot)).
       iApply (swap_mapper_service_spec _ _ END%proto with "Hfspec Hc").
       auto. }
     wp_smart_apply (llength_spec with "HIT"); iIntros "HIT".
     wp_smart_apply (send_all_spec with "[$HIT Hc]").
-    { iApply (iProto_mapsto_le with "Hc").
+    { iApply (iProto_pointsto_le with "Hc").
       iApply subprot_n_swap. }
     iIntros "[HIT Hc]".
     rewrite right_id rev_involutive.