.gitlab-ci.yml

@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.17.0:
+build-coq.8.18.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0"
+    OPAM_PINS: "coq version 8.18.0"
     DENY_WARNINGS: "1"
     OPAM_PKG: "1"
   tags:

README.md

@@ -10,7 +10,7 @@ the paper
 
 It has been built and tested with the following dependencies
 
- - Coq 8.17.0
+ - Coq 8.18.0
  - The version of Iris in the [opam file](opam)
 
 In order to build, install the above dependencies and then run

_CoqProject

@@ -4,8 +4,9 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
+# Fixing this one requires Coq 8.19
+-arg -w -arg -argument-scope-delimiter
 
-theories/utils/skip.v
 theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v

coq-actris.opam

@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-11-06.5.4cfd3db8") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/channel/channel.v

@@ -25,7 +25,7 @@ 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.
@@ -38,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".
 
@@ -221,10 +221,10 @@ Section channel.
     - rewrite iProto_pointsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
   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]".

theories/channel/proofmode.v

@@ -420,7 +420,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 Σ) Φ :
@@ -484,3 +484,22 @@ 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) :=
+  let iNew := iFresh in
+  wp_fork_chan prot as ? iNew.

theories/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 Σ)))).
+    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.

theories/examples/basics.v

@@ -8,17 +8,17 @@ 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
@@ -26,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
@@ -71,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");;
@@ -79,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
@@ -87,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
@@ -95,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
@@ -104,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;;
@@ -113,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
@@ -209,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.
@@ -217,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.
@@ -225,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Φ".
@@ -234,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.
@@ -242,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Φ".
@@ -251,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 "_".
@@ -261,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.
@@ -271,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Φ".
@@ -283,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".
@@ -294,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Ψ'".
@@ -309,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]".
@@ -335,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Φ".
@@ -344,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 "_".
@@ -354,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".
@@ -368,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

@@ -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,7 +74,7 @@ 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_pointsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".

theories/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
@@ -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.
@@ -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

@@ -49,7 +49,7 @@ 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".
@@ -173,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.
@@ -203,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/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

@@ -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

@@ -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

@@ -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.
 
@@ -373,7 +373,7 @@ 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. }

theories/logrel/term_typing_rules.v

@@ -441,7 +441,7 @@ Section term_typing_rules.
     iDestruct "Hn" as %[k ->].
     iDestruct "Hv" as %[n ->].
     wp_faa.
-    iMod ("Hclose" with "[Hl]") as %_.
+    iMod ("Hclose" with "[Hl]") as % _.
     { iExists #(k + n). iFrame "Hl". by iExists (k + n)%Z. }
     by iExists k.
   Qed.

theories/utils/skip.v

-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
-
-Definition skipN : val :=
-  rec: "go" "n" := if: #0 < "n" then "go" ("n" - #1) else #().
-
-Lemma skipN_spec `{heapGS Σ} Φ (n : nat) : ▷^n (Φ #()) -∗ WP skipN #n {{ Φ }}.
-Proof.
-  iIntros "HΦ". iInduction n as [|n] "IH"; wp_rec; wp_pures; [done|].
-  rewrite Z.sub_1_r Nat2Z.inj_succ Z.pred_succ. by iApply "IH".
-Qed.