...
 
Commits (274)
......@@ -15,3 +15,4 @@ build-dep/
Makefile.coq
Makefile.coq.conf
*.crashcoqide
.env
......@@ -23,6 +23,7 @@ variables:
except:
- triggers
- schedules
- api
## Build jobs
......@@ -31,44 +32,35 @@ build-coq.dev:
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
VALIDATE: "1"
CI_COQCHK: "1"
build-coq.8.9.dev:
build-coq.8.10.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.dev"
TIMING_PROJECT: "iris"
TIMING_CONF: "coq-8.9.dev"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version 8.10.dev"
build-coq.8.8.1:
build-coq.8.9.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.1"
OPAM_PINS: "coq version 8.9.1"
build-coq.8.8.0:
build-coq.8.9.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.0"
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-iris"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
TIMING_PROJECT: "iris"
TIMING_CONF: "coq-8.8.0"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
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"
build-coq.8.7.1:
build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1"
OPAM_PINS: "coq version 8.7.2"
<!--
When reporting a bug, please always include the version of Iris you are using.
If you are using opam, you can determine your Iris version by running
opam show coq-iris -f version
-->
......@@ -53,11 +53,10 @@ Changes in Coq:
- `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:
changes. For developments just using the proof mode tactics, porting should
not be too much effort. Notable things to port are:
- All the BI laws moved from the `uPred` module to the `bi` module. For
example, `uPred.later_equivI` became `bi.later_equivI`.
- Big-ops are automatically imported, imports of `iris.base_logic.big_op` have
......@@ -68,6 +67,8 @@ Changes in Coq:
* The `iInv` tactic can now be used without the second argument (the name for
the closing update). It will then instead add the obligation to close the
invariant to the goal.
* The new `iEval` tactic can be used to execute a simplification or rewriting
tactic on some specific part(s) of the proofmode goal.
* Added support for defining derived connectives involving n-ary binders using
telescopes.
* The proof mode now more consistently "prettifies" the goal after each tactic.
......@@ -99,6 +100,38 @@ Changes in Coq:
* A new tactic, `wp_pures`, executes as many pure steps as possible, excluding
steps that would require unlocking subterms. Every impure wp_ tactic executes
this tactic before doing anything else.
* Add `big_sepM_insert_acc`.
* Add big separating conjunctions that operate on pairs of lists (`big_sepL2`)
and on pairs of maps (`big_sepM2`). In the former case the lists are required
to have the same length, and in the latter case the maps are required to
have the same domains.
* The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite
sets, instead of just for cofinite sets. The versions with cofinite
sets have been renamed to use the `_cofinite` suffix.
* Remove locked value lambdas. The value scope notations `rec: f x := e` and
`(λ: x, e)` no longer add a `locked`. Instead, we made the `wp_` tactics
smarter to no longer unfold lambdas/recs that occur behind definitions.
* Export the fact that `iPreProp` is a COFE.
* The CMRA `auth` now can have fractional authoritative parts. So now `auth` has
3 types of elements: the fractional authoritative `●{q} a`, the full
authoritative `● a ≡ ●{1} a`, and the non-authoritative `◯ a`. Updates are
only possible with the full authoritative element `● a`, while fractional
authoritative elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`. As a
consequence, `auth` is no longer a COFE and does not preserve Leibniz
equality.
* Rename in `auth`:
- Use `auth_auth_proj`/`auth_frag_proj` for the projections of `auth`:
`authoritative``auth_auth_proj` and `auth_own``auth_frag_proj`.
- Use `auth_auth` and `auth_frag` for the injections into authoritative
elements and non-authoritative elements respectively.
- Lemmas for the projections and injections are renamed accordingly.
For examples:
+ `authoritative_validN``auth_auth_proj_validN`
+ `auth_own_validN``auth_frag_proj_validN`
+ `auth_auth_valid` was not renamed because it was already used for the
authoritative injection.
- `auth_both_valid``auth_both_valid_2`
- `auth_valid_discrete_2``auth_both_valid`
## Iris 3.1.0 (released 2017-12-19)
......
# Contributing to the Iris Coq Development
Discussion about the Iris Coq development happens on the mailing list
[iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club) and
in the [Iris Chat](https://mattermost.mpi-sws.org/iris). This is also the right
place to ask questions. The chat requires an account at the
[MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
tab).
If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
requires an MPI-SWS GitLab account. To contribute code, please send your
MPI-SWS GitLab username to [Ralf Jung](https://gitlab.mpi-sws.org/jung) to
enable personal projects for your account. Then you can fork the
[Iris git repository](https://gitlab.mpi-sws.org/FP/iris-coq/), make your
changes in your fork, and create a merge request.
Here you can find some how-tos for various thing sthat might come up when doing
Iris development.
## How to submit a merge request
To contribute code, you need an [MPI-SWS GitLab account][account] (use the
"Register" tab). Please send your MPI-SWS GitLab username to [Ralf Jung][jung]
to enable personal projects for your account. Then you can fork the
[Iris git repository][iris], make your changes in your fork, and create a merge
request.
Please do *not* use the master branch of your fork, that might confuse CI. Use
a feature branch instead.
[account]: https://gitlab.mpi-sws.org/users/sign_in
[jung]: https://gitlab.mpi-sws.org/jung
[iris]: https://gitlab.mpi-sws.org/iris/iris
## How to update the std++ dependency
* Do the change in std++, push it.
* 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.
* 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.
## How to write/update test cases
The files in `tests/` are test cases. Each of the `.v` files comes with a
matching `.ref` file containing the expected output of `coqc`. Adding `Show.`
in selected places in the proofs makes `coqc` print the current goal state.
This is used to make sure the proof mode prints goals and reduces terms the way
we expect it to. You can run `make MAKE_REF=1` to re-generate all the `.ref` files;
this is useful after adding or removing `Show.` from a test. If you do this,
make sure to check the diff for any unexpected changes in the output!
Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
Coq-8.8-specific `.ref` file). If you change one of these, remember to update
*all* the `.ref` files.
## How to measure the timing effect on a reverse dependency
So say you did a change in Iris, and want to know how it affects [lambda-rust]
or the [examples]. To do this, check out the respective project and change its
`.gitlab-ci.yml` to contain only one build job, which should look like
```
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0 coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
```
You will have to adjust this a bit: you should use the same Coq version as
whatever the master branch uses for its timing job, which you can determine by
checking its `.gitlab-ci.yml`. If you change the Coq version, remember to do it
in both places (`OPAM_PINS` and `TIMING_CONF`). You will also have to adjust
the Iris branch being used, which is determined after the `#` in `OPAM_PINS`.
If you are in doubt, ask on Mattermost *before* pushing your branch. Please
double-check that the job name is `build-iris.dev` to avoid polluting the caches
of regular CI builds! This way, you are going to share the cache with the
nightly builds, which is fine.
Once you are confident with your CI configuration, push this to a new branch
whose name starts with `ci/`. It should usually be of the form
`ci/yourname/feature`. You should see a pipeline running in GitLab with just a
single job, and you can follow its progress there.
When the job is done, you should be able to see it as a single dot on our
[statistics server][coq-speed] after selecting the right project and branch.
Click on "Coq-Speed" on the top-left corner to switch to another dashboard, and
select "Coq-Compare". Now you can select the project and the two measurements
you want to compare, which would be the SHA of the commit you just created as
"Commit 2", and the SHA of its parent as "Commit 1". Don't forget to also
select the right configuration for both of them. The "Grouping" is a regular
expression that you can use to switch between per-file, per-directory and
per-project grouping of the measurements.
If you changed your Iris branch and want to make another measurement, *do not*
just "Retry" the CI job. That will lead to an error, because you would end up
with two measurements for the same commit. Instead, create an empty commit in
your branch of the to-be-measured project (`git commit --allow-empty -m
"rerun"`), and push that.
[lambda-rust]: https://gitlab.mpi-sws.org/iris/lambda-rust
[examples]: https://gitlab.mpi-sws.org/iris/examples
[coq-speed]: https://coq-speed.mpi-sws.org
# HeapLang overview
HeapLang is the example language that gets shipped with Iris. It is not the
only language you can reason about with Iris, but meant as a reasonable demo
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,
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.
Recursive functions are the only binders, so the sum elimination (`Case`)
expects both branches to be of function type and passes them the data component
of the sum.
For technical reasons, the only terms that are considered values are those that
begin with the `Val` expression former. This means that, for example, `Pair
(Val a) (Val b)` is *not* a value -- it reduces to `Val (PairV a b)`, which is.
This leads to some administrative redexes, and to a distinction between "value
pairs", "value sums", "value closures" and their "expression" counterparts.
However, this also makes values syntactically uniform, which we exploit in the
definition of substitution which just skips over `Val` terms, because values
should be closed and hence not affected by substitution. As a consequence, we
can entirely avoid even talking about "closed terms", that notion just does not
have to come up anywhere. We also exploit this when writing specifications,
because we can just write lemmas involving terms of the form `Val ?v` and Coq
can determine `?v` by unification (because all values start with the `Val`
constructor).
## Notation
Notation for writing HeapLang terms is defined in
[`notation.v`](theories/heap_lang/notation.v). There are two scopes, `%E` for
expressions and `%V` for values. For example, `(a, b)%E` is an expression pair
and `(a, b)%V` a value pair. The `e` of a `WP e {{ Q }}` is implicitly in `%E`
scope.
We define a whole lot of short-hands, such as non-recursive functions (`λ:`),
let-bindings, sequential composition, and a more conventional `match:` that has
binders in both branches.
The widely used `#` is a short-hand to turn a basic literal (an integer, a
location, a boolean literal or a unit value) into a value. Since values coerce
to expressions, `#` is widely used whenever a Coq value needs to be placed into
a HeapLang term.
## Tactics
HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang
programs as part of proving a weakest precondition. All of these tactics assume
that the current goal is of the shape `WP e @ E {{ Q }}`.
Tactics to take one or more pure program steps:
- `wp_pure`: Perform one pure reduction step. Pure steps are defined by the
`PureExec` typeclass and include beta reduction, projections, constructors, as
well as unary and binary arithmetic operators.
- `wp_pures`: Perform as many pure reduction steps as possible. This
tactic will **not** reduce lambdas/recs that are hidden behind a definition.
- `wp_rec`, `wp_lam`: Perform a beta reduction. Unlike `wp_pure`, this will
also reduce lambdas that are hidden behind a definition.
- `wp_let`, `wp_seq`: Reduce a let-binding or a sequential composition.
- `wp_proj`: Reduce a projection.
- `wp_if_true`, `wp_if_false`, `wp_if`: Reduce a conditional expression. The
discriminant must already be `true` or `false`.
- `wp_unop`, `wp_binop`, `wp_op`: Reduce a unary, binary or either kind of
arithmetic operator.
- `wp_case`, `wp_match`: Reduce `Case`/`match:` constructs.
- `wp_inj`, `wp_pair`, `wp_closure`: Reduce constructors that turn expression
sums/pairs/closures into their value counterpart.
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 "?"`.
- `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
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
goal if it cannot prove this goal.
- `wp_cas as H1 | H2`: Reduce a CAS, 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`.
- `wp_faa`: Reduce a FAA. This automatically finds the points-to assertion.
Further tactics:
- `wp_bind pat`: Apply the bind rule to "focus" the term matching `pat`. For
example, `wp_bind (!_)%E` focuses a load operation. This is useful in
particular when accessing invariants, which is only possible when the `WP` in
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
explanation of `pm_trm`.
There is no tactic for `Fork`, just do `wp_apply wp_fork`.
## Notation and lemmas for derived notions involving a thunk
Sometimes, it is useful to define a derived notion in HeapLang that involves
thunks. For example, the parallel composition `e1 ||| e2` is defineable in
HeapLang, but that requires thunking `e1` and `e2` before passing them to
`par`. (This is defined in [`par.v`](theories/heap_lang/lib/par.v).) However,
this is somewhat subtle because of the distinction between expression lambdas
and value lambdas.
The normal `e1 ||| e2` notation uses expression lambdas, because clearly we want
`e1` and `e2` to behave normal under substitution (which they would not in a
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
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.
This works very well for non-recursive notions. For `while` loops, the
situation is unfortunately more complex and proving the desired specification
will likely be more involved than expected, see this [discussion].
[discussion]: https://gitlab.mpi-sws.org/iris/iris/merge_requests/210#note_32842
......@@ -8,7 +8,7 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
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
.PHONY: clean
......@@ -28,16 +28,15 @@ build-dep: build-dep/opam phony
@# 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.
@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@# package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
((! opam --version | grep "^1\." > /dev/null) || ( \
echo "# Reinstalling build-dep package." && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \
))
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
# run tests with main build
real-all: test
# Run tests interleaved with main build. They have to be in the same target for this.
real-all: $(if $(NO_TEST),,test)
# the test suite
TESTFILES=$(wildcard tests/*.v)
......@@ -8,12 +8,8 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_BROKEN=
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
# Oh Unix...
REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES'
......@@ -21,17 +17,17 @@ tests/.coqdeps.d: $(TESTFILES)
-include tests/.coqdeps.d
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
$(SHOW)$(if $(MAKE_REF),COQTEST [ref],$(if $(COQ_BROKEN),COQTEST [ignored],COQTEST)) $<
$(HIDE)TEST="$$(basename -s .v $<)" && \
if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
else \
REF="tests/$$TEST.ref"; \
fi && \
echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \
TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
$(if $(MAKE_REF), \
mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
$(if $(COQ_BROKEN), \
true, \
diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered" \
) \
$(if $(COQ_OLD),true, \
$(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \
) && \
rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
rm -f "$$TMPFILE" && \
touch $@
# Iris Proof Guide
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).
## Resource algebra management
When using ghost state in Iris, you have to make sure that the resource algebras
you need are actually available. Every Iris proof is carried out using a
universally quantified list `Σ: gFunctors` defining which resource algebras are
available. You can think of this as a list of resource algebras, though in
reality it is a list of functors from OFEs to Cameras (where Cameras are a
step-indexed generalization of resource algebras). This is the *global* list of
resources that the entire proof can use. We keep it universally quantified to
enable composition of proofs. The formal side of this is described in §7.4 of
[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we
describe the Coq aspects of this approach.
The assumptions that an Iris proof makes are collected in a type class called
`somethingG`. The most common kind of assumptions is `inG`, which says that a
particular resource algebra is available for ghost state. For example, in the
[one-shot example](tests/one_shot.v):
```
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
```
The `:>` means that the projection `one_shot_inG` is automatically registered as
an instance for type-class resolution. If you need several resource algebras,
just add more `inG` fields. If you are using another module as part of yours,
add a field like `one_shot_other :> otherG Σ`.
Having defined the type class, we need to provide a way to instantiate it. This
is an important step, as not every resource algebra can actually be used: if
your resource algebra refers to `Σ`, the definition becomes recursive. That is
actually legal under some conditions (which is why the global list `Σ` contains
functors and not just resource algebras), but for the purpose of this guide we
will ignore that case. We have to define a list that contains all the resource
algebras we need:
```
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
```
This time, there is no `Σ` in the context, so we cannot accidentally introduce a
bad dependency. If you are using another module as part of yours, add their
`somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`. (The
`#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each
other; together with a coercion from a single functor to a singleton list, this
means lists can be nested arbitrarily.)
Now we can define the one and only instance that our type class will ever need:
```
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. solve_inG. Qed.
```
The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
global list `Σ`. Typically, this should be the only assumption your instance
needs, showing that the assumptions of the module (and all the modules it
uses internally) can trivially be satisfied by picking the right `Σ`.
Now you can add `one_shotG` as an assumption to all your module definitions and
proofs. We typically use a section for this:
```
Section proof.
Context `{!heapG Σ, !one_shotG Σ}.
```
Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
which are assumptions that every HeapLang proof makes (they are related to
defining the `↦` connective as well as the basic Iris infrastructure for
invariants and WP). For this purpose, `heapG` contains not only assumptions
about `Σ`, it also contains some ghost names to refer to particular ghost state
(see "global ghost state instances" below).
The backtic (`` ` ``) is used to make anonymous assumptions and to automatically
generalize the `Σ`. When adding assumptions with backtic, you should most of
the time also add a `!` in front of every assumption. If you do not then Coq
will also automatically generalize all indices of type-classes that you are
assuming. This can easily lead to making more assumptions than you are aware
of, and often it leads to duplicate assumptions which breaks type class
resolutions.
### Obtaining a closed proof
To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
`inG`, you have to assemble a list of functors of all the involved modules,
and if your proof relies on some singleton (most do, at least indirectly; also
see the next section), you have to call the respective initialization or
adequacy lemma. [For example](tests/one_shot.v):
```
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
Lemma client_safe : WP client {{ _, True }}%I.
(* ... *)
End client.
(** Assemble all functors needed by the [client_safe] proof. *)
Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
(** Apply [heap_adequacy] with this list of all functors. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
```
### Advanced topic: Ghost state singletons
Some Iris modules involve a form of "global state". For example, defining the
`↦` for HeapLang involves a piece of ghost state that matches the current
physical heap. The `gname` of that ghost state must be picked once when the
proof starts, and then globally known everywhere. Hence it is added to
`gen_heapG`, the type class for the generalized heap module:
```
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
gen_heap_name : gname
}.
```
Such modules always need some kind of "initialization" to create an instance
of their type class. For example, the initialization for `heapG` is happening
as part of [`heap_adequacy`](theories/heap_lang/adequacy.v); this in turn uses
the initialization lemma for `gen_heapG` from
[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
```
Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
(|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
```
These lemmas themselves only make assumptions the way normal modules (those
without global state) do, which are typically collected in a `somethingPreG`
type class (such as `gen_heapPreG`):
```
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V))
}.
```
Just like in the normal case, `somethingPreG` type classes have an `Instance`
showing that a `subG` is enough to instantiate them:
```
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
Proof. solve_inG. Qed.
```
The initialization lemma then shows that the `somethingPreG` type class is
enough to create an instance of the main `somethingG` class *below a view
shift*. This is written with an existential quantifier in the lemma because the
statement after the view shift (`gen_heap_ctx σ` in this case) depends on having
an instance of `gen_heapG` in the context.
Given that these global ghost state instances are singletons, they must be
assumed explicitly everywhere. Bundling `heapG` in a module type class like
`one_shotG` would lose track of the fact that there exists just one `heapG`
instance that is shared by everyone.
### Advanced topic: Additional module assumptions
Some modules need additional assumptions. For example, the STS module is
parameterized by an STS and assumes that the STS state space is inhabited:
```
Class stsG Σ (sts : stsT) := {
sts_inG :> inG Σ (stsR sts);
sts_inhabited :> Inhabited (sts.state sts);
}.
```
In this rather exceptional case, the `Instance` for this class has more than
just a `subG` assumption:
```
Instance subG_stsΣ Σ sts :
subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
```
If users of this module follow the pattern described above, their own type class
instance will check these additional assumption. But this is one more reason
why it is important for every module to have an instance for its `somethingG`:
to make sure that it does not accidentally make more assumptions than it intends
to.
Another subtle detail here is that the `subG` assumption comes first in
`subG_stsΣ`, i.e., it appears before the `Inhabited`. This is important because
otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
type class search diverge.
## Canonical structures and type classes
In Iris, we use both canonical structures and type classes, and some careful
tweaking is necessary to make the two work together properly. The details of
this still need to be written up properly, but here is some background material:
* [Type Classes for Mathematics in Type Theory](http://www.eelis.net/research/math-classes/mscs.pdf)
* [Canonical Structures for the working Coq user](https://hal.inria.fr/hal-00816703v1/document)
This diff is collapsed.
......@@ -18,13 +18,13 @@ definitions and some derived forms is available in
This version is known to compile with:
- Coq 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
- Coq 8.7.2 / 8.8.2 / 8.9.0 / 8.9.1
- 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
[iris-3.1 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.1).
[iris-3.1 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.1).
If you need to work with Coq 8.5, please check out the
[iris-3.0 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0).
[iris-3.0 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.0).
### Working *with* Iris
......@@ -36,7 +36,7 @@ repository:
To obtain a development version, also add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Either way, you can now do `opam install coq-iris`. To fetch updates later, run
`opam update && opam upgrade`. However, notice that we do not guarnatee
......@@ -50,7 +50,7 @@ recommend you do that with opam (1.2.2 or newer). This requires the following
two repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
......@@ -89,7 +89,7 @@ followed by `make build-dep`.
* The subfolder [lib](theories/heap_lang/lib) contains a few derived
constructions within this language, e.g., parallel composition.
For more examples of using Iris and heap_lang, have a look at the
[Iris Examples](https://gitlab.mpi-sws.org/FP/iris-examples).
[Iris Examples](https://gitlab.mpi-sws.org/iris/examples).
* The folder [tests](theories/tests) contains modules we use to test our
infrastructure. Users of the Iris Coq library should *not* depend on these
modules; they may change or disappear without any notice.
......@@ -99,38 +99,45 @@ followed by `make build-dep`.
The following is a (probably incomplete) list of case studies that use Iris, and
that should be compatible with this version:
* [Iris Examples](https://gitlab.mpi-sws.org/FP/iris-examples) is where we
* [Iris Examples](https://gitlab.mpi-sws.org/iris/examples) is where we
collect miscellaneous case studies that do not have their own repository.
* [LambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/) is a Coq
* [LambdaRust](https://gitlab.mpi-sws.org/iris/lambda-rust) is a Coq
formalization of the core Rust type system.
* [iGPS](https://gitlab.mpi-sws.org/FP/sra-gps/tree/gen_proofmode_WIP) is a
logic for release-acquire memory.
* [Iris Atomic](https://gitlab.mpi-sws.org/FP/iris-atomic/) is an experimental
formalization of logically atomic triples in Iris.
## Notes for Iris Developers
* [GPFSL](https://gitlab.mpi-sws.org/iris/gpfsl) is a logic for release-acquire
and relaxed memory.
* [Iron](https://gitlab.mpi-sws.org/iris/iron) is a linear separation logic
built on top of Iris for precise reasoning about resources (such as making
sure there are no memory leaks).
## Further Resources
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).
* 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 generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
Contacting the developers:
* Discussion about the Iris Coq development happens on the mailing list
[iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club)
and in the [Iris Chat](https://mattermost.mpi-sws.org/iris). This is also the
right place to ask questions. The chat requires an account at the
[MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
tab). If you have trouble joining the chat, please contact
[Ralf](https://gitlab.mpi-sws.org/jung).
* If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which also
requires an MPI-SWS GitLab account.
* To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
Miscellaneous:
* Information on how to set up your editor for unicode input and output is
collected in [Editor.md](Editor.md).
* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
* Naming conventions are documented at [Naming.md](Naming.md).
### How to update the std++ dependency
* Do the change in std++, push it.
* 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.
* 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.
### How to write/update test cases
The files in `tests/` are test cases. Each of the `.v` files comes with a
matching `.ref` file containing the expected output of `coqc`. Adding `Show.`
in selected places in the proofs makes `coqc` print the current goal state.
This is used to make sure the proof mode prints goals and reduces terms the way
we expect it to. You can run `MAKE_REF=1 make` to re-generate all the `.ref` files;
this is useful after adding or removing `Show.` from a test. If you do this,
make sure to check the diff for any unexpected changes in the output!
* 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
connectives.
# Naming conventions for variables/arguments/hypotheses in the Coq development
# Iris Style Guide
## small letters
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).
## Implicit generalization
We often use the implicit generalization feature of Coq, triggered by a backtic:
`` `{!term A B}`` means that an implicit argument of type `term A B` is added,
and if any of the identifiers that are used here is not yet bound, it gets added
as well. Usually, `term` will be some existing type class or similar, and we
use this syntax to also generalize over `A` and `B`; then the above is
equivalent to `{A B} {Hterm: term A B}`. The `!` in front of the term disables
an even stronger form of generalization, where if `term` is a type class then
all missing arguments get implicitly generalized as well. This is sometimes
useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C,
!Countable C}``. However, generally it is more important to be aware of the
assumptions you are making, so implicit generalization without `!` should be
avoided.
## Type class resolution control
When you are writing a module that exports some Iris term for others to use
(e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be
sure to mark these terms as opaque for type class search at the *end* of your
module (and outside any section):
```
Typeclasses Opaque join_handle.
```
This makes sure that the proof mode does not "look into" your definition when it
is used by clients.
## Naming conventions for variables/arguments/hypotheses
### small letters
* a : A = cmraT or cofeT
* b : B = cmraT or cofeT
......@@ -31,7 +65,7 @@
* y
* z
## capital letters
### capital letters
* A : Type, cmraT or cofeT
* B : Type, cmraT or cofeT
......@@ -61,20 +95,20 @@
* Y : sets
* Z : sets
## small greek letters
### small greek letters
* γ : gname
* σ : state = state of language
* φ : interpretation of STS/Auth
## capital greek letters
### capital greek letters
* Φ : general predicate (over uPred, iProp or Prop)
* Ψ : general predicate (over uPred, iProp or Prop)
# Naming conventions for algebraic classes in the Coq development
## Naming conventions for algebraic classes
## Suffixes
### Suffixes
* C: OFEs
* R: cameras
......
-Q theories iris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
# We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
# is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
theories/algebra/monoid.v
theories/algebra/cmra.v
theories/algebra/big_op.v
......@@ -41,7 +50,7 @@ theories/bi/monpred.v
theories/bi/embedding.v
theories/bi/weakestpre.v
theories/bi/telescopes.v
theories/bi/lib/counter_examples.v
theories/bi/lib/counterexamples.v
theories/bi/lib/fixpoint.v
theories/bi/lib/fractional.v
theories/bi/lib/laterable.v
......@@ -52,7 +61,7 @@ theories/base_logic/bi.v
theories/base_logic/derived.v
theories/base_logic/proofmode.v
theories/base_logic/base_logic.v
theories/base_logic/double_negation.v
theories/base_logic/bupd_alt.v
theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v
theories/base_logic/lib/saved_prop.v
......@@ -67,6 +76,7 @@ theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/gen_heap.v
theories/base_logic/lib/fancy_updates_from_vs.v
theories/base_logic/lib/proph_map.v
theories/program_logic/adequacy.v
theories/program_logic/lifting.v
theories/program_logic/weakestpre.v
......@@ -81,6 +91,7 @@ theories/program_logic/ownp.v
theories/program_logic/total_lifting.v
theories/program_logic/total_ectx_lifting.v
theories/program_logic/atomic.v
theories/heap_lang/locations.v
theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
......@@ -89,7 +100,6 @@ 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_map.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/assert.v
......
#!/usr/bin/python3
import sys, os
import requests
# A script to build Iris' reverse-dependencies (the one that usually get built every night against Iris master)
# against a branch of your choice.
# Set the GITLAB_TOKEN environment variable to a GitLab access token.
# Set at least one of IRIS_REV or STDPP_REV to control which branches of these projects to build against
# (default to `master`).
if not "GITLAB_TOKEN" in os.environ:
print("You need to set the GITLAB_TOKEN environment variable to a GitLab access token.")
print("You can create such tokens at <https://gitlab.mpi-sws.org/profile/personal_access_tokens>.")
print("Make sure you grant access to the 'api' scope.")
sys.exit(1)
GITLAB_TOKEN = os.environ["GITLAB_TOKEN"]
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'] },
{ 'name': 'iron', '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'])
json = {
'ref': project['branch'],
'variables': list(map(lambda var: { 'key': var, 'value': os.environ.get(var, "master") }, project['vars'])),
}
r = requests.post(url, headers={'PRIVATE-TOKEN': GITLAB_TOKEN}, json=json)
r.raise_for_status()
print(" Pipeline running at {}".format(r.json()['web_url']))
......@@ -17,6 +17,8 @@ This definition varies slightly from the original one in~\cite{catlogic}.
The key intuition behind OFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{ofe-mono})---and in the limit, it agrees with plain equality (\ruleref{ofe-limit}).
Notice that OFEs are just a different presentation of bisected 1-bounded ultrametric spaces, where the family of equivalence relations gives rise to the distance function (two elements that are equal for $n$ steps are no more than $2^{-n}$ apart).
\begin{defn}
An element $x \in \ofe$ of an OFE is called \emph{discrete} if
\[ \All y \in \ofe. x \nequiv{0} y \Ra x = y\]
......
......@@ -57,12 +57,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]
This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless propositions.
The following rules can be derived about except-0:
Except-0 satisfies the usual laws of a ``monadic'' modality (similar to, \eg the update modalities):
\begin{mathpar}
\inferH{ex0-mono}
{\prop \proves \propB}
......@@ -87,6 +82,28 @@ The following rules can be derived about except-0:
\diamond\later\prop &\proves& \later{\prop}
\end{array}
\end{mathpar}
In particular, from \ruleref{ex0-mono} and \ruleref{ex0-idem} we can derive a ``bind''-like elimination rule:
\begin{mathpar}
\inferH{ex0-elim}
{\prop \proves \diamond\propB}
{\diamond\prop \proves \diamond\propB}
\end{mathpar}
This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
In other words, when working below the except-0 modality, we can \emph{strip
away} the later from timeless propositions (using \ruleref{ex0-elim}):
\begin{mathpar}
\inferH{ex0-timeless-strip}{\timeless{\prop} \and \prop \proves \diamond\propB}
{\later\prop \proves \diamond\propB}
\end{mathpar}
In fact, it turns out that we can strip away later from timeless propositions even when working under the later modality:
\begin{mathpar}
\inferH{later-timeless-strip}{\timeless{\prop} \and \prop \proves \later \propB}
{\later\prop \proves \later\propB}
\end{mathpar}
This follows from $\later \prop \proves \later\FALSE \lor \prop$, and then by straightforward disjunction elimination.
The following rules identify the class of timeless propositions:
\begin{mathparpagebreakable}
......
......@@ -398,7 +398,7 @@
\newcommand{\cfg}[2]{{#1};{#2}}
\def\fill#1[#2]{#1 {[}\, #2\,{]} }
\def\fillctx#1[#2]{#1 {[}\, #2\,{]} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% STANDARD DERIVED CONSTRUCTIONS
......
......@@ -28,7 +28,7 @@
\begin{abstract}
This document describes formally the Iris program logic.
Every result in this document has been fully verified in Coq.
The latest versions of this document and the Coq formalization can be found in the git repository at \url{https://gitlab.mpi-sws.org/FP/iris-coq/}.
The latest versions of this document and the Coq formalization can be found in the git repository at \url{https://gitlab.mpi-sws.org/iris/iris}.
For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
\end{abstract}
......
opam-version: "1.2"
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/FP/iris-coq/issues"
bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
license: "BSD"
dev-repo: "https://gitlab.mpi-sws.org/FP/iris-coq.git"
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"]
depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-12-12.0.9cbafb67") | (= "dev") }
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-05-30.0.84fd0660") | (= "dev") }
]
From iris.base_logic.lib Require Import invariants.
Instance test_cofe {Σ} : Cofe (iPreProp Σ) := _.
Section tests.
Context `{invG Σ}.
Context `{!invG Σ}.
Program Definition test : (iProp Σ -n> iProp Σ) -n> (iProp Σ -n> iProp Σ) :=
λne P v, ( (P v))%I.
......
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 }}
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
......@@ -10,11 +24,9 @@
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -23,14 +35,12 @@
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >>
<< ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -46,11 +56,9 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -59,14 +67,11 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >>
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
......@@ -82,11 +87,9 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}