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 (206)
106 additional commits have been omitted to prevent performance issues.
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 779 additions and 654 deletions
.gitignore
View file @ c9249305
......@@ -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 @ c9249305
......@@ -5,6 +5,7 @@ stages:
variables:
CPU_CORES: "10"
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
.template: &template
stage: build
......@@ -18,8 +19,8 @@ variables:
paths:
- _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 8.13.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 coq-iris-heap-lang.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 @ c9249305
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
# Default target
all: Makefile.coq
+@make -f Makefile.coq all
+@$(MAKE) -f Makefile.coq all
.PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@$(MAKE) -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .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 @ c9249305
......@@ -10,7 +10,7 @@ the paper
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
......@@ -37,7 +37,7 @@ 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`.
+ `select_spec` and `branch_spec`: proof rule for the derived (binary)
......
_CoqProject
View file @ c9249305
-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
# Coq emits warnings when a custom entry is reimported, this is too noisy.
-arg -w -arg -custom-entry-overriden
# 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/equivalence.v
theories/examples/sort.v
theories/examples/sort_br_del.v
theories/examples/sort_fg.v
theories/examples/par_map.v
theories/examples/map_reduce.v
theories/examples/swap_mapper.v
theories/examples/subprotocols.v
theories/examples/list_rev.v
theories/examples/rpc.v
theories/logrel/model.v
theories/logrel/telescopes.v
theories/logrel/subtyping.v
theories/logrel/contexts.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/list.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
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 @ c9249305
......@@ -25,9 +25,11 @@ From iris.heap_lang Require Export primitive_laws notation.
From iris.heap_lang Require Export proofmode.
From iris.heap_lang.lib Require Import spin_lock.
From actris.channel Require Export proto.
From actris.utils Require Import llist skip.
From actris.utils Require Import llist.
Set Default Proof Using "Type".
Local Existing Instance spin_lock.
(** * The definition of the message-passing connectives *)
Definition new_chan : val :=
λ: <>,
......@@ -36,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.
......@@ -198,30 +191,42 @@ 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.
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 (γp) "(Hctx & Hcl & Hcr)".
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_smart_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
......@@ -235,24 +240,30 @@ 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.
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 & Hctx)". destruct s; simpl.
- iMod (iProto_send_l with "Hctx H []") as "[Hctx H]".
{ rewrite iMsg_base_eq /=; auto. }
wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
wp_smart_apply (llength_spec with "[$Hr //]"); iIntros "Hr".
wp_smart_apply skipN_spec.
wp_smart_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]".
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_smart_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
wp_smart_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
wp_smart_apply skipN_spec.
wp_smart_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)
......@@ -262,7 +273,7 @@ Section channel.
{{{ RET #(); c ↣ (p tt) }}}.
Proof.
iIntros (Φ) "[Hc HP] HΦ".
iDestruct (iProto_mapsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
iDestruct (iProto_pointsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
as "Hc".
{ iIntros "!>".
iApply iProto_le_trans.
......@@ -277,35 +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.
rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
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 & Hctx)". destruct s; simpl.
- 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]"); [by eauto with iFrame|].
iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
wp_smart_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_exist with "Hm") as (x <-) "[Hp HP]".
wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
by iRewrite "Hp".
- wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct vsl as [|vl vsl]; wp_pures.
{ wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
wp_smart_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
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]".
wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
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.
......@@ -328,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.
......@@ -341,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/proofmode.v → actris/channel/proofmode.v
View file @ c9249305
......@@ -24,19 +24,19 @@ Ltac solve_proto_contractive :=
(** * Normalization of protocols *)
Class ActionDualIf (d : bool) (a1 a2 : action) :=
dual_action_if : a2 = if d then action_dual a1 else a1.
Hint Mode ActionDualIf ! ! - : typeclass_instances.
Global Hint Mode ActionDualIf ! ! - : typeclass_instances.
Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
Instance action_dual_if_true_send : ActionDualIf true Send Recv := eq_refl.
Instance action_dual_if_true_recv : ActionDualIf true Recv Send := eq_refl.
Global Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
Global Instance action_dual_if_true_send : ActionDualIf true Send Recv := eq_refl.
Global Instance action_dual_if_true_recv : ActionDualIf true Recv Send := eq_refl.
Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
(pas : list (bool * iProto Σ)) (q : iProto Σ) :=
proto_normalize :
⊢ iProto_dual_if d p <++>
foldr (iProto_app ∘ curry iProto_dual_if) END%proto pas ⊑ q.
Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
Arguments ProtoNormalize {_} _ _%_proto _%_proto _%_proto.
Notation ProtoUnfold p1 p2 := (∀ d pas q,
ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
......@@ -45,11 +45,11 @@ Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
(pas : list (bool * iProto Σ)) (m2 : iMsg Σ) :=
msg_normalize a :
ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
Arguments MsgNormalize {_} _ _%_msg _%_msg _%_msg.
Section classes.
Context `{!chanG Σ, !heapG Σ}.
Context `{!chanG Σ, !heapGS Σ}.
Implicit Types TT : tele.
Implicit Types p : iProto Σ.
Implicit Types m : iMsg Σ.
......@@ -135,7 +135,7 @@ Section classes.
(∀.. x1, MsgTele (tele_app tm1 x1) tv2 tP2 (tele_app tp x1)) →
ProtoNormalize d (<a> m) pas (<!.. x2> MSG tele_app tv2 x2 {{ tele_app tP2 x2 }};
<?.. x1> MSG tele_app tv1 x1 {{ tele_app tP1 x1 }};
tele_app (tele_app tp x1) x2).
tele_app (tele_app tp x1) x2) | 1.
Proof.
rewrite /ActionDualIf /MsgNormalize /ProtoNormalize /MsgTele.
rewrite tforall_forall=> Ha Hm Hm' Hm''.
......@@ -164,27 +164,27 @@ Section classes.
(** Automatically perform normalization of protocols in the proof mode when
using [iAssumption] and [iFrame]. *)
Global Instance mapsto_proto_from_assumption q c p1 p2 :
Global Instance pointsto_proto_from_assumption q c p1 p2 :
ProtoNormalize false p1 [] p2 →
FromAssumption q (c ↣ p1) (c ↣ p2).
Proof.
rewrite /FromAssumption /ProtoNormalize /= right_id.
rewrite bi.intuitionistically_if_elim.
iIntros (?) "H". by iApply (iProto_mapsto_le with "H").
iIntros (?) "H". by iApply (iProto_pointsto_le with "H").
Qed.
Global Instance mapsto_proto_from_frame q c p1 p2 :
Global Instance pointsto_proto_from_frame q c p1 p2 :
ProtoNormalize false p1 [] p2 →
Frame q (c ↣ p1) (c ↣ p2) True.
Proof.
rewrite /Frame /ProtoNormalize /= right_id.
rewrite bi.intuitionistically_if_elim.
iIntros (?) "[H _]". by iApply (iProto_mapsto_le with "H").
iIntros (?) "[H _]". by iApply (iProto_pointsto_le with "H").
Qed.
End classes.
(** * Symbolic execution tactics *)
(* TODO: Maybe strip laters from other hypotheses in the future? *)
Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K c p m tv tP tP' tp Φ :
Lemma tac_wp_recv `{!chanG Σ, !heapGS Σ} {TT : tele} Δ i j K c p m tv tP tP' tp Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (<?> m) →
MsgTele m tv tP tp →
......@@ -198,25 +198,25 @@ Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K c p m tv tP tP' t
end) →
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /MsgTele /MaybeIntoLaterN /=.
rewrite envs_entails_unseal /ProtoNormalize /MsgTele /MaybeIntoLaterN /=.
rewrite !tforall_forall right_id.
intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl.
assert (c ↣ p ⊢ c ↣ <?.. x>
MSG tele_app tv x {{ ▷ tele_app tP' x }}; tele_app tp x) as ->.
{ iIntros "Hc". iApply (iProto_mapsto_le with "Hc"). iIntros "!>".
{ iIntros "Hc". iApply (iProto_pointsto_le with "Hc"). iIntros "!>".
iApply iProto_le_trans; [iApply Hp|rewrite Hm].
iApply iProto_le_texist_elim_l; iIntros (x).
iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ x)]; simpl.
iIntros "H". by iDestruct (HP with "H") as "$". }
rewrite -wp_bind. eapply bi.wand_apply;
[by eapply (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv].
[by eapply bi.wand_entails, (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
rewrite -bi.later_intro; apply bi.forall_intro=> x.
specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
Qed.
Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
let solve_mapsto _ :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
wp_pures;
......@@ -226,10 +226,10 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
|fail 1 "wp_recv: cannot find 'recv' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_recv: protocol not of the shape <?>"
|iSolveTC || fail 1 "wp_recv: cannot convert to telescope"
|iSolveTC
[solve_pointsto ()
|tc_solve || fail 1 "wp_recv: protocol not of the shape <?>"
|tc_solve || fail 1 "wp_recv: cannot convert to telescope"
|tc_solve
|pm_reduce; simpl; tac_intros;
tac Hnew;
wp_finish]
......@@ -241,39 +241,11 @@ Tactic Notation "wp_recv" "as" constr(pat) :=
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K c v p m tv tP tp Φ :
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as"
"(" ne_simple_intropattern_list(ys) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => _iDestructHyp H ys pat).
Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K c v p m tv tP tp Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (<!> m) →
MsgTele m tv tP tp →
......@@ -292,7 +264,7 @@ Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K c v p m tv t
end) →
envs_entails Δ (WP fill K (send c v) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /MsgTele /= right_id texist_exist.
rewrite envs_entails_unseal /ProtoNormalize /MsgTele /= right_id texist_exist.
intros ? Hp Hm [x HΦ]. rewrite envs_lookup_sound //; simpl.
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
......@@ -300,14 +272,14 @@ Proof.
destruct HΦ as (-> & -> & ->). rewrite right_id assoc.
assert (c ↣ p ⊢
c ↣ <!.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->.
{ iIntros "Hc". iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
{ iIntros "Hc". iApply (iProto_pointsto_le with "Hc"); iIntros "!>".
iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. }
eapply bi.wand_apply; [rewrite -wp_bind; by eapply send_spec_tele|].
eapply bi.wand_apply; [rewrite -wp_bind; by eapply bi.wand_entails, send_spec_tele|].
by rewrite -bi.later_intro.
Qed.
Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
let solve_mapsto _ :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
let solve_done d :=
......@@ -327,9 +299,9 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
|fail 1 "wp_send: cannot find 'send' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <!>"
|iSolveTC || fail 1 "wp_send: cannot convert to telescope"
[solve_pointsto ()
|tc_solve || fail 1 "wp_send: protocol not of the shape <!>"
|tc_solve || fail 1 "wp_send: cannot convert to telescope"
|pm_reduce; simpl; tac_exist;
repeat lazymatch goal with
| |- ∃ _, _ => eexists _
......@@ -347,33 +319,10 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
Tactic Notation "wp_send" "with" constr(pat) :=
wp_send_core (idtac) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) ")" "with" constr(pat) :=
wp_send_core (eexists x1) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) ")"
"with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
"with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4)
uconstr(x5) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) uconstr(x7) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6; eexists x7) with pat.
Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
uconstr(x5) uconstr(x6) uconstr(x7) uconstr(x8) ")" "with" constr(pat) :=
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6; eexists x7; eexists x8) with pat.
Lemma tac_wp_branch `{!chanG Σ, !heapG Σ} Δ i j K
Tactic Notation "wp_send" "(" ne_uconstr_list(xs) ")" "with" constr(pat) :=
wp_send_core (ltac1_list_iter ltac:(fun x => eexists x) xs) with pat.
Lemma tac_wp_branch `{!chanG Σ, !heapGS Σ} Δ i j K
c p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (p1 <{P1}&{P2}> p2) →
......@@ -386,17 +335,17 @@ Lemma tac_wp_branch `{!chanG Σ, !heapG Σ} Δ i j K
end) →
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_entails_unseal /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl.
rewrite (iProto_mapsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv].
rewrite (iProto_pointsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply bi.wand_entails, branch_spec|f_equiv; first done].
rewrite -bi.later_intro; apply bi.forall_intro=> b.
specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
Qed.
Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
let solve_mapsto _ :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
iAssumptionCore || fail "wp_branch: cannot find" c "↣ ? @ ?" in
wp_pures;
......@@ -406,8 +355,8 @@ Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_branch _ _ Hnew K))
|fail 1 "wp_branch: cannot find 'recv' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <&>"
[solve_pointsto ()
|tc_solve || fail 1 "wp_send: protocol not of the shape <&>"
|pm_reduce; intros []; [tac1 Hnew|tac2 Hnew]; wp_finish]
| _ => fail "wp_branch: not a 'wp'"
end.
......@@ -420,9 +369,9 @@ Tactic Notation "wp_branch" "as" constr(pat1) "|" "%" simple_intropattern(pat2)
wp_branch_core as (fun H => iDestructHyp H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" "%" simple_intropattern(pat2) :=
wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" := wp_branch as %_ | %_.
Tactic Notation "wp_branch" := wp_branch as % _ | % _.
Lemma tac_wp_select `{!chanG Σ, !heapG Σ} Δ neg i js K
Lemma tac_wp_select `{!chanG Σ, !heapGS Σ} Δ neg i js K
c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (p1 <{P1}+{P2}> p2) →
......@@ -439,11 +388,11 @@ Lemma tac_wp_select `{!chanG Σ, !heapG Σ} Δ neg i js K
end →
envs_entails Δ (WP fill K (send c #b) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_entails_unseal /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl.
rewrite (iProto_mapsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
rewrite -assoc; f_equiv.
rewrite (iProto_pointsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply bi.wand_entails, select_spec|].
rewrite -assoc; f_equiv; first done.
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
......@@ -451,7 +400,7 @@ Proof.
Qed.
Tactic Notation "wp_select" "with" constr(pat) :=
let solve_mapsto _ :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
iAssumptionCore || fail "wp_select: cannot find" c "↣ ? @ ?" in
let solve_done d :=
......@@ -471,8 +420,8 @@ Tactic Notation "wp_select" "with" constr(pat) :=
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_select _ neg _ Hs' K))
|fail 1 "wp_select: cannot find 'send' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_select: protocol not of the shape <+>"
[solve_pointsto ()
|tc_solve || fail 1 "wp_select: protocol not of the shape <+>"
|pm_reduce;
lazymatch goal with
| |- False => fail "wp_select:" Hs' "not fresh"
......@@ -484,3 +433,21 @@ Tactic Notation "wp_select" "with" constr(pat) :=
end.
Tactic Notation "wp_select" := wp_select with "[//]".
Tactic Notation "wp_new_chan" constr(prot) "as"
"(" simple_intropattern(c1) simple_intropattern(c2) ")" constr(pat) :=
wp_smart_apply (new_chan_spec prot); [done|];
iIntros (c1); iIntros (c2); iIntros pat.
Tactic Notation "wp_fork_chan" constr(prot) "as"
simple_intropattern(c1) constr(pat1) "and"
simple_intropattern(c2) constr(pat2) :=
wp_smart_apply (fork_chan_spec prot); [iIntros (c2); iIntros pat2|
iIntros (c1); iIntros pat1].
Tactic Notation "wp_fork_chan" constr(prot) "as"
simple_intropattern(c) constr(pat) :=
wp_fork_chan prot as c pat and c pat.
Tactic Notation "wp_fork_chan" constr(prot) :=
wp_fork_chan prot as ? "?".
theories/channel/proto_model.v → actris/channel/proto_model.v
View file @ c9249305
......@@ -34,16 +34,16 @@ 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.
......@@ -53,82 +53,93 @@ Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe :=
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 pre_proto_result (V : Type) := result_2 (proto_auxOF V).
Definition pre_proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
solution_2_car (pre_proto_result V) PROPn _ PROP _.
Global Instance pre_proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} :
Cofe (pre_proto V PROPn PROP).
Proof. apply _. Qed.
Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
solution_2_car (proto_result V) PROPn _ PROP _.
Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
proto_auxO V PROP (pre_proto V PROP PROPn).
Global Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} :
Cofe (proto V PROPn PROP).
Proof. apply _. Qed.
Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
ofe_iso (proto_auxO V PROP (proto V PROP PROPn)) (proto V PROPn PROP).
Proof. apply proto_result. Qed.
ofe_iso (proto V PROPn PROP) (pre_proto V PROPn PROP).
Proof. apply pre_proto_result. Qed.
Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
proto_auxO V PROP (proto V PROP PROPn) -n> proto V PROPn PROP := ofe_iso_1 proto_iso.
pre_proto V PROPn PROP -n> proto V PROPn PROP := ofe_iso_2 proto_iso.
Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
proto V PROPn PROP -n> proto_auxO V PROP (proto V PROP PROPn) := ofe_iso_2 proto_iso.
proto V PROPn PROP -n> pre_proto V PROPn PROP := ofe_iso_1 proto_iso.
Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
proto_fold (proto_unfold p) ≡ p.
Proof. apply (ofe_iso_12 proto_iso). Qed.
Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
(p : proto_auxO V PROP (proto V PROP PROPn)) :
proto_unfold (proto_fold p) ≡ p.
Proof. apply (ofe_iso_21 proto_iso). Qed.
Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP} (p : pre_proto V PROPn PROP) :
proto_unfold (proto_fold p) ≡ p.
Proof. apply (ofe_iso_12 proto_iso). Qed.
Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
proto_fold None.
None.
Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
(m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
proto_fold (Some (a, m)).
Some (a, λ v, m v ◎ laterO_map proto_fold).
Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
Global Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
Proper (pointwise_relation V (dist n) ==> dist n)
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
Proof.
intros c1 c2 Hc. rewrite /proto_message.
(repeat constructor)=> //= v. by f_equiv.
Qed.
Global Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
Proper (pointwise_relation V (≡) ==> (≡))
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
Proof.
intros c1 c2 Hc. rewrite /proto_message.
(repeat constructor)=> //= v. by f_equiv.
Qed.
Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
p ≡ proto_end ∨ ∃ a m, p ≡ proto_message a m.
Proof.
destruct (proto_unfold p) as [[a m]|] eqn:E; simpl in *; last first.
- left. by rewrite -(proto_fold_unfold p) E.
- right. exists a, m. by rewrite /proto_message -E proto_fold_unfold.
destruct p as [[a m]|]; [|by left].
right. exists a, (λ v, m v ◎ laterO_map proto_unfold).
rewrite /proto_message. do 2 f_equiv. intros v p; simpl. f_equiv.
rewrite -later_map_compose -{1}(later_map_id p).
apply later_map_ext=> p' /=. by rewrite proto_unfold_fold.
Qed.
Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end.
Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
Proof.
trans (proto_unfold (proto_message a1 m1) ≡ proto_unfold (proto_message a2 m2) : SPROP)%I.
{ iSplit.
- iIntros "Heq". by iRewrite "Heq".
- iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
iRewrite "Heq". by rewrite proto_fold_unfold. }
rewrite /proto_message !proto_unfold_fold option_equivI prod_equivI /=.
rewrite discrete_eq discrete_fun_equivI.
by setoid_rewrite ofe_morO_equivI.
rewrite /proto_message option_equivI prod_equivI /=.
rewrite discrete_eq discrete_fun_equivI. f_equiv; [done|]. f_equiv=> x.
rewrite ofe_morO_equivI /=. iSplit; iIntros "H %p //".
assert (p ≡ later_map proto_fold (later_map proto_unfold p)) as ->; last done.
rewrite -later_map_compose -{1}(later_map_id p).
apply later_map_ext=> p' /=. by rewrite proto_fold_unfold.
Qed.
Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{SPROP} False.
Proof.
trans (proto_unfold (proto_message a m) ≡ proto_unfold proto_end : SPROP)%I.
{ iIntros "Heq". by iRewrite "Heq". }
by rewrite /proto_message !proto_unfold_fold option_equivI.
Qed.
Proof. by rewrite option_equivI. Qed.
Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
is contractive *)
Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
(p : proto V PROPn PROP) : A :=
match proto_unfold p with None => x | Some (a, m) => f a m end.
match p with
| None => x
| Some (a, m) => f a (λ v, m v ◎ laterO_map proto_unfold)
end.
Global Arguments proto_elim : simpl never.
Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f1 f2 : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n :
......@@ -136,31 +147,22 @@ Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
p1 ≡{n}≡ p2 →
proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2.
Proof.
intros Hf Hp. rewrite /proto_elim.
apply (_ : NonExpansive proto_unfold) in Hp
as [[a1 m1] [a2 m2] [-> ?]|]; simplify_eq/=; [|done].
apply Hf. destruct n; by simpl.
intros Hf [[a1 m1] [a2 m2] [[=->] ?]|]; rewrite /proto_elim //=.
apply Hf=> v. by f_equiv.
Qed.
Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) :
proto_elim x f proto_end ≡ x.
Proof.
rewrite /proto_elim /proto_end.
pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
Qed.
Proof. done. Qed.
Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
`{Hf : ∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)} a m :
(x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) a m :
(∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)) →
proto_elim x f (proto_message a m) ≡ f a m.
Proof.
rewrite /proto_elim /proto_message /=.
pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
(PROP:=PROP) (Some (a, m))) as Hfold.
destruct (proto_unfold (proto_fold (Some (a, m))))
as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
by f_equiv=> v.
intros. rewrite /proto_elim /proto_message /=. f_equiv=> v p /=. f_equiv.
rewrite -later_map_compose -{2}(later_map_id p).
apply later_map_ext=> p' /=. by rewrite proto_fold_unfold.
Qed.
(** Functor *)
......@@ -173,13 +175,13 @@ Next Obligation.
apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv.
Qed.
Instance proto_map_aux_contractive {V}
Global Instance proto_map_aux_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
Proof.
intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm.
f_equiv=> v p' /=. do 2 f_equiv; [done|].
apply Next_contractive; destruct n as [|n]=> //=.
apply Next_contractive; by dist_later_intro as n' Hn'.
Qed.
Definition proto_map_aux_2 {V}
......@@ -188,7 +190,7 @@ Definition proto_map_aux_2 {V}
(rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
proto V PROPn PROP -n> proto V PROPn' PROP' :=
proto_map_aux g (proto_map_aux gn rec).
Instance proto_map_aux_2_contractive {V}
Global Instance proto_map_aux_2_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
Contractive (proto_map_aux_2 (V:=V) gn g).
......@@ -211,20 +213,20 @@ Proof.
induction (lt_wf n) as [n _ IH]=>
PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
apply proto_map_aux_contractive; destruct n as [|n]; [done|]; simpl.
symmetry. apply: IH. lia.
apply proto_map_aux_contractive; constructor=> n' ?. symmetry. by apply: IH.
Qed.
Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
proto_map (V:=V) gn g proto_end ≡ proto_end.
Proof. by rewrite proto_map_unfold /proto_map_aux /= proto_elim_end. Qed.
Proof. by rewrite proto_map_unfold /proto_map_aux. Qed.
Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
proto_map (V:=V) gn g (proto_message a m)
≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
apply: proto_elim_message=> a' m1 m2 Hm; f_equiv; solve_proper.
rewrite ->proto_elim_message; [done|].
intros a' m1 m2 Hm. f_equiv; solve_proper.
Qed.
Lemma proto_map_ne {V}
......@@ -239,7 +241,7 @@ Proof.
destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
apply Next_contractive; destruct n as [|n]=> //=; auto using dist_S with lia.
apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_lt.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
......@@ -255,7 +257,7 @@ Proof.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
apply Next_contractive; destruct n as [|n]=> //=; auto.
apply Next_contractive; dist_later_intro as n' Hn'; auto.
Qed.
Lemma proto_map_compose {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
......@@ -270,7 +272,7 @@ Proof.
PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
do 3 f_equiv. apply Next_contractive; destruct n as [|n]=> //=; auto.
do 3 f_equiv. apply Next_contractive; dist_later_intro as n' Hn'; simpl; auto.
Qed.
Program Definition protoOF (V : Type) (Fn F : oFunctor)
......@@ -294,13 +296,14 @@ Next Obligation.
apply proto_map_ext=> //= y; by rewrite ofe.oFunctor_map_compose.
Qed.
Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
oFunctorContractive Fn → oFunctorContractive F →
oFunctorContractive (protoOF V Fn F).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
apply proto_map_ne=> //= y;
[destruct n; [|destruct Hfg]; by apply oFunctor_map_contractive..].
intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
apply proto_map_ne=> y //=.
+ apply HFn. dist_later_intro as n' Hn'. f_equiv; apply Hfg.
+ apply HF. by dist_later_intro as n' Hn'.
Qed.
theories/examples/basics.v → actris/examples/basics.v
View file @ c9249305
......@@ -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,42 +26,42 @@ Definition prog_del : val := λ: <>,
(** Dependent protocols *)
Definition prog_dep : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
let: "x" := recv "c'" in send "c'" ("x" + #2)) in
send "c" #40;;
recv "c".
Definition prog_dep_ref : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
let: "l" := recv "c'" in "l" <- !"l" + #2;; send "c'" #()) in
let: "l" := ref #40 in send "c" "l";; recv "c";; !"l".
Definition prog_dep_del : val := λ: <>,
let: "c1" := start_chan (λ: "c1'",
let: "c1" := fork_chan (λ: "c1'",
let: "cc2" := new_chan #() in
send "c1'" (Fst "cc2");;
let: "x" := recv (Snd "cc2") in send (Snd "cc2") ("x" + #2)) in
let: "c2'" := recv "c1" in send "c2'" #40;; recv "c2'".
Definition prog_dep_del_2 : val := λ: <>,
let: "c1" := start_chan (λ: "c1'",
let: "c1" := fork_chan (λ: "c1'",
send (recv "c1'") #40;;
send "c1'" #()) in
let: "c2" := start_chan (λ: "c2'",
let: "c2" := fork_chan (λ: "c2'",
let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
send "c1" "c2";; recv "c1";; recv "c2".
Definition prog_dep_del_3 : val := λ: <>,
let: "c1" := start_chan (λ: "c1'",
let: "c1" := fork_chan (λ: "c1'",
let: "c" := recv "c1'" in let: "y" := recv "c1'" in
send "c" "y";; send "c1'" #()) in
let: "c2" := start_chan (λ: "c2'",
let: "c2" := fork_chan (λ: "c2'",
let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
send "c1" "c2";; send "c1" #40;; recv "c1";; recv "c2".
(** Loops *)
Definition prog_loop : val := λ: <>,
let: "c" := start_chan (rec: "go" "c'" :=
let: "c" := fork_chan (rec: "go" "c'" :=
let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
send "c" #18;;
let: "x1" := recv "c" in
......@@ -69,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");;
......@@ -77,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
......@@ -85,7 +87,7 @@ Definition prog_lock : val := λ: <>,
(** Swapping of sends *)
Definition prog_swap : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
send "c'" #20;;
let: "y" := recv "c'" in
send "c'" ("y" + #2)) in
......@@ -93,7 +95,7 @@ Definition prog_swap : val := λ: <>,
recv "c" + recv "c".
Definition prog_swap_twice : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "c" := fork_chan (λ: "c'",
send "c'" #20;;
let: "y1" := recv "c'" in
let: "y2" := recv "c'" in
......@@ -102,7 +104,7 @@ Definition prog_swap_twice : val := λ: <>,
recv "c" + recv "c".
Definition prog_swap_loop : val := λ: <>,
let: "c" := start_chan (rec: "go" "c'" :=
let: "c" := fork_chan (rec: "go" "c'" :=
let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
send "c" #18;;
send "c" #20;;
......@@ -111,7 +113,7 @@ Definition prog_swap_loop : val := λ: <>,
"x1" + "x2".
Definition prog_ref_swap_loop : val := λ: <>,
let: "c" := start_chan (rec: "go" "c'" :=
let: "c" := fork_chan (rec: "go" "c'" :=
let: "l" := recv "c'" in
"l" <- !"l" + #2;; send "c'" #();; "go" "c'") in
let: "l1" := ref #18 in
......@@ -122,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 Σ :=
......@@ -207,7 +209,7 @@ Definition prot_swap_loop : iProto Σ :=
Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot); iIntros (c) "Hc".
- by wp_send with "[]".
- wp_recv as "_". by iApply "HΦ".
Qed.
......@@ -215,7 +217,7 @@ Qed.
Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_ref); iIntros (c) "Hc".
- wp_alloc l as "Hl". by wp_send with "[$Hl]".
- wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
Qed.
......@@ -223,7 +225,7 @@ Qed.
Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_del); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_del); iIntros (c) "Hc".
- wp_smart_apply (new_chan_spec prot with "[//]").
iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
- wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
......@@ -232,7 +234,7 @@ Qed.
Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c) "Hc".
- wp_recv (x) as "_". by wp_send with "[]".
- wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
Qed.
......@@ -240,7 +242,7 @@ Qed.
Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep_ref); iIntros (c) "Hc".
- wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
- wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
by iApply "HΦ".
......@@ -249,7 +251,7 @@ Qed.
Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep_del); iIntros (c) "Hc".
- wp_smart_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
- wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
......@@ -259,9 +261,9 @@ Qed.
Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep_del_2); iIntros (c) "Hc".
{ wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
wp_smart_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
{ wp_recv (x) as "_". by wp_send with "[//]". }
wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.
......@@ -269,10 +271,10 @@ Qed.
Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_dep_del_3); iIntros (c) "Hc".
{ wp_recv (c2) as "Hc2". wp_recv (y) as "_".
wp_send with "[//]". by wp_send with "[$Hc2]". }
wp_smart_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
{ wp_recv (x) as "_". by wp_send with "[//]". }
wp_send with "[$Hc2]". wp_send with "[//]".
wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
......@@ -281,10 +283,10 @@ Qed.
Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
- iLöb as "IH".
wp_recv (x) as "_". wp_send with "[//]".
do 2 wp_pure _. 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.
......@@ -292,7 +294,7 @@ Qed.
Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_fun); iIntros (c) "Hc".
- wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
iIntros "!>" (Ψ') "HP HΨ'". wp_smart_apply ("Hf" with "HP"); iIntros (x) "HΨ".
wp_pures. by iApply "HΨ'".
......@@ -307,7 +309,7 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
{{{ True }}} prog_lock #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec (prot_lock 2)); iIntros (c) "Hc".
- iMod contribution_init as (γ) "Hs".
iMod (alloc_client with "Hs") as "[Hs Hcl1]".
iMod (alloc_client with "Hs") as "[Hs Hcl2]".
......@@ -333,7 +335,7 @@ Qed.
Lemma prog_swap_spec : {{{ True }}} prog_swap #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_swap); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_swap); iIntros (c) "Hc".
- wp_send with "[//]". wp_recv (x) as "_". by wp_send with "[//]".
- wp_send with "[//]". wp_recv as "_". wp_recv as "_".
wp_pures. by iApply "HΦ".
......@@ -342,7 +344,7 @@ Qed.
Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_swap_twice); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_swap_twice); iIntros (c) "Hc".
- wp_send with "[//]". wp_recv (x1) as "_". wp_recv (x2) as "_".
by wp_send with "[//]".
- wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
......@@ -352,10 +354,10 @@ Qed.
Lemma prog_swap_loop_spec : {{{ True }}} prog_swap_loop #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
- iLöb as "IH".
wp_recv (x) as "_". wp_send with "[//]".
do 2 wp_pure _. 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.
......@@ -366,10 +368,10 @@ Actris journal paper *)
Lemma prog_ref_swap_loop_spec : ∀ Φ, Φ #42 -∗ WP prog_ref_swap_loop #() {{ Φ }}.
Proof.
iIntros (Φ) "HΦ". wp_lam.
wp_smart_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec prot_ref_loop); iIntros (c) "Hc".
- iLöb as "IH". wp_lam.
wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
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".
......
theories/examples/equivalence.v → actris/examples/equivalence.v
View file @ c9249305
From actris.channel Require Import channel proofmode.
Section equivalence_examples.
Context `{heapG Σ, chanG Σ}.
Context `{heapGS Σ, chanG Σ}.
Lemma binder_swap_equivalence_example :
((<! (x y : Z)> MSG (#x,#y) ; END):iProto Σ)%proto ≡
......
theories/examples/list_rev.v → actris/examples/list_rev.v
View file @ c9249305
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 }} ;
......@@ -39,8 +39,7 @@ Section list_rev_example.
+ iExists []. eauto.
+ iDestruct "Hl" as (v lcons) "[HIT [Hlcons Hrec]]".
iDestruct ("IH" with "Hrec") as (vs) "[Hvs H]".
iExists (v::vs). iFrame.
iExists v, lcons. eauto with iFrame.
iExists (v::vs). by iFrame.
- iDestruct 1 as (vs) "[Hvs HIT]".
iInduction xs as [|x xs] "IH" forall (l vs).
+ by iDestruct (big_sepL2_nil_inv_l with "HIT") as %->.
......@@ -75,10 +74,10 @@ Section list_rev_example.
{{{ RET #(); llist IT l (reverse xs) }}}.
Proof.
iIntros (Φ) "Hl HΦ". wp_lam.
wp_smart_apply (start_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
- rewrite -(iProto_app_end_r list_rev_prot).
iApply (list_rev_service_spec with "Hc"). eauto.
- iDestruct (iProto_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 @ c9249305
......@@ -8,8 +8,8 @@ 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,7 +142,7 @@ Section mapper.
case_bool_decide; wp_pures; simplify_eq/=.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []). rewrite right_id_L. auto with iFrame. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct xs as [|x xs]; csimpl; wp_pures.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
......@@ -159,8 +159,8 @@ Section mapper.
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,7 +188,7 @@ Section mapper.
Proof.
iIntros (acc accv Hys Hsort Hi Φ) "[Hl Hcsort] HΦ".
iLöb as "IH" forall (ys Hys Hsort Hi Φ); wp_rec; wp_pures; simpl.
wp_branch as %_|%Hperm; last first; wp_pures.
wp_branch as % _|%Hperm; last first; wp_pures.
{ iApply ("HΦ" $! [] None with "[Hl $Hcsort]"); simpl.
iEval (rewrite !right_id_L); auto with iFrame. }
wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L.
......@@ -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,7 +239,7 @@ Section mapper.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! [] with "[$Hl]"); iPureIntro; simpl.
by rewrite gmultiset_elements_empty !right_id_L Hmiy. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- destruct miy as [[[i y] w]|]; simplify_eq/=; wp_pures; last first.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
iApply ("IH" $! _ _ None
......@@ -265,8 +265,8 @@ Section mapper.
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,16 +275,16 @@ 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_smart_apply (start_chan_spec (par_map_protocol IA IZB map n ∅));
wp_smart_apply (fork_chan_spec (par_map_protocol IA IZB map n ∅));
iIntros (cmap) "// Hcmap".
{ wp_pures. wp_smart_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
wp_smart_apply (start_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
wp_smart_apply (fork_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
iIntros (csort) "Hcsort".
{ wp_smart_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
iApply RZB_cmp_spec. }
......@@ -292,10 +292,10 @@ Section mapper.
wp_smart_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
wp_smart_apply (start_chan_spec (par_map_protocol IZBs IC (curry red) m ∅));
wp_smart_apply (fork_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
iIntros (cred) "// Hcred".
{ wp_pures. wp_smart_apply (par_map_service_spec with "Hred Hcred"); auto. }
wp_branch as %_|%Hnil; last first.
wp_branch as % _|%Hnil; last first.
{ wp_pures. iApply ("HΦ" $! [] with "[$Hl]"); simpl.
by rewrite /map_reduce /= -Hiys -Hnil. }
wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures.
......
theories/examples/par_map.v → actris/examples/par_map.v
View file @ c9249305
......@@ -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.
......@@ -109,7 +111,7 @@ Section map.
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_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
{ iExists (S i), _. iFrame. }
......@@ -118,10 +120,9 @@ Section map.
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_smart_apply (release_spec with "[$Hlk $Hl Hc Hs]").
{ iExists (S i), _. iFrame. }
......@@ -172,7 +173,7 @@ Section map.
case_bool_decide; wp_pures; simplify_eq/=.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []); simpl; auto with iFrame. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
destruct n as [|n]=> //=. wp_branch as %?|% _; wp_pures.
- wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct xs as [|x xs]; csimpl; wp_pures.
+ wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
......@@ -187,8 +188,8 @@ Section map.
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,7 +203,7 @@ Section map.
{{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
Proof.
iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
wp_smart_apply (start_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
wp_smart_apply (fork_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
{ wp_smart_apply (par_map_service_spec with "Hmap Hc"); auto. }
wp_pures. wp_smart_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
wp_smart_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
......
actris/examples/pizza.v 0 → 100644
View file @ c9249305
From iris.heap_lang Require Import lib.spin_lock lib.par.
From actris.utils Require Import llist.
From actris.channel Require Import proofmode.
From stdpp Require Import list.
Local Existing Instance spin_lock.
Inductive pizza :=
| Margherita
| Calzone.
Section example.
Context `{heapGS Σ, chanG Σ, spawnG Σ}.
Definition pizza_to_val (p : pizza) :=
match p with
| Margherita => #0
| Calzone => #1
end.
Fixpoint list_to_val {T} (f : T → val) (xs : list T) :=
match xs with
| [] => NONEV
| x::xs => SOMEV ((f x), (list_to_val f xs))%V
end.
Notation pizza_list_to_val := (list_to_val pizza_to_val).
Fixpoint is_list {T} (f : T → val) (v : val) (ws : list T) : iProp Σ :=
match ws with
| [] => ⌜v = NONEV⌝
| w::ws => ∃ (v' : val), ⌜v = SOMEV ((f w), v')%V⌝ ∗ is_list f v' ws
end.
Notation is_int_list := (is_list (λ v, LitV $ LitInt $ v)).
Notation is_pizza_list := (is_list pizza_to_val).
Lemma is_pizza_list_pizzas pizzas :
⊢ is_pizza_list (pizza_list_to_val pizzas) pizzas.
Proof. induction pizzas; [eauto | iExists _; eauto]. Qed.
Fixpoint int_list_sum (xs : list Z) : Z :=
match xs with
| [] => 0
| x::xs => x + int_list_sum xs
end.
Definition sum_list : val :=
rec: "go" "xs" :=
match: "xs" with
NONE => #0
| SOME "xs" => Fst "xs" + "go" (Snd "xs")
end.
Lemma sum_list_spec v xs :
{{{ is_int_list v xs }}}
sum_list v
{{{ RET #(int_list_sum xs); True }}}.
Proof.
unfold is_int_list.
iIntros (Φ) "Hxs HΦ".
iInduction xs as [|x xs] "IH" forall (v Φ).
- wp_rec. iDestruct "Hxs" as "->".
wp_pures. by iApply "HΦ".
- wp_rec. unfold is_int_list. simpl.
iDestruct "Hxs" as (v') "[-> Hrec]".
wp_pures.
wp_apply ("IH" with "Hrec").
iIntros "_". wp_pures.
by iApply "HΦ".
Qed.
Definition order_pizza (pizzas : list pizza) : val :=
λ: "cc" "c",
send "c" (pizza_list_to_val pizzas);;
send "c" "cc";;
let: "receipt" := recv "c" in
(sum_list "receipt", !"cc").
Definition pizza_prot_aux (rec : iProto Σ) : iProto Σ :=
(<! (v1 : val) (xs1 : list pizza)> MSG v1 {{ is_pizza_list v1 xs1 }} ;
<! (l : loc) (x : Z)> MSG #l {{ l ↦ #x }};
<? (v2 : val) (xs2 : list Z)> MSG v2 {{ is_int_list v2 xs2 ∗
⌜Zlength xs1 = Zlength xs2⌝ ∗
l ↦ #(x - int_list_sum xs2)%Z }};
rec)%proto.
Instance pizza_prot_aux_contractive : Contractive pizza_prot_aux.
Proof. solve_proto_contractive. Qed.
Definition pizza_prot := fixpoint pizza_prot_aux.
Global Instance pizza_prot_unfold :
ProtoUnfold pizza_prot (pizza_prot_aux pizza_prot).
Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
Lemma order_pizza_spec pizzas c cc (x1 : Z) :
{{{ c ↣ pizza_prot ∗ cc ↦ #x1 }}}
order_pizza pizzas #cc c
{{{ (x2 : Z), RET (#x2, #(x1 - x2))%V;
c ↣ pizza_prot ∗ cc ↦ #(x1 - x2)%Z }}}.
Proof.
iIntros (Φ) "[Hc Hcc] HΦ".
wp_lam.
wp_send (_ pizzas) with "[]".
{ iApply is_pizza_list_pizzas. }
wp_send with "[Hcc //]".
wp_recv (v2 xs2) as "[Hxs2 [_ Hcc]]".
wp_load.
wp_apply (sum_list_spec with "Hxs2").
iIntros "_".
wp_pures.
iModIntro.
iApply "HΦ".
eauto with iFrame.
Qed.
Definition lock_example : val :=
λ: "jesper_cc" "robbert_cc" "c",
let: "lk" := newlock #() in
(
(acquire "lk";;
let: "v1" := order_pizza [Margherita] "jesper_cc" "c" in
release "lk";;
"v1")
|||
(acquire "lk";;
let: "v2" := order_pizza [Calzone] "robbert_cc" "c" in
release "lk";;
"v2")
).
Lemma lock_example_spec `{!lockG Σ} jcc rcc c (x1 y1 : Z) :
{{{ c ↣ pizza_prot ∗ jcc ↦ #x1 ∗ rcc ↦ #y1 }}}
lock_example #jcc #rcc c
{{{ (x2 y2 : Z), RET ((#x2, #(x1 - x2)), (#y2, #(y1 - y2)))%V;
jcc ↦ #(x1 - x2) ∗ rcc ↦ #(y1 - y2) }}}.
Proof.
iIntros (Φ) "[Hc [Hjcc Hrcc]] HΦ".
wp_lam. wp_pures.
wp_apply (newlock_spec with "Hc").
iIntros (lk γ) "#Hlk".
wp_pures.
wp_apply (wp_par (λ v, ∃ (x2:Z), ⌜v = (#x2, #(x1 - x2))%V⌝ ∗
jcc ↦ #(x1 - x2)%Z)%I
(λ v, ∃ (y2:Z), ⌜v = (#y2, #(y1 - y2))%V⌝ ∗
rcc ↦ #(y1 - y2)%Z)%I
with "[Hjcc] [Hrcc]").
- wp_pures.
wp_apply (acquire_spec with "Hlk").
iIntros "[Hlocked Hc]".
wp_pures. wp_apply (order_pizza_spec with "[$Hc $Hjcc]").
iIntros (x2) "[Hc Hjcc]".
wp_pures.
wp_apply (release_spec with "[$Hlk $Hlocked $Hc]").
iIntros "_".
wp_pures.
eauto.
- wp_pures.
wp_apply (acquire_spec with "Hlk").
iIntros "[Hlocked Hc]".
wp_pures. wp_apply (order_pizza_spec with "[$Hc $Hrcc]").
iIntros (y2) "[Hc Hrcc]".
wp_pures.
wp_apply (release_spec with "[$Hlk $Hlocked $Hc]").
iIntros "_".
wp_pures.
eauto.
- iIntros (v1 v2) "[HΨ1 HΨ2]".
iIntros "!>".
iDestruct "HΨ1" as (x2) "[-> HΨ1]".
iDestruct "HΨ2" as (y2) "[-> HΨ2]".
iApply ("HΦ" with "[$HΨ1 $HΨ2]").
Qed.
End example.
theories/examples/rpc.v → actris/examples/rpc.v
View file @ c9249305
......@@ -33,7 +33,7 @@ Definition program : val :=
client (Fst "c").
Section rpc_example.
Context `{!heapG Σ, !chanG Σ}.
Context `{!heapGS Σ, !chanG Σ}.
Definition f_spec {T U} (IT : T → val → iProp Σ) (IU : U → val → iProp Σ)
(f : T → U) (fv : val) : iProp Σ :=
......
theories/examples/sort.v → actris/examples/sort.v
View file @ c9249305
......@@ -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 }};
......@@ -105,10 +105,10 @@ Section sort.
wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
wp_smart_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
iDestruct 1 as (->) "[Hl1 Hl2]".
wp_smart_apply (start_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_smart_apply ("IH" with "Hcy"); auto. }
wp_smart_apply (start_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_smart_apply ("IH" with "Hcz"); auto. }
wp_send with "[$Hl1]".
......@@ -141,7 +141,7 @@ Section sort.
{{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_smart_apply (start_chan_spec sort_protocol_func); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec sort_protocol_func); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)).
wp_smart_apply (sort_service_func_spec with "Hc"); auto. }
wp_send with "[$Hcmp]".
......
theories/examples/sort_br_del.v → actris/examples/sort_br_del.v
View file @ c9249305
......@@ -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 Σ :=
......@@ -76,7 +76,7 @@ Section sort_service_br_del.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_smart_apply (start_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
{ wp_smart_apply (fork_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
{ wp_pures. wp_smart_apply (sort_service_spec with "Hcmp Hc'"); auto. }
wp_send with "[$Hc']". by wp_smart_apply ("IH" with "Hc"). }
by iApply "HΨ".
......@@ -102,7 +102,7 @@ Section sort_service_br_del.
{ wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_smart_apply ("IH" with "Hc"). }
wp_branch; wp_pures.
{ wp_smart_apply (start_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
{ wp_smart_apply (fork_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
{ wp_smart_apply ("IH" with "Hc'"); auto. }
wp_send with "[$Hc']".
by wp_smart_apply ("IH" with "Hc"). }
......
theories/examples/sort_fg.v → actris/examples/sort_fg.v
View file @ c9249305
......@@ -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}.
......@@ -148,7 +148,7 @@ Section sort_fg.
Proof.
iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
wp_rec. wp_branch as %_ | %Hys'.
wp_rec. wp_branch as % _ | %Hys'.
- wp_recv (x v) as (Htl) "HI".
wp_select. wp_send with "[$HI]"; first by auto.
wp_smart_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
......@@ -181,7 +181,7 @@ Section sort_fg.
iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
wp_rec. wp_branch as %_ | %Hys2.
wp_rec. wp_branch as % _ | %Hys2.
- wp_recv (x v) as (Htl2) "HIx".
wp_pures. wp_smart_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
case_bool_decide.
......@@ -221,17 +221,17 @@ Section sort_fg.
wp_rec; wp_pures. wp_branch; wp_pures.
- wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
+ wp_recv (x2 v2) as "HIx2".
wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
{ iIntros (cy) "Hcy". wp_smart_apply ("IH" with "Hcy"). auto. }
iIntros (cy) "Hcy".
wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
{ iIntros (cz) "Hcz". wp_smart_apply ("IH" with "Hcz"); auto. }
iIntros (cz) "Hcz". rewrite !right_id.
wp_select. wp_send with "[$HIx1]".
wp_select. wp_send with "[$HIx2]".
wp_smart_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
wp_branch as %_ | %[]%Permutation_nil_cons.
wp_branch as % _ | %[]%Permutation_nil_cons.
wp_recv (x v) as "[_ HIx]".
wp_smart_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
......@@ -265,7 +265,7 @@ Section sort_fg.
Proof.
iIntros (Hsort Φ) "[Hl Hc] HΦ".
iLöb as "IH" forall (xs ys' Φ Hsort).
wp_lam. wp_branch as %_ | %Hperm; wp_pures.
wp_lam. wp_branch as % _ | %Hperm; wp_pures.
- wp_recv (y v) as (Htl) "HIx".
wp_smart_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
......@@ -281,7 +281,7 @@ Section sort_fg.
{{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
{ wp_smart_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
wp_smart_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
wp_select.
......
theories/examples/subprotocols.v → actris/examples/subprotocols.v
View file @ c9249305
From actris.channel Require Import proofmode proto channel.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
Section subprotocol_basics.
Context `{heapG Σ, chanG Σ}.
Context `{heapGS Σ, chanG Σ}.
Lemma reference_example (l1' : loc) :
l1' ↦ #20 -∗
......@@ -66,10 +66,10 @@ Section subprotocol_basics.
Proof.
iIntros "H".
iInduction (xs) as [|x xs] "IH" forall (v).
- eauto.
- iDestruct "H" as (v' Heq) "H".
iDestruct ("IH" with "H") as (ws) "[Hlist Heq]".
iExists (#x::ws)=> /=; eauto.
{ 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 :
......