.gitattributes

+*.v gitlab-language=coq

.gitignore

 *.vo
+*.vos
+*.vok
 *.vio
 *.v.d
 .coqdeps.d
@@ -11,7 +13,9 @@
 *.bak
 .coqdeps.d
 .coq-native/
-build-dep/
+builddep/
 Makefile.coq
 Makefile.coq.conf
+.Makefile.coq.d
 *.crashcoqide
+_opam

.gitlab-ci.yml

+image: ralfjung/opam-ci:opam2
+
+stages:
+  - build
+
+variables:
+  CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+
+.template: &template
+  stage: build
+  tags:
+  - fp
+  script:
+  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
+  - ci/buildjob
+  cache:
+    key: "$CI_JOB_NAME"
+    paths:
+    - _opam/
+  only:
+  - master@iris/actris
+  - /^ci/@iris/actris
+  except:
+  - triggers
+  - schedules
+  - api
+
+## Build jobs
+
+build-coq.8.20.0:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.20.0"
+    DENY_WARNINGS: "1"
+    OPAM_PKG: "1"
+  tags:
+  - fp-timing
+
+trigger-iris.dev:
+  <<: *template
+  variables:
+    STDPP_REPO: "iris/stdpp"
+    IRIS_REPO: "iris/iris"
+    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
+  - schedules
+  - api

LICENSE

 All files in this development are distributed under the terms of the BSD
 license, included below.
 
-------------------------------------------------------------------------------
+Copyright: Actris developers and contributors
 
-                            BSD LICENCE
+------------------------------------------------------------------------------
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
@@ -12,17 +12,17 @@ modification, are permitted provided that the following conditions are met:
     * Redistributions in binary form must reproduce the above copyright
       notice, this list of conditions and the following disclaimer in the
       documentation and/or other materials provided with the distribution.
-    * Neither the name of the <organization> nor the
-      names of its contributors may be used to endorse or promote products
-      derived from this software without specific prior written permission.
+    * Neither the name of the copyright holder nor the names of its contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
 
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
 ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
-DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
-ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Makefile

-# Forward most targets to Coq makefile (with some trick to make this phony)
-%: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
+# Default target
 all: Makefile.coq
