README.md 3.25 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2 3 4 5 6 7 8 9 10
# THIS PROJECT HAS MOVED TO
<https://gitlab.mpi-sws.org/iris/reloc>


The code here remains for historical reasons
.
.
.
.

Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14
# Prerequisites

This version is known to compile with:

Ralf Jung's avatar
Ralf Jung committed
15
 - Coq 8.7.2
16
 - Ssreflect 1.6.4
Ralf Jung's avatar
Ralf Jung committed
17
 - Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
Dan Frumin's avatar
Dan Frumin committed
18
 - std++ version [32570aa6e0d04633047d9fddb3cf8da1748d9695](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/32570aa6e0d04633047d9fddb3cf8da1748d9695)
Dan Frumin's avatar
Dan Frumin committed
19
 - Iris version [7e33a806f2cd8da0409f1e5a13126317afd23e3d](https://gitlab.mpi-sws.org/FP/iris-coq/tree/7e33a806f2cd8da0409f1e5a13126317afd23e3d)
20 21 22

# Compilation

Dan Frumin's avatar
Dan Frumin committed
23
Make sure that all the dependencies are installed and run `make`.
24 25 26 27 28 29

# Documentation

See [refman.md](docs/refman.md).

Work in progress.
30 31 32 33 34

# Structure

- `logrel.v` - exports all the modules required to perform refinement proofs such as those in the `example/` folder
- `F_mu_ref_conc` - definition of the object language
35 36 37 38 39 40 41 42 43 44
  + `binder.v` - auxiliary lemmas/instances for binders
  + `lang.v` - definition of the object language with operational semantics
  + `subst.v` - parallel substitution
  + `notation.v` - useful Coq notation for the language
  + `typing.v` - the type system
  + `reflection.v` - a refined version of the target language for proving certain properties by computation
  + `rules.v` - WP calculus
  + `adequacy.v` - soundness of the WP rules
  + `context_refinement.v` - definition of contextual refinement
  + `pureexec.v`, `tactics.v` - instances and tactics for doing symbolic execution
45
- `examples` - example refinements
46 47 48 49 50 51 52
  + `bit.v` - "representation independence example" for a simple bit interface
  + `par.v` - compatibility lemma for parallel composition
  + `or.v` - expressing non-determinism with concurrency
  + `counter.v` - fine-grained concurrent counter refines coarse-grained concurrent counter
  + `stack/module_refinement.v`, `stack/refinement.v` - Treiber stack refines sequential stack
  + `stack/helping.v` - stack with helping refines sequential stack
  + `various.v` - some examples with higher-order functions with local state, in the style of "The effects of higher-order state and control on local relational reasoning" paper
Dan Frumin's avatar
Dan Frumin committed
53
  + `symbol.v` and `generative.v` - generative ADTs examples from the "State-Dependent Representational Independence" paper
54 55 56 57 58 59 60 61 62 63
- `logrel` contains modules related to the relational interpretation
  + `threadpool.v` - definitions for the ghost threadpool RA
  + `rules_threadpool.v` - symbolic execution in the threadpool
  + `proofmode/tactics_threadpool.v` - tactics for preforming symbolic execution in the threadpool
  + `semtypes.v` - interpretation of types/semantics in terms of values
  + `logrel_binary.v` - interpretation of sequents/semantics in terms of open expressions
  + `rules.v` - symbolic execution rules for the relational interpretation
  + `proofmode/tactics_rel.v` - tactics for performing symbolic execution in the relational interpretation
  + `fundamental_binary.v` - compatibility lemmas and the fundamental theorem of logical relations
  + `contextual_refinement.v` - proof that logical relations are closed under contextual refinement
64
  + `soundness_binary.v` - type safety and contextual refinement proofs for terms in the relational interpretation  
65
- `prelude` - some files shares by the whole development