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 (RAPL/NVML/SMC). REQUIRES a
  present measured figure.
- `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.

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.

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

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