M5: Correctness

[tamnd]

Four weeks. Part V, correctness. This sits before the backend rather than at the end on purpose. Once you have watched a solver hand you a counterexample you stop trusting your own reasoning about poison, and that is the right state of mind for everything after it.

Exit criterion. V06's treatment of boundedness is reviewed and confirmed not to oversell, because every Alive2 claim in the project links there.

Tasks

• V01 to V06
• irx.reduce and irx.lit
• The ReduceTrace and AliveVerdict widgets
• The graders CI job, hardened

Gates

• V03's boss fight, reducing 900 lines to under 15, is completed by testers in under 50 minutes
• V06 is reviewed and confirmed not to describe bounded verification as proof
• update_test_checks.py integration produces tests an LLVM reviewer would accept, confirmed by asking one

The V06 gate is a quality bar item as much as a content one. Alive2 unrolls loops to a fixed depth, so "no counterexample found" is strong evidence and is not a proof, and a reader who leaves this project believing otherwise has been taught something false by the one lesson that was supposed to prevent that.