A counter-model is a DECISION (the goal is false), not a failure to decide. The
cascade previously collapsed `z3`'s `sat` into `Verdict::Unproved`, and the
router escalates on any non-Proved verdict — so a z3-refuted FALSE goal fell
through to `FrontierModel`, whose `attempt` returns `proved` unconditionally, and
came back "PROVED by BigModel". A fabricated proof of a refuted goal.
Fix, three crates:
- proof-schema: `Verdict::Refuted { counter_model }` + `is_refuted()` + a
`refuted` wire tag.
- proof-solvers: `Z3Smt` and `Z3Server` emit `Refuted` on `sat`, with the
witness fetched via a one-shot `(get-model)` (refutation path is terminal,
so the proved path pays nothing).
- proof-cascade: `prove()` HALTS on a `Refuted` verdict — does not escalate,
does not cache (only proofs are durable assets), and does not count the
deciding solver's joules as escalation waste. `CascadeResult` gains
`refuted` + `counter_model` (serde-defaulted, so existing receipts/vectors
are unaffected).
Regression test `a_refutation_halts_the_cascade_and_never_escalates_to_a_proving_rung`
puts a refuter before an always-prove stand-in and asserts the model rung never
runs. Surfaced by joule-code-remediate's formal_fix example, which reported the
buggy candidate "PROVED by BigModel" at ~50 J against real_ladder().
Co-Authored-By: Claude Opus 4.8 <[email protected]>
2f5a683f79