858d029e76
The schema has always promised a HwShunt provenance (a true hardware reading, the strongest tier) but nothing produced one — the solvers reported ModelBased (wall time × a power model). Add proof-cascade::meter: it brackets a real proof, run on every spare core, against an idle baseline using the platform's energy interface (IOReport via macmon on Apple Silicon, RAPL energy_uj on Linux) and returns the marginal microjoules of one proof. No interface reachable ⇒ None, so the caller keeps the honestly-tagged ModelBased figure rather than inventing a number; multi-thread saturation is what clears a loaded machine's noisy idle baseline (a single thread vanishes into it). `proof --measure` meters a real, non-trivial T0 proof — validity of a 16-variable propositional tautology by the actual truth-table decider (2^16 rows), genuine parallelizable compute — and reports measured joules-per-proof with HwShunt provenance + measured_uj present. The standard's headline (joules per verified proof) is now a real reading, not only a model. Measured ~50 mJ on an M-series box. Co-Authored-By: Claude Opus 4.8 <[email protected]>
57 lines
5 KiB
Markdown
57 lines
5 KiB
Markdown
# proof — A Carrier for Verified Work
|
||
|
||
The verification cargo class of the substrate. 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 **JCR-1 receipt** that records
|
||
which tier closed it and the joules it cost. The standard fixes the one axis the
|
||
theorem-proving 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 same tooling as a Map, Sandbox, or Joule Code receipt.
|
||
|
||
The cheapest sufficient solver wins. Every obligation goes to the cheapest rung
|
||
that can discharge it — deterministic automation (T0), then SMT (T1), then a
|
||
small distilled prover (T2), then a frontier model (T3, last resort) — and
|
||
escalates only on failure. Correctness is never traded for energy: a solver
|
||
returns `proved` only when a verifier would accept the artifact, so the standard
|
||
changes *which tier pays* for a proof, not whether it is checked. The joules
|
||
spent on a cheaper solver that ran and failed first are **disclosed** as the cost
|
||
of escalation, never hidden. Energy carries an honest provenance tag
|
||
(`HwShunt` / `ModelBased` / `Estimator`), and a receipt for an `Ungrounded`
|
||
statement says, in the signed artifact, that the statement was never validated
|
||
against intent — *a proof is not a specification.*
|
||
|
||
- **Site:** [jouleproof.transaction.science](https://jouleproof.transaction.science) (the JouleProof pillar is the steward + services layer over this standard).
|
||
- **Licence:** Apache-2.0 for reference code (see [`LICENSE`](LICENSE)); CC-BY-4.0 for specification text (see [`LICENSE-SPEC`](LICENSE-SPEC)).
|
||
- **Status:** v0.1.0 draft. Specification core published ([`SPEC.md`](SPEC.md)); reference workspace `proof-rs/`.
|
||
|
||
## What's here
|
||
|
||
```
|
||
proof/
|
||
├── SPEC.md — the normative standard (§1–§9)
|
||
├── conformance/v1/ — published vectors (receipt wire + signed core + envelope)
|
||
└── proof-rs/ — the Apache-2.0 reference implementation
|
||
```
|
||
|
||
### The reference implementation (`proof-rs/`)
|
||
|
||
- **`proof-schema`** — the content-addressed goal (`blake3(statement‖0x00‖context)`), the cheapest-first tier ladder, the honest energy model (`HwShunt`/`ModelBased`/`Estimator` with the coupling enforced), `SpecGrounding`, the verdict, and the `Solver` trait every backend implements. Canonical det-CBOR content addressing.
|
||
- **`proof-solvers`** — two **real** rungs with measured energy: a propositional decider (T0) that parses a boolean goal and decides validity by truth-table in process, and `z3` (T1) — shell or kept **resident** across goals — that decides an SMT-LIB goal (assert the negation; `unsat` ⇒ valid). Each refuses rather than fakes, so the router escalates. The model rungs (T2/T3) are honest stand-ins behind the same trait.
|
||
- **`proof-cascade`** — the escalation router (every joule accounted, `wasted_uj` disclosed), the content-addressed proof cache (the energy flywheel, durable as line-delimited JSON), batch energy accounting against a frontier-only baseline with the per-tier Amdahl breakdown, and a **real hardware energy meter** (`meter` — the `HwShunt` backend): it brackets a real proof, run on every core, against an idle baseline using the platform's energy interface (IOReport via `macmon` on Apple Silicon, RAPL on Linux) and returns measured microjoules, so the headline `joules per verified proof` can be a real reading, not only a model. Returns nothing where no interface is reachable — the caller keeps the honestly-tagged `ModelBased` figure rather than inventing one.
|
||
- **`proof-receipt`** — the `proof/1` JCR-1 receipt: canonical det-CBOR + COSE_Sign1/EdDSA, vendored byte-compatible with the family's cross-language verifiers; refuses to seal an unproved goal.
|
||
- **`proof-conformance`** — C1–C5 + a negative pack, all checks real, published vectors in `conformance/v1/`.
|
||
- **`proof-cli`** — the `proof` reference demo: a proof workload reporting joules-per-proof against a frontier-only baseline, the Amdahl breakdown, the cache flywheel, and a sealed + verified receipt. `proof --measure` adds a **real hardware reading** of a non-trivial T0 proof (`HwShunt`, where an energy interface is present).
|
||
|
||
`cargo test --workspace` green; `cargo clippy --workspace --all-targets`
|
||
warning-free. The two bottom rungs decide for real with measured energy; the
|
||
model rungs are honestly marked as stand-ins until inference backends are wired.
|
||
|
||
## Honesty the standard records
|
||
|
||
- **A proof is not a specification.** `spec_grounding` rides in the signed
|
||
receipt; `Ungrounded` is the default and a prover may never self-certify it.
|
||
- **The multiple shrinks with difficulty.** The accounting reports energy per
|
||
closing tier, so the few hardest goals dominating the joules (Amdahl) is
|
||
visible, not averaged away.
|
||
- **Energy is reported at all** — per proof, with an honest provenance tag —
|
||
which the field otherwise leaves to be inferred from device-days.
|