README.md 5.74 KB
Newer Older
1
## Requirements
2

3
The project is known to compile with:
4
 *  Coq 8.8.2
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
5
 *  coq-iris dev.2018-11-01.3.19aae59a (development version of Iris)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
6
 *  coq-tlc 20181116 (for the proof of union-find)
7

8 9 10
As those dependencies (especially Iris) often make breaking changes,
compatibility with other versions is not guaranteed.

11 12
### Step 1: Install opam

13
_If opam is not already installed:_ See instructions [there][install-opam] to
14
install it; then:
15 16

    opam init --comp=4.06.1
17
    eval $(opam config env)
18 19 20

(This will create a `~/.opam` directory.)

21 22
_If opam is already installed:_ Create a new switch for the project:

23 24
    opam switch iris-time-proofs --alias-of 4.06.1 # for opam 1.x
    opam switch create iris-time-proofs 4.06.1     # for opam 2.x
25
    eval $(opam config env)
26

27 28 29 30
### Step 2: Install Coq

    opam repo add coq-released https://coq.inria.fr/opam/released
    opam update
31
    opam install -j4 -v coq.8.8.2
32 33 34

If you want to use CoqIDE (a graphical, interactive toplevel for Coq), install
it as well:
35

36
    # NOTE: this version of CoqIDE is only available if using opam 2.x
37
    opam install coqide.8.8.2
38 39 40 41 42

### Step 3: Install a development version of Iris

    opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
    opam update
MEVEL Glen's avatar
MEVEL Glen committed
43
    opam pin add coq-iris -k version dev.2018-11-01.3.19aae59a
44 45 46 47 48 49

(This will also install `coq-stdpp`, another Coq library made available through
the same repo.)

More info on the Coq development of Iris: [there][coq-iris].

50 51 52 53 54
### Step 4: Install TLC

The TLC library is required by the proof of the union-find algorithm. It is
available through an opam package in the Coq repository (added earlier).

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
55
    opam pin add coq-tlc -k version 20181116
56

57 58 59 60 61 62
Alternatively, TLC can be installed from source:

    git clone 'https://gitlab.inria.fr/charguer/tlc'
    ( cd tlc && git checkout a7c9f61 )
    opam pin add coq-tlc -k path ./tlc

63
## Compiling
64

65 66
To compile the Coq scripts:

67
    make -j4
68 69 70 71 72 73 74

The first time (and each time `_CoqProject` is updated), it also creates the
file `Makefile.coq`.

Other recipes are available, such as `all`, `clean` and `userinstall` (Makefile
taken from [here][coqproject]).

75 76 77 78
To create an archive of the project:

    ./make_archive.sh

79 80
[install-opam]: https://opam.ocaml.org/doc/Install.html
[coq-iris]: https://gitlab.mpi-sws.org/FP/iris-coq
81 82 83 84
[coqproject]: https://blog.zhenzhang.me/2016/09/19/coq-dev.html

## Index of modules

85 86
Important modules are highlighted.

87 88 89
 *  `Misc`: some basic things
 *  `Auth_nat`, `Auth_mnat`: simple lemmas about the authoritative resources on
    (ℕ, +) and (ℕ, max)
MEVEL Glen's avatar
MEVEL Glen committed
90
 *  `heap_lang/` directory: the toy language under study
91
 *  `Reduction`: generic lemmas about reduction, safety, closedness, fresh
MEVEL Glen's avatar
MEVEL Glen committed
92
    locations…
93 94 95 96 97 98
 *  `Tactics`: helper tactics to reduce concrete terms
 *  __`Translation`: definition of the translation and syntactic lemmas about
    it__
 *  __`Simulation`: generic definition of `tick`; operational lemmas about the
    translation with that `tick`__
 *  __`TimeCredits`: interface, implementation, and proof of soundness for time
MEVEL Glen's avatar
MEVEL Glen committed
99 100 101
    credits (plus proof-mode tactics `wp_tick_*`)__
 *  __`TimeCreditsAltProofs`: alternative proofs for the soundness theorem of
    time credits__
102
 *  __`TimeReceipts`: interface, implementation, and proof of soundness for time
MEVEL Glen's avatar
MEVEL Glen committed
103
    receipts, both exclusive and persistent (plus proof-mode tactics)__
MEVEL Glen's avatar
MEVEL Glen committed
104 105
 *  __`Combined`: logical system providing both time credits and time receipts
    at the same time__
106 107 108
 *  `Examples`: a very simple example illustrating the use of time credits to
    specify a program with lists
 *  __`Thunks`: implementation of timed thunks using time credits__
MEVEL Glen's avatar
MEVEL Glen committed
109 110 111 112
 *  __`ClockIntegers`: reconstruction of Clochard’s integer types (`onetime` and
    `peano`) using time receipts__
 *  __`union_find/` directory: application of the combined system to a
    union-find program__
113

MEVEL Glen's avatar
MEVEL Glen committed
114
### From ESOP paper to Coq proofs
115 116 117 118

#### Generic translation and “tick”

The basic properties of the translation are proven in `Translation.v` (for
119
example, `translation_subst`).
120 121 122

In `Simulation.v`:

MEVEL Glen's avatar
MEVEL Glen committed
123 124 125 126
 *  Lemma 1 (“Reduction Preservation”) is `simulation_exec_success`.
 *  Lemma 2 (“Immediate Safety Preservation”) is `safe_translation__safe_here`.
 *  Lemma 3 (“Safety Preservation”) is `adequate_translation__nadequate` (in the
    Coq development, by contrast with the paper, not only do we prove safety of
127 128 129 130 131 132 133
    programs, but also their _adequacy_ with respect to some formula φ; this is
    not a difficult property to transfer anyway).

#### Time credits

In `TimeCredits.v`:

MEVEL Glen's avatar
MEVEL Glen committed
134 135 136 137 138 139
 *  Lemma 4 (“Credit Exhaustion”) is `simulation_step_failure`.
 *  Lemma 5 (“Safety Preservation, Strengthened”) is presented in
    `TimeCreditsAltProofs.v`, as `adequate_tctranslation__nadequate`; the main
    development in `TimeCredits.v` uses a slightly weaker version, named
    `adequate_tctranslation__adequate_and_bounded`.
 *  Lemma 6 (“Time Credit Initialization”) does not have an exact counterpart in
140
    the Coq development, but corresponds roughly to a portion of the proof of
MEVEL Glen's avatar
MEVEL Glen committed
141 142 143
    `spec_tctranslation__adequate_translation`. The fact that our implementation
    matches the interface is stated by `TC_implementation`.
 *  Theorem 1 (“Soundness of Iris^$ ”) is
144 145 146 147 148 149
    `abstract_spec_tctranslation__adequate_and_bounded`.

#### Time receipts

In `TimeReceipts.v`:

MEVEL Glen's avatar
MEVEL Glen committed
150 151 152 153 154 155 156
 *  Lemma 7 (“Time Receipt Initialization”) lemma does not have an exact
    counterpart in the Coq development, but corresponds roughly to a portion of
    the proof of `spec_trtranslation__adequate_translation`. The fact that our
    implementation matches the interface is stated by `TR_implementation`.
 *  Theorem 2 (“Soundness of Iris^⧗ ”) is
    `abstract_spec_trtranslation__adequate`.

MEVEL Glen's avatar
MEVEL Glen committed
157
#### Marrying time credits and time receipts
MEVEL Glen's avatar
MEVEL Glen committed
158 159 160 161

In `Combined.v`:

 *  Theorem 3 (“Soundness of Iris^$⧗ ”) is `tctr_sound_abstract`.