We discharged the LRAT checker soundness accept ⇒ UNSAT via Aeneas → Lean (#12/#39/#46), and keep a direct-in-Lean bv_decide-style checker as a documented fallback. The approach upgrade: don't shelve the second mechanisation — run both and mine the disagreements.
Two independent formalisations of the same checker soundness are a bug-finding tool: where the Aeneas-translated proof and a hand-written Lean checker disagree — on a corner of LRAT replay, a trimming rule, an overflow edge — that disagreement localises either a translation-faithfulness gap (Aeneas) or a spec ambiguity, exactly where the trusted base actually bites. Today the fallback is dead weight; run it as a differential and it becomes a second, independent witness that our one soundness theorem is about the right thing.
First step: stand up the bv_decide-style checker on a shared corpus of LRAT certificates (the burn-in set from #29 is a start) and gate on verdict agreement with the Aeneas path — a disagreement is a hard error, the way the ordeal-vs-Z3 differential already is.
Part of a verification-approach sweep (direction, not a defect): prefer generation over checking (a single source emits the artifacts, so drift becomes unrepresentable), use independence adversarially (run a second mechanisation to hunt spec bugs rather than shelving it), and invest reference oracles (one artifact everything else differential-tests against).
We discharged the LRAT checker soundness
accept ⇒ UNSATvia Aeneas → Lean (#12/#39/#46), and keep a direct-in-Leanbv_decide-style checker as a documented fallback. The approach upgrade: don't shelve the second mechanisation — run both and mine the disagreements.Two independent formalisations of the same checker soundness are a bug-finding tool: where the Aeneas-translated proof and a hand-written Lean checker disagree — on a corner of LRAT replay, a trimming rule, an overflow edge — that disagreement localises either a translation-faithfulness gap (Aeneas) or a spec ambiguity, exactly where the trusted base actually bites. Today the fallback is dead weight; run it as a differential and it becomes a second, independent witness that our one soundness theorem is about the right thing.
First step: stand up the
bv_decide-style checker on a shared corpus of LRAT certificates (the burn-in set from #29 is a start) and gate on verdict agreement with the Aeneas path — a disagreement is a hard error, the way the ordeal-vs-Z3 differential already is.Part of a verification-approach sweep (direction, not a defect): prefer generation over checking (a single source emits the artifacts, so drift becomes unrepresentable), use independence adversarially (run a second mechanisation to hunt spec bugs rather than shelving it), and invest reference oracles (one artifact everything else differential-tests against).