proof: a joule ceiling, and two soundness bugs that were hiding each other #62
2026-08-26
proof: two soundness bugs that were hiding each other (SPEC §5.2)
All checks were successful
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 3s
Found by running the shipped ladder on a real statement instead of reading it.
Each bug masked the other, so fixing the first exposed the second.
**1. Any non-SMT goal was reported as REFUTED.**
`Z3Smt` piped `goal.statement` — an arbitrary string — straight into `z3 -in
-smt2`. z3 reports a parse failure as `(error "...")` on STDOUT, then answers
`(check-sat)` anyway, against an assertion stack that is empty because nothing
parsed. That answer is `sat`, and `run_z3` scanned for the first line equal to
`sat|unsat|unknown` and skipped the error line entirely. `sat` maps to
`Verdict::Refuted`.
So "I could not understand the goal" became "the goal is FALSE" — and because a
refutation is terminal in this cascade, that was final. Feeding it Goldbach's
conjecture returned `refuted: true` with the counter-model `"(\n)"`. Three
fixes, because each catches a case the others miss:
- an `(error` anywhere in z3's output makes the run undecided, never a verdict;
- `Z3Smt` now applies the same `looks_like_smt` shape guard the resident
`Z3Server` already had — one call site had simply been missed;
- a `sat` becomes a refutation only when a substantive counter-model exists. A
script asserting nothing is trivially satisfiable, so `sat` from an empty
assertion stack means "no constraints", not "here is a counter-example". The
shape guard alone would not catch this: `(check-sat)` is well-formed SMT.
Note the stderr redirect was a red herring — z3 writes these errors to stdout.
**2. With the false refutation gone, the cascade reaches a rung that proves
anything.**
`FrontierModel` (T3) returns `Proved` for every goal, and the "artifact" is
`ContentId::of_bytes(goal.statement)` — the claim offered as its own evidence.
`seal()` gates only on `proved`, so this signs into a JCR-1 receipt that
verifies under the steward key. The demonstration is a 438-byte receipt
asserting `verdict: "proved", closed_by: "T3"` for Goldbach's conjecture. It is
not forged; it is honestly signed and substantively empty, which is worse,
because it verifies.
Neither existing qualifier catches it: `Provenance` qualifies an attempt's
energy, `SpecGrounding` its intent, and neither says whether the verdict was
earned. So `Solver::is_reference_stub()` is now declared by all four
stand-ins, `CascadeResult::closed_by_stub` records whether the **closing**
solver was one, and `require_substantive_proof()` is the relying-party check.
The proof cache persists the marker, because a cache hit that dropped it would
launder an unearned proof into an unmarked one.
`closed_by_stub` is deliberately NOT in the JCR-1 wire yet. Every published
vector is generated from the all-stand-in `reference_ladder()` — including an
`("open conjecture", Hard)` case sealed as proved at T3 — so encoding it would
regenerate the entire conformance corpus. That is a decision about the standard
rather than an implementation detail, and it is left open rather than taken
quietly. Until it is, the marker is on the result and the check is available.
The trait default is "not a stand-in", which is the unsafe direction, and §5.2
says so plainly: it spares real solvers an opt-out, but it makes the declaration
a contract on the implementor rather than something the framework can infer.
Verified: 38 workspace tests pass (4 new soundness tests pinning both bugs and
the cache-laundering path), conformance passes all 10 classes, published vectors
unchanged on disk.
proof: give the cascade a joule ceiling (SPEC §5.1)
Some checks failed
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Has been cancelled
`grep -rn "ceiling\|budget" proof-rs/crates/**/*.rs` returned nothing. The standard whose entire premise is joules-per-verified-proof could measure joules, attribute them per tier, disclose escalation waste and seal the total — and had no way to say "spend at most this many". That matters because the ladder spans a millionfold: 50 uJ at `Automation`, 50 J at `BigModel`. An unbounded cascade escalates a goal nobody wanted solved that badly straight into the most expensive rung and reports the bill afterwards, which is accounting rather than control. `Router::with_ceiling` refuses to *begin* any rung whose nominal cost would take the run past the ceiling. The check is deliberately on the next rung's cost before it runs: refusing afterwards spends exactly the joules the ceiling exists to withhold, and at T3 that is 50 J of frontier inference for a goal whose owner had declared it was not worth that much. Four distinctions the design turns on: - **A budget halt is not a mathematical verdict.** `proved = false` alone conflates "no rung could decide it" with "we stopped paying", which are different claims about the world — the second says nothing whatever about whether the goal is provable. `halted_at` records the refused tier so a reader cannot mistake an exhausted wallet for a result. - **A budget halt is not a refutation** either, and must not reach the receipt as one. - **Actual spend may exceed the ceiling** when a solver overshoots its nominal cost. Those joules were really spent, so the receipt reports them rather than clamping to the budget: a ceiling bounds what is attempted, not what physics did. `breached_ceiling()` surfaces the gap instead of hiding it. - **A ceiling below the cheapest rung attempts nothing and says so.** That is a coherent request, not an error. The receipt carries `ceiling_uj` when one was declared, which upgrades a proved receipt's claim from "this cost N" to "this was obtained under a declared budget of C and cost N". Omitted when absent, so an unbounded run canonicalizes to exactly the bytes it always did — the published vectors still verify untouched, which C6 asserts directly rather than leaving to trust. Batch accounting counts budget halts separately from failures for the same reason as above: folding them together makes a batch look mathematically harder than it was. Verified: 34 workspace tests pass, conformance passes all 10 classes including the new C6, published vectors unchanged on disk, no new clippy warnings (the two in `meter.rs` are pre-existing and that file is untouched).