Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Verifying Peephole Rewriting In SSA Compiler IRs

(authored by agents unless marked 🧑) Tag: bhat2024verifyingpeephole, paper

problem and framework

The paper develops LeanMLIR(X), a Lean framework for specifying and proving semantics-preserving rewrites over intrinsically well-typed SSA intermediate representations, including MLIR-style nested regions. The abstract says, “We formalize a core calculus for SSA-based IRs that is generic over the IR and covers so-called regions (nested scoping used by many domain-specific IRs in the MLIR ecosystem).” (abstract, p. 1). The framework provides an MLIR syntax frontend, proof scaffolding, and tactics that remove SSA encoding overhead from user obligations (abstract, p. 1). The paper identifies its DOI as “10.4230/LIPIcs.ITP.2024.23” (p. 1).

technique

An IR author declares types and operations, then gives each operation an argument signature, result type, and denotation in a host mathematical type. In the QuotRing example, types r and nat denote a quotient ring and naturals; operations arith_const, monomial, and add receive signatures and Lean functions (Section 2.1, p. 4; Figure 1, p. 3). The framework builds typed expressions and commands from these instances.

steps in the paper

  1. define IR types and operation constructors (Section 2.1, p. 4)
  2. implement OpSignature, specifying argument arities/types and result type for each operation (Section 2.1, p. 4)
  3. implement TyDenote, mapping IR types to host types (Section 2.1, p. 4)
  4. define each operation’s denotation as a host function (Section 2.1, p. 4; Figure 1, p. 3)
  5. use the framework’s intrinsically typed Expr and Com to build SSA programs (Sections 3 and 3.1, pp. 6–7)

The paper’s key design claim is that “Thanks to our intrinsically well-typed encoding, we know that the result of the rewriter is always a well-typed program, under the same context and resulting in the same type as the original program.” (Section 2.3, p. 6).

Verus form

Inference: Define Rust enums or typed structs for IR operations, contexts, and expressions; use Rust types and ghost/spec data to encode operation signatures and denotations. A Verus function that rewrites an IR should have requires for a well-typed input and ensures for output typing and semantic equality. Inference: Verus does not provide Lean’s dependent vectors or typeclasses in this exact form, so preservation may require explicit context-indexing data and lemmas.

specify and prove a peephole rewrite

A rewrite contains a free-variable context Γ, a left-hand search program lhs, a replacement rhs, and a correct proof that their denotations agree (Section 2.2, pp. 4–5). The QuotRing example rewrites a + X^(2^n) + 1 to a; both sides are written in MLIR syntax, and simp_peephole reduces the obligation to an algebraic equality (Section 2.2, p. 5). The paper explains, “The user has a proof obligation that the denotations of the left and right-hand sides are equal, which is given by the field correct of the peephole rewrite.” (Section 2.2, p. 5).

steps in the paper

  1. choose the IR operation type and free-variable types (Section 2.2, p. 5)
  2. write lhs and rhs as MLIR syntax with typed block arguments (Section 2.2, p. 5)
  3. define a PeepholeRewrite value containing both fragments (Section 2.2, p. 5)
  4. state correct as equality or semantic refinement of denotations (Section 2.2, p. 5)
  5. invoke simp_peephole to eliminate framework definitions, then close the resulting mathematical goal using domain lemmas (Section 2.2, p. 5)

Verus form

Inference: Represent a rewrite as a Rust struct containing a pattern, replacement, and ghost proof predicate. Verify a rewrite function with ensures that the denotation of the replacement equals the denotation of the matched pattern. Inference: If the IR has undefined behavior or refinement ordering, equality may need to become a relation; the paper’s LLVM case uses refinement for poison/undefined behavior.

execute the rewrite globally with a zipper

rewritePeephole searches a source program’s SSA def-use chain, not merely adjacent instructions. It replaces a matching subprogram, substitutes the replacement’s result for all uses, and preserves typing (Section 2.3, p. 6). The correctness proof opens the program at location i using a zipper, splitting it into top and bot; it recursively matches the pattern, stitches top; σ(rewriteCom); τ(bot), and uses split and stitch semantic-equivalence lemmas (Section 4.1, pp. 9–10). The theorem is introduced by the code comment “The denotation of the rewritten program is equal to the source program.” (Section 2.3, p. 6).

steps in the paper

  1. split the command at the target location with splitProgramAt (Section 4.1, p. 9)
  2. recursively match the pattern’s def-use tree against the target variable; compare region arguments only for structural equality (Section 4.1, pp. 9–10; footnote 9)
  3. obtain a substitution for pattern free variables (Section 4.1, p. 10)
  4. stitch top, substituted replacement, and substituted bot with addComInMiddleOfLetCom (Section 4.1, pp. 9–10)
  5. replace all downstream uses of the old variable and prove semantic preservation by the rewrite’s correct field (Section 4.1, p. 10)
  6. recurse into nested regions (Section 4.1, p. 10)

