README.md 5.67 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
    opam install coqide.8.8.2
37 38 39 40 41

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

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

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

49 50 51 52 53
### 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
54
    opam pin add coq-tlc -k version 20181116
55

56 57 58 59 60 61
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

62
## Compiling
63

64 65
To compile the Coq scripts:

66
    make -j4
67 68 69 70 71 72 73

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

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

    ./make_archive.sh

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

## Index of modules

84 85
Important modules are highlighted.

86 87 88
 *  `Misc`: some basic things
 *  `Auth_nat`, `Auth_mnat`: simple lemmas about the authoritative resources on
    (ℕ, +) and (ℕ, max)
Glen Mével's avatar
Glen Mével committed
89
 *  `heap_lang/` directory: the toy language under study
90
 *  `Reduction`: generic lemmas about reduction, safety, closedness, fresh
Glen Mével's avatar
Glen Mével committed
91
    locations…
92 93 94 95 96 97
 *  `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
Glen Mével's avatar
Glen Mével committed
98 99 100
    credits (plus proof-mode tactics `wp_tick_*`)__
 *  __`TimeCreditsAltProofs`: alternative proofs for the soundness theorem of
    time credits__
101
 *  __`TimeReceipts`: interface, implementation, and proof of soundness for time
Glen Mével's avatar
Glen Mével committed
102
    receipts, both exclusive and persistent (plus proof-mode tactics)__
Glen Mével's avatar
Glen Mével committed
103 104
 *  __`Combined`: logical system providing both time credits and time receipts
    at the same time__
105 106 107
 *  `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__
Glen Mével's avatar
Glen Mével committed
108 109 110 111
 *  __`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__
112

Glen Mével's avatar
Glen Mével committed
113
### From ESOP paper to Coq proofs
114 115 116 117

#### Generic translation and “tick”

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

In `Simulation.v`:

Glen Mével's avatar
Glen Mével committed
122 123 124 125
 *  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
126 127 128 129 130 131 132
    programs, but also their _adequacy_ with respect to some formula φ; this is
    not a difficult property to transfer anyway).

#### Time credits

In `TimeCredits.v`:

Glen Mével's avatar
Glen Mével committed
133 134 135 136 137 138
 *  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
139
    the Coq development, but corresponds roughly to a portion of the proof of
Glen Mével's avatar
Glen Mével committed
140 141 142
    `spec_tctranslation__adequate_translation`. The fact that our implementation
    matches the interface is stated by `TC_implementation`.
 *  Theorem 1 (“Soundness of Iris^$ ”) is
143 144 145 146 147 148
    `abstract_spec_tctranslation__adequate_and_bounded`.

#### Time receipts

In `TimeReceipts.v`:

Glen Mével's avatar
Glen Mével committed
149 150 151 152 153 154 155
 *  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`.

Glen Mével's avatar
Glen Mével committed
156
#### Marrying time credits and time receipts
Glen Mével's avatar
Glen Mével committed
157 158 159 160

In `Combined.v`:

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