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), and batch energy accounting against a frontier-only baseline with the per-tier Amdahl breakdown.
• 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.

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.