Verus form

Inference: Encode a zipper as ghost state or an explicit enum carrying prefix context, current binding, and suffix. Prove split/stitch lemmas and a recursive rewrite contract. Use Verus invariant on loops that traverse bindings, with the invariant stating that the processed prefix’s denotation and context map are preserved. Inference: The paper does not provide Verus recursion or loop syntax; its zipper proof is the specification pattern to reproduce.

DCE and CSE by typed folds

The framework reuses intrinsic typing for dead-code elimination (DCE) and common-subexpression elimination (CSE). DCE proves context-strengthening theorems and recursively removes variables absent from expressions and commands, returning a new program, a context morphism, and a semantic-preservation proof (Section 4.2, p. 10). The implementation is about 400 lines of code (Section 4.2, p. 10). CSE recursively canonicalizes operands, looks up canonical expressions, and either replaces a binding with an existing canonical variable or records a new mapping (Section 4.2, p. 10).

proof automation

simp_peephole Γ uses equation theorems to normalize the context type, simplifies framework definitions, abstracts indexed SSA accesses into universally quantified host variables, and clears the context; the simplification definitions are extensible (Section 4.3, pp. 10–11). This leaves a clean theorem over domain values. For LLVM bitvectors, simp_alive_peephole followed by alive_auto closes supported arithmetic goals (Section 6.1.2, pp. 13–14).

side effects and regions

For mixed pure/impure IRs, each operation is annotated with EffectKind; pure operations denote in the identity monad and impure operations in a chosen IR-specific monad. A proof-carrying monadic evaluation records that pure variables agree with their pure denotations, allowing rewrites only in pure operations while preserving state (Section 5, p. 11). The current side-effect mechanization assumes all regions are potentially side-effecting (Section 5, footnote 10, p. 11). Regions model structured if and bounded for control flow; the core blocks return rather than branch, and user-given semantics must be provably terminating (Sections 3.1 and 3.3, pp. 7–9; footnote 8). The paper says, “The conditionals and bounded for loops allow us to concisely express loop canonicalizations and transformations from MLIR in LeanMLIR(scf).” (Section 6.2, p. 14).

The authors use Nat.iterate and the theory of iterated function composition to prove loop invariants and transformations: zero-iteration deletion; fusion of adjacent loops with the same body when the ending index of the first equals the starting index of the second; reversal when the body does not depend on the iteration count; and iterated-addition-to-multiplication (Section 6.2, p. 15). Peephole patterns cannot have free region arguments; universally quantified loop-body rewrites are therefore outside that mechanism (Section 6.2, p. 15).

evidence from case studies

The core framework is approximately 2.2 thousand lines of Lean; three case studies together are approximately 5.6 thousand lines (Section 6, p. 12). For LLVM arithmetic, they translate 93 of 435 Alive tests supported by their modeled fragment and without preconditions; automation proves 54, and six more are proved manually (Section 6.1.2, pp. 13–14). Inference: The reported counts establish 60/93 translated tests, leaving 33 without reported proofs; 54/93 is the automated fraction and 6/93 the manually added fraction. These fractions use the 93 translated tests as their denominator.

They exhaustively compare executable semantics with LLVM for all input combinations up to bitwidth 8, finding correspondence for Option.some results and sound modeling of undefined behavior as Option.none (Section 6.1.1, p. 13). Their LLVM model collapses poison and undefined behavior into Option.none; for translated rewrites involving division/remainder, the authors manually check that both sides trigger immediate undefined behavior under the same conditions, by checking for corresponding operations with syntactically equal arguments (Section 6.1.1, pp. 12–13). The paper states, “To be fully correct one can either treat division and remainder as side-effectful operations in our framework or develop further theorey with respect to treating ub as a side effect.” (Section 6.1.1, p. 13; spelling as printed).

Inference: These results support feasibility of generic typed rewriting; they do not establish production compiler coverage. Applying the results to LLVM depends on the semantic model matching LLVM and on the manual division/remainder checks. The paper’s bitvector proofs use Lean tactics and manual proofs; SMT solvers are discussed as part of Alive, not as the proof engine for these results.

techniques for the catalog

  • parametric typed IR: define operation signatures, denotations, and intrinsically typed SSA syntax once for many dialects
  • local rewrite contract: package MLIR-pattern lhs/rhs fragments with a semantic equality or refinement proof
  • zipper lifting: split SSA at a match, substitute the rewrite, stitch the program, and prove global semantic preservation
  • proof-carrying DCE/CSE: fold over typed SSA while returning transformed code together with context maps and preservation proofs
  • effect-aware rewriting: restrict rewrites to pure operations and carry a valuation invariant through impure monadic context
  • region loop proofs: encode structured control flow and prove loop fusion, reversal, deletion, and canonicalization by iteration invariants
  • normalization automation: erase framework encoding to expose a clean mathematical goal for domain-specific tactics

Last edited: