.gitignore

@@ -13,7 +13,9 @@
 *.bak
 .coqdeps.d
 .coq-native/
-build-dep/
+builddep/
 Makefile.coq
 Makefile.coq.conf
+.Makefile.coq.d
 *.crashcoqide
+_opam

.gitlab-ci.yml

@@ -5,6 +5,7 @@ stages:
 
 variables:
   CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
 
 .template: &template
   stage: build
@@ -16,10 +17,10 @@ variables:
   cache:
     key: "$CI_JOB_NAME"
     paths:
-    - opamroot/
+    - _opam/
   only:
-  - master
-  - /^ci/
+  - master@iris/actris
+  - /^ci/@iris/actris
   except:
   - triggers
   - schedules
@@ -27,15 +28,21 @@ variables:
 
 ## Build jobs
 
-build-coq.8.11.1:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.11.1"
+    OPAM_PINS: "coq version 8.20.0"
+    DENY_WARNINGS: "1"
+    OPAM_PKG: "1"
+  tags:
+  - fp-timing
 
-build-iris.dev:
+trigger-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV  coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
+    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

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 .lia.cache
+	+@$(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 "# Installing build-dep package."
-	@opam install $(OPAMFLAGS) build-dep/
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
 
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-opam: ;
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
 
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+# 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 Coq mechanization of the Actris framework,
-first presented in the paper
+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.
+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.11.1
+ - Coq 8.18.0
  - The version of Iris in the [opam file](opam)
 
 In order to build, install the above dependencies and then run
@@ -34,11 +37,11 @@ The individual types contain the following:
   bidirectional channels in terms of Iris's HeapLang language, with specifications
   defined in terms of the dependent separation protocols.
   The relevant definitions and proof rules are as follows:
-  + `mapsto_proto`: endpoint ownership (notation `↣`).
+  + `iProto_pointsto`: endpoint ownership (notation `↣`).
   + `new_chan_spec`, `send_spec` and `recv_spec`: proof rule for `new_chan`,
-    `send`, and `recv`.
+	`send`, and `recv`.
   + `select_spec` and `branch_spec`: proof rule for the derived (binary)
-    `select` and `branch` operations.
+	`select` and `branch` operations.
 
 ## Notation
 
@@ -47,7 +50,7 @@ and the Coq mechanization:
 
 Dependent Separation Protocols:
 
-|        | POPL paper                    | Coq mechanization                     |
+|        | 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`  |
@@ -57,16 +60,19 @@ Dependent Separation Protocols:
 | 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:
 
-|        | CONCUR 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 | `(+){ S_1 .. S_n }`           | `lty_choice SEND Ss`                  |
-| Branch | `&{ S_1 .. S_n }`             | `lty_choice RECV Ss`                  |
-| Dual   | An overlined protocol         | No notation                           |
+|          | 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
 
@@ -129,39 +135,52 @@ The logical relation is defined across the following files:
   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),
+  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. As mentioned, recursive session types can be defined using
-  the mechanism defined in [theories/logrel/model.v](theories/logrel/model.v).
-- [theories/logrel/environments.v](theories/logrel/environments.v):
-  Definition of semantic type environments, which are used in the semantic
-  typing relation. This also contains the rules for splitting and copying of
-  environments, which is used for distributing affine resources across the
-  various parts of the program inside the typing rules.
+  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.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.v):
+- [theories/logrel/session_typing_rules.v](theories/logrel/session_typing_rules.v):
   Semantic typing lemmas (typing rules) for the semantic session types.
-- [theories/logrel/subtyping_rules.v](theories/logrel/subtyping_rules.v):
-  Subtyping rules for term types and 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 resource shared between multiple
-threads.
+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 CONCUR 2020 submission, see
-[papers/CONCUR20.md](papers/CONCUR20.md).
+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/skip.v
-theories/utils/llist.v
-theories/utils/compare.v
-theories/utils/contribution.v
-theories/utils/group.v
-theories/utils/cofe_solver_2.v
-theories/utils/switch.v
-theories/channel/proto_model.v
-theories/channel/proto.v
-theories/channel/channel.v
-theories/channel/proofmode.v
-theories/examples/basics.v
-theories/examples/sort.v
-theories/examples/sort_br_del.v
-theories/examples/sort_fg.v
-theories/examples/map.v
-theories/examples/map_reduce.v
-theories/examples/subprotocols.v
-theories/logrel/model.v
-theories/logrel/telescopes.v
-theories/logrel/subtyping.v
-theories/logrel/environments.v
-theories/logrel/term_types.v
-theories/logrel/session_types.v
-theories/logrel/operators.v
-theories/logrel/term_typing_judgment.v
-theories/logrel/subtyping_rules.v
-theories/logrel/term_typing_rules.v
-theories/logrel/lib/mutex.v
-theories/logrel/examples/double.v
-theories/logrel/examples/pair.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

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

@@ -21,13 +21,15 @@ In this file we define the three message-passing connectives:
 
 It is additionaly shown that the channel ownership [c ↣ prot] is closed under
 the subprotocol relation [⊑] *)
-From iris.heap_lang Require Export lifting notation.
-From iris.heap_lang Require Import proofmode.
+From iris.heap_lang Require Export primitive_laws notation.
+From iris.heap_lang Require Export proofmode.
 From iris.heap_lang.lib Require Import spin_lock.
 From actris.channel Require Export proto.
-From actris.utils Require Import llist skip.
+From actris.utils Require Import llist.
 Set Default Proof Using "Type".
 
+Local Existing Instance spin_lock.
+
 (** * The definition of the message-passing connectives *)
 Definition new_chan : val :=
   λ: <>,
@@ -36,17 +38,17 @@ Definition new_chan : val :=
      let: "lk" := newlock #() in
      ((("l","r"),"lk"), (("r","l"),"lk")).
 
-Definition start_chan : val := λ: "f",
+Definition fork_chan : val := λ: "f",
   let: "cc" := new_chan #() in
   Fork ("f" (Snd "cc"));; Fst "cc".
 
 Definition send : val :=
   λ: "c" "v",
     let: "lk" := Snd "c" in
-    acquire "lk";;
     let: "l" := Fst (Fst "c") in
+    let: "r" := Snd (Fst "c") in
+    acquire "lk";;
     lsnoc "l" "v";;
-    skipN (llength (Snd (Fst "c")));; (* "Ghost" operation for later stripping *)
     release "lk".
 
 Definition try_recv : val :=
@@ -66,55 +68,51 @@ Definition recv : val :=
 
 (** * Setup of Iris's cameras *)
 Class chanG Σ := {
-  chanG_lockG :> lockG Σ;
-  chanG_protoG :> protoG Σ val;
+  #[local] chanG_lockG :: lockG Σ;
+  #[local] chanG_protoG :: protoG Σ val;
 }.
-Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
-Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
+Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
+Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
-Record chan_name := ChanName {
-  chan_lock_name : gname;
-  chan_proto_name : proto_name;
-}.
-Instance chan_name_inhabited : Inhabited chan_name :=
-  populate (ChanName inhabitant inhabitant).
-Instance chan_name_eq_dec : EqDecision chan_name.
-Proof. solve_decision. Qed.
-Instance chan_name_countable : Countable chan_name.
-Proof.
- refine (inj_countable (λ '(ChanName γl γr), (γl,γr))
-   (λ '(γl, γr), Some (ChanName γl γr)) _); by intros [].
-Qed.
-
-(** * Definition of the mapsto connective *)
+(** * Definition of the pointsto connective *)
 Notation iProto Σ := (iProto Σ val).
 Notation iMsg Σ := (iMsg Σ val).
 
-Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
+Definition iProto_lock_inv `{!heapGS Σ, !chanG Σ}
+    (l r : loc) (γl γr : gname) : iProp Σ :=
+  ∃ vsl vsr,
+    llist internal_eq l vsl ∗
+    llist internal_eq r vsr ∗
+    steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
+    iProto_ctx γl γr vsl vsr.
+
+Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
     (c : val) (p : iProto Σ) : iProp Σ :=
-  ∃ γ s (l r : loc) (lk : val),
-    ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
-    is_lock (chan_lock_name γ) lk (∃ vsl vsr,
-      llist sbi_internal_eq l vsl ∗
-      llist sbi_internal_eq r vsr ∗
-      iProto_ctx (chan_proto_name γ) vsl vsr) ∗
-    iProto_own (chan_proto_name γ) s p.
-Definition iProto_mapsto_aux : seal (@iProto_mapsto_def). by eexists. Qed.
-Definition iProto_mapsto := iProto_mapsto_aux.(unseal).
-Definition iProto_mapsto_eq :
-  @iProto_mapsto = @iProto_mapsto_def := iProto_mapsto_aux.(seal_eq).
-Arguments iProto_mapsto {_ _ _} _ _%proto.
-Instance: Params (@iProto_mapsto) 4 := {}.
-Notation "c ↣ p" := (iProto_mapsto c p)
+  ∃ γl γr γlk (l r : loc) (lk : val),
+    ⌜ c = ((#l, #r), lk)%V ⌝ ∗
+    is_lock γlk lk (iProto_lock_inv l r γl γr) ∗
+    iProto_own γl p.
+
+Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
+Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
+Definition iProto_pointsto_eq :
+  @iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
+Arguments iProto_pointsto {_ _ _} _ _%_proto.
+Global Instance: Params (@iProto_pointsto) 4 := {}.
+Notation "c ↣ p" := (iProto_pointsto c p)
   (at level 20, format "c  ↣  p").
 
+Global Instance iProto_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.
-Typeclasses Opaque iProto_choice.
-Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
-Instance: Params (@iProto_choice) 2 := {}.
+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.
@@ -125,19 +123,19 @@ 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 `{!heapG Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
   Implicit Types p : iProto Σ.
   Implicit Types TT : tele.
 
-  Global Instance iProto_mapsto_ne c : NonExpansive (iProto_mapsto c).
-  Proof. rewrite iProto_mapsto_eq. solve_proper. Qed.
-  Global Instance iProto_mapsto_proper c : Proper ((≡) ==> (≡)) (iProto_mapsto c).
+  Global Instance iProto_pointsto_ne c : NonExpansive (iProto_pointsto c).
+  Proof. rewrite iProto_pointsto_eq. solve_proper. Qed.
+  Global Instance iProto_pointsto_proper c : Proper ((≡) ==> (≡)) (iProto_pointsto c).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
+  Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
   Proof.
-    rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
-    iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+    rewrite iProto_pointsto_eq. iDestruct 1 as (γl γr γlk l r lk ->) "[Hlk H]".
+    iIntros "Hle'". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
     by iApply (iProto_own_le with "H").
   Qed.
 
@@ -152,6 +150,22 @@ Section channel.
     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).
@@ -177,35 +191,47 @@ Section channel.
       iDestruct ("H" with "HP") as "[$ ?]"; by iModIntro.
   Qed.
 
+  Lemma iProto_lock_inv_sym l r γl γr :
+    iProto_lock_inv l r γl γr ⊢ iProto_lock_inv r l γr γl.
+  Proof.
+    iIntros "(%vsl & %vsr & Hlistl & Hlistr & Hstepsl & Hstepsr & Hctx)".
+    iExists vsr, vsl. iFrame. by iApply iProto_ctx_sym.
+  Qed.
+
   (** ** Specifications of [send] and [recv] *)
   Lemma new_chan_spec p :
     {{{ True }}}
       new_chan #()
     {{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
   Proof.
-    iIntros (Φ _) "HΦ". wp_lam.
-    wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (l) "Hl".
-    wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (r) "Hr".
-    iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
-    wp_apply (newlock_spec (∃ vsl vsr,
-      llist sbi_internal_eq l vsl ∗ llist sbi_internal_eq r vsr ∗
-      iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
-    { iExists [], []. iFrame. }
+    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Φ".
-    set (γ := ChanName γlk γp). iSplitL "Hcl".
-    - rewrite iProto_mapsto_eq. iExists γ, Left, l, r, lk. by iFrame "Hcl #".
-    - rewrite iProto_mapsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
+    iSplitL "Hcl".
+    - rewrite iProto_pointsto_eq.
+      iExists γl, γr, γlk, l, r, lk. by iFrame "Hcl #".
+    - rewrite iProto_pointsto_eq.
+      iExists γr, γl, γlk, r, l, lk. iFrame "Hcr #".
+      iModIntro. iSplit; first done. iApply (is_lock_iff with "Hlk").
+      iIntros "!> !>". iSplit; iIntros; by iApply iProto_lock_inv_sym.
   Qed.
 
-  Lemma start_chan_spec p Φ (f : val) :
+  Lemma fork_chan_spec p Φ (f : val) :
     ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
     ▷ (∀ c, c ↣ p -∗ Φ c) -∗
-    WP start_chan f {{ Φ }}.
+    WP fork_chan f {{ Φ }}.
   Proof.
     iIntros "Hfork HΦ". wp_lam.
-    wp_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
-    wp_apply (wp_fork with "[Hfork Hc2]").
-    { iNext. wp_apply ("Hfork" with "Hc2"). }
+    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.
 
@@ -214,65 +240,74 @@ Section channel.
       send c v
     {{{ RET #(); c ↣ p }}}.
   Proof.
-    rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
-    wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
-    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
-    - iMod (iProto_send_l with "Hctx H []") as "[Hctx H]".
+    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. }
-      wp_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
-      wp_apply (llength_spec with "[$Hr //]"); iIntros "Hr".
-      wp_apply skipN_spec.
-      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
-    - iMod (iProto_send_r with "Hctx H []") as "[Hctx H]".
-      { rewrite iMsg_base_eq /=; auto. }
-      wp_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
-      wp_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
-      wp_apply skipN_spec.
-      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
+      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 }}}
+    {{{ 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) ∨
+    {{{ 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.
-    assert (∀ w lp (m : TT → iMsg Σ),
-      iMsg_car (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, iMsg_car (m x) w lp)) as iMsg_texist.
-    { intros w lp m. clear v P p. rewrite /iMsg_texist iMsg_exist_eq.
-      induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH. }
-    rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
-    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
-    wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
-    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
-    - wp_apply (lisnil_spec with "Hr"); iIntros "Hr".
-      destruct vsr as [|vr vsr]; wp_pures.
-      { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-        iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
-        iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
-      wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
-      iMod (iProto_recv_l with "Hctx H") as "H". wp_pures.
-      iMod "H" as (q) "(Hctx & H & Hm)".
-      rewrite iMsg_base_eq. iDestruct (iMsg_texist with "Hm") as (x <-) "[Hp HP]".
-      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
-      iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
-      by iRewrite "Hp".
-    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
-      destruct vsl as [|vl vsl]; wp_pures.
-      { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-        iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
-        iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
-      wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
-      iMod (iProto_recv_r with "Hctx H") as "H". wp_pures.
-      iMod "H" as (q) "(Hctx & H & Hm)".
-      rewrite iMsg_base_eq. iDestruct (iMsg_texist with "Hm") as (x <-) "[Hp HP]".
-      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
-      iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
-      iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+    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.
 
@@ -282,9 +317,9 @@ Section channel.
     {{{ x, RET v x; c ↣ p x ∗ P x }}}.
   Proof.
     iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
-    wp_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
+    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Φ". iFrame.
+    iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
   Qed.
 
   (** ** Specifications for choice *)
@@ -295,7 +330,7 @@ Section channel.
   Proof.
     rewrite /iProto_choice. iIntros (Φ) "[Hc HP] HΦ".
     iApply (send_spec with "[Hc HP] HΦ").
-    iApply (iProto_mapsto_le with "Hc").
+    iApply (iProto_pointsto_le with "Hc").
     iIntros "!>". iExists b. by iFrame "HP".
   Qed.
 
@@ -308,7 +343,7 @@ Section channel.
     iApply (recv_spec _ (tele_app _)
       (tele_app (TT:=[tele _ : bool]) (λ b, if b then P1 else P2))%I
       (tele_app _) with "[Hc]").
-    { iApply (iProto_mapsto_le with "Hc").
+    { iApply (iProto_pointsto_le with "Hc").
       iIntros "!> /=" (b) "HP". iExists b. by iSplitL. }
     rewrite -bi_tforall_forall.
     iIntros "!>" (x) "[Hc H]". iApply "HΦ". iFrame.

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

@@ -34,133 +34,135 @@ The defined functions on the type [proto] are:
 - [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 tactics.
+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.
-  Instance action_inhabited : Inhabited action := populate Send.
+  Global Instance action_inhabited : Inhabited action := populate Send.
   Definition action_dual (a : action) : action :=
     match a with Send => Recv | Recv => Send end.
-  Instance action_dual_involutive : Involutive (=) action_dual.
+  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 : ofeT) (A : ofeT) : ofeT :=
+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 : ofeT) : oFunctor :=
+Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
   optionOF (actionO * (V -d> ▶ ∙ -n> PROP)).
 
-Definition proto_result (V : Type) := result_2 (proto_auxOF V).
-Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
-  proto_result V PROPn _ PROP _.
-Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn 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_auxO V PROP (proto V PROP PROPn)) (proto V PROPn PROP).
-Proof. apply proto_result. Qed.
+  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} :
-  proto_auxO V PROP (proto V PROP PROPn) -n> proto V PROPn PROP := ofe_iso_1 proto_iso.
+  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> proto_auxO V PROP (proto V PROP PROPn) := ofe_iso_2 proto_iso.
+  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_12 proto_iso). Qed.
-Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
-    (p : proto_auxO V PROP (proto V PROP PROPn)) :
-  proto_unfold (proto_fold 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 :=
-  proto_fold None.
+  None.
 Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
     (m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
-  proto_fold (Some (a, m)).
+  Some (a, λ v, m v ◎ laterO_map proto_fold).
 
-Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
+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. f_equiv. by repeat constructor. Qed.
-Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe 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. f_equiv. by repeat constructor. Qed.
+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 (proto_unfold p) as [[a m]|] eqn:E; simpl in *; last first.
-  - left. by rewrite -(proto_fold_unfold p) E.
-  - right. exists a, m. by rewrite /proto_message -E proto_fold_unfold.
+  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.
-Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
+Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
   Inhabited (proto V PROPn PROP) := populate proto_end.
 
-Lemma proto_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
+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.
-  trans (proto_unfold (proto_message a1 m1) ≡ proto_unfold (proto_message a2 m2) : SPROP)%I.
-  { iSplit.
-    - iIntros "Heq". by iRewrite "Heq".
-    - iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
-      iRewrite "Heq". by rewrite proto_fold_unfold. }
-  rewrite /proto_message !proto_unfold_fold bi.option_equivI bi.prod_equivI /=.
-  rewrite bi.discrete_eq bi.discrete_fun_equivI.
-  by setoid_rewrite bi.ofe_morO_equivI.
+  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 {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+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.
-  trans (proto_unfold (proto_message a m) ≡ proto_unfold proto_end : SPROP)%I.
-  { iIntros "Heq". by iRewrite "Heq". }
-  by rewrite /proto_message !proto_unfold_fold bi.option_equivI.
-Qed.
-Lemma proto_end_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+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 bi.internal_eq_sym proto_message_end_equivI. Qed.
+Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
 
-(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
-is contractive *)
 Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
     (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
     (p : proto V PROPn PROP) : A :=
-  match proto_unfold p with None => x | Some (a, m) => f a m end.
+  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 : ofeT}
+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 Hp. rewrite /proto_elim.
-  apply (_ : NonExpansive proto_unfold) in Hp
-    as [[a1 m1] [a2 m2] [-> ?]|]; simplify_eq/=; [|done].
-  apply Hf. destruct n; by simpl.
+  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 : ofeT}
+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.
-  rewrite /proto_elim /proto_end.
-  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
-  by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
-Qed.
-Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
-    (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
-    `{Hf : ∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)} a m :
+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.
-  rewrite /proto_elim /proto_message /=.
-  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
-    (PROP:=PROP) (Some (a, m))) as Hfold.
-  destruct (proto_unfold (proto_fold (Some (a, m))))
-    as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
-  by f_equiv=> v.
+  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 *)
@@ -173,13 +175,13 @@ Next Obligation.
   apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv.
 Qed.
 
