open-standards/proof

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 (the JouleProof pillar is the steward + services layer over this standard).
• Licence: Apache-2.0 for reference code (see LICENSE); CC-BY-4.0 for specification text (see LICENSE-SPEC).
• Status: v0.1.0 draft. Specification core published (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.