Transaction-Science/open-standards
Watch
1
0
Fork
You've already forked open-standards
 0
Code Issues Pull requests Projects Releases 15 Packages Wiki Activity Actions 1
open-standards/proof/README.md
Transaction Science 13df129cb0 Add the proof open standard — a carrier for verified work 
The verification cargo class: energy-accounted formal verification as a
vendor-neutral standard. A proof obligation is content-addressed; a solver
attempts one at a declared tier; a discharged obligation seals as a signed
JCR-1 receipt recording which tier closed it and the joules it cost. The
cheapest sufficient solver wins, correctness stays the verifier's, and the
joules a cheaper solver spent before failing are disclosed, never hidden.

- SPEC.md (§1–§9): the obligation, canonical det-CBOR addressing, the
  cheapest-sufficient cascade with disclosed escalation, the honest
  energy/provenance model, the proof/1 JCR-1 receipt, the cache, conformance.
- proof-rs/: a 6-crate Apache-2.0 reference workspace. Two real rungs with
  measured energy — an in-process propositional decider (T0) and z3, shelled
  or kept resident (T1) — over honest model-tier stand-ins; the escalation
  router with the proof-cache flywheel and frontier-only baseline accounting;
  the proof/1 receipt vendored byte-compatible with the family JCR-1 verifiers;
  C1–C5 + a negative pack, all checks real, with published vectors.
- proof carries spec_grounding in the signed receipt: a proof is not a
  specification, and a prover may never self-certify that the statement
  encodes intent.

cargo test --workspace green; cargo clippy --workspace --all-targets clean.
JouleProof (jouleproof.transaction.science) is the steward + services layer
over this standard.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
2026-06-07 15:30:07 -04:00

4.3 KiB
Raw Permalink Blame History

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.