| Filename | Latest commit message | Latest commit date |
|---|---|---|
7597bc5aa9
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). |
||
| .. | ||
| bin | ||
| lib.rs | ||
| main.rs | ||