1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
+++
title = "Hacking CompCert"
date = "2020-12-10"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a3", "3a"]
forwardlinks = ["3a5", "3a4a"]
zettelid = "3a4"
+++
CompCert is built in a way which makes it very easy to hack, meaning one
can insert extra passes and build on the proofs that they developed.
There have been many examples of this, for example Compositional
CompCert \[1\] or CompCertM \[2\].
The main reason that CompCert facilitates this is because they have
designed the proofs for each of their language translations is a similar
way, meaning one can adopt the same translation style and get a similar
proof for ones own intermediate language. In addition to that, CompCert
contains many helper theorems for proofs of simulation, which are the
main arguments that are used to prove equivalence. Finally, all the
proofs of the different languages are composed at various levels,
meaning that if they are changed, one can compose the proof in a custom
way that still proves the original property that the behaviour stays the
same throughout the translations.
<div id="refs" class="references csl-bib-body" markdown="1">
<div id="ref-stewart15_compos_compc" class="csl-entry" markdown="1">
<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">G. Stewart, L. Beringer, S.
Cuellar, and A. W. Appel, “Compositional CompCert,” in *Proceedings of
the 42nd annual ACM SIGPLAN-SIGACT symposium on principles of
programming languages*, in POPL ’15. Mumbai, India: Association for
Computing Machinery, 2015, pp. 275–287. doi:
[10.1145/2676726.2676985].</span>
</div>
<div id="ref-song19_compc" class="csl-entry" markdown="1">
<span class="csl-left-margin">\[2\]
</span><span class="csl-right-inline">Y. Song, M. Cho, D. Kim, Y. Kim,
J. Kang, and C.-K. Hur, “CompCertM: CompCert with C-assembly linking and
lightweight modular verification,” *Proc. ACM Program. Lang.*, vol. 4,
no. POPL, Dec. 2019, doi: [10.1145/3371091].</span>
</div>
</div>
[10.1145/2676726.2676985]: https://doi.org/10.1145/2676726.2676985
[10.1145/3371091]: https://doi.org/10.1145/3371091
|
