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

Verification of Program Optimisations (Lean)

Agenda. The blocker with reifying variables has been solved, so I can just go and do the rest of reification and probably get done with denoting today as well.

    experiments: restructure modules
    experiments: reify reduced size of proof term
    experiments: reifying `+nsw`
    experiments: got over `IR.eval .var` hurdle

• Implement binOps when reifying (abstract the addNsw infrastructure). ✅ 2025-12-31
• Denoting. ✅ 2025-12-31

Aftermath

• Figure out how to deal with having ir and ir', but not proof that ir' = impl ir (the optimisation actually happened).
• Optimisation/proof chaining for real this time.