Document Open Access Logo

Correctly Compiling Proofs About Programs Without Proving Compilers Correct

Authors Audrey Seo , Christopher Lam , Dan Grossman , Talia Ringer

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.33.pdf
  • Filesize: 0.91 MB
  • 20 pages

Document Identifiers

Author Details

Audrey Seo
  • University of Washington, Seattle, WA, USA
Christopher Lam
  • University of Illinois Urbana-Champaign, IL, USA
Dan Grossman
  • University of Washington, Seattle, WA, USA
Talia Ringer
  • University of Illinois Urbana-Champaign, IL, USA

Funding

This research was developed with funding from the Defense Advanced Research Projects Agency. The views, opinions, and/or findings expressed are those of the author(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.

Acknowledgements

We thank the Coq team for their proof engineering advice. We thank Guilherme Espada, John Leo, Pedro Amorim, Sophia Roshal, and Zachary Tatlock for their paper feedback.

Cite AsGet BibTex

Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer. Correctly Compiling Proofs About Programs Without Proving Compilers Correct. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.33

Abstract

Guaranteeing correct compilation is nearly synonymous with compiler verification. However, the correctness guarantees for certified compilers and translation validation can be stronger than we need. While many compilers do have incorrect behavior, even when a compiler bug occurs it may not change the program’s behavior meaningfully with respect to its specification. Many real-world specifications are necessarily partial in that they do not completely specify all of a program’s behavior. While compiler verification and formal methods have had great success for safety-critical systems, there are magnitudes more code, such as math libraries, compiled with incorrect compilers, that would benefit from a guarantee of its partial specification. This paper explores a technique to get guarantees about compiled programs even in the presence of an unverified, or even incorrect, compiler. Our workflow compiles programs, specifications, and proof objects, from an embedded source language and logic to an embedded target language and logic. We implement two simple imperative languages, each with its own Hoare-style program logic, and a system for instantiating proof compilers out of compilers between these two languages that fulfill certain equational conditions in Coq. We instantiate our system on four compilers: one that is incomplete, two that are incorrect, and one that is correct but unverified. We use these instances to compile Hoare proofs for several programs, and we are able to leverage compiled proofs to assist in proofs of larger programs. Our proof compiler system is formally proven sound in Coq. We demonstrate how our approach enables strong target program guarantees even in the presence of incorrect compilation, opening up new options for which proof burdens one might shoulder instead of, or in addition to, compiler correctness.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Hoare logic
  • Software and its engineering → Compilers
Keywords
  • proof transformations
  • compiler validation
  • program logics
  • proof engineering

Metrics

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

Supplementary Materials

References

  1. Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. Cogent: Verifying high-assurance file system implementations. In International Conference on Architectural Support for Programming Languages and Operating Systems, pages 175-188, Atlanta, GA, USA, April 2016. URL: https://doi.org/10.1145/2872362.2872404.
  2. Abhishek Anand, Andrew W. Appel, Greg Morrisett, Matthew Weaver, Matthieu Sozeau, Olivier Savary Belanger, Randy Pollack, and Zoe Paraskevopoulou. CertiCoq: A verified compiler for Coq. In CoqPL, 2017. URL: http://www.cs.princeton.edu/~appel/papers/certicoq-coqpl.pdf.
  3. Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara Rezk. Certificate translation for optimizing compilers. ACM Trans. Program. Lang. Syst., 31(5), July 2009. URL: https://doi.org/10.1145/1538917.1538919.
  4. Gilles Barthe, Tamara Rezk, and Ando Saabas. Proof obligations preserving compilation. In Formal Aspects in Security and Trust: Thrid International Workshop, FAST 2005, Newcastle upon Tyne, UK, July 18-19, 2005, Revised Selected Papers, pages 112-126. Springer, 2005. Google Scholar
  5. Lennart Beringer and Andrew W. Appel. Abstraction and subsumption in modular verification of C programs. Formal Methods in System Design, 58(1):322-345, October 2021. URL: https://doi.org/10.1007/s10703-020-00353-1.
  6. Sandrine Blazy and Xavier Leroy. Mechanized Semantics for the Clight Subset of the C Language. Journal of Automated Reasoning, 43(3):263-288, October 2009. URL: https://doi.org/10.1007/s10817-009-9148-3.
  7. William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. Type-preserving cps translation of Sigma and Pi types is not not possible. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158110.
  8. Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. Journal of Automated Reasoning, 61(1):367-422, June 2018. URL: https://doi.org/10.1007/s10817-018-9457-5.
  9. Mario Carneiro. Metamath zero: Designing a theorem prover prover. In Christoph Benzmüller and Bruce Miller, editors, Intelligent Computer Mathematics, pages 71-88, Cham, 2020. Springer International Publishing. Google Scholar
  10. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. SIGPLAN Not., 46(9):418-430, September 2011. URL: https://doi.org/10.1145/2034574.2034828.
  11. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using crash hoare logic for certifying the fscq file system. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP '15, pages 18-37, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2815400.2815402.
  12. Adam Chlipala. Mostly-automated verification of low-level programs in computational separation logic. SIGPLAN Not., 46(6):234-245, June 2011. URL: https://doi.org/10.1145/1993316.1993526.
  13. Adam Chlipala. The bedrock structured programming system: Combining generative metaprogramming and hoare logic in an extensible program verifier. SIGPLAN Not., 48(9):391-402, September 2013. URL: https://doi.org/10.1145/2544174.2500592.
  14. Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. SIGPLAN Not., 50(1):595-608, January 2015. URL: https://doi.org/10.1145/2775051.2676975.
  15. Robert W Hasker and Uday S Reddy. Generalization at higher types. In Proceedings of the Workshop on the λProlog Programming Language, pages 257-271, 1992. Google Scholar
  16. Bruno Hauser. Embedding proof-carrying components into Isabelle. Master’s thesis, ETH, Swiss Federal Institute of Technology Zurich, Institute of Theoretical …, 2009. Google Scholar
  17. Einar Broch Johnsen and Christoph Lüth. Theorem reuse by proof term transformation. In Theorem Proving in Higher Order Logics: 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004. Proceedings, pages 152-167. Springer, Berlin, Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-30142-4_12.
  18. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. SIGPLAN Not., 50(1):637-650, January 2015. URL: https://doi.org/10.1145/2775051.2676980.
  19. Jérémie Koenig and Zhong Shao. Compcerto: Compiling certified open c components. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 1095-1109, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454097.
  20. Thomas Kolbe and Christoph Walther. Proof Analysis, Generalization and Reuse, pages 189-219. Springer, Dordrecht, 1998. URL: https://doi.org/10.1007/978-94-017-0435-9_8.
  21. Paulette Koronkevitch, Ramon Rakow, Amal Ahmed, and William J. Bowman. Anf preserves dependent types up to extensional equality. Journal of Functional Programming, 32:e12, 2022. URL: https://doi.org/10.1017/S0956796822000090.
  22. Dexter Kozen and Maria-Cristina Patron. Certification of compiler optimizations using kleene algebra with tests. In John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey, editors, Computational Logic - CL 2000, pages 568-582, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-44957-4_38.
  23. Dexter Kozen and Jerzy Tiuryn. On the completeness of propositional hoare logic. Information Sciences, 139(3):187-195, 2001. Relational Methods in Computer Sciece. URL: https://doi.org/10.1016/S0020-0255(01)00164-5.
  24. Robbert Krebbers, Amin Timany, and Lars Birkedal. Interactive proofs in higher-order concurrent separation logic. SIGPLAN Not., 52(1):205-217, January 2017. URL: https://doi.org/10.1145/3093333.3009855.
  25. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 179-191, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2535838.2535841.
  26. César Kunz. Certificate Translation Alongside Program Transformations. PhD thesis, ParisTech, Paris, France, 2009. Google Scholar
  27. Peter Lammich. Refinement to imperative HOL. J. Autom. Reason., 62(4):481-503, April 2019. URL: https://doi.org/10.1007/s10817-017-9437-1.
  28. Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd ACM symposium on Principles of Programming Languages, pages 42-54. ACM Press, 2006. URL: http://xavierleroy.org/publi/compiler-certif.pdf.
  29. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, July 2009. URL: https://doi.org/10.1145/1538788.1538814.
  30. Xavier Leroy. Coq development for the course "Mechanized semantics", 2019-2021. URL: https://github.com/xavierleroy/cdf-mech-sem.
  31. Nicolas Magaud. Changing data representation within the Coq system. In International Conference on Theorem Proving in Higher Order Logics, pages 87-102. Springer, 2003. Google Scholar
  32. Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman. Oeuf: Minimizing the Coq extraction TCB. In CPP, pages 172-185, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3167089.
  33. Peter Müller and Martin Nordio. Proof-transforming compilation of programs with abrupt termination. In SAVCBS, pages 39-46, January 2007. URL: https://doi.org/10.1145/1292316.1292321.
  34. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Dependent types for imperative programs. SIGPLAN Not., 43(9):229-240, September 2008. URL: https://doi.org/10.1145/1411203.1411237.
  35. George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '97, pages 106-119, New York, NY, USA, January 1997. Association for Computing Machinery. URL: https://doi.org/10.1145/263699.263712.
  36. George C. Necula. Translation validation for an optimizing compiler. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, PLDI '00, pages 83-94, New York, NY, USA, 2000. Association for Computing Machinery. URL: https://doi.org/10.1145/349299.349314.
  37. Martin Nordio, Peter Müller, and Bertrand Meyer. Formalizing proof-transforming compilation of Eiffel programs. Technical report, ETH Zurich, 2008. Google Scholar
  38. Daniel Patterson and Amal Ahmed. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, 2nd Summit on Advances in Programming Languages (SNAPL 2017), volume 71 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:15, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.SNAPL.2017.12.
  39. Frank Pfenning. Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, 1987. Google Scholar
  40. Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, and Adam Chlipala. Relational compilation for performance-critical applications: Extensible proof-producing translation of functional models into low-level code. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, pages 918-933, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3519939.3523706.
  41. Talia Ringer. Proof Repair. PhD thesis, University of Washington, 2021. Google Scholar
  42. Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller, and Gerwin Klein. A framework for the automatic formal verification of refinement from Cogent to C. In Interactive Theorem Proving, pages 323-340, Cham, 2016. Springer. URL: https://doi.org/10.1007/978-3-319-43144-4_20.
  43. Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. Dimsum: A decentralized approach to multi-language semantics and verification. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571220.
  44. Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer. uwplse/potpie. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:5b78a12be7ef95b92fe5db2acf903d436e951851;origin=https://github.com/uwplse/potpie;visit=swh:1:snp:26d63d87f40e97c18fafd5c3f0abdea38e8db6cc;anchor=swh:1:rev:a57f960958901dee3b8075be0a312d6a194be456 (visited on 2024-08-21). URL: https://github.com/uwplse/potpie/tree/v0.5.
  45. The Coq Development Team. The coq proof assistant, July 2023. URL: https://doi.org/10.5281/zenodo.8161141.
  46. Yuting Wang, Pierre Wilke, and Zhong Shao. An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290375.
  47. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and understanding bugs in c compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 283-294, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/1993498.1993532.
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