+++ 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.
\[1\] 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].
\[2\] 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].
[10.1145/2676726.2676985]: https://doi.org/10.1145/2676726.2676985 [10.1145/3371091]: https://doi.org/10.1145/3371091