Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof engine by studying the asymptotic performance of proof engines and redesigning their building blocks. As a case study, w...
| Үндсэн зохиолчид: | , , , , |
|---|---|
| Бусад зохиолчид: | |
| Формат: | Өгүүллэг |
| Хэл сонгох: | English |
| Хэвлэсэн: |
Springer Netherlands
2024
|
| Онлайн хандалт: | https://hdl.handle.net/1721.1/156261 |
| _version_ | 1826196665672925184 |
|---|---|
| author | Gross, Jason Erbsen, Andres Philipoom, Jade Agrawal, Rajashree Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Gross, Jason Erbsen, Andres Philipoom, Jade Agrawal, Rajashree Chlipala, Adam |
| author_sort | Gross, Jason |
| collection | MIT |
| description | We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof engine by studying the asymptotic performance of proof engines and redesigning their building blocks. As a case study, we explore equational rewriting and introduce a novel prototype proof engine building block for rewriting in Coq, utilizing proof by reflection for enhanced performance. Our prototype implementation can significantly improve the development of verified compilers, as demonstrated in a case study with the Fiat Cryptography toolchain. The resulting extracted command-line compiler is about 1000× faster while featuring simpler compiler-specific proofs. This work lays some foundation for scaling verification efforts and contributes to the broader goal of developing a proof engine with good asymptotic performance, ultimately aimed at enabling the verification of larger and more complex systems. |
| first_indexed | 2024-09-23T10:33:23Z |
| format | Article |
| id | mit-1721.1/156261 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2025-02-19T04:19:17Z |
| publishDate | 2024 |
| publisher | Springer Netherlands |
| record_format | dspace |
| spelling | mit-1721.1/1562612024-12-21T06:12:38Z Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq Gross, Jason Erbsen, Andres Philipoom, Jade Agrawal, Rajashree Chlipala, Adam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof engine by studying the asymptotic performance of proof engines and redesigning their building blocks. As a case study, we explore equational rewriting and introduce a novel prototype proof engine building block for rewriting in Coq, utilizing proof by reflection for enhanced performance. Our prototype implementation can significantly improve the development of verified compilers, as demonstrated in a case study with the Fiat Cryptography toolchain. The resulting extracted command-line compiler is about 1000× faster while featuring simpler compiler-specific proofs. This work lays some foundation for scaling verification efforts and contributes to the broader goal of developing a proof engine with good asymptotic performance, ultimately aimed at enabling the verification of larger and more complex systems. 2024-08-19T16:19:16Z 2024-08-19T16:19:16Z 2024-08-14 2024-08-19T10:47:50Z Article http://purl.org/eprint/type/JournalArticle https://hdl.handle.net/1721.1/156261 Gross, J., Erbsen, A., Philipoom, J. et al. Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. J Autom Reasoning 68, 19 (2024). PUBLISHER_CC en 10.1007/s10817-024-09705-6 Journal of Automated Reasoning Creative Commons Attribution https://creativecommons.org/licenses/by/4.0/ The Author(s) application/pdf Springer Netherlands Springer Netherlands |
| spellingShingle | Gross, Jason Erbsen, Andres Philipoom, Jade Agrawal, Rajashree Chlipala, Adam Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq |
| title | Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq |
| title_full | Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq |
| title_fullStr | Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq |
| title_full_unstemmed | Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq |
| title_short | Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq |
| title_sort | towards a scalable proof engine a performant prototype rewriting primitive for coq |
| url | https://hdl.handle.net/1721.1/156261 |
| work_keys_str_mv | AT grossjason towardsascalableproofengineaperformantprototyperewritingprimitiveforcoq AT erbsenandres towardsascalableproofengineaperformantprototyperewritingprimitiveforcoq AT philipoomjade towardsascalableproofengineaperformantprototyperewritingprimitiveforcoq AT agrawalrajashree towardsascalableproofengineaperformantprototyperewritingprimitiveforcoq AT chlipalaadam towardsascalableproofengineaperformantprototyperewritingprimitiveforcoq |