README.md 3.13 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4
# Prerequisites

This version is known to compile with:

5
 - Coq 8.6.1
Robbert Krebbers's avatar
Robbert Krebbers committed
6
 - Ssreflect 1.6
7
 - Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
Dan Frumin's avatar
Dan Frumin committed
8 9
 - std++ version [32570aa6e0d04633047d9fddb3cf8da1748d9695](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/32570aa6e0d04633047d9fddb3cf8da1748d9695)
 - Iris version [6117c3e4a57307fd374780836a130ac86608d8cd](https://gitlab.mpi-sws.org/FP/iris-coq/tree/6117c3e4a57307fd374780836a130ac86608d8cd)
10 11 12

# Compilation

Dan Frumin's avatar
Dan Frumin committed
13
Make sure that all the dependencies are installed and run `make`.
14 15 16 17 18 19

# Documentation

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

Work in progress.
20 21 22 23 24

# 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
25 26 27 28 29 30 31 32 33 34
  + `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
35
- `examples` - example refinements
36 37 38 39 40 41 42
  + `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
43
  + `symbol.v` and `generative.v` - generative ADTs examples from the "State-Dependent Representational Independence" paper
44 45 46 47 48 49 50 51 52 53
- `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
54
  + `soundness_binary.v` - type safety and contextual refinement proofs for terms in the relational interpretation  
55
- `prelude` - some files shares by the whole development