IRIS EXAMPLES
Some example verification demonstrating the use of Iris.
Prerequisites
This version is known to compile with:
Building from source
When building from source, we recommend to use opam (1.2.2 or newer) for installing the dependencies. 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
Once you got opam set up, run make build-dep
to install the right versions
of the dependencies.
Run make -jN
to build the full development, where N
is the number of your
CPU cores.
To update, do git pull
. After an update, the development may fail to compile
because of outdated dependencies. To fix that, please run opam update
followed by make build-dep
.
Case Studies
This repository contains the following case studies:
- barrier: Implementation and proof of a barrier as described in "Higher-Order Ghost State".
-
logrel: Logical relations from the
IPM paper:
- STLC
- Unary logical relations proving type safety
- F_mu (System F with recursive types)
- Unary logical relations proving type safety
- F_mu_ref (System F with recursive types and references)
- Unary logical relations proving type safety
- Binary logical relations for proving contextual refinements
- F_mu_ref_conc (System F with recursive types, references and concurrency)
- Unary logical relations proving type safety
- Binary logical relations for proving contextual refinements
- Proof of refinement for a pair of fine-grained/coarse-grained concurrent counter implementations
- Proof of refinement for a pair of fine-grained/coarse-grained concurrent stack implementations
- STLC
- logrel_heaplang: A unary logical relation for semantic typing of heap lang.
-
logatom: Proofs of various logically atomic specifications:
- Elimination Stack
- Treiber Stack (by Zhen Zhang)
- Flat Combiner (by Zhen Zhang, also see this archived documentation)
- spanning-tree: Proof of a concurrent spanning tree algorithm by Amin Timany.
- concurrent-stacks: Proof of an implementation of concurrent stacks with helping by Daniel Gratzer et. al., as described in the report.
- lecture-notes: Coq examples for the Iris lecture notes.
- hocap: Formalisations of the concurrent bag and concurrent runners libraries from the HOCAP paper. See the associated README.
For Developers: How to update the Iris dependency
- Do the change in Iris, push it.
- Wait for CI to publish a new Iris version on the opam archive, then run
opam update iris-dev
. - In iris-examples, change the
opam
file to depend on the new version. - Run
make build-dep
(in iris-examples) to install the new version of Iris. You may have to domake clean
as Coq will likely complain about .vo file mismatches.