0503e69b32
All checks were successful
standards workspaces build + test / jouleclaw-rs (pull_request) Successful in 1m57s
standards workspaces build + test / aac-rs (pull_request) Successful in 39s
standards workspaces build + test / joule-code-rs (pull_request) Successful in 38s
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 37s
standards workspaces build + test / map-rs (pull_request) Successful in 31s
standards workspaces build + test / mesh-rs (pull_request) Successful in 28s
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 3s
standards workspaces build + test / openpay (pull_request) Successful in 1m41s
standards workspaces build + test / eoc-rs (pull_request) Successful in 1m49s
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m17s
standards workspaces build + test / proof-rs (pull_request) Successful in 1m11s
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m7s
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 2m33s
standards workspaces build + test / arl-rs (pull_request) Successful in 5m52s
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 5m24s
standards workspaces build + test / jouledesk-rs (pull_request) Successful in 4m25s
standards workspaces build + test / joulehook-rs (pull_request) Successful in 10m23s
standards workspaces build + test / sense-rs (pull_request) Successful in 7m31s
standards workspaces build + test / macOS energy backend (jcp-energy) (pull_request) Successful in 4m38s
The IOReport watch, `CPU_RAILS`, was "any one": Live as soon as ONE CPU rail
met the sustained-advance rule. The power reading sums every CPU rail
(`counts_once`), and on a multi-die part that is two rails, `DIE_0_CPU
Energy` and `DIE_1_CPU Energy` on an M3 Ultra. So one die live beside a
frozen one would have admitted the meter and bracketed one die's energy as
the whole CPU's, as `HwShunt`. RAPL was already held to every package
counter it sums (9334ec0c); IOReport now is too.
The rule: Live only when every CPU rail present in the samples advanced in
at least five intervals, in at least 80% of those observed, over at least
300 ms; Frozen otherwise; Absent with no CPU rail. A rail is present if it is
in any sample, the first included (the watch already registered every
sample's rails; a test now pins it), and is judged over every interval
observed. With every source on the same rule there is nothing for
`Watched.every` to choose, so the field is gone: a `Watched` is which
channels to watch, and the watch needs every one of them.
Two test-side checks encoded the old rule and now encode this one: the
oracle behind the real-IOReport tests says "moved" only when every CPU rail
it reads changed at five reads or more and at 80% of them, and
`assert_verdict_matches_record`, the tests' own reading of a probe record,
calls a run Live only when every CPU rail seen, the first sample's included,
rose in at least 5 intervals at 80% over 300 ms. The oracle reads exactly the
probe's rails on both hosts: one on this M5 Max, the two dies on the M3
Ultra.
Docs: the meter module doc, `IoReportStatus`, `CpuRail`, `Watched`,
`CPU_RAILS`, `RailWatch` and `PACKAGES`; SPEC §5's liveness clause (for
IOReport, every CPU rail the figure sums, one per die, must advance on its
own); the proof README.
Tests, all scripted (macOS here). The rule:
`watch_two_dies_that_both_keep_advancing_is_live` (live at the tenth
interval, or at the fifteenth when one die misses its first three, either
die), `watch_one_die_that_keeps_advancing_beside_a_frozen_one_is_frozen` (the
other die held, stepped once, stepped five times, or advanced three
intervals in five, either die; and twin `CPU Energy` channels),
`watch_one_die_alone_that_keeps_advancing_is_live`, and
`watch_a_die_in_only_some_samples_is_a_rail_the_watch_needs`. The whole probe
loop: `the_probe_needs_every_die_to_keep_advancing`. The real `host_status()`
on scripted reads: `host_status_calls_two_dies_that_keep_advancing_live` and
`host_status_calls_one_live_die_beside_a_frozen_one_frozen`. The single-rail
tests are unchanged. Two existing tests encoded "any one":
`two_advances_of_the_same_rail_are_not_live_and_sustained_ones_are` held
DIE_0 constant and expected Live from DIE_1 alone, so DIE_0 now advances at
every interval and the verdict is still DIE_1's; and
`rapl_every_package_counter_must_keep_advancing` drops its contrast with the
any-one-rail watch, which no longer exists.
proof-cascade: 86 lib tests and the three integration files pass on this M5
Max. The same lib test binary passes 86/86 on the M3 Ultra (macOS 27.0.1),
where the real probe gave `CpuRailFrozen` over 25 and 26 intervals and the
oracle saw 0 changes on both dies in 19 reads. `cargo test --workspace`
passes (126 tests) and the proof-conformance binary passes all 10 checks.
Clippy adds nothing for aarch64-apple-darwin (two warnings in the IOReport
FFI predate this) and is clean for x86_64-unknown-linux-gnu.
Falsified, each restored from git and the suite re-run green: the rule back
to any one rail fails the one-live-die-beside-a-frozen-one tests (rule, loop
and `host_status`), the two-live-dies test, the some-samples test, the
updated two-advances test and the RAPL every-package test; registering a
rail only once an interval has closed fails
`watch_a_die_in_only_some_samples_is_a_rail_the_watch_needs`.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
59 lines
6.4 KiB
Markdown
59 lines
6.4 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 modeled from measured wall time (`ModelBased`, a ~15 W power model — not a hardware reading): 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's Energy Model, read directly through its C API on Apple Silicon and used only while every CPU energy rail is live, one per die on a multi-die part; RAPL's package counters on Linux, used only while every one is live) and returns measured microjoules, so the headline `joules per verified proof` can be a real reading, not only a model. A vendor 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 brackets anything, by one rule on both platforms (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): on Apple Silicon for every IOReport CPU energy rail the figure sums (`CPU Energy`, or each die's `DIE_<n>_CPU Energy`), on Linux for every RAPL package counter the figure sums (`psys` is neither summed nor probed). Returns nothing where no interface is reachable or its counter is not live — 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 — 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; that needs a counter the meter has seen to be live (on Apple Silicon every IOReport CPU energy rail, on Linux every RAPL package counter). 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, so `--measure` declines there, says why, and leaves every figure `ModelBased`; 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 modeled from
|
||
wall time; 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.
|