The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.17
URN: urn:nbn:de:0030-drops-167262
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16726/
Go to the corresponding LIPIcs Volume Portal

Gross, Jason ; Erbsen, Andres ; Philipoom, Jade ; Poddar-Agrawal, Miraya ; Chlipala, Adam

Accelerating Verified-Compiler Development with a Verified Rewriting Engine

pdf-format:
LIPIcs-ITP-2022-17.pdf (1 MB)

Abstract

Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach is to present compilers as sets of algebraic rewrite rules, which a generic engine can apply efficiently. Now each rewrite rule can be proved separately, with no need to revisit past proofs for other parts of the compiler. We present the first realization of this idea, in the form of a framework for the Coq proof assistant. Our new Coq command takes normal proved theorems and combines them automatically into fast compilers with proofs. We applied our framework to improve the Fiat Cryptography toolchain for generating cryptographic arithmetic, producing an extracted command-line compiler that is about 1000× faster while actually featuring simpler compiler-specific proofs.

BibTeX - Entry

@InProceedings{gross_et_al:LIPIcs.ITP.2022.17,
  author =	{Gross, Jason and Erbsen, Andres and Philipoom, Jade and Poddar-Agrawal, Miraya and Chlipala, Adam},
  title =	{{Accelerating Verified-Compiler Development with a Verified Rewriting Engine}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16726},
  URN =		{urn:nbn:de:0030-drops-167262},
  doi =		{10.4230/LIPIcs.ITP.2022.17},
  annote =	{Keywords: compiler verification, rewriting engines, cryptography}
}

Keywords: compiler verification, rewriting engines, cryptography
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: Software (Source Code): https://github.com/mit-plv/rewriter/tree/ITP-2022-perf-data archived at: https://archive.softwareheritage.org/swh:1:rev:1787ab401a7e71afc9937010e2e155e4b1594ab5
Software (Source Code): https://github.com/mit-plv/fiat-crypto/tree/perf-testing-data-ITP-2022-rewriting archived at: https://archive.softwareheritage.org/swh:1:rev:72fe0dddee5e6dceeab0b8a2e6a745abf5287d3e

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI