open-standards/proof/SPEC.md

# 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.

A cache hit's zero is not a reading: nothing was metered to close it. Its
`energy_provenance` **MUST** be `Estimator`, never the grade of the solver that
closed the goal when it was first proved, so a hit can never be graded above the
proof it reuses or present a measured zero.

## 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.