Document Open Access Logo

Accelerating Verified-Compiler Development with a Verified Rewriting Engine

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

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.17.pdf
  • Filesize: 1.09 MB
  • 18 pages

Document Identifiers

Author Details

Jason Gross
  • CSAIL, Massachusetts Institute of Technology, Cambridge, MA, USA
  • Machine Intelligence Research Institute, Berkeley, CA, USA
Andres Erbsen
  • CSAIL, Massachusetts Institute of Technology, Cambridge, MA, USA
Jade Philipoom
  • CSAIL, Massachusetts Institute of Technology, Cambridge, MA, USA
  • Google
Miraya Poddar-Agrawal
  • Reed College, Portland, OR, USA
Adam Chlipala
  • CSAIL, Massachusetts Institute of Technology, Cambridge, MA, USA

Funding

This work was supported in part by a Google Research Award, National Science Foundation grants CCF-1253229, CCF-1512611, and CCF-1521584, and the National Science Foundation Graduate Research Fellowship under Grant Nos. 1122374 and 1745302. Any opinion, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.

Cite AsGet BibTex

Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, and Adam Chlipala. Accelerating Verified-Compiler Development with a Verified Rewriting Engine. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.17

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Equational logic and rewriting
  • Software and its engineering → Compilers
  • Software and its engineering → Translator writing systems and compiler generators
Keywords
  • compiler verification
  • rewriting engines
  • cryptography

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Klaus Aehlig, Florian Haftmann, and Tobias Nipkow. A compiled implementation of normalization by evaluation. In Proc. TPHOLs, 2008. Google Scholar
  2. Nada Amin and Tiark Rompf. LMS-Verify: Abstraction without regret for verified systems programming. In Proc. POPL, 2017. Google Scholar
  3. U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203-211, July 1991. URL: https://doi.org/10.1109/LICS.1991.151645.
  4. Mathieu Boespflug. Efficient normalization by evaluation. In Olivier Danvy, editor, Workshop on Normalization by Evaluation, Los Angeles, United States, August 2009. URL: https://hal.inria.fr/inria-00434283.
  5. Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full reduction at full throttle. In Proc. CPP, 2011. Google Scholar
  6. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In ICFP'08: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, Victoria, British Columbia, Canada, September 2008. URL: http://adam.chlipala.net/papers/PhoasICFP08/.
  7. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. Elsevier, 1972. Google Scholar
  8. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In IEEE Security & Privacy, San Francisco, CA, USA, May 2019. URL: http://adam.chlipala.net/papers/FiatCryptoSP19/.
  9. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Proc. ICFP, 2002. Google Scholar
  10. Florian Haftmann and Tobias Nipkow. A code generator framework for Isabelle/HOL. In Proc. TPHOLs, 2007. Google Scholar
  11. Jason Hickey and Aleksey Nogin. Formal compiler construction in a logical framework. Higher-Order and Symbolic Computation, 19(2):197-230, 2006. URL: https://doi.org/10.1007/s10990-006-8746-6.
  12. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179-191. ACM Press, January 2014. URL: https://cakeml.org/popl14.pdf.
  13. Xavier Leroy. A formally verified compiler back-end. J. Autom. Reason., 43(4):363-446, December 2009. URL: http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf.
  14. Gregory Malecha and Jesper Bengtson. Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, chapter Extensible and Efficient Automation Through Reflective Tactics, pages 532-559. Springer Berlin Heidelberg, Berlin, Heidelberg, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_21.
  15. Luc Maranget. Compiling pattern matching to good decision trees. In Proceedings of the 2008 ACM SIGPLAN workshop on ML, pages 35-46. ACM, 2008. URL: http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf.
  16. Tiark Rompf and Martin Odersky. Lightweight modular staging: A pragmatic approach to runtime code generation and compiled DSLs. Proceedings of GPCE, 2010. URL: https://infoscience.epfl.ch/record/150347/files/gpce63-rompf.pdf.
  17. Zachary Tatlock and Sorin Lerner. Bringing extensibility to verified compilers. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '10, pages 111-121, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1806596.1806611.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact