# IRIS COQ DEVELOPMENT

This is the Coq development of the Iris Project.

## Prerequisites

This version is known to compile with:

- Coq 8.5pl3 / 8.6
- Ssreflect 1.6.1

The easiest way to install the correct versions of the dependencies is through
opam. Once you got opam set up, just run `make build-dep`

to install the right
versions of the dependencies. When the dependencies change, just run ```
make
build-dep
```

again.

## Building Instructions

Run `make`

to build the full development.

## Structure

- The folder prelude contains an extended "Standard Library" by Robbert Krebbers.
- 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 proofmode contains the Iris proof mode, which extends Coq with contexts for persistent and spatial Iris assertions. It also contains tactics for interactive proofs in Iris. 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. Most notable here is lib/barrier, the implementation and proof of a barrier as described in http://doi.acm.org/10.1145/2818638.

- 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.

## Documentation

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.