-Instance proto_map_aux_contractive {V}
+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; destruct n as [|n]=> //=.
+  apply Next_contractive; by dist_later_intro as n' Hn'.
 Qed.
 
 Definition proto_map_aux_2 {V}
@@ -188,7 +190,7 @@ Definition proto_map_aux_2 {V}
     (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).
-Instance proto_map_aux_2_contractive {V}
+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).
@@ -211,20 +213,20 @@ Proof.
   induction (lt_wf n) as [n _ IH]=>
     PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
   etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
-  apply proto_map_aux_contractive; destruct n as [|n]; [done|]; simpl.
-  symmetry. apply: IH. lia.
+  apply proto_map_aux_contractive; constructor=> n' ?. symmetry. by apply: IH.
 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 /= proto_elim_end. Qed.
+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 /=.
-  apply: proto_elim_message=> a' m1 m2 Hm; f_equiv; solve_proper.
+  rewrite ->proto_elim_message; [done|].
+  intros a' m1 m2 Hm. f_equiv; solve_proper.
 Qed.
 
 Lemma proto_map_ne {V}
@@ -239,7 +241,7 @@ Proof.
   destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=.
   apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
-  apply Next_contractive; destruct n as [|n]=> //=; auto using dist_S with lia.
+  apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_lt.
 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 :
