Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq

Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala

TL;DR

This work tackles the problem of scaling formal verification to the size of real-world systems by analyzing and redesigning the building blocks of proof engines, with a focus on equational rewriting in Coq. It introduces a proof-by-reflection-based rewriting prototype that integrates normalization-by-evaluation and pattern-matching compilation to achieve orders-of-magnitude speedups in realistic pipelines, notably Fiat Cryptography, where extracted code runs up to about $1000\times$ faster than prior approaches. The authors identify and analyze deep bottlenecks in current rewriting tactics—subterm sharing, evar handling, and proof-term growth—and propose a set of desiderata for a scalable rewriting kernel, including correctness without extending the trusted code base, modularity for side conditions, and strong subterm sharing. The results demonstrate practical gains for large-scale programs and outline a concrete research agenda toward a full-fledged proof engine building block capable of handling the full Coq language and very large verification efforts.

Abstract

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.

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq

TL;DR

This work tackles the problem of scaling formal verification to the size of real-world systems by analyzing and redesigning the building blocks of proof engines, with a focus on equational rewriting in Coq. It introduces a proof-by-reflection-based rewriting prototype that integrates normalization-by-evaluation and pattern-matching compilation to achieve orders-of-magnitude speedups in realistic pipelines, notably Fiat Cryptography, where extracted code runs up to about faster than prior approaches. The authors identify and analyze deep bottlenecks in current rewriting tactics—subterm sharing, evar handling, and proof-term growth—and propose a set of desiderata for a scalable rewriting kernel, including correctness without extending the trusted code base, modularity for side conditions, and strong subterm sharing. The results demonstrate practical gains for large-scale programs and outline a concrete research agenda toward a full-fledged proof engine building block capable of handling the full Coq language and very large verification efforts.

Abstract

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.
Paper Structure (36 sections, 13 equations, 7 figures, 1 table)

This paper contains 36 sections, 13 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Blue Sky
  3. Performant Rewriting
  4. Where is the Status Quo on Rewriting?
  5. Why is the Status Quo so Slow?
  6. Inefficient Matching Representations involving Existential-Variable Contexts
  7. Proof-Term Size
  8. Poor Subterm Sharing
  9. Asymptotic Performance Challenges in Rewriting
  10. Empirical Cost of Incrementality
  11. Overhead from the let Typing Rule
  12. Desiderata for a New Rewriting Building Block
  13. How Well Does Our Prototype Do?
  14. Building a Rewriter
  15. Our Approach in Ten Steps
  16. ...and 21 more sections

Figures (7)

  • Figure 1: Performance numbers for coqsetoid_rewrite and rewrite_strat
  • Figure 2: Partial Pseudocode Rewriting: Function Application Case
  • Figure 3: Partial Pseudocode Rewriting: $\lambda$ Abstraction Case
  • Figure 4: Implementation of normalization by evaluation
  • Figure 5: PHOAS implementation of normalization by evaluation
  • ...and 2 more figures