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

Verification of Program Optimisations (Lean)

Agenda. Last stream only denoting and reification have been implemented, and the beginning of proof chaining was being done. Between this stream and now I actually got proof chaining done though.

An example is this, so given an optimisation function impl and a proof that the function implements a correct optimisation in wf together they make a Rule which describes an optimisation.

You can apply that rule using the ⟦ opt : func ⟧ syntax (which is for debugging really), and end up with a new function + a proof that the old function (before optimisation) is equivalent (up to UB) to the new one.

• Implementing a tactic to work on goals of the form lhs ~> rhs, and convert them to goals of the form lhs' ~> rhs, where lhs' is the optimised form of lhs. ✅ 2026-01-02
• Implement a real optimisation! (Probably reassociation.) ✅ 2026-01-02

Aftermath

To deal with the walker + rewrite issue (proof of termination), need to show confluent rewriting rules (that is, the repeat rewriting terminates). So another framework needs to be implemented.

Other than that, the implementation of reassoc' was a pretty good benchmark.

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

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

• Implement more optimisations.

The proof of the optimisation’s validity is a simple induction argument.