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).

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

Verification of Program Optimisations (Lean)

Work on https://github.com/l1mey112/bitbasher.

Agenda.

You would probably want to go over what this project is even about before you go those things below. ✅ 2025-12-17
- Create blog post on this.

Work on a general theory of noUb and wf functions, so you can make conversions and rewrites super easy. ✅ 2025-12-17
The proposition wf : f poison = poison only tells you that f doesn’t observe poison if f is nonconstant/doesn’t depend on the argument. Though, it usually does depend on the argument so is this really a misname? ✅ 2025-12-17
The wf argument to congrApp shouldn’t be passed by the user basically ever. Calculating this should be fast too, it shouldn’t use by simp [simp_iN].

theorem congrApp {n} (f : iN n → iN n)
    {wf : f poison = poison := by opt_poison_input}
    {a a' : iN n} (h : a ~> a') : f a ~> f a'

Aftermath

Infrastructure for opt theorems.
- The above, and for example using a Monad as you traverse terms to ascertain whether or not UB is preserved or not. (This uses a general theory of noUb, wF, ubEquiv', ubEquiv, whatever works.)
General typeclasses the different possible ways to raise UB. So for example x + y doesn’t introduce any MORE UB than it’s arguments, but x +nsw y does.
- Generally you could have a theorem relating these typeclasses.

Proving.
1. Prove by rewriting based on what you already know (human).
2. Prove by the semantics of the actual program (human).
3. Automatically prove (machine).

At the moment, (1), (3). I guess we need (2).

Solving (2)

Support argument to the conversion iN_convert_goal_bitvec a b c, then use simplification lemmas to bring things back down in terms of BitVec.

/-
(h :
  (x ≥ₛ 0) &&& (y ≥ₛ 0) &&& (z ≥ₛ 0) ~> 1 ∨
  (x <ₛ 0) &&& (y <ₛ 0) &&& (z <ₛ 0) ~> 1)
-/
def hyp {n} (a b c : BitVec n) :=
  !(a.sle 0) && !(b.sle 0) && !(c.sle 0) ∨
  (a.slt 0) && (b.slt 0) && (c.slt 0)

When using iN_convert_goal_bitvec there should be another SimpSet to further reduce to the definition but don’t go further than BitVec.

@[opt ideal]
theorem add_zero {n} (x : iN n) : x + 0 ~> x := by
  iN_convert_goal_bitvec
  /-
  case bitvec
  n : Nat
  a✝ : BitVec n
  ⊢ bitvec a✝ + 0 ~> bitvec a✝
  -/

When doing simp only [iN_simp] you end up with the below which isn’t really useful because you’re not going to the definition. I would want to convert ~> bitvec to something.

⊢ (bitvec a✝).pBind₂ (bitvec 0#n) iN.add? ~> bitvec a✝

Proving Math Theorems in Lean

Aftermath

Proving Math Theorems in Lean

Aftermath

RandomX.js and EquiX.js

Aftermath

RandomX.js and EquiX.js

Aftermath

RandomX.js and EquiX.js

Verification of Program Optimisations (Lean)

Aftermath

Verification of Program Optimisations (Lean)

Aftermath

Verification of Program Optimisations (Lean)

Aftermath

Verification of Program Optimisations (Lean)

Aftermath

Verification of Program Optimisations (Lean)

Aftermath

Verification of Program Optimisations (Lean)

Aftermath

Verification of Program Optimisations (Lean)

Aftermath

Solving (2)