...
 
Commits (269)
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
.Makefile.coq.d
*.glob
*.cache
*.aux
......
......@@ -18,8 +18,8 @@ variables:
paths:
- opamroot/
only:
- master
- /^ci/
- master@iris/iris
- /^ci/@iris/iris
except:
- triggers
- schedules
......@@ -30,38 +30,35 @@ variables:
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
CI_COQCHK: "1"
build-coq.8.10.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version 8.10.dev"
# CI_COQCHK: "1"
TIMING_CONF: "coq-dev"
tags:
- fp-timing
build-coq.8.9.1:
build-coq.8.11.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.1"
OPAM_PINS: "coq version 8.11.dev"
CI_COQCHK: "1"
build-coq.8.9.0:
build-coq.8.10.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PINS: "coq version 8.10.2"
OPAM_PKG: "coq-iris"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
TIMING_CONF: "coq-8.9.0"
# DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
# DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
TIMING_CONF: "coq-8.10.2"
tags:
- fp-timing
build-coq.8.8.2:
build-coq.8.9.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
OPAM_PINS: "coq version 8.9.1"
build-coq.8.7.2:
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
OPAM_PINS: "coq version 8.8.2"
......@@ -5,7 +5,81 @@ Coq development, but not every API-breaking change is listed. Changes marked
## Iris master
Changes in the theory of Iris itself:
**Changes in the theory of Iris itself:**
* [#] Redefine invariants as "semantic invariants" so that they support
splitting and other forms of weakening.
* Updated the strong variant of the opening lemma for cancellable invariants
to match that of regular invariants, where you can pick the mask at a later time.
**Changes in program logic:**
* In the axiomatization of ectx languages we replace the axiom of positivity of
context composition with an axiom that says if `fill K e` takes a head step,
then either `K` is the empty evaluation context or `e` is a value.
**Changes in Coq:**
* Added support for Coq 8.10; dropped support for Coq 8.7.
* A new tactic `iStopProof` to turn the proof mode entailment into an ordinary
Coq goal `big star of context ⊢ proof mode goal`.
* Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s.
Introduce `iProp` for the `Type` carrier of `iPropO`.
* Move derived camera constructions (`frac_auth` and `ufrac_auth`) to the folder
`algebra/lib`.
* Add derived camera construction `excl_auth A` for `auth (option (excl A))`.
* Make use of `notypeclasses refine` in the implementation of `iPoseProof` and
`iAssumption`, see https://gitlab.mpi-sws.org/iris/iris/merge_requests/329
This has two consequences:
1. Coq's "new" unification algorithm (the one in `refine`, not the "old" one
in `apply`) is used more often by the proof mode tactics.
2. Due to the use of `notypeclasses refine`, TC constraints are solved less
eagerly, see https://github.com/coq/coq/issues/6583.
In order to port your development, it is often needed to instantiate evars
explicitly (since TC search is performed less eagerly), and in few cases it is
needed to unfold definitions explicitly (due to new unification algorithm
behaving differently).
* Removed `Core` type class for defining the total core; it is now always
defined in terms of the partial core. The only user of this type class was the
STS RA.
* Added the type `siProp` of "plain" step-indexed propositions, together with
basic proofmode support.
* Sealed the definitions of `big_opS`, `big_opMS`, `big_opM` and `big_sepM2`
to prevent undesired simplification.
## Iris 3.2.0 (released 2019-08-29)
The highlight of this release is the completely re-engineered interactive proof
mode. Not only did many tactics become more powerful; the entire proof mode can
now be used not just for Iris but also for other separation logics satisfying
the proof mode interface (e.g., [Iron] and [GPFSL]). Also see the
[accompanying paper][MoSeL].
[Iron]: https://iris-project.org/iron/
[GPFSL]: https://gitlab.mpi-sws.org/iris/gpfsl/
[MoSeL]: https://iris-project.org/mosel/
Beyond that, the Iris program logic gained the ability to reason about
potentially stuck programs, and a significantly strengthened adequacy theorem
that unifies the three previously separately presented theorems. There are now
also Hoare triples for total program correctness (but with very limited support
for invariants) and logical atomicity.
And finally, our example language HeapLang was made more realistic
(Compare-and-set got replaced by compare-exchange and limited to only compare
values that can actually be compared atomically) and more powerful, with added
support for arrays and prophecy variables.
Further details are given in the changelog below.
This release of Iris received contributions by Aleš Bizjak, Amin Timany, Dan
Frumin, Glen Mével, Hai Dang, Hugo Herbelin, Jacques-Henri Jourdan, Jan Menz,
Jan-Oliver Kaiser, Jonas Kastberg Hinrichsen, Joseph Tassarotti, Mackie Loeffel,
Marianna Rapoport, Maxime Dénès, Michael Sammler, Paolo G. Giarrusso,
Pierre-Marie Pédrot, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, and Tej
Chajed. Thanks a lot to everyone involved!
**Changes in the theory of Iris itself:**
* Change in the definition of WP, so that there is a fancy update between
the quantification over the next states and the later modality. This makes it
......@@ -33,7 +107,7 @@ Changes in the theory of Iris itself:
* The user-chosen functor used to instantiate the Iris logic now goes from
COFEs to Cameras (it was OFEs to Cameras).
Changes in heap_lang:
**Changes in heap_lang:**
* CAS (compare-and-set) got replaced by CmpXchg (compare-exchange). The
difference is that CmpXchg returns a pair consisting of the old value and a
......@@ -50,7 +124,7 @@ Changes in heap_lang:
operator allowed compared closures with each other.
* Implement prophecy variables using the new support for "observations". The
erasure theorem (showing that prophecy variables do not alter program
behavior) can be found [in the iris/examples repository](https://gitlab.mpi-sws.org/iris/examples/blob/3f33781fe6e19cfdb25259c8194d34403f1134d5/theories/logatom/proph_erasure.v).
behavior) can be found [in the iris/examples repository][prophecy-erasure].
* heap_lang now uses right-to-left evaluation order. This makes it
significantly easier to write specifications of curried functions.
* heap_lang values are now injected in heap_lang expressions via a specific
......@@ -63,17 +137,18 @@ Changes in heap_lang:
(continuously allocated regions of memory).
* One can now assign "meta" data to heap_lang locations.
Changes in Coq:
[prophecy-erasure]: https://gitlab.mpi-sws.org/iris/examples/blob/3f33781fe6e19cfdb25259c8194d34403f1134d5/theories/logatom/proph_erasure.v
**Changes in Coq:**
* An all-new generalized proof mode that abstracts away from Iris! See
<http://iris-project.org/mosel/> for the corresponding paper. Major new
* An all-new generalized proof mode that abstracts away from Iris! Major new
features:
- The proof mode can now be used with logics derived from Iris (like iGPS),
with non-step-indexed logics and even with non-affine (i.e., linear) logics.
- `iModIntro` is more flexible and more powerful, it now also subsumes
`iNext` and `iAlways`.
- General infrastructure for deriving a logic for monotone predicates over
an existing logic (see the paper for more details).
an existing logic (see the paper for more details).
Developments instantiating the proof mode typeclasses may need significant
changes. For developments just using the proof mode tactics, porting should
not be too much effort. Notable things to port are:
......@@ -159,6 +234,13 @@ Changes in Coq:
fractional camera (`frac_auth`) with unbounded fractions.
* Changed `frac_auth` notation from `●!`/`◯!` to `●F`/`◯F`. sed script:
`s/◯!/◯F/g; s/●!/●F/g;`.
* Lemma `prop_ext` works in both directions; its default direction is the
opposite of what it used to be.
* Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`,
`Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`,
`cmra_morphism_core`.
* Rename lemmas `fupd_big_sep{L,M,S,MS}` into `big_sep{L,M,S,MS}_fupd` to be
consistent with other such big op lemmas. Also add such lemmas for `bupd`.
* Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also
rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into
`-d>`. The renaming can be automatically done using the following script (on
......@@ -221,7 +303,7 @@ s/\bcoPset\_disjC/coPset\_disjO/g;
## Iris 3.1.0 (released 2017-12-19)
Changes in and extensions of the theory:
**Changes in and extensions of the theory:**
* Define `uPred` as a quotient on monotone predicates `M -> SProp`.
* Get rid of some primitive laws; they can be derived:
......@@ -241,7 +323,7 @@ Changes in and extensions of the theory:
latter. The full judgment is `WP e @ s; E {{ Φ }}`, where non-stuck WP uses
*stuckness bit* `s = NotStuck` while stuck WP uses `s = MaybeStuck`.
Changes in Coq:
**Changes in Coq:**
* Move the `prelude` folder to its own project:
[coq-std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
......
# Contributing to the Iris Coq Development
Here you can find some how-tos for various thing sthat might come up when doing
Iris development.
Iris development. This is for contributing to Iris itself; see
[the README](README.md#further-resources) for resources helpful for all Iris
users.
## How to submit a merge request
......@@ -24,6 +26,8 @@ a feature branch instead.
* Wait for CI to publish a new std++ version on the opam archive, then run
`opam update iris-dev`.
* In Iris, change the `opam` file to depend on the new version.
(In case you do not use opam yourself, you can see recently published versions
[in this repository](https://gitlab.mpi-sws.org/iris/opam/commits/master).)
* Run `make build-dep` (in Iris) to install the new version of std++.
You may have to do `make clean` as Coq will likely complain about .vo file
mismatches.
......
......@@ -9,7 +9,7 @@ all: Makefile.coq
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
rm -f Makefile.coq .lia.cache
.PHONY: clean
# Create Coq Makefile.
......@@ -29,14 +29,8 @@ build-dep: build-dep/opam phony
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
@echo "# Installing build-dep package."
@opam install $(OPAMFLAGS) build-dep/
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
......@@ -9,7 +9,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1)
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8)\b" -q && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES)
......
This diff is collapsed.
......@@ -9,8 +9,8 @@ For using the Coq library, check out the
For understanding the theory of Iris, a LaTeX version of the core logic
definitions and some derived forms is available in
[docs/iris.tex](docs/iris.tex). A compiled PDF version of this document is
[available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
[tex/iris.tex](tex/iris.tex). A compiled PDF version of this document is
[available online](http://plv.mpi-sws.org/iris/appendix-3.2.pdf).
## Building Iris
......@@ -18,7 +18,7 @@ definitions and some derived forms is available in
This version is known to compile with:
- Coq 8.7.2 / 8.8.2 / 8.9.0 / 8.9.1
- Coq 8.8.2 / 8.9.1 / 8.10.2
- A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
For a version compatible with Coq 8.6, have a look at the
......@@ -28,7 +28,7 @@ If you need to work with Coq 8.5, please check out the
### Working *with* Iris
To use Iris in your own proofs, we recommend you install Iris via opam (1.2.2 or
To use Iris in your own proofs, we recommend you install Iris via opam (2.0.0 or
newer). To obtain the latest stable release, you have to add the Coq opam
repository:
......@@ -46,7 +46,7 @@ developments.
### Working *on* Iris
To work on Iris itself, you need to install its build-dependencies. Again we
recommend you do that with opam (1.2.2 or newer). This requires the following
recommend you do that with opam (2.0.0 or newer). This requires the following
two repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
......@@ -83,7 +83,7 @@ followed by `make build-dep`.
[MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
intuitionistic and spatial BI++ assertions. It also contains tactics for
interactive proofs. Documentation can be found in
[ProofMode.md](ProofMode.md).
[proof_mode.md](docs/proof_mode.md).
* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
language
* The subfolder [lib](theories/heap_lang/lib) contains a few derived
......@@ -113,11 +113,11 @@ that should be compatible with this version:
Getting along with Iris in Coq:
* Iris proof patterns are documented in the [proof guide](ProofGuide.md).
* Syntactic conventions are described in the [style guide](StyleGuide.md).
* Iris proof patterns are documented in the [proof guide](docs/proof_guide.md).
* Syntactic conventions are described in the [style guide](docs/style_guide.md).
* The Iris tactics are described in the
[the Iris Proof Mode (IPM) / MoSeL documentation](ProofMode.md) as well as the
[HeapLang documentation](HeapLang.md).
[the Iris Proof Mode (IPM) / MoSeL documentation](docs/proof_mode.md) as well as the
[HeapLang documentation](docs/heap_lang.md).
* The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
Contacting the developers:
......@@ -137,7 +137,7 @@ Contacting the developers:
Miscellaneous:
* Information on how to set up your editor for unicode input and output is
collected in [Editor.md](Editor.md).
collected in [editor.md](docs/editor.md).
* If you are writing a paper that uses Iris in one way or another, you could use
the [Iris LaTeX macros](docs/iris.sty) for typesetting the various Iris
the [Iris LaTeX macros](tex/iris.sty) for typesetting the various Iris
connectives.
......@@ -17,7 +17,6 @@ theories/algebra/big_op.v
theories/algebra/cmra_big_op.v
theories/algebra/sts.v
theories/algebra/auth.v
theories/algebra/frac_auth.v
theories/algebra/gmap.v
theories/algebra/ofe.v
theories/algebra/base.v
......@@ -39,7 +38,11 @@ theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/algebra/ufrac.v
theories/algebra/namespace_map.v
theories/algebra/ufrac_auth.v
theories/algebra/lib/excl_auth.v
theories/algebra/lib/frac_auth.v
theories/algebra/lib/ufrac_auth.v
theories/si_logic/siprop.v
theories/si_logic/bi.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
......@@ -100,10 +103,12 @@ theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/array.v
theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v
theories/heap_lang/proph_erasure.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/assert.v
......@@ -116,6 +121,8 @@ theories/heap_lang/lib/clairvoyant_coin.v
theories/heap_lang/lib/counter.v
theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v
theories/heap_lang/lib/diverge.v
theories/heap_lang/lib/arith.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
......
......@@ -24,16 +24,19 @@ PROJECTS = [
{ 'name': 'lambda-rust', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'lambda-rust', 'branch': 'ci/weak_mem', 'vars': ['STDPP_REV', 'IRIS_REV', 'ORC11_REV', 'GPFSL_REV'] }, # covers GPFSL and ORC11
{ 'name': 'iron', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'fairis', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'ora', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'reloc', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'c', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'tutorial-popl18', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'spygame', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] }, # these do not work, for some reason
{ 'name': 'time-credits', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'actris', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
]
for project in PROJECTS:
print("Triggering build for {}{}...".format(project['name'], '' if project['branch'] == 'master' else ':'+project['branch']))
url = "https://gitlab.mpi-sws.org/api/v4/projects/iris%2F{}/pipeline".format(project['name'])
id = str(project['id']) if 'id' in project else "iris%2F{}".format(project['name'])
url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id)
json = {
'ref': project['branch'],
'variables': list(map(lambda var: { 'key': var, 'value': os.environ.get(var, "master") }, project['vars'])),
......
This is the Coq development of the Iris Project.
......@@ -68,6 +68,9 @@ on the math symbol list, and with some custom aliases for symbols used a lot in
(append math-symbol-list-basic math-symbol-list-extended))
```
Finally, set your default input method with `M-x customize-set-value`, setting
`default-input-method` to `math`.
### Font Configuration
Even when usable fonts are installed, Emacs tends to pick bad fonts for some
......
......@@ -7,7 +7,7 @@ language for simple examples.
## Language
HeapLang is a lambda-calculus with operations to allocate individual locations,
`load`, `store`, `CAS` (compare-and-swap) and `FAA` (fetch-and-add). Moreover,
`load`, `store`, `CmpXchg` (compare-and-exchange) and `FAA` (fetch-and-add). Moreover,
it has a `fork` construct to spawn new threads. In terms of values, we have
integers, booleans, unit, heap locations, as well as (binary) sums and products.
......@@ -76,17 +76,17 @@ Tactics for the heap:
- `wp_alloc l as "H"`: Reduce an allocation instruction and call the new
location `l` (in the Coq context) and the points-to assertion `H` (in the
spatial context). You can leave away the `as "H"` to introduce it as an
anonymous assertion, i.e., that is equivalent to `as "?"`.
spatial context). You can leave out the `as "H"` to introduce it as an
anonymous assertion, which is equivalent to `as "?"`.
- `wp_load`: Reduce a load operation. This automatically finds the points-to
assertion in the spatial context, and fails if it cannot be found.
- `wp_store`: Reduce a store operation. This automatically finds the points-to
assertion in the spatial context, and fails if it cannot be found.
- `wp_cas_suc`, `wp_cas_fail`: Reduce a succeeding/failing CAS. This
- `wp_cmpxchg_suc`, `wp_cmpxchg_fail`: Reduce a succeeding/failing CmpXchg. This
automatically finds the points-to assertion. It also automatically tries to
solve the (in)equality to show that the CAS succeeds/fails, and opens a new
solve the (in)equality to show that the CmpXchg succeeds/fails, and opens a new
goal if it cannot prove this goal.
- `wp_cas as H1 | H2`: Reduce a CAS, performing a case distinction over whether
- `wp_cmpxchg as H1 | H2`: Reduce a CmpXchg, performing a case distinction over whether
it succeeds or fails. This automatically finds the points-to assertion. The
proof of equality in the first new subgoal will be called `H1`, and the proof
of the inequality in the second new subgoal will be called `H2`.
......@@ -100,11 +100,17 @@ Further tactics:
the goal is for a single, atomic operation -- `wp_bind` can be used to bring
the goal into the right shape.
- `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically
applying `wp_bind` as needed. See the [ProofMode docs](ProofMode.md) for an
applying `wp_bind` as needed. See the [ProofMode docs](./proof_mode.md) for an
explanation of `pm_trm`.
There is no tactic for `Fork`, just do `wp_apply wp_fork`.
To verify a recursive function, use `iLöb`. Make sure you do `wp_pures` before
running `iLöb`; otherwise the induction hypothesis will likely not be applicable
when you need it. (This makes sure that all administrative redexes are reduced
in your induction hypothesis, just like we state our `WP` specifications with
all of the redexes reduced.)
## Notation and lemmas for derived notions involving a thunk
Sometimes, it is useful to define a derived notion in HeapLang that involves
......@@ -120,7 +126,7 @@ value lambda). However, the *specification* for parallel composition should use
value lambdas, because prior to applying it the term will be reduced as much as
possible to achieve a normal form. To facilitate this, we define a copy of the
`e1 ||| e2` notation in the value scope that uses value lambdas.
This is not actually a value, but we still but it in the value scope to
This is not actually a value, but we still put it in the value scope to
differentiate from the other notation that uses expression lambdas. (In the
future, we might decide to add a separate scope for this.) Then, we write the
canonical specification using the notation in the value scope.
......
......@@ -2,9 +2,27 @@
This work-in-progress document serves to explain how Iris proofs are typically
carried out in Coq: what are the common patterns, what are the common pitfalls.
This complements the tactic documentation for the [proof mode](ProofMode.md) and
[HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
the [style guide](StyleGuide.md).
This complements the tactic documentation for the [proof mode](./proof_mode.md) and
[HeapLang](./heap_lang.md) as well as the documentation of syntactic conventions in
the [style guide](./style_guide.md).
## Order of `Requires`
In Coq, declarations in modules imported later may override the
previous definition. Therefore, in order to make sure the most
relevant declarations and notations always take priority, we recommend
importing dependencies from the furthest to the closest.
In particular, when importing Iris, Stdpp and Coq stdlib modules, we
recommend importing in the following order:
- Coq
- stdpp
- iris.bi
- iris.proofmode
- iris.algebra
- iris.base_logic
- iris.program_logic
- iris.heap_lang
## Combinators for functors
......
This diff is collapsed.
......@@ -2,8 +2,8 @@
This document lays down syntactic conventions about how we usually write our
Iris proofs in Coq. It is a work-in-progress. This complements the tactic
documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as
well as the [proof guide](ProofGuide.md).
documentation for the [proof mode](./proof_mode.md) and [HeapLang](./heap_lang.md) as
well as the [proof guide](.doco/proof_guide.md).
## Implicit generalization
......@@ -114,5 +114,8 @@ is used by clients.
* R: cameras
* UR: unital cameras or resources algebras
* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
* G: global camera functor management
* T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
* G: global camera functor management (typeclass; see [proof\_guide.md](./proof_guide.md))
* I: bunched implication logic (of type `bi`)
* SI: step-indexed bunched implication logic (of type `sbi`)
* T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](./proof_guide.md))
opam-version: "1.2"
opam-version: "2.0"
name: "coq-iris"
synopsis: "This is the Coq development of the Iris Project"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The Iris Team"
homepage: "http://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
license: "BSD"
dev-repo: "https://gitlab.mpi-sws.org/iris/iris.git"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
homepage: "https://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
synopsis: "This is the Coq development of the Iris Project"
depends: [
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-07-08.0.2e0bf441") | (= "dev") }
"coq" { (= "8.8.2") | (>= "8.9.1" & < "8.12~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-01-18.0.7e0096d8") | (= "dev") }
]
build: [make "-j%{jobs}%"]
install: [make "install"]
From iris.base_logic.lib Require Import invariants.
Instance test_cofe {Σ} : Cofe (iPreProp Σ) := _.
Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Section tests.
Context `{!invG Σ}.
Program Definition test : (iProp Σ -n> iProp Σ) -n> (iProp Σ -n> iProp Σ) :=
Program Definition test : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ) :=
λne P v, ( (P v))%I.
Solve Obligations with solve_proper.
......
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
aheap : atomic_heap Σ
Q : iProp Σ
l : loc
v : val
============================
"Hl" : l ↦ v
--------------------------------------∗
AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
<< l ↦{q} v0, COMM Q -∗ Q >>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
============================
<<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
"Now come the long pre/post tests"
: string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy
∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
============================
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
============================
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
============================
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
============================
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
"Prettification"
: string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
"AU" : ∃ x : val, P x
∗ (P x
={∅,⊤}=∗ AU << ∀ x0 : val,
P x0 >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>)
∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
--------------------------------------∗
WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
......@@ -12,6 +12,18 @@
AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
<< l ↦{q} v0, COMM Q -∗ Q >>
"non_laterable"
: string
The command has indeed failed with message:
Ltac call to "iAuIntro" failed.
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
The command has indeed failed with message:
In nested Ltac calls to "awp_apply (open_constr)",
"<ssreflect_plugin::ssrtclseq@0> wp_apply_core lem fun H => iApplyHyp H ; last iAuIntro" and
"iAuIntro", last call failed.
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
"printing"
: string
1 subgoal
Σ : gFunctors
......
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation atomic_heap.
Set Ltac Backtrace.
Set Default Proof Using "Type".
Section tests.
......@@ -17,7 +18,24 @@ Section tests.
Qed.
End tests.
(* Test if we get reasonable error messages with non-laterable assertions in the context. *)
Section error.
Context `{!heapG Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation.
Check "non_laterable".
Lemma non_laterable (P : iProp Σ) (l : loc) :
P - WP !#l {{ _, True }}.
Proof.
iIntros "HP". wp_apply load_spec. Fail iAuIntro.
Restart.
iIntros "HP". Fail awp_apply load_spec.
Abort.
End error.
(* Test if AWP and the AU obtained from AWP print. *)
Check "printing".
Section printing.
Context `{!heapG Σ}.
......
......@@ -86,6 +86,16 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
--------------------------------------∗
WP "x" {{ _, True }}
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go",
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iAndDestruct (constr) as (constr) (constr)", last call failed.
Tactic failure: iAndDestruct: cannot destruct (l ↦∗ (vs1 ++ vs2))%I.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: (l ↦∗ (vs1 ++ vs2))%I not a separating conjunction.
1 subgoal
Σ : gFunctors
......
......@@ -155,6 +155,23 @@ Section tests.
by iApply "HΦ".
Qed.
Lemma wp_load_array l :
{{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l + #1) {{{ RET #1; True }}}.
Proof.
iIntros (Φ) "Hl HΦ". wp_op.
wp_apply (wp_load_offset _ _ _ 1 with "Hl"); first done.
iIntros "Hl". by iApply "HΦ".
Qed.
Lemma test_array_app l vs1 vs2 :
l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
Proof.
Fail iIntros "[H1 H2]". (* this should, one day, split at the fraction. *)
iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
Fail iSplitL "H1".
iApply array_app. iSplitL "H1"; done.
Qed.
End tests.
Section printing_tests.
......
(* Test yet another way of importing heap_lang modules that used to break
printing *)
From iris.heap_lang Require Export lifting notation.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
......@@ -3,8 +3,8 @@
Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany and Lars Birkedal
POPL 2017 *)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import base_logic.
From iris.program_logic Require Export hoare.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
......@@ -10,7 +10,7 @@
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
--------------------------------------∗
WP rev hd acc [{ v, Φ v }]
WP (rev hd) acc [{ v, Φ v }]
1 subgoal
......@@ -28,6 +28,6 @@
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
"l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
end [{ v, Φ v }]
......@@ -10,7 +10,7 @@
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
--------------------------------------∗
WP (rev hd) acc [{ v, Φ v }]
WP rev hd acc [{ v, Φ v }]
1 subgoal
......@@ -28,6 +28,6 @@
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
"l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
end [{ v, Φ v }]
(** Correctness of in-place list reversal *)
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export total_weakestpre weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
......@@ -5,8 +5,8 @@ Separation Logic
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
ICFP 2018 *)
From iris.proofmode Require Import tactics monpred.
From iris.bi Require Import monpred.
From iris.proofmode Require Import tactics monpred.
Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A PROP) :
P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a).
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl agree csum.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl agree csum.
From iris.heap_lang Require Import assert proofmode notation adequacy.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import par.
Set Default Proof Using "Type".
(** This is the introductory example from the "Iris from the Ground Up" journal
paper. *)
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(* tryset *) (λ: "n",
......
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
one_shotG0 : one_shotG Σ
Φ : val → iProp Σ
N : namespace
l : loc
γ : gname
============================
"HN" : inv N (one_shot_inv γ l)
--------------------------------------□
"Hl" : l ↦ InjLV #()
_ : own γ (Pending (1 / 2))
--------------------------------------∗
one_shot_inv γ l
∗ (⌜InjLV #() = InjLV #()⌝
∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
one_shotG0 : one_shotG Σ
Φ : val → iProp Σ
N : namespace
l : loc
γ : gname
m, m' : Z
============================
"HN" : inv N (one_shot_inv γ l)
"Hγ'" : own γ (Shot m)
--------------------------------------□
"Hl" : l ↦ InjRV #m'
"Hγ" : own γ (Shot m')
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
∗ WP let: "y'" := InjRV #m' in
match: InjRV #m with
InjL <> => #()
| InjR <> => assert: InjRV #m = "y'"
end {{ _, True }}
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac agree csum.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import assert proofmode notation adequacy.
From iris.heap_lang.lib Require Import par.
Set Default Proof Using "Type".
(** This is the introductory example from Ralf's PhD thesis.
The difference to [one_shot] is that [set] asserts to be called only once. *)
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(* set *) (λ: "n",
assert: CAS "x" NONE (SOME "n")),
(* check *) (λ: <>,
let: "y" := !"x" in λ: <>,
let: "y'" := !"x" in
match: "y" with
NONE => #()
| SOME <> => assert: "y" = "y'"
end)).
Definition one_shotR := csumR fracR (agreeR ZO).
Definition Pending (q : Qp) : one_shotR := Cinl q.
Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ one_shotG Σ.
Proof. solve_inG. Qed.
Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !one_shotG Σ}.
Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
(l NONEV own γ (Pending (1/2)%Qp)
n : Z, l SOMEV #n own γ (Shot n))%I.
Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) =>
unfold one_shot_inv : core.
Lemma pending_split γ q :
own γ (Pending q) own γ (Pending (q/2)) own γ (Pending (q/2)).
Proof.
rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op' Qp_div_2 //.
Qed.
Lemma pending_shoot γ n :
own γ (Pending 1%Qp) == own γ (Shot n).
Proof.
iIntros "Hγ". iMod (own_update with "Hγ") as "$"; last done.
by apply cmra_update_exclusive with (y:=Shot n).
Qed.
Lemma wp_one_shot (Φ : val iProp Σ) :
( (f1 f2 : val) (T : iProp Σ), T
( n : Z, T - WP f1 #n {{ w, True }})
WP f2 #() {{ g, WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "Hf /=". pose proof (nroot .@ "N") as N.
rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Pending 1%Qp)) as (γ) "Hγ"; first done.
iDestruct (pending_split with "Hγ") as "[Hγ1 Hγ2]".
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ2]") as "#HN".
{ iNext. iLeft. by iFrame. }
wp_pures. iModIntro. iApply ("Hf" $! _ _ (own γ (Pending (1/2)%Qp))).
iSplitL; first done. iSplit.
- iIntros (n) "!# Hγ1". wp_pures.
iApply wp_assert. wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as ">[[Hl Hγ2]|H]"; last iDestruct "H" as (m) "[Hl Hγ']".
+ iDestruct (pending_split with "[$Hγ1 $Hγ2]") as "Hγ".
iMod (pending_shoot _ n with "Hγ") as "Hγ".
wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
iNext; iRight; iExists n; by iFrame.
+ by iDestruct (own_valid_2 with "Hγ1 Hγ'") as %?.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ".
iAssert ( v, l v (v = NONEV own γ (Pending (1/2)%Qp)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]" as "Hv".
{ iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
+ iExists NONEV. iFrame. eauto.
+ iExists (SOMEV #m). iFrame. eauto. }
iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
iAssert (one_shot_inv γ l (v = NONEV n : Z,
v = SOMEV #n own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
+ Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iSplitL "Hinv"; first by eauto.
iModIntro. wp_pures. iIntros "!#". wp_lam. wp_bind (! _)%E.
iInv N as "Hinv".
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
+ iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]";
wp_load; iModIntro; (iSplitL "Hl Hγ"; first by eauto with iFrame);
wp_pures; done.
+ iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
{ by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
wp_load. Show.
iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
iModIntro. iSplitL "Hl Hγ"; first by eauto with iFrame.
wp_pures. iApply wp_assert. wp_op. by case_bool_decide.
Qed.
Lemma ht_one_shot (Φ : val iProp Σ) :
{{ True }} one_shot_example #()
{{ ff, T, T
( n : Z, {{ T }} Fst ff #n {{ _, True }})
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
}}.
Proof.
iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
iExists T. iFrame "HT". iSplit.
- iIntros (n) "!# HT". wp_apply "Hf1". done.
- iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.
(* Have a client with a closed proof. *)
Definition client : expr :=
let: "ff" := one_shot_example #() in
(Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
Lemma client_safe : WP client {{ _, True }}%I.
Proof using Type*.
rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
wp_let. wp_apply (wp_par with "[HT]").
- wp_apply "Hf1". done.
- wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2".
iIntros (check) "Hcheck". wp_pures. iApply "Hcheck".
- auto.
Qed.
End client.
(** Put together all library functors. *)
Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
(** This lemma implicitly shows that these functors are enough to meet
all library assumptions. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
......@@ -21,6 +21,25 @@
--------------------------------------□
Q ∨ P
"test_iStopProof"
: string
1 subgoal
PROP : sbi
Q : PROP
============================
"H1" : emp