proof: a joule ceiling, and two soundness bugs that were hiding each other #62

Merged

dcharlot merged 2 commits from proof/joule-ceiling into main 2026-08-29 03:09:28 -04:00

Conversation 0 Commits 2 Files changed 7 +520 -9

dcharlot commented 2026-08-26 08:50:56 -04:00

Owner

Copy link

grep -rn "ceiling|budget" proof-rs/crates/**/*.rs   ->   (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:

tier	nominal
Automation	50 µJ
Smt	5,000 µJ
SmallModel	500,000 µJ
BigModel	50,000,000 µJ

An unbounded cascade escalates a goal nobody wanted solved that badly straight into the most expensive rung and reports the bill afterwards. That is accounting, not control.

The design

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 BigModel that is 50 J of frontier inference for a goal whose owner had already declared it wasn't 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" — different claims about the world, and the second says nothing whatever about whether the goal is provable. halted_at records the refused tier so an exhausted wallet cannot read as a result.
• A budget halt is not a refutation, 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. A coherent request, not an error.

The receipt

ceiling_uj is sealed when one was declared, upgrading a proved receipt from "this cost N" to "this was obtained under a declared budget of C and cost N" — the difference between reporting a cost and honouring a limit.

Omitted when absent, so an unbounded run canonicalizes to exactly the bytes it always did. C6 asserts that directly (ceiling_uj must be absent, not a null) rather than leaving it to trust.

Batch accounting counts budget halts separately from failures, for the same reason as the first bullet: folding them together makes a batch look mathematically harder than it was.

Verification

• 34 workspace tests pass.
• Conformance passes all 10 classes, including the new C6 joule ceiling.
• Published vectors unchanged on disk — git status proof/conformance/ is clean.
• No new clippy warnings; the two in meter.rs are pre-existing and that file is untouched.

---

Second commit: two soundness bugs that were hiding each other

Found by running the shipped ladder on a real statement rather than reading it. Each 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:

$ printf 'every even integer greater than 2 is the sum of two primes\n(check-sat)\n' | z3 -in -smt2
(error "line 1 column 1: invalid command, '(' expected")
sat

run_z3 scanned for the first line equal to sat|unsat|unknown and skipped the error line. sat maps to Verdict::Refuted.

So "I could not understand the goal" became "the goal is FALSE" — and since a refutation is terminal in this cascade, that was final. Feeding it Goldbach's conjecture returned refuted: true with 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 with a substantive counter-model. A script asserting nothing is trivially satisfiable, so sat from an empty stack means "no constraints", not "here is a counter-example". The shape guard alone misses this — (check-sat) is well-formed SMT.

(The stderr(Stdio::null()) was a red herring — z3 writes these 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 it signs into a JCR-1 receipt that verifies under the steward key:

{"verdict":"proved","closed_by":"T3","artifact":"ad3091ab…",
 "energy_provenance":"Estimator","spec_grounding":"Ungrounded"}
   → 438 bytes, verifies = true

A signed attestation that Goldbach's conjecture is proved. 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.

• Solver::is_reference_stub() — declared by all four stand-ins
• CascadeResult::closed_by_stub — records whether the closing solver was one
• require_substantive_proof() — 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

Left open deliberately

closed_by_stub is not in the JCR-1 wire. 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 regenerates the entire conformance corpus. That is a decision about the standard, not an implementation detail, so it is flagged rather than taken quietly. Until then the marker is on the result and the check is available.

§5.2 also states plainly that the trait default is "not a stand-in" — the unsafe direction. It spares real solvers an opt-out, but makes the declaration a contract on the implementor rather than something the framework can infer.

Verification

38 workspace tests pass (4 new, pinning both bugs and the cache-laundering path); conformance passes all 10 classes; published vectors unchanged on disk.

``` grep -rn "ceiling|budget" proof-rs/crates/**/*.rs -> (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**: | tier | nominal | |---|---| | `Automation` | 50 µJ | | `Smt` | 5,000 µJ | | `SmallModel` | 500,000 µJ | | `BigModel` | 50,000,000 µJ | An unbounded cascade escalates a goal nobody wanted solved that badly straight into the most expensive rung and reports the bill afterwards. That is accounting, not control. ## The design `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 `BigModel` that is 50 J of frontier inference for a goal whose owner had already declared it wasn't 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"* — different claims about the world, and the second says nothing whatever about whether the goal is provable. `halted_at` records the refused tier so an exhausted wallet cannot read as a result. - **A budget halt is not a refutation**, 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.** A coherent request, not an error. ## The receipt `ceiling_uj` is sealed when one was declared, upgrading a proved receipt from *"this cost N"* to *"this was obtained under a declared budget of C and cost N"* — the difference between reporting a cost and honouring a limit. Omitted when absent, so an unbounded run canonicalizes to **exactly the bytes it always did**. C6 asserts that directly (`ceiling_uj` must be *absent*, not a null) rather than leaving it to trust. Batch accounting counts budget halts separately from failures, for the same reason as the first bullet: folding them together makes a batch look mathematically harder than it was. ## Verification - **34 workspace tests** pass. - **Conformance passes all 10 classes**, including the new **C6 joule ceiling**. - **Published vectors unchanged on disk** — `git status proof/conformance/` is clean. - No new clippy warnings; the two in `meter.rs` are pre-existing and that file is untouched. --- ## Second commit: two soundness bugs that were hiding each other Found by *running* the shipped ladder on a real statement rather than reading it. Each 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: ``` $ printf 'every even integer greater than 2 is the sum of two primes\n(check-sat)\n' | z3 -in -smt2 (error "line 1 column 1: invalid command, '(' expected") sat ``` `run_z3` scanned for the first line equal to `sat|unsat|unknown` and **skipped the error line**. `sat` maps to `Verdict::Refuted`. So *"I could not understand the goal"* became *"the goal is FALSE"* — and since a refutation is terminal in this cascade, that was final. Feeding it Goldbach's conjecture returned `refuted: true` with 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 with a **substantive counter-model**. A script asserting nothing is trivially satisfiable, so `sat` from an empty stack means "no constraints", not "here is a counter-example". The shape guard alone misses this — `(check-sat)` is well-formed SMT. *(The `stderr(Stdio::null())` was a red herring — z3 writes these 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 it signs into a JCR-1 receipt that verifies under the steward key: ```json {"verdict":"proved","closed_by":"T3","artifact":"ad3091ab…", "energy_provenance":"Estimator","spec_grounding":"Ungrounded"} → 438 bytes, verifies = true ``` A signed attestation that **Goldbach's conjecture is proved**. 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**. - `Solver::is_reference_stub()` — declared by all four stand-ins - `CascadeResult::closed_by_stub` — records whether the **closing** solver was one - `require_substantive_proof()` — 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 ### Left open deliberately `closed_by_stub` is **not** in the JCR-1 wire. 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 regenerates the entire conformance corpus. That is a decision about the standard, not an implementation detail, so it is flagged rather than taken quietly. Until then the marker is on the result and the check is available. §5.2 also states plainly that the trait default is "not a stand-in" — the unsafe direction. It spares real solvers an opt-out, but makes the declaration a **contract on the implementor** rather than something the framework can infer. ### Verification 38 workspace tests pass (4 new, pinning both bugs and the cache-laundering path); conformance passes all 10 classes; **published vectors unchanged on disk**.

dcharlot added 1 commit 2026-08-26 08:50:56 -04:00

proof: give the cascade a joule ceiling (SPEC §5.1) ... 7597bc5aa9

`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).

dcharlot added 1 commit 2026-08-26 09:07:20 -04:00

proof: two soundness bugs that were hiding each other (SPEC §5.2) ... 0ad7ef9d67

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.

dcharlot changed title from proof: give the cascade a joule ceiling (SPEC §5.1) to proof: a joule ceiling, and two soundness bugs that were hiding each other 2026-08-26 09:07:52 -04:00

dcharlot merged commit f77908198f into main 2026-08-29 03:09:28 -04:00

dcharlot referenced this pull request from a commit 2026-08-29 03:09:29 -04:00

proof: a joule ceiling, and two soundness bugs that were hiding each other (#62)

dcharlot referenced this pull request from a commit 2026-08-29 11:34:06 -04:00

Merge origin/main into ar-1-on-main — reconcile the two stand-in markers

dcharlot referenced this pull request 2026-08-30 17:23:06 -04:00

proof: closed_by_stub rides in the signed receipt (SPEC §6.1) #72

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!62

No description provided.