-	+@make -f Makefile.coq all
+	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Permit local customization
+-include Makefile.local
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
+
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq
+	+@$(MAKE) -f Makefile.coq clean
+	@# Make sure not to enter the `_opam` folder.
+	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	rm -f Makefile.coq .lia.cache builddep/*
 .PHONY: clean
 
 # Create Coq Makefile.
 Makefile.coq: _CoqProject Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
-build-dep/opam: opam Makefile
-	@echo "# Creating build-dep package."
-	@mkdir -p build-dep
-	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
-	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
-
-build-dep: build-dep/opam phony
-	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+	@echo "# Creating builddep package for $<."
+	@mkdir -p builddep
+	@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+	@# We want opam to not just install the build-deps now, but to also keep satisfying these
 	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
 	@# that are incompatible with our build requirements.
 	@# To achieve this, we create a fake opam package that has our build-dependencies as
 	@# dependencies, but does not actually install anything itself.
-	@echo "# Pinning build-dep package." && \
-	  if opam --version | grep "^1\." -q; then \
-	    BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
-	    opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
-	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
-	  else \
-	    opam install $(OPAMFLAGS) build-dep/; \
-	  fi
-
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-opam: ;
-
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
+
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
+
+# Some files that do *not* need to be forwarded to Makefile.coq.
+# ("::" lets Makefile.local overwrite this.)
+Makefile Makefile.local _CoqProject $(OPAMFILES):: ;

README.md

 # ACTRIS COQ DEVELOPMENT
 
-This directory contains the artifact for the paper "Actris: Session Type
-Based Reasoning in Separation Logic".
+This repository contains:
+- The Coq mechanization of the Actris framework, first presented in the paper
+[Actris: Session Type Based Reasoning in Separation Logic](https://iris-project.org/pdfs/2020-popl-actris-final.pdf)
+at POPL'20
+- The logical relations model for a semantic session type system, first presented in
+the paper
+[Machine-Checked Semantic Session Typing](https://iris-project.org/pdfs/2021-cpp-sessions-final.pdf)
 
 It has been built and tested with the following dependencies
 
- - Coq 8.9.1
- - [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp) at
-   commit 9041e6d8.
- - [iris](https://gitlab.mpi-sws.org/iris/iris) at
-   commit 15f1ac56.
+ - Coq 8.18.0
+ - The version of Iris in the [opam file](opam)
 
 In order to build, install the above dependencies and then run
 `make -j [num CPU cores]` to compile Actris.
 
-## Directory structure
-
-### Theory
-
-The theory can be found in `theories/channel`. Some used utilities can be found
-in `theories/utils`.
-
-The files correspond to the following content of the paper:
-
-- `theories/channel/channel.v`: The definitional semantics of bidirectional
-  channels in HeapLang.
-- `theories/channel/proto_model.v`: The CPS model of Dependent Separation
-  Protocols.
-- `theories/channel/proto_channel.v`: The definition of the connective `↣` for
-  channel ownership and the proof rules of the Actris logic.
-- `theories/channel/proofmode.v`: The Coq tactics for symbolic execution.
-
-### Examples
-
-The examples can be found in `theories/examples`.
-
-The following list gives a mapping between the examples in the paper and their
-mechanization in Coq:
-
-* 1. Introduction: `theories/examples/basics.v`
-* 2. Tour of Actris
-  * 2.3 Basic: `theories/examples/sort.v`
-  * 2.4 Higher-Order Functions: `theories/examples/sort.v`
-  * 2.5 Branching: `theories/examples/sort_br_del.v`
-  * 2.6 Recursion: `theories/examples/sort_br_del.v`
-  * 2.7 Delegation: `theories/examples/sort_br_del.v`
-  * 2.8 Dependent: `theories/examples/sort_fg.v`
-* 3. Manifest sharing via locks
-  * 3.1 Sample program: `theories/examples/basics.v`
-  * 3.2 Distributed mapper: `theories/examples/map.v`
-* 4. Case study: map reduce:
-  * Utilities for shuffling/grouping: `theories/utils/group.v`
-  * Implementation and verification: `theories/examples/map_reduce.v`
-
-## Differences between the formalization and the paper
-
-There are a number of small differences between the paper presentation
-of Actris and the formalization in Coq, that are briefly discussed here.
-
-### Connectives for physical ownership of channels
-
-In the paper physical ownership of a channel is formalized using a single
-connective `(c1,c2) ↣ (vs1,vs2)`, while the mechanisation has two connectives
-for the endpoints and one for connecting them, namely:
-
-- `chan_own γ Left vs1` and `chan_own γ Right vs1`
-- `is_chan N γ c1 c2`
-
-Where `γ` is a ghost name and `N` the invariant used internally. This setup is
-less intuitive but gives rise to a more practical Jacobs/Piessens-style spec
-of `recv` that does not need a closing view shift (to handle the case that
-the buffer is empty).
-
-### Later modalities in primitive rules for channels
-
-The primitive rules for `send` and `recv` (`send_spec` and `recv_spec`) contain
-three later modalities, which are omitted for brevity's sake in the paper. These
-later modalities expose that these operations perform at least three steps in
-the operational semantics, and are needed to deal with the three levels of
-indirection in the invariant for protocols: 1.) the `▶` in the CPS encoding of
-protocols, 2.) the higher-order ghost state used for ownership of protocols,
-3.) the opening of the protocol invariant.
+## Theory of Actris
+
+The theory of Actris (semantics of channels, the model, and the proof rules)
+can be found in the directory [theories/channel](theories/channel).
+The individual types contain the following:
+
+- [theories/channel/proto_model.v](theories/channel/proto_model.v): The
+  construction of the model of dependent separation protocols as the solution of
+  a recursive domain equation.
+- [theories/channel/proto.v](theories/channel/proto.v): The instantiation of
+  protocols with the Iris logic, definition of `iProto_own` for channel endpoint
+  ownership, and lemmas corresponding to the Actris proof rules.
+  The relevant definitions and proof rules are as follows:
+  + `iProto Σ`: The type of protocols.
+  + `iProto_message`: The constructor for sends and receives.
+  + `iProto_end`: The constructor for terminated protocols.
+  + `iProto_le`: The subprotocol relation for protocols (notation `⊑`).
+- [theories/channel/channel.v](theories/channel/channel.v): The encoding of
+  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_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)
+	`select` and `branch` operations.
+
+## Notation
+
+The following table gives a mapping between the notation in literature
+and the Coq mechanization:
+
+Dependent Separation Protocols:
+
+|        | POPL20 paper                  | Coq mechanization                     |
+|--------|-------------------------------|---------------------------------------|
+| Send   | `! x_1 .. x_n <v>{ P }. prot` | `<! x_1 .. x_n> MSG v {{ P }}; prot`  |
+| Recv   | `? x_1 .. x_n <v>{ P }. prot` | `<? x_1 .. x_n> MSG v {{ P }}; prot`  |
+| End    | `end`                         | `END`                                 |
+| Select | `prot_1 {Q_1}⊕{Q_2} prot_2`   | `prot_1 <{Q_1}+{Q_2}> prot_2`         |
+| Branch | `prot_1 {Q_1}&{Q_2} prot_2`   | `prot_1 <{Q_1}&{Q_2}> prot_2`         |
+| Append | `prot_1 · prot_2`             | `prot_1 <++> prot_2`                  |
+| Dual   | An overlined protocol         | No notation                           |
+
+This notation is additionally used for the LMCS submission.
+
+Semantic Session Types:
+
+|          | CPP21 submission              | Coq mechanization                     |
+|----------|-------------------------------|---------------------------------------|
+| Send     | `!_{X_1 .. X_n} A . S`        | `<!! X_1 .. X_n> TY A ; S`            |
+| Recv     | `?_{X_1 .. X_n} A . S`        | `<?? X_1 .. X_n> TY A ; S`            |
+| End      | `end`                         | `END`                                 |
+| Select   | `(+){ Ss }`                   | `lty_choice SEND Ss`                  |
+| Branch   | `&{ Ss }`                     | `lty_choice RECV Ss`                  |
+| Dual     | An overlined type             | No notation                           |
+| N-append | `S^n`                         | lty_napp S n                          |
+
+## Coq tactics
+
+In order to prove programs using Actris, one can make use of a combination of
+[Iris's symbolic execution tactics for HeapLang programs][HeapLang] and
+[Actris's symbolic execution tactics for message passing][ActrisProofMode]. The
+Actris tactics are as follows:
+
+- `wp_send (t1 .. tn) with "selpat"`: symbolically execute `send c v` by looking
+  up ownership of a send protocol `H : c ↣ <!> y1 .. yn, MSG v; {{ P }}; prot`
+  in the proof mode context. The tactic instantiates the variables `y1 .. yn`
+  using the terms `t1 .. tn` and uses `selpat` to prove `P`. If fewer terms
+  `t` are given than variables `y`, they will be instantiated using existential
+  variables (evars). The tactic will put `H : c ↣ prot` back into the context.
+- `wp_recv (x1 .. xn) as "ipat"`: symbolically execute `recv c` by looking up
+  `H : c ↣  <?> y1 .. yn, MSG v; {{ P }}; prot` in the proof mode context. The
+  variables `y1 .. yn` are introduced as `x1 .. xn`, and the predicate `P` is
+  introduced using the introduction pattern `ipat`. The tactic will put
+  `H : c ↣ prot` back into the context.
+- `wp_select with "selpat"`: symbolically execute `select c b` by looking up
+  `H : c ↣  prot1 {Q1}<+>{Q2} prot2` in the proof mode context. The selection
+  pattern `selpat` is used to resolve either `Q1` or `Q2`, based on the chosen
+  branch `b`. The tactic will put `H : c ↣  prot1` or `H : c ↣ prot2` back
+  into the context based on the chosen branch `b`.
+- `wp_branch as ipat1 | ipat2`: symbolically execute `branch c e1 e2` by looking
+  up `H : c ↣ prot1 {Q1}<&>{Q2} prot2` in the proof mode context. The result of
+  the tactic involves two subgoals, in which `Q1` and `Q2` are introduced using
+  the introduction patterns `ipat1` and `ipat2`, respectively. The tactic will
+  put `H : c ↣ prot1` and `H : c ↣ prot2` back into the contexts of the two
+  respectively goals.
+
+The above tactics implicitly perform normalization of the protocol `prot` in
+the hypothesis `H : c ↣ prot`. For example, `wp_send` also works if there is a
+channel with the protocol `iProto_dual ((<?> y1 .. yn, MSG v; {{ P }}; END) <++> prot)`.
+Concretely, the normalization performs the following actions:
+
+- It re-associates appends (`<++>`), and removes left-identities (`END`) of it.
+- It moves appends (`<++>`) into sends (`<!>`), receives (`<?>`), selections
+  (`<+>`) and branches (`<&>`).
+- It distributes duals (`iProto_dual`) over append (`<++>`).
+- It unfolds `prot1` into `prot2` if there is an instance of the type class
+  `ProtoUnfold prot1 prot2`. When defining a recursive protocol, it is
+  useful to define a `ProtoUnfold` instance to obtain automatic unfolding
+  of the recursive protocol. For example, see `sort_protocol_br_unfold` in
+  [theories/examples/sort_br_del.v](theories/examples/sort_br_del.v).
+
+[HeapLang]: https://gitlab.mpi-sws.org/iris/iris/blob/master/HeapLang.md
+[ProofMode]: https://gitlab.mpi-sws.org/iris/iris/blob/master/ProofMode.md
+[ActrisProofMode]: theories/channel/proofmode.v
+
+## Semantic Session Type System
+
+The logical relation for type safety of a semantic session type system is contained
+in the directory [theories/logrel](theories/logrel).
+The logical relation is defined across the following files:
+
+- [theories/logrel/model.v](theories/logrel/model.v): Definition of the
+  notions of a semantic term type and a semantic session type in terms of
+  unary Iris predicates (on values) and Actris protocols, respectively. Also
+  provides the required Coq definitions for creating recursive term/session
+  types.
+- [theories/logrel/term_types.v](theories/logrel/term_types.v): Definitions
+  of the following semantic term types: basic types (integers, booleans, unit),
+  sums, products, copyable/affine functions, universally and existentially
+  quantified types, unique/shared references, and session-typed channels.
+- [theories/logrel/session_types.v](theories/logrel/session_types.v):
+  Definitions of the following semantic session types: sending and receiving
+  with session polymorphism, n-ary choice. Session type duality is also
+  defined here. Recursive session types can be defined using the mechanism
+  defined in [theories/logrel/model.v](theories/logrel/model.v).
+- [theories/logrel/operators.v](theories/logrel/operators.v):
+  Type definitions of unary and binary operators.
+- [theories/logrel/contexts.v](theories/logrel/contexts.v):
+  Definition of the semantic type contexts, which is used in the semantic
+  typing relation. This also contains the rules for updating the context,
+  which is used for distributing affine resources across the
+  various parts of the proofs inside the typing rules.
+- [theories/logrel/term_typing_judgment.v](theories/logrel/term_typing_judgment.v):
+  Definition of the semantic typing relation, as well as the proof of type
+  soundness, showing that semantically well-typed programs do not get stuck.
+- [theories/logrel/subtyping.v](theories/logrel/subtyping.v):
+  Definition of the semantic subtyping relation for both term and session types.
+  This file also defines the notion of copyability of types in terms of subtyping.
+- [theories/logrel/subtyping_rules.v](theories/logrel/subtyping_rules.v):
+  Subtyping rules for term types and session types.
+- [theories/logrel/term_typing_rules.v](theories/logrel/term_typing_rules.v):
+  Semantic typing lemmas (typing rules) for the semantic term types.
+- [theories/logrel/session_typing_rules.v](theories/logrel/session_typing_rules.v):
+  Semantic typing lemmas (typing rules) for the semantic session types.
+- [theories/logrel/napp.v](theories/logrel/napp.v):
+  Definition of session types iteratively being appended to themselves a finite
+  number of times, with support for swapping e.g. a send over an arbitrary number
+  of receives.
+
+An extension to the basic type system is given in
+[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), which defines
+mutexes as a type-safe abstraction. Mutexes are implemented using spin locks
+and allow one to gain exclusive ownership of resources shared between multiple
+threads. An encoding of a list type is found in
+[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), along with axillary
+lemmas, and a weakest precondition for `llength`,
+that converts ownership of a list type into a list reference predicate, with
+the values of the list made explicit.
+
+## Paper-specific remarks
+
+For remarks about the paper-specific submissions, see
+
+- [papers/POPL20.md](papers/POPL20.md)
+- [papers/CPP21.md](papers/CPP21.md)
+- [papers/LMCS.md](papers/LMCS.md)

_CoqProject

--Q theories actris
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
-theories/utils/auth_excl.v
-theories/utils/llist.v
-theories/utils/compare.v
-theories/utils/contribution.v
-theories/utils/group.v
-theories/utils/misc.v
-theories/channel/channel.v
-theories/channel/proto_model.v
-theories/channel/proto_channel.v
-theories/channel/proofmode.v
-theories/examples/basics.v
-theories/examples/sort.v
-theories/examples/sort_br_del.v
-theories/examples/sort_fg.v
-theories/examples/map.v
-theories/examples/map_reduce.v
+-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
+# 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
+
+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

actris/channel/channel.v

+(** This file contains the definition of the channels, encoded as a pair of
+lock-protected buffers, and their primitive proof rules. Moreover:
+
+- It defines the connective [c ↣ prot] for ownership of channel endpoints,
+  which describes that channel endpoint [c] adheres to protocol [prot].
+- It proves Actris's specifications of [send] and [recv] w.r.t. dependent
+  separation protocols.
+
+An encoding of the usual (binary) choice connectives [prot1 <{Q1}+{Q2}> prot2]
+and [prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in
+this file.
+
+In this file we define the three message-passing connectives:
+
+- [new_chan] creates references to two empty buffers and a lock, and returns a
+  pair of endpoints, where the order of the two references determines the
+  polarity of the endpoints.
+- [send] takes an endpoint and adds an element to the first buffer.
+- [recv] performs a busy loop until there is something in the second buffer,
+  which it pops and returns, locking during each peek.
+
+It is additionaly shown that the channel ownership [c ↣ prot] is closed under
+the subprotocol relation [⊑] *)
+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.
+Set Default Proof Using "Type".
+
+Local Existing Instance spin_lock.
+
+(** * The definition of the message-passing connectives *)
+Definition new_chan : val :=
+  λ: <>,
+     let: "l" := lnil #() in
+     let: "r" := lnil #() in
+     let: "lk" := newlock #() in
+     ((("l","r"),"lk"), (("r","l"),"lk")).
+
+Definition fork_chan : val := λ: "f",
+  let: "cc" := new_chan #() in
+  Fork ("f" (Snd "cc"));; Fst "cc".
+
+Definition send : val :=
+  λ: "c" "v",
+    let: "lk" := Snd "c" in
+    let: "l" := Fst (Fst "c") in
+    let: "r" := Snd (Fst "c") in
+    acquire "lk";;
+    lsnoc "l" "v";;
+    release "lk".
+
+Definition try_recv : val :=
+  λ: "c",
+    let: "lk" := Snd "c" in
+    acquire "lk";;
+    let: "l" := Snd (Fst "c") in
+    let: "ret" := if: lisnil "l" then NONE else SOME (lpop "l") in
+    release "lk";; "ret".
+
+Definition recv : val :=
+  rec: "go" "c" :=
+    match: try_recv "c" with
+      SOME "p" => "p"
+    | NONE => "go" "c"
+    end.
+
+(** * Setup of Iris's cameras *)
+Class chanG Σ := {
+  #[local] chanG_lockG :: lockG Σ;
+  #[local] chanG_protoG :: protoG Σ val;
+}.
+Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
+Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
+Proof. solve_inG. Qed.
+
+(** * Definition of the pointsto connective *)
+Notation iProto Σ := (iProto Σ val).
+Notation iMsg Σ := (iMsg Σ val).
+
+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 Σ :=
+  ∃ γ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_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.
+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.
+Infix "<+{ P2 }>" := (iProto_choice Send True P2) (at level 85) : proto_scope.
+Infix "<&{ P2 }>" := (iProto_choice Recv True P2) (at level 85) : proto_scope.
+Infix "<{ P1 }+>" := (iProto_choice Send P1 True) (at level 85) : proto_scope.
+Infix "<{ P1 }&>" := (iProto_choice Recv P1 True) (at level 85) : proto_scope.
+Infix "<+>" := (iProto_choice Send True True) (at level 85) : proto_scope.
+Infix "<&>" := (iProto_choice Recv True True) (at level 85) : proto_scope.
+
+Section channel.
+  Context `{!heapGS Σ, !chanG Σ}.
+  Implicit Types p : iProto Σ.
+  Implicit Types TT : tele.
+
+  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_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
+  Proof.
+    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.
+
+  Global Instance iProto_choice_contractive n a :
+    Proper (dist n ==> dist n ==>
+            dist_later n ==> dist_later n ==> dist n) (@iProto_choice Σ a).
+  Proof. solve_contractive. Qed.
+  Global Instance iProto_choice_ne n a :
+    Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_choice Σ a).
+  Proof. solve_proper. Qed.
+  Global Instance iProto_choice_proper a :
+    Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_choice Σ a).
+  Proof. solve_proper. Qed.
+
+  Lemma iProto_choice_equiv a1 a2 (P11 P12 P21 P22 : iProp Σ)
+        (p11 p12 p21 p22 : iProto Σ) :
+    ⌜a1 = a2⌝ -∗ ((P11 ≡ P12):iProp Σ) -∗ (P21 ≡ P22) -∗
+    ▷ (p11 ≡ p12) -∗ ▷ (p21 ≡ p22) -∗
+    iProto_choice a1 P11 P21 p11 p21 ≡ iProto_choice a2 P12 P22 p12 p22.
+  Proof.
+    iIntros (->) "#HP1 #HP2 #Hp1 #Hp2".
+    rewrite /iProto_choice. iApply iProto_message_equiv; [ eauto | | ].
+    - iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
+      destruct b;
+        [ iRewrite -"HP1"; iFrame "H Hp1" | iRewrite -"HP2"; iFrame "H Hp2" ].
+    - iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
+      destruct b;
+        [ iRewrite "HP1"; iFrame "H Hp1" | iRewrite "HP2"; iFrame "H Hp2" ].
+  Qed.
+
+  Lemma iProto_dual_choice a P1 P2 p1 p2 :
+    iProto_dual (iProto_choice a P1 P2 p1 p2)
+    ≡ iProto_choice (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
+  Proof.
+    rewrite /iProto_choice iProto_dual_message /= iMsg_dual_exist.
+    f_equiv; f_equiv=> -[]; by rewrite iMsg_dual_base.
+  Qed.
+
+  Lemma iProto_app_choice a P1 P2 p1 p2 q :
+    (iProto_choice a P1 P2 p1 p2 <++> q)%proto
+    ≡ (iProto_choice a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
+  Proof.
+    rewrite /iProto_choice iProto_app_message /= iMsg_app_exist.
+    f_equiv; f_equiv=> -[]; by rewrite iMsg_app_base.
+  Qed.
+
+  Lemma iProto_le_choice a P1 P2 p1 p2 p1' p2' :
+    (P1 -∗ P1 ∗ ▷ (p1 ⊑ p1')) ∧ (P2 -∗ P2 ∗ ▷ (p2 ⊑ p2')) -∗
+    iProto_choice a P1 P2 p1 p2 ⊑ iProto_choice a P1 P2 p1' p2'.
+  Proof.
+    iIntros "H". rewrite /iProto_choice. destruct a;
+      iIntros (b) "HP"; iExists b; destruct b;
+      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. 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 (γ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 γl γr vsl vsr) with "[Hl Hr Hctx]").
+    { iExists [], []. iFrame "#∗". }
+    iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
+    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 fork_chan_spec p Φ (f : val) :
+    ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
+    ▷ (∀ c, c ↣ p -∗ Φ c) -∗
+    WP fork_chan f {{ Φ }}.
+  Proof.
+    iIntros "Hfork HΦ". wp_lam.
+    wp_smart_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
+    wp_smart_apply (wp_fork with "[Hfork Hc2]").
+    { iNext. wp_smart_apply ("Hfork" with "Hc2"). }
+    wp_pures. iApply ("HΦ" with "Hc1").
+  Qed.
+
+  Lemma send_spec c v p :
+    {{{ c ↣ <!> MSG v; p }}}
+      send c v
+    {{{ RET #(); c ↣ p }}}.
+  Proof.
+    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)".
+    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)
+        (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+    {{{ c ↣ (<!.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+      send c (v tt)
+    {{{ RET #(); c ↣ (p tt) }}}.
+  Proof.
+    iIntros (Φ) "[Hc HP] HΦ".
+    iDestruct (iProto_pointsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
+      as "Hc".
+    { iIntros "!>".
+      iApply iProto_le_trans.
+      iApply iProto_le_texist_intro_l.
+      by iFrame "HP". }
+    by iApply (send_spec with "Hc").
+  Qed.
+
+  Lemma try_recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+    {{{ c ↣ <?.. x> MSG v x {{ P x }}; p x }}}
+      try_recv c
+    {{{ 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_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)".
+    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]").
+      { 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.
+
+  Lemma recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+    {{{ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x }}}
+      recv c
+    {{{ x, RET v x; c ↣ p x ∗ P x }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
+    wp_smart_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
+    { wp_pures. by iApply ("IH" with "[$]"). }
+    iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
+  Qed.
+
+  (** ** Specifications for choice *)
+  Lemma select_spec c (b : bool) P1 P2 p1 p2 :
+    {{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}
+      send c #b
+    {{{ RET #(); c ↣ (if b then p1 else p2) }}}.
+  Proof.
+    rewrite /iProto_choice. iIntros (Φ) "[Hc HP] HΦ".
+    iApply (send_spec with "[Hc HP] HΦ").
+    iApply (iProto_pointsto_le with "Hc").
+    iIntros "!>". iExists b. by iFrame "HP".
+  Qed.
+
+  Lemma branch_spec c P1 P2 p1 p2 :
+    {{{ c ↣ (p1 <{P1}&{P2}> p2) }}}
+      recv c
+    {{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}.
+  Proof.
+    rewrite /iProto_choice. iIntros (Φ) "Hc HΦ".
+    iApply (recv_spec _ (tele_app _)
+      (tele_app (TT:=[tele _ : bool]) (λ b, if b then P1 else P2))%I
+      (tele_app _) 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.
+  Qed.
+End channel.

actris/channel/proto_model.v

+(** This file defines the model of dependent separation protocols as the
+solution of a recursive domain equation, along with various primitive
+operations, such as append and map.
+
+Important: This file should not be used directly, but rather the wrappers in
+[proto] should be used.
+
+Dependent Separation Protocols are modeled as the solution of the following
+recursive domain equation:
+
+[proto = 1 + (action * (V → ▶ proto → PROP))]
+
+Here, the left-hand side of the sum is used for the terminated process, while
+the right-hand side is used for the communication constructors. The type
+[action] is an inductively defined datatype with two constructors [Send] and
+[Recv]. Compared to having an additional sum in [proto], this makes it
+possible to factorize the code in a better way.
+
+The remainder [V → ▶ proto → PROP] is a predicate that ranges over the
+communicated value [V] and the tail protocol [proto]. Note that to solve this
+recursive domain equation using Iris's COFE solver, the recursive occurrence
+of [proto] appear under the later [▶].
+
+On top of the type [proto], we define the constructors:
+
+- [proto_end], which constructs the left-side of the sum.
+- [proto_msg], which takes an action and a predicate and constructs the
+  right-hand side of the sum accordingly.
+
+The defined functions on the type [proto] are:
+
+- [proto_map], which can be used to map the actions and the propositions of
+  a given protocol.
+- [proto_app], which appends two protocols [p1] and [p2], by substituting
+  all terminations [END] in [p1] with [p2]. *)
+From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import proofmode.
+From actris.utils Require Import cofe_solver_2.
+Set Default Proof Using "Type".
+
+Module Export action.
+  Inductive action := Send | Recv.
+  Global Instance action_inhabited : Inhabited action := populate Send.
+  Definition action_dual (a : action) : action :=
+    match a with Send => Recv | Recv => Send end.
+  Global Instance action_dual_involutive : Involutive (=) action_dual.
+  Proof. by intros []. Qed.
+  Canonical Structure actionO := leibnizO action.
+End action.
+
+Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe :=
+  optionO (prodO actionO (V -d> laterO A -n> PROP)).
+Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
+  optionOF (actionO * (V -d> ▶ ∙ -n> PROP)).
+
+Definition pre_proto_result (V : Type) := result_2 (proto_auxOF V).
+Definition pre_proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
+  solution_2_car (pre_proto_result V) PROPn _ PROP _.
+Global Instance pre_proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} :
+  Cofe (pre_proto V PROPn PROP).
+Proof. apply _. Qed.
+
+Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
+  proto_auxO V PROP (pre_proto V PROP PROPn).
+Global Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} :
+  Cofe (proto V PROPn PROP).
+Proof. apply _. Qed.
+
+Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
+  ofe_iso (proto V PROPn PROP) (pre_proto V PROPn PROP).
+Proof. apply pre_proto_result. Qed.
+
+Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
+  pre_proto V PROPn PROP -n> proto V PROPn PROP := ofe_iso_2 proto_iso.
+Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
+  proto V PROPn PROP -n> pre_proto V PROPn PROP := ofe_iso_1 proto_iso.
+Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
+  proto_fold (proto_unfold p) ≡ p.
+Proof. apply (ofe_iso_21 proto_iso). Qed.
+Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP} (p : pre_proto V PROPn PROP) :
+  proto_unfold (proto_fold p) ≡ p.
+Proof. apply (ofe_iso_12 proto_iso). Qed.
+
+Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
+  None.
+Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
+    (m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
+  Some (a, λ v, m v ◎ laterO_map proto_fold).
+
+Global Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
+  Proper (pointwise_relation V (dist n) ==> dist n)
+         (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
+Proof.
+  intros c1 c2 Hc. rewrite /proto_message.
+  (repeat constructor)=> //= v. by f_equiv.
+Qed.
+Global Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
+  Proper (pointwise_relation V (≡) ==> (≡))
+         (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
+Proof.
+  intros c1 c2 Hc. rewrite /proto_message.
+  (repeat constructor)=> //= v. by f_equiv.
+Qed.
+
+Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
+  p ≡ proto_end ∨ ∃ a m, p ≡ proto_message a m.
+Proof.
+  destruct p as [[a m]|]; [|by left].
+  right. exists a, (λ v, m v ◎ laterO_map proto_unfold).
+  rewrite /proto_message. do 2 f_equiv. intros v p; simpl. f_equiv.
+  rewrite -later_map_compose -{1}(later_map_id p).
+  apply later_map_ext=> p' /=. by rewrite proto_unfold_fold.
+Qed.
+Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
+  Inhabited (proto V PROPn PROP) := populate proto_end.
+
+Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
+  proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
+  ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
+Proof.
+  rewrite /proto_message option_equivI prod_equivI /=.
+  rewrite discrete_eq discrete_fun_equivI. f_equiv; [done|]. f_equiv=> x.
+  rewrite ofe_morO_equivI /=. iSplit; iIntros "H %p //".
+  assert (p ≡ later_map proto_fold (later_map proto_unfold p)) as ->; last done.
+  rewrite -later_map_compose -{1}(later_map_id p).
+  apply later_map_ext=> p' /=. by rewrite proto_fold_unfold.
+Qed.
+Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+  proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{SPROP} False.
+Proof. by rewrite option_equivI. Qed.
+Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+  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.
+
+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 :=
+  match p with
+  | None => x
+  | Some (a, m) => f a (λ v, m v ◎ laterO_map proto_unfold)
+  end.
+Global Arguments proto_elim : simpl never.
+
+Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
+    (x : A) (f1 f2 : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n :
+  (∀ a m1 m2, (∀ v, m1 v ≡{n}≡ m2 v) → f1 a m1 ≡{n}≡ f2 a m2) →
+  p1 ≡{n}≡ p2 →
+  proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2.
+Proof.
+  intros Hf [[a1 m1] [a2 m2] [[=->] ?]|]; rewrite /proto_elim //=.
+  apply Hf=> v. by f_equiv.
+Qed.
+
+Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
+    (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) :
+  proto_elim x f proto_end ≡ x.
+Proof. done. 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) a m :
+  (∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)) →
+  proto_elim x f (proto_message a m) ≡ f a m.
+Proof.
+  intros. rewrite /proto_elim /proto_message /=. f_equiv=> v p /=. f_equiv.
+  rewrite -later_map_compose -{2}(later_map_id p).
+  apply later_map_ext=> p' /=. by rewrite proto_fold_unfold.
+Qed.
+
+(** Functor *)
+Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
+    proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
+  proto_elim proto_end (λ a m, proto_message a (λ v, g ◎ m v ◎ laterO_map rec)) p.
+Next Obligation.
+  intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
+  apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv.
+Qed.
+
+Global Instance proto_map_aux_contractive {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
+  Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
+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; by dist_later_intro as n' Hn'.
+Qed.
+
+Definition proto_map_aux_2 {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP')
+    (rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
+    proto V PROPn PROP -n> proto V PROPn' PROP' :=
+  proto_map_aux g (proto_map_aux gn rec).
+Global Instance proto_map_aux_2_contractive {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+  Contractive (proto_map_aux_2 (V:=V) gn g).
+Proof.
+  intros n rec1 rec2 Hrec. rewrite /proto_map_aux_2.
+  f_equiv. by apply proto_map_aux_contractive.
+Qed.
+Definition proto_map {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+    proto V PROPn PROP -n> proto V PROPn' PROP' :=
+  fixpoint (proto_map_aux_2 gn g).
+
+Lemma proto_map_unfold {V}
+    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
+  proto_map (V:=V) gn g p ≡ proto_map_aux g (proto_map g gn) p.
+Proof.
+  apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
+  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; 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') :
+  proto_map (V:=V) gn g proto_end ≡ proto_end.
+Proof. by rewrite proto_map_unfold /proto_map_aux. Qed.
+Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
+  proto_map (V:=V) gn g (proto_message a m)
+  ≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
+Proof.
+  rewrite proto_map_unfold /proto_map_aux /=.
+  rewrite ->proto_elim_message; [done|].
+  intros a' m1 m2 Hm. f_equiv; solve_proper.
+Qed.
+
+Lemma proto_map_ne {V}
+    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
+    (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
+  gn1 ≡{n}≡ gn2 → g1 ≡{n}≡ g2 →
+  proto_map (V:=V) gn1 g1 p ≡{n}≡ proto_map (V:=V) gn2 g2 p.
+Proof.
+  revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn1 gn2 g1 g2 p.
+  induction (lt_wf n) as [n _ IH]=>
+    PROPn ? PROPn' ? PROP ? PROP' ? gn1 gn2 g1 g2 p Hgn Hg /=.
+  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; 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 :
+  gn1 ≡ gn2 → g1 ≡ g2 → proto_map (V:=V) gn1 g1 p ≡ proto_map (V:=V) gn2 g2 p.
+Proof.
+  intros Hgn Hg. apply equiv_dist=> n.
+  apply proto_map_ne=> // ?; by apply equiv_dist.
+Qed.
+Lemma proto_map_id {V} `{Hcn:!Cofe PROPn, Hc:!Cofe PROP} (p : proto V PROPn PROP) :
+  proto_map cid cid p ≡ p.
+Proof.
+  apply equiv_dist=> n. revert PROPn Hcn PROP Hc p.
+  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; dist_later_intro as n' Hn'; auto.
+Qed.
+Lemma proto_map_compose {V}
+   `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
+     Hc:!Cofe PROP, Hc':!Cofe PROP', Hc'':!Cofe PROP''}
+    (gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
+    (g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
+  proto_map (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map gn1 g2 (proto_map gn2 g1 p).
+Proof.
+  apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROPn'' Hcn''
+    PROP Hc PROP' Hc' PROP'' Hc'' gn1 gn2 g1 g2 p.
+  induction (lt_wf n) as [n _ IH]=> PROPn ? PROPn' ? PROPn'' ?
+    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; dist_later_intro as n' Hn'; simpl; auto.
+Qed.
+
+Program Definition protoOF (V : Type) (Fn F : oFunctor)
+    `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
+    `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} : oFunctor := {|
+  oFunctor_car A _ B _ := proto V (oFunctor_car Fn B A) (oFunctor_car F A B);
+  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+    proto_map (oFunctor_map Fn (fg.2, fg.1)) (oFunctor_map F fg)
+|}.
+Next Obligation.
+  intros V Fn F ?? A1 ? A2 ? B1 ? B2 ? n f g [??] p; simpl in *.
+  apply proto_map_ne=> // y; by apply oFunctor_map_ne.
+Qed.
+Next Obligation.
+  intros V Fn F ?? A ? B ? p; simpl in *. rewrite /= -{2}(proto_map_id p).
+  apply proto_map_ext=> //= y; by rewrite oFunctor_map_id.
+Qed.
+Next Obligation.
+  intros V Fn F ?? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' p; simpl in *.
+  rewrite -proto_map_compose.
+  apply proto_map_ext=> //= y; by rewrite ofe.oFunctor_map_compose.
+Qed.
+
+Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
+    `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
+    `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
+  oFunctorContractive Fn → oFunctorContractive F → 
+  oFunctorContractive (protoOF V Fn F).
+Proof.
+  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.

actris/examples/basics.v

+(** This file includes basic examples that each describe a unique feature of
+dependent separation protocols. *)
+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" := fork_chan (λ: "c'", send "c'" #42) in
+  recv "c".
+
+(** Tranfering References *)
+Definition prog_ref : val := λ: <>,
+  let: "c" := fork_chan (λ: "c'", send "c'" (ref #42)) in
+  ! (recv "c").
+
+(** Delegation, i.e. transfering channels *)
+Definition prog_del : val := λ: <>,
+  let: "c1" := fork_chan (λ: "c1'",
+    let: "cc2" := new_chan #() in
+    send "c1'" (Fst "cc2");;
+    send (Snd "cc2") #42) in
+  recv (recv "c1").
+
+(** Dependent protocols *)
+Definition prog_dep : val := λ: <>,
+  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" := 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" := 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" := fork_chan (λ: "c1'",
+    send (recv "c1'") #40;;
+    send "c1'" #()) in
+  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" := fork_chan (λ: "c1'",
+    let: "c" := recv "c1'" in let: "y" := recv "c1'" in
+    send "c" "y";; send "c1'" #()) in
+  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" := 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
+  send "c" #20;;
+  let: "x2" := recv "c" in
+  "x1" + "x2".
+
+(** Transfering higher-order functions *)
+Definition prog_fun : val := λ: <>,
+  let: "c" := fork_chan (λ: "c'",
+    let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
+  let: "r" := ref #40 in
+  send "c" (λ: <>, !"r");;
+  recv "c" #().
+
+(** Lock protected channel endpoints *)
+Definition prog_lock : val := λ: <>,
+  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
+  recv "c" + recv "c".
+
+(** Swapping of sends *)
+Definition prog_swap : val := λ: <>,
+  let: "c" := fork_chan (λ: "c'",
+    send "c'" #20;;
+    let: "y" := recv "c'" in
+    send "c'" ("y" + #2)) in
+  send "c" #20;;
+  recv "c" + recv "c".
+
+Definition prog_swap_twice : val := λ: <>,
+  let: "c" := fork_chan (λ: "c'",
+    send "c'" #20;;
+    let: "y1" := recv "c'" in
+    let: "y2" := recv "c'" in
+    send "c'" ("y1" + "y2")) in
+  send "c" #11;; send "c" #11;;
+  recv "c" + recv "c".
+
+Definition prog_swap_loop : val := λ: <>,
+  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;;
+  let: "x1" := recv "c" in
+  let: "x2" := recv "c" in
+  "x1" + "x2".
+
+Definition prog_ref_swap_loop : val := λ: <>,
+  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
+  let: "l2" := ref #20 in
+  send "c" "l1";;
+  send "c" "l2";;
+  recv "c";; recv "c";;
+  !"l1" + !"l2".
+
+Section proofs.
+Context `{heapGS Σ, chanG Σ}.
+
+(** Protocols for the respective programs *)
+Definition prot : iProto Σ :=
+  (<?> MSG #42; END)%proto.
+
+Definition prot_ref : iProto Σ :=
+  (<? (l : loc)> MSG #l {{ l ↦ #42 }}; END)%proto.
+
+Definition prot_del : iProto Σ :=
+  (<? c> MSG c {{ c ↣ prot }}; END)%proto.
+
+Definition prot_dep : iProto Σ :=
+  (<! (x : Z)> MSG #x; <?> MSG #(x + 2); END)%proto.
+
+Definition prot_dep_ref : iProto Σ :=
+  (<! (l : loc) (x : Z)> MSG #l {{ l ↦ #x }};
+   <?> MSG #() {{ l ↦ #(x + 2) }};
+   END)%proto.
+
+Definition prot_dep_del : iProto Σ :=
+  (<? c> MSG c {{ c ↣ prot_dep }}; END)%proto.
+
+Definition prot_dep_del_2 : iProto Σ :=
+  (<! c> MSG c {{ c ↣ prot_dep }};
+   <?> MSG #() {{ c ↣ <?> MSG #42; END }};
+   END)%proto.
+
+Definition prot_dep_del_3 : iProto Σ :=
+  (<! c> MSG c {{ c ↣ prot_dep }};
+   <! (y : Z)> MSG #y; <?> MSG #() {{ c ↣ <?> MSG #(y + 2); END }};
+   END)%proto.
+
+Definition prot_loop_aux (rec : iProto Σ) : iProto Σ :=
+  (<! (x : Z)> MSG #x; <?> MSG #(x + 2); rec)%proto.
+Instance prot_loop_contractive : Contractive prot_loop_aux.
+Proof. solve_proto_contractive. Qed.
+Definition prot_loop : iProto Σ := fixpoint prot_loop_aux.
+Global Instance prot_loop_unfold :
+  ProtoUnfold prot_loop (prot_loop_aux prot_loop).
+Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
+
+Definition prot_ref_loop_aux (rec : iProto Σ) : iProto Σ :=
+  (<! (l : loc) (x : Z)> MSG #l {{ l ↦ #x }}; <?> MSG #() {{ l ↦ #(x+2) }}; rec)%proto.
+Instance prot_ref_loop_contractive : Contractive prot_ref_loop_aux.
+Proof. solve_proto_contractive. Qed.
+Definition prot_ref_loop : iProto Σ := fixpoint prot_ref_loop_aux.
+Global Instance prot_ref_loop_unfold :
+  ProtoUnfold prot_ref_loop (prot_ref_loop_aux prot_ref_loop).
+Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
+
+Definition prot_fun : iProto Σ :=
+  (<! (P : iProp Σ) (Φ : Z → iProp Σ) (vf : val)>
+     MSG vf {{ {{{ P }}} vf #() {{{ x, RET #x; Φ x }}} }};
+   <? (vg : val)>
+     MSG vg {{ {{{ P }}} vg #() {{{ x, RET #(x + 2); Φ x }}} }};
+   END)%proto.
+
+Fixpoint prot_lock (n : nat) : iProto Σ :=
+  match n with
+  | 0 => END
+  | S n' => <?> MSG #21; prot_lock n'
+  end%proto.
+
+Definition prot_swap : iProto Σ :=
+  (<! (x : Z)> MSG #x;
+   <?> MSG #20;
+   <?> MSG #(x + 2); END)%proto.
+
+Definition prot_swap_twice : iProto Σ :=
+  (<! (x : Z)> MSG #x;
+   <! (y : Z)> MSG #y;
+   <?> MSG #20;
+   <?> MSG #(x+y); END)%proto.
+
+Definition prot_swap_loop : iProto Σ :=
+  (<! (x : Z)> MSG #x;
+   <! (y : Z)> MSG #y;
+   <?> MSG #(x+2);
+   <?> MSG #(y+2); prot_loop)%proto.
+
+(** Specs and proofs of the respective programs *)
+Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  wp_smart_apply (fork_chan_spec prot); iIntros (c) "Hc".
+  - by wp_send with "[]".
+  - wp_recv as "_". by iApply "HΦ".
+Qed.
+
+Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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.
+
+Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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Φ".
+Qed.
+
+Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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.
+
+Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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Φ".
+Qed.
+
+Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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 "_".
+    by iApply "HΦ".
+Qed.
+
+Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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 (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.
+
+Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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 (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Φ".
+Qed.
+
+Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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".
+  - wp_send with "[//]". wp_recv as "_". wp_send with "[//]". wp_recv as "_".
+    wp_pures. by iApply "HΦ".
+Qed.
+
+Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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Ψ'".
+  - wp_alloc l as "Hl".
+    wp_send ((l ↦ #40)%I (λ w, ⌜ w = 40%Z ⌝ ∗ l ↦ #40)%I) with "[]".
+    { iIntros "!>" (Ψ') "Hl HΨ'". wp_load. iApply "HΨ'"; auto. }
+    wp_recv (vg) as "#Hg". wp_smart_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
+    by iApply "HΦ".
+Qed.
+
+Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
+  {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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]".
+    wp_smart_apply (newlock_spec (∃ n, server γ n ε ∗
+      c ↣ iProto_dual (prot_lock n))%I
+      with "[Hc Hs]"); first by eauto with iFrame.
+    iIntros (lk γlk) "#Hlk".
+    iAssert (client γ ε -∗
+      WP acquire lk;; send c #21;; release lk {{ _, True }})%I with "[]" as "#Hhelp".
+    { iIntros "Hcl".
+      wp_smart_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
+      iDestruct "H" as (n) "[Hs Hc]".
+      iDestruct (server_agree with "Hs Hcl") as %[? _].
+      destruct n as [|n]=> //=. wp_send with "[//]".
+      iMod (dealloc_client with "Hs Hcl") as "Hs /=".
+      wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]"); eauto with iFrame. }
+    wp_smart_apply (wp_fork with "[Hcl1]").
+    { iNext. by iApply "Hhelp". }
+    by wp_smart_apply "Hhelp".
+  - wp_recv as "_". wp_recv as "_". wp_pures. by iApply "HΦ".
+Qed.
+
+Lemma prog_swap_spec : {{{ True }}} prog_swap #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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Φ".
+Qed.
+
+Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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 "_".
+    wp_pures. by iApply "HΦ".
+Qed.
+
+Lemma prog_swap_loop_spec : {{{ True }}} prog_swap_loop #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  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".
+  - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
+    wp_pures. by iApply "HΦ".
+Qed.
+
+(** This lemma is stated as the underlying weakest precondition of the
+hoare triple notation to make it equivalent to what is presented in the
+Actris journal paper *)
+Lemma prog_ref_swap_loop_spec : ∀ Φ, Φ #42 -∗ WP prog_ref_swap_loop #() {{ Φ }}.
+Proof.
+  iIntros (Φ) "HΦ". wp_lam.
+  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".
+  - wp_alloc l1 as "Hl1". wp_alloc l2 as "Hl2".
+    wp_send with "[$Hl1]". wp_send with "[$Hl2]".
+    wp_recv as "Hl1". wp_recv as "Hl2".
+    wp_load. wp_load.
+    wp_pures. by iApply "HΦ".
+Qed.
+
+End proofs.

actris/examples/equivalence.v

+From actris.channel Require Import channel proofmode.
+
+Section equivalence_examples.
+  Context `{heapGS Σ, chanG Σ}.
+
+  Lemma binder_swap_equivalence_example :
+    ((<! (x y : Z)> MSG (#x,#y) ; END):iProto Σ)%proto ≡
+    ((<! (y x : Z)> MSG (#x,#y) ; END):iProto Σ)%proto.
+  Proof.
+    apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+    iApply iProto_message_equiv; [ done | | ].
+    - iIntros "!>" (x y) "_". iExists y, x. eauto.
+    - iIntros "!>" (y x) "_". iExists x, y. eauto.
+  Qed.
+
+  Lemma choice_equivalence_example (P1 P2 Q1 Q2: iProp Σ) (S1 S2 : iProto Σ) :
+    (S1 <{P1 ∗ Q1}+{P2 ∗ Q2}> S2)%proto ≡ (S1 <{Q1 ∗ P1}+{Q2 ∗ P2}> S2)%proto.
+  Proof.
+    apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+    iApply iProto_choice_equiv; [ done | | | done | done ].
+    iApply prop_ext. iSplit; iIntros "!> [$ $]".
+    iApply prop_ext. iSplit; iIntros "!> [$ $]".
+  Qed.
+
+End equivalence_examples.

actris/examples/list_rev.v

+From actris.channel Require Import proofmode proto channel.
+From iris.proofmode Require Import proofmode.
+From actris.utils Require Import llist.
+
+Definition list_rev_service : val :=
+  λ: "c",
+    let: "l" := recv "c" in
+    lreverse "l";; send "c" #().
+
+Definition list_rev_client : val :=
+  λ: "l",
+    let: "c" := fork_chan list_rev_service in
+    send "c" "l";; recv "c".
+
+Section list_rev_example.
+  Context `{heapGS Σ, chanG Σ}.
+
+  Definition list_rev_prot : iProto Σ :=
+    (<! (l : loc) (vs : list val)> MSG #l {{ llist internal_eq l vs }} ;
+     <?> MSG #() {{ llist internal_eq l (reverse vs) }} ; END)%proto.
+
+  Lemma list_rev_service_spec c prot :
+    {{{ c ↣ (iProto_app (iProto_dual list_rev_prot) prot) }}}
+      list_rev_service c
+    {{{ RET #(); c ↣ prot }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ".
+    wp_lam. wp_recv (l vs) as "Hl". wp_smart_apply (lreverse_spec with "Hl").
+    iIntros "Hl". wp_send with "[$Hl]". iApply ("HΦ" with "Hc").
+  Qed.
+
+  Lemma llist_split {T} (IT : T → val → iProp Σ) xs l :
+    ⊢ llist IT l xs ∗-∗
+      ∃ (vs : list val), llist internal_eq l vs ∗ [∗ list] x;v ∈ xs;vs, IT x v.
+  Proof.
+    iSplit.
+    - iIntros "Hl".
+      iInduction xs as [|x xs] "IH" forall (l).
+      + iExists []. eauto.
+      + iDestruct "Hl" as (v lcons) "[HIT [Hlcons Hrec]]".
+        iDestruct ("IH" with "Hrec") as (vs) "[Hvs H]".
+        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 %->.
+      + iDestruct (big_sepL2_cons_inv_l with "HIT") as (v vs' ->) "[HIT HITs]".
+        iDestruct "Hvs" as (w lcons Heq) "[Hl Hvs]".
+        iExists w, lcons. iFrame "Hl".
+        iSplitL "HIT".
+        { by iEval (rewrite -Heq). }
+        iApply ("IH" with "Hvs HITs").
+  Qed.
+
+  Definition list_rev_protI {T} (IT : T → val → iProp Σ) : iProto Σ :=
+    (<! (l : loc) (xs : list T)> MSG #l {{ llist IT l xs }} ;
+     <?> MSG #() {{ llist IT l (reverse xs) }} ; END)%proto.
+
+  Lemma list_rev_subprot {T} (IT : T → val → iProp Σ) :
+    ⊢ list_rev_prot ⊑ list_rev_protI IT.
+  Proof.
+    iIntros (l xs) "Hl".
+    iDestruct (llist_split with "Hl") as (vs) "[Hl HIT]".
+    iExists l, vs. iFrame "Hl".
+    iModIntro. iIntros "Hl".
+    iSplitL "Hl HIT".
+    { iApply llist_split. rewrite big_sepL2_reverse_2.
+      iExists (reverse vs). iFrame "Hl HIT". }
+    done.
+  Qed.
+
+  Lemma list_rev_client_spec {T} (IT : T → val → iProp Σ) l xs :
+    {{{ llist IT l xs }}}
+      list_rev_client #l
+    {{{ RET #(); llist IT l (reverse xs) }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_lam.
+    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".
+      { iApply list_rev_subprot. }
+      wp_send (l xs) with "[$Hl]". wp_recv as "Hl". by iApply "HΦ".
+  Qed.
+
+End list_rev_example.

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

-(** This file implements a map-reduce program,
-a specification thereof and its proofs. *)
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+(** This file implements a simple distributed map-reduce function, a
+specification thereof, and its proofs. *)
+From actris.channel Require Import proofmode.
 From actris.utils Require Import llist compare contribution group.
-From actris.examples Require Import map sort_fg.
+From actris.examples Require Import par_map sort_fg.
 From iris.algebra Require Import gmultiset.
 
-(** Functional version of map reduce (aka the specification) *)
+(** * Functional version of map reduce (aka the specification) *)
 Definition map_reduce {A B C} `{EqDecision K}
     (map : A → list (K * B)) (red : K → list B → list C) : list A → list C :=
-  mbind (curry red) ∘ group ∘ mbind map.
-Instance: Params (@map_reduce) 7 := {}.
+  mbind (uncurry red) ∘ group ∘ mbind map.
+Global Instance: Params (@map_reduce) 7 := {}.
 
-(** Distributed version *)
+(** * Distributed version (aka the implementation) *)
 Definition par_map_reduce_map : val :=
   rec: "go" "n" "cmap" "csort" "xs" :=
     if: "n" = #0 then #() else
@@ -61,23 +60,23 @@ 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
   par_map_reduce_reduce "m" "csort" "cred" (SOME "jy") "xs".
 
 
-(** Properties about the functional version *)
+(** * Properties about the functional version *)
 Section map_reduce.
   Context {A B C} `{EqDecision K} (map : A → list (K * B)) (red : K → list B → list C).
   Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
 
-  Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (curry red)).
+  Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (uncurry red)).
   Proof.
     induction 1 as [|[i1 xs1] [i2 xs2] ixss1 ixss2 [??]|[i1 xs1] [i2 xs2] ixss|];
       simplify_eq/=; try done.
@@ -89,15 +88,15 @@ Section map_reduce.
   Proof. intros xs1 xs2 Hxs. by rewrite /map_reduce /= Hxs. Qed.
 End map_reduce.
 
-(** Correctness proofs of the distributed version *)
+(** * 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.
   Context `{Countable A, Countable B} {C : Type}.
-  Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B}.
+  Context `{!heapGS Σ, !chanG Σ, !map_reduceG Σ A B}.
   Context (IA : A → val → iProp Σ) (IB : Z → B → val → iProp Σ) (IC : C → val → iProp Σ).
   Context (map : A → list (Z * B)) (red : Z → list B → list C).
   Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
@@ -116,7 +115,7 @@ Section mapper.
   Proof. intros [i1 y1] [i2 y2]. destruct (total (≤)%Z i1 i2); [left|right]; done. Qed.
   Instance RZB_trans : Transitive RZB.
   Proof. by apply (prod_relation_trans _). Qed.
-  Lemma RZB_cmp_spec : cmp_spec IZB RZB cmpZfst.
+  Lemma RZB_cmp_spec : ⊢ cmp_spec IZB RZB cmpZfst.
   Proof.
     iIntros ([i1 y1] [i2 y2] v1 v2) "!>"; iIntros (Φ) "[HI1 HI2] HΦ".
     iDestruct "HI1" as (w1 ->) "HI1". iDestruct "HI2" as (w2 ->) "HI2 /=".
@@ -143,25 +142,25 @@ 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.
-    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    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.
         iApply ("IH" $! _ [] with "[%] Hl Hcmap Hcsort HΦ"); naive_solver.
-      + wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+      + wp_select. wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
         wp_send with "[$HIx]".
-        wp_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
+        wp_smart_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
         rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
         rewrite assoc_L -(comm _ [x]). iApply "HΦ".
     - wp_recv (x k) as (Hx) "Hk".
       rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)).
-      wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
+      wp_smart_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
       rewrite right_id.
-      wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
+      wp_smart_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
       iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=.
       rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
-      iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-        -?gmultiset_elem_of_singleton_subseteq //.
+      iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
+        ?gmultiset_singleton_subseteq_l //.
       rewrite (comm_L disj_union) gmultiset_elements_disj_union.
       by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm.
   Qed.
@@ -189,13 +188,13 @@ 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.
     case_bool_decide as Hij; simplify_eq/=; wp_pures.
-    - wp_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
-      rewrite -reverse_snoc. wp_apply ("IH" $! (ys ++ [y])
+    - wp_smart_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
+      rewrite -reverse_snoc. wp_smart_apply ("IH" $! (ys ++ [y])
         with "[%] [%] [//] Hl [Hcsort] [HΦ]"); try iClear "IH".
       + intros ?; discriminate_list.
       + rewrite fmap_app /= assoc_L. by apply Sorted_snoc.
@@ -212,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 :
@@ -225,12 +224,12 @@ Section mapper.
       llist IC l zs ∗
       csort ↣ from_option (λ _, sort_fg_tail_protocol IZB RZB iys
         (iys_sorted ++ acc miy)) END%proto miy ∗
-      cred ↣ par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) ∗
+      cred ↣ par_map_protocol IZBs IC (uncurry red) n (Y : gmultiset (Z * list B)) ∗
       from_option (λ '(i,y,w), IB i y w) True miy
     }}}
       par_map_reduce_reduce #n csort cred (accv miy) #l
     {{{ zs', RET #();
-       ⌜ (group iys_sorted ≫= curry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= curry red ⌝ ∗
+       ⌜ (group iys_sorted ≫= uncurry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= uncurry red ⌝ ∗
        llist IC l (zs' ++ zs)
     }}}.
   Proof.
@@ -240,14 +239,14 @@ 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
           with "[%] [%] [%] Hl Hcsort Hcred [] HΦ"); naive_solver.
-      + wp_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
-        wp_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
-        wp_apply (par_map_reduce_collect_spec _ _ _ _ _ [_] 
+      + wp_smart_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
+        wp_smart_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
+        wp_smart_apply (par_map_reduce_collect_spec _ _ _ _ _ [_] 
           with "[$Hk $Hcsort]"); try done.
         iIntros (ys' miy). iDestruct 1 as (? Hmiy') "(Hk & Hcsort & HImiy)"; csimpl.
         wp_select; wp_pures. wp_send ((i, reverse (y :: ys'))) with "[Hk]".
@@ -262,12 +261,12 @@ Section mapper.
         rewrite !bind_app /= right_id_L -!assoc_L -(comm _ zs') !assoc_L.
         apply (inj (.++ _)).
     - wp_recv ([i ys] k) as (Hy) "Hk".
-      wp_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
-      wp_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
+      wp_smart_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
+      wp_smart_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
       iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
       iApply ("HΦ" $! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L.
-      iPureIntro. rewrite (gmultiset_disj_union_difference {[ i,ys ]} Y)
-        -?gmultiset_elem_of_singleton_subseteq //.
+      iPureIntro. rewrite (gmultiset_disj_union_difference {[+ (i,ys) +]} Y)
+        ?gmultiset_singleton_subseteq_l //.
       rewrite (comm_L disj_union) gmultiset_elements_disj_union.
       rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
       by rewrite right_id_L !assoc_L.
@@ -276,34 +275,34 @@ Section mapper.
   Lemma par_map_reduce_spec n m vmap vred l xs :
     0 < n → 0 < m →
     map_spec IA IZB map vmap -∗
-    map_spec IZBs IC (curry red) vred -∗
+    map_spec IZBs IC (uncurry red) vred -∗
     {{{ llist IA l xs }}}
       par_map_reduce #n #m vmap vred #l
     {{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
   Proof.
     iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_apply (start_chan_proto_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_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
-    wp_apply (start_chan_proto_spec (sort_fg_protocol IZB RZB <++> END)%proto);
+    { wp_pures. wp_smart_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
+    wp_smart_apply (fork_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
       iIntros (csort) "Hcsort".
-    { wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
+    { wp_smart_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
       iApply RZB_cmp_spec. }
     rewrite right_id.
-    wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
+    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_apply (start_chan_proto_spec (par_map_protocol IZBs IC (curry red) m ∅));
+    wp_smart_apply (fork_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
       iIntros (cred) "// Hcred".
-    { wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
-    wp_branch as %_|%Hnil; last first.
+    { wp_pures. wp_smart_apply (par_map_service_spec with "Hred Hcred"); auto. }
+    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.
-    wp_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
+    wp_smart_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
       with "[$Hl $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
     iIntros (zs). rewrite /= gmultiset_elements_empty !right_id.
-    iDestruct 1 as (Hzs) "Hk". wp_pures.
+    iDestruct 1 as (Hzs) "Hk".
     iApply ("HΦ" with "[$Hk]"). by rewrite Hzs Hiys.
   Qed.
 End mapper.

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

-(** This file implements a distributed map service,
-a specification thereof and its proofs. *)
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation lib.spin_lock.
+(** This file implements a distributed mapper service, a specification thereof,
+and its proofs. *)
+From actris.channel Require Import proofmode.
+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" :=
     acquire "l";;
@@ -46,19 +49,20 @@ 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.
   Context `{Countable A} {B : Type}.
-  Context `{!heapG Σ, !proto_chanG Σ, !mapG Σ A}.
+  Context `{!heapGS Σ, !chanG Σ, !mapG Σ A}.
   Context (IA : A → val → iProp Σ) (IB : B → val → iProp Σ) (map : A → list B).
   Local Open Scope nat_scope.
   Implicit Types n : nat.
@@ -70,12 +74,12 @@ Section map.
       nat -d> gmultiset A -d> iProto Σ := λ i X,
     let rec : nat → gmultiset A → iProto Σ := rec in
     (if i is 0 then END else
-     ((<!> x v, MSG v {{ IA x v }}; rec i (X ⊎ {[ x ]}))
+     ((<! x v> MSG v {{ IA x v }}; rec i (X ⊎ {[+ x +]}))
         <+>
       rec (pred i) X
      ) <{⌜ i ≠ 1 ∨ X = ∅ ⌝}&>
-         <?> x (l : loc), MSG #l {{ ⌜ x ∈ X ⌝ ∗ llist IB l (map x) }};
-         rec i (X ∖ {[ x ]}))%proto.
+         <? x (l : loc)> MSG #l {{ ⌜ x ∈ X ⌝ ∗ llist IB l (map x) }};
+         rec i (X ∖ {[+ x +]}))%proto.
   Instance par_map_protocol_aux_contractive : Contractive par_map_protocol_aux.
   Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
   Definition par_map_protocol := fixpoint par_map_protocol_aux.
@@ -88,13 +92,13 @@ Section map.
 
   Lemma par_map_worker_spec γl γ vmap lk c :
     map_spec vmap -∗
-    {{{ is_lock nroot γl lk (map_worker_lock_inv γ c) ∗ client γ (∅ : gmultiset A) }}}
+    {{{ is_lock γl lk (map_worker_lock_inv γ c) ∗ client γ (∅ : gmultiset A) }}}
       par_map_worker vmap lk c
     {{{ RET #(); True }}}.
   Proof.
     iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH".
     wp_rec; wp_pures.
-    wp_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
+    wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
     iDestruct "H" as (i X) "[Hs Hc]".
     iDestruct (@server_agree with "Hs Hγ") as %[??]; destruct i as [|i]=>//=.
     iAssert ⌜ S i ≠ 1 ∨ X = ∅ ⌝%I as %?.
@@ -102,33 +106,32 @@ Section map.
       iDestruct (@server_1_agree with "Hs Hγ") as %?%leibniz_equiv; auto. }
     wp_select. wp_branch; wp_pures; last first.
     { iMod (@dealloc_client with "Hs Hγ") as "Hs /=".
-      wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
+      wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
       { iExists i, _. iFrame. }
       iIntros "_". by iApply "HΦ". }
     wp_recv (x v) as "HI".
     iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
-    { apply (gmultiset_local_update_alloc _ _ {[ x ]}). }
+    { apply (gmultiset_local_update_alloc _ _ {[+ x +]}). }
     rewrite left_id_L.
-    wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
+    wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
     { iExists (S i), _. iFrame. }
-    clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (l) "HI".
-    wp_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
+    clear dependent i X. iIntros "Hu". wp_smart_apply ("Hmap" with "HI"); iIntros (l) "HI".
+    wp_smart_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
     iDestruct "H" as (i X) "[Hs Hc]".
     iDestruct (@server_agree with "Hs Hγ")
       as %[??%gmultiset_included]; destruct i as [|i]=>//=.
-    wp_select. wp_send with "[$HI]".
-    { by rewrite gmultiset_elem_of_singleton_subseteq. }
+    wp_select. wp_send with "[$HI]"; first (iPureIntro; multiset_solver).
     iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
-    { by apply (gmultiset_local_update_dealloc _ _ {[ x ]}). }
+    { by apply (gmultiset_local_update_dealloc _ _ {[+ x +]}). }
     rewrite gmultiset_difference_diag.
-    wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
+    wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
     { iExists (S i), _. iFrame. }
-    iIntros "Hu". by wp_apply ("IH" with "[$] [$]").
+    iIntros "Hu". by wp_smart_apply ("IH" with "[$] [$]").
   Qed.
 
   Lemma par_map_workers_spec γl γ n vmap lk c :
     map_spec vmap -∗
-    {{{ is_lock nroot γl lk (map_worker_lock_inv γ c) ∗
+    {{{ is_lock γl lk (map_worker_lock_inv γ c) ∗
         [∗] replicate n (client γ (∅:gmultiset A)) }}}
       par_map_workers #n vmap lk c
     {{{ RET #(); True }}}.
@@ -137,10 +140,10 @@ Section map.
     iInduction n as [|n] "IH"; wp_rec; wp_pures; simpl.
     { by iApply "HΦ". }
     iDestruct "Hγs" as "[Hγ Hγs]".
-    wp_apply (wp_fork with "[Hγ]").
-    { iNext. wp_apply (par_map_worker_spec with "Hmap [$]"); auto. }
+    wp_smart_apply (wp_fork with "[Hγ]").
+    { iNext. wp_smart_apply (par_map_worker_spec with "Hmap [$]"); auto. }
     wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-    wp_apply ("IH" with "[$] [$]").
+    wp_smart_apply ("IH" with "[$] [$]").
   Qed.
 
   Lemma par_map_service_spec n vmap c :
@@ -151,10 +154,10 @@ Section map.
   Proof.
     iIntros "#Hf !>"; iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iMod (contribution_init_pow (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
-    wp_apply (newlock_spec nroot (map_worker_lock_inv γ c) with "[Hc Hs]").
+    wp_smart_apply (newlock_spec (map_worker_lock_inv γ c) with "[Hc Hs]").
     { iExists n, ∅. iFrame. }
     iIntros (lk γl) "#Hlk".
-    wp_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
+    wp_smart_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
   Qed.
 
   Lemma par_map_client_loop_spec n c l k xs X ys :
@@ -170,23 +173,23 @@ 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.
-    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    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.
         iApply ("IH" with "[%] Hl Hk Hc [$]"); naive_solver.
-      + wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+      + wp_select. wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
         wp_send with "[$HIx]".
-        wp_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
+        wp_smart_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
         rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
         rewrite assoc_L -(comm _ [x]). iApply "HΦ".
     - wp_recv (x l') as (Hx) "Hl'".
-      wp_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
-      wp_apply ("IH" with "[] Hl Hk Hc"); first done.
+      wp_smart_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
+      wp_smart_apply ("IH" with "[] Hl Hk Hc"); first done.
       iIntros (ys'); iDestruct 1 as (Hys) "Hk"; simplify_eq/=.
       iApply ("HΦ" $! (ys' ++ map x)). iSplit.
-      + iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-          -?gmultiset_elem_of_singleton_subseteq //.
+      + iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
+          ?gmultiset_singleton_subseteq_l //.
         rewrite (comm_L disj_union) gmultiset_elements_disj_union.
         by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L.
       + by rewrite -assoc_L.
@@ -200,12 +203,12 @@ Section map.
     {{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
   Proof.
     iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_apply (start_chan_proto_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
-    { wp_apply (par_map_service_spec with "Hmap Hc"); auto. }
-    wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
-    wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
+    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.
     iIntros (ys) "(?&Hl&Hk)". rewrite /= gmultiset_elements_empty !right_id_L.
-    wp_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
-    wp_pures. iApply "HΦ"; auto.
+    wp_smart_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
+    iApply "HΦ"; auto.
   Qed.
 End map.

actris/examples/pizza.v

+From iris.heap_lang Require Import lib.spin_lock lib.par.
+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.
+
+Section example.
+  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
+
+  Definition pizza_to_val (p : pizza) :=
+    match p with
+    | Margherita => #0
+    | Calzone => #1
+    end.
+
+  Fixpoint list_to_val {T} (f : T → val) (xs : list T) :=
+    match xs with
+    | [] => NONEV
+    | x::xs => SOMEV ((f x), (list_to_val f xs))%V
+    end.
+
+  Notation pizza_list_to_val := (list_to_val pizza_to_val).
+
+  Fixpoint is_list {T} (f : T → val) (v : val) (ws : list T) : iProp Σ :=
+    match ws with
+    | []    => ⌜v = NONEV⌝
+    | w::ws => ∃ (v' : val), ⌜v = SOMEV ((f w), v')%V⌝ ∗ is_list f v' ws
+  end.
+
+  Notation is_int_list := (is_list (λ v, LitV $ LitInt $ v)).
+  Notation is_pizza_list := (is_list pizza_to_val).
+
+  Lemma is_pizza_list_pizzas pizzas :
+    ⊢ is_pizza_list (pizza_list_to_val pizzas) pizzas.
+  Proof. induction pizzas; [eauto | iExists _; eauto]. Qed.
+
+  Fixpoint int_list_sum (xs : list Z) : Z :=
+    match xs with
+    | []    => 0
+    | x::xs => x + int_list_sum xs
+    end.
+
+  Definition sum_list : val :=
+    rec: "go" "xs" :=
+      match: "xs" with
+        NONE => #0
+      | SOME "xs" => Fst "xs" + "go" (Snd "xs")
+      end.
+
+  Lemma sum_list_spec v xs :
+    {{{ is_int_list v xs }}}
+      sum_list v
+    {{{ RET #(int_list_sum xs); True }}}.
+  Proof.
+    unfold is_int_list.
+    iIntros (Φ) "Hxs HΦ".
+    iInduction xs as [|x xs] "IH" forall (v Φ).
+    - wp_rec. iDestruct "Hxs" as "->".
+      wp_pures. by iApply "HΦ".
+    - wp_rec. unfold is_int_list. simpl.
+      iDestruct "Hxs" as (v') "[-> Hrec]".
+      wp_pures.
+      wp_apply ("IH" with "Hrec").
+      iIntros "_". wp_pures.
+      by iApply "HΦ".
+  Qed.
+
+  Definition order_pizza (pizzas : list pizza) : val :=
+    λ: "cc" "c",
+    send "c" (pizza_list_to_val pizzas);;
+    send "c" "cc";;
+    let: "receipt" := recv "c" in
+    (sum_list "receipt", !"cc").
+
+  Definition pizza_prot_aux (rec : iProto Σ) : iProto Σ :=
+    (<! (v1 : val) (xs1 : list pizza)> MSG v1 {{ is_pizza_list v1 xs1 }} ;
+     <! (l : loc) (x : Z)> MSG #l {{ l ↦ #x }};
+     <? (v2 : val) (xs2 : list Z)> MSG v2 {{ is_int_list v2 xs2 ∗
+                                             ⌜Zlength xs1 = Zlength xs2⌝ ∗
+                                             l ↦ #(x - int_list_sum xs2)%Z }};
+    rec)%proto.
+
+  Instance pizza_prot_aux_contractive : Contractive pizza_prot_aux.
+  Proof. solve_proto_contractive. Qed.
+
+  Definition pizza_prot := fixpoint pizza_prot_aux.
+  Global Instance pizza_prot_unfold :
+    ProtoUnfold pizza_prot (pizza_prot_aux pizza_prot).
+  Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
+
+  Lemma order_pizza_spec pizzas c cc (x1 : Z) :
+    {{{ c ↣ pizza_prot ∗ cc ↦ #x1 }}}
+      order_pizza pizzas #cc c
+    {{{ (x2 : Z), RET (#x2, #(x1 - x2))%V;
+        c ↣ pizza_prot ∗ cc ↦ #(x1 - x2)%Z }}}.
+  Proof.
+    iIntros (Φ) "[Hc Hcc] HΦ".
+    wp_lam.
+    wp_send (_ pizzas) with "[]".
+    { iApply is_pizza_list_pizzas. }
+    wp_send with "[Hcc //]".
+    wp_recv (v2 xs2) as "[Hxs2 [_ Hcc]]".
+    wp_load.
+    wp_apply (sum_list_spec with "Hxs2").
+    iIntros "_".
+    wp_pures.
+    iModIntro.
+    iApply "HΦ".
+    eauto with iFrame.
+  Qed.
+
+  Definition lock_example : val :=
+    λ: "jesper_cc" "robbert_cc" "c",
+    let: "lk" := newlock #() in
+    (
+      (acquire "lk";;
+       let: "v1" := order_pizza [Margherita] "jesper_cc" "c" in
+       release "lk";;
+       "v1")
+      |||
+      (acquire "lk";;
+       let: "v2" := order_pizza [Calzone] "robbert_cc" "c" in
+       release "lk";;
+       "v2")
+    ).
+
+  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;
+        jcc ↦ #(x1 - x2) ∗ rcc ↦ #(y1 - y2) }}}.
+  Proof.
+    iIntros (Φ) "[Hc [Hjcc Hrcc]] HΦ".
+    wp_lam. wp_pures.
+    wp_apply (newlock_spec with "Hc").
+    iIntros (lk γ) "#Hlk".
+    wp_pures.
+    wp_apply (wp_par (λ v, ∃ (x2:Z), ⌜v = (#x2, #(x1 - x2))%V⌝ ∗
+                                     jcc ↦ #(x1 - x2)%Z)%I
+                     (λ v, ∃ (y2:Z), ⌜v = (#y2, #(y1 - y2))%V⌝ ∗
+                                     rcc ↦ #(y1 - y2)%Z)%I
+                with "[Hjcc] [Hrcc]").
+    - wp_pures.
+      wp_apply (acquire_spec with "Hlk").
+      iIntros "[Hlocked Hc]".
+      wp_pures. wp_apply (order_pizza_spec with "[$Hc $Hjcc]").
+      iIntros (x2) "[Hc Hjcc]".
+      wp_pures.
+      wp_apply (release_spec with "[$Hlk $Hlocked $Hc]").
+      iIntros "_".
+      wp_pures.
+      eauto.
+    - wp_pures.
+      wp_apply (acquire_spec with "Hlk").
+      iIntros "[Hlocked Hc]".
+      wp_pures. wp_apply (order_pizza_spec with "[$Hc $Hrcc]").
+      iIntros (y2) "[Hc Hrcc]".
+      wp_pures.
+      wp_apply (release_spec with "[$Hlk $Hlocked $Hc]").
+      iIntros "_".
+      wp_pures.
+      eauto.
+    - iIntros (v1 v2) "[HΨ1 HΨ2]".
+      iIntros "!>".
+      iDestruct "HΨ1" as (x2) "[-> HΨ1]".
+      iDestruct "HΨ2" as (y2) "[-> HΨ2]".
+      iApply ("HΦ" with "[$HΨ1 $HΨ2]").
+  Qed.
+
+End example.

actris/examples/rpc.v

+From iris.heap_lang Require Import proofmode.
+From actris.channel Require Import proofmode.
+
+Definition server : val :=
+  rec: "go" "dict" "c" :=
+    if: ~ (recv "c") then #()
+    else
+      let: "f" := "dict" (recv "c") in
+      let: "res" := "f" (recv "c") in
+      send "c" "res";;
+      "go" "dict" "c".
+
+Definition Left : val := #true.
+Definition Right : val := #false.
+
+Notation plus_id := 1%Z.
+Notation incr_ref_id := 2%Z.
+
+Definition client : val :=
+  λ: "c",
+    send "c" Left;;
+    send "c" #plus_id;; send "c" (#40,#2);; let: "res1" := recv "c" in
+    send "c" Left;;
+    let: "l" := ref #41 in
+    send "c" #incr_ref_id;; send "c" "l";; let: "res2" := ! (recv "c") in
+    send "c" Right;;
+    ("res1","res2").
+
+Definition program : val :=
+  λ: "dict",
+    let: "c" := new_chan #() in
+    Fork (server "dict" (Snd "c"));;
+    client (Fst "c").
+
+Section rpc_example.
+  Context `{!heapGS Σ, !chanG Σ}.
+
+  Definition f_spec {T U} (IT : T → val → iProp Σ) (IU : U → val → iProp Σ)
+             (f : T → U) (fv : val) : iProp Σ :=
+    (∀ x v, {{{ IT x v }}} fv v {{{ w, RET w; IU (f x) w }}})%I.
+
+  Definition rpc_prot_aux (f_specs : gmap Z (val → iProp Σ)) (rec : iProto Σ)
+    : iProto Σ :=
+    ((<! (T U:Type) IT IU (f : T → U) (id:Z)> MSG #id
+        {{ ⌜f_specs !! id = Some (f_spec IT IU f)⌝ }};
+      <! (x:T) (v:val)> MSG v {{ IT x v }} ;
+      <? (w:val)> MSG w {{ IU (f x) w }} ; rec)
+    <+> END)%proto.
+
+  Instance rpc_prot_aux_contractive (f_specs : gmap Z (val → iProp Σ)) :
+    Contractive (rpc_prot_aux f_specs).
+  Proof. solve_proto_contractive. Qed.
+  Definition rpc_prot (f_specs : gmap Z (val → iProp Σ)) : iProto Σ :=
+    fixpoint (rpc_prot_aux f_specs).
+  Global Instance rpc_prot_unfold f_specs :
+    ProtoUnfold (rpc_prot f_specs) (rpc_prot_aux f_specs (rpc_prot f_specs)).
+  Proof. apply proto_unfold_eq, fixpoint_unfold. Qed.
+
+  Definition dict_spec (dict : val) (f_specs : gmap Z _) : iProp Σ :=
+    ∀ (T U : Type) (id : Z) (IT : T → val → iProp Σ) (IU : U → val → iProp Σ)
+      (f : T → U),
+      {{{ ⌜f_specs !! id = Some (f_spec IT IU f)⌝ }}}
+        dict #id
+      {{{ fv, RET fv; f_spec IT IU f fv }}}.
+
+  Lemma server_spec dict f_specs c prot :
+    {{{ dict_spec dict f_specs ∗
+        c ↣ (iProto_dual (rpc_prot f_specs) <++> prot)%proto }}}
+      server dict c
+    {{{ RET #(); c ↣ prot }}}.
+  Proof.
+    iIntros (Φ) "[#Hdict Hc] HΦ".
+    iLöb as "IH".
+    wp_rec.
+    wp_branch; last first.
+    { wp_pures. by iApply "HΦ". }
+    wp_recv (T U IT IU f id) as "Hlookup".
+    wp_smart_apply ("Hdict" with "Hlookup"); iIntros (fv) "Hfv".
+    wp_recv (x v) as "HIT".
+    wp_smart_apply ("Hfv" with "HIT"); iIntros (w) "HIU".
+    wp_send (w) with "[$HIU]".
+    wp_pures. by iApply ("IH" with "Hc").
+  Qed.
+
+  Definition plus_spec :=
+    f_spec (λ (x:Z*Z) (v:val), ⌜(#(fst x), #(snd x))%V = v⌝)%I
+           (λ y w, ⌜#y = w⌝)%I
+           (λ (x:Z*Z), (fst x) + (snd x))%Z.
+
+  Definition incr_ref_spec :=
+    f_spec (λ (x:Z) (v:val), ∃ (l : loc), ⌜v = #l⌝ ∗ l ↦ #x)%I
+           (λ (y:Z) (w:val), ∃ (l : loc), ⌜w = #l⌝ ∗ l ↦ #y)%I
+           (λ (x:Z), x+1)%Z.
+
+  Definition client_f_specs : gmap Z (val → iProp Σ) :=
+    {[ plus_id := plus_spec ]} ∪
+    {[ incr_ref_id := incr_ref_spec ]}.
+
+  Lemma client_spec c :
+    {{{ c ↣ rpc_prot client_f_specs }}}
+      client c
+    {{{ RET (#42, #42); True }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ".
+    wp_lam.
+    (** plus *)
+    wp_select.
+    wp_send with "[//]". wp_send with "[]".
+    { by instantiate (1:=(40,2)%Z). }
+    wp_recv (w) as "<-".
+    (** incr_ref *)
+    wp_select.
+    wp_alloc l as "Hl".
+    wp_send with "[//]". wp_send with "[Hl]".
+    { eauto. }
+    wp_recv (w) as (l') "[-> Hl]".
+    wp_load.
+    (** Termination *)
+    wp_select.
+    wp_pures.
+    by iApply "HΦ".
+  Qed.
+
+  Lemma program_spec dict :
+    {{{ dict_spec dict client_f_specs }}}
+      program dict
+    {{{ v, RET v; True }}}.
+  Proof.
+    iIntros (Φ) "#Hdict HΦ".
+    wp_lam.
+    wp_smart_apply (new_chan_spec (rpc_prot client_f_specs))=> //.
+    iIntros (c1 c2) "[Hc1 Hc2]".
+    wp_smart_apply (wp_fork with "[Hc2]").
+    - iIntros "!>". wp_smart_apply (server_spec _ _ _ END%proto with "[Hc2]").
+      rewrite right_id. iFrame "Hdict Hc2". by iIntros "_".
+    - by wp_smart_apply (client_spec with "Hc1").
+  Qed.
+
+End rpc_example.

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

-(** This file implements a distributed Merge Sort,
-a specification thereof and its proofs, including
-a variant in which the comparison function is sent
-over the channel. *)
+(** This file implements a distributed version of merge sort, a specification
+thereof, and its proofs. There are two variants:
+
+- [sort_service]: a service that takes both a comparison function and a channel
+  as its arguments.
+- [sort_service_func]: a service that only takes a channel as its argument. The
+  comparison function is sent over the channel. *)
 From stdpp Require Import sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
 From actris.utils Require Export llist compare.
 
 Definition lmerge : val :=
@@ -22,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";;
@@ -35,22 +37,21 @@ 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".
 
 Section sort.
-  Context `{!heapG Σ, !proto_chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
 
-  Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop)
-      `{!RelDecision R, !Total R} : iProto Σ :=
-    (<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
-     <?> (xs' : list A), MSG #() {{ ⌜ Sorted R xs' ⌝ ∗ ⌜ xs' ≡ₚ xs ⌝ ∗ llist I l xs' }};
+  Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop) : iProto Σ :=
+    (<! (xs : list A) (l : loc)> MSG #l {{ llist I l xs }};
+     <? (xs' : list A)> MSG #() {{ ⌜ Sorted R xs' ⌝ ∗ ⌜ xs' ≡ₚ xs ⌝ ∗ llist I l xs' }};
      END)%proto.
 
   Definition sort_protocol_func : iProto Σ :=
-    (<!> A (I : A → val → iProp Σ) (R : A → A → Prop)
-         `{!RelDecision R, !Total R} (cmp : val),
+    (<! A (I : A → val → iProp Σ) (R : A → A → Prop)
+         `(!RelDecision R, !Total R) (cmp : val)>
        MSG cmp {{ cmp_spec I R cmp }};
      sort_protocol I R)%proto.
 
@@ -63,29 +64,29 @@ Section sort.
   Proof.
     iIntros "#Hcmp" (Ψ) "!> [Hl1 Hl2] HΨ".
     iLöb as "IH" forall (l2 xs1 xs2 Ψ).
-    wp_lam. wp_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
+    wp_lam. wp_smart_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
     destruct xs1 as [|x1 xs1]; wp_pures.
-    { wp_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
+    { wp_smart_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
       iApply "HΨ". iFrame. by rewrite list_merge_nil_l. }
-    wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
+    wp_smart_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
     destruct xs2 as [|x2 xs2]; wp_pures.
-    { iApply "HΨ". iFrame. }
-    wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
-    wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
-    wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
+    { iApply "HΨ". by iFrame. }
+    wp_smart_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
+    wp_smart_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
+    wp_smart_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
     case_bool_decide; wp_pures.
     - rewrite decide_True //.
-      wp_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
-      wp_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
+      wp_smart_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
+      wp_smart_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
       { iExists _, _. iFrame. }
       iIntros "Hl1".
-      wp_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
+      wp_smart_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
     - rewrite decide_False //.
-      wp_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
-      wp_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
+      wp_smart_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
+      wp_smart_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
       { iExists _, _. iFrame. }
       iIntros "Hl1".
-      wp_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
+      wp_smart_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
   Qed.
 
   Lemma sort_service_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
@@ -97,24 +98,24 @@ Section sort.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
     wp_recv (xs l) as "Hl".
-    wp_apply (llength_spec with "Hl"); iIntros "Hl".
+    wp_smart_apply (llength_spec with "Hl"); iIntros "Hl".
     wp_op; case_bool_decide as Hlen; wp_if.
     { assert (Sorted R xs).
       { destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
       wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
-    wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
+    wp_smart_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
       iDestruct 1 as (->) "[Hl1 Hl2]".
-    wp_apply (start_chan_proto_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_apply ("IH" with "Hcy"); auto. }
-    wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cz) "Hcz".
+      wp_smart_apply ("IH" with "Hcy"); auto. }
+    wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
-      wp_apply ("IH" with "Hcz"); auto. }
+      wp_smart_apply ("IH" with "Hcz"); auto. }
     wp_send with "[$Hl1]".
     wp_send with "[$Hl2]".
     wp_recv (ys1) as (??) "Hl1".
     wp_recv (ys2) as (??) "Hl2".
-    wp_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
+    wp_smart_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
     wp_send ((list_merge R ys1 ys2)) with "[$Hl]".
     - iSplit; iPureIntro.
       + by apply (Sorted_list_merge _).
@@ -129,7 +130,7 @@ Section sort.
   Proof.
     iIntros (Ψ) "Hc HΨ". wp_lam.
     wp_recv (A I R ?? cmp) as "#Hcmp".
-    by wp_apply (sort_service_spec with "Hcmp Hc").
+    by wp_smart_apply (sort_service_spec with "Hcmp Hc").
   Qed.
 
   Lemma sort_client_func_spec {A} (I : A → val → iProp Σ) R
@@ -140,12 +141,12 @@ Section sort.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_proto_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_apply (sort_service_func_spec with "Hc"); auto. }
-    wp_send (A I R) with "[$Hcmp]".
+      wp_smart_apply (sort_service_func_spec with "Hc"); auto. }
+    wp_send with "[$Hcmp]".
     wp_send with "[$Hl]".
     wp_recv (ys) as "(Hsorted & Hperm & Hl)".
-    wp_pures. iApply "HΦ"; iFrame.
+    iApply "HΦ"; by iFrame.
   Qed.
 End sort.

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

-(** This file implements a looping distributed Merge Sort,
-a specification thereof and its proofs. *)
+(** This file provides three wrappers around the distributed version of merge
+sort, demonstrating Actris's support for delegation and branching:
+
+- [sort_service_br]: a service that allows one to sort a series of lists in 
+  sequence. 
+- [sort_service_del]: a service that allows one to sort a series of lists in
+  parallel by delegating a sort service for a single list to a new channel.
+- [sort_service_br_del]: a service that allows one to sort a series of list by
+  forking itself. *)
 From stdpp Require Import sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
 From actris.examples Require Import sort.
 
 Definition sort_service_br : val :=
@@ -14,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 :=
@@ -23,12 +29,12 @@ 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 #().
 
 Section sort_service_br_del.
-  Context `{!heapG Σ, !proto_chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
   Context {A} (I : A → val → iProp Σ) (R : A → A → Prop) `{!RelDecision R, !Total R}.
 
   Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
@@ -48,13 +54,13 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
-      by wp_apply ("IH" with "Hc"). }
+    { wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
+      by wp_smart_apply ("IH" with "Hc"). }
     by iApply "HΨ".
   Qed.
 
   Definition sort_protocol_del_aux (rec : iProto Σ) : iProto Σ :=
-    ((<?> c, MSG c {{ c ↣ sort_protocol I R }}; rec) <+> END)%proto.
+    ((<? c> MSG c {{ c ↣ sort_protocol I R }}; rec) <+> END)%proto.
   Instance sort_protocol_del_aux_contractive : Contractive sort_protocol_del_aux.
   Proof. solve_proto_contractive. Qed.
   Definition sort_protocol_del : iProto Σ := fixpoint sort_protocol_del_aux.
@@ -70,15 +76,14 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_apply (start_chan_proto_spec (sort_protocol I R <++> END)%proto);
-        iIntros (c') "Hc'".
-      { wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
-      wp_send with "[$Hc']". by wp_apply ("IH" with "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Ψ".
   Qed.
 
   Definition sort_protocol_br_del_aux (rec : iProto Σ) : iProto Σ :=
-    ((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec }}; rec) <+> END))%proto.
+    ((sort_protocol I R <++> rec) <+> ((<? c> MSG c {{ c ↣ rec }}; rec) <+> END))%proto.
   Instance sort_protocol_br_del_aux_contractive : Contractive sort_protocol_br_del_aux.
   Proof. solve_proto_contractive. Qed.
   Definition sort_protocol_br_del : iProto Σ := fixpoint sort_protocol_br_del_aux.
@@ -94,13 +99,13 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
-      by wp_apply ("IH" with "Hc"). }
+    { wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
+      by wp_smart_apply ("IH" with "Hc"). }
     wp_branch; wp_pures.
-    { wp_apply (start_chan_proto_spec sort_protocol_br_del); iIntros (c') "Hc'".
-      { wp_apply ("IH" with "Hc'"); auto. }
+    { 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_apply ("IH" with "Hc"). }
+      by wp_smart_apply ("IH" with "Hc"). }
     by iApply "HΨ".
   Qed.
 End sort_service_br_del.