IRIS COQ DEVELOPMENT coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)

This is the Coq development of the Iris Project, which includes MoSeL, a general proof mode for carrying out separation logic proofs in Coq.

For using the Coq library, check out the API documentation.

For understanding the theory of Iris, a LaTeX version of the core logic definitions and some derived forms is available in docs/iris.tex. A compiled PDF version of this document is available online.

Building Iris

Prerequisites

This version is known to compile with:

• Coq 8.7.1 / 8.7.2 / 8.8.0 / 8.8.2 / 8.9.0
• A development version of std++

For a version compatible with Coq 8.6, have a look at the iris-3.1 branch. If you need to work with Coq 8.5, please check out the iris-3.0 branch.

Working with Iris

To use Iris in your own proofs, we recommend you install Iris via opam (1.2.2 or newer). To obtain the latest stable release, you have to add the Coq opam repository:

opam repo add coq-released https://coq.inria.fr/opam/released

To obtain a development version, also add the Iris opam repository:

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 backwards-compatibility, so upgrading Iris may break your Iris-using 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 two repositories:

opam repo add coq-released https://coq.inria.fr/opam/released
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.

Run make -jN to build the full development, where N is the number of your CPU cores.

To update Iris, 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.

Directory Structure

• The folder algebra contains the COFE and CMRA constructions as well as the solver for recursive domain equations.
• The folder base_logic defines the Iris base logic and the primitive connectives. It also contains derived constructions that are entirely independent of the choice of resources.
  • The subfolder lib contains some generally useful derived constructions. Most importantly, it defines composeable dynamic resources and ownership of them; the other constructions depend on this setup.
• The folder program_logic specializes the base logic to build Iris, the program logic. This includes weakest preconditions that are defined for any language satisfying some generic axioms, and some derived constructions that work for any such language.
• The folder bi contains the BI++ laws, as well as derived connectives, laws and constructions that are applicable for general BIS.
• The folder proofmode contains 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.
• The folder heap_lang defines the ML-like concurrent heap language
  • The subfolder 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.
• The folder 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.

Case Studies

The following is a (probably incomplete) list of case studies that use Iris, and that should be compatible with this version:

• Iris Examples is where we collect miscellaneous case studies that do not have their own repository.
• LambdaRust is a Coq formalization of the core Rust type system.
• GPFSL is a logic for release-acquire and relaxed memory.
• 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.
• Syntactic conventions are described in the style guide.
• The Iris tactics are described in the the Iris Proof Mode (IPM) / MoSeL documentation as well as the HeapLang documentation.
• The generated coqdoc is available online.

Contacting the developers:

• Discussion about the Iris Coq development happens on the mailing list iris-club@lists.mpi-sws.org and in the Iris Chat. This is also the right place to ask questions. The chat requires an account at the MPI-SWS GitLab (use the "Register" tab).
• If you want to report a bug, please use the issue tracker, which also requires an MPI-SWS GitLab account.
• To contribute to Iris itself, see the contribution guide.

Miscellaneous:

• Information on how to set up your editor for unicode input and output is collected in Editor.md.
• If you are writing a paper that uses Iris in one way or another, you could use the Iris LaTeX macros for typesetting the various Iris connectives.