| Filename | Latest commit message | Latest commit date |
|---|---|---|
0ad7ef9d67
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.
|
||
| .. | ||
| crates | ||
| Cargo.lock | ||
| Cargo.toml | ||