VOD: https://www.youtube.com/watch?v=lY1GF-8sdsA

Verification of Program Optimisations (Lean)

Agenda. Getting stuff done in /stream/1765922400 served to be quite annoying. The most important part is encoding the theorem below in a nice way that is amenable to automatic and manual proofs (of any bitwidth n).

That’s the goal of this stream.

• Encoding assumptions nicely (above). ✅ 2025-12-19

• Manual proofs over BitVec, so conversion with iN_convert_goal_bitvec and unwrapping the definitions if an expression doesn’t have UB, and so on. This needs proof automation and shouldn’t be done with just simp. ✅ 2025-12-22

  • Try simp with restriction to certain theorems/definitions first.

• More infrastructure for opt theorems like in /stream/1765922400.

After this stream today I’m going to upload both stream VODs and create a blog post about the project itself as a better introduction, before next week.

Aftermath

Formalised a proof of addNsw_assoc_all_pos, which is actually very close to what I wanted to get done.

• Change the way definitions are unwrapped to make the proof of addNsw_assoc_all_pos much less brittle to changes to simp_iN. The proof is also quite ugly, so that can be changed as well.