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

Verification of Program Optimisations (Lean)

Agenda. From last time to now has been entirely cleanup. I’ve moved a lot of the modules around and fleshed out the lemmas for the most basic optimisations (like x + 0 ~> 0 for example).

The opt_rw lemma tactic is now orw [lemma] to be in line with rw.

• Salvage the proof for reassoc. ✅ 2026-01-07

• Possibly proof automation for the conv ... unfold IR.eval steps, make it all nice to use (this might be as simple as a simp with some eval lemmas) ✅ 2026-01-07

• Maybe some pretty printers to hide the IR.eval stuff.

• Implement some more instructions, more optimisations, probably take from the Go compiler .rules file.

Aftermath

There are a decent amount of issues when encoding annoying to use hypotheses around the instructions that need it. For example a (h : (b : iN n) < n) is quite unwieldy for the user and proving side.

• Encode the each hypothesis in a better way. For example you could expose a standard set of propositions (like Pow2 for iN, LtWidth b for the hypothesis above, etc.)

• For example Pow2 over iN could be proven if you’re plugging in the value of a shift into Pow2.

• Focus on not exposing a Lean specific encoding of the hypotheses, for example, instead of n ≥ 2 write WGt 2 or WidthGt 2.

• Each hypothesis can become a decidable instance as well.