@@ -255,7 +257,7 @@ Proof.
   induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
   destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
-  apply Next_contractive; destruct n as [|n]=> //=; auto.
+  apply Next_contractive; dist_later_intro as n' Hn'; auto.
 Qed.
 Lemma proto_map_compose {V}
    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
@@ -270,7 +272,7 @@ Proof.
     PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
   destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
-  do 3 f_equiv. apply Next_contractive; destruct n as [|n]=> //=; auto.
+  do 3 f_equiv. apply Next_contractive; dist_later_intro as n' Hn'; simpl; auto.
 Qed.
 
 Program Definition protoOF (V : Type) (Fn F : oFunctor)
@@ -294,13 +296,14 @@ Next Obligation.
   apply proto_map_ext=> //= y; by rewrite ofe.oFunctor_map_compose.
 Qed.
 
-Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
+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 ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
-  apply proto_map_ne=> //= y;
-    [destruct n; [|destruct Hfg]; by apply oFunctor_map_contractive..].
+  intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
+  apply proto_map_ne=> y //=.
+  + apply HFn. dist_later_intro as n' Hn'. f_equiv; apply Hfg.
+  + apply HF. by dist_later_intro as n' Hn'.
 Qed.

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

-(** This file includes basic examples that each describe a unique feature of 
+(** 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" := start_chan (λ: "c'", send "c'" #42) in
+  let: "c" := fork_chan (λ: "c'", send "c'" #42) in
   recv "c".
 
 (** Tranfering References *)
 Definition prog_ref : val := λ: <>,
-  let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
+  let: "c" := fork_chan (λ: "c'", send "c'" (ref #42)) in
   ! (recv "c").
 
 (** Delegation, i.e. transfering channels *)
 Definition prog_del : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
     send "c1'" (Fst "cc2");;
     send (Snd "cc2") #42) in
@@ -24,46 +26,43 @@ Definition prog_del : val := λ: <>,
 
 (** Dependent protocols *)
 Definition prog_dep : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "x" := recv "c'" in send "c'" ("x" + #2)) in
   send "c" #40;;
   recv "c".
 
 Definition prog_dep_ref : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "l" := recv "c'" in "l" <- !"l" + #2;; send "c'" #()) in
   let: "l" := ref #40 in send "c" "l";; recv "c";; !"l".
 
 Definition prog_dep_del : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
     send "c1'" (Fst "cc2");;
     let: "x" := recv (Snd "cc2") in send (Snd "cc2") ("x" + #2)) in
   let: "c2'" := recv "c1" in send "c2'" #40;; recv "c2'".
 
 Definition prog_dep_del_2 : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     send (recv "c1'") #40;;
     send "c1'" #()) in
-  let: "c2" := start_chan (λ: "c2'",
+  let: "c2" := fork_chan (λ: "c2'",
     let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
   send "c1" "c2";; recv "c1";; recv "c2".
 
 Definition prog_dep_del_3 : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "c" := recv "c1'" in let: "y" := recv "c1'" in
     send "c" "y";; send "c1'" #()) in
-  let: "c2" := start_chan (λ: "c2'",
+  let: "c2" := fork_chan (λ: "c2'",
     let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
   send "c1" "c2";; send "c1" #40;; recv "c1";; recv "c2".
 
 (** Loops *)
 Definition prog_loop : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
-    let: "go" :=
-      rec: "go" <> :=
-        let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" #() in
-    "go" #()) in
+  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;;
@@ -72,7 +71,7 @@ Definition prog_loop : val := λ: <>,
 
 (** Transfering higher-order functions *)
 Definition prog_fun : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
   let: "r" := ref #40 in
   send "c" (λ: <>, !"r");;
@@ -80,7 +79,7 @@ Definition prog_fun : val := λ: <>,
 
 (** Lock protected channel endpoints *)
 Definition prog_lock : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "l" := newlock #() in
     Fork (acquire "l";; send "c'" #21;; release "l");;
     acquire "l";; send "c'" #21;; release "l") in
@@ -88,15 +87,15 @@ Definition prog_lock : val := λ: <>,
 
 (** Swapping of sends *)
 Definition prog_swap : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     send "c'" #20;;
     let: "y" := recv "c'" in
-    send "c'" "y") in
-  send "c" #22;;
+    send "c'" ("y" + #2)) in
+  send "c" #20;;
   recv "c" + recv "c".
 
 Definition prog_swap_twice : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     send "c'" #20;;
     let: "y1" := recv "c'" in
     let: "y2" := recv "c'" in
@@ -104,8 +103,28 @@ Definition prog_swap_twice : val := λ: <>,
   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 `{heapG Σ, chanG Σ}.
+Context `{heapGS Σ, chanG Σ}.
 
 (** Protocols for the respective programs *)
 Definition prot : iProto Σ :=
@@ -147,6 +166,15 @@ 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 }}} }};
@@ -163,7 +191,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
 Definition prot_swap : iProto Σ :=
   (<! (x : Z)> MSG #x;
    <?> MSG #20;
-   <?> MSG #x; END)%proto.
+   <?> MSG #(x + 2); END)%proto.
 
 Definition prot_swap_twice : iProto Σ :=
   (<! (x : Z)> MSG #x;
@@ -171,11 +199,17 @@ Definition prot_swap_twice : iProto Σ :=
    <?> 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_apply (start_chan_spec prot); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot); iIntros (c) "Hc".
   - by wp_send with "[]".
   - wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -183,7 +217,7 @@ Qed.
 Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_ref); iIntros (c) "Hc".
   - wp_alloc l as "Hl". by wp_send with "[$Hl]".
   - wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
 Qed.
@@ -191,8 +225,8 @@ Qed.
 Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_del); iIntros (c) "Hc".
-  - wp_apply (new_chan_spec prot with "[//]").
+  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.
@@ -200,7 +234,7 @@ Qed.
 Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c) "Hc".
   - wp_recv (x) as "_". by wp_send with "[]".
   - wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -208,7 +242,7 @@ Qed.
 Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_ref); iIntros (c) "Hc".
   - wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
   - wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
     by iApply "HΦ".
@@ -217,8 +251,8 @@ Qed.
 Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
-  - wp_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
+  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Φ".
@@ -227,9 +261,9 @@ Qed.
 Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_del_2); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -237,10 +271,10 @@ Qed.
 Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_del_3); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_recv (y) as "_".
     wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_send with "[//]".
   wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -249,12 +283,10 @@ Qed.
 Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
-  - iAssert (∀ Ψ, WP (rec: "go" <> := let: "x" := recv c in
-      send c ("x" + #2) ;; "go" #())%V #() {{ Ψ }})%I with "[Hc]" as "H".
-    { iIntros (Ψ). iLöb as "IH". wp_recv (x) as "_". wp_send with "[//]".
-      wp_seq. by iApply "IH". }
-    wp_lam. wp_closure. wp_let. iApply "H".
+  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.
@@ -262,14 +294,14 @@ Qed.
 Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_fun); iIntros (c) "Hc".
   - wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
-    iIntros "!>" (Ψ') "HP HΨ'". wp_apply ("Hf" with "HP"); iIntros (x) "HΨ".
+    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_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
+    wp_recv (vg) as "#Hg". wp_smart_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
     by iApply "HΦ".
 Qed.
 
@@ -277,33 +309,33 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
   {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec (prot_lock 2)); iIntros (c) "Hc".
   - iMod contribution_init as (γ) "Hs".
     iMod (alloc_client with "Hs") as "[Hs Hcl1]".
     iMod (alloc_client with "Hs") as "[Hs Hcl2]".
-    wp_apply (newlock_spec (∃ n, server γ n ε ∗
+    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_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
+      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_apply (release_spec with "[$Hlk $Hl Hc Hs]"); eauto with iFrame. }
-    wp_apply (wp_fork with "[Hcl1]").
+      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_apply "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_apply (start_chan_spec prot_swap); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_swap); iIntros (c) "Hc".
   - wp_send with "[//]". wp_recv (x) as "_". by wp_send with "[//]".
   - wp_send with "[//]". wp_recv as "_". wp_recv as "_".
     wp_pures. by iApply "HΦ".
@@ -312,10 +344,39 @@ Qed.
 Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_apply (start_chan_spec prot_swap_twice); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_swap_twice); iIntros (c) "Hc".
   - wp_send with "[//]". wp_recv (x1) as "_". wp_recv (x2) as "_".
     by wp_send with "[//]".
   - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
     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

@@ -2,14 +2,14 @@
 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) *)
 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 (aka the implementation) *)
 Definition par_map_reduce_map : val :=
@@ -60,11 +60,11 @@ Definition par_map_reduce_reduce : val :=
 Definition cmpZfst : val := λ: "x" "y", Fst "x" ≤ Fst "y".
 
 Definition par_map_reduce : val := λ: "n" "m" "map" "red" "xs",
-  let: "cmap" := start_chan (λ: "c", par_map_service "n" "map" "c") in
-  let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in
+  let: "cmap" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
+  let: "csort" := fork_chan (λ: "c", sort_service_fg cmpZfst "c") in
   par_map_reduce_map "n" "cmap" "csort" "xs";;
   send "csort" #stop;;
-  let: "cred" := start_chan (λ: "c", par_map_service "m" "red" "c") in
+  let: "cred" := fork_chan (λ: "c", par_map_service "m" "red" "c") in
   (* We need the first sorted element in the loop to compare subsequent elements *)
   if: ~recv "csort" then #() else (* Handle the empty case *)
   let: "jy" := recv "csort" in
@@ -76,7 +76,7 @@ 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.
@@ -90,13 +90,13 @@ End map_reduce.
 
 (** * Correctness proofs of the distributed version *)
 Class map_reduceG Σ A B `{Countable A, Countable B} := {
-  map_reduce_mapG :> mapG Σ A;
-  map_reduce_reduceG :> mapG Σ (Z * list B);
+  map_reduce_mapG :: mapG Σ A;
+  map_reduce_reduceG :: mapG Σ (Z * list B);
 }.
 
 Section mapper.
   Context `{Countable A, Countable B} {C : Type}.
-  Context `{!heapG Σ, !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)}.
@@ -142,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.
@@ -188,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.
@@ -211,7 +211,7 @@ Section mapper.
       inversion 1 as [|?? [? _]]; discriminate_list || simplify_list_eq.
       assert (RZB (j',y') (i,y'')) as [??]; last (simpl in *; lia).
       apply (Sorted_StronglySorted _) in Hsort.
-      eapply elem_of_StronglySorted_app; set_solver.
+      eapply StronglySorted_app; set_solver.
   Qed.
 
   Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred :
@@ -224,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.
@@ -239,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]".
@@ -261,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.
@@ -275,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_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_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_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

@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import llist contribution.
 From iris.algebra Require Import gmultiset.
 
+Local Existing Instance spin_lock.
+
 (** * Distributed version (aka the implementation) *)
 Definition par_map_worker : val :=
   rec: "go" "map" "l" "c" :=
@@ -47,20 +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 Σ, !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.
@@ -72,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.
+         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.
@@ -96,7 +98,7 @@ Section map.
   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 %?.
@@ -104,28 +106,27 @@ 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 :
@@ -139,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 :
@@ -153,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 (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 :
@@ -172,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.
@@ -202,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_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

@@ -24,8 +24,8 @@ Definition sort_service : val :=
     let: "xs" := recv "c" in
     if: llength "xs" ≤ #1 then send "c" #() else
     let: "zs" := lsplit "xs" in
-    let: "cy" := start_chan (λ: "c", "go" "cmp" "c") in
-    let: "cz" := start_chan (λ: "c", "go" "cmp" "c") in
+    let: "cy" := fork_chan (λ: "c", "go" "cmp" "c") in
+    let: "cz" := fork_chan (λ: "c", "go" "cmp" "c") in
     send "cy" "xs";;
     send "cz" "zs";;
     recv "cy";; recv "cz";;
@@ -37,12 +37,12 @@ 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 Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
 
   Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop) : iProto Σ :=
     (<! (xs : list A) (l : loc)> MSG #l {{ llist I l xs }};
@@ -51,7 +51,7 @@ Section sort.
 
   Definition sort_protocol_func : iProto Σ :=
     (<! A (I : A → val → iProp Σ) (R : A → A → Prop)
-         `{!RelDecision R, !Total R} (cmp : val)>
+         `(!RelDecision R, !Total R) (cmp : val)>
        MSG cmp {{ cmp_spec I R cmp }};
      sort_protocol I R)%proto.
 
@@ -64,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)
@@ -98,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_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_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 _).
@@ -130,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
@@ -141,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_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_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

@@ -20,7 +20,7 @@ Definition sort_service_br : val :=
 Definition sort_service_del : val :=
   rec: "go" "cmp" "c" :=
     if: ~recv "c" then #() else
-    send "c" (start_chan (λ: "c", sort_service "cmp" "c"));;
+    send "c" (fork_chan (λ: "c", sort_service "cmp" "c"));;
     "go" "cmp" "c".
 
 Definition sort_service_br_del : val :=
@@ -29,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 Σ, !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 Σ :=
@@ -54,8 +54,8 @@ 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.
 
@@ -76,9 +76,9 @@ 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_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.
 
@@ -99,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_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.

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

@@ -42,8 +42,8 @@ Definition sort_service_fg : val :=
     let: "x" := recv "c" in
     if: ~(recv "c") then send "c" #cont;; send "c" "x";; send "c" #stop else
     let: "y" := recv "c" in
-    let: "c1" := start_chan (λ: "c", "go" "cmp" "c") in
-    let: "c2" := start_chan (λ: "c", "go" "cmp" "c") in
+    let: "c1" := fork_chan (λ: "c", "go" "cmp" "c") in
+    let: "c2" := fork_chan (λ: "c", "go" "cmp" "c") in
     send "c1" #cont;; send "c1" "x";;
     send "c2" #cont;; send "c2" "y";;
     sort_service_fg_split "c" "c1" "c2";;
@@ -66,13 +66,13 @@ Definition recv_all : val :=
     "go" "c" "ys";; lcons "x" "ys".
 
 Definition sort_client_fg : val := λ: "cmp" "xs",
-  let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
+  let: "c" := fork_chan (λ: "c", sort_service_fg "cmp" "c") in
   send_all "c" "xs";;
   send "c" #stop;;
   recv_all "c" "xs".
 
 Section sort_fg.
-  Context `{!heapG Σ, !chanG Σ}.
+  Context `{!heapGS Σ, !chanG Σ}.
 
   Section sort_fg_inner.
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
@@ -126,7 +126,7 @@ Section sort_fg.
     iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
     wp_rec. wp_branch.
     - wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
-      wp_apply ("IH" with "Hc Hc2 Hc1").
+      wp_smart_apply ("IH" with "Hc Hc2 Hc1").
       iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
       rewrite -!(assoc_L (++)).
       iApply "HΨ". iFrame "Hc Hc1 Hc2". by rewrite Hxs' (comm (++) xs1') assoc_L.
@@ -148,10 +148,10 @@ Section sort_fg.
   Proof.
     iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
     iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
-    wp_rec. wp_branch as %_ | %Hys'.
+    wp_rec. wp_branch as % _ | %Hys'.
     - wp_recv (x v) as (Htl) "HI".
       wp_select. wp_send with "[$HI]"; first by auto.
-      wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
+      wp_smart_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
       * done.
       * by rewrite Hys -!assoc_L (comm _ zs).
       * auto using Sorted_snoc.
@@ -159,7 +159,7 @@ Section sort_fg.
         inversion 1; discriminate_list || simplify_list_eq. by constructor.
     - wp_select with "[]".
       { by rewrite /= Hys Hxs Hys'. }
-      iApply "HΨ". iFrame.
+      iApply "HΨ". by iFrame.
   Qed.
 
   Lemma sort_service_fg_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
@@ -181,12 +181,12 @@ Section sort_fg.
     iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
     iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
     iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
-    wp_rec. wp_branch as %_ | %Hys2.
+    wp_rec. wp_branch as % _ | %Hys2.
     - wp_recv (x v) as (Htl2) "HIx".
-      wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
+      wp_pures. wp_smart_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
       case_bool_decide.
       + wp_select. wp_send with "[$HIy1 //]".
-        wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
+        wp_smart_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
         * by rewrite comm.
         * by rewrite assoc (comm _ ys2) Hys.
         * by apply Sorted_snoc.
@@ -195,14 +195,14 @@ Section sort_fg.
           inversion 1; discriminate_list || simplify_list_eq. by constructor.
       + wp_select. wp_send with "[$HIx]".
         { iPureIntro. by apply Htl_le, total_not. }
-        wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
+        wp_smart_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
         * by rewrite Hys assoc.
         * by apply Sorted_snoc, Htl_le, total_not.
         * constructor. by apply total_not.
         * intros x'.
           inversion 1; discriminate_list || simplify_list_eq. by constructor.
     - wp_select. wp_send with "[$HIy1 //]".
-      wp_apply (sort_service_fg_forward_spec with "[$Hc $Hc1]").
+      wp_smart_apply (sort_service_fg_forward_spec with "[$Hc $Hc1]").
       * done.
       * by rewrite Hys Hys2 -!assoc_L (comm _ xs2).
       * by apply Sorted_snoc.
@@ -221,19 +221,19 @@ Section sort_fg.
     wp_rec; wp_pures. wp_branch; wp_pures.
     - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
       + wp_recv (x2 v2) as "HIx2".
-        wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
-        { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
+        wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
+        { iIntros (cy) "Hcy". wp_smart_apply ("IH" with "Hcy"). auto. }
         iIntros (cy) "Hcy".
-        wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
-        { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
+        wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
+        { iIntros (cz) "Hcz". wp_smart_apply ("IH" with "Hcz"); auto. }
         iIntros (cz) "Hcz". rewrite !right_id.
         wp_select. wp_send with "[$HIx1]".
         wp_select. wp_send with "[$HIx2]".
-        wp_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
+        wp_smart_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
         iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
-        wp_branch as %_ | %[]%Permutation_nil_cons.
+        wp_branch as % _ | %[]%Permutation_nil_cons.
         wp_recv (x v) as "[_ HIx]".
-        wp_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
+        wp_smart_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
           with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
         by rewrite Hxs' Permutation_middle.
       + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
@@ -248,11 +248,11 @@ Section sort_fg.
   Proof.
     iIntros (Φ) "[Hl Hc] HΦ".
     iInduction xs as [|x xs] "IH" forall (xs').
-    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
-      iApply "HΦ". rewrite right_id_L. iFrame. }
-    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
-    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
-    wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
+    { wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
+      iApply "HΦ". rewrite right_id_L. by iFrame. }
+    wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
+    wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+    wp_send with "[$HIx]". wp_smart_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
   Qed.
 
   Lemma recv_all_spec c p l xs ys' :
@@ -265,11 +265,11 @@ Section sort_fg.
   Proof.
     iIntros (Hsort Φ) "[Hl Hc] HΦ".
     iLöb as "IH" forall (xs ys' Φ Hsort).
-    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
+    wp_lam. wp_branch as % _ | %Hperm; wp_pures.
     - wp_recv (y v) as (Htl) "HIx".
-      wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
+      wp_smart_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
       iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
-      wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl"; wp_pures.
+      wp_smart_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl".
       iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto.
     - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
   Qed.
@@ -281,11 +281,11 @@ Section sort_fg.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
-    { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
-    wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
+    wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
+    { wp_smart_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
+    wp_smart_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
     wp_select.
-    wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
+    wp_smart_apply (recv_all_spec with "[$Hl $Hc]"); auto.
     iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
     iApply "HΦ"; auto with iFrame.
   Qed.
@@ -294,7 +294,7 @@ Section sort_fg.
 
   Definition sort_fg_func_protocol : iProto Σ :=
     (<! A (I : A → val → iProp Σ) (R : A → A → Prop)
-         `{!RelDecision R, !Total R} (cmp : val)>
+         `(!RelDecision R, !Total R) (cmp : val)>
        MSG cmp {{ cmp_spec I R cmp }};
      sort_fg_head_protocol I R [])%proto.
 
@@ -305,6 +305,6 @@ Section sort_fg.
   Proof.
     iIntros (Ψ) "Hc HΨ". wp_lam.
     wp_recv (A I R ? ? cmp) as "#Hcmp".
-    by wp_apply (sort_service_fg_spec with "Hcmp Hc").
+    by wp_smart_apply (sort_service_fg_spec with "Hcmp Hc").
   Qed.
-End sort_fg.
\ No newline at end of file
+End sort_fg.

actris/examples/subprotocols.v

+From actris.channel Require Import proofmode proto channel.
+From iris.proofmode Require Import proofmode.
+
+Section subprotocol_basics.
+  Context `{heapGS Σ, chanG Σ}.
+
+  Lemma reference_example (l1' : loc) :
+    l1' ↦ #20 -∗
+    (<! (l1 l2 : loc)> MSG (#l1, #l2) {{ l1 ↦ #20 ∗ l2 ↦ #22 }}; END) ⊑
+    (<! (l2 : loc)> MSG (#l1', #l2) {{ l2 ↦ #22 }}; END).
+  Proof. iIntros "Hl1'" (l2) "Hl2". iExists l1', l2. by iFrame "Hl1' Hl2". Qed.
+
+  Lemma framing_example (P Q R : iProp Σ) (v w : val) :
+    ⊢ ((<!> MSG v {{ P }} ; <?> MSG w {{ Q }}; END)%proto ⊑
+       (<!> MSG v {{ P ∗ R }} ; <?> MSG w {{ Q ∗ R }};END)%proto)%proto.
+  Proof.
+    iIntros "[HP HR]". iFrame "HP". iModIntro.
+    iIntros "HQ". iFrame "HQ HR". eauto.
+  Qed.
+
+  Definition prot1_aux (prot : iProto Σ) : iProto Σ :=
+    (<! (x:Z)> MSG #x ; <?> MSG #(x+2) ; prot)%proto.
+  Definition prot2_aux (prot : iProto Σ) : iProto Σ :=
+    (<! (x:Z)> MSG #x ; <! (y:Z)> MSG #y ;
+     <?> MSG #(x+2) ; <?> MSG #(y+2) ; prot)%proto.
+
+  Instance prot1_aux_contractive : Contractive prot1_aux.
+  Proof. solve_proto_contractive. Qed.
+  Instance prot2_aux_contractive : Contractive prot2_aux.
+  Proof. solve_proto_contractive. Qed.
+
+  Definition prot1 : iProto Σ := fixpoint prot1_aux.
+  Definition prot2 : iProto Σ := fixpoint prot2_aux.
+
+  Lemma nonstructural_recursion_example :
+    ⊢ prot1 ⊑ prot2.
+  Proof.
+    iLöb as "IH".
+    iEval (rewrite /prot1 /prot2).
+    do 2 rewrite (fixpoint_unfold prot1_aux).
+    rewrite (fixpoint_unfold prot2_aux).
+    iIntros (x). iExists x. iModIntro.
+    iIntros (y).
+    iApply (iProto_le_trans).
+    { iModIntro. iExists y. iApply iProto_le_refl. }
+    iApply iProto_le_trans; [ iApply iProto_le_base_swap | ].
+    iModIntro. iModIntro. iModIntro.
+    iApply "IH".
+  Qed.
+
+  Fixpoint is_list (v : val) (ws : list val) : iProp Σ :=
+    match ws with
+    | []    => True
+    | w::ws => ∃ (v' : val), ⌜v = PairV w v'⌝ ∗ is_list v' ws
+  end.
+
+  Fixpoint is_int_list (v : val) (xs : list Z) : iProp Σ :=
+    match xs with
+    | []    => True
+    | x::xs => ∃ (v' : val), ⌜v = PairV (LitV $ LitInt $ x) v'⌝ ∗ is_int_list v' xs
+  end.
+
+  Lemma is_list_int_list v xs :
+    is_int_list v xs -∗ ∃ (ws : list val), is_list v ws ∗
+                        [∗ list] i↦x;w ∈ xs;ws, ⌜LitV $ LitInt $ x = w⌝%I.
+  Proof.
+    iIntros "H".
+    iInduction (xs) as [|x xs] "IH" forall (v).
+    { iExists []; eauto. }
+    iDestruct "H" as (v' ->) "H".
+    iDestruct ("IH" with "H") as (ws) "[Hlist Heq]".
+    iExists (#x :: ws); simpl; eauto.
+  Qed.
+
+  Lemma list_length_example :
+    ⊢ (<? (v:val) (xs : list Z)> MSG v {{ is_int_list v xs }} ;
+       <!> MSG #(length xs) ; END) ⊑
+      (<? (v:val) (ws : list val)> MSG v {{ is_list v ws }} ;
+       <!> MSG #(length ws) ; END).
+  Proof.
+    iIntros (v xs) "H".
+    iDestruct (is_list_int_list with "H") as (ws) "[H Hlen]".
+    iDestruct (big_sepL2_length with "Hlen") as %Hlen.
+    iExists v, ws. iFrame "H".
+    iModIntro. rewrite Hlen. eauto.
+  Qed.
+
+End subprotocol_basics.