Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909287179091968 |
|---|---|
| author | Gross, Jason Erbsen, Andres Philipoom, Jade Agrawal, Rajashree Chlipala, Adam |
| author_facet | Gross, Jason Erbsen, Andres Philipoom, Jade Agrawal, Rajashree Chlipala, Adam |
| contents | 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$\times$ 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2305_02521 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq Gross, Jason Erbsen, Andres Philipoom, Jade Agrawal, Rajashree Chlipala, Adam Programming Languages 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$\times$ 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. |
| title | Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2305.02521 |