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 tex/iris.tex. A compiled PDF version of this document is available online.

Side-effects

Importing Iris has some side effects as the library sets some global options.

• First of all, Iris imports std++, so the std++ side-effects apply.
• On top of that, Iris imports ssreflect, which replaces the default rewrite tactic with the ssreflect version. However, done is overwritten to keep using the std++ version of the tactic. We also set SsrOldRewriteGoalsOrder and re-open general_if_scope to un-do some effects of ssreflect.

Building Iris

Prerequisites

This version is known to compile with:

• Coq 8.10.2 / 8.11.2 / 8.12.0
• A development version of std++

If you need to work with Coq 8.7 or Coq 8.8, please check out the iris-3.2 branch. For Coq 8.9, you can use the iris-3.3 branch.

Working with Iris

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:

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.

The development version of Iris is regularly subject to breaking changes. If you want to be notified of such changes, please let us know your account name on the MPI-SWS GitLab so we can add you to the notification group.

Working on Iris

To work on Iris itself, you need to install its build-dependencies. Again we 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
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 proof_mode.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.
• The folder si_logic defines a "plain" step-indexed logic and shows that it is an instance of the BI interface.

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).
• Actris is a separation logic built on top of Iris for session-type based reasoning of message-passing programs.

Further Resources

Getting along with Iris in Coq:

• Iris proof patterns and conventions are documented in the proof 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 have trouble joining the chat, please contact Ralf.
• 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.