Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Accelerating Verified-Compiler Development with a Verified Rewriting Engine

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

TL;DR

This work introduces a verified rewriting engine within Coq that converts sets of proven theorems into an extraction-ready compiler, enabling modular proofs for each rewrite rule and avoiding reproofs as the compiler evolves. It leverages normalization by evaluation (NbE) and a PHOAS-based syntax to maintain subterm sharing and termination, while employing a decision-tree pattern-matching compiler to achieve scalable, efficient rewriting. Applied to Fiat Cryptography, the framework delivers dramatic performance gains (roughly $10^3\times$ faster in some cases) and simplifies proofs, enabling new backends and direct-style code without expanding the trusted code base. The approach reduces the verification burden and scales to thousands of variables, making verified compiler development more practical for real-world cryptographic toolchains and beyond.

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$\times$ faster while actually featuring simpler compiler-specific proofs.

Accelerating Verified-Compiler Development with a Verified Rewriting Engine

TL;DR

This work introduces a verified rewriting engine within Coq that converts sets of proven theorems into an extraction-ready compiler, enabling modular proofs for each rewrite rule and avoiding reproofs as the compiler evolves. It leverages normalization by evaluation (NbE) and a PHOAS-based syntax to maintain subterm sharing and termination, while employing a decision-tree pattern-matching compiler to achieve scalable, efficient rewriting. Applied to Fiat Cryptography, the framework delivers dramatic performance gains (roughly faster in some cases) and simplifies proofs, enabling new backends and direct-style code without expanding the trusted code base. The approach reduces the verification burden and scales to thousands of variables, making verified compiler development more practical for real-world cryptographic toolchains and beyond.

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.
Paper Structure (60 sections, 14 equations, 10 figures)

This paper contains 60 sections, 14 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Our Solution
  4. A Motivating Example
  5. The Structure of a Rewriter
  6. Our Approach in Ten Steps
  7. Pattern-Matching Compilation and Evaluation
  8. Adding Higher-Order Features
  9. Scaling Challenges
  10. Variable Environments Will Be Large
  11. Subterm Sharing Is Crucial
  12. Rules Need Side Conditions
  13. Side Conditions Need Abstract Interpretation
  14. Evaluation
  15. Iteration on the Fiat Cryptography Compiler
  16. ...and 45 more sections

Figures (10)

  • Figure 1: Implementation of normalization by evaluation
  • Figure 2: PHOAS implementation of normalization by evaluation
  • Figure 3: Timing of different partial-evaluation implementations
  • Figure 4: Timing of different partial-evaluation implementations for code with no binders for fixed $m$. Note that we have a logarithmic time scale, because term size is proportional to $2^n$.
  • Figure 5: Timing of different partial-evaluation implementations for code with no binders for fixed $n$ (1, 2, 3, and then we jump to 9)
  • ...and 5 more figures