Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • tlsomers/actris
  • iris/actris
  • dfrumin/actris
3 results
Show changes
Commits on Source (642)
542 additional commits have been omitted to prevent performance issues.
Hide whitespace changes
Inline Side-by-side
Showing
with 3676 additions and 292 deletions
.gitattributes 0 → 100644
View file @ c9249305
*.v gitlab-language=coq
.gitignore
View file @ c9249305
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
......@@ -11,7 +13,9 @@
*.bak
.coqdeps.d
.coq-native/
build-dep/
builddep/
Makefile.coq
Makefile.coq.conf
.Makefile.coq.d
*.crashcoqide
_opam
.gitlab-ci.yml 0 → 100644
View file @ c9249305
image: ralfjung/opam-ci:opam2
stages:
- build
variables:
CPU_CORES: "10"
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
.template: &template
stage: build
tags:
- fp
script:
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
- _opam/
only:
- master@iris/actris
- /^ci/@iris/actris
except:
- triggers
- schedules
- api
## Build jobs
build-coq.8.20.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.20.0"
DENY_WARNINGS: "1"
OPAM_PKG: "1"
tags:
- fp-timing
trigger-iris.dev:
<<: *template
variables:
STDPP_REPO: "iris/stdpp"
IRIS_REPO: "iris/iris"
OPAM_PINS: "coq version $NIGHTLY_COQ git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
except:
only:
- triggers
- schedules
- api
LICENSE
View file @ c9249305
All files in this development are distributed under the terms of the BSD
license, included below.
------------------------------------------------------------------------------
Copyright: Actris developers and contributors
BSD LICENCE
------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
......@@ -12,17 +12,17 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the
names of its contributors may be used to endorse or promote products
derived from this software without specific prior written permission.
* Neither the name of the copyright holder nor the names of its contributors
may be used to endorse or promote products derived from this software
without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Makefile
View file @ c9249305
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
# Default target
all: Makefile.coq
+@make -f Makefile.coq all
+@$(MAKE) -f Makefile.coq all
.PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@$(MAKE) -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
+@$(MAKE) -f Makefile.coq clean
@# Make sure not to enter the `_opam` folder.
find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache builddep/*
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies
build-dep/opam: opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
OPAMFILES=$(wildcard *.opam)
BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
builddep/%-builddep.opam: %.opam Makefile
@echo "# Creating builddep package for $<."
@mkdir -p builddep
@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
builddep-opamfiles: $(BUILDDEPFILES)
.PHONY: builddep-opamfiles
builddep: builddep-opamfiles
@# We want opam to not just install the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
@echo "# Installing builddep packages."
@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
.PHONY: builddep
# Backwards compatibility target
build-dep: builddep
.PHONY: build-dep
# Some files that do *not* need to be forwarded to Makefile.coq.
# ("::" lets Makefile.local overwrite this.)
Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
README.md
View file @ c9249305
# ACTRIS COQ DEVELOPMENT
This directory contains the artifact for the paper "Actris: Session Type
Based Reasoning in Separation Logic".
This repository contains:
- The Coq mechanization of the Actris framework, first presented in the paper
[Actris: Session Type Based Reasoning in Separation Logic](https://iris-project.org/pdfs/2020-popl-actris-final.pdf)
at POPL'20
- The logical relations model for a semantic session type system, first presented in
the paper
[Machine-Checked Semantic Session Typing](https://iris-project.org/pdfs/2021-cpp-sessions-final.pdf)
It has been built and tested with the following dependencies
- Coq 8.9.1
- [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp) at
commit 9041e6d8.
- [iris](https://gitlab.mpi-sws.org/iris/iris) at
commit 15f1ac56.
- Coq 8.18.0
- The version of Iris in the [opam file](opam)
In order to build, install the above dependencies and then run
`make -j [num CPU cores]` to compile Actris.
## Directory structure
### Theory
The theory can be found in `theories/channel`. Some used utilities can be found
in `theories/utils`.
The files correspond to the following content of the paper:
- `theories/channel/channel.v`: The definitional semantics of bidirectional
channels in HeapLang.
- `theories/channel/proto_model.v`: The CPS model of Dependent Separation
Protocols.
- `theories/channel/proto_channel.v`: The definition of the connective `↣` for
channel ownership and the proof rules of the Actris logic.
- `theories/channel/proofmode.v`: The Coq tactics for symbolic execution.
### Examples
The examples can be found in `theories/examples`.
The following list gives a mapping between the examples in the paper and their
mechanization in Coq:
* 1. Introduction: `theories/examples/basics.v`
* 2. Tour of Actris
* 2.3 Basic: `theories/examples/sort.v`
* 2.4 Higher-Order Functions: `theories/examples/sort.v`
* 2.5 Branching: `theories/examples/sort_br_del.v`
* 2.6 Recursion: `theories/examples/sort_br_del.v`
* 2.7 Delegation: `theories/examples/sort_br_del.v`
* 2.8 Dependent: `theories/examples/sort_fg.v`
* 3. Manifest sharing via locks
* 3.1 Sample program: `theories/examples/basics.v`
* 3.2 Distributed mapper: `theories/examples/map.v`
* 4. Case study: map reduce:
* Utilities for shuffling/grouping: `theories/utils/group.v`
* Implementation and verification: `theories/examples/map_reduce.v`
## Differences between the formalization and the paper
There are a number of small differences between the paper presentation
of Actris and the formalization in Coq, that are briefly discussed here.
### Connectives for physical ownership of channels
In the paper physical ownership of a channel is formalized using a single
connective `(c1,c2) ↣ (vs1,vs2)`, while the mechanisation has two connectives
for the endpoints and one for connecting them, namely:
- `chan_own γ Left vs1` and `chan_own γ Right vs1`
- `is_chan N γ c1 c2`
Where `γ` is a ghost name and `N` the invariant used internally. This setup is
less intuitive but gives rise to a more practical Jacobs/Piessens-style spec
of `recv` that does not need a closing view shift (to handle the case that
the buffer is empty).
### Later modalities in primitive rules for channels
The primitive rules for `send` and `recv` (`send_spec` and `recv_spec`) contain
three later modalities, which are omitted for brevity's sake in the paper. These
later modalities expose that these operations perform at least three steps in
the operational semantics, and are needed to deal with the three levels of
indirection in the invariant for protocols: 1.) the `▶` in the CPS encoding of
protocols, 2.) the higher-order ghost state used for ownership of protocols,
3.) the opening of the protocol invariant.
## Theory of Actris
The theory of Actris (semantics of channels, the model, and the proof rules)
can be found in the directory [theories/channel](theories/channel).
The individual types contain the following:
- [theories/channel/proto_model.v](theories/channel/proto_model.v): The
construction of the model of dependent separation protocols as the solution of
a recursive domain equation.
- [theories/channel/proto.v](theories/channel/proto.v): The instantiation of
protocols with the Iris logic, definition of `iProto_own` for channel endpoint
ownership, and lemmas corresponding to the Actris proof rules.
The relevant definitions and proof rules are as follows:
+ `iProto Σ`: The type of protocols.
+ `iProto_message`: The constructor for sends and receives.
+ `iProto_end`: The constructor for terminated protocols.
+ `iProto_le`: The subprotocol relation for protocols (notation `⊑`).
- [theories/channel/channel.v](theories/channel/channel.v): The encoding of
bidirectional channels in terms of Iris's HeapLang language, with specifications
defined in terms of the dependent separation protocols.
The relevant definitions and proof rules are as follows:
+ `iProto_pointsto`: endpoint ownership (notation `↣`).
+ `new_chan_spec`, `send_spec` and `recv_spec`: proof rule for `new_chan`,
`send`, and `recv`.
+ `select_spec` and `branch_spec`: proof rule for the derived (binary)
`select` and `branch` operations.
## Notation
The following table gives a mapping between the notation in literature
and the Coq mechanization:
Dependent Separation Protocols:
| | POPL20 paper | Coq mechanization |
|--------|-------------------------------|---------------------------------------|
| Send | `! x_1 .. x_n <v>{ P }. prot` | `<! x_1 .. x_n> MSG v {{ P }}; prot` |
| Recv | `? x_1 .. x_n <v>{ P }. prot` | `<? x_1 .. x_n> MSG v {{ P }}; prot` |
| End | `end` | `END` |
| Select | `prot_1 {Q_1}⊕{Q_2} prot_2` | `prot_1 <{Q_1}+{Q_2}> prot_2` |
| Branch | `prot_1 {Q_1}&{Q_2} prot_2` | `prot_1 <{Q_1}&{Q_2}> prot_2` |
| Append | `prot_1 · prot_2` | `prot_1 <++> prot_2` |
| Dual | An overlined protocol | No notation |
This notation is additionally used for the LMCS submission.
Semantic Session Types:
| | CPP21 submission | Coq mechanization |
|----------|-------------------------------|---------------------------------------|
| Send | `!_{X_1 .. X_n} A . S` | `<!! X_1 .. X_n> TY A ; S` |
| Recv | `?_{X_1 .. X_n} A . S` | `<?? X_1 .. X_n> TY A ; S` |
| End | `end` | `END` |
| Select | `(+){ Ss }` | `lty_choice SEND Ss` |
| Branch | `&{ Ss }` | `lty_choice RECV Ss` |
| Dual | An overlined type | No notation |
| N-append | `S^n` | lty_napp S n |
## Coq tactics
In order to prove programs using Actris, one can make use of a combination of
[Iris's symbolic execution tactics for HeapLang programs][HeapLang] and
[Actris's symbolic execution tactics for message passing][ActrisProofMode]. The
Actris tactics are as follows:
- `wp_send (t1 .. tn) with "selpat"`: symbolically execute `send c v` by looking
up ownership of a send protocol `H : c ↣ <!> y1 .. yn, MSG v; {{ P }}; prot`
in the proof mode context. The tactic instantiates the variables `y1 .. yn`
using the terms `t1 .. tn` and uses `selpat` to prove `P`. If fewer terms
`t` are given than variables `y`, they will be instantiated using existential
variables (evars). The tactic will put `H : c ↣ prot` back into the context.
- `wp_recv (x1 .. xn) as "ipat"`: symbolically execute `recv c` by looking up
`H : c ↣ <?> y1 .. yn, MSG v; {{ P }}; prot` in the proof mode context. The
variables `y1 .. yn` are introduced as `x1 .. xn`, and the predicate `P` is
introduced using the introduction pattern `ipat`. The tactic will put
`H : c ↣ prot` back into the context.
- `wp_select with "selpat"`: symbolically execute `select c b` by looking up
`H : c ↣ prot1 {Q1}<+>{Q2} prot2` in the proof mode context. The selection
pattern `selpat` is used to resolve either `Q1` or `Q2`, based on the chosen
branch `b`. The tactic will put `H : c ↣ prot1` or `H : c ↣ prot2` back
into the context based on the chosen branch `b`.
- `wp_branch as ipat1 | ipat2`: symbolically execute `branch c e1 e2` by looking
up `H : c ↣ prot1 {Q1}<&>{Q2} prot2` in the proof mode context. The result of
the tactic involves two subgoals, in which `Q1` and `Q2` are introduced using
the introduction patterns `ipat1` and `ipat2`, respectively. The tactic will
put `H : c ↣ prot1` and `H : c ↣ prot2` back into the contexts of the two
respectively goals.
The above tactics implicitly perform normalization of the protocol `prot` in
the hypothesis `H : c ↣ prot`. For example, `wp_send` also works if there is a
channel with the protocol `iProto_dual ((<?> y1 .. yn, MSG v; {{ P }}; END) <++> prot)`.
Concretely, the normalization performs the following actions:
- It re-associates appends (`<++>`), and removes left-identities (`END`) of it.
- It moves appends (`<++>`) into sends (`<!>`), receives (`<?>`), selections
(`<+>`) and branches (`<&>`).
- It distributes duals (`iProto_dual`) over append (`<++>`).
- It unfolds `prot1` into `prot2` if there is an instance of the type class
`ProtoUnfold prot1 prot2`. When defining a recursive protocol, it is
useful to define a `ProtoUnfold` instance to obtain automatic unfolding
of the recursive protocol. For example, see `sort_protocol_br_unfold` in
[theories/examples/sort_br_del.v](theories/examples/sort_br_del.v).
[HeapLang]: https://gitlab.mpi-sws.org/iris/iris/blob/master/HeapLang.md
[ProofMode]: https://gitlab.mpi-sws.org/iris/iris/blob/master/ProofMode.md
[ActrisProofMode]: theories/channel/proofmode.v
## Semantic Session Type System
The logical relation for type safety of a semantic session type system is contained
in the directory [theories/logrel](theories/logrel).
The logical relation is defined across the following files:
- [theories/logrel/model.v](theories/logrel/model.v): Definition of the
notions of a semantic term type and a semantic session type in terms of
unary Iris predicates (on values) and Actris protocols, respectively. Also
provides the required Coq definitions for creating recursive term/session
types.
- [theories/logrel/term_types.v](theories/logrel/term_types.v): Definitions
of the following semantic term types: basic types (integers, booleans, unit),
sums, products, copyable/affine functions, universally and existentially
quantified types, unique/shared references, and session-typed channels.
- [theories/logrel/session_types.v](theories/logrel/session_types.v):
Definitions of the following semantic session types: sending and receiving
with session polymorphism, n-ary choice. Session type duality is also
defined here. Recursive session types can be defined using the mechanism
defined in [theories/logrel/model.v](theories/logrel/model.v).
- [theories/logrel/operators.v](theories/logrel/operators.v):
Type definitions of unary and binary operators.
- [theories/logrel/contexts.v](theories/logrel/contexts.v):
Definition of the semantic type contexts, which is used in the semantic
typing relation. This also contains the rules for updating the context,
which is used for distributing affine resources across the
various parts of the proofs inside the typing rules.
- [theories/logrel/term_typing_judgment.v](theories/logrel/term_typing_judgment.v):
Definition of the semantic typing relation, as well as the proof of type
soundness, showing that semantically well-typed programs do not get stuck.
- [theories/logrel/subtyping.v](theories/logrel/subtyping.v):
Definition of the semantic subtyping relation for both term and session types.
This file also defines the notion of copyability of types in terms of subtyping.
- [theories/logrel/subtyping_rules.v](theories/logrel/subtyping_rules.v):
Subtyping rules for term types and session types.
- [theories/logrel/term_typing_rules.v](theories/logrel/term_typing_rules.v):
Semantic typing lemmas (typing rules) for the semantic term types.
- [theories/logrel/session_typing_rules.v](theories/logrel/session_typing_rules.v):
Semantic typing lemmas (typing rules) for the semantic session types.
- [theories/logrel/napp.v](theories/logrel/napp.v):
Definition of session types iteratively being appended to themselves a finite
number of times, with support for swapping e.g. a send over an arbitrary number
of receives.
An extension to the basic type system is given in
[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), which defines
mutexes as a type-safe abstraction. Mutexes are implemented using spin locks
and allow one to gain exclusive ownership of resources shared between multiple
threads. An encoding of a list type is found in
[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), along with axillary
lemmas, and a weakest precondition for `llength`,
that converts ownership of a list type into a list reference predicate, with
the values of the list made explicit.
## Paper-specific remarks
For remarks about the paper-specific submissions, see
- [papers/POPL20.md](papers/POPL20.md)
- [papers/CPP21.md](papers/CPP21.md)
- [papers/LMCS.md](papers/LMCS.md)
_CoqProject
View file @ c9249305
-Q theories actris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
theories/utils/auth_excl.v
theories/utils/llist.v
theories/utils/compare.v
theories/utils/contribution.v
theories/utils/group.v
theories/utils/misc.v
theories/channel/channel.v
theories/channel/proto_model.v
theories/channel/proto_channel.v
theories/channel/proofmode.v
theories/examples/basics.v
theories/examples/sort.v
theories/examples/sort_br_del.v
theories/examples/sort_fg.v
theories/examples/map.v
theories/examples/map_reduce.v
-Q actris actris
-Q multris multris
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-incompatible-prefix
# No common logical root, so we have to specify documentation root, to avoid warnings
-docroot actris
actris/utils/llist.v
actris/utils/compare.v
actris/utils/contribution.v
actris/utils/group.v
actris/utils/cofe_solver_2.v
actris/utils/switch.v
actris/channel/proto_model.v
actris/channel/proto.v
actris/channel/channel.v
actris/channel/proofmode.v
actris/examples/basics.v
actris/examples/equivalence.v
actris/examples/sort.v
actris/examples/sort_br_del.v
actris/examples/sort_fg.v
actris/examples/par_map.v
actris/examples/map_reduce.v
actris/examples/swap_mapper.v
actris/examples/subprotocols.v
actris/examples/list_rev.v
actris/examples/rpc.v
actris/examples/pizza.v
actris/logrel/model.v
actris/logrel/telescopes.v
actris/logrel/subtyping.v
actris/logrel/contexts.v
actris/logrel/term_types.v
actris/logrel/session_types.v
actris/logrel/operators.v
actris/logrel/term_typing_judgment.v
actris/logrel/subtyping_rules.v
actris/logrel/term_typing_rules.v
actris/logrel/session_typing_rules.v
actris/logrel/napp.v
actris/logrel/lib/mutex.v
actris/logrel/lib/list.v
actris/logrel/lib/par_start.v
actris/logrel/examples/pair.v
actris/logrel/examples/par_recv.v
actris/logrel/examples/rec_subtyping.v
actris/logrel/examples/choice_subtyping.v
actris/logrel/examples/mapper.v
actris/logrel/examples/mapper_list.v
actris/logrel/examples/compute_service.v
actris/logrel/examples/compute_client_list.v
multris/utils/cofe_solver_2.v
multris/utils/matrix.v
multris/channel/proto_model.v
multris/channel/proto.v
multris/channel/channel.v
multris/channel/proofmode.v
multris/examples/basics.v
multris/examples/two_buyer.v
multris/examples/three_buyer.v
multris/examples/leader_election.v
actris/channel/channel.v 0 → 100644
View file @ c9249305
(** This file contains the definition of the channels, encoded as a pair of
lock-protected buffers, and their primitive proof rules. Moreover:
- It defines the connective [c ↣ prot] for ownership of channel endpoints,
which describes that channel endpoint [c] adheres to protocol [prot].
- It proves Actris's specifications of [send] and [recv] w.r.t. dependent
separation protocols.
An encoding of the usual (binary) choice connectives [prot1 <{Q1}+{Q2}> prot2]
and [prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in
this file.
In this file we define the three message-passing connectives:
- [new_chan] creates references to two empty buffers and a lock, and returns a
pair of endpoints, where the order of the two references determines the
polarity of the endpoints.
- [send] takes an endpoint and adds an element to the first buffer.
- [recv] performs a busy loop until there is something in the second buffer,
which it pops and returns, locking during each peek.
It is additionaly shown that the channel ownership [c ↣ prot] is closed under
the subprotocol relation [⊑] *)
From iris.heap_lang Require Export primitive_laws notation.
From iris.heap_lang Require Export proofmode.
From iris.heap_lang.lib Require Import spin_lock.
From actris.channel Require Export proto.
From actris.utils Require Import llist.
Set Default Proof Using "Type".
Local Existing Instance spin_lock.
(** * The definition of the message-passing connectives *)
Definition new_chan : val :=
λ: <>,
let: "l" := lnil #() in
let: "r" := lnil #() in
let: "lk" := newlock #() in
((("l","r"),"lk"), (("r","l"),"lk")).
Definition fork_chan : val := λ: "f",
let: "cc" := new_chan #() in
Fork ("f" (Snd "cc"));; Fst "cc".
Definition send : val :=
λ: "c" "v",
let: "lk" := Snd "c" in
let: "l" := Fst (Fst "c") in
let: "r" := Snd (Fst "c") in
acquire "lk";;
lsnoc "l" "v";;
release "lk".
Definition try_recv : val :=
λ: "c",
let: "lk" := Snd "c" in
acquire "lk";;
let: "l" := Snd (Fst "c") in
let: "ret" := if: lisnil "l" then NONE else SOME (lpop "l") in
release "lk";; "ret".
Definition recv : val :=
rec: "go" "c" :=
match: try_recv "c" with
SOME "p" => "p"
| NONE => "go" "c"
end.
(** * Setup of Iris's cameras *)
Class chanG Σ := {
#[local] chanG_lockG :: lockG Σ;
#[local] chanG_protoG :: protoG Σ val;
}.
Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
Proof. solve_inG. Qed.
(** * Definition of the pointsto connective *)
Notation iProto Σ := (iProto Σ val).
Notation iMsg Σ := (iMsg Σ val).
Definition iProto_lock_inv `{!heapGS Σ, !chanG Σ}
(l r : loc) (γl γr : gname) : iProp Σ :=
∃ vsl vsr,
llist internal_eq l vsl ∗
llist internal_eq r vsr ∗
steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
iProto_ctx γl γr vsl vsr.
Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
∃ γl γr γlk (l r : loc) (lk : val),
⌜ c = ((#l, #r), lk)%V ⌝ ∗
is_lock γlk lk (iProto_lock_inv l r γl γr) ∗
iProto_own γl p.
Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
Definition iProto_pointsto_eq :
@iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
Arguments iProto_pointsto {_ _ _} _ _%_proto.
Global Instance: Params (@iProto_pointsto) 4 := {}.
Notation "c ↣ p" := (iProto_pointsto c p)
(at level 20, format "c ↣ p").
Global Instance iProto_pointsto_contractive `{!heapGS Σ, !chanG Σ} c :
Contractive (iProto_pointsto c).
Proof. rewrite iProto_pointsto_eq. solve_contractive. Qed.
Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
(p1 p2 : iProto Σ) : iProto Σ :=
(<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
Global Typeclasses Opaque iProto_choice.
Arguments iProto_choice {_} _ _%_I _%_I _%_proto _%_proto.
Global Instance: Params (@iProto_choice) 2 := {}.
Infix "<{ P1 }+{ P2 }>" := (iProto_choice Send P1 P2) (at level 85) : proto_scope.
Infix "<{ P1 }&{ P2 }>" := (iProto_choice Recv P1 P2) (at level 85) : proto_scope.
Infix "<+{ P2 }>" := (iProto_choice Send True P2) (at level 85) : proto_scope.
Infix "<&{ P2 }>" := (iProto_choice Recv True P2) (at level 85) : proto_scope.
Infix "<{ P1 }+>" := (iProto_choice Send P1 True) (at level 85) : proto_scope.
Infix "<{ P1 }&>" := (iProto_choice Recv P1 True) (at level 85) : proto_scope.
Infix "<+>" := (iProto_choice Send True True) (at level 85) : proto_scope.
Infix "<&>" := (iProto_choice Recv True True) (at level 85) : proto_scope.
Section channel.
Context `{!heapGS Σ, !chanG Σ}.
Implicit Types p : iProto Σ.
Implicit Types TT : tele.
Global Instance iProto_pointsto_ne c : NonExpansive (iProto_pointsto c).
Proof. rewrite iProto_pointsto_eq. solve_proper. Qed.
Global Instance iProto_pointsto_proper c : Proper ((≡) ==> (≡)) (iProto_pointsto c).
Proof. apply (ne_proper _). Qed.
Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
Proof.
rewrite iProto_pointsto_eq. iDestruct 1 as (γl γr γlk l r lk ->) "[Hlk H]".
iIntros "Hle'". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
by iApply (iProto_own_le with "H").
Qed.
Global Instance iProto_choice_contractive n a :
Proper (dist n ==> dist n ==>
dist_later n ==> dist_later n ==> dist n) (@iProto_choice Σ a).
Proof. solve_contractive. Qed.
Global Instance iProto_choice_ne n a :
Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_choice Σ a).
Proof. solve_proper. Qed.
Global Instance iProto_choice_proper a :
Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_choice Σ a).
Proof. solve_proper. Qed.
Lemma iProto_choice_equiv a1 a2 (P11 P12 P21 P22 : iProp Σ)
(p11 p12 p21 p22 : iProto Σ) :
⌜a1 = a2⌝ -∗ ((P11 ≡ P12):iProp Σ) -∗ (P21 ≡ P22) -∗
▷ (p11 ≡ p12) -∗ ▷ (p21 ≡ p22) -∗
iProto_choice a1 P11 P21 p11 p21 ≡ iProto_choice a2 P12 P22 p12 p22.
Proof.
iIntros (->) "#HP1 #HP2 #Hp1 #Hp2".
rewrite /iProto_choice. iApply iProto_message_equiv; [ eauto | | ].
- iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
destruct b;
[ iRewrite -"HP1"; iFrame "H Hp1" | iRewrite -"HP2"; iFrame "H Hp2" ].
- iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
destruct b;
[ iRewrite "HP1"; iFrame "H Hp1" | iRewrite "HP2"; iFrame "H Hp2" ].
Qed.
Lemma iProto_dual_choice a P1 P2 p1 p2 :
iProto_dual (iProto_choice a P1 P2 p1 p2)
≡ iProto_choice (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
Proof.
rewrite /iProto_choice iProto_dual_message /= iMsg_dual_exist.
f_equiv; f_equiv=> -[]; by rewrite iMsg_dual_base.
Qed.
Lemma iProto_app_choice a P1 P2 p1 p2 q :
(iProto_choice a P1 P2 p1 p2 <++> q)%proto
≡ (iProto_choice a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
Proof.
rewrite /iProto_choice iProto_app_message /= iMsg_app_exist.
f_equiv; f_equiv=> -[]; by rewrite iMsg_app_base.
Qed.
Lemma iProto_le_choice a P1 P2 p1 p2 p1' p2' :
(P1 -∗ P1 ∗ ▷ (p1 ⊑ p1')) ∧ (P2 -∗ P2 ∗ ▷ (p2 ⊑ p2')) -∗
iProto_choice a P1 P2 p1 p2 ⊑ iProto_choice a P1 P2 p1' p2'.
Proof.
iIntros "H". rewrite /iProto_choice. destruct a;
iIntros (b) "HP"; iExists b; destruct b;
iDestruct ("H" with "HP") as "[$ ?]"; by iModIntro.
Qed.
Lemma iProto_lock_inv_sym l r γl γr :
iProto_lock_inv l r γl γr ⊢ iProto_lock_inv r l γr γl.
Proof.
iIntros "(%vsl & %vsr & Hlistl & Hlistr & Hstepsl & Hstepsr & Hctx)".
iExists vsr, vsl. iFrame. by iApply iProto_ctx_sym.
Qed.
(** ** Specifications of [send] and [recv] *)
Lemma new_chan_spec p :
{{{ True }}}
new_chan #()
{{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
Proof.
iIntros (Φ _) "HΦ". wp_lam. iMod (steps_lb_0) as "#Hlb".
wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
iMod (iProto_init p) as (γl γr) "(Hctx & Hcl & Hcr)".
wp_smart_apply (newlock_spec (∃ vsl vsr,
llist internal_eq l vsl ∗ llist internal_eq r vsr ∗
steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
iProto_ctx γl γr vsl vsr) with "[Hl Hr Hctx]").
{ iExists [], []. iFrame "#∗". }
iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
iSplitL "Hcl".
- rewrite iProto_pointsto_eq.
iExists γl, γr, γlk, l, r, lk. by iFrame "Hcl #".
- rewrite iProto_pointsto_eq.
iExists γr, γl, γlk, r, l, lk. iFrame "Hcr #".
iModIntro. iSplit; first done. iApply (is_lock_iff with "Hlk").
iIntros "!> !>". iSplit; iIntros; by iApply iProto_lock_inv_sym.
Qed.
Lemma fork_chan_spec p Φ (f : val) :
▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
▷ (∀ c, c ↣ p -∗ Φ c) -∗
WP fork_chan f {{ Φ }}.
Proof.
iIntros "Hfork HΦ". wp_lam.
wp_smart_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
wp_smart_apply (wp_fork with "[Hfork Hc2]").
{ iNext. wp_smart_apply ("Hfork" with "Hc2"). }
wp_pures. iApply ("HΦ" with "Hc1").
Qed.
Lemma send_spec c v p :
{{{ c ↣ <!> MSG v; p }}}
send c v
{{{ RET #(); c ↣ p }}}.
Proof.
rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (γl γr γlk l r lk ->) "[#Hlk H]"; wp_pures.
wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
wp_pures. wp_bind (lsnoc _ _).
iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
{ iApply fupd_mask_intro; [set_solver|]. simpl.
iIntros "Hclose !>!>".
iMod (iProto_send with "Hctx H []") as "[Hctx H]".
{ rewrite iMsg_base_eq /=; auto. }
iModIntro.
iApply step_fupdN_intro; [done|].
iIntros "!>". iMod "Hclose".
iCombine ("Hctx H") as "H".
iExact "H". }
iApply (wp_lb_update with "Hlbl").
wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
iIntros "#Hlbl' [Hctx H] !>".
wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
{ iExists (vsl ++ [v]), vsr.
rewrite length_app /=.
replace (length vsl + 1) with (S (length vsl)) by lia.
iFrame "#∗". }
iIntros "_". iApply "HΦ". iExists γl, γr, γlk. eauto 10 with iFrame.
Qed.
Lemma send_spec_tele {TT} c (tt : TT)
(v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
{{{ c ↣ (<!.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
send c (v tt)
{{{ RET #(); c ↣ (p tt) }}}.
Proof.
iIntros (Φ) "[Hc HP] HΦ".
iDestruct (iProto_pointsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
as "Hc".
{ iIntros "!>".
iApply iProto_le_trans.
iApply iProto_le_texist_intro_l.
by iFrame "HP". }
by iApply (send_spec with "Hc").
Qed.
Lemma try_recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
{{{ c ↣ <?.. x> MSG v x {{ P x }}; p x }}}
try_recv c
{{{ w, RET w; (⌜w = NONEV⌝ ∗ c ↣ <?.. x> MSG v x {{ P x }}; p x) ∨
(∃.. x, ⌜w = SOMEV (v x)⌝ ∗ c ↣ p x ∗ P x) }}}.
Proof.
rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (γl γr γlk l r lk ->) "[#Hlk H]"; wp_pures.
wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
destruct vsr as [|vr vsr]; wp_pures.
- wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
{ unfold iProto_lock_inv; by eauto with iFrame. }
iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
iExists γl, γr, γlk. eauto 10 with iFrame.
- wp_smart_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
iMod (iProto_recv with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
rewrite iMsg_base_eq.
iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
iDestruct (steps_lb_le _ (length vsr) with "Hlbr") as "#Hlbr'"; [lia|].
wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
{ unfold iProto_lock_inv; by eauto with iFrame. }
iIntros "_". wp_pures. iModIntro. iApply "HΦ".
iRight. iExists x. iSplit; [done|].
iFrame "HP". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
by iRewrite "Hp".
Qed.
Lemma recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
{{{ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x }}}
recv c
{{{ x, RET v x; c ↣ p x ∗ P x }}}.
Proof.
iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
wp_smart_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
{ wp_pures. by iApply ("IH" with "[$]"). }
iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
Qed.
(** ** Specifications for choice *)
Lemma select_spec c (b : bool) P1 P2 p1 p2 :
{{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}
send c #b
{{{ RET #(); c ↣ (if b then p1 else p2) }}}.
Proof.
rewrite /iProto_choice. iIntros (Φ) "[Hc HP] HΦ".
iApply (send_spec with "[Hc HP] HΦ").
iApply (iProto_pointsto_le with "Hc").
iIntros "!>". iExists b. by iFrame "HP".
Qed.
Lemma branch_spec c P1 P2 p1 p2 :
{{{ c ↣ (p1 <{P1}&{P2}> p2) }}}
recv c
{{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}.
Proof.
rewrite /iProto_choice. iIntros (Φ) "Hc HΦ".
iApply (recv_spec _ (tele_app _)
(tele_app (TT:=[tele _ : bool]) (λ b, if b then P1 else P2))%I
(tele_app _) with "[Hc]").
{ iApply (iProto_pointsto_le with "Hc").
iIntros "!> /=" (b) "HP". iExists b. by iSplitL. }
rewrite -bi_tforall_forall.
iIntros "!>" (x) "[Hc H]". iApply "HΦ". iFrame.
Qed.
End channel.
theories/channel/proofmode.v → actris/channel/proofmode.v
View file @ c9249305
(** This file contains tactics for the message-passing connectives,
as well as the necessary typeclasses.
This includes a way of reducing protocols to a normal form, to prepare
them for use in the appropriate specifications.
This normalisation includes e.g. resolving duals.
The tactics are:
- [wp_send (x1 .. xn) with "selpat"] which resolves weakest preconditions of the
form [wp (send c v) Q], in the presence of an ownership of a send protocol
[c ↣ <!> x .. y, MSG v; {{ P }}; prot] in the context. That is done by using
[x1 .. xn] to existentially quantify the variables [x .. y], and "ipat" to
resolve the predicate [P]. The result is continuing as [Q],
with [c ↣ prot] in the context.
- [wp_recv (x1 .. xn) as "ipat"] which conversely resolves [wp (recv c) Q] with
[c ↣ <?> x .. y, MSG v; {{ P }}; prot] in the context, where the variables
[x .. y] are introduced as [x1 .. xn], and the predicate [P] is introduces based
on the pattern [ipat].
- [wp_select with "selpat"] which resolves [wp (select c b) Q] with
[c ↣ prot1 {Q1}<+>{Q2} prot2] in the context. Here [selpat] is used to
resolve either [Q1] or [Q2], based on the chosen branch. The resulting
protocol is similarly [c ↣ prot1] or [c ↣ prot2] based on the chosen
branch.
- [wp_branch as ipat1 | ipat2] which resolves [wp (branch c e1 e2) Q] with
[c ↣ prot1 {Q1}<&>{Q2} prot2] in the context. The result is two subgoals,
in which [Q1] and [Q2] are introduced using [ipat1] and [ipat2], and the
protocol ownership is [c ↣ prot1] and [c ↣ prot2] respectively. *)
From iris.heap_lang Require Export proofmode notation.
From iris.proofmode Require Export tactics.
From actris Require Export proto_channel.
(** This file contains the definitions of Actris's tactics for symbolic
execution of message-passing programs. The API of these tactics is documented
in the [README.md] file. The implementation follows the same pattern for the
implementation of these tactics that is used in Iris. In addition, it uses a
standard pattern using type classes to perform the normalization.
In addition to the tactics for symbolic execution, this file defines the tactic
[solve_proto_contractive], which can be used to automatically prove that
recursive protocols are contractive. *)
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
From iris.heap_lang Require Export proofmode notation.
From actris Require Export channel.
(** Classes *)
Class ActionDualIf (d : bool) (a1 a2 : action) :=
dual_action_if : a2 = if d then action_dual a1 else a1.
Hint Mode ActionDualIf ! ! - : typeclass_instances.
(** Tactics for proving contractiveness of protocols *)
Ltac f_proto_contractive :=
(** * Tactics for proving contractiveness of protocols *)
Ltac f_dist_le :=
match goal with
| _ => apply iProto_branch_contractive
| _ => apply iProto_message_contractive; simpl; intros; [reflexivity|..]
| H : _ ≡{?n}≡ _ |- _ ≡{?n'}≡ _ => apply (dist_le n); [apply H|lia]
end;
try match goal with
| |- @dist_later ?A _ ?n ?x ?y =>
destruct n as [|n]; simpl in *; [exact Logic.I|change (@dist A _ n x y)]
end.
Ltac solve_proto_contractive :=
solve_proper_core ltac:(fun _ => first [f_contractive | f_proto_contractive | f_equiv]).
solve_proper_core ltac:(fun _ =>
first [f_contractive; simpl in * | f_equiv | f_dist_le]).
(** Normalization of protocols *)
Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
Instance action_dual_if_true_send : ActionDualIf true Send Receive := eq_refl.
Instance action_dual_if_true_receive : ActionDualIf true Receive Send := eq_refl.
(** * Normalization of protocols *)
Class ActionDualIf (d : bool) (a1 a2 : action) :=
dual_action_if : a2 = if d then action_dual a1 else a1.
Global Hint Mode ActionDualIf ! ! - : typeclass_instances.
Global Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
Global Instance action_dual_if_true_send : ActionDualIf true Send Recv := eq_refl.
Global Instance action_dual_if_true_recv : ActionDualIf true Recv Send := eq_refl.
Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
(pas : list (bool * iProto Σ)) (q : iProto Σ) :=
proto_normalize :
q ≡ (iProto_dual_if d p <++>
foldr (iProto_app ∘ curry iProto_dual_if) END pas)%proto.
Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
Class ProtoContNormalize {Σ TT} (d : bool) (pc : TT → val * iProp Σ * iProto Σ)
(pas : list (bool * iProto Σ)) (qc : TT → val * iProp Σ * iProto Σ) :=
proto_cont_normalize x :
(qc x).1.1 = (pc x).1.1 ∧
(qc x).1.2 ≡ (pc x).1.2 ∧
ProtoNormalize d ((pc x).2) pas ((qc x).2).
Hint Mode ProtoContNormalize ! ! ! ! ! - : typeclass_instances.
⊢ iProto_dual_if d p <++>
foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
Arguments ProtoNormalize {_} _ _%_proto _%_proto _%_proto.
Notation ProtoUnfold p1 p2 := (∀ d pas q,
ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
(pas : list (bool * iProto Σ)) (m2 : iMsg Σ) :=
msg_normalize a :
ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
Arguments MsgNormalize {_} _ _%_msg _%_msg _%_msg.
Section classes.
Context `{!proto_chanG Σ, !heapG Σ}.
Implicit Types p : iProto Σ.
Context `{!chanG Σ, !heapGS Σ}.
Implicit Types TT : tele.
Implicit Types p : iProto Σ.
Implicit Types m : iMsg Σ.
Implicit Types P : iProp Σ.
(** Classes *)
Lemma proto_unfold_eq p1 p2 : p1 ≡ p2 → ProtoUnfold p1 p2.
Proof. rewrite /ProtoNormalize=> Hp d pas q ->. by rewrite Hp. Qed.
Proof. rewrite /ProtoNormalize=> Hp d pas q. by rewrite Hp. Qed.
Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0.
Proof. by rewrite /ProtoNormalize /= right_id. Qed.
Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
Global Instance proto_normalize_done_dual p :
ProtoNormalize true p [] (iProto_dual p) | 0.
Proof. by rewrite /ProtoNormalize /= right_id. Qed.
Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
Global Instance proto_normalize_done_dual_end :
ProtoNormalize (Σ:=Σ) true END [] END | 0.
Proof. by rewrite /ProtoNormalize /= right_id iProto_dual_end. Qed.
Proof. rewrite /ProtoNormalize /= right_id iProto_dual_end. auto. Qed.
Global Instance proto_normalize_dual d p pas q :
ProtoNormalize (negb d) p pas q →
ProtoNormalize d (iProto_dual p) pas q.
Proof. rewrite /ProtoNormalize=> ->. by destruct d; rewrite /= ?involutive. Qed.
Proof. rewrite /ProtoNormalize. by destruct d; rewrite /= ?involutive. Qed.
Global Instance proto_normalize_app_l d p1 p2 pas q :
ProtoNormalize d p1 ((d,p2) :: pas) q →
ProtoNormalize d (p1 <++> p2) pas q.
Proof.
rewrite /ProtoNormalize=> -> /=. rewrite assoc.
rewrite /ProtoNormalize /=. rewrite assoc.
by destruct d; by rewrite /= ?iProto_dual_app.
Qed.
......@@ -112,103 +84,139 @@ Section classes.
ProtoNormalize d p pas q →
ProtoNormalize d' END ((d,p) :: pas) q | 0.
Proof.
rewrite /ProtoNormalize=> -> /=.
rewrite /ProtoNormalize /=.
destruct d'; by rewrite /= ?iProto_dual_end left_id.
Qed.
Global Instance proto_normalize_app_r d p1 p2 pas q :
ProtoNormalize d p2 pas q →
ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 0.
Proof. by rewrite /ProtoNormalize=> -> /=. Qed.
Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
Global Instance proto_normalize_app_r_dual d p1 p2 pas q :
ProtoNormalize d p2 pas q →
ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 0.
Proof. by rewrite /ProtoNormalize=> -> /=. Qed.
Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
Global Instance proto_cont_normalize_O d v P p q pas :
Global Instance msg_normalize_base d v P p q pas :
ProtoNormalize d p pas q →
ProtoContNormalize d (tele_app (TT:=TeleO) (v,P,p)) pas
(tele_app (TT:=TeleO) (v,P,q)).
Proof. rewrite /ProtoContNormalize=> ?. by apply tforall_forall. Qed.
Global Instance proto_cont_normalize_S {A} {TT : A → tele} d
(pc qc : ∀ a, TT a -t> val * iProp Σ * iProto Σ) pas :
(∀ a, ProtoContNormalize d (tele_app (pc a)) pas (tele_app (qc a))) →
ProtoContNormalize d (tele_app (TT:=TeleS TT) pc) pas (tele_app (TT:=TeleS TT) qc).
MsgNormalize d (MSG v {{ P }}; p) pas (MSG v {{ P }}; q).
Proof.
rewrite /MsgNormalize /ProtoNormalize=> H a.
iApply iProto_le_trans; [|by iApply iProto_le_base].
destruct d; by rewrite /= ?iProto_dual_message ?iMsg_dual_base
iProto_app_message iMsg_app_base.
Qed.
Global Instance msg_normalize_exist {A} d (m1 m2 : A → iMsg Σ) pas :
(∀ x, MsgNormalize d (m1 x) pas (m2 x)) →
MsgNormalize d (∃ x, m1 x) pas (∃ x, m2 x).
Proof.
rewrite /ProtoContNormalize=> H. apply tforall_forall=> /= x.
apply tforall_forall, (H x).
rewrite /MsgNormalize /ProtoNormalize=> H a.
destruct d, a; simpl in *; rewrite ?iProto_dual_message ?iMsg_dual_exist
?iProto_app_message ?iMsg_app_exist /=; iIntros (x); iExists x; first
[move: (H x Send); by rewrite ?iProto_dual_message ?iProto_app_message
|move: (H x Recv); by rewrite ?iProto_dual_message ?iProto_app_message].
Qed.
Global Instance proto_normalize_message {TT} d a1 a2
(pc qc : TT → val * iProp Σ * iProto Σ) pas :
Global Instance proto_normalize_message d a1 a2 m1 m2 pas :
ActionDualIf d a1 a2 →
ProtoContNormalize d pc pas qc →
ProtoNormalize d (iProto_message a1 pc) pas
(iProto_message a2 qc).
MsgNormalize d m1 pas m2 →
ProtoNormalize d (<a1> m1) pas (<a2> m2).
Proof. by rewrite /ActionDualIf /MsgNormalize /ProtoNormalize=> ->. Qed.
Global Instance proto_normalize_swap {TT1 TT2} d a m m'
(tv1 : TT1 -t> val) (tP1 : TT1 -t> iProp Σ) (tm1 : TT1 -t> iMsg Σ)
(tv2 : TT2 -t> val) (tP2 : TT2 -t> iProp Σ)
(tp : TT1 -t> TT2 -t> iProto Σ) pas :
ActionDualIf d a Recv →
MsgNormalize d m pas m' →
MsgTele m' tv1 tP1 (tele_bind (λ.. x1, <!> tele_app tm1 x1))%proto →
(∀.. x1, MsgTele (tele_app tm1 x1) tv2 tP2 (tele_app tp x1)) →
ProtoNormalize d (<a> m) pas (<!.. x2> MSG tele_app tv2 x2 {{ tele_app tP2 x2 }};
<?.. x1> MSG tele_app tv1 x1 {{ tele_app tP1 x1 }};
tele_app (tele_app tp x1) x2) | 1.
Proof.
rewrite /ActionDualIf /ProtoContNormalize /ProtoNormalize=> -> H.
destruct d; simpl.
- rewrite iProto_dual_message iProto_app_message.
apply iProto_message_proper; apply tforall_forall=> x /=; apply H.
- rewrite iProto_app_message.
apply iProto_message_proper; apply tforall_forall=> x /=; apply H.
rewrite /ActionDualIf /MsgNormalize /ProtoNormalize /MsgTele.
rewrite tforall_forall=> Ha Hm Hm' Hm''.
iApply iProto_le_trans; [iApply Hm|]. rewrite Hm' -Ha. clear Ha Hm Hm'.
iApply iProto_le_texist_elim_l; iIntros (x1).
iApply iProto_le_texist_elim_r; iIntros (x2).
rewrite !tele_app_bind Hm'' {Hm''}.
iApply iProto_le_trans;
[iApply iProto_le_base; iApply (iProto_le_texist_intro_l _ x2)|].
iApply iProto_le_trans;
[|iApply iProto_le_base; iApply (iProto_le_texist_intro_r _ x1)]; simpl.
iApply iProto_le_base_swap.
Qed.
Global Instance proto_normalize_branch d a1 a2 P1 P2 p1 p2 q1 q2 pas :
Global Instance proto_normalize_choice d a1 a2 P1 P2 p1 p2 q1 q2 pas :
ActionDualIf d a1 a2 →
ProtoNormalize d p1 pas q1 → ProtoNormalize d p2 pas q2 →
ProtoNormalize d (iProto_branch a1 P1 P2 p1 p2) pas
(iProto_branch a2 P1 P2 q1 q2).
ProtoNormalize d (iProto_choice a1 P1 P2 p1 p2) pas
(iProto_choice a2 P1 P2 q1 q2).
Proof.
rewrite /ActionDualIf /ProtoNormalize=> -> -> ->.
destruct d; by rewrite /= -?iProto_app_branch -?iProto_dual_branch.
rewrite /ActionDualIf /ProtoNormalize=> -> H1 H2. destruct d; simpl.
- rewrite !iProto_dual_choice !iProto_app_choice.
iApply iProto_le_choice; iSplit; by iIntros "$".
- rewrite !iProto_app_choice. iApply iProto_le_choice; iSplit; by iIntros "$".
Qed.
(** Automatically perform normalization of protocols in the proof mode *)
Global Instance mapsto_proto_from_assumption q c p1 p2 :
(** Automatically perform normalization of protocols in the proof mode when
using [iAssumption] and [iFrame]. *)
Global Instance pointsto_proto_from_assumption q c p1 p2 :
ProtoNormalize false p1 [] p2 →
FromAssumption q (c ↣ p1) (c ↣ p2).
Proof.
rewrite /FromAssumption /ProtoNormalize=> ->.
by rewrite /= right_id bi.intuitionistically_if_elim.
rewrite /FromAssumption /ProtoNormalize /= right_id.
rewrite bi.intuitionistically_if_elim.
iIntros (?) "H". by iApply (iProto_pointsto_le with "H").
Qed.
Global Instance mapsto_proto_from_frame q c p1 p2 :
Global Instance pointsto_proto_from_frame q c p1 p2 :
ProtoNormalize false p1 [] p2 →
Frame q (c ↣ p1) (c ↣ p2) True.
Proof.
rewrite /Frame /ProtoNormalize=> ->.
by rewrite /= !right_id bi.intuitionistically_if_elim.
rewrite /Frame /ProtoNormalize /= right_id.
rewrite bi.intuitionistically_if_elim.
iIntros (?) "[H _]". by iApply (iProto_pointsto_le with "H").
Qed.
End classes.
(** Symbolic execution tactics *)
(* TODO: strip laters *)
Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K
c p (pc : TT → val * iProp Σ * iProto Σ) Φ :
(** * Symbolic execution tactics *)
(* TODO: Maybe strip laters from other hypotheses in the future? *)
Lemma tac_wp_recv `{!chanG Σ, !heapGS Σ} {TT : tele} Δ i j K c p m tv tP tP' tp Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (iProto_message Receive pc) →
ProtoNormalize false p [] (<?> m) →
MsgTele m tv tP tp →
(∀.. x, MaybeIntoLaterN false 1 (tele_app tP x) (tele_app tP' x)) →
let Δ' := envs_delete false i false Δ in
(∀.. x : TT,
match envs_app false
(Esnoc (Esnoc Enil j ((pc x).1.2)) i (c ↣ (pc x).2)) Δ' with
| Some Δ'' => envs_entails Δ'' (WP fill K (of_val (pc x).1.1) {{ Φ }})
(Esnoc (Esnoc Enil j (tele_app tP' x)) i (c ↣ tele_app tp x)) Δ' with
| Some Δ'' => envs_entails Δ'' (WP fill K (of_val (tele_app tv x)) {{ Φ }})
| None => False
end) →
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply recv_proto_spec|f_equiv].
rewrite -bi.later_intro bi_tforall_forall; apply bi.forall_intro=> x.
rewrite envs_entails_unseal /ProtoNormalize /MsgTele /MaybeIntoLaterN /=.
rewrite !tforall_forall right_id.
intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl.
assert (c ↣ p ⊢ c ↣ <?.. x>
MSG tele_app tv x {{ ▷ tele_app tP' x }}; tele_app tp x) as ->.
{ iIntros "Hc". iApply (iProto_pointsto_le with "Hc"). iIntros "!>".
iApply iProto_le_trans; [iApply Hp|rewrite Hm].
iApply iProto_le_texist_elim_l; iIntros (x).
iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ x)]; simpl.
iIntros "H". by iDestruct (HP with "H") as "$". }
rewrite -wp_bind. eapply bi.wand_apply;
[by eapply bi.wand_entails, (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
rewrite -bi.later_intro; apply bi.forall_intro=> x.
specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
rewrite envs_app_sound //; simpl.
by rewrite right_id HΦ bi.wand_curry.
rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
Qed.
Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
let solve_mapsto _ :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
wp_pures;
......@@ -218,8 +226,10 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
|fail 1 "wp_recv: cannot find 'recv' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <?>"
[solve_pointsto ()
|tc_solve || fail 1 "wp_recv: protocol not of the shape <?>"
|tc_solve || fail 1 "wp_recv: cannot convert to telescope"
|tc_solve
|pm_reduce; simpl; tac_intros;
tac Hnew;
wp_finish]
......@@ -231,50 +241,22 @@ Tactic Notation "wp_recv" "as" constr(pat) :=
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
c v p (pc : TT → val * iProp Σ * iProto Σ) Φ :
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as"
"(" ne_simple_intropattern_list(ys) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => _iDestructHyp H ys pat).
Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K c v p m tv tP tp Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (iProto_message Send pc) →
ProtoNormalize false p [] (<!> m) →
MsgTele m tv tP tp →
let Δ' := envs_delete false i false Δ in
(∃.. x : TT,
match envs_split (if neg is true then Right else Left) js Δ' with
match envs_split (if neg is true then base.Right else base.Left) js Δ' with
| Some (Δ1,Δ2) =>
match envs_app false (Esnoc Enil i (c ↣ (pc x).2)) Δ2 with
match envs_app false (Esnoc Enil i (c ↣ tele_app tp x)) Δ2 with
| Some Δ2' =>
v = (pc x).1.1 ∧
envs_entails Δ1 (pc x).1.2 ∧
v = tele_app tv x ∧
envs_entails Δ1 (tele_app tP x) ∧
envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
| None => False
end
......@@ -282,19 +264,22 @@ Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
end) →
envs_entails Δ (WP fill K (send c v) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ].
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_proto_spec|f_equiv].
rewrite bi_texist_exist -(bi.exist_intro x).
rewrite envs_entails_unseal /ProtoNormalize /MsgTele /= right_id texist_exist.
intros ? Hp Hm [x HΦ]. rewrite envs_lookup_sound //; simpl.
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
destruct HΦ as (-> & -> & ->). rewrite bi.pure_True // left_id.
by rewrite -bi.later_intro right_id.
destruct HΦ as (-> & -> & ->). rewrite right_id assoc.
assert (c ↣ p ⊢
c ↣ <!.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->.
{ iIntros "Hc". iApply (iProto_pointsto_le with "Hc"); iIntros "!>".
iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. }
eapply bi.wand_apply; [rewrite -wp_bind; by eapply bi.wand_entails, send_spec_tele|].
by rewrite -bi.later_intro.
Qed.
Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
let solve_mapsto _ :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
let solve_done d :=
......@@ -314,15 +299,18 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
|fail 1 "wp_send: cannot find 'send' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <!>"
[solve_pointsto ()
|tc_solve || fail 1 "wp_send: protocol not of the shape <!>"
|tc_solve || fail 1 "wp_send: cannot convert to telescope"
|pm_reduce; simpl; tac_exist;
repeat lazymatch goal with
| |- ∃ _, _ => eexists _
end;
lazymatch goal with
| |- False => fail "wp_send:" Hs' "not found"
| _ => split; [try fast_done|split;[iFrame Hs_frame; solve_done d|wp_finish]]
| _ => notypeclasses refine (conj (eq_refl _) (conj _ _));
[iFrame Hs_frame; solve_done d
|wp_finish]
end]
| _ => fail "wp_send: not a 'wp'"
end
......@@ -331,33 +319,10 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
Tactic Notation "wp_send" "with" constr(pat) :=
wp_send_core (idtac) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) ")" "with" constr(pat) :=
wp_send_core (eexists x1) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) ")"
"with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
"with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4)
uconstr(x5) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) uconstr(x7) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6; eexists x7) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) uconstr(x7) uconstr(x8) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6; eexists x7; eexists x8) with pat.
Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K
Tactic Notation "wp_send" "(" ne_uconstr_list(xs) ")" "with" constr(pat) :=
wp_send_core (ltac1_list_iter ltac:(fun x => eexists x) xs) with pat.
Lemma tac_wp_branch `{!chanG Σ, !heapGS Σ} Δ i j K
c p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (p1 <{P1}&{P2}> p2) →
......@@ -370,16 +335,17 @@ Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K
end) →
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv].
rewrite envs_entails_unseal /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl.
rewrite (iProto_pointsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply bi.wand_entails, branch_spec|f_equiv; first done].
rewrite -bi.later_intro; apply bi.forall_intro=> b.
specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
Qed.
Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
let solve_mapsto _ :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
iAssumptionCore || fail "wp_branch: cannot find" c "↣ ? @ ?" in
wp_pures;
......@@ -389,8 +355,8 @@ Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_branch _ _ Hnew K))
|fail 1 "wp_branch: cannot find 'recv' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <&>"
[solve_pointsto ()
|tc_solve || fail 1 "wp_send: protocol not of the shape <&>"
|pm_reduce; intros []; [tac1 Hnew|tac2 Hnew]; wp_finish]
| _ => fail "wp_branch: not a 'wp'"
end.
......@@ -402,15 +368,15 @@ Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" constr(pat2)
Tactic Notation "wp_branch" "as" constr(pat1) "|" "%" simple_intropattern(pat2) :=
wp_branch_core as (fun H => iDestructHyp H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" "%" simple_intropattern(pat2) :=
wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" := wp_branch as %_ | %_.
wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" := wp_branch as % _ | % _.
Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K
Lemma tac_wp_select `{!chanG Σ, !heapGS Σ} Δ neg i js K
c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (p1 <{P1}+{P2}> p2) →
let Δ' := envs_delete false i false Δ in
match envs_split (if neg is true then Right else Left) js Δ' with
match envs_split (if neg is true then base.Right else base.Left) js Δ' with
| Some (Δ1,Δ2) =>
match envs_app false (Esnoc Enil i (c ↣ if b then p1 else p2)) Δ2 with
| Some Δ2' =>
......@@ -422,10 +388,11 @@ Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K
end →
envs_entails Δ (WP fill K (send c #b) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
rewrite -assoc; f_equiv.
rewrite envs_entails_unseal /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl.
rewrite (iProto_pointsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply bi.wand_entails, select_spec|].
rewrite -assoc; f_equiv; first done.
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
......@@ -433,7 +400,7 @@ Proof.
Qed.
Tactic Notation "wp_select" "with" constr(pat) :=
let solve_mapsto _ :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
iAssumptionCore || fail "wp_select: cannot find" c "↣ ? @ ?" in
let solve_done d :=
......@@ -453,12 +420,12 @@ Tactic Notation "wp_select" "with" constr(pat) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_select _ neg _ Hs' K))
|fail 1 "wp_select: cannot find 'send' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_select: protocol not of the shape <+>"
[solve_pointsto ()
|tc_solve || fail 1 "wp_select: protocol not of the shape <+>"
|pm_reduce;
lazymatch goal with
| |- False => fail "wp_select:" Hs' "not fresh"
| _ => split;[iFrame Hs_frame; solve_done d|wp_finish]
| _ => notypeclasses refine (conj _ _); [iFrame Hs_frame; solve_done d|wp_finish]
end]
| _ => fail "wp_select: not a 'wp'"
end
......@@ -466,3 +433,21 @@ Tactic Notation "wp_select" "with" constr(pat) :=
end.
Tactic Notation "wp_select" := wp_select with "[//]".
Tactic Notation "wp_new_chan" constr(prot) "as"
"(" simple_intropattern(c1) simple_intropattern(c2) ")" constr(pat) :=
wp_smart_apply (new_chan_spec prot); [done|];
iIntros (c1); iIntros (c2); iIntros pat.
Tactic Notation "wp_fork_chan" constr(prot) "as"
simple_intropattern(c1) constr(pat1) "and"
simple_intropattern(c2) constr(pat2) :=
wp_smart_apply (fork_chan_spec prot); [iIntros (c2); iIntros pat2|
iIntros (c1); iIntros pat1].
Tactic Notation "wp_fork_chan" constr(prot) "as"
simple_intropattern(c) constr(pat) :=
wp_fork_chan prot as c pat and c pat.
Tactic Notation "wp_fork_chan" constr(prot) :=
wp_fork_chan prot as ? "?".
actris/channel/proto.v 0 → 100644
View file @ c9249305
(** This file defines the core of the Actris logic: It defines dependent
separation protocols and the various operations on it like dual, append, and
branching.
Dependent separation protocols [iProto] are defined by instantiating the
parameterized version in [proto_model] with the type of propositions [iProp] of Iris.
We define ways of constructing instances of the instantiated type via two
constructors:
- [iProto_end], which is identical to [proto_end].
- [iProto_message], which takes an [action] and an [iMsg]. The type [iMsg] is a
sequence of binders [iMsg_exist], terminated by the payload constructed with
[iMsg_base] based on arguments [v], [P] and [prot], which are the value, the
carried proposition and the [iProto] tail, respectively.
For convenience sake, we provide the following notations:
- [END], which is simply [iProto_end].
- [∃ x, m], which is [iMsg_exist] with argument [m].
- [MSG v {{ P }}; prot], which is [iMsg_Base] with arguments [v], [P] and [prot].
- [<a> m], which is [iProto_message] with arguments [a] and [m].
We also include custom notation to more easily construct complete constructions:
- [<a x1 .. xn> m], which is [<a> ∃ x1, .. ∃ xn, m].
- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol.
Futhermore, we define the following operations:
- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa.
- [iProto_app], which appends two protocols.
In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
the following inductive definition for asynchronous subtyping on session types:
p1 <: p2 p1 <: p2 p1 <: !B.p3 ?A.p3 <: p2
---------- ---------------- ---------------- ----------------------------
end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2 ?A.p1 <: !B.p2
Example:
!R <: !R ?Q <: ?Q ?Q <: ?Q
------------------- --------------
?Q.!R <: !R.?Q ?P.?Q <: ?P.?Q
------------------------------------
?P.?Q.!R <: !R.?P.?Q
Lastly, relevant type classes instances are defined for each of the above
notions, such as contractiveness and non-expansiveness, after which the
specifications of the message-passing primitives are defined in terms of the
protocol connectives. *)
From iris.algebra Require Import excl_auth.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Export lib.iprop.
From iris.base_logic Require Import lib.own.
From iris.program_logic Require Import language.
From actris.channel Require Import proto_model.
Set Default Proof Using "Type".
Export action.
(** * Types *)
Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
Declare Scope proto_scope.
Delimit Scope proto_scope with proto.
Bind Scope proto_scope with iProto.
Open Scope proto.
(** * Setup of Iris's cameras *)
Class protoG Σ V :=
protoG_authG ::
inG Σ (excl_authR (laterO (iProto Σ V))).
Definition protoΣ V := #[
GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
].
Global Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
Proof. solve_inG. Qed.
(** * Messages *)
Section iMsg.
Set Primitive Projections.
Record iMsg Σ V := IMsg { iMsg_car : V → laterO (iProto Σ V) -n> iPropO Σ }.
End iMsg.
Arguments IMsg {_ _} _.
Arguments iMsg_car {_ _} _.
Declare Scope msg_scope.
Delimit Scope msg_scope with msg.
Bind Scope msg_scope with iMsg.
Global Instance iMsg_inhabited {Σ V} : Inhabited (iMsg Σ V) := populate (IMsg inhabitant).
Section imsg_ofe.
Context {Σ : gFunctors} {V : Type}.
Instance iMsg_equiv : Equiv (iMsg Σ V) := λ m1 m2,
∀ w p, iMsg_car m1 w p ≡ iMsg_car m2 w p.
Instance iMsg_dist : Dist (iMsg Σ V) := λ n m1 m2,
∀ w p, iMsg_car m1 w p ≡{n}≡ iMsg_car m2 w p.
Lemma iMsg_ofe_mixin : OfeMixin (iMsg Σ V).
Proof. by apply (iso_ofe_mixin (iMsg_car : _ → V -d> _ -n> _)). Qed.
Canonical Structure iMsgO := Ofe (iMsg Σ V) iMsg_ofe_mixin.
Global Instance iMsg_cofe : Cofe iMsgO.
Proof. by apply (iso_cofe (IMsg : (V -d> _ -n> _) → _) iMsg_car). Qed.
End imsg_ofe.
Program Definition iMsg_base_def {Σ V}
(v : V) (P : iProp Σ) (p : iProto Σ V) : iMsg Σ V :=
IMsg (λ v', λne p', ⌜ v = v' ⌝ ∗ Next p ≡ p' ∗ P)%I.
Next Obligation. solve_proper. Qed.
Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
Definition iMsg_base := iMsg_base_aux.(unseal).
Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
Arguments iMsg_base {_ _} _%_V _%_I _%_proto.
Global Instance: Params (@iMsg_base) 3 := {}.
Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
IMsg (λ v', λne p', ∃ x, iMsg_car (m x) v' p')%I.
Next Obligation. solve_proper. Qed.
Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
Definition iMsg_exist := iMsg_exist_aux.(unseal).
Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
Arguments iMsg_exist {_ _ _} _%_msg.
Global Instance: Params (@iMsg_exist) 3 := {}.
Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
Arguments iMsg_texist {_ _ !_} _%_msg /.
Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
(at level 200, v at level 20, right associativity,
format "MSG v {{ P } } ; p") : msg_scope.
Notation "'MSG' v ; p" := (iMsg_base v True p)
(at level 200, v at level 20, right associativity,
format "MSG v ; p") : msg_scope.
Notation "∃ x .. y , m" :=
(iMsg_exist (λ x, .. (iMsg_exist (λ y, m)) ..)%msg) : msg_scope.
Notation "'∃..' x .. y , m" :=
(iMsg_texist (λ x, .. (iMsg_texist (λ y, m)) .. )%msg)
(at level 200, x binder, y binder, right associativity,
format "∃.. x .. y , m") : msg_scope.
Lemma iMsg_texist_exist {Σ V} {TT : tele} w lp (m : TT → iMsg Σ V) :
iMsg_car (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, iMsg_car (m x) w lp).
Proof.
rewrite /iMsg_texist iMsg_exist_eq.
induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH.
Qed.
(** * Operators *)
Definition iProto_end_def {Σ V} : iProto Σ V := proto_end.
Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
Definition iProto_end := iProto_end_aux.(unseal).
Definition iProto_end_eq : @iProto_end = @iProto_end_def := iProto_end_aux.(seal_eq).
Arguments iProto_end {_ _}.
Definition iProto_message_def {Σ V} (a : action) (m : iMsg Σ V) : iProto Σ V :=
proto_message a (iMsg_car m).
Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
Definition iProto_message := iProto_message_aux.(unseal).
Definition iProto_message_eq :
@iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
Arguments iProto_message {_ _} _ _%_msg.
Global Instance: Params (@iProto_message) 3 := {}.
Notation "'END'" := iProto_end : proto_scope.
Notation "< a > m" := (iProto_message a m)
(at level 200, a at level 10, m at level 200,
format "< a > m") : proto_scope.
Notation "< a @ x1 .. xn > m" := (iProto_message a (∃ x1, .. (∃ xn, m) ..))
(at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
format "< a @ x1 .. xn > m") : proto_scope.
Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m) ..))
(at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
format "< a @.. x1 .. xn > m") : proto_scope.
Notation "<!> m" := (<Send> m) (at level 200, m at level 200) : proto_scope.
Notation "<! x1 .. xn > m" := (<!> ∃ x1, .. (∃ xn, m) ..)
(at level 200, x1 closed binder, xn closed binder, m at level 200,
format "<! x1 .. xn > m") : proto_scope.
Notation "<!.. x1 .. xn > m" := (<!> ∃.. x1, .. (∃.. xn, m) ..)
(at level 200, x1 closed binder, xn closed binder, m at level 200,
format "<!.. x1 .. xn > m") : proto_scope.
Notation "<?> m" := (<Recv> m) (at level 200, m at level 200) : proto_scope.
Notation "<? x1 .. xn > m" := (<?> ∃ x1, .. (∃ xn, m) ..)
(at level 200, x1 closed binder, xn closed binder, m at level 200,
format "<? x1 .. xn > m") : proto_scope.
Notation "<?.. x1 .. xn > m" := (<?> ∃.. x1, .. (∃.. xn, m) ..)
(at level 200, x1 closed binder, xn closed binder, m at level 200,
format "<?.. x1 .. xn > m") : proto_scope.
Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
(tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
Global Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
(** * Operations *)
Program Definition iMsg_map {Σ V}
(rec : iProto Σ V → iProto Σ V) (m : iMsg Σ V) : iMsg Σ V :=
IMsg (λ v, λne p1', ∃ p1, iMsg_car m v (Next p1) ∗ p1' ≡ Next (rec p1))%I.
Next Obligation. solve_proper. Qed.
Program Definition iProto_map_app_aux {Σ V}
(f : action → action) (p2 : iProto Σ V)
(rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p,
proto_elim p2 (λ a m,
proto_message (f a) (iMsg_car (iMsg_map rec (IMsg m)))) p.
Next Obligation.
intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a m1 m2 Hm.
apply proto_message_ne=> v p' /=. by repeat f_equiv.
Qed.
Global Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
Contractive (iProto_map_app_aux f p2).
Proof.
intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a m1 m2 Hm.
apply proto_message_ne=> v p' /=. by repeat (f_contractive || f_equiv).
Qed.
Definition iProto_map_app {Σ V} (f : action → action)
(p2 : iProto Σ V) : iProto Σ V -n> iProto Σ V :=
fixpoint (iProto_map_app_aux f p2).
Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
iProto_map_app id p2 p1.
Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
Definition iProto_app := iProto_app_aux.(unseal).
Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
Arguments iProto_app {_ _} _%_proto _%_proto.
Global Instance: Params (@iProto_app) 2 := {}.
Infix "<++>" := iProto_app (at level 60) : proto_scope.
Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V :=
iProto_map_app action_dual proto_end p.
Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
Definition iProto_dual := iProto_dual_aux.(unseal).
Definition iProto_dual_eq :
@iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
Arguments iProto_dual {_ _} _%_proto.
Global Instance: Params (@iProto_dual) 2 := {}.
Notation iMsg_dual := (iMsg_map iProto_dual).
Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
if d then iProto_dual p else p.
Arguments iProto_dual_if {_ _} _ _%_proto.
Global Instance: Params (@iProto_dual_if) 3 := {}.
(** * Protocol entailment *)
Definition iProto_le_pre {Σ V}
(rec : iProto Σ V → iProto Σ V → iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
(p1 ≡ END ∗ p2 ≡ END) ∨
∃ a1 a2 m1 m2,
(p1 ≡ <a1> m1) ∗ (p2 ≡ <a2> m2) ∗
match a1, a2 with
| Recv, Recv => ∀ v p1',
iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ rec p1' p2' ∗ iMsg_car m2 v (Next p2')
| Send, Send => ∀ v p2',
iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ rec p1' p2' ∗ iMsg_car m1 v (Next p1')
| Recv, Send => ∀ v1 v2 p1' p2',
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
▷ rec p1' (<!> MSG v2; pt) ∗ ▷ rec (<?> MSG v1; pt) p2'
| Send, Recv => False
end.
Global Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
NonExpansive2 (iProto_le_pre rec).
Proof. solve_proper. Qed.
Program Definition iProto_le_pre' {Σ V}
(rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
iProto Σ V -n> iProto Σ V -n> iPropO Σ := λne p1 p2,
iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
Solve Obligations with solve_proper.
Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V).
Proof.
intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
by repeat (f_contractive || f_equiv).
Qed.
Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
fixpoint iProto_le_pre' p1 p2.
Arguments iProto_le {_ _} _%_proto _%_proto.
Global Instance: Params (@iProto_le) 2 := {}.
Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
Global Instance iProto_le_ne {Σ V} : NonExpansive2 (@iProto_le Σ V).
Proof. solve_proper. Qed.
Global Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
Proof. solve_proper. Qed.
Fixpoint iProto_app_recvs {Σ V} (vs : list V) (p : iProto Σ V) : iProto Σ V :=
match vs with
| [] => p
| v :: vs => <?> MSG v; iProto_app_recvs vs p
end.
Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
∃ p, iProto_app_recvs vsr p ⊑ pl ∗ iProto_app_recvs vsl (iProto_dual p) ⊑ pr.
Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
(p : iProto Σ V) : iProp Σ :=
own γ (◯E (Next p)).
Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
(p : iProto Σ V) : iProp Σ :=
own γ (●E (Next p)).
(** In the original Actris papers we a single ghost name for [iProto_ctx] and
[iProto_own]. To distinguish the two [iProto_own]s for both sides, we used
an enum [Left]/[Right]. This turned out to be cumbersome because at various
places we need to case at this enum. The current version of [iProto_ctx] has two
ghost names, one for each [iProto_own], enabling more uniform definitions. *)
Definition iProto_ctx `{protoG Σ V}
(γl γr : gname) (vsl vsr : list V) : iProp Σ :=
∃ pl pr,
iProto_own_auth γl pl ∗
iProto_own_auth γr pr ∗
▷ iProto_interp vsl vsr pl pr.
(** * The connective for ownership of channel ends *)
Definition iProto_own `{!protoG Σ V} (γ : gname) (p : iProto Σ V) : iProp Σ :=
∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ p'.
Arguments iProto_own {_ _ _} _ _%_proto.
Global Instance: Params (@iProto_own) 4 := {}.
Global Instance iProto_own_contractive `{protoG Σ V} γ :
Contractive (iProto_own γ).
Proof. solve_contractive. Qed.
(** * Proofs *)
Section proto.
Context `{!protoG Σ V}.
Implicit Types v : V.
Implicit Types p pl pr : iProto Σ V.
Implicit Types m : iMsg Σ V.
(** ** Equality *)
Lemma iProto_case p : p ≡ END ∨ ∃ a m, p ≡ <a> m.
Proof.
rewrite iProto_message_eq iProto_end_eq.
destruct (proto_case p) as [|(a&m&?)]; [by left|right].
by exists a, (IMsg m).
Qed.
Lemma iProto_message_equivI `{!BiInternalEq SPROP} a1 a2 m1 m2 :
(<a1> m1) ≡ (<a2> m2) ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧
(∀ v lp, iMsg_car m1 v lp ≡ iMsg_car m2 v lp).
Proof. rewrite iProto_message_eq. apply proto_message_equivI. Qed.
Lemma iProto_message_end_equivI `{!BiInternalEq SPROP} a m :
(<a> m) ≡ END ⊢@{SPROP} False.
Proof. rewrite iProto_message_eq iProto_end_eq. apply proto_message_end_equivI. Qed.
Lemma iProto_end_message_equivI `{!BiInternalEq SPROP} a m :
END ≡ (<a> m) ⊢@{SPROP} False.
Proof. by rewrite internal_eq_sym iProto_message_end_equivI. Qed.
(** ** Non-expansiveness of operators *)
Global Instance iMsg_car_proper :
Proper (iMsg_equiv ==> (=) ==> (≡) ==> (≡)) (iMsg_car (Σ:=Σ) (V:=V)).
Proof.
intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
f_equiv; [ by f_equiv | done ].
Qed.
Global Instance iMsg_car_ne n :
Proper (iMsg_dist n ==> (=) ==> (dist n) ==> (dist n)) (iMsg_car (Σ:=Σ) (V:=V)).
Proof.
intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
f_equiv; [ by f_equiv | done ].
Qed.
Global Instance iMsg_contractive v n :
Proper (dist n ==> dist_later n ==> dist n) (iMsg_base (Σ:=Σ) (V:=V) v).
Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_contractive. Qed.
Global Instance iMsg_ne v : NonExpansive2 (iMsg_base (Σ:=Σ) (V:=V) v).
Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_proper. Qed.
Global Instance iMsg_proper v :
Proper ((≡) ==> (≡) ==> (≡)) (iMsg_base (Σ:=Σ) (V:=V) v).
Proof. apply (ne_proper_2 _). Qed.
Global Instance iMsg_exist_ne A n :
Proper (pointwise_relation _ (dist n) ==> (dist n)) (@iMsg_exist Σ V A).
Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
Global Instance iMsg_exist_proper A :
Proper (pointwise_relation _ (≡) ==> (≡)) (@iMsg_exist Σ V A).
Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
Global Instance msg_tele_base (v:V) (P : iProp Σ) (p : iProto Σ V) :
MsgTele (TT:=TeleO) (MSG v {{ P }}; p) v P p.
Proof. done. Qed.
Global Instance msg_tele_exist {A} {TT : A → tele} (m : A → iMsg Σ V) tv tP tp :
(∀ x, MsgTele (TT:=TT x) (m x) (tv x) (tP x) (tp x)) →
MsgTele (TT:=TeleS TT) (∃ x, m x) tv tP tp.
Proof. intros Hm. rewrite /MsgTele /=. f_equiv=> x. apply Hm. Qed.
Global Instance iProto_message_ne a :
NonExpansive (iProto_message (Σ:=Σ) (V:=V) a).
Proof. rewrite iProto_message_eq. solve_proper. Qed.
Global Instance iProto_message_proper a :
Proper ((≡) ==> (≡)) (iProto_message (Σ:=Σ) (V:=V) a).
Proof. apply (ne_proper _). Qed.
Lemma iProto_message_equiv {TT1 TT2 : tele} a1 a2
(m1 m2 : iMsg Σ V)
(v1 : TT1 -t> V) (v2 : TT2 -t> V)
(P1 : TT1 -t> iProp Σ) (P2 : TT2 -t> iProp Σ)
(prot1 : TT1 -t> iProto Σ V) (prot2 : TT2 -t> iProto Σ V) :
MsgTele m1 v1 P1 prot1 →
MsgTele m2 v2 P2 prot2 →
⌜ a1 = a2 ⌝ -∗
(■ ∀.. (xs1 : TT1), tele_app P1 xs1 -∗
∃.. (xs2 : TT2), ⌜tele_app v1 xs1 = tele_app v2 xs2⌝ ∗
▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
tele_app P2 xs2) -∗
(■ ∀.. (xs2 : TT2), tele_app P2 xs2 -∗
∃.. (xs1 : TT1), ⌜tele_app v1 xs1 = tele_app v2 xs2⌝ ∗
▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
tele_app P1 xs1) -∗
(<a1> m1) ≡ (<a2> m2).
Proof.
iIntros (Hm1 Hm2 Heq) "#Heq1 #Heq2".
unfold MsgTele in Hm1. rewrite Hm1. clear Hm1.
unfold MsgTele in Hm2. rewrite Hm2. clear Hm2.
rewrite iProto_message_eq proto_message_equivI.
iSplit; [ done | ].
iIntros (v p').
do 2 rewrite iMsg_texist_exist.
rewrite iMsg_base_eq /=.
iApply prop_ext.
iIntros "!>". iSplit.
- iDestruct 1 as (xs1 Hveq1) "[Hrec1 HP1]".
iDestruct ("Heq1" with "HP1") as (xs2 Hveq2) "[Hrec2 HP2]".
iExists xs2. rewrite -Hveq1 Hveq2.
iSplitR; [ done | ]. iSplitR "HP2"; [ | done ].
iRewrite -"Hrec1". iApply later_equivI. iIntros "!>". by iRewrite "Hrec2".
- iDestruct 1 as (xs2 Hveq2) "[Hrec2 HP2]".
iDestruct ("Heq2" with "HP2") as (xs1 Hveq1) "[Hrec1 HP1]".
iExists xs1. rewrite -Hveq2 Hveq1.
iSplitR; [ done | ]. iSplitR "HP1"; [ | done ].
iRewrite -"Hrec2". iApply later_equivI. iIntros "!>". by iRewrite "Hrec1".
Qed.
(** Helpers *)
Lemma iMsg_map_base f v P p :
NonExpansive f →
iMsg_map f (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; f p)%msg.
Proof.
rewrite iMsg_base_eq. intros ? v' p'; simpl. iSplit.
- iDestruct 1 as (p'') "[(->&Hp&$) Hp']". iSplit; [done|].
iRewrite "Hp'". iIntros "!>". by iRewrite "Hp".
- iIntros "(->&Hp'&$)". iExists p. iRewrite -"Hp'". auto.
Qed.
Lemma iMsg_map_exist {A} f (m : A → iMsg Σ V) :
iMsg_map f (∃ x, m x) ≡ (∃ x, iMsg_map f (m x))%msg.
Proof.
rewrite iMsg_exist_eq. intros v' p'; simpl. iSplit.
- iDestruct 1 as (p'') "[H Hp']". iDestruct "H" as (x) "H"; auto.
- iDestruct 1 as (x p'') "[Hm Hp']". auto.
Qed.
(** ** Dual *)
Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
Proof. rewrite iProto_dual_eq. solve_proper. Qed.
Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ V).
Proof. apply (ne_proper _). Qed.
Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d).
Proof. solve_proper. Qed.
Global Instance iProto_dual_if_proper d :
Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
Proof. apply (ne_proper _). Qed.
Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END.
Proof.
rewrite iProto_end_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
by rewrite proto_elim_end.
Qed.
Lemma iProto_dual_message a m :
iProto_dual (<a> m) ≡ <action_dual a> iMsg_dual m.
Proof.
rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
intros a' m1 m2 Hm; f_equiv; solve_proper.
Qed.
Lemma iMsg_dual_base v P p :
iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg.
Proof. apply iMsg_map_base, _. Qed.
Lemma iMsg_dual_exist {A} (m : A → iMsg Σ V) :
iMsg_dual (∃ x, m x) ≡ (∃ x, iMsg_dual (m x))%msg.
Proof. apply iMsg_map_exist. Qed.
Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
Proof.
intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&m&->)].
{ by rewrite !iProto_dual_end. }
rewrite !iProto_dual_message involutive.
iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
iApply prop_ext; iIntros "!>"; iSplit.
- iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'".
iDestruct "H" as (pdd) "[H #Hpd]".
iApply (internal_eq_rewrite); [|done]; iIntros "!>".
iRewrite "Hpd". by iRewrite ("IH" $! pdd).
- iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists _.
rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
Qed.
(** ** Append *)
Global Instance iProto_app_end_l : LeftId (≡) END (@iProto_app Σ V).
Proof.
intros p. rewrite iProto_end_eq iProto_app_eq /iProto_app_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
by rewrite proto_elim_end.
Qed.
Lemma iProto_app_message a m p2 : (<a> m) <++> p2 ≡ <a> m <++> p2.
Proof.
rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
intros a' m1 m2 Hm. f_equiv; solve_proper.
Qed.
Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
Proof.
assert (∀ n, Proper (dist n ==> (=) ==> dist n) (@iProto_app Σ V)).
{ intros n p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
assert (Proper ((≡) ==> (=) ==> (≡)) (@iProto_app Σ V)).
{ intros p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
intros n p1 p1' Hp1 p2 p2' Hp2. rewrite Hp1. clear p1 Hp1.
revert p1'. induction (lt_wf n) as [n _ IH]; intros p1.
destruct (iProto_case p1) as [->|(a&m&->)].
{ by rewrite !left_id. }
rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
f_contractive. apply IH; eauto using dist_lt.
Qed.
Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
Proof. apply (ne_proper_2 _). Qed.
Lemma iMsg_app_base v P p1 p2 :
((MSG v {{ P }}; p1) <++> p2)%msg ≡ (MSG v {{ P }}; p1 <++> p2)%msg.
Proof. apply: iMsg_map_base. Qed.
Lemma iMsg_app_exist {A} (m : A → iMsg Σ V) p2 :
((∃ x, m x) <++> p2)%msg ≡ (∃ x, m x <++> p2)%msg.
Proof. apply iMsg_map_exist. Qed.
Global Instance iProto_app_end_r : RightId (≡) END (@iProto_app Σ V).
Proof.
intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&m&->)].
{ by rewrite left_id. }
rewrite iProto_app_message.
iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
iApply prop_ext; iIntros "!>". iSplit.
- iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'".
iApply (internal_eq_rewrite); [|done]; iIntros "!>".
by iRewrite ("IH" $! p1').
- iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists p''.
rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
Qed.
Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
Proof.
intros p1 p2 p3. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
iLöb as "IH" forall (p1). destruct (iProto_case p1) as [->|(a&m&->)].
{ by rewrite !left_id. }
rewrite !iProto_app_message.
iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=".
iApply prop_ext; iIntros "!>". iSplit.
- iDestruct 1 as (p1') "[H #Hp']".
iExists (p1' <++> p2). iSplitL; [by auto|].
iRewrite "Hp'". iIntros "!>". iApply "IH".
- iDestruct 1 as (p12) "[H #Hp123]". iDestruct "H" as (p1') "[H #Hp12]".
iExists p1'. iFrame "H". iRewrite "Hp123".
iIntros "!>". iRewrite "Hp12". by iRewrite ("IH" $! p1').
Qed.
Lemma iProto_dual_app p1 p2 :
iProto_dual (p1 <++> p2) ≡ iProto_dual p1 <++> iProto_dual p2.
Proof.
apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
iLöb as "IH" forall (p1 p2). destruct (iProto_case p1) as [->|(a&m&->)].
{ by rewrite iProto_dual_end !left_id. }
rewrite iProto_dual_message !iProto_app_message iProto_dual_message /=.
iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p12) "/=".
iApply prop_ext; iIntros "!>". iSplit.
- iDestruct 1 as (p12d) "[H #Hp12]". iDestruct "H" as (p1') "[H #Hp12d]".
iExists (iProto_dual p1'). iSplitL; [by auto|].
iRewrite "Hp12". iIntros "!>". iRewrite "Hp12d". iApply "IH".
- iDestruct 1 as (p1') "[H #Hp12]". iDestruct "H" as (p1d) "[H #Hp1']".
iExists (p1d <++> p2). iSplitL; [by auto|].
iRewrite "Hp12". iIntros "!>". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
Qed.
(** ** Protocol entailment **)
Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2 ≡ iProto_le_pre iProto_le p1 p2.
Proof. apply: (fixpoint_unfold iProto_le_pre'). Qed.
Lemma iProto_le_end : ⊢ END ⊑ (END : iProto Σ V).
Proof. rewrite iProto_le_unfold. iLeft. auto 10. Qed.
Lemma iProto_le_send m1 m2 :
(∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1',
▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')) -∗
(<!> m1) ⊑ (<!> m2).
Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
Lemma iProto_le_recv m1 m2 :
(∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2',
▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2')) -∗
(<?> m1) ⊑ (<?> m2).
Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
Lemma iProto_le_swap m1 m2 :
(∀ v1 v2 p1' p2',
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2')) -∗
(<?> m1) ⊑ (<!> m2).
Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
Lemma iProto_le_end_inv_l p : p ⊑ END -∗ (p ≡ END).
Proof.
rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
iDestruct "H" as (a1 a2 m1 m2) "(_ & Heq & _)".
by iDestruct (iProto_end_message_equivI with "Heq") as %[].
Qed.
Lemma iProto_le_end_inv_r p : END ⊑ p -∗ (p ≡ END).
Proof.
rewrite iProto_le_unfold. iIntros "[[_ Hp]|H] //".
iDestruct "H" as (a1 a2 m1 m2) "(Heq & _ & _)".
iDestruct (iProto_end_message_equivI with "Heq") as %[].
Qed.
Lemma iProto_le_send_inv p1 m2 :
p1 ⊑ (<!> m2) -∗ ∃ a1 m1,
(p1 ≡ <a1> m1) ∗
match a1 with
| Send => ∀ v p2',
iMsg_car m2 v (Next p2') -∗ ∃ p1',
▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')
| Recv => ∀ v1 v2 p1' p2',
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2')
end.
Proof.
rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
{ iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
iExists _, _; iSplit; [done|]. destruct a1, a2.
- iIntros (v p2') "Hm2".
iDestruct (iProto_message_equivI with "Hp2") as (_) "{Hp2} #Hm".
iApply "H". by iRewrite -("Hm" $! v (Next p2')).
- done.
- iIntros (v1 v2 p1' p2') "Hm1 Hm2".
iDestruct (iProto_message_equivI with "Hp2") as (_) "{Hp2} #Hm".
iApply ("H" with "Hm1"). by iRewrite -("Hm" $! v2 (Next p2')).
- iDestruct (iProto_message_equivI with "Hp2") as ([=]) "_".
Qed.
Lemma iProto_le_send_send_inv m1 m2 v p2' :
(<!> m1) ⊑ (<!> m2) -∗
iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
Proof.
iIntros "H Hm2". iDestruct (iProto_le_send_inv with "H") as (a m1') "[Hm1 H]".
iDestruct (iProto_message_equivI with "Hm1") as (<-) "Hm1".
iDestruct ("H" with "Hm2") as (p1') "[Hle Hm]".
iRewrite -("Hm1" $! v (Next p1')) in "Hm". auto with iFrame.
Qed.
Lemma iProto_le_recv_send_inv m1 m2 v1 v2 p1' p2' :
(<?> m1) ⊑ (<!> m2) -∗
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2').
Proof.
iIntros "H Hm1 Hm2". iDestruct (iProto_le_send_inv with "H") as (a m1') "[Hm H]".
iDestruct (iProto_message_equivI with "Hm") as (<-) "{Hm} #Hm".
iApply ("H" with "[Hm1] Hm2"). by iRewrite -("Hm" $! v1 (Next p1')).
Qed.
Lemma iProto_le_recv_inv p1 m2 :
p1 ⊑ (<?> m2) -∗ ∃ m1,
(p1 ≡ <?> m1) ∗
∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2',
▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
Proof.
rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
{ iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
iExists m1.
iDestruct (iProto_message_equivI with "Hp2") as (<-) "{Hp2} #Hm2".
destruct a1; [done|]. iSplit; [done|].
iIntros (v p1') "Hm". iDestruct ("H" with "Hm") as (p2') "[Hle Hm]".
iExists p2'. iIntros "{$Hle}". by iRewrite ("Hm2" $! v (Next p2')).
Qed.
Lemma iProto_le_recv_recv_inv m1 m2 v p1' :
(<?> m1) ⊑ (<?> m2) -∗
iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
Proof.
iIntros "H Hm2". iDestruct (iProto_le_recv_inv with "H") as (m1') "[Hm1 H]".
iApply "H". iDestruct (iProto_message_equivI with "Hm1") as (_) "Hm1".
by iRewrite -("Hm1" $! v (Next p1')).
Qed.
Lemma iProto_le_refl p : ⊢ p ⊑ p.
Proof.
iLöb as "IH" forall (p). destruct (iProto_case p) as [->|([]&m&->)].
- iApply iProto_le_end.
- iApply iProto_le_send. auto 10 with iFrame.
- iApply iProto_le_recv. auto 10 with iFrame.
Qed.
Lemma iProto_le_trans p1 p2 p3 : p1 ⊑ p2 -∗ p2 ⊑ p3 -∗ p1 ⊑ p3.
Proof.
iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
destruct (iProto_case p3) as [->|([]&m3&->)].
- iDestruct (iProto_le_end_inv_l with "H2") as "H2". by iRewrite "H2" in "H1".
- iDestruct (iProto_le_send_inv with "H2") as (a2 m2) "[Hp2 H2]".
iRewrite "Hp2" in "H1"; clear p2. destruct a2.
+ iDestruct (iProto_le_send_inv with "H1") as (a1 m1) "[Hp1 H1]".
iRewrite "Hp1"; clear p1. destruct a1.
* iApply iProto_le_send. iIntros (v p3') "Hm3".
iDestruct ("H2" with "Hm3") as (p2') "[Hle Hm2]".
iDestruct ("H1" with "Hm2") as (p1') "[Hle' Hm1]".
iExists p1'. iIntros "{$Hm1} !>". by iApply ("IH" with "Hle'").
* iApply iProto_le_swap. iIntros (v1 v3 p1' p3') "Hm1 Hm3".
iDestruct ("H2" with "Hm3") as (p2') "[Hle Hm2]".
iDestruct ("H1" with "Hm1 Hm2") as (pt) "[Hp1' Hp2']".
iExists pt. iIntros "{$Hp1'} !>". by iApply ("IH" with "Hp2'").
+ iDestruct (iProto_le_recv_inv with "H1") as (m1) "[Hp1 H1]".
iRewrite "Hp1"; clear p1. iApply iProto_le_swap.
iIntros (v1 v3 p1' p3') "Hm1 Hm3".
iDestruct ("H1" with "Hm1") as (p2') "[Hle Hm2]".
iDestruct ("H2" with "Hm2 Hm3") as (pt) "[Hp2' Hp3']".
iExists pt. iIntros "{$Hp3'} !>". by iApply ("IH" with "Hle").
- iDestruct (iProto_le_recv_inv with "H2") as (m2) "[Hp2 H3]".
iRewrite "Hp2" in "H1".
iDestruct (iProto_le_recv_inv with "H1") as (m1) "[Hp1 H2]".
iRewrite "Hp1". iApply iProto_le_recv. iIntros (v p1') "Hm1".
iDestruct ("H2" with "Hm1") as (p2') "[Hle Hm2]".
iDestruct ("H3" with "Hm2") as (p3') "[Hle' Hm3]".
iExists p3'. iIntros "{$Hm3} !>". by iApply ("IH" with "Hle").
Qed.
Lemma iProto_le_payload_elim_l a m v P p :
(P -∗ (<?> MSG v; p) ⊑ (<a> m)) ⊢
(<?> MSG v {{ P }}; p) ⊑ (<a> m).
Proof.
rewrite iMsg_base_eq. iIntros "H". destruct a.
- iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= (#?&#?&HP) Hm2 /=".
iApply (iProto_le_recv_send_inv with "(H HP)"); simpl; auto.
- iApply iProto_le_recv. iIntros (v' p') "(->&Hp&HP)".
iApply (iProto_le_recv_recv_inv with "(H HP)"); simpl; auto.
Qed.
Lemma iProto_le_payload_elim_r a m v P p :
(P -∗ (<a> m) ⊑ (<!> MSG v; p)) ⊢
(<a> m) ⊑ (<!> MSG v {{ P }}; p).
Proof.
rewrite iMsg_base_eq. iIntros "H". destruct a.
- iApply iProto_le_send. iIntros (v' p') "(->&Hp&HP)".
iApply (iProto_le_send_send_inv with "(H HP)"); simpl; auto.
- iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 (->&#?&HP) /=".
iApply (iProto_le_recv_send_inv with "(H HP) Hm1"); simpl; auto.
Qed.
Lemma iProto_le_payload_intro_l v P p :
P -∗ (<!> MSG v {{ P }}; p) ⊑ (<!> MSG v; p).
Proof.
rewrite iMsg_base_eq.
iIntros "HP". iApply iProto_le_send. iIntros (v' p') "(->&Hp&_) /=".
iExists p'. iSplitR; [iApply iProto_le_refl|]. auto.
Qed.
Lemma iProto_le_payload_intro_r v P p :
P -∗ (<?> MSG v; p) ⊑ (<?> MSG v {{ P }}; p).
Proof.
rewrite iMsg_base_eq.
iIntros "HP". iApply iProto_le_recv. iIntros (v' p') "(->&Hp&_) /=".
iExists p'. iSplitR; [iApply iProto_le_refl|]. auto.
Qed.
Lemma iProto_le_exist_elim_l {A} (m1 : A → iMsg Σ V) a m2 :
(∀ x, (<?> m1 x) ⊑ (<a> m2)) ⊢
(<? x> m1 x) ⊑ (<a> m2).
Proof.
rewrite iMsg_exist_eq. iIntros "H". destruct a.
- iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=".
iDestruct "Hm1" as (x) "Hm1".
iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
- iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
by iApply (iProto_le_recv_recv_inv with "H").
Qed.
Lemma iProto_le_exist_elim_l_inhabited `{!Inhabited A} (m : A → iMsg Σ V) p :
(∀ x, (<?> m x) ⊑ p) ⊢
(<? x> m x) ⊑ p.
Proof.
rewrite iMsg_exist_eq. iIntros "H".
destruct (iProto_case p) as [Heq | [a [m' Heq]]].
- unshelve iSpecialize ("H" $!inhabitant); first by apply _.
rewrite Heq.
iDestruct (iProto_le_end_inv_l with "H") as "H".
rewrite iProto_end_eq iProto_message_eq.
iDestruct (proto_message_end_equivI with "H") as "[]".
- iEval (rewrite Heq). destruct a.
+ iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=".
iDestruct "Hm1" as (x) "Hm1".
iSpecialize ("H" $! x). rewrite Heq.
iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
+ iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
iSpecialize ("H" $! x). rewrite Heq.
by iApply (iProto_le_recv_recv_inv with "H").
Qed.
Lemma iProto_le_exist_elim_r {A} a m1 (m2 : A → iMsg Σ V) :
(∀ x, (<a> m1) ⊑ (<!> m2 x)) ⊢
(<a> m1) ⊑ (<! x> m2 x).
Proof.
rewrite iMsg_exist_eq. iIntros "H". destruct a.
- iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
by iApply (iProto_le_send_send_inv with "H").
- iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1".
iDestruct 1 as (x) "Hm2".
iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
Qed.
Lemma iProto_le_exist_elim_r_inhabited `{Hinh : Inhabited A} p (m : A → iMsg Σ V) :
(∀ x, p ⊑ (<!> m x)) ⊢
p ⊑ (<! x> m x).
Proof.
rewrite iMsg_exist_eq. iIntros "H".
destruct (iProto_case p) as [Heq | [a [m' Heq]]].
- unshelve iSpecialize ("H" $!inhabitant); first by apply _.
rewrite Heq.
iDestruct (iProto_le_end_inv_r with "H") as "H".
rewrite iProto_end_eq iProto_message_eq.
iDestruct (proto_message_end_equivI with "H") as "[]".
- iEval (rewrite Heq). destruct a.
+ iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
iSpecialize ("H" $! x). rewrite Heq.
by iApply (iProto_le_send_send_inv with "H").
+ iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1".
iDestruct 1 as (x) "Hm2".
iSpecialize ("H" $! x). rewrite Heq.
iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
Qed.
Lemma iProto_le_exist_intro_l {A} (m : A → iMsg Σ V) a :
⊢ (<! x> m x) ⊑ (<!> m a).
Proof.
rewrite iMsg_exist_eq. iApply iProto_le_send. iIntros (v p') "Hm /=".
iExists p'. iSplitR; last by auto. iApply iProto_le_refl.
Qed.
Lemma iProto_le_exist_intro_r {A} (m : A → iMsg Σ V) a :
⊢ (<?> m a) ⊑ (<? x> m x).
Proof.
rewrite iMsg_exist_eq. iApply iProto_le_recv. iIntros (v p') "Hm /=".
iExists p'. iSplitR; last by auto. iApply iProto_le_refl.
Qed.
Lemma iProto_le_texist_elim_l {TT : tele} (m1 : TT → iMsg Σ V) a m2 :
(∀ x, (<?> m1 x) ⊑ (<a> m2)) ⊢
(<?.. x> m1 x) ⊑ (<a> m2).
Proof.
iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
iApply iProto_le_exist_elim_l; iIntros (x).
iApply "IH". iIntros (xs). iApply "H".
Qed.
Lemma iProto_le_texist_elim_r {TT : tele} a m1 (m2 : TT → iMsg Σ V) :
(∀ x, (<a> m1) ⊑ (<!> m2 x)) -∗
(<a> m1) ⊑ (<!.. x> m2 x).
Proof.
iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
iApply iProto_le_exist_elim_r; iIntros (x).
iApply "IH". iIntros (xs). iApply "H".
Qed.
Lemma iProto_le_texist_intro_l {TT : tele} (m : TT → iMsg Σ V) x :
⊢ (<!.. x> m x) ⊑ (<!> m x).
Proof.
induction x as [|T TT x xs IH] using tele_arg_ind; simpl.
{ iApply iProto_le_refl. }
iApply iProto_le_trans; [by iApply iProto_le_exist_intro_l|]. iApply IH.
Qed.
Lemma iProto_le_texist_intro_r {TT : tele} (m : TT → iMsg Σ V) x :
⊢ (<?> m x) ⊑ (<?.. x> m x).
Proof.
induction x as [|T TT x xs IH] using tele_arg_ind; simpl.
{ iApply iProto_le_refl. }
iApply iProto_le_trans; [|by iApply iProto_le_exist_intro_r]. iApply IH.
Qed.
Lemma iProto_le_base a v P p1 p2 :
▷ (p1 ⊑ p2) ⊢
(<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
Proof.
rewrite iMsg_base_eq. iIntros "H". destruct a.
- iApply iProto_le_send. iIntros (v' p') "(->&Hp&$)".
iExists p1. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
- iApply iProto_le_recv. iIntros (v' p') "(->&Hp&$)".
iExists p2. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
Qed.
Lemma iProto_le_base_swap v1 v2 P1 P2 p :
⊢ (<?> MSG v1 {{ P1 }}; <!> MSG v2 {{ P2 }}; p)
⊑ (<!> MSG v2 {{ P2 }}; <?> MSG v1 {{ P1 }}; p).
Proof.
rewrite {1 3}iMsg_base_eq. iApply iProto_le_swap.
iIntros (v1' v2' p1' p2') "/= (->&#Hp1&HP1) (->&#Hp2&HP2)". iExists p.
iSplitL "HP2".
- iIntros "!>". iRewrite -"Hp1". by iApply iProto_le_payload_intro_l.
- iIntros "!>". iRewrite -"Hp2". by iApply iProto_le_payload_intro_r.
Qed.
Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
Proof.
iIntros "H". iLöb as "IH" forall (p1 p2).
destruct (iProto_case p1) as [->|([]&m1&->)].
- iDestruct (iProto_le_end_inv_l with "H") as "H".
iRewrite "H". iApply iProto_le_refl.
- iDestruct (iProto_le_send_inv with "H") as (a2 m2) "[Hp2 H]".
iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message).
destruct a2; simpl.
+ iApply iProto_le_recv. iIntros (v p1d).
iDestruct 1 as (p1') "[Hm1 #Hp1d]".
iDestruct ("H" with "Hm1") as (p2') "[H Hm2]".
iDestruct ("IH" with "H") as "H". iExists (iProto_dual p2').
iSplitL "H"; [iIntros "!>"; by iRewrite "Hp1d"|]. simpl; auto.
+ iApply iProto_le_swap. iIntros (v1 v2 p1d p2d).
iDestruct 1 as (p1') "[Hm1 #Hp1d]". iDestruct 1 as (p2') "[Hm2 #Hp2d]".
iDestruct ("H" with "Hm2 Hm1") as (pt) "[H1 H2]".
iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}".
rewrite !iProto_dual_message /=. iExists (iProto_dual pt). iSplitL "H2".
* iIntros "!>". iRewrite "Hp1d". by rewrite -iMsg_dual_base.
* iIntros "!>". iRewrite "Hp2d". by rewrite -iMsg_dual_base.
- iDestruct (iProto_le_recv_inv with "H") as (m2) "[Hp2 H]".
iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message /=).
iApply iProto_le_send. iIntros (v p2d).
iDestruct 1 as (p2') "[Hm2 #Hp2d]".
iDestruct ("H" with "Hm2") as (p1') "[H Hm1]".
iDestruct ("IH" with "H") as "H". iExists (iProto_dual p1').
iSplitL "H"; [iIntros "!>"; by iRewrite "Hp2d"|]. simpl; auto.
Qed.
Lemma iProto_le_amber_internal (p1 p2 : iProto Σ V → iProto Σ V)
`{Contractive p1, Contractive p2}:
□ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) ⊢
fixpoint p1 ⊑ fixpoint p2.
Proof.
iIntros "#H". iLöb as "IH".
iEval (rewrite (fixpoint_unfold p1)).
iEval (rewrite (fixpoint_unfold p2)).
iApply "H". iApply "IH".
Qed.
Lemma iProto_le_amber_external (p1 p2 : iProto Σ V → iProto Σ V)
`{Contractive p1, Contractive p2}:
(∀ rec1 rec2, (⊢ rec1 ⊑ rec2) → ⊢ p1 rec1 ⊑ p2 rec2) →
⊢ fixpoint p1 ⊑ fixpoint p2.
Proof.
intros IH. apply fixpoint_ind.
- by intros p1' p2' -> ?.
- exists (fixpoint p2). iApply iProto_le_refl.
- intros p' ?. rewrite (fixpoint_unfold p2). by apply IH.
- apply bi.limit_preserving_entails; [done|solve_proper].
Qed.
Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 ⊢ iProto_dual p1 ⊑ p2.
Proof.
iIntros "H". iEval (rewrite -(involutive iProto_dual p2)).
by iApply iProto_le_dual.
Qed.
Lemma iProto_le_dual_r p1 p2 : p2 ⊑ iProto_dual p1 ⊢ p1 ⊑ iProto_dual p2.
Proof.
iIntros "H". iEval (rewrite -(involutive iProto_dual p1)).
by iApply iProto_le_dual.
Qed.
Lemma iProto_le_app p1 p2 p3 p4 :
p1 ⊑ p2 -∗ p3 ⊑ p4 -∗ p1 <++> p3 ⊑ p2 <++> p4.
Proof.
iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3 p4).
destruct (iProto_case p2) as [->|([]&m2&->)].
- iDestruct (iProto_le_end_inv_l with "H1") as "H1".
iRewrite "H1". by rewrite !left_id.
- iDestruct (iProto_le_send_inv with "H1") as (a1 m1) "[Hp1 H1]".
iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. destruct a1; simpl.
+ iApply iProto_le_send. iIntros (v p24).
iDestruct 1 as (p2') "[Hm2 #Hp24]".
iDestruct ("H1" with "Hm2") as (p1') "[H1 Hm1]".
iExists (p1' <++> p3). iSplitR "Hm1"; [|by simpl; eauto].
iIntros "!>". iRewrite "Hp24". by iApply ("IH" with "H1").
+ iApply iProto_le_swap. iIntros (v1 v2 p13 p24).
iDestruct 1 as (p1') "[Hm1 #Hp13]". iDestruct 1 as (p2') "[Hm2 #Hp24]".
iSpecialize ("H1" with "Hm1 Hm2").
iDestruct "H1" as (pt) "[H1 H1']".
iExists (pt <++> p3). iSplitL "H1".
* iIntros "!>". iRewrite "Hp13".
rewrite /= -iMsg_app_base -iProto_app_message.
iApply ("IH" with "H1"). iApply iProto_le_refl.
* iIntros "!>". iRewrite "Hp24".
rewrite /= -iMsg_app_base -iProto_app_message.
iApply ("IH" with "H1' H2").
- iDestruct (iProto_le_recv_inv with "H1") as (m1) "[Hp1 H1]".
iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. iApply iProto_le_recv.
iIntros (v p13). iDestruct 1 as (p1') "[Hm1 #Hp13]".
iDestruct ("H1" with "Hm1") as (p2'') "[H1 Hm2]".
iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto].
iIntros "!>". iRewrite "Hp13". by iApply ("IH" with "H1").
Qed.
(** ** Lemmas about the auxiliary definitions and invariants *)
Global Instance iProto_app_recvs_ne vs :
NonExpansive (iProto_app_recvs (Σ:=Σ) (V:=V) vs).
Proof. induction vs; solve_proper. Qed.
Global Instance iProto_app_recvs_proper vs :
Proper ((≡) ==> (≡)) (iProto_app_recvs (Σ:=Σ) (V:=V) vs).
Proof. induction vs; solve_proper. Qed.
Global Instance iProto_interp_ne vsl vsr :
NonExpansive2 (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
Proof. solve_proper. Qed.
Global Instance iProto_interp_proper vsl vsr :
Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
Proof. apply (ne_proper_2 _). Qed.
Global Instance iProto_own_frag_ne γ : NonExpansive (iProto_own_frag γ).
Proof. solve_proper. Qed.
Lemma iProto_own_auth_agree γ p p' :
iProto_own_auth γ p -∗ iProto_own_frag γ p' -∗ ▷ (p ≡ p').
Proof.
iIntros "H● H◯". iCombine "H● H◯" gives "H✓".
iDestruct (excl_auth_agreeI with "H✓") as "{H✓} H✓".
iApply (later_equivI_1 with "H✓").
Qed.
Lemma iProto_own_auth_update γ p p' p'' :
iProto_own_auth γ p -∗ iProto_own_frag γ p' ==∗
iProto_own_auth γ p'' ∗ iProto_own_frag γ p''.
Proof.
iIntros "H● H◯". iDestruct (own_update_2 with "H● H◯") as "H".
{ eapply (excl_auth_update _ _ (Next p'')). }
by rewrite own_op.
Qed.
Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
Proof. iExists p; simpl. iSplitL; iApply iProto_le_refl. Qed.
Lemma iProto_interp_sym vsl vsr pl pr :
iProto_interp vsl vsr pl pr ⊢ iProto_interp vsr vsl pr pl.
Proof.
iDestruct 1 as (p) "[Hp Hdp]". iExists (iProto_dual p).
rewrite (involutive iProto_dual). iFrame.
Qed.
Lemma iProto_interp_le_l vsl vsr pl pl' pr :
iProto_interp vsl vsr pl pr -∗ pl ⊑ pl' -∗ iProto_interp vsl vsr pl' pr.
Proof.
iDestruct 1 as (p) "[Hp Hdp]". iIntros "Hle". iExists p.
iFrame "Hdp". by iApply (iProto_le_trans with "Hp").
Qed.
Lemma iProto_interp_le_r vsl vsr pl pr pr' :
iProto_interp vsl vsr pl pr -∗ pr ⊑ pr' -∗ iProto_interp vsl vsr pl pr'.
Proof.
iIntros "H Hle". iApply iProto_interp_sym.
iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_sym.
Qed.
Lemma iProto_interp_send vl ml vsl vsr pr pl' :
iProto_interp vsl vsr (<!> ml) pr -∗
iMsg_car ml vl (Next pl') -∗
▷^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
Proof.
iDestruct 1 as (p) "[Hp Hdp] /="; iIntros "Hml".
iDestruct (iProto_le_trans _ _ (<!> MSG vl; pl') with "Hp [Hml]") as "Hp".
{ iApply iProto_le_send. rewrite iMsg_base_eq. iIntros (v' p') "(->&Hp&_) /=".
iExists p'. iSplitR; [iApply iProto_le_refl|]. by iRewrite -"Hp". }
iInduction vsr as [|vr vsr] "IH" forall (pl'); simpl.
{ iExists pl'; simpl. iSplitR; [iApply iProto_le_refl|].
iApply (iProto_le_trans with "[Hp] Hdp").
iInduction vsl as [|vl' vsl] "IH"; simpl.
{ iApply iProto_le_dual_r. rewrite iProto_dual_message iMsg_dual_base /=.
by rewrite involutive. }
iApply iProto_le_base; iIntros "!>". by iApply "IH". }
iDestruct (iProto_le_recv_send_inv _ _ vr vl
(iProto_app_recvs vsr p) pl' with "Hp [] []") as (p') "[H1 H2]";
[rewrite iMsg_base_eq; by auto..|].
iIntros "!>". iSpecialize ("IH" with "Hdp H1"). iIntros "!>".
iDestruct "IH" as (p'') "[Hp'' Hdp'']". iExists p''. iFrame "Hdp''".
iApply (iProto_le_trans with "[Hp''] H2"); simpl. by iApply iProto_le_base.
Qed.
Lemma iProto_interp_recv vl vsl vsr pl mr :
iProto_interp (vl :: vsl) vsr pl (<?> mr) -∗
∃ pr, iMsg_car mr vl (Next pr) ∗ ▷ iProto_interp vsl vsr pl pr.
Proof.
iDestruct 1 as (p) "[Hp Hdp] /=".
iDestruct (iProto_le_recv_inv with "Hdp") as (m) "[#Hm Hpr]".
iDestruct (iProto_message_equivI with "Hm") as (_) "{Hm} #Hm".
iDestruct ("Hpr" $! vl (iProto_app_recvs vsl (iProto_dual p)) with "[]")
as (pr'') "[Hler Hpr]".
{ iRewrite -("Hm" $! vl (Next (iProto_app_recvs vsl (iProto_dual p)))).
rewrite iMsg_base_eq; auto. }
iExists pr''. iIntros "{$Hpr} !>". iExists p. iFrame.
Qed.
Lemma iProto_ctx_sym γl γr vsl vsr :
iProto_ctx γl γr vsl vsr ⊢ iProto_ctx γr γl vsr vsl.
Proof.
iIntros "(%pl & %pr & Hauthl & Hauthr & Hinterp)".
iDestruct (iProto_interp_sym with "Hinterp") as "Hinterp".
iExists pr, pl; iFrame.
Qed.
Global Instance iProto_own_ne γ : NonExpansive (iProto_own γ).
Proof. solve_proper. Qed.
Global Instance iProto_own_proper γ : Proper ((≡) ==> (≡)) (iProto_own γ).
Proof. apply (ne_proper _). Qed.
Lemma iProto_own_le γ p1 p2 :
iProto_own γ p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ p2.
Proof.
iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
Qed.
Lemma iProto_init p :
⊢ |==> ∃ γl γr,
iProto_ctx γl γr [] [] ∗
iProto_own γl p ∗ iProto_own γr (iProto_dual p).
Proof.
iMod (own_alloc (●E (Next p) ⋅ ◯E (Next p))) as (γl) "[H●l H◯l]".
{ by apply excl_auth_valid. }
iMod (own_alloc (●E (Next (iProto_dual p)) ⋅
◯E (Next (iProto_dual p)))) as (γr) "[H●r H◯r]".
{ by apply excl_auth_valid. }
iModIntro. iExists γl, γr. iSplitL "H●l H●r".
{ iExists p, (iProto_dual p). iFrame. iApply iProto_interp_nil. }
iSplitL "H◯l"; iExists _; iFrame; iApply iProto_le_refl.
Qed.
Lemma iProto_send γl γr m vsr vsl vl p :
iProto_ctx γl γr vsl vsr -∗
iProto_own γl (<!> m) -∗
iMsg_car m vl (Next p) ==∗
▷^(length vsr) iProto_ctx γl γr (vsl ++ [vl]) vsr ∗
iProto_own γl p.
Proof.
iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
iDestruct 1 as (pl') "[Hle H◯]". iIntros "Hm".
iDestruct (iProto_own_auth_agree with "H●l H◯") as "#Hp".
iAssert (▷ (pl ⊑ <!> m))%I
with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
iMod (iProto_own_auth_update _ _ _ p with "H●l H◯") as "[H●l H◯]".
iIntros "!>". iSplitR "H◯".
- iIntros "!>". iExists p, pr. iFrame.
- iExists p. iFrame. iApply iProto_le_refl.
Qed.
Lemma iProto_recv γl γr m vr vsr vsl :
iProto_ctx γl γr vsl (vr :: vsr) -∗
iProto_own γl (<?> m) ==∗
▷ ∃ p,
iProto_ctx γl γr vsl vsr ∗
iProto_own γl p ∗
iMsg_car m vr (Next p).
Proof.
iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
iDestruct 1 as (p) "[Hle H◯]".
iDestruct (iProto_own_auth_agree with "H●l H◯") as "#Hp".
iDestruct (iProto_interp_le_l with "Hinterp [Hle]") as "Hinterp".
{ iIntros "!>". by iRewrite "Hp". }
iDestruct (iProto_interp_sym with "Hinterp") as "Hinterp".
iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
iMod (iProto_own_auth_update _ _ _ q with "H●l H◯") as "[H●l H◯]".
iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "H◯".
- iExists q, pr. iFrame. by iApply iProto_interp_sym.
- iExists q. iIntros "{$H◯} !>". iApply iProto_le_refl.
Qed.
(** The instances below make it possible to use the tactics [iIntros],
[iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [iProto_le] goals. *)
Global Instance iProto_le_from_forall_l {A} a (m1 : A → iMsg Σ V) m2 name :
AsIdentName m1 name →
FromForall (iProto_message Recv (iMsg_exist m1) ⊑ (<a> m2))
(λ x, (<?> m1 x) ⊑ (<a> m2))%I name | 10.
Proof. intros _. apply iProto_le_exist_elim_l. Qed.
Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A → iMsg Σ V) name :
AsIdentName m2 name →
FromForall ((<a> m1) ⊑ iProto_message Send (iMsg_exist m2))
(λ x, (<a> m1) ⊑ (<!> m2 x))%I name | 11.
Proof. intros _. apply iProto_le_exist_elim_r. Qed.
Global Instance iProto_le_from_wand_l a m v P p :
TCIf (TCEq P True%I) False TCTrue →
FromWand ((<?> MSG v {{ P }}; p) ⊑ (<a> m)) P ((<?> MSG v; p) ⊑ (<a> m)) | 10.
Proof. intros _. apply iProto_le_payload_elim_l. Qed.
Global Instance iProto_le_from_wand_r a m v P p :
FromWand ((<a> m) ⊑ (<!> MSG v {{ P }}; p)) P ((<a> m) ⊑ (<!> MSG v; p)) | 11.
Proof. apply iProto_le_payload_elim_r. Qed.
Global Instance iProto_le_from_exist_l {A} (m : A → iMsg Σ V) p :
FromExist ((<! x> m x) ⊑ p) (λ a, (<!> m a) ⊑ p)%I | 10.
Proof.
rewrite /FromExist. iDestruct 1 as (x) "H".
iApply (iProto_le_trans with "[] H"). iApply iProto_le_exist_intro_l.
Qed.
Global Instance iProto_le_from_exist_r {A} (m : A → iMsg Σ V) p :
FromExist (p ⊑ <? x> m x) (λ a, p ⊑ (<?> m a))%I | 11.
Proof.
rewrite /FromExist. iDestruct 1 as (x) "H".
iApply (iProto_le_trans with "H"). iApply iProto_le_exist_intro_r.
Qed.
Global Instance iProto_le_from_sep_l m v P p :
FromSep ((<!> MSG v {{ P }}; p) ⊑ (<!> m)) P ((<!> MSG v; p) ⊑ (<!> m)) | 10.
Proof.
rewrite /FromSep. iIntros "[HP H]".
iApply (iProto_le_trans with "[HP] H"). by iApply iProto_le_payload_intro_l.
Qed.
Global Instance iProto_le_from_sep_r m v P p :
FromSep ((<?> m) ⊑ (<?> MSG v {{ P }}; p)) P ((<?> m) ⊑ (<?> MSG v; p)) | 11.
Proof.
rewrite /FromSep. iIntros "[HP H]".
iApply (iProto_le_trans with "H"). by iApply iProto_le_payload_intro_r.
Qed.
Global Instance iProto_le_frame_l q m v R P Q p :
Frame q R P Q →
Frame q R ((<!> MSG v {{ P }}; p) ⊑ (<!> m))
((<!> MSG v {{ Q }}; p) ⊑ (<!> m)) | 10.
Proof.
rewrite /Frame /=. iIntros (HP) "[HR H]".
iApply (iProto_le_trans with "[HR] H"). iApply iProto_le_payload_elim_r.
iIntros "HQ". iApply iProto_le_payload_intro_l. iApply HP; iFrame.
Qed.
Global Instance iProto_le_frame_r q m v R P Q p :
Frame q R P Q →
Frame q R ((<?> m) ⊑ (<?> MSG v {{ P }}; p))
((<?> m) ⊑ (<?> MSG v {{ Q }}; p)) | 11.
Proof.
rewrite /Frame /=. iIntros (HP) "[HR H]".
iApply (iProto_le_trans with "H"). iApply iProto_le_payload_elim_l.
iIntros "HQ". iApply iProto_le_payload_intro_r. iApply HP; iFrame.
Qed.
Global Instance iProto_le_from_modal a v p1 p2 :
FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
Proof. intros _. apply iProto_le_base. Qed.
End proto.
Global Typeclasses Opaque iProto_ctx iProto_own.
Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
actris/channel/proto_model.v 0 → 100644
View file @ c9249305
(** This file defines the model of dependent separation protocols as the
solution of a recursive domain equation, along with various primitive
operations, such as append and map.
Important: This file should not be used directly, but rather the wrappers in
[proto] should be used.
Dependent Separation Protocols are modeled as the solution of the following
recursive domain equation:
[proto = 1 + (action * (V → ▶ proto → PROP))]
Here, the left-hand side of the sum is used for the terminated process, while
the right-hand side is used for the communication constructors. The type
[action] is an inductively defined datatype with two constructors [Send] and
[Recv]. Compared to having an additional sum in [proto], this makes it
possible to factorize the code in a better way.
The remainder [V → ▶ proto → PROP] is a predicate that ranges over the
communicated value [V] and the tail protocol [proto]. Note that to solve this
recursive domain equation using Iris's COFE solver, the recursive occurrence
of [proto] appear under the later [▶].
On top of the type [proto], we define the constructors:
- [proto_end], which constructs the left-side of the sum.
- [proto_msg], which takes an action and a predicate and constructs the
right-hand side of the sum accordingly.
The defined functions on the type [proto] are:
- [proto_map], which can be used to map the actions and the propositions of
a given protocol.
- [proto_app], which appends two protocols [p1] and [p2], by substituting
all terminations [END] in [p1] with [p2]. *)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import proofmode.
From actris.utils Require Import cofe_solver_2.
Set Default Proof Using "Type".
Module Export action.
Inductive action := Send | Recv.
Global Instance action_inhabited : Inhabited action := populate Send.
Definition action_dual (a : action) : action :=
match a with Send => Recv | Recv => Send end.
Global Instance action_dual_involutive : Involutive (=) action_dual.
Proof. by intros []. Qed.
Canonical Structure actionO := leibnizO action.
End action.
Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe :=
optionO (prodO actionO (V -d> laterO A -n> PROP)).
Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
optionOF (actionO * (V -d> ▶ ∙ -n> PROP)).
Definition pre_proto_result (V : Type) := result_2 (proto_auxOF V).
Definition pre_proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
solution_2_car (pre_proto_result V) PROPn _ PROP _.
Global Instance pre_proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} :
Cofe (pre_proto V PROPn PROP).
Proof. apply _. Qed.
Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
proto_auxO V PROP (pre_proto V PROP PROPn).
Global Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} :
Cofe (proto V PROPn PROP).
Proof. apply _. Qed.
Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
ofe_iso (proto V PROPn PROP) (pre_proto V PROPn PROP).
Proof. apply pre_proto_result. Qed.
Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
pre_proto V PROPn PROP -n> proto V PROPn PROP := ofe_iso_2 proto_iso.
Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
proto V PROPn PROP -n> pre_proto V PROPn PROP := ofe_iso_1 proto_iso.
Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
proto_fold (proto_unfold p) ≡ p.
Proof. apply (ofe_iso_21 proto_iso). Qed.
Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP} (p : pre_proto V PROPn PROP) :
proto_unfold (proto_fold p) ≡ p.
Proof. apply (ofe_iso_12 proto_iso). Qed.
Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
None.
Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
(m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
Some (a, λ v, m v ◎ laterO_map proto_fold).
Global Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
Proper (pointwise_relation V (dist n) ==> dist n)
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof.
intros c1 c2 Hc. rewrite /proto_message.
(repeat constructor)=> //= v. by f_equiv.
Qed.
Global Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
Proper (pointwise_relation V (≡) ==> (≡))
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof.
intros c1 c2 Hc. rewrite /proto_message.
(repeat constructor)=> //= v. by f_equiv.
Qed.
Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
p ≡ proto_end ∨ ∃ a m, p ≡ proto_message a m.
Proof.
destruct p as [[a m]|]; [|by left].
right. exists a, (λ v, m v ◎ laterO_map proto_unfold).
rewrite /proto_message. do 2 f_equiv. intros v p; simpl. f_equiv.
rewrite -later_map_compose -{1}(later_map_id p).
apply later_map_ext=> p' /=. by rewrite proto_unfold_fold.
Qed.
Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end.
Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
Proof.
rewrite /proto_message option_equivI prod_equivI /=.
rewrite discrete_eq discrete_fun_equivI. f_equiv; [done|]. f_equiv=> x.
rewrite ofe_morO_equivI /=. iSplit; iIntros "H %p //".
assert (p ≡ later_map proto_fold (later_map proto_unfold p)) as ->; last done.
rewrite -later_map_compose -{1}(later_map_id p).
apply later_map_ext=> p' /=. by rewrite proto_fold_unfold.
Qed.
Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{SPROP} False.
Proof. by rewrite option_equivI. Qed.
Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
(p : proto V PROPn PROP) : A :=
match p with
| None => x
| Some (a, m) => f a (λ v, m v ◎ laterO_map proto_unfold)
end.
Global Arguments proto_elim : simpl never.
Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f1 f2 : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n :
(∀ a m1 m2, (∀ v, m1 v ≡{n}≡ m2 v) → f1 a m1 ≡{n}≡ f2 a m2) →
p1 ≡{n}≡ p2 →
proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2.
Proof.
intros Hf [[a1 m1] [a2 m2] [[=->] ?]|]; rewrite /proto_elim //=.
apply Hf=> v. by f_equiv.
Qed.
Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) :
proto_elim x f proto_end ≡ x.
Proof. done. Qed.
Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) a m :
(∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)) →
proto_elim x f (proto_message a m) ≡ f a m.
Proof.
intros. rewrite /proto_elim /proto_message /=. f_equiv=> v p /=. f_equiv.
rewrite -later_map_compose -{2}(later_map_id p).
apply later_map_ext=> p' /=. by rewrite proto_fold_unfold.
Qed.
(** Functor *)
Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
proto_elim proto_end (λ a m, proto_message a (λ v, g ◎ m v ◎ laterO_map rec)) p.
Next Obligation.
intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv.
Qed.
Global Instance proto_map_aux_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
Proof.
intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm.
f_equiv=> v p' /=. do 2 f_equiv; [done|].
apply Next_contractive; by dist_later_intro as n' Hn'.
Qed.
Definition proto_map_aux_2 {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP')
(rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
proto V PROPn PROP -n> proto V PROPn' PROP' :=
proto_map_aux g (proto_map_aux gn rec).
Global Instance proto_map_aux_2_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
Contractive (proto_map_aux_2 (V:=V) gn g).
Proof.
intros n rec1 rec2 Hrec. rewrite /proto_map_aux_2.
f_equiv. by apply proto_map_aux_contractive.
Qed.
Definition proto_map {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
proto V PROPn PROP -n> proto V PROPn' PROP' :=
fixpoint (proto_map_aux_2 gn g).
Lemma proto_map_unfold {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
proto_map (V:=V) gn g p ≡ proto_map_aux g (proto_map g gn) p.
Proof.
apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
induction (lt_wf n) as [n _ IH]=>
PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
apply proto_map_aux_contractive; constructor=> n' ?. symmetry. 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. Qed.
Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
proto_map (V:=V) gn g (proto_message a m)
≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
rewrite ->proto_elim_message; [done|].
intros a' m1 m2 Hm. f_equiv; solve_proper.
Qed.
Lemma proto_map_ne {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
gn1 ≡{n}≡ gn2 → g1 ≡{n}≡ g2 →
proto_map (V:=V) gn1 g1 p ≡{n}≡ proto_map (V:=V) gn2 g2 p.
Proof.
revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn1 gn2 g1 g2 p.
induction (lt_wf n) as [n _ IH]=>
PROPn ? PROPn' ? PROP ? PROP' ? gn1 gn2 g1 g2 p Hgn Hg /=.
destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_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 :
gn1 ≡ gn2 → g1 ≡ g2 → proto_map (V:=V) gn1 g1 p ≡ proto_map (V:=V) gn2 g2 p.
Proof.
intros Hgn Hg. apply equiv_dist=> n.
apply proto_map_ne=> // ?; by apply equiv_dist.
Qed.
Lemma proto_map_id {V} `{Hcn:!Cofe PROPn, Hc:!Cofe PROP} (p : proto V PROPn PROP) :
proto_map cid cid p ≡ p.
Proof.
apply equiv_dist=> n. revert PROPn Hcn PROP Hc p.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
apply Next_contractive; dist_later_intro as n' Hn'; auto.
Qed.
Lemma proto_map_compose {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
Hc:!Cofe PROP, Hc':!Cofe PROP', Hc'':!Cofe PROP''}
(gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
(g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
proto_map (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map gn1 g2 (proto_map gn2 g1 p).
Proof.
apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROPn'' Hcn''
PROP Hc PROP' Hc' PROP'' Hc'' gn1 gn2 g1 g2 p.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROPn' ? PROPn'' ?
PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
do 3 f_equiv. apply Next_contractive; dist_later_intro as n' Hn'; simpl; auto.
Qed.
Program Definition protoOF (V : Type) (Fn F : oFunctor)
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} : oFunctor := {|
oFunctor_car A _ B _ := proto V (oFunctor_car Fn B A) (oFunctor_car F A B);
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
proto_map (oFunctor_map Fn (fg.2, fg.1)) (oFunctor_map F fg)
|}.
Next Obligation.
intros V Fn F ?? A1 ? A2 ? B1 ? B2 ? n f g [??] p; simpl in *.
apply proto_map_ne=> // y; by apply oFunctor_map_ne.
Qed.
Next Obligation.
intros V Fn F ?? A ? B ? p; simpl in *. rewrite /= -{2}(proto_map_id p).
apply proto_map_ext=> //= y; by rewrite oFunctor_map_id.
Qed.
Next Obligation.
intros V Fn F ?? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' p; simpl in *.
rewrite -proto_map_compose.
apply proto_map_ext=> //= y; by rewrite ofe.oFunctor_map_compose.
Qed.
Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
oFunctorContractive Fn → oFunctorContractive F →
oFunctorContractive (protoOF V Fn F).
Proof.
intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
apply proto_map_ne=> y //=.
+ apply HFn. dist_later_intro as n' Hn'. f_equiv; apply Hfg.
+ apply HF. by dist_later_intro as n' Hn'.
Qed.
actris/examples/basics.v 0 → 100644
View file @ c9249305
(** This file includes basic examples that each describe a unique feature of
dependent separation protocols. *)
From actris.channel Require Import proofmode.
From iris.heap_lang Require Import lib.spin_lock.
From actris.utils Require Import contribution.
Local Existing Instance spin_lock.
(** Basic *)
Definition prog : val := λ: <>,
let: "c" := fork_chan (λ: "c'", send "c'" #42) in
recv "c".
(** Tranfering References *)
Definition prog_ref : val := λ: <>,
let: "c" := fork_chan (λ: "c'", send "c'" (ref #42)) in
! (recv "c").
(** Delegation, i.e. transfering channels *)
Definition prog_del : val := λ: <>,
let: "c1" := fork_chan (λ: "c1'",
let: "cc2" := new_chan #() in
send "c1'" (Fst "cc2");;
send (Snd "cc2") #42) in
recv (recv "c1").
(** Dependent protocols *)
Definition prog_dep : val := λ: <>,
let: "c" := fork_chan (λ: "c'",
let: "x" := recv "c'" in send "c'" ("x" + #2)) in
send "c" #40;;
recv "c".
Definition prog_dep_ref : val := λ: <>,
let: "c" := fork_chan (λ: "c'",
let: "l" := recv "c'" in "l" <- !"l" + #2;; send "c'" #()) in
let: "l" := ref #40 in send "c" "l";; recv "c";; !"l".
Definition prog_dep_del : val := λ: <>,
let: "c1" := fork_chan (λ: "c1'",
let: "cc2" := new_chan #() in
send "c1'" (Fst "cc2");;
let: "x" := recv (Snd "cc2") in send (Snd "cc2") ("x" + #2)) in
let: "c2'" := recv "c1" in send "c2'" #40;; recv "c2'".
Definition prog_dep_del_2 : val := λ: <>,
let: "c1" := fork_chan (λ: "c1'",
send (recv "c1'") #40;;
send "c1'" #()) in
let: "c2" := fork_chan (λ: "c2'",
let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
send "c1" "c2";; recv "c1";; recv "c2".
Definition prog_dep_del_3 : val := λ: <>,
let: "c1" := fork_chan (λ: "c1'",
let: "c" := recv "c1'" in let: "y" := recv "c1'" in
send "c" "y";; send "c1'" #()) in
let: "c2" := fork_chan (λ: "c2'",
let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
send "c1" "c2";; send "c1" #40;; recv "c1";; recv "c2".
(** Loops *)
Definition prog_loop : val := λ: <>,
let: "c" := fork_chan (rec: "go" "c'" :=
let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
send "c" #18;;
let: "x1" := recv "c" in
send "c" #20;;
let: "x2" := recv "c" in
"x1" + "x2".
(** Transfering higher-order functions *)
Definition prog_fun : val := λ: <>,
let: "c" := fork_chan (λ: "c'",
let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
let: "r" := ref #40 in
send "c" (λ: <>, !"r");;
recv "c" #().
(** Lock protected channel endpoints *)
Definition prog_lock : val := λ: <>,
let: "c" := fork_chan (λ: "c'",
let: "l" := newlock #() in
Fork (acquire "l";; send "c'" #21;; release "l");;
acquire "l";; send "c'" #21;; release "l") in
recv "c" + recv "c".
(** Swapping of sends *)
Definition prog_swap : val := λ: <>,
let: "c" := fork_chan (λ: "c'",
send "c'" #20;;
let: "y" := recv "c'" in
send "c'" ("y" + #2)) in
send "c" #20;;
recv "c" + recv "c".
Definition prog_swap_twice : val := λ: <>,
let: "c" := fork_chan (λ: "c'",
send "c'" #20;;
let: "y1" := recv "c'" in
let: "y2" := recv "c'" in
send "c'" ("y1" + "y2")) in
send "c" #11;; send "c" #11;;
recv "c" + recv "c".
Definition prog_swap_loop : val := λ: <>,
let: "c" := fork_chan (rec: "go" "c'" :=
let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
send "c" #18;;
send "c" #20;;
let: "x1" := recv "c" in
let: "x2" := recv "c" in
"x1" + "x2".
Definition prog_ref_swap_loop : val := λ: <>,
let: "c" := fork_chan (rec: "go" "c'" :=
let: "l" := recv "c'" in
"l" <- !"l" + #2;; send "c'" #();; "go" "c'") in
let: "l1" := ref #18 in
let: "l2" := ref #20 in
send "c" "l1";;
send "c" "l2";;
recv "c";; recv "c";;
!"l1" + !"l2".
Section proofs.
Context `{heapGS Σ, chanG Σ}.
(** Protocols for the respective programs *)
Definition prot : iProto Σ :=
(<?> MSG #42; END)%proto.
Definition prot_ref : iProto Σ :=
(<? (l : loc)> MSG #l {{ l ↦ #42 }}; END)%proto.
Definition prot_del : iProto Σ :=
(<? c> MSG c {{ c ↣ prot }}; END)%proto.
Definition prot_dep : iProto Σ :=
(<! (x : Z)> MSG #x; <?> MSG #(x + 2); END)%proto.
Definition prot_dep_ref : iProto Σ :=
(<! (l : loc) (x : Z)> MSG #l {{ l ↦ #x }};
<?> MSG #() {{ l ↦ #(x + 2) }};
END)%proto.
Definition prot_dep_del : iProto Σ :=
(<? c> MSG c {{ c ↣ prot_dep }}; END)%proto.
Definition prot_dep_del_2 : iProto Σ :=
(<! c> MSG c {{ c ↣ prot_dep }};
<?> MSG #() {{ c ↣ <?> MSG #42; END }};
END)%proto.
Definition prot_dep_del_3 : iProto Σ :=
(<! c> MSG c {{ c ↣ prot_dep }};
<! (y : Z)> MSG #y; <?> MSG #() {{ c ↣ <?> MSG #(y + 2); END }};
END)%proto.
Definition prot_loop_aux (rec : iProto Σ) : iProto Σ :=
(<! (x : Z)> MSG #x; <?> MSG #(x + 2); rec)%proto.
Instance prot_loop_contractive : Contractive prot_loop_aux.
Proof. solve_proto_contractive. Qed.
Definition prot_loop : iProto Σ := fixpoint prot_loop_aux.
Global Instance prot_loop_unfold :
ProtoUnfold prot_loop (prot_loop_aux prot_loop).
Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
Definition prot_ref_loop_aux (rec : iProto Σ) : iProto Σ :=
(<! (l : loc) (x : Z)> MSG #l {{ l ↦ #x }}; <?> MSG #() {{ l ↦ #(x+2) }}; rec)%proto.
Instance prot_ref_loop_contractive : Contractive prot_ref_loop_aux.
Proof. solve_proto_contractive. Qed.
Definition prot_ref_loop : iProto Σ := fixpoint prot_ref_loop_aux.
Global Instance prot_ref_loop_unfold :
ProtoUnfold prot_ref_loop (prot_ref_loop_aux prot_ref_loop).
Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
Definition prot_fun : iProto Σ :=
(<! (P : iProp Σ) (Φ : Z → iProp Σ) (vf : val)>
MSG vf {{ {{{ P }}} vf #() {{{ x, RET #x; Φ x }}} }};
<? (vg : val)>
MSG vg {{ {{{ P }}} vg #() {{{ x, RET #(x + 2); Φ x }}} }};
END)%proto.
Fixpoint prot_lock (n : nat) : iProto Σ :=
match n with
| 0 => END
| S n' => <?> MSG #21; prot_lock n'
end%proto.
Definition prot_swap : iProto Σ :=
(<! (x : Z)> MSG #x;
<?> MSG #20;
<?> MSG #(x + 2); END)%proto.
Definition prot_swap_twice : iProto Σ :=
(<! (x : Z)> MSG #x;
<! (y : Z)> MSG #y;
<?> MSG #20;
<?> MSG #(x+y); END)%proto.
Definition prot_swap_loop : iProto Σ :=
(<! (x : Z)> MSG #x;
<! (y : Z)> MSG #y;
<?> MSG #(x+2);
<?> MSG #(y+2); prot_loop)%proto.
(** Specs and proofs of the respective programs *)
Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot); iIntros (c) "Hc".
- by wp_send with "[]".
- wp_recv as "_". by iApply "HΦ".
Qed.
Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_ref); iIntros (c) "Hc".
- wp_alloc l as "Hl". by wp_send with "[$Hl]".
- wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
Qed.
Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_del); iIntros (c) "Hc".
- wp_smart_apply (new_chan_spec prot with "[//]").
iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
- wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.
Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c) "Hc".
- wp_recv (x) as "_". by wp_send with "[]".
- wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
Qed.
Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_dep_ref); iIntros (c) "Hc".
- wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
- wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
by iApply "HΦ".
Qed.
Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_dep_del); iIntros (c) "Hc".
- wp_smart_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
- wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
by iApply "HΦ".
Qed.
Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_dep_del_2); iIntros (c) "Hc".
{ wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
{ wp_recv (x) as "_". by wp_send with "[//]". }
wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.
Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_dep_del_3); iIntros (c) "Hc".
{ wp_recv (c2) as "Hc2". wp_recv (y) as "_".
wp_send with "[//]". by wp_send with "[$Hc2]". }
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
{ wp_recv (x) as "_". by wp_send with "[//]". }
wp_send with "[$Hc2]". wp_send with "[//]".
wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.
Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
- iLöb as "IH".
wp_recv (x) as "_". wp_send with "[//]".
by wp_smart_apply "IH".
- wp_send with "[//]". wp_recv as "_". wp_send with "[//]". wp_recv as "_".
wp_pures. by iApply "HΦ".
Qed.
Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_fun); iIntros (c) "Hc".
- wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
iIntros "!>" (Ψ') "HP HΨ'". wp_smart_apply ("Hf" with "HP"); iIntros (x) "HΨ".
wp_pures. by iApply "HΨ'".
- wp_alloc l as "Hl".
wp_send ((l ↦ #40)%I (λ w, ⌜ w = 40%Z ⌝ ∗ l ↦ #40)%I) with "[]".
{ iIntros "!>" (Ψ') "Hl HΨ'". wp_load. iApply "HΨ'"; auto. }
wp_recv (vg) as "#Hg". wp_smart_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
by iApply "HΦ".
Qed.
Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
{{{ True }}} prog_lock #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec (prot_lock 2)); iIntros (c) "Hc".
- iMod contribution_init as (γ) "Hs".
iMod (alloc_client with "Hs") as "[Hs Hcl1]".
iMod (alloc_client with "Hs") as "[Hs Hcl2]".
wp_smart_apply (newlock_spec (∃ n, server γ n ε ∗
c ↣ iProto_dual (prot_lock n))%I
with "[Hc Hs]"); first by eauto with iFrame.
iIntros (lk γlk) "#Hlk".
iAssert (client γ ε -∗
WP acquire lk;; send c #21;; release lk {{ _, True }})%I with "[]" as "#Hhelp".
{ iIntros "Hcl".
wp_smart_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
iDestruct "H" as (n) "[Hs Hc]".
iDestruct (server_agree with "Hs Hcl") as %[? _].
destruct n as [|n]=> //=. wp_send with "[//]".
iMod (dealloc_client with "Hs Hcl") as "Hs /=".
wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]"); eauto with iFrame. }
wp_smart_apply (wp_fork with "[Hcl1]").
{ iNext. by iApply "Hhelp". }
by wp_smart_apply "Hhelp".
- wp_recv as "_". wp_recv as "_". wp_pures. by iApply "HΦ".
Qed.
Lemma prog_swap_spec : {{{ True }}} prog_swap #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_swap); iIntros (c) "Hc".
- wp_send with "[//]". wp_recv (x) as "_". by wp_send with "[//]".
- wp_send with "[//]". wp_recv as "_". wp_recv as "_".
wp_pures. by iApply "HΦ".
Qed.
Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_swap_twice); iIntros (c) "Hc".
- wp_send with "[//]". wp_recv (x1) as "_". wp_recv (x2) as "_".
by wp_send with "[//]".
- wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
wp_pures. by iApply "HΦ".
Qed.
Lemma prog_swap_loop_spec : {{{ True }}} prog_swap_loop #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
- iLöb as "IH".
wp_recv (x) as "_". wp_send with "[//]".
by wp_smart_apply "IH".
- wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
wp_pures. by iApply "HΦ".
Qed.
(** This lemma is stated as the underlying weakest precondition of the
hoare triple notation to make it equivalent to what is presented in the
Actris journal paper *)
Lemma prog_ref_swap_loop_spec : ∀ Φ, Φ #42 -∗ WP prog_ref_swap_loop #() {{ Φ }}.
Proof.
iIntros (Φ) "HΦ". wp_lam.
wp_smart_apply (fork_chan_spec prot_ref_loop); iIntros (c) "Hc".
- iLöb as "IH". wp_lam.
wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
by wp_smart_apply "IH".
- wp_alloc l1 as "Hl1". wp_alloc l2 as "Hl2".
wp_send with "[$Hl1]". wp_send with "[$Hl2]".
wp_recv as "Hl1". wp_recv as "Hl2".
wp_load. wp_load.
wp_pures. by iApply "HΦ".
Qed.
End proofs.
actris/examples/equivalence.v 0 → 100644
View file @ c9249305
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 0 → 100644
View file @ c9249305
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
View file @ c9249305
(** This file implements a map-reduce program,
a specification thereof and its proofs. *)
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
(** This file implements a simple distributed map-reduce function, a
specification thereof, and its proofs. *)
From actris.channel Require Import proofmode.
From actris.utils Require Import llist compare contribution group.
From actris.examples Require Import map sort_fg.
From actris.examples Require Import par_map sort_fg.
From iris.algebra Require Import gmultiset.
(** Functional version of map reduce (aka the specification) *)
(** * Functional version of map reduce (aka the specification) *)
Definition map_reduce {A B C} `{EqDecision K}
(map : A → list (K * B)) (red : K → list B → list C) : list A → list C :=
mbind (curry red) ∘ group ∘ mbind map.
Instance: Params (@map_reduce) 7 := {}.
mbind (uncurry red) ∘ group ∘ mbind map.
Global Instance: Params (@map_reduce) 7 := {}.
(** Distributed version *)
(** * Distributed version (aka the implementation) *)
Definition par_map_reduce_map : val :=
rec: "go" "n" "cmap" "csort" "xs" :=
if: "n" = #0 then #() else
......@@ -61,23 +60,23 @@ Definition par_map_reduce_reduce : val :=
Definition cmpZfst : val := λ: "x" "y", Fst "x" ≤ Fst "y".
Definition par_map_reduce : val := λ: "n" "m" "map" "red" "xs",
let: "cmap" := start_chan (λ: "c", par_map_service "n" "map" "c") in
let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in
let: "cmap" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
let: "csort" := fork_chan (λ: "c", sort_service_fg cmpZfst "c") in
par_map_reduce_map "n" "cmap" "csort" "xs";;
send "csort" #stop;;
let: "cred" := start_chan (λ: "c", par_map_service "m" "red" "c") in
let: "cred" := fork_chan (λ: "c", par_map_service "m" "red" "c") in
(* We need the first sorted element in the loop to compare subsequent elements *)
if: ~recv "csort" then #() else (* Handle the empty case *)
let: "jy" := recv "csort" in
par_map_reduce_reduce "m" "csort" "cred" (SOME "jy") "xs".
(** Properties about the functional version *)
(** * Properties about the functional version *)
Section map_reduce.
Context {A B C} `{EqDecision K} (map : A → list (K * B)) (red : K → list B → list C).
Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (curry red)).
Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (uncurry red)).
Proof.
induction 1 as [|[i1 xs1] [i2 xs2] ixss1 ixss2 [??]|[i1 xs1] [i2 xs2] ixss|];
simplify_eq/=; try done.
......@@ -89,15 +88,15 @@ Section map_reduce.
Proof. intros xs1 xs2 Hxs. by rewrite /map_reduce /= Hxs. Qed.
End map_reduce.
(** Correctness proofs of the distributed version *)
(** * Correctness proofs of the distributed version *)
Class map_reduceG Σ A B `{Countable A, Countable B} := {
map_reduce_mapG :> mapG Σ A;
map_reduce_reduceG :> mapG Σ (Z * list B);
map_reduce_mapG :: mapG Σ A;
map_reduce_reduceG :: mapG Σ (Z * list B);
}.
Section mapper.
Context `{Countable A, Countable B} {C : Type}.
Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B}.
Context `{!heapGS Σ, !chanG Σ, !map_reduceG Σ A B}.
Context (IA : A → val → iProp Σ) (IB : Z → B → val → iProp Σ) (IC : C → val → iProp Σ).
Context (map : A → list (Z * B)) (red : Z → list B → list C).
Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
......@@ -116,7 +115,7 @@ Section mapper.
Proof. intros [i1 y1] [i2 y2]. destruct (total (≤)%Z i1 i2); [left|right]; done. Qed.
Instance RZB_trans : Transitive RZB.
Proof. by apply (prod_relation_trans _). Qed.
Lemma RZB_cmp_spec : cmp_spec IZB RZB cmpZfst.
Lemma RZB_cmp_spec : ⊢ cmp_spec IZB RZB cmpZfst.
Proof.
iIntros ([i1 y1] [i2 y2] v1 v2) "!>"; iIntros (Φ) "[HI1 HI2] HΦ".
iDestruct "HI1" as (w1 ->) "HI1". iDestruct "HI2" as (w2 ->) "HI2 /=".
......@@ -143,25 +142,25 @@ Section mapper.
case_bool_decide; wp_pures; simplify_eq/=.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []). rewrite right_id_L. auto with iFrame. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
- wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct xs as [|x xs]; csimpl; wp_pures.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
iApply ("IH" $! _ [] with "[%] Hl Hcmap Hcsort HΦ"); naive_solver.
+ wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+ wp_select. wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
wp_send with "[$HIx]".
wp_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
wp_smart_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
rewrite assoc_L -(comm _ [x]). iApply "HΦ".
- wp_recv (x k) as (Hx) "Hk".
rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)).
wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
wp_smart_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
rewrite right_id.
wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
wp_smart_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=.
rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm.
Qed.
......@@ -189,13 +188,13 @@ Section mapper.
Proof.
iIntros (acc accv Hys Hsort Hi Φ) "[Hl Hcsort] HΦ".
iLöb as "IH" forall (ys Hys Hsort Hi Φ); wp_rec; wp_pures; simpl.
wp_branch as %_|%Hperm; last first; wp_pures.
wp_branch as % _|%Hperm; last first; wp_pures.
{ iApply ("HΦ" $! [] None with "[Hl $Hcsort]"); simpl.
iEval (rewrite !right_id_L); auto with iFrame. }
wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L.
case_bool_decide as Hij; simplify_eq/=; wp_pures.
- wp_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
rewrite -reverse_snoc. wp_apply ("IH" $! (ys ++ [y])
- wp_smart_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
rewrite -reverse_snoc. wp_smart_apply ("IH" $! (ys ++ [y])
with "[%] [%] [//] Hl [Hcsort] [HΦ]"); try iClear "IH".
+ intros ?; discriminate_list.
+ rewrite fmap_app /= assoc_L. by apply Sorted_snoc.
......@@ -212,7 +211,7 @@ Section mapper.
inversion 1 as [|?? [? _]]; discriminate_list || simplify_list_eq.
assert (RZB (j',y') (i,y'')) as [??]; last (simpl in *; lia).
apply (Sorted_StronglySorted _) in Hsort.
eapply elem_of_StronglySorted_app; set_solver.
eapply StronglySorted_app; set_solver.
Qed.
Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred :
......@@ -225,12 +224,12 @@ Section mapper.
llist IC l zs ∗
csort ↣ from_option (λ _, sort_fg_tail_protocol IZB RZB iys
(iys_sorted ++ acc miy)) END%proto miy ∗
cred ↣ par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) ∗
cred ↣ par_map_protocol IZBs IC (uncurry red) n (Y : gmultiset (Z * list B)) ∗
from_option (λ '(i,y,w), IB i y w) True miy
}}}
par_map_reduce_reduce #n csort cred (accv miy) #l
{{{ zs', RET #();
⌜ (group iys_sorted ≫= curry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= curry red ⌝ ∗
⌜ (group iys_sorted ≫= uncurry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= uncurry red ⌝ ∗
llist IC l (zs' ++ zs)
}}}.
Proof.
......@@ -240,14 +239,14 @@ Section mapper.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! [] with "[$Hl]"); iPureIntro; simpl.
by rewrite gmultiset_elements_empty !right_id_L Hmiy. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- destruct miy as [[[i y] w]|]; simplify_eq/=; wp_pures; last first.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
iApply ("IH" $! _ _ None
with "[%] [%] [%] Hl Hcsort Hcred [] HΦ"); naive_solver.
+ wp_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
wp_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
wp_apply (par_map_reduce_collect_spec _ _ _ _ _ [_]
+ wp_smart_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
wp_smart_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
wp_smart_apply (par_map_reduce_collect_spec _ _ _ _ _ [_]
with "[$Hk $Hcsort]"); try done.
iIntros (ys' miy). iDestruct 1 as (? Hmiy') "(Hk & Hcsort & HImiy)"; csimpl.
wp_select; wp_pures. wp_send ((i, reverse (y :: ys'))) with "[Hk]".
......@@ -262,12 +261,12 @@ Section mapper.
rewrite !bind_app /= right_id_L -!assoc_L -(comm _ zs') !assoc_L.
apply (inj (.++ _)).
- wp_recv ([i ys] k) as (Hy) "Hk".
wp_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
wp_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
wp_smart_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
wp_smart_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
iApply ("HΦ" $! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L.
iPureIntro. rewrite (gmultiset_disj_union_difference {[ i,ys ]} Y)
-?gmultiset_elem_of_singleton_subseteq //.
iPureIntro. rewrite (gmultiset_disj_union_difference {[+ (i,ys) +]} Y)
?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
by rewrite right_id_L !assoc_L.
......@@ -276,34 +275,34 @@ Section mapper.
Lemma par_map_reduce_spec n m vmap vred l xs :
0 < n → 0 < m →
map_spec IA IZB map vmap -∗
map_spec IZBs IC (curry red) vred -∗
map_spec IZBs IC (uncurry red) vred -∗
{{{ llist IA l xs }}}
par_map_reduce #n #m vmap vred #l
{{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
Proof.
iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
wp_apply (start_chan_proto_spec (par_map_protocol IA IZB map n ∅));
wp_smart_apply (fork_chan_spec (par_map_protocol IA IZB map n ∅));
iIntros (cmap) "// Hcmap".
{ wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
wp_apply (start_chan_proto_spec (sort_fg_protocol IZB RZB <++> END)%proto);
{ wp_pures. wp_smart_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
wp_smart_apply (fork_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
iIntros (csort) "Hcsort".
{ wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
{ wp_smart_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
iApply RZB_cmp_spec. }
rewrite right_id.
wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
wp_smart_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
wp_apply (start_chan_proto_spec (par_map_protocol IZBs IC (curry red) m ∅));
wp_smart_apply (fork_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
iIntros (cred) "// Hcred".
{ wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
wp_branch as %_|%Hnil; last first.
{ wp_pures. wp_smart_apply (par_map_service_spec with "Hred Hcred"); auto. }
wp_branch as % _|%Hnil; last first.
{ wp_pures. iApply ("HΦ" $! [] with "[$Hl]"); simpl.
by rewrite /map_reduce /= -Hiys -Hnil. }
wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures.
wp_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
wp_smart_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
with "[$Hl $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
iIntros (zs). rewrite /= gmultiset_elements_empty !right_id.
iDestruct 1 as (Hzs) "Hk". wp_pures.
iDestruct 1 as (Hzs) "Hk".
iApply ("HΦ" with "[$Hk]"). by rewrite Hzs Hiys.
Qed.
End mapper.
theories/examples/map.v → actris/examples/par_map.v
View file @ c9249305
(** This file implements a distributed map service,
a specification thereof and its proofs. *)
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation lib.spin_lock.
(** This file implements a distributed mapper service, a specification thereof,
and its proofs. *)
From actris.channel Require Import proofmode.
From iris.heap_lang Require Import lib.spin_lock.
From actris.utils Require Import llist contribution.
From iris.algebra Require Import gmultiset.
Local Existing Instance spin_lock.
(** * Distributed version (aka the implementation) *)
Definition par_map_worker : val :=
rec: "go" "map" "l" "c" :=
acquire "l";;
......@@ -46,19 +49,20 @@ Definition par_map_client_loop : val :=
"go" "n" "c" "xs" "ys".
Definition par_map_client : val := λ: "n" "map" "xs",
let: "c" := start_chan (λ: "c", par_map_service "n" "map" "c") in
let: "c" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
let: "ys" := lnil #() in
par_map_client_loop "n" "c" "xs" "ys";;
lapp "xs" "ys".
(** * Correctness proofs of the distributed version *)
Class mapG Σ A `{Countable A} := {
map_contributionG :> contributionG Σ (gmultisetUR A);
map_lockG :> lockG Σ;
map_contributionG :: contributionG Σ (gmultisetUR A);
map_lockG :: lockG Σ;
}.
Section map.
Context `{Countable A} {B : Type}.
Context `{!heapG Σ, !proto_chanG Σ, !mapG Σ A}.
Context `{!heapGS Σ, !chanG Σ, !mapG Σ A}.
Context (IA : A → val → iProp Σ) (IB : B → val → iProp Σ) (map : A → list B).
Local Open Scope nat_scope.
Implicit Types n : nat.
......@@ -70,12 +74,12 @@ Section map.
nat -d> gmultiset A -d> iProto Σ := λ i X,
let rec : nat → gmultiset A → iProto Σ := rec in
(if i is 0 then END else
((<!> x v, MSG v {{ IA x v }}; rec i (X ⊎ {[ x ]}))
((<! x v> MSG v {{ IA x v }}; rec i (X ⊎ {[+ x +]}))
<+>
rec (pred i) X
) <{⌜ i ≠ 1 ∨ X = ∅ ⌝}&>
<?> x (l : loc), MSG #l {{ ⌜ x ∈ X ⌝ ∗ llist IB l (map x) }};
rec i (X ∖ {[ x ]}))%proto.
<? x (l : loc)> MSG #l {{ ⌜ x ∈ X ⌝ ∗ llist IB l (map x) }};
rec i (X ∖ {[+ x +]}))%proto.
Instance par_map_protocol_aux_contractive : Contractive par_map_protocol_aux.
Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
Definition par_map_protocol := fixpoint par_map_protocol_aux.
......@@ -88,13 +92,13 @@ Section map.
Lemma par_map_worker_spec γl γ vmap lk c :
map_spec vmap -∗
{{{ is_lock nroot γl lk (map_worker_lock_inv γ c) ∗ client γ (∅ : gmultiset A) }}}
{{{ is_lock γl lk (map_worker_lock_inv γ c) ∗ client γ (∅ : gmultiset A) }}}
par_map_worker vmap lk c
{{{ RET #(); True }}}.
Proof.
iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH".
wp_rec; wp_pures.
wp_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
iDestruct "H" as (i X) "[Hs Hc]".
iDestruct (@server_agree with "Hs Hγ") as %[??]; destruct i as [|i]=>//=.
iAssert ⌜ S i ≠ 1 ∨ X = ∅ ⌝%I as %?.
......@@ -102,33 +106,32 @@ Section map.
iDestruct (@server_1_agree with "Hs Hγ") as %?%leibniz_equiv; auto. }
wp_select. wp_branch; wp_pures; last first.
{ iMod (@dealloc_client with "Hs Hγ") as "Hs /=".
wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
{ iExists i, _. iFrame. }
iIntros "_". by iApply "HΦ". }
wp_recv (x v) as "HI".
iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
{ apply (gmultiset_local_update_alloc _ _ {[ x ]}). }
{ apply (gmultiset_local_update_alloc _ _ {[+ x +]}). }
rewrite left_id_L.
wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
{ iExists (S i), _. iFrame. }
clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (l) "HI".
wp_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
clear dependent i X. iIntros "Hu". wp_smart_apply ("Hmap" with "HI"); iIntros (l) "HI".
wp_smart_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
iDestruct "H" as (i X) "[Hs Hc]".
iDestruct (@server_agree with "Hs Hγ")
as %[??%gmultiset_included]; destruct i as [|i]=>//=.
wp_select. wp_send with "[$HI]".
{ by rewrite gmultiset_elem_of_singleton_subseteq. }
wp_select. wp_send with "[$HI]"; first (iPureIntro; multiset_solver).
iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
{ by apply (gmultiset_local_update_dealloc _ _ {[ x ]}). }
{ by apply (gmultiset_local_update_dealloc _ _ {[+ x +]}). }
rewrite gmultiset_difference_diag.
wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
{ iExists (S i), _. iFrame. }
iIntros "Hu". by wp_apply ("IH" with "[$] [$]").
iIntros "Hu". by wp_smart_apply ("IH" with "[$] [$]").
Qed.
Lemma par_map_workers_spec γl γ n vmap lk c :
map_spec vmap -∗
{{{ is_lock nroot γl lk (map_worker_lock_inv γ c) ∗
{{{ is_lock γl lk (map_worker_lock_inv γ c) ∗
[∗] replicate n (client γ (∅:gmultiset A)) }}}
par_map_workers #n vmap lk c
{{{ RET #(); True }}}.
......@@ -137,10 +140,10 @@ Section map.
iInduction n as [|n] "IH"; wp_rec; wp_pures; simpl.
{ by iApply "HΦ". }
iDestruct "Hγs" as "[Hγ Hγs]".
wp_apply (wp_fork with "[Hγ]").
{ iNext. wp_apply (par_map_worker_spec with "Hmap [$]"); auto. }
wp_smart_apply (wp_fork with "[Hγ]").
{ iNext. wp_smart_apply (par_map_worker_spec with "Hmap [$]"); auto. }
wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply ("IH" with "[$] [$]").
wp_smart_apply ("IH" with "[$] [$]").
Qed.
Lemma par_map_service_spec n vmap c :
......@@ -151,10 +154,10 @@ Section map.
Proof.
iIntros "#Hf !>"; iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iMod (contribution_init_pow (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
wp_apply (newlock_spec nroot (map_worker_lock_inv γ c) with "[Hc Hs]").
wp_smart_apply (newlock_spec (map_worker_lock_inv γ c) with "[Hc Hs]").
{ iExists n, ∅. iFrame. }
iIntros (lk γl) "#Hlk".
wp_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
wp_smart_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
Qed.
Lemma par_map_client_loop_spec n c l k xs X ys :
......@@ -170,23 +173,23 @@ Section map.
case_bool_decide; wp_pures; simplify_eq/=.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []); simpl; auto with iFrame. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
- wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct xs as [|x xs]; csimpl; wp_pures.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
iApply ("IH" with "[%] Hl Hk Hc [$]"); naive_solver.
+ wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+ wp_select. wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
wp_send with "[$HIx]".
wp_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
wp_smart_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
rewrite assoc_L -(comm _ [x]). iApply "HΦ".
- wp_recv (x l') as (Hx) "Hl'".
wp_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
wp_apply ("IH" with "[] Hl Hk Hc"); first done.
wp_smart_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
wp_smart_apply ("IH" with "[] Hl Hk Hc"); first done.
iIntros (ys'); iDestruct 1 as (Hys) "Hk"; simplify_eq/=.
iApply ("HΦ" $! (ys' ++ map x)). iSplit.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L.
+ by rewrite -assoc_L.
......@@ -200,12 +203,12 @@ Section map.
{{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
Proof.
iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
wp_apply (start_chan_proto_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
{ wp_apply (par_map_service_spec with "Hmap Hc"); auto. }
wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
wp_smart_apply (fork_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
{ wp_smart_apply (par_map_service_spec with "Hmap Hc"); auto. }
wp_pures. wp_smart_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
wp_smart_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
iIntros (ys) "(?&Hl&Hk)". rewrite /= gmultiset_elements_empty !right_id_L.
wp_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
wp_pures. iApply "HΦ"; auto.
wp_smart_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
iApply "HΦ"; auto.
Qed.
End map.
actris/examples/pizza.v 0 → 100644
View file @ c9249305
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 0 → 100644
View file @ c9249305
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
View file @ c9249305
(** This file implements a distributed Merge Sort,
a specification thereof and its proofs, including
a variant in which the comparison function is sent
over the channel. *)
(** This file implements a distributed version of merge sort, a specification
thereof, and its proofs. There are two variants:
- [sort_service]: a service that takes both a comparison function and a channel
as its arguments.
- [sort_service_func]: a service that only takes a channel as its argument. The
comparison function is sent over the channel. *)
From stdpp Require Import sorting.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From actris.channel Require Import proofmode.
From actris.utils Require Export llist compare.
Definition lmerge : val :=
......@@ -22,8 +24,8 @@ Definition sort_service : val :=
let: "xs" := recv "c" in
if: llength "xs" ≤ #1 then send "c" #() else
let: "zs" := lsplit "xs" in
let: "cy" := start_chan (λ: "c", "go" "cmp" "c") in
let: "cz" := start_chan (λ: "c", "go" "cmp" "c") in
let: "cy" := fork_chan (λ: "c", "go" "cmp" "c") in
let: "cz" := fork_chan (λ: "c", "go" "cmp" "c") in
send "cy" "xs";;
send "cz" "zs";;
recv "cy";; recv "cz";;
......@@ -35,22 +37,21 @@ Definition sort_service_func : val := λ: "c",
sort_service "cmp" "c".
Definition sort_client_func : val := λ: "cmp" "xs",
let: "c" := start_chan sort_service_func in
let: "c" := fork_chan sort_service_func in
send "c" "cmp";; send "c" "xs";;
recv "c".
Section sort.
Context `{!heapG Σ, !proto_chanG Σ}.
Context `{!heapGS Σ, !chanG Σ}.
Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop)
`{!RelDecision R, !Total R} : iProto Σ :=
(<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
<?> (xs' : list A), MSG #() {{ ⌜ Sorted R xs' ⌝ ∗ ⌜ xs' ≡ₚ xs ⌝ ∗ llist I l xs' }};
Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop) : iProto Σ :=
(<! (xs : list A) (l : loc)> MSG #l {{ llist I l xs }};
<? (xs' : list A)> MSG #() {{ ⌜ Sorted R xs' ⌝ ∗ ⌜ xs' ≡ₚ xs ⌝ ∗ llist I l xs' }};
END)%proto.
Definition sort_protocol_func : iProto Σ :=
(<!> A (I : A → val → iProp Σ) (R : A → A → Prop)
`{!RelDecision R, !Total R} (cmp : val),
(<! A (I : A → val → iProp Σ) (R : A → A → Prop)
`(!RelDecision R, !Total R) (cmp : val)>
MSG cmp {{ cmp_spec I R cmp }};
sort_protocol I R)%proto.
......@@ -63,29 +64,29 @@ Section sort.
Proof.
iIntros "#Hcmp" (Ψ) "!> [Hl1 Hl2] HΨ".
iLöb as "IH" forall (l2 xs1 xs2 Ψ).
wp_lam. wp_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
wp_lam. wp_smart_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
destruct xs1 as [|x1 xs1]; wp_pures.
{ wp_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
{ wp_smart_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
iApply "HΨ". iFrame. by rewrite list_merge_nil_l. }
wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
wp_smart_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
destruct xs2 as [|x2 xs2]; wp_pures.
{ iApply "HΨ". iFrame. }
wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
{ iApply "HΨ". by iFrame. }
wp_smart_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
wp_smart_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
wp_smart_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
case_bool_decide; wp_pures.
- rewrite decide_True //.
wp_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
wp_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
wp_smart_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
wp_smart_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
{ iExists _, _. iFrame. }
iIntros "Hl1".
wp_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
wp_smart_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
- rewrite decide_False //.
wp_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
wp_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
wp_smart_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
wp_smart_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
{ iExists _, _. iFrame. }
iIntros "Hl1".
wp_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
wp_smart_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
Qed.
Lemma sort_service_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
......@@ -97,24 +98,24 @@ Section sort.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
wp_recv (xs l) as "Hl".
wp_apply (llength_spec with "Hl"); iIntros "Hl".
wp_smart_apply (llength_spec with "Hl"); iIntros "Hl".
wp_op; case_bool_decide as Hlen; wp_if.
{ assert (Sorted R xs).
{ destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
wp_smart_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
iDestruct 1 as (->) "[Hl1 Hl2]".
wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cy) "Hcy".
wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcy"); auto. }
wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cz) "Hcz".
wp_smart_apply ("IH" with "Hcy"); auto. }
wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcz"); auto. }
wp_smart_apply ("IH" with "Hcz"); auto. }
wp_send with "[$Hl1]".
wp_send with "[$Hl2]".
wp_recv (ys1) as (??) "Hl1".
wp_recv (ys2) as (??) "Hl2".
wp_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
wp_smart_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
wp_send ((list_merge R ys1 ys2)) with "[$Hl]".
- iSplit; iPureIntro.
+ by apply (Sorted_list_merge _).
......@@ -129,7 +130,7 @@ Section sort.
Proof.
iIntros (Ψ) "Hc HΨ". wp_lam.
wp_recv (A I R ?? cmp) as "#Hcmp".
by wp_apply (sort_service_spec with "Hcmp Hc").
by wp_smart_apply (sort_service_spec with "Hcmp Hc").
Qed.
Lemma sort_client_func_spec {A} (I : A → val → iProp Σ) R
......@@ -140,12 +141,12 @@ Section sort.
{{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_proto_spec sort_protocol_func); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec sort_protocol_func); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)).
wp_apply (sort_service_func_spec with "Hc"); auto. }
wp_send (A I R) with "[$Hcmp]".
wp_smart_apply (sort_service_func_spec with "Hc"); auto. }
wp_send with "[$Hcmp]".
wp_send with "[$Hl]".
wp_recv (ys) as "(Hsorted & Hperm & Hl)".
wp_pures. iApply "HΦ"; iFrame.
iApply "HΦ"; by iFrame.
Qed.
End sort.
theories/examples/sort_br_del.v → actris/examples/sort_br_del.v
View file @ c9249305
(** This file implements a looping distributed Merge Sort,
a specification thereof and its proofs. *)
(** This file provides three wrappers around the distributed version of merge
sort, demonstrating Actris's support for delegation and branching:
- [sort_service_br]: a service that allows one to sort a series of lists in
sequence.
- [sort_service_del]: a service that allows one to sort a series of lists in
parallel by delegating a sort service for a single list to a new channel.
- [sort_service_br_del]: a service that allows one to sort a series of list by
forking itself. *)
From stdpp Require Import sorting.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From actris.channel Require Import proofmode.
From actris.examples Require Import sort.
Definition sort_service_br : val :=
......@@ -14,7 +20,7 @@ Definition sort_service_br : val :=
Definition sort_service_del : val :=
rec: "go" "cmp" "c" :=
if: ~recv "c" then #() else
send "c" (start_chan (λ: "c", sort_service "cmp" "c"));;
send "c" (fork_chan (λ: "c", sort_service "cmp" "c"));;
"go" "cmp" "c".
Definition sort_service_br_del : val :=
......@@ -23,12 +29,12 @@ Definition sort_service_br_del : val :=
sort_service "cmp" "c";;
"go" "cmp" "c"
else if: recv "c" then
send "c" (start_chan (λ: "c", "go" "cmp" "c"));;
send "c" (fork_chan (λ: "c", "go" "cmp" "c"));;
"go" "cmp" "c"
else #().
Section sort_service_br_del.
Context `{!heapG Σ, !proto_chanG Σ}.
Context `{!heapGS Σ, !chanG Σ}.
Context {A} (I : A → val → iProp Σ) (R : A → A → Prop) `{!RelDecision R, !Total R}.
Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
......@@ -48,13 +54,13 @@ Section sort_service_br_del.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_apply ("IH" with "Hc"). }
{ wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_smart_apply ("IH" with "Hc"). }
by iApply "HΨ".
Qed.
Definition sort_protocol_del_aux (rec : iProto Σ) : iProto Σ :=
((<?> c, MSG c {{ c ↣ sort_protocol I R }}; rec) <+> END)%proto.
((<? c> MSG c {{ c ↣ sort_protocol I R }}; rec) <+> END)%proto.
Instance sort_protocol_del_aux_contractive : Contractive sort_protocol_del_aux.
Proof. solve_proto_contractive. Qed.
Definition sort_protocol_del : iProto Σ := fixpoint sort_protocol_del_aux.
......@@ -70,15 +76,14 @@ Section sort_service_br_del.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (start_chan_proto_spec (sort_protocol I R <++> END)%proto);
iIntros (c') "Hc'".
{ wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
wp_send with "[$Hc']". by wp_apply ("IH" with "Hc"). }
{ wp_smart_apply (fork_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
{ wp_pures. wp_smart_apply (sort_service_spec with "Hcmp Hc'"); auto. }
wp_send with "[$Hc']". by wp_smart_apply ("IH" with "Hc"). }
by iApply "HΨ".
Qed.
Definition sort_protocol_br_del_aux (rec : iProto Σ) : iProto Σ :=
((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec }}; rec) <+> END))%proto.
((sort_protocol I R <++> rec) <+> ((<? c> MSG c {{ c ↣ rec }}; rec) <+> END))%proto.
Instance sort_protocol_br_del_aux_contractive : Contractive sort_protocol_br_del_aux.
Proof. solve_proto_contractive. Qed.
Definition sort_protocol_br_del : iProto Σ := fixpoint sort_protocol_br_del_aux.
......@@ -94,13 +99,13 @@ Section sort_service_br_del.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_apply ("IH" with "Hc"). }
{ wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_smart_apply ("IH" with "Hc"). }
wp_branch; wp_pures.
{ wp_apply (start_chan_proto_spec sort_protocol_br_del); iIntros (c') "Hc'".
{ wp_apply ("IH" with "Hc'"); auto. }
{ wp_smart_apply (fork_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
{ wp_smart_apply ("IH" with "Hc'"); auto. }
wp_send with "[$Hc']".
by wp_apply ("IH" with "Hc"). }
by wp_smart_apply ("IH" with "Hc"). }
by iApply "HΨ".
Qed.
End sort_service_br_del.