From 5759fc5bab6ab0d54b597c645f31b15ce65a5625 Mon Sep 17 00:00:00 2001
From: =?UTF8?q?Glen=20M=C3=A9vel?=
Date: Fri, 16 Nov 2018 09:39:34 +0100
Subject: [PATCH] Update README

README.md  69 ++++++++++++++++++++++++++++++
1 file changed, 38 insertions(+), 31 deletions()
diff git a/README.md b/README.md
index e9c4909..e5f33d0 100644
 a/README.md
+++ b/README.md
@@ 36,7 +36,7 @@ support it.
opam repo add irisdev https://gitlab.mpisws.org/FP/opamdev.git
opam update
 opam pin add coqiris k version dev.20181013.0.7041c043
+ opam pin add coqiris k version dev.20181101.3.19aae59a
(This will also install `coqstdpp`, another Coq library made available through
the same repo.)
@@ 49,8 +49,7 @@ The TLC library is required by the proof of the unionfind algorithm. It is
available through an opam package in the Coq repository (added earlier).
opam install coqtlc

TODO: version?
+ opam pin add coqtlc k version 20180316
## Compiling
@@ 79,28 +78,31 @@ Important modules are highlighted.
* `Misc`: some basic things
* `Auth_nat`, `Auth_mnat`: simple lemmas about the authoritative resources on
(ℕ, +) and (ℕ, max)
+ * `heap_lang/` directory: the toy language under study
* `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
* __`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
 credits (plus a proofmode tactic `wp_tick`)__
 * __`TimeCreditsAltProofs`: alternative proofs of the soundness theorem of
 time credits, that does not rely on the unsafe behavior of `tick`__
+ credits (plus proofmode tactics `wp_tick_*`)__
+ * __`TimeCreditsAltProofs`: alternative proofs for the soundness theorem of
+ time credits__
* __`TimeReceipts`: interface, implementation, and proof of soundness for time
 receipts (both exclusive and persistent)__
+ receipts, both exclusive and persistent (plus proofmode tactics)__
* __`Combined`: logical system providing both time credits and time receipts
at the same time__
* `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__
 * __`ClockedIntegers`: reconstruction of Clochard’s integer types (`onetime`
 and `peano`) using time receipts__
+ * __`ClockIntegers`: reconstruction of Clochard’s integer types (`onetime` and
+ `peano`) using time receipts__
+ * __`union_find/` directory: application of the combined system to a
+ unionfind program__
### From the paper to the Coq code
+### From ESOP paper to the Coq code
#### Generic translation and “tick”
@@ 109,13 +111,10 @@ example, `translation_subst`).
In `Simulation.v`:
 * The operational semantics of “tick” in the nonzero case is given by lemma
 `exec_tick_success`.
 * The “Forward Simulation” lemma is `simulation_exec_success`.
 * The “Forward Simulation of Unsafe Behaviors” lemma corresponds roughly to
 `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
+ * 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
programs, but also their _adequacy_ with respect to some formula φ; this is
not a difficult property to transfer anyway).
@@ 123,23 +122,31 @@ In `Simulation.v`:
In `TimeCredits.v`:
 * The “Credit Exhaustion” lemma is `simulation_exec_failure_now`.
 * The “Soundness of the Time Credit Translation” lemma is
 `simulation_exec_failure`.
 * The “Time Credit Initialization” lemma does not have an exact counterpart in
+ * 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
the Coq development, but corresponds roughly to a portion of the proof of
 `spec_tctranslation__adequate`. The fact that our implementation matches the
 interface is stated by `TC_implementation`.
 * The “Soundness of Iris^$ ” lemma is
+ `spec_tctranslation__adequate_translation`. The fact that our implementation
+ matches the interface is stated by `TC_implementation`.
+ * Theorem 1 (“Soundness of Iris^$ ”) is
`abstract_spec_tctranslation__adequate_and_bounded`.
#### Time receipts
In `TimeReceipts.v`:
 * The “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`.
 * The “Credit Exhaustion” lemma is `simulation_exec_failure_now`.
 * The “Soundness of Iris^⧗ ” lemma is `abstract_spec_trtranslation__adequate`.
+ * 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`.
+
+### Marrying time credits and time receipts
+
+In `Combined.v`:
+
+ * Theorem 3 (“Soundness of Iris^$⧗ ”) is `tctr_sound_abstract`.

2.26.2