VOD: https://www.youtube.com/watch?v=2rChq0gwhxo

Verification of Program Optimisations (Lean)

Agenda. Blog post has been released: https://l-m.dev/cs/formally-verifying-peephole-optimisations-in-lean/.

Between last stream and this stream, the theorem

was proved. This wasn’t what I expected, but it makes sense. I always thought of x <~> y meaning that the “definedness” of x is the same as y. But, apparently they’re equal.

So now the RewriteIff := x ~> y ∧ y ~> x relation has been removed from the codebase and replaced with equality. Theorems that rewrite back and forth are replaced with equality like here:

• Change the role of the comparison >ₛ to actually be a proposition instead of a function returning iN 1. This proposition should be definitionally equivalent to the original definition. Delegate all notation for things like >ₛ to be functions instead.

• Work on a better proof automation framework to help implement canon, which works like instcombine to canonicalise some instructions (for example canon should also work like ac_nf, but rewrite aware).

  • The ideal directory contains the canonicalisations (the “ideal” forms). At the moment, canon will just be a simple simplifier but might become an SoN-esque worklist optimiser later.

• Create poison_propagate which simplifies based on poison arguments and calls trivial at the end. This will use a much smaller SimpSet compared to simp_iN which should make everything faster. ✅ 2025-12-24

Aftermath

• Implement an optimisation framework behind an AST over iN expressions (replace Expr in Lean). This will replace existing stuff behind opt.

• The goal is to encode these rewrites in this framework as functions you can just pass to opt, then you’ll be able to prove certain rewrites confluent, and so on.

  • opt/the framework is just to be a low level wrapper over actual optimisation functions. Eventually you would want to prove these correct as well, but the initial implementation should be amenable to rewrite proofs (proof of confluence, etc).