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 (275)
175 additional commits have been omitted to prevent performance issues.
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 1565 additions and 873 deletions
.gitignore
View file @ 316a5108
......@@ -13,7 +13,7 @@
*.bak
.coqdeps.d
.coq-native/
build-dep/
builddep/
Makefile.coq
Makefile.coq.conf
.Makefile.coq.d
......
.gitlab-ci.yml
View file @ 316a5108
......@@ -5,6 +5,7 @@ stages:
variables:
CPU_CORES: "10"
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
.template: &template
stage: build
......@@ -16,10 +17,10 @@ variables:
cache:
key: "$CI_JOB_NAME"
paths:
- opamroot/
- _opam/
only:
- master
- /^ci/
- master@iris/actris
- /^ci/@iris/actris
except:
- triggers
- schedules
......@@ -27,16 +28,21 @@ variables:
## Build jobs
build-coq.8.12.0:
build-coq.8.20.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.0"
OPAM_PINS: "coq version 8.20.0"
DENY_WARNINGS: "1"
OPAM_PKG: "1"
tags:
- fp-timing
build-iris.dev:
trigger-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
STDPP_REPO: "iris/stdpp"
IRIS_REPO: "iris/iris"
OPAM_PINS: "coq version $NIGHTLY_COQ git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
except:
only:
- triggers
......
Makefile
View file @ 316a5108
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
# Default target
all: Makefile.coq
+@make -f Makefile.coq all
+@$(MAKE) -f Makefile.coq all
.PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@$(MAKE) -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache
+@$(MAKE) -f Makefile.coq clean
@# Make sure not to enter the `_opam` folder.
find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache builddep/*
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies
build-dep/opam: opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
OPAMFILES=$(wildcard *.opam)
BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
builddep/%-builddep.opam: %.opam Makefile
@echo "# Creating builddep package for $<."
@mkdir -p builddep
@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
builddep-opamfiles: $(BUILDDEPFILES)
.PHONY: builddep-opamfiles
builddep: builddep-opamfiles
@# We want opam to not just install the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Installing build-dep package."
@opam install $(OPAMFLAGS) build-dep/
@echo "# Installing builddep packages."
@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
.PHONY: builddep
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
opam: ;
# Backwards compatibility target
build-dep: builddep
.PHONY: build-dep
# Phony wildcard targets
phony: ;
.PHONY: phony
# Some files that do *not* need to be forwarded to Makefile.coq.
# ("::" lets Makefile.local overwrite this.)
Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
README.md
View file @ 316a5108
# ACTRIS COQ DEVELOPMENT
This directory contains the Coq mechanization of the Actris framework,
first presented in the paper
This repository contains:
- The Coq mechanization of the Actris framework, first presented in the paper
[Actris: Session Type Based Reasoning in Separation Logic](https://iris-project.org/pdfs/2020-popl-actris-final.pdf)
at POPL'20.
at POPL'20
- The logical relations model for a semantic session type system, first presented in
the paper
[Machine-Checked Semantic Session Typing](https://iris-project.org/pdfs/2021-cpp-sessions-final.pdf)
It has been built and tested with the following dependencies
- Coq 8.12.0
- Coq 8.18.0
- The version of Iris in the [opam file](opam)
In order to build, install the above dependencies and then run
......@@ -34,11 +37,11 @@ The individual types contain the following:
bidirectional channels in terms of Iris's HeapLang language, with specifications
defined in terms of the dependent separation protocols.
The relevant definitions and proof rules are as follows:
+ `iProto_mapsto`: endpoint ownership (notation `↣`).
+ `iProto_pointsto`: endpoint ownership (notation `↣`).
+ `new_chan_spec`, `send_spec` and `recv_spec`: proof rule for `new_chan`,
`send`, and `recv`.
`send`, and `recv`.
+ `select_spec` and `branch_spec`: proof rule for the derived (binary)
`select` and `branch` operations.
`select` and `branch` operations.
## Notation
......@@ -57,16 +60,19 @@ Dependent Separation Protocols:
| Append | `prot_1 · prot_2` | `prot_1 <++> prot_2` |
| Dual | An overlined protocol | No notation |
This notation is additionally used for the LMCS submission.
Semantic Session Types:
| | 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 |
| | 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
......@@ -139,9 +145,9 @@ The logical relation is defined across the following files:
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/environments.v](theories/logrel/environments.v):
Definition of the semantic type environment, which is used in the semantic
typing relation. This also contains the rules for updating the environment,
- [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):
......@@ -150,20 +156,31 @@ The logical relation is defined across the following files:
- [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/subtyping_rules.v](theories/logrel/subtyping_rules.v):
Subtyping rules for term types and session types.
- [theories/logrel/napp.v](theories/logrel/napp.v):
Definition of session types iteratively being appended to themselves a finite
number of times, with support for swapping e.g. a send over an arbitrary number
of receives.
An extension to the basic type system is given in
[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), which defines
mutexes as a type-safe abstraction. Mutexes are implemented using spin locks
and allow one to gain exclusive ownership of resources shared between multiple
threads.
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 CPP21 submission, see
[papers/CPP21.md](papers/CPP21.md).
For remarks about the paper-specific submissions, see
- [papers/POPL20.md](papers/POPL20.md)
- [papers/CPP21.md](papers/CPP21.md)
- [papers/LMCS.md](papers/LMCS.md)
_CoqProject
View file @ 316a5108
-Q theories actris
-Q actris actris
-Q multris multris
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-incompatible-prefix
# No common logical root, so we have to specify documentation root, to avoid warnings
-docroot actris
theories/utils/skip.v
theories/utils/llist.v
theories/utils/compare.v
theories/utils/contribution.v
theories/utils/group.v
theories/utils/cofe_solver_2.v
theories/utils/switch.v
theories/channel/proto_model.v
theories/channel/proto.v
theories/channel/channel.v
theories/channel/proofmode.v
theories/examples/basics.v
theories/examples/sort.v
theories/examples/sort_br_del.v
theories/examples/sort_fg.v
theories/examples/map.v
theories/examples/map_reduce.v
theories/examples/swap_mapper.v
theories/examples/subprotocols.v
theories/examples/list_rev.v
theories/logrel/model.v
theories/logrel/telescopes.v
theories/logrel/subtyping.v
theories/logrel/environments.v
theories/logrel/term_types.v
theories/logrel/session_types.v
theories/logrel/operators.v
theories/logrel/term_typing_judgment.v
theories/logrel/subtyping_rules.v
theories/logrel/term_typing_rules.v
theories/logrel/session_typing_rules.v
theories/logrel/napp.v
theories/logrel/lib/mutex.v
theories/logrel/lib/par_start.v
theories/logrel/examples/pair.v
theories/logrel/examples/par_recv.v
theories/logrel/examples/rec_subtyping.v
theories/logrel/examples/choice_subtyping.v
theories/logrel/examples/mapper.v
theories/logrel/examples/mapper_list.v
theories/logrel/examples/compute_service.v
theories/logrel/examples/compute_client_list.v
\ No newline at end of file
actris/utils/llist.v
actris/utils/compare.v
actris/utils/contribution.v
actris/utils/group.v
actris/utils/cofe_solver_2.v
actris/utils/switch.v
actris/channel/proto_model.v
actris/channel/proto.v
actris/channel/channel.v
actris/channel/proofmode.v
actris/examples/basics.v
actris/examples/equivalence.v
actris/examples/sort.v
actris/examples/sort_br_del.v
actris/examples/sort_fg.v
actris/examples/par_map.v
actris/examples/map_reduce.v
actris/examples/swap_mapper.v
actris/examples/subprotocols.v
actris/examples/list_rev.v
actris/examples/rpc.v
actris/examples/pizza.v
actris/logrel/model.v
actris/logrel/telescopes.v
actris/logrel/subtyping.v
actris/logrel/contexts.v
actris/logrel/term_types.v
actris/logrel/session_types.v
actris/logrel/operators.v
actris/logrel/term_typing_judgment.v
actris/logrel/subtyping_rules.v
actris/logrel/term_typing_rules.v
actris/logrel/session_typing_rules.v
actris/logrel/napp.v
actris/logrel/lib/mutex.v
actris/logrel/lib/list.v
actris/logrel/lib/par_start.v
actris/logrel/examples/pair.v
actris/logrel/examples/par_recv.v
actris/logrel/examples/rec_subtyping.v
actris/logrel/examples/choice_subtyping.v
actris/logrel/examples/mapper.v
actris/logrel/examples/mapper_list.v
actris/logrel/examples/compute_service.v
actris/logrel/examples/compute_client_list.v
multris/utils/cofe_solver_2.v
multris/utils/matrix.v
multris/channel/proto_model.v
multris/channel/proto.v
multris/channel/channel.v
multris/channel/proofmode.v
multris/examples/basics.v
multris/examples/two_buyer.v
multris/examples/three_buyer.v
multris/examples/leader_election.v
theories/channel/channel.v → actris/channel/channel.v
View file @ 316a5108
......@@ -22,12 +22,14 @@ In this file we define the three message-passing connectives:
It is additionaly shown that the channel ownership [c ↣ prot] is closed under
the subprotocol relation [⊑] *)
From iris.heap_lang Require Export primitive_laws notation.
From iris.heap_lang Require Import proofmode.
From iris.heap_lang Require Export proofmode.
From iris.heap_lang.lib Require Import spin_lock.
From actris.channel Require Export proto.
From actris.utils Require Import llist skip.
From actris.utils Require Import llist.
Set Default Proof Using "Type".
Local Existing Instance spin_lock.
(** * The definition of the message-passing connectives *)
Definition new_chan : val :=
λ: <>,
......@@ -36,7 +38,7 @@ Definition new_chan : val :=
let: "lk" := newlock #() in
((("l","r"),"lk"), (("r","l"),"lk")).
Definition start_chan : val := λ: "f",
Definition fork_chan : val := λ: "f",
let: "cc" := new_chan #() in
Fork ("f" (Snd "cc"));; Fst "cc".
......@@ -47,7 +49,6 @@ Definition send : val :=
let: "r" := Snd (Fst "c") in
acquire "lk";;
lsnoc "l" "v";;
skipN (llength "r");; (* "Ghost" operation for later stripping *)
release "lk".
Definition try_recv : val :=
......@@ -67,59 +68,51 @@ Definition recv : val :=
(** * Setup of Iris's cameras *)
Class chanG Σ := {
chanG_lockG :> lockG Σ;
chanG_protoG :> protoG Σ val;
#[local] chanG_lockG :: lockG Σ;
#[local] chanG_protoG :: protoG Σ val;
}.
Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
Proof. solve_inG. Qed.
Record chan_name := ChanName {
chan_lock_name : gname;
chan_proto_name : proto_name;
}.
Instance chan_name_inhabited : Inhabited chan_name :=
populate (ChanName inhabitant inhabitant).
Instance chan_name_eq_dec : EqDecision chan_name.
Proof. solve_decision. Qed.
Instance chan_name_countable : Countable chan_name.
Proof.
refine (inj_countable (λ '(ChanName γl γr), (γl,γr))
(λ '(γl, γr), Some (ChanName γl γr)) _); by intros [].
Qed.
(** * Definition of the mapsto connective *)
(** * Definition of the pointsto connective *)
Notation iProto Σ := (iProto Σ val).
Notation iMsg Σ := (iMsg Σ val).
Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
Definition iProto_lock_inv `{!heapGS Σ, !chanG Σ}
(l r : loc) (γl γr : gname) : iProp Σ :=
∃ vsl vsr,
llist internal_eq l vsl ∗
llist internal_eq r vsr ∗
steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
iProto_ctx γl γr vsl vsr.
Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
∃ γ s (l r : loc) (lk : val),
⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
is_lock (chan_lock_name γ) lk (∃ vsl vsr,
llist internal_eq l vsl ∗
llist internal_eq r vsr ∗
iProto_ctx (chan_proto_name γ) vsl vsr) ∗
iProto_own (chan_proto_name γ) s p.
Definition iProto_mapsto_aux : seal (@iProto_mapsto_def). by eexists. Qed.
Definition iProto_mapsto := iProto_mapsto_aux.(unseal).
Definition iProto_mapsto_eq :
@iProto_mapsto = @iProto_mapsto_def := iProto_mapsto_aux.(seal_eq).
Arguments iProto_mapsto {_ _ _} _ _%proto.
Instance: Params (@iProto_mapsto) 4 := {}.
Notation "c ↣ p" := (iProto_mapsto c p)
∃ γl γr γlk (l r : loc) (lk : val),
⌜ c = ((#l, #r), lk)%V ⌝ ∗
is_lock γlk lk (iProto_lock_inv l r γl γr) ∗
iProto_own γl p.
Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
Definition iProto_pointsto_eq :
@iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
Arguments iProto_pointsto {_ _ _} _ _%_proto.
Global Instance: Params (@iProto_pointsto) 4 := {}.
Notation "c ↣ p" := (iProto_pointsto c p)
(at level 20, format "c ↣ p").
Instance iProto_mapsto_contractive `{!heapG Σ, !chanG Σ} c :
Contractive (iProto_mapsto c).
Proof. rewrite iProto_mapsto_eq. solve_contractive. Qed.
Global Instance iProto_pointsto_contractive `{!heapGS Σ, !chanG Σ} c :
Contractive (iProto_pointsto c).
Proof. rewrite iProto_pointsto_eq. solve_contractive. Qed.
Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
(p1 p2 : iProto Σ) : iProto Σ :=
(<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
Typeclasses Opaque iProto_choice.
Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
Instance: Params (@iProto_choice) 2 := {}.
Global Typeclasses Opaque iProto_choice.
Arguments iProto_choice {_} _ _%_I _%_I _%_proto _%_proto.
Global Instance: Params (@iProto_choice) 2 := {}.
Infix "<{ P1 }+{ P2 }>" := (iProto_choice Send P1 P2) (at level 85) : proto_scope.
Infix "<{ P1 }&{ P2 }>" := (iProto_choice Recv P1 P2) (at level 85) : proto_scope.
Infix "<+{ P2 }>" := (iProto_choice Send True P2) (at level 85) : proto_scope.
......@@ -130,19 +123,19 @@ Infix "<+>" := (iProto_choice Send True True) (at level 85) : proto_scope.
Infix "<&>" := (iProto_choice Recv True True) (at level 85) : proto_scope.
Section channel.
Context `{!heapG Σ, !chanG Σ}.
Context `{!heapGS Σ, !chanG Σ}.
Implicit Types p : iProto Σ.
Implicit Types TT : tele.
Global Instance iProto_mapsto_ne c : NonExpansive (iProto_mapsto c).
Proof. rewrite iProto_mapsto_eq. solve_proper. Qed.
Global Instance iProto_mapsto_proper c : Proper ((≡) ==> (≡)) (iProto_mapsto c).
Global Instance iProto_pointsto_ne c : NonExpansive (iProto_pointsto c).
Proof. rewrite iProto_pointsto_eq. solve_proper. Qed.
Global Instance iProto_pointsto_proper c : Proper ((≡) ==> (≡)) (iProto_pointsto c).
Proof. apply (ne_proper _). Qed.
Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
Proof.
rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
rewrite iProto_pointsto_eq. iDestruct 1 as (γl γr γlk l r lk ->) "[Hlk H]".
iIntros "Hle'". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
by iApply (iProto_own_le with "H").
Qed.
......@@ -157,6 +150,22 @@ Section channel.
Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_choice Σ a).
Proof. solve_proper. Qed.
Lemma iProto_choice_equiv a1 a2 (P11 P12 P21 P22 : iProp Σ)
(p11 p12 p21 p22 : iProto Σ) :
⌜a1 = a2⌝ -∗ ((P11 ≡ P12):iProp Σ) -∗ (P21 ≡ P22) -∗
▷ (p11 ≡ p12) -∗ ▷ (p21 ≡ p22) -∗
iProto_choice a1 P11 P21 p11 p21 ≡ iProto_choice a2 P12 P22 p12 p22.
Proof.
iIntros (->) "#HP1 #HP2 #Hp1 #Hp2".
rewrite /iProto_choice. iApply iProto_message_equiv; [ eauto | | ].
- iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
destruct b;
[ iRewrite -"HP1"; iFrame "H Hp1" | iRewrite -"HP2"; iFrame "H Hp2" ].
- iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
destruct b;
[ iRewrite "HP1"; iFrame "H Hp1" | iRewrite "HP2"; iFrame "H Hp2" ].
Qed.
Lemma iProto_dual_choice a P1 P2 p1 p2 :
iProto_dual (iProto_choice a P1 P2 p1 p2)
≡ iProto_choice (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
......@@ -182,35 +191,47 @@ Section channel.
iDestruct ("H" with "HP") as "[$ ?]"; by iModIntro.
Qed.
Lemma iProto_lock_inv_sym l r γl γr :
iProto_lock_inv l r γl γr ⊢ iProto_lock_inv r l γr γl.
Proof.
iIntros "(%vsl & %vsr & Hlistl & Hlistr & Hstepsl & Hstepsr & Hctx)".
iExists vsr, vsl. iFrame. by iApply iProto_ctx_sym.
Qed.
(** ** Specifications of [send] and [recv] *)
Lemma new_chan_spec p :
{{{ True }}}
new_chan #()
{{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
Proof.
iIntros (Φ _) "HΦ". wp_lam.
wp_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
wp_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
wp_apply (newlock_spec (∃ vsl vsr,
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 ∗
iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
{ iExists [], []. iFrame. }
steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
iProto_ctx γl γr vsl vsr) with "[Hl Hr Hctx]").
{ iExists [], []. iFrame "#∗". }
iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
set (γ := ChanName γlk γp). iSplitL "Hcl".
- rewrite iProto_mapsto_eq. iExists γ, Left, l, r, lk. by iFrame "Hcl #".
- rewrite iProto_mapsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
iSplitL "Hcl".
- rewrite iProto_pointsto_eq.
iExists γl, γr, γlk, l, r, lk. by iFrame "Hcl #".
- rewrite iProto_pointsto_eq.
iExists γr, γl, γlk, r, l, lk. iFrame "Hcr #".
iModIntro. iSplit; first done. iApply (is_lock_iff with "Hlk").
iIntros "!> !>". iSplit; iIntros; by iApply iProto_lock_inv_sym.
Qed.
Lemma start_chan_spec p Φ (f : val) :
Lemma fork_chan_spec p Φ (f : val) :
▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
▷ (∀ c, c ↣ p -∗ Φ c) -∗
WP start_chan f {{ Φ }}.
WP fork_chan f {{ Φ }}.
Proof.
iIntros "Hfork HΦ". wp_lam.
wp_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
wp_apply (wp_fork with "[Hfork Hc2]").
{ iNext. wp_apply ("Hfork" with "Hc2"). }
wp_smart_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
wp_smart_apply (wp_fork with "[Hfork Hc2]").
{ iNext. wp_smart_apply ("Hfork" with "Hc2"). }
wp_pures. iApply ("HΦ" with "Hc1").
Qed.
......@@ -219,24 +240,46 @@ Section channel.
send c v
{{{ RET #(); c ↣ p }}}.
Proof.
rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
- iMod (iProto_send_l with "Hctx H []") as "[Hctx H]".
rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (γl γr γlk l r lk ->) "[#Hlk H]"; wp_pures.
wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
wp_pures. wp_bind (lsnoc _ _).
iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
{ iApply fupd_mask_intro; [set_solver|]. simpl.
iIntros "Hclose !>!>".
iMod (iProto_send with "Hctx H []") as "[Hctx H]".
{ rewrite iMsg_base_eq /=; auto. }
wp_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
wp_apply (llength_spec with "[$Hr //]"); iIntros "Hr".
wp_apply skipN_spec.
wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
- iMod (iProto_send_r with "Hctx H []") as "[Hctx H]".
{ rewrite iMsg_base_eq /=; auto. }
wp_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
wp_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
wp_apply skipN_spec.
wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
iModIntro.
iApply step_fupdN_intro; [done|].
iIntros "!>". iMod "Hclose".
iCombine ("Hctx H") as "H".
iExact "H". }
iApply (wp_lb_update with "Hlbl").
wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
iIntros "#Hlbl' [Hctx H] !>".
wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
{ iExists (vsl ++ [v]), vsr.
rewrite length_app /=.
replace (length vsl + 1) with (S (length vsl)) by lia.
iFrame "#∗". }
iIntros "_". iApply "HΦ". iExists γl, γr, γlk. eauto 10 with iFrame.
Qed.
Lemma send_spec_tele {TT} c (tt : TT)
(v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
{{{ c ↣ (<!.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
send c (v tt)
{{{ RET #(); c ↣ (p tt) }}}.
Proof.
iIntros (Φ) "[Hc HP] HΦ".
iDestruct (iProto_pointsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
as "Hc".
{ iIntros "!>".
iApply iProto_le_trans.
iApply iProto_le_texist_intro_l.
by iFrame "HP". }
by iApply (send_spec with "Hc").
Qed.
Lemma try_recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
......@@ -245,37 +288,26 @@ Section channel.
{{{ w, RET w; (⌜w = NONEV⌝ ∗ c ↣ <?.. x> MSG v x {{ P x }}; p x) ∨
(∃.. x, ⌜w = SOMEV (v x)⌝ ∗ c ↣ p x ∗ P x) }}}.
Proof.
assert (∀ w lp (m : TT → iMsg Σ),
iMsg_car (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, iMsg_car (m x) w lp)) as iMsg_texist.
{ intros w lp m. clear v P p. rewrite /iMsg_texist iMsg_exist_eq.
induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH. }
rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
- wp_apply (lisnil_spec with "Hr"); iIntros "Hr".
destruct vsr as [|vr vsr]; wp_pures.
{ wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
rewrite iMsg_base_eq. iDestruct (iMsg_texist with "Hm") as (x <-) "[Hp HP]".
wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
by iRewrite "Hp".
- wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct vsl as [|vl vsl]; wp_pures.
{ wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
rewrite iMsg_base_eq. iDestruct (iMsg_texist with "Hm") as (x <-) "[Hp HP]".
wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (γl γr γlk l r lk ->) "[#Hlk H]"; wp_pures.
wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
destruct vsr as [|vr vsr]; wp_pures.
- wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
{ unfold iProto_lock_inv; by eauto with iFrame. }
iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
iExists γl, γr, γlk. eauto 10 with iFrame.
- wp_smart_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
iMod (iProto_recv with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
rewrite iMsg_base_eq.
iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
iDestruct (steps_lb_le _ (length vsr) with "Hlbr") as "#Hlbr'"; [lia|].
wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
{ unfold iProto_lock_inv; by eauto with iFrame. }
iIntros "_". wp_pures. iModIntro. iApply "HΦ".
iRight. iExists x. iSplit; [done|].
iFrame "HP". iExists γl, γr, γlk, l, r, lk. iSplit; [done|]. iFrame "Hlk".
by iRewrite "Hp".
Qed.
......@@ -285,9 +317,9 @@ Section channel.
{{{ x, RET v x; c ↣ p x ∗ P x }}}.
Proof.
iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
wp_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
wp_smart_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
{ wp_pures. by iApply ("IH" with "[$]"). }
iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". iFrame.
iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
Qed.
(** ** Specifications for choice *)
......@@ -298,7 +330,7 @@ Section channel.
Proof.
rewrite /iProto_choice. iIntros (Φ) "[Hc HP] HΦ".
iApply (send_spec with "[Hc HP] HΦ").
iApply (iProto_mapsto_le with "Hc").
iApply (iProto_pointsto_le with "Hc").
iIntros "!>". iExists b. by iFrame "HP".
Qed.
......@@ -311,7 +343,7 @@ Section channel.
iApply (recv_spec _ (tele_app _)
(tele_app (TT:=[tele _ : bool]) (λ b, if b then P1 else P2))%I
(tele_app _) with "[Hc]").
{ iApply (iProto_mapsto_le with "Hc").
{ iApply (iProto_pointsto_le with "Hc").
iIntros "!> /=" (b) "HP". iExists b. by iSplitL. }
rewrite -bi_tforall_forall.
iIntros "!>" (x) "[Hc H]". iApply "HΦ". iFrame.
......
theories/channel/proto_model.v → actris/channel/proto_model.v
View file @ 316a5108
......@@ -34,29 +34,29 @@ The defined functions on the type [proto] are:
- [proto_app], which appends two protocols [p1] and [p2], by substituting
all terminations [END] in [p1] with [p2]. *)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From actris.utils Require Import cofe_solver_2.
Set Default Proof Using "Type".
Module Export action.
Inductive action := Send | Recv.
Instance action_inhabited : Inhabited action := populate Send.
Global Instance action_inhabited : Inhabited action := populate Send.
Definition action_dual (a : action) : action :=
match a with Send => Recv | Recv => Send end.
Instance action_dual_involutive : Involutive (=) action_dual.
Global Instance action_dual_involutive : Involutive (=) action_dual.
Proof. by intros []. Qed.
Canonical Structure actionO := leibnizO action.
End action.
Definition proto_auxO (V : Type) (PROP : ofeT) (A : ofeT) : ofeT :=
Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe :=
optionO (prodO actionO (V -d> laterO A -n> PROP)).
Definition proto_auxOF (V : Type) (PROP : ofeT) : oFunctor :=
Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
optionOF (actionO * (V -d> ▶ ∙ -n> PROP)).
Definition proto_result (V : Type) := result_2 (proto_auxOF V).
Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
solution_2_car (proto_result V) PROPn _ PROP _.
Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
Global Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
Proof. apply _. Qed.
Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
ofe_iso (proto_auxO V PROP (proto V PROP PROPn)) (proto V PROPn PROP).
......@@ -80,11 +80,11 @@ Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
(m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
proto_fold (Some (a, m)).
Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
Global Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
Proper (pointwise_relation V (dist n) ==> dist n)
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
Global Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
Proper (pointwise_relation V (≡) ==> (≡))
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
......@@ -96,7 +96,7 @@ Proof.
- left. by rewrite -(proto_fold_unfold p) E.
- right. exists a, m. by rewrite /proto_message -E proto_fold_unfold.
Qed.
Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end.
Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
......@@ -123,14 +123,12 @@ Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe P
proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
is contractive *)
Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
(p : proto V PROPn PROP) : A :=
match proto_unfold p with None => x | Some (a, m) => f a m end.
Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f1 f2 : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n :
(∀ a m1 m2, (∀ v, m1 v ≡{n}≡ m2 v) → f1 a m1 ≡{n}≡ f2 a m2) →
p1 ≡{n}≡ p2 →
......@@ -142,7 +140,7 @@ Proof.
apply Hf. destruct n; by simpl.
Qed.
Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) :
proto_elim x f proto_end ≡ x.
Proof.
......@@ -150,12 +148,12 @@ Proof.
pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
Qed.
Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
`{Hf : ∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)} a m :
Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) a m :
(∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)) →
proto_elim x f (proto_message a m) ≡ f a m.
Proof.
rewrite /proto_elim /proto_message /=.
intros. rewrite /proto_elim /proto_message /=.
pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
(PROP:=PROP) (Some (a, m))) as Hfold.
destruct (proto_unfold (proto_fold (Some (a, m))))
......@@ -173,13 +171,13 @@ Next Obligation.
apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv.
Qed.
Instance proto_map_aux_contractive {V}
Global Instance proto_map_aux_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
Proof.
intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm.
f_equiv=> v p' /=. do 2 f_equiv; [done|].
apply Next_contractive; destruct n as [|n]=> //=.
apply Next_contractive; by dist_later_intro as n' Hn'.
Qed.
Definition proto_map_aux_2 {V}
......@@ -188,7 +186,7 @@ Definition proto_map_aux_2 {V}
(rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
proto V PROPn PROP -n> proto V PROPn' PROP' :=
proto_map_aux g (proto_map_aux gn rec).
Instance proto_map_aux_2_contractive {V}
Global Instance proto_map_aux_2_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
Contractive (proto_map_aux_2 (V:=V) gn g).
......@@ -211,8 +209,7 @@ Proof.
induction (lt_wf n) as [n _ IH]=>
PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
apply proto_map_aux_contractive; destruct n as [|n]; [done|]; simpl.
symmetry. apply: IH. lia.
apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
Qed.
Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
......@@ -224,7 +221,8 @@ Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'
≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
apply: proto_elim_message=> a' m1 m2 Hm; f_equiv; solve_proper.
rewrite ->proto_elim_message; [done|].
intros a' m1 m2 Hm. f_equiv; solve_proper.
Qed.
Lemma proto_map_ne {V}
......@@ -239,7 +237,7 @@ Proof.
destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
apply Next_contractive; destruct n as [|n]=> //=; auto using dist_S with lia.
apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_le with lia.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
......@@ -255,7 +253,7 @@ Proof.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
apply Next_contractive; destruct n as [|n]=> //=; auto.
apply Next_contractive; dist_later_intro as n' Hn'; auto.
Qed.
Lemma proto_map_compose {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
......@@ -270,7 +268,7 @@ Proof.
PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
do 3 f_equiv. apply Next_contractive; destruct n as [|n]=> //=; auto.
do 3 f_equiv. apply Next_contractive; dist_later_intro as n' Hn'; simpl; auto.
Qed.
Program Definition protoOF (V : Type) (Fn F : oFunctor)
......@@ -294,13 +292,14 @@ Next Obligation.
apply proto_map_ext=> //= y; by rewrite ofe.oFunctor_map_compose.
Qed.
Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
oFunctorContractive Fn → oFunctorContractive F →
oFunctorContractive (protoOF V Fn F).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
apply proto_map_ne=> //= y;
[destruct n; [|destruct Hfg]; by apply oFunctor_map_contractive..].
intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
apply proto_map_ne=> y //=.
+ apply HFn. dist_later_intro as n' Hn'. f_equiv; apply Hfg.
+ apply HF. by dist_later_intro as n' Hn'.
Qed.
theories/examples/basics.v → actris/examples/basics.v
View file @ 316a5108
......@@ -4,19 +4,21 @@ From actris.channel Require Import proofmode.
From iris.heap_lang Require Import lib.spin_lock.
From actris.utils Require Import contribution.
Local Existing Instance spin_lock.
(** Basic *)
Definition prog : val := λ: <>,
let: "c" := start_chan (λ: "c'", send "c'" #42) in
let: "c" := fork_chan (λ: "c'", send "c'" #42) in
recv "c".
(** Tranfering References *)
Definition prog_ref : val := λ: <>,
let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
let: "c" := fork_chan (λ: "c'", send "c'" (ref #42)) in
! (recv "c").
(** Delegation, i.e. transfering channels *)
Definition prog_del : val := λ: <>,
let: "c1" := start_chan (λ: "c1'",
let: "c1" := fork_chan (λ: "c1'",
let: "cc2" := new_chan #() in
send "c1'" (Fst "cc2");;
send (Snd "cc2") #42) in
......@@ -24,46 +26,43 @@ Definition prog_del : val := λ: <>,
(** Dependent protocols *)
Definition prog_dep : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
let: "x" := recv "c'" in send "c'" ("x" + #2)) in
send "c" #40;;
recv "c".
Definition prog_dep_ref : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
let: "l" := recv "c'" in "l" <- !"l" + #2;; send "c'" #()) in
let: "l" := ref #40 in send "c" "l";; recv "c";; !"l".
Definition prog_dep_del : val := λ: <>,
let: "c1" := start_chan (λ: "c1'",
let: "c1" := fork_chan (λ: "c1'",
let: "cc2" := new_chan #() in
send "c1'" (Fst "cc2");;
let: "x" := recv (Snd "cc2") in send (Snd "cc2") ("x" + #2)) in
let: "c2'" := recv "c1" in send "c2'" #40;; recv "c2'".
Definition prog_dep_del_2 : val := λ: <>,
let: "c1" := start_chan (λ: "c1'",
let: "c1" := fork_chan (λ: "c1'",
send (recv "c1'") #40;;
send "c1'" #()) in
let: "c2" := start_chan (λ: "c2'",
let: "c2" := fork_chan (λ: "c2'",
let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
send "c1" "c2";; recv "c1";; recv "c2".
Definition prog_dep_del_3 : val := λ: <>,
let: "c1" := start_chan (λ: "c1'",
let: "c1" := fork_chan (λ: "c1'",
let: "c" := recv "c1'" in let: "y" := recv "c1'" in
send "c" "y";; send "c1'" #()) in
let: "c2" := start_chan (λ: "c2'",
let: "c2" := fork_chan (λ: "c2'",
let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
send "c1" "c2";; send "c1" #40;; recv "c1";; recv "c2".
(** Loops *)
Definition prog_loop : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "go" :=
rec: "go" <> :=
let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" #() in
"go" #()) in
let: "c" := fork_chan (rec: "go" "c'" :=
let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
send "c" #18;;
let: "x1" := recv "c" in
send "c" #20;;
......@@ -72,7 +71,7 @@ Definition prog_loop : val := λ: <>,
(** Transfering higher-order functions *)
Definition prog_fun : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
let: "r" := ref #40 in
send "c" (λ: <>, !"r");;
......@@ -80,7 +79,7 @@ Definition prog_fun : val := λ: <>,
(** Lock protected channel endpoints *)
Definition prog_lock : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
let: "l" := newlock #() in
Fork (acquire "l";; send "c'" #21;; release "l");;
acquire "l";; send "c'" #21;; release "l") in
......@@ -88,15 +87,15 @@ Definition prog_lock : val := λ: <>,
(** Swapping of sends *)
Definition prog_swap : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
send "c'" #20;;
let: "y" := recv "c'" in
send "c'" "y") in
send "c" #22;;
send "c'" ("y" + #2)) in
send "c" #20;;
recv "c" + recv "c".
Definition prog_swap_twice : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
send "c'" #20;;
let: "y1" := recv "c'" in
let: "y2" := recv "c'" in
......@@ -105,11 +104,8 @@ Definition prog_swap_twice : val := λ: <>,
recv "c" + recv "c".
Definition prog_swap_loop : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "go" :=
rec: "go" <> :=
let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" #() in
"go" #()) in
let: "c" := fork_chan (rec: "go" "c'" :=
let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
send "c" #18;;
send "c" #20;;
let: "x1" := recv "c" in
......@@ -117,12 +113,9 @@ Definition prog_swap_loop : val := λ: <>,
"x1" + "x2".
Definition prog_ref_swap_loop : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "go" :=
rec: "go" <> :=
let: "l" := recv "c'" in
"l" <- !"l" + #2;; send "c'" #();; "go" #() in
"go" #()) in
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";;
......@@ -131,7 +124,7 @@ Definition prog_ref_swap_loop : val := λ: <>,
!"l1" + !"l2".
Section proofs.
Context `{heapG Σ, chanG Σ}.
Context `{heapGS Σ, chanG Σ}.
(** Protocols for the respective programs *)
Definition prot : iProto Σ :=
......@@ -198,7 +191,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
Definition prot_swap : iProto Σ :=
(<! (x : Z)> MSG #x;
<?> MSG #20;
<?> MSG #x; END)%proto.
<?> MSG #(x + 2); END)%proto.
Definition prot_swap_twice : iProto Σ :=
(<! (x : Z)> MSG #x;
......@@ -216,7 +209,7 @@ Definition prot_swap_loop : iProto Σ :=
Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot); iIntros (c) "Hc".
- by wp_send with "[]".
- wp_recv as "_". by iApply "HΦ".
Qed.
......@@ -224,7 +217,7 @@ Qed.
Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_ref); iIntros (c) "Hc".
- wp_alloc l as "Hl". by wp_send with "[$Hl]".
- wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
Qed.
......@@ -232,8 +225,8 @@ Qed.
Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_del); iIntros (c) "Hc".
- wp_apply (new_chan_spec prot with "[//]").
wp_smart_apply (fork_chan_spec prot_del); iIntros (c) "Hc".
- wp_smart_apply (new_chan_spec prot with "[//]").
iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
- wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.
......@@ -241,7 +234,7 @@ Qed.
Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c) "Hc".
- wp_recv (x) as "_". by wp_send with "[]".
- wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
Qed.
......@@ -249,7 +242,7 @@ Qed.
Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep_ref); iIntros (c) "Hc".
- wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
- wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
by iApply "HΦ".
......@@ -258,8 +251,8 @@ Qed.
Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
- wp_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
wp_smart_apply (fork_chan_spec prot_dep_del); iIntros (c) "Hc".
- wp_smart_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
- wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
by iApply "HΦ".
......@@ -268,9 +261,9 @@ Qed.
Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep_del_2); iIntros (c) "Hc".
{ wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
{ wp_recv (x) as "_". by wp_send with "[//]". }
wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.
......@@ -278,10 +271,10 @@ Qed.
Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep_del_3); iIntros (c) "Hc".
{ wp_recv (c2) as "Hc2". wp_recv (y) as "_".
wp_send with "[//]". by wp_send with "[$Hc2]". }
wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
{ wp_recv (x) as "_". by wp_send with "[//]". }
wp_send with "[$Hc2]". wp_send with "[//]".
wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
......@@ -290,10 +283,10 @@ Qed.
Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
- wp_pures. iLöb as "IH".
wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
- iLöb as "IH".
wp_recv (x) as "_". wp_send with "[//]".
wp_pures. by iApply "IH".
by wp_smart_apply "IH".
- wp_send with "[//]". wp_recv as "_". wp_send with "[//]". wp_recv as "_".
wp_pures. by iApply "HΦ".
Qed.
......@@ -301,14 +294,14 @@ Qed.
Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_fun); iIntros (c) "Hc".
- wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
iIntros "!>" (Ψ') "HP HΨ'". wp_apply ("Hf" with "HP"); iIntros (x) "HΨ".
iIntros "!>" (Ψ') "HP HΨ'". wp_smart_apply ("Hf" with "HP"); iIntros (x) "HΨ".
wp_pures. by iApply "HΨ'".
- wp_alloc l as "Hl".
wp_send ((l ↦ #40)%I (λ w, ⌜ w = 40%Z ⌝ ∗ l ↦ #40)%I) with "[]".
{ iIntros "!>" (Ψ') "Hl HΨ'". wp_load. iApply "HΨ'"; auto. }
wp_recv (vg) as "#Hg". wp_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
wp_recv (vg) as "#Hg". wp_smart_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
by iApply "HΦ".
Qed.
......@@ -316,33 +309,33 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
{{{ True }}} prog_lock #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec (prot_lock 2)); iIntros (c) "Hc".
- iMod contribution_init as (γ) "Hs".
iMod (alloc_client with "Hs") as "[Hs Hcl1]".
iMod (alloc_client with "Hs") as "[Hs Hcl2]".
wp_apply (newlock_spec (∃ n, server γ n ε ∗
wp_smart_apply (newlock_spec (∃ n, server γ n ε ∗
c ↣ iProto_dual (prot_lock n))%I
with "[Hc Hs]"); first by eauto with iFrame.
iIntros (lk γlk) "#Hlk".
iAssert (client γ ε -∗
WP acquire lk;; send c #21;; release lk {{ _, True }})%I with "[]" as "#Hhelp".
{ iIntros "Hcl".
wp_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
wp_smart_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
iDestruct "H" as (n) "[Hs Hc]".
iDestruct (server_agree with "Hs Hcl") as %[? _].
destruct n as [|n]=> //=. wp_send with "[//]".
iMod (dealloc_client with "Hs Hcl") as "Hs /=".
wp_apply (release_spec with "[$Hlk $Hl Hc Hs]"); eauto with iFrame. }
wp_apply (wp_fork with "[Hcl1]").
wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]"); eauto with iFrame. }
wp_smart_apply (wp_fork with "[Hcl1]").
{ iNext. by iApply "Hhelp". }
by wp_apply "Hhelp".
by wp_smart_apply "Hhelp".
- wp_recv as "_". wp_recv as "_". wp_pures. by iApply "HΦ".
Qed.
Lemma prog_swap_spec : {{{ True }}} prog_swap #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_swap); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_swap); iIntros (c) "Hc".
- wp_send with "[//]". wp_recv (x) as "_". by wp_send with "[//]".
- wp_send with "[//]". wp_recv as "_". wp_recv as "_".
wp_pures. by iApply "HΦ".
......@@ -351,7 +344,7 @@ Qed.
Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_swap_twice); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_swap_twice); iIntros (c) "Hc".
- wp_send with "[//]". wp_recv (x1) as "_". wp_recv (x2) as "_".
by wp_send with "[//]".
- wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
......@@ -361,26 +354,29 @@ Qed.
Lemma prog_swap_loop_spec : {{{ True }}} prog_swap_loop #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
- wp_pures. iLöb as "IH".
wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
- iLöb as "IH".
wp_recv (x) as "_". wp_send with "[//]".
wp_pures. by iApply "IH".
by wp_smart_apply "IH".
- wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
wp_pures. by iApply "HΦ".
Qed.
Lemma prog_ref_swap_loop_spec :
{{{ True }}} prog_ref_swap_loop #() {{{ RET #42; True }}}.
(** 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_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
- do 4 wp_pure _. iLöb as "IH". wp_lam.
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]".
do 2 wp_pure _. by iApply "IH".
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Φ".
wp_load. wp_load.
wp_pures. by iApply "HΦ".
Qed.
End proofs.
actris/examples/equivalence.v 0 → 100644
View file @ 316a5108
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.
theories/examples/list_rev.v → actris/examples/list_rev.v
View file @ 316a5108
From actris.channel Require Import proofmode proto channel.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From actris.utils Require Import llist.
Definition list_rev_service : val :=
......@@ -9,11 +9,11 @@ Definition list_rev_service : val :=
Definition list_rev_client : val :=
λ: "l",
let: "c" := start_chan list_rev_service in
let: "c" := fork_chan list_rev_service in
send "c" "l";; recv "c".
Section list_rev_example.
Context `{heapG Σ, chanG Σ}.
Context `{heapGS Σ, chanG Σ}.
Definition list_rev_prot : iProto Σ :=
(<! (l : loc) (vs : list val)> MSG #l {{ llist internal_eq l vs }} ;
......@@ -25,7 +25,7 @@ Section list_rev_example.
{{{ RET #(); c ↣ prot }}}.
Proof.
iIntros (Φ) "Hc HΦ".
wp_lam. wp_recv (l vs) as "Hl". wp_apply (lreverse_spec with "Hl").
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.
......@@ -39,8 +39,7 @@ Section list_rev_example.
+ iExists []. eauto.
+ iDestruct "Hl" as (v lcons) "[HIT [Hlcons Hrec]]".
iDestruct ("IH" with "Hrec") as (vs) "[Hvs H]".
iExists (v::vs). iFrame.
iExists v, lcons. eauto with iFrame.
iExists (v::vs). by iFrame.
- iDestruct 1 as (vs) "[Hvs HIT]".
iInduction xs as [|x xs] "IH" forall (l vs).
+ by iDestruct (big_sepL2_nil_inv_l with "HIT") as %->.
......@@ -62,8 +61,7 @@ Section list_rev_example.
iIntros (l xs) "Hl".
iDestruct (llist_split with "Hl") as (vs) "[Hl HIT]".
iExists l, vs. iFrame "Hl".
iModIntro.
iIntros "Hl".
iModIntro. iIntros "Hl".
iSplitL "Hl HIT".
{ iApply llist_split. rewrite big_sepL2_reverse_2.
iExists (reverse vs). iFrame "Hl HIT". }
......@@ -76,10 +74,10 @@ Section list_rev_example.
{{{ RET #(); llist IT l (reverse xs) }}}.
Proof.
iIntros (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
- rewrite -(iProto_app_end_r list_rev_prot).
iApply (list_rev_service_spec with "Hc"). eauto.
- iDestruct (iProto_mapsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".
- iDestruct (iProto_pointsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".
{ iApply list_rev_subprot. }
wp_send (l xs) with "[$Hl]". wp_recv as "Hl". by iApply "HΦ".
Qed.
......
theories/examples/map_reduce.v → actris/examples/map_reduce.v
View file @ 316a5108
......@@ -2,14 +2,14 @@
specification thereof, and its proofs. *)
From actris.channel Require Import proofmode.
From actris.utils Require Import llist compare contribution group.
From actris.examples Require Import map sort_fg.
From actris.examples Require Import par_map sort_fg.
From iris.algebra Require Import gmultiset.
(** * Functional version of map reduce (aka the specification) *)
Definition map_reduce {A B C} `{EqDecision K}
(map : A → list (K * B)) (red : K → list B → list C) : list A → list C :=
mbind (curry red) ∘ group ∘ mbind map.
Instance: Params (@map_reduce) 7 := {}.
mbind (uncurry red) ∘ group ∘ mbind map.
Global Instance: Params (@map_reduce) 7 := {}.
(** * Distributed version (aka the implementation) *)
Definition par_map_reduce_map : val :=
......@@ -60,11 +60,11 @@ Definition par_map_reduce_reduce : val :=
Definition cmpZfst : val := λ: "x" "y", Fst "x" ≤ Fst "y".
Definition par_map_reduce : val := λ: "n" "m" "map" "red" "xs",
let: "cmap" := start_chan (λ: "c", par_map_service "n" "map" "c") in
let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in
let: "cmap" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
let: "csort" := fork_chan (λ: "c", sort_service_fg cmpZfst "c") in
par_map_reduce_map "n" "cmap" "csort" "xs";;
send "csort" #stop;;
let: "cred" := start_chan (λ: "c", par_map_service "m" "red" "c") in
let: "cred" := fork_chan (λ: "c", par_map_service "m" "red" "c") in
(* We need the first sorted element in the loop to compare subsequent elements *)
if: ~recv "csort" then #() else (* Handle the empty case *)
let: "jy" := recv "csort" in
......@@ -76,7 +76,7 @@ Section map_reduce.
Context {A B C} `{EqDecision K} (map : A → list (K * B)) (red : K → list B → list C).
Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (curry red)).
Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (uncurry red)).
Proof.
induction 1 as [|[i1 xs1] [i2 xs2] ixss1 ixss2 [??]|[i1 xs1] [i2 xs2] ixss|];
simplify_eq/=; try done.
......@@ -90,13 +90,13 @@ End map_reduce.
(** * Correctness proofs of the distributed version *)
Class map_reduceG Σ A B `{Countable A, Countable B} := {
map_reduce_mapG :> mapG Σ A;
map_reduce_reduceG :> mapG Σ (Z * list B);
map_reduce_mapG :: mapG Σ A;
map_reduce_reduceG :: mapG Σ (Z * list B);
}.
Section mapper.
Context `{Countable A, Countable B} {C : Type}.
Context `{!heapG Σ, !chanG Σ, !map_reduceG Σ A B}.
Context `{!heapGS Σ, !chanG Σ, !map_reduceG Σ A B}.
Context (IA : A → val → iProp Σ) (IB : Z → B → val → iProp Σ) (IC : C → val → iProp Σ).
Context (map : A → list (Z * B)) (red : Z → list B → list C).
Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
......@@ -142,25 +142,25 @@ Section mapper.
case_bool_decide; wp_pures; simplify_eq/=.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []). rewrite right_id_L. auto with iFrame. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
- wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct xs as [|x xs]; csimpl; wp_pures.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
iApply ("IH" $! _ [] with "[%] Hl Hcmap Hcsort HΦ"); naive_solver.
+ wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+ wp_select. wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
wp_send with "[$HIx]".
wp_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
wp_smart_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
rewrite assoc_L -(comm _ [x]). iApply "HΦ".
- wp_recv (x k) as (Hx) "Hk".
rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)).
wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
wp_smart_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
rewrite right_id.
wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
wp_smart_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=.
rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm.
Qed.
......@@ -188,13 +188,13 @@ Section mapper.
Proof.
iIntros (acc accv Hys Hsort Hi Φ) "[Hl Hcsort] HΦ".
iLöb as "IH" forall (ys Hys Hsort Hi Φ); wp_rec; wp_pures; simpl.
wp_branch as %_|%Hperm; last first; wp_pures.
wp_branch as % _|%Hperm; last first; wp_pures.
{ iApply ("HΦ" $! [] None with "[Hl $Hcsort]"); simpl.
iEval (rewrite !right_id_L); auto with iFrame. }
wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L.
case_bool_decide as Hij; simplify_eq/=; wp_pures.
- wp_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
rewrite -reverse_snoc. wp_apply ("IH" $! (ys ++ [y])
- wp_smart_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
rewrite -reverse_snoc. wp_smart_apply ("IH" $! (ys ++ [y])
with "[%] [%] [//] Hl [Hcsort] [HΦ]"); try iClear "IH".
+ intros ?; discriminate_list.
+ rewrite fmap_app /= assoc_L. by apply Sorted_snoc.
......@@ -211,7 +211,7 @@ Section mapper.
inversion 1 as [|?? [? _]]; discriminate_list || simplify_list_eq.
assert (RZB (j',y') (i,y'')) as [??]; last (simpl in *; lia).
apply (Sorted_StronglySorted _) in Hsort.
eapply elem_of_StronglySorted_app; set_solver.
eapply StronglySorted_app; set_solver.
Qed.
Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred :
......@@ -224,12 +224,12 @@ Section mapper.
llist IC l zs ∗
csort ↣ from_option (λ _, sort_fg_tail_protocol IZB RZB iys
(iys_sorted ++ acc miy)) END%proto miy ∗
cred ↣ par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) ∗
cred ↣ par_map_protocol IZBs IC (uncurry red) n (Y : gmultiset (Z * list B)) ∗
from_option (λ '(i,y,w), IB i y w) True miy
}}}
par_map_reduce_reduce #n csort cred (accv miy) #l
{{{ zs', RET #();
⌜ (group iys_sorted ≫= curry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= curry red ⌝ ∗
⌜ (group iys_sorted ≫= uncurry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= uncurry red ⌝ ∗
llist IC l (zs' ++ zs)
}}}.
Proof.
......@@ -239,14 +239,14 @@ Section mapper.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! [] with "[$Hl]"); iPureIntro; simpl.
by rewrite gmultiset_elements_empty !right_id_L Hmiy. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- destruct miy as [[[i y] w]|]; simplify_eq/=; wp_pures; last first.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
iApply ("IH" $! _ _ None
with "[%] [%] [%] Hl Hcsort Hcred [] HΦ"); naive_solver.
+ wp_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
wp_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
wp_apply (par_map_reduce_collect_spec _ _ _ _ _ [_]
+ wp_smart_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
wp_smart_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
wp_smart_apply (par_map_reduce_collect_spec _ _ _ _ _ [_]
with "[$Hk $Hcsort]"); try done.
iIntros (ys' miy). iDestruct 1 as (? Hmiy') "(Hk & Hcsort & HImiy)"; csimpl.
wp_select; wp_pures. wp_send ((i, reverse (y :: ys'))) with "[Hk]".
......@@ -261,12 +261,12 @@ Section mapper.
rewrite !bind_app /= right_id_L -!assoc_L -(comm _ zs') !assoc_L.
apply (inj (.++ _)).
- wp_recv ([i ys] k) as (Hy) "Hk".
wp_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
wp_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
wp_smart_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
wp_smart_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
iApply ("HΦ" $! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L.
iPureIntro. rewrite (gmultiset_disj_union_difference {[ i,ys ]} Y)
-?gmultiset_elem_of_singleton_subseteq //.
iPureIntro. rewrite (gmultiset_disj_union_difference {[+ (i,ys) +]} Y)
?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
by rewrite right_id_L !assoc_L.
......@@ -275,34 +275,34 @@ Section mapper.
Lemma par_map_reduce_spec n m vmap vred l xs :
0 < n → 0 < m →
map_spec IA IZB map vmap -∗
map_spec IZBs IC (curry red) vred -∗
map_spec IZBs IC (uncurry red) vred -∗
{{{ llist IA l xs }}}
par_map_reduce #n #m vmap vred #l
{{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
Proof.
iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
wp_apply (start_chan_spec (par_map_protocol IA IZB map n ∅));
wp_smart_apply (fork_chan_spec (par_map_protocol IA IZB map n ∅));
iIntros (cmap) "// Hcmap".
{ wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
wp_apply (start_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
{ wp_pures. wp_smart_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
wp_smart_apply (fork_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
iIntros (csort) "Hcsort".
{ wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
{ wp_smart_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
iApply RZB_cmp_spec. }
rewrite right_id.
wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
wp_smart_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
wp_apply (start_chan_spec (par_map_protocol IZBs IC (curry red) m ∅));
wp_smart_apply (fork_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
iIntros (cred) "// Hcred".
{ wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
wp_branch as %_|%Hnil; last first.
{ wp_pures. wp_smart_apply (par_map_service_spec with "Hred Hcred"); auto. }
wp_branch as % _|%Hnil; last first.
{ wp_pures. iApply ("HΦ" $! [] with "[$Hl]"); simpl.
by rewrite /map_reduce /= -Hiys -Hnil. }
wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures.
wp_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
wp_smart_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
with "[$Hl $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
iIntros (zs). rewrite /= gmultiset_elements_empty !right_id.
iDestruct 1 as (Hzs) "Hk". wp_pures.
iDestruct 1 as (Hzs) "Hk".
iApply ("HΦ" with "[$Hk]"). by rewrite Hzs Hiys.
Qed.
End mapper.
theories/examples/map.v → actris/examples/par_map.v
View file @ 316a5108
......@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lib.spin_lock.
From actris.utils Require Import llist contribution.
From iris.algebra Require Import gmultiset.
Local Existing Instance spin_lock.
(** * Distributed version (aka the implementation) *)
Definition par_map_worker : val :=
rec: "go" "map" "l" "c" :=
......@@ -47,20 +49,20 @@ Definition par_map_client_loop : val :=
"go" "n" "c" "xs" "ys".
Definition par_map_client : val := λ: "n" "map" "xs",
let: "c" := start_chan (λ: "c", par_map_service "n" "map" "c") in
let: "c" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
let: "ys" := lnil #() in
par_map_client_loop "n" "c" "xs" "ys";;
lapp "xs" "ys".
(** * Correctness proofs of the distributed version *)
Class mapG Σ A `{Countable A} := {
map_contributionG :> contributionG Σ (gmultisetUR A);
map_lockG :> lockG Σ;
map_contributionG :: contributionG Σ (gmultisetUR A);
map_lockG :: lockG Σ;
}.
Section map.
Context `{Countable A} {B : Type}.
Context `{!heapG Σ, !chanG Σ, !mapG Σ A}.
Context `{!heapGS Σ, !chanG Σ, !mapG Σ A}.
Context (IA : A → val → iProp Σ) (IB : B → val → iProp Σ) (map : A → list B).
Local Open Scope nat_scope.
Implicit Types n : nat.
......@@ -72,12 +74,12 @@ Section map.
nat -d> gmultiset A -d> iProto Σ := λ i X,
let rec : nat → gmultiset A → iProto Σ := rec in
(if i is 0 then END else
((<! x v> MSG v {{ IA x v }}; rec i (X ⊎ {[ x ]}))
((<! x v> MSG v {{ IA x v }}; rec i (X ⊎ {[+ x +]}))
<+>
rec (pred i) X
) <{⌜ i ≠ 1 ∨ X = ∅ ⌝}&>
<? x (l : loc)> MSG #l {{ ⌜ x ∈ X ⌝ ∗ llist IB l (map x) }};
rec i (X ∖ {[ x ]}))%proto.
rec i (X ∖ {[+ x +]}))%proto.
Instance par_map_protocol_aux_contractive : Contractive par_map_protocol_aux.
Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
Definition par_map_protocol := fixpoint par_map_protocol_aux.
......@@ -96,7 +98,7 @@ Section map.
Proof.
iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH".
wp_rec; wp_pures.
wp_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
iDestruct "H" as (i X) "[Hs Hc]".
iDestruct (@server_agree with "Hs Hγ") as %[??]; destruct i as [|i]=>//=.
iAssert ⌜ S i ≠ 1 ∨ X = ∅ ⌝%I as %?.
......@@ -104,28 +106,27 @@ Section map.
iDestruct (@server_1_agree with "Hs Hγ") as %?%leibniz_equiv; auto. }
wp_select. wp_branch; wp_pures; last first.
{ iMod (@dealloc_client with "Hs Hγ") as "Hs /=".
wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
{ iExists i, _. iFrame. }
iIntros "_". by iApply "HΦ". }
wp_recv (x v) as "HI".
iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
{ apply (gmultiset_local_update_alloc _ _ {[ x ]}). }
{ apply (gmultiset_local_update_alloc _ _ {[+ x +]}). }
rewrite left_id_L.
wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
{ iExists (S i), _. iFrame. }
clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (l) "HI".
wp_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
clear dependent i X. iIntros "Hu". wp_smart_apply ("Hmap" with "HI"); iIntros (l) "HI".
wp_smart_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
iDestruct "H" as (i X) "[Hs Hc]".
iDestruct (@server_agree with "Hs Hγ")
as %[??%gmultiset_included]; destruct i as [|i]=>//=.
wp_select. wp_send with "[$HI]".
{ by rewrite gmultiset_elem_of_singleton_subseteq. }
wp_select. wp_send with "[$HI]"; first (iPureIntro; multiset_solver).
iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
{ by apply (gmultiset_local_update_dealloc _ _ {[ x ]}). }
{ by apply (gmultiset_local_update_dealloc _ _ {[+ x +]}). }
rewrite gmultiset_difference_diag.
wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
wp_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
{ iExists (S i), _. iFrame. }
iIntros "Hu". by wp_apply ("IH" with "[$] [$]").
iIntros "Hu". by wp_smart_apply ("IH" with "[$] [$]").
Qed.
Lemma par_map_workers_spec γl γ n vmap lk c :
......@@ -139,10 +140,10 @@ Section map.
iInduction n as [|n] "IH"; wp_rec; wp_pures; simpl.
{ by iApply "HΦ". }
iDestruct "Hγs" as "[Hγ Hγs]".
wp_apply (wp_fork with "[Hγ]").
{ iNext. wp_apply (par_map_worker_spec with "Hmap [$]"); auto. }
wp_smart_apply (wp_fork with "[Hγ]").
{ iNext. wp_smart_apply (par_map_worker_spec with "Hmap [$]"); auto. }
wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply ("IH" with "[$] [$]").
wp_smart_apply ("IH" with "[$] [$]").
Qed.
Lemma par_map_service_spec n vmap c :
......@@ -153,10 +154,10 @@ Section map.
Proof.
iIntros "#Hf !>"; iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iMod (contribution_init_pow (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
wp_apply (newlock_spec (map_worker_lock_inv γ c) with "[Hc Hs]").
wp_smart_apply (newlock_spec (map_worker_lock_inv γ c) with "[Hc Hs]").
{ iExists n, ∅. iFrame. }
iIntros (lk γl) "#Hlk".
wp_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
wp_smart_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
Qed.
Lemma par_map_client_loop_spec n c l k xs X ys :
......@@ -172,23 +173,23 @@ Section map.
case_bool_decide; wp_pures; simplify_eq/=.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []); simpl; auto with iFrame. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
- wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct xs as [|x xs]; csimpl; wp_pures.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
iApply ("IH" with "[%] Hl Hk Hc [$]"); naive_solver.
+ wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+ wp_select. wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
wp_send with "[$HIx]".
wp_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
wp_smart_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
rewrite assoc_L -(comm _ [x]). iApply "HΦ".
- wp_recv (x l') as (Hx) "Hl'".
wp_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
wp_apply ("IH" with "[] Hl Hk Hc"); first done.
wp_smart_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
wp_smart_apply ("IH" with "[] Hl Hk Hc"); first done.
iIntros (ys'); iDestruct 1 as (Hys) "Hk"; simplify_eq/=.
iApply ("HΦ" $! (ys' ++ map x)). iSplit.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
?gmultiset_singleton_subseteq_l //.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L.
+ by rewrite -assoc_L.
......@@ -202,12 +203,12 @@ Section map.
{{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
Proof.
iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
wp_apply (start_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
{ wp_apply (par_map_service_spec with "Hmap Hc"); auto. }
wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
wp_smart_apply (fork_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
{ wp_smart_apply (par_map_service_spec with "Hmap Hc"); auto. }
wp_pures. wp_smart_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
wp_smart_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
iIntros (ys) "(?&Hl&Hk)". rewrite /= gmultiset_elements_empty !right_id_L.
wp_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
wp_pures. iApply "HΦ"; auto.
wp_smart_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
iApply "HΦ"; auto.
Qed.
End map.
actris/examples/pizza.v 0 → 100644
View file @ 316a5108
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 @ 316a5108
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 @ 316a5108
......@@ -24,8 +24,8 @@ Definition sort_service : val :=
let: "xs" := recv "c" in
if: llength "xs" ≤ #1 then send "c" #() else
let: "zs" := lsplit "xs" in
let: "cy" := start_chan (λ: "c", "go" "cmp" "c") in
let: "cz" := start_chan (λ: "c", "go" "cmp" "c") in
let: "cy" := fork_chan (λ: "c", "go" "cmp" "c") in
let: "cz" := fork_chan (λ: "c", "go" "cmp" "c") in
send "cy" "xs";;
send "cz" "zs";;
recv "cy";; recv "cz";;
......@@ -37,12 +37,12 @@ Definition sort_service_func : val := λ: "c",
sort_service "cmp" "c".
Definition sort_client_func : val := λ: "cmp" "xs",
let: "c" := start_chan sort_service_func in
let: "c" := fork_chan sort_service_func in
send "c" "cmp";; send "c" "xs";;
recv "c".
Section sort.
Context `{!heapG Σ, !chanG Σ}.
Context `{!heapGS Σ, !chanG Σ}.
Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop) : iProto Σ :=
(<! (xs : list A) (l : loc)> MSG #l {{ llist I l xs }};
......@@ -64,29 +64,29 @@ Section sort.
Proof.
iIntros "#Hcmp" (Ψ) "!> [Hl1 Hl2] HΨ".
iLöb as "IH" forall (l2 xs1 xs2 Ψ).
wp_lam. wp_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
wp_lam. wp_smart_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
destruct xs1 as [|x1 xs1]; wp_pures.
{ wp_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
{ wp_smart_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
iApply "HΨ". iFrame. by rewrite list_merge_nil_l. }
wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
wp_smart_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
destruct xs2 as [|x2 xs2]; wp_pures.
{ iApply "HΨ". iFrame. }
wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
{ iApply "HΨ". by iFrame. }
wp_smart_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
wp_smart_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
wp_smart_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
case_bool_decide; wp_pures.
- rewrite decide_True //.
wp_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
wp_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
wp_smart_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
wp_smart_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
{ iExists _, _. iFrame. }
iIntros "Hl1".
wp_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
wp_smart_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
- rewrite decide_False //.
wp_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
wp_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
wp_smart_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
wp_smart_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
{ iExists _, _. iFrame. }
iIntros "Hl1".
wp_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
wp_smart_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
Qed.
Lemma sort_service_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
......@@ -98,24 +98,24 @@ Section sort.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
wp_recv (xs l) as "Hl".
wp_apply (llength_spec with "Hl"); iIntros "Hl".
wp_smart_apply (llength_spec with "Hl"); iIntros "Hl".
wp_op; case_bool_decide as Hlen; wp_if.
{ assert (Sorted R xs).
{ destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
wp_smart_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
iDestruct 1 as (->) "[Hl1 Hl2]".
wp_apply (start_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcy"); auto. }
wp_apply (start_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
wp_smart_apply ("IH" with "Hcy"); auto. }
wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcz"); auto. }
wp_smart_apply ("IH" with "Hcz"); auto. }
wp_send with "[$Hl1]".
wp_send with "[$Hl2]".
wp_recv (ys1) as (??) "Hl1".
wp_recv (ys2) as (??) "Hl2".
wp_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
wp_smart_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
wp_send ((list_merge R ys1 ys2)) with "[$Hl]".
- iSplit; iPureIntro.
+ by apply (Sorted_list_merge _).
......@@ -130,7 +130,7 @@ Section sort.
Proof.
iIntros (Ψ) "Hc HΨ". wp_lam.
wp_recv (A I R ?? cmp) as "#Hcmp".
by wp_apply (sort_service_spec with "Hcmp Hc").
by wp_smart_apply (sort_service_spec with "Hcmp Hc").
Qed.
Lemma sort_client_func_spec {A} (I : A → val → iProp Σ) R
......@@ -141,12 +141,12 @@ Section sort.
{{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_spec sort_protocol_func); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec sort_protocol_func); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)).
wp_apply (sort_service_func_spec with "Hc"); auto. }
wp_smart_apply (sort_service_func_spec with "Hc"); auto. }
wp_send with "[$Hcmp]".
wp_send with "[$Hl]".
wp_recv (ys) as "(Hsorted & Hperm & Hl)".
wp_pures. iApply "HΦ"; iFrame.
iApply "HΦ"; by iFrame.
Qed.
End sort.
theories/examples/sort_br_del.v → actris/examples/sort_br_del.v
View file @ 316a5108
......@@ -20,7 +20,7 @@ Definition sort_service_br : val :=
Definition sort_service_del : val :=
rec: "go" "cmp" "c" :=
if: ~recv "c" then #() else
send "c" (start_chan (λ: "c", sort_service "cmp" "c"));;
send "c" (fork_chan (λ: "c", sort_service "cmp" "c"));;
"go" "cmp" "c".
Definition sort_service_br_del : val :=
......@@ -29,12 +29,12 @@ Definition sort_service_br_del : val :=
sort_service "cmp" "c";;
"go" "cmp" "c"
else if: recv "c" then
send "c" (start_chan (λ: "c", "go" "cmp" "c"));;
send "c" (fork_chan (λ: "c", "go" "cmp" "c"));;
"go" "cmp" "c"
else #().
Section sort_service_br_del.
Context `{!heapG Σ, !chanG Σ}.
Context `{!heapGS Σ, !chanG Σ}.
Context {A} (I : A → val → iProp Σ) (R : A → A → Prop) `{!RelDecision R, !Total R}.
Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
......@@ -54,8 +54,8 @@ Section sort_service_br_del.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_apply ("IH" with "Hc"). }
{ wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_smart_apply ("IH" with "Hc"). }
by iApply "HΨ".
Qed.
......@@ -76,9 +76,9 @@ Section sort_service_br_del.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (start_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
{ wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
wp_send with "[$Hc']". by wp_apply ("IH" with "Hc"). }
{ wp_smart_apply (fork_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
{ wp_pures. wp_smart_apply (sort_service_spec with "Hcmp Hc'"); auto. }
wp_send with "[$Hc']". by wp_smart_apply ("IH" with "Hc"). }
by iApply "HΨ".
Qed.
......@@ -99,13 +99,13 @@ Section sort_service_br_del.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_apply ("IH" with "Hc"). }
{ wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_smart_apply ("IH" with "Hc"). }
wp_branch; wp_pures.
{ wp_apply (start_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
{ wp_apply ("IH" with "Hc'"); auto. }
{ wp_smart_apply (fork_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
{ wp_smart_apply ("IH" with "Hc'"); auto. }
wp_send with "[$Hc']".
by wp_apply ("IH" with "Hc"). }
by wp_smart_apply ("IH" with "Hc"). }
by iApply "HΨ".
Qed.
End sort_service_br_del.
theories/examples/sort_fg.v → actris/examples/sort_fg.v
View file @ 316a5108
......@@ -42,8 +42,8 @@ Definition sort_service_fg : val :=
let: "x" := recv "c" in
if: ~(recv "c") then send "c" #cont;; send "c" "x";; send "c" #stop else
let: "y" := recv "c" in
let: "c1" := start_chan (λ: "c", "go" "cmp" "c") in
let: "c2" := start_chan (λ: "c", "go" "cmp" "c") in
let: "c1" := fork_chan (λ: "c", "go" "cmp" "c") in
let: "c2" := fork_chan (λ: "c", "go" "cmp" "c") in
send "c1" #cont;; send "c1" "x";;
send "c2" #cont;; send "c2" "y";;
sort_service_fg_split "c" "c1" "c2";;
......@@ -66,13 +66,13 @@ Definition recv_all : val :=
"go" "c" "ys";; lcons "x" "ys".
Definition sort_client_fg : val := λ: "cmp" "xs",
let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
let: "c" := fork_chan (λ: "c", sort_service_fg "cmp" "c") in
send_all "c" "xs";;
send "c" #stop;;
recv_all "c" "xs".
Section sort_fg.
Context `{!heapG Σ, !chanG Σ}.
Context `{!heapGS Σ, !chanG Σ}.
Section sort_fg_inner.
Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
......@@ -126,7 +126,7 @@ Section sort_fg.
iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
wp_rec. wp_branch.
- wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
wp_apply ("IH" with "Hc Hc2 Hc1").
wp_smart_apply ("IH" with "Hc Hc2 Hc1").
iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
rewrite -!(assoc_L (++)).
iApply "HΨ". iFrame "Hc Hc1 Hc2". by rewrite Hxs' (comm (++) xs1') assoc_L.
......@@ -148,10 +148,10 @@ Section sort_fg.
Proof.
iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
wp_rec. wp_branch as %_ | %Hys'.
wp_rec. wp_branch as % _ | %Hys'.
- wp_recv (x v) as (Htl) "HI".
wp_select. wp_send with "[$HI]"; first by auto.
wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
wp_smart_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
* done.
* by rewrite Hys -!assoc_L (comm _ zs).
* auto using Sorted_snoc.
......@@ -159,7 +159,7 @@ Section sort_fg.
inversion 1; discriminate_list || simplify_list_eq. by constructor.
- wp_select with "[]".
{ by rewrite /= Hys Hxs Hys'. }
iApply "HΨ". iFrame.
iApply "HΨ". by iFrame.
Qed.
Lemma sort_service_fg_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
......@@ -181,12 +181,12 @@ Section sort_fg.
iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
wp_rec. wp_branch as %_ | %Hys2.
wp_rec. wp_branch as % _ | %Hys2.
- wp_recv (x v) as (Htl2) "HIx".
wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
wp_pures. wp_smart_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
case_bool_decide.
+ wp_select. wp_send with "[$HIy1 //]".
wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
wp_smart_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
* by rewrite comm.
* by rewrite assoc (comm _ ys2) Hys.
* by apply Sorted_snoc.
......@@ -195,14 +195,14 @@ Section sort_fg.
inversion 1; discriminate_list || simplify_list_eq. by constructor.
+ wp_select. wp_send with "[$HIx]".
{ iPureIntro. by apply Htl_le, total_not. }
wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
wp_smart_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
* by rewrite Hys assoc.
* by apply Sorted_snoc, Htl_le, total_not.
* constructor. by apply total_not.
* intros x'.
inversion 1; discriminate_list || simplify_list_eq. by constructor.
- wp_select. wp_send with "[$HIy1 //]".
wp_apply (sort_service_fg_forward_spec with "[$Hc $Hc1]").
wp_smart_apply (sort_service_fg_forward_spec with "[$Hc $Hc1]").
* done.
* by rewrite Hys Hys2 -!assoc_L (comm _ xs2).
* by apply Sorted_snoc.
......@@ -221,19 +221,19 @@ Section sort_fg.
wp_rec; wp_pures. wp_branch; wp_pures.
- wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
+ wp_recv (x2 v2) as "HIx2".
wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
{ iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
{ iIntros (cy) "Hcy". wp_smart_apply ("IH" with "Hcy"). auto. }
iIntros (cy) "Hcy".
wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
{ iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
{ iIntros (cz) "Hcz". wp_smart_apply ("IH" with "Hcz"); auto. }
iIntros (cz) "Hcz". rewrite !right_id.
wp_select. wp_send with "[$HIx1]".
wp_select. wp_send with "[$HIx2]".
wp_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
wp_smart_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
wp_branch as %_ | %[]%Permutation_nil_cons.
wp_branch as % _ | %[]%Permutation_nil_cons.
wp_recv (x v) as "[_ HIx]".
wp_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
wp_smart_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
by rewrite Hxs' Permutation_middle.
+ wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
......@@ -248,11 +248,11 @@ Section sort_fg.
Proof.
iIntros (Φ) "[Hl Hc] HΦ".
iInduction xs as [|x xs] "IH" forall (xs').
{ wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
iApply "HΦ". rewrite right_id_L. iFrame. }
wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
{ wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
iApply "HΦ". rewrite right_id_L. by iFrame. }
wp_lam. wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
wp_smart_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
wp_send with "[$HIx]". wp_smart_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
Qed.
Lemma recv_all_spec c p l xs ys' :
......@@ -265,11 +265,11 @@ Section sort_fg.
Proof.
iIntros (Hsort Φ) "[Hl Hc] HΦ".
iLöb as "IH" forall (xs ys' Φ Hsort).
wp_lam. wp_branch as %_ | %Hperm; wp_pures.
wp_lam. wp_branch as % _ | %Hperm; wp_pures.
- wp_recv (y v) as (Htl) "HIx".
wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
wp_smart_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl"; wp_pures.
wp_smart_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl".
iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto.
- iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
Qed.
......@@ -281,11 +281,11 @@ Section sort_fg.
{{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
{ wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
{ wp_smart_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
wp_smart_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
wp_select.
wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
wp_smart_apply (recv_all_spec with "[$Hl $Hc]"); auto.
iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
iApply "HΦ"; auto with iFrame.
Qed.
......@@ -305,6 +305,6 @@ Section sort_fg.
Proof.
iIntros (Ψ) "Hc HΨ". wp_lam.
wp_recv (A I R ? ? cmp) as "#Hcmp".
by wp_apply (sort_service_fg_spec with "Hcmp Hc").
by wp_smart_apply (sort_service_fg_spec with "Hcmp Hc").
Qed.
End sort_fg.
actris/examples/subprotocols.v 0 → 100644
View file @ 316a5108
From actris.channel Require Import proofmode proto channel.
From iris.proofmode Require Import proofmode.
Section subprotocol_basics.
Context `{heapGS Σ, chanG Σ}.
Lemma reference_example (l1' : loc) :
l1' ↦ #20 -∗
(<! (l1 l2 : loc)> MSG (#l1, #l2) {{ l1 ↦ #20 ∗ l2 ↦ #22 }}; END) ⊑
(<! (l2 : loc)> MSG (#l1', #l2) {{ l2 ↦ #22 }}; END).
Proof. iIntros "Hl1'" (l2) "Hl2". iExists l1', l2. by iFrame "Hl1' Hl2". Qed.
Lemma framing_example (P Q R : iProp Σ) (v w : val) :
⊢ ((<!> MSG v {{ P }} ; <?> MSG w {{ Q }}; END)%proto ⊑
(<!> MSG v {{ P ∗ R }} ; <?> MSG w {{ Q ∗ R }};END)%proto)%proto.
Proof.
iIntros "[HP HR]". iFrame "HP". iModIntro.
iIntros "HQ". iFrame "HQ HR". eauto.
Qed.
Definition prot1_aux (prot : iProto Σ) : iProto Σ :=
(<! (x:Z)> MSG #x ; <?> MSG #(x+2) ; prot)%proto.
Definition prot2_aux (prot : iProto Σ) : iProto Σ :=
(<! (x:Z)> MSG #x ; <! (y:Z)> MSG #y ;
<?> MSG #(x+2) ; <?> MSG #(y+2) ; prot)%proto.
Instance prot1_aux_contractive : Contractive prot1_aux.
Proof. solve_proto_contractive. Qed.
Instance prot2_aux_contractive : Contractive prot2_aux.
Proof. solve_proto_contractive. Qed.
Definition prot1 : iProto Σ := fixpoint prot1_aux.
Definition prot2 : iProto Σ := fixpoint prot2_aux.
Lemma nonstructural_recursion_example :
⊢ prot1 ⊑ prot2.
Proof.
iLöb as "IH".
iEval (rewrite /prot1 /prot2).
do 2 rewrite (fixpoint_unfold prot1_aux).
rewrite (fixpoint_unfold prot2_aux).
iIntros (x). iExists x. iModIntro.
iIntros (y).
iApply (iProto_le_trans).
{ iModIntro. iExists y. iApply iProto_le_refl. }
iApply iProto_le_trans; [ iApply iProto_le_base_swap | ].
iModIntro. iModIntro. iModIntro.
iApply "IH".
Qed.
Fixpoint is_list (v : val) (ws : list val) : iProp Σ :=
match ws with
| [] => True
| w::ws => ∃ (v' : val), ⌜v = PairV w v'⌝ ∗ is_list v' ws
end.
Fixpoint is_int_list (v : val) (xs : list Z) : iProp Σ :=
match xs with
| [] => True
| x::xs => ∃ (v' : val), ⌜v = PairV (LitV $ LitInt $ x) v'⌝ ∗ is_int_list v' xs
end.
Lemma is_list_int_list v xs :
is_int_list v xs -∗ ∃ (ws : list val), is_list v ws ∗
[∗ list] i↦x;w ∈ xs;ws, ⌜LitV $ LitInt $ x = w⌝%I.
Proof.
iIntros "H".
iInduction (xs) as [|x xs] "IH" forall (v).
{ iExists []; eauto. }
iDestruct "H" as (v' ->) "H".
iDestruct ("IH" with "H") as (ws) "[Hlist Heq]".
iExists (#x :: ws); simpl; eauto.
Qed.
Lemma list_length_example :
⊢ (<? (v:val) (xs : list Z)> MSG v {{ is_int_list v xs }} ;
<!> MSG #(length xs) ; END) ⊑
(<? (v:val) (ws : list val)> MSG v {{ is_list v ws }} ;
<!> MSG #(length ws) ; END).
Proof.
iIntros (v xs) "H".
iDestruct (is_list_int_list with "H") as (ws) "[H Hlen]".
iDestruct (big_sepL2_length with "Hlen") as %Hlen.
iExists v, ws. iFrame "H".
iModIntro. rewrite Hlen. eauto.
Qed.
End subprotocol_basics.