e42c3d1c07
ns_to_uj prices an attempt at wall time × a fixed ~15 W that no host calibrated, and Propositional, Z3Smt, LeanVerifier and every Z3Server attempt that is not sealed as a tree reading graded that figure ModelBased. By the JCP ladder (SPEC §5.1) and the proof SPEC's own definition a model earns ModelBased by its calibration; an assumed power scaled by time is an estimate, so the figure claimed better provenance than how it was obtained. - proof-schema: Energy::estimator(uj), and Provenance docs that say a default or assumed parameter makes a figure Estimator. - proof-solvers: DEFAULT_ACTIVE_MILLIWATTS (15 W, same arithmetic) and wall_time_estimate; all four sites now Energy::estimator. The public Modelled / modelled_uj names are kept; their docs say estimate. - Tests that pinned the over-claim now pin Estimator: grade_attempt's unit tests, z3_tree.rs (server(), refuted goal, settle bound, cascade total [Estimator, HwShunt] -> Estimator, undeclared z3), and proof-cli tests/measure.rs (receipt "provenance Estimator", "stay Estimator"). New test: every wall-time rung (T0 proved/refused, one-shot z3, an absent Lean) is Estimator with no measurement. - proof-cli, proof-cascade, proof SPEC §5 / README, and joule-code-remediate (FormalOutcome docs, joule_fix's printed label) say Estimator. proof/conformance/v1 is unchanged: gen-vectors output is byte-identical (it seals the stand-in ladder's estimate_tier figures, never ns_to_uj). Co-Authored-By: Claude Opus 5.5 <[email protected]>
60 lines
8.1 KiB
Markdown
60 lines
8.1 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, their energy estimated from measured wall time (`Estimator`: wall time × a default ~15 W power that no host calibrated — not a hardware reading, and not a calibrated model): 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). The resident `z3` is the one rung read off hardware: where the kernel counts each process's CPU energy live (macOS), each decision is read off the resident `z3`'s own process tree, and the attempt is that reading (`HwShunt`) only when the reading saw nothing missing — no gap of any kind — the decision ran entirely in the tree, and the operator has declared that the `z3` it runs decides in its own process (`Z3Server::declared_self_contained`; `proof` reads `PROOF_Z3_SELF_CONTAINED=1`) — a tree reading cannot see work handed to a container, VM or remote solver, so a forwarding `z3` would read whole. Otherwise (a gapped reading, no declaration, a refutation whose counter-model a one-shot `z3` fetches outside the tree, Linux) it keeps the wall-time estimate and records why, beside the absolute path of the `z3` binary that ran. Each goal is decided as a fresh `z3` would decide it: the answer is read off the crate's own `(check-sat)` before an unpredictable per-goal end marker, an error anywhere is undecided, and the resident session is replaced after any goal that sets an option or is not answered cleanly. 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, and a goal's figure graded by the weakest of the attempts it sums), 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 runs a real proof on every spare core and returns its measured microjoules from the first live source — on macOS **this process's own CPU energy counter** (`proc_pid_rusage`'s `ri_energy_nj`, public API, no privilege), read before the workers start and after they are joined, so other processes are excluded by construction and no idle baseline is subtracted; else IOReport's Energy Model, read directly through its C API on Apple Silicon and bracketed against idle; on Linux RAPL's package counters, bracketed against idle — so the headline `joules per verified proof` can be a real reading, not only a model. A vendor or kernel counter's reading is graded `HwShunt` only while the counter is live for the domain it claims ([`SPEC.md`](SPEC.md) §5), and the meter checks that before it meters anything, by one rule for every source (the counter keeps advancing in at least 5 sample intervals, at least 4 of every 5, over at least 300 ms while the probe burns CPU): the process counter itself, every IOReport CPU energy rail the figure sums (`CPU Energy`, or each die's `DIE_<n>_CPU Energy`), every RAPL package counter the figure sums (`psys` is neither summed nor probed). Each figure carries its domain: the process counter's is this process's CPU energy only — not other processes, child processes, GPU, ANE or DRAM. Returns nothing where no source is live — the caller keeps its honestly-tagged estimate rather than inventing a figure.
|
||
- **`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 — like for like, charged only for the goals the cascade proved, with the all-goals figure and its goal count beside it — 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 the meter produces one, and prints which source metered it, its domain, and why each other source was not used; that needs a counter the meter has seen to be live. On the Macs measured so far (macOS 27.0.1, an M5 Max and an M3 Ultra) IOReport's CPU energy rail is frozen for an unprivileged reader, but this process's CPU energy counter is live, so `--measure` meters with it; the receipt still seals the cascade's own `Estimator` figure for the first goal. On Linux, RAPL's `energy_uj` is root-only on current kernels.
|
||
|
||
`cargo test --workspace` green; `cargo clippy --workspace --all-targets` is
|
||
warning-free for Linux, and on macOS reports two lints in proof-cascade's
|
||
IOReport FFI. The two bottom rungs decide for real, with energy estimated from
|
||
wall time (the resident `z3`'s decisions read off its own process tree where
|
||
that reading is whole and the `z3` declared self-contained); 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.
|