README.md 2.2 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6 7 8
# IRIS EXAMPLES

Some example verification demonstrating the use of Iris.

## Prerequisites

This version is known to compile with:

9
 - Coq 8.6.1 / 8.7.0
Ralf Jung's avatar
Ralf Jung committed
10
 - Ssreflect 1.6.4
Ralf Jung's avatar
Ralf Jung committed
11
 - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
Ralf Jung's avatar
Ralf Jung committed
12
 - The coq86-devel branch of [Autosubst](https://github.com/uds-psl/autosubst)
Ralf Jung's avatar
Ralf Jung committed
13 14

The easiest way to install the correct versions of the dependencies is through
Ralf Jung's avatar
Ralf Jung committed
15
opam.  You will need the Coq and Iris opam repositories:
Ralf Jung's avatar
Ralf Jung committed
16

Ralf Jung's avatar
Ralf Jung committed
17 18 19 20 21
    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.
Ralf Jung's avatar
Ralf Jung committed
22

Ralf Jung's avatar
Ralf Jung committed
23
## Building
Ralf Jung's avatar
Ralf Jung committed
24 25 26

Run `make` to build the full development.

Ralf Jung's avatar
Ralf Jung committed
27 28 29 30
## Case Studies

This repository contains the following case studies:

Ralf Jung's avatar
Ralf Jung committed
31 32 33 34
* [barrier](theories/barrier): Implementation and proof of a barrier as
  described in ["Higher-Order Ghost State"](http://doi.acm.org/10.1145/2818638).
* [logrel](theories/logrel): Logical relations from the
  [IPM paper](http://doi.acm.org/10.1145/3093333.3009855):
Ralf Jung's avatar
no tabs  
Ralf Jung committed
35 36 37 38 39 40 41 42 43 44 45 46
  - 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
Ralf Jung's avatar
Ralf Jung committed
47

Ralf Jung's avatar
Ralf Jung committed
48 49
## For Developers: How to update the Iris dependency

Ralf Jung's avatar
Ralf Jung committed
50 51 52 53 54 55
* 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 do `make clean` as Coq will likely complain about .vo file
Ralf Jung's avatar
Ralf Jung committed
56
  mismatches.