13df129cb0
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]>
35 lines
1.7 KiB
Markdown
35 lines
1.7 KiB
Markdown
# Contributing to Proof
|
|
|
|
Proof is one of the [Transaction Science open standards](../README.md). The wire
|
|
format and the right to fork are public; Transaction Science is the steward, not
|
|
the proprietor.
|
|
|
|
## Ground rules
|
|
|
|
- **Reference code** (`proof-rs/`) is Apache-2.0. **Specification text**
|
|
(`SPEC.md`) is CC-BY-4.0.
|
|
- Rust toolchain is pinned by the repo `rust-toolchain.toml`. `cargo test
|
|
--workspace` MUST pass and `cargo clippy --workspace --all-targets` MUST be
|
|
warning-free.
|
|
- Any change to a wire structure (the `proof/1` receipt core, the canonical
|
|
encoding) requires regenerating and committing `conformance/v1/` (`cargo run -p
|
|
proof-conformance --bin gen-vectors -- conformance/v1`).
|
|
- A solver MUST NOT return `proved` without verifier acceptance, and MUST NOT
|
|
upgrade a goal's `spec_grounding` on its own. These are correctness and honesty
|
|
invariants, not style.
|
|
|
|
## The smallest valuable contributions
|
|
|
|
- **Real backends behind the `Solver` trait:** a Lean tactic runner at T0, CVC5
|
|
alongside `z3` at T1, a distilled in-domain prover at T2 — each reporting what
|
|
actually happened, with measured energy.
|
|
- **Measured energy:** a `HwShunt` backend (RAPL/NVML) so a solver reports
|
|
hardware-measured joules instead of a wall-time model.
|
|
- **Conformance:** adversarial negatives (a router that hides escalation waste, a
|
|
receipt sealed for an unproved goal, a provenance/measured mismatch), and
|
|
independent implementations certifying against `conformance/v1/`.
|
|
- **Spec-grounding tooling:** cross-checkers that earn a `CrossChecked` grounding
|
|
by comparing a statement against an independent encoding — the honest path the
|
|
standard refuses to let a prover shortcut.
|
|
|
|
Issues and PRs scope by the `proof` subdirectory tag.
|