4. Check our list of Coq lemmas and definitions (*List of Claims*) below and make sure that the definitions are present and match up with what is presented in the paper.
We list differences between the Coq definitions and statements and what is presented in the paper in the Section *Differences to the paper* below.
We list differences between the Coq definitions and statements and what is presented in the paper in the Section *Mechanization notes* below.
5. Play around with some of the examples and try to verify some new optimizations :)
...
...
@@ -86,7 +86,7 @@ We list differences between the Coq definitions and statements and what is prese
## List of claims
We claim to fully mechanize all results mentioned in the paper.
Below, we list the relevant theorems and definitions mentioned in the paper by section, and map them to the corresponding Coq definitions and lemmas.
The section *Differences to the paper* lists minor differences in the presentation on paper and in Coq.
The section *Mechanization notes* lists minor differences in the presentation on paper and in Coq.
### Section 2
| Paper | Coq file | Coq name |
...
...
@@ -180,7 +180,7 @@ As mentioned in the related work section, we have verified the reorderings and e
For further information on this, we refer to Section 5 of the technical appendix.
### Differences to the paper
### Mechanization notes
* As mentioned in footnote 5, we omit assertions controlling the size of allocations which are needed for deallocating an allocation and escaping an entire allocation at once.
The resources `† l …s n` and `† l …t n` state that the allocation starting at `l` has size `n` (in source and target, respectively), and appears in the corresponding rules in Coq.
* As mentioned in the paper, the definitions in Section 6 are simplified in order to ease presentation. The full definitions (given in the appendix and used in the Coq code) are slightly more complex to obtain all of the relevant rules for exploiting non-atomic accesses.
