# Proof v0.1 — A Carrier for Verified Work **Status:** v0.1.0 draft. **Licence:** specification text CC-BY-4.0; reference code Apache-2.0. A vendor-neutral standard for **energy-accounted formal verification**. A proof obligation is content-addressed; a solver is anything that can attempt one at a declared tier; a discharged obligation seals as a signed receipt that records which tier closed it and the joules it cost. The standard fixes the one axis the field leaves implicit — *joules per verified proof* — and makes it portable: any prover can emit a Proof receipt, and any auditor can verify it with the family's shared JCR-1 tooling. --- ## 1. Scope and doctrine 1. **Correctness is the verifier's, not the optimizer's.** A solver returns `proved` only when a verifier would accept the artifact. Energy is never traded for correctness; the standard changes *which tier pays* for a proof, not whether it is checked. 2. **Cheapest sufficient solver wins.** Every obligation goes to the cheapest tier that can discharge it and escalates only on failure (§4). 3. **Energy is reported, honestly.** Every closed obligation carries the joules it cost with a provenance tag (§5). An estimate is never dressed as a measurement. 4. **A proof is not a specification.** A receipt attests that an obligation was discharged. Whether the *statement* encodes what was meant is a separate, declared property (`spec_grounding`, §2) that a prover MUST NOT self-certify. 5. **Non-goals.** The standard does not mandate a proof language, a solver implementation, or a model. It standardizes the *goal*, the *cascade accounting*, and the *receipt* — not the prover. ## 2. The proof obligation (REQUIRED) A **goal** is `{ statement, context, kind, intent, grounding }`: - `statement` — the formal proposition, in some `context` (e.g. `lean4@mathlib`, `smt2`). The pair `(statement, context)` is the unit of identity. - `kind` — a coarse difficulty hint (`Trivial`, `Arithmetic`, `Decidable`, `General`, `Hard`). It informs but does not bind routing. - `intent` — free text: what the statement is *meant* to encode. - `grounding` — the **spec-grounding** of the statement against intent: `Ungrounded` (default), `HumanReviewed`, or `CrossChecked`. A conforming prover MUST default to `Ungrounded` and MUST NOT upgrade grounding on its own. A goal's **id** is `blake3(statement ‖ 0x00 ‖ context)` (§3). Identity depends on the statement and context only; `intent` and `grounding` do not change it. ## 3. Canonical serialization and content addressing (REQUIRED) Content addresses and the signed receipt core use **canonical det-CBOR** (RFC 8949 §4.2.1): length-first then bytewise key ordering, shortest integer form, and **no floats, bools, or nulls** in the signed core. A content id is `blake3(canonical_cbor(value))`, rendered lowercase-hex on the wire. This is the same canonical encoding the JCR-1 receipt signs over (§6), so an id and a receipt agree on bytes. ## 4. The cascade (REQUIRED) Solvers occupy a strictly ordered ladder, cheapest first: | Tier | Class | Energy (reference) | |---|---|---| | **T0** | deterministic automation (proof-language tactics) | ~free CPU | | **T1** | SMT / decision procedures | cheap CPU | | **T2** | a small distilled in-domain prover | a small model | | **T3** | a frontier reasoning model — last resort | the most expensive rung | A conforming router MUST: 1. Attempt solvers in non-decreasing tier order. 2. Stop at the first solver returning `proved` (the **closing tier**). 3. Account **every** joule spent, including on cheaper solvers that ran and failed first. Those joules are `wasted_uj` — the **disclosed cost of escalation**, which MUST NOT be hidden. 4. Treat a solver's refusal (it cannot decide the goal) as escalation, never as a counter-result. A solver MUST NOT report `proved` without verifier acceptance. The reference energy per tier (`50 µJ / 5 mJ / 0.5 J / 50 J`) is non-normative. The normative requirement is that the figure is *reported and honestly tagged* (§5), not its value. ## 5. Energy and provenance (REQUIRED) Every reading is integer microjoules with a provenance tag: - `HwShunt` — read from a hardware energy interface: a shunt or power meter, the SMC, or a vendor energy counter (RAPL, NVML, Apple IOReport, ...). REQUIRES a present measured figure. A vendor counter's reading is a hardware reading, subject to the liveness requirement below. - `ModelBased` — computed from a calibrated per-operation model (e.g. measured wall time × a power model). A measured figure MAY be absent. - `Estimator` — a coarse constant. A measured figure MUST be absent. A conforming implementation MUST enforce this coupling: `HwShunt` without a measured figure, or `Estimator` with one, is invalid. **Liveness.** A reading from a vendor energy counter (RAPL, NVML, Apple IOReport, ...) MAY be graded as a hardware reading only while the counter is demonstrably live for the domain the figure claims: the implementation MUST have observed the counter covering that domain advance under load (for Apple IOReport: every CPU energy rail the figure sums - the rail itself, one per die on a multi-die part - advancing on its own in at least 5 sample intervals, in at least 4 of every 5, over at least 300 ms while the probing thread burns CPU; one rail that held leaves the whole figure not live). A counter that is present but not live - frozen, or republished in lumps - MUST NOT produce a hardware-graded figure; the implementation falls back to its estimator or reports the work unmetered, and SHOULD record why. In this standard a hardware-graded figure is `HwShunt`; the fallback is `ModelBased` or `Estimator`. Batch accounting reports, against a **frontier-only baseline** (every goal costed at T3), the total joules, the savings, and the energy attributed to each *closing* tier. The per-tier breakdown is REQUIRED so that Amdahl behaviour — the few hardest goals dominating the joules — is visible rather than averaged away. ### 5.1 The joule ceiling (OPTIONAL to declare, REQUIRED to honour) Accounting says what a proof cost. A **ceiling** says what it is allowed to cost. A standard whose premise is joules-per-verified-proof needs both: the ladder spans a millionfold from `T0` to `T3`, so an unbounded cascade will escalate a goal nobody wanted solved that badly into the most expensive rung available and report the bill afterwards. A caller MAY declare a ceiling in microjoules for a run. Where one is declared: - An implementation **MUST NOT** begin a rung whose nominal cost would take the run past the ceiling. The check is on the **next rung's cost, before it runs**. Refusing after the fact spends precisely the joules the ceiling exists to withhold. - A ceiling below the cheapest rung's nominal cost attempts nothing and reports that it attempted nothing. This is a coherent request, not an error. - A run halted for want of budget **MUST** be distinguishable from a run no rung could decide. `proved = false` alone conflates them, and the two are different claims about the world: a budget halt says nothing whatever about whether the goal is provable. An implementation MUST record the tier it refused. - Actual spend MAY exceed the ceiling when a solver overshoots its nominal cost. Those joules were really spent, so the receipt **MUST** report them as spent rather than clamping to the budget. A ceiling bounds what is *attempted*, not what physics did. - Batch accounting **MUST** count budget halts separately from failures, for the same reason: folding them together makes a batch look mathematically harder than it was. Where a ceiling was declared, the receipt (§6) carries it, so a proof is not merely costed but demonstrably obtained *within a declared budget*. A receipt from a run with no ceiling omits the field and is byte-identical to one sealed before this section existed. ### 5.2 Stand-in solvers (REQUIRED to declare) A **reference stand-in** is a solver that returns a verdict to exercise the ladder and discharges nothing — it decides by goal *kind*, never by inspecting the claim. The reference implementation ships a full ladder of them so the cascade, the accounting and the receipt can be demonstrated without a solver estate. They are a hazard precisely because the rest of the pipeline is sound. A stand-in at the top rung returns `Proved` for **any** goal, with the content address of the goal's own statement as its "artifact" — the claim offered as its own evidence — and the sealing path will sign that into a JCR-1 receipt that verifies under the steward key. Such a receipt is not forged. It is honestly signed and substantively empty, which is worse, because it verifies. Neither existing qualifier catches this. `Provenance` qualifies an attempt's *energy*; `SpecGrounding` qualifies its *intent*. Neither says whether the verdict was earned. - A solver that is a stand-in **MUST** declare itself as one. - An implementation **MUST** record, on the result and through any proof cache, whether the **closing** solver was a stand-in. A cache hit that dropped the marker would launder an unearned proof into an unmarked one. - A relying party that will act on a proof **MUST** check it. Verifying the envelope establishes the signature, not that anything was proved. The marker therefore rides in the signed receipt as `closed_by_stub` (§6.1), so a party holding only the artifact can make that check without trusting the prover. - A stand-in **MUST NOT** be presented as a decision procedure in any published figure or claim derived from a run. Note the trait-level default is "not a stand-in", which is the unsafe direction and is deliberate: it keeps real solvers from having to opt out, but it means the declaration is a **contract on the implementor**, not a property the framework can infer. A new stand-in that forgets to declare itself is indistinguishable from a real one. ## 6. The receipt (REQUIRED) A discharged obligation seals as a **JCR-1** receipt — the family's shared signed-receipt envelope: canonical det-CBOR inside a COSE_Sign1 envelope (RFC 9052, EdDSA/Ed25519, `alg = -8`). The `proof/1` profile signs a flat uint/text core: ``` proof_receipt = "proof/1" goal_id = hex(blake3(statement ‖ 0x00 ‖ context)) verdict = "proved" | "unproved" closed_by = "T0".."T3" ; omitted if unproved artifact = hex(content-id) ; omitted if unproved total_uj = uint ; all joules, incl. escalation wasted_uj = uint ; joules on failed cheaper attempts baseline_uj = uint ; frontier-only cost of this goal energy_provenance = "HwShunt" | "ModelBased" | "Estimator" spec_grounding = "Ungrounded" | "HumanReviewed" | "CrossChecked" from_cache = 0 | 1 closed_by_stub = 1 ; omitted when the closer was real (§5.2) ceiling_uj = uint ; omitted when the run was unbounded steward = the signer's id (the COSE kid) ``` A conforming implementation MUST refuse to seal a receipt for an `unproved` goal, and MUST carry `spec_grounding` so a receipt for an `Ungrounded` statement says, in the signed artifact itself, that the statement was not validated against intent. Proof receipts are byte-compatible with the family's JCR-1 verifiers. ### 6.1 `closed_by_stub` — the verdict's own qualifier An implementation MUST emit `closed_by_stub = 1` when the rung that closed the goal was a reference stand-in (§5.2), and MUST omit the field otherwise. §5.2 already requires a relying party to check this before acting on a proof. Until it entered the signed core the marker lived only on the in-process result, so a party holding **only the receipt** — which is the entire purpose of sealing one — could not perform the check the specification asks of them. A verifier that must consult the prover to learn whether a proof is real is not a verifier. `closed_by` does not answer this. It names a **tier**, and the same tag covers a real decision procedure on one ladder and a stand-in on another; `T0` is a propositional decider in a real ladder and a `GoalKind` gate in the reference one. Nor do the other qualifiers: `energy_provenance` qualifies the *energy* and `spec_grounding` the *intent*. This is the only field that says whether the **verdict** was earned. Omit-when-false is normative, not an optimization. It makes the field free for honest proofs: a receipt closed by a real solver canonicalizes to exactly the bytes it did before this field existed, so every such receipt sealed under an earlier revision still verifies. The byte cost falls only on receipts that were making an unearned claim. ## 7. The cache (RECOMMENDED) A verified proof SHOULD be memoized by goal id. An identical goal then closes for **zero new joules** (`from_cache = 1`, `total_uj = 0`), and the accumulating corpus of verified proofs — not the routing — is the durable asset. The cache is the energy flywheel: the more proved, the cheaper future proofs become. ## 8. Conformance A conforming implementation passes, with real checks: - **C1 — cheapest-sufficient routing:** each goal closes at the cheapest tier that can discharge it. - **C2 — disclosed escalation:** `total_uj` equals the sum of all attempts, and `wasted_uj` is exactly the joules of cheaper attempts that failed first. - **C3 — energy honesty:** the ladder is strictly monotone; the batch is accounted against a frontier-only baseline with non-negative savings. - **C4 — the flywheel:** re-proving an identical goal costs zero new joules. - **C5 — the receipt:** a proved result seals to JCR-1 and verifies; a wrong steward fails. - **C-neg:** provenance coupling is enforced; an unproved goal cannot be sealed; a tampered envelope fails; canonical CBOR rejects floats/bools. Published vectors live in [`conformance/v1/`](conformance/v1/) (`cargo run -p proof-conformance --bin gen-vectors`). ## 9. Non-goals The standard does not certify a prover's *capability*, does not validate that a statement encodes a real-world requirement (that is the `spec_grounding` axis, owned by humans), and does not prescribe a model or a proof language. Efficiency diffuses; the standard's contribution is to make the joules portable and the spec-grounding honest, so that "verify every line" can be reasoned about as a cost, not a slogan.