Commit 5759fc5b authored by Glen Mével's avatar Glen Mével

Update README

parent e19aa532
...@@ -36,7 +36,7 @@ support it. ...@@ -36,7 +36,7 @@ support it.
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
opam update opam update
opam pin add coq-iris -k version dev.2018-10-13.0.7041c043 opam pin add coq-iris -k version dev.2018-11-01.3.19aae59a
(This will also install `coq-stdpp`, another Coq library made available through (This will also install `coq-stdpp`, another Coq library made available through
the same repo.) the same repo.)
...@@ -49,8 +49,7 @@ The TLC library is required by the proof of the union-find algorithm. It is ...@@ -49,8 +49,7 @@ 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). available through an opam package in the Coq repository (added earlier).
opam install coq-tlc opam install coq-tlc
opam pin add coq-tlc -k version 20180316
TODO: version?
## Compiling ## Compiling
...@@ -79,28 +78,31 @@ Important modules are highlighted. ...@@ -79,28 +78,31 @@ Important modules are highlighted.
* `Misc`: some basic things * `Misc`: some basic things
* `Auth_nat`, `Auth_mnat`: simple lemmas about the authoritative resources on * `Auth_nat`, `Auth_mnat`: simple lemmas about the authoritative resources on
(ℕ, +) and (ℕ, max) (ℕ, +) and (ℕ, max)
* `heap_lang/` directory: the toy language under study
* `Reduction`: generic lemmas about reduction, safety, closedness, fresh * `Reduction`: generic lemmas about reduction, safety, closedness, fresh
locations… [should be renamed or split into several files] locations…
* `Tactics`: helper tactics to reduce concrete terms * `Tactics`: helper tactics to reduce concrete terms
* __`Translation`: definition of the translation and syntactic lemmas about * __`Translation`: definition of the translation and syntactic lemmas about
it__ it__
* __`Simulation`: generic definition of `tick`; operational lemmas about the * __`Simulation`: generic definition of `tick`; operational lemmas about the
translation with that `tick`__ translation with that `tick`__
* __`TimeCredits`: interface, implementation, and proof of soundness for time * __`TimeCredits`: interface, implementation, and proof of soundness for time
credits (plus a proof-mode tactic `wp_tick`)__ credits (plus proof-mode tactics `wp_tick_*`)__
* __`TimeCreditsAltProofs`: alternative proofs of the soundness theorem of * __`TimeCreditsAltProofs`: alternative proofs for the soundness theorem of
time credits, that does not rely on the unsafe behavior of `tick`__ time credits__
* __`TimeReceipts`: interface, implementation, and proof of soundness for time * __`TimeReceipts`: interface, implementation, and proof of soundness for time
receipts (both exclusive and persistent)__ receipts, both exclusive and persistent (plus proof-mode tactics)__
* __`Combined`: logical system providing both time credits and time receipts * __`Combined`: logical system providing both time credits and time receipts
at the same time__ at the same time__
* `Examples`: a very simple example illustrating the use of time credits to * `Examples`: a very simple example illustrating the use of time credits to
specify a program with lists specify a program with lists
* __`Thunks`: implementation of timed thunks using time credits__ * __`Thunks`: implementation of timed thunks using time credits__
* __`ClockedIntegers`: reconstruction of Clochard’s integer types (`onetime` * __`ClockIntegers`: reconstruction of Clochard’s integer types (`onetime` and
and `peano`) using time receipts__ `peano`) using time receipts__
* __`union_find/` directory: application of the combined system to a
union-find program__
### From the paper to the Coq code ### From ESOP paper to the Coq code
#### Generic translation and “tick” #### Generic translation and “tick”
...@@ -109,13 +111,10 @@ example, `translation_subst`). ...@@ -109,13 +111,10 @@ example, `translation_subst`).
In `Simulation.v`: In `Simulation.v`:
* The operational semantics of “tick” in the nonzero case is given by lemma * Lemma 1 (“Reduction Preservation”) is `simulation_exec_success`.
`exec_tick_success`. * Lemma 2 (“Immediate Safety Preservation”) is `safe_translation__safe_here`.
* The “Forward Simulation” lemma is `simulation_exec_success`. * Lemma 3 (“Safety Preservation”) is `adequate_translation__nadequate` (in the
* The “Forward Simulation of Unsafe Behaviors” lemma corresponds roughly to Coq development, by contrast with the paper, not only do we prove safety of
`safe_translation__safe_here`.
* The “Safety Transfer” lemma is `adequate_translation__adequate` (in the Coq
development, by contrast with the paper, not only do we prove safety of
programs, but also their _adequacy_ with respect to some formula φ; this is programs, but also their _adequacy_ with respect to some formula φ; this is
not a difficult property to transfer anyway). not a difficult property to transfer anyway).
...@@ -123,23 +122,31 @@ In `Simulation.v`: ...@@ -123,23 +122,31 @@ In `Simulation.v`:
In `TimeCredits.v`: In `TimeCredits.v`:
* The “Credit Exhaustion” lemma is `simulation_exec_failure_now`. * Lemma 4 (“Credit Exhaustion”) is `simulation_step_failure`.
* The “Soundness of the Time Credit Translation” lemma is * Lemma 5 (“Safety Preservation, Strengthened”) is presented in
`simulation_exec_failure`. `TimeCreditsAltProofs.v`, as `adequate_tctranslation__nadequate`; the main
* The “Time Credit Initialization” lemma does not have an exact counterpart in 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
the Coq development, but corresponds roughly to a portion of the proof of the Coq development, but corresponds roughly to a portion of the proof of
`spec_tctranslation__adequate`. The fact that our implementation matches the `spec_tctranslation__adequate_translation`. The fact that our implementation
interface is stated by `TC_implementation`. matches the interface is stated by `TC_implementation`.
* The “Soundness of Iris^$ ” lemma is * Theorem 1 (“Soundness of Iris^$ ”) is
`abstract_spec_tctranslation__adequate_and_bounded`. `abstract_spec_tctranslation__adequate_and_bounded`.
#### Time receipts #### Time receipts
In `TimeReceipts.v`: In `TimeReceipts.v`:
* The “Time Receipt Initialization” lemma does not have an exact counterpart * Lemma 7 (“Time Receipt Initialization”) lemma does not have an exact
in the Coq development, but corresponds roughly to a portion of the proof of counterpart in the Coq development, but corresponds roughly to a portion of
`spec_trtranslation__adequate_translation`. The fact that our implementation the proof of `spec_trtranslation__adequate_translation`. The fact that our
matches the interface is stated by `TR_implementation`. implementation matches the interface is stated by `TR_implementation`.
* The “Credit Exhaustion” lemma is `simulation_exec_failure_now`. * Theorem 2 (“Soundness of Iris^⧗ ”) is
* The “Soundness of Iris^⧗ ” lemma is `abstract_spec_trtranslation__adequate`. `abstract_spec_trtranslation__adequate`.
### Marrying time credits and time receipts
In `Combined.v`:
* Theorem 3 (“Soundness of Iris^$⧗ ”) is `tctr_sound_abstract`.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment