| Filename | Latest commit message | Latest commit date |
|---|---|---|
0ad7ef9d67
All checks were successful
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 3s
Found by running the shipped ladder on a real statement instead of reading it.
Each bug masked the other, so fixing the first exposed the second.
**1. Any non-SMT goal was reported as REFUTED.**
`Z3Smt` piped `goal.statement` — an arbitrary string — straight into `z3 -in
-smt2`. z3 reports a parse failure as `(error "...")` on STDOUT, then answers
`(check-sat)` anyway, against an assertion stack that is empty because nothing
parsed. That answer is `sat`, and `run_z3` scanned for the first line equal to
`sat|unsat|unknown` and skipped the error line entirely. `sat` maps to
`Verdict::Refuted`.
So "I could not understand the goal" became "the goal is FALSE" — and because a
refutation is terminal in this cascade, that was final. Feeding it Goldbach's
conjecture returned `refuted: true` with the counter-model `"(\n)"`. Three
fixes, because each catches a case the others miss:
- an `(error` anywhere in z3's output makes the run undecided, never a verdict;
- `Z3Smt` now applies the same `looks_like_smt` shape guard the resident
`Z3Server` already had — one call site had simply been missed;
- a `sat` becomes a refutation only when a substantive counter-model exists. A
script asserting nothing is trivially satisfiable, so `sat` from an empty
assertion stack means "no constraints", not "here is a counter-example". The
shape guard alone would not catch this: `(check-sat)` is well-formed SMT.
Note the stderr redirect was a red herring — z3 writes these errors to stdout.
**2. With the false refutation gone, the cascade reaches a rung that proves
anything.**
`FrontierModel` (T3) returns `Proved` for every goal, and the "artifact" is
`ContentId::of_bytes(goal.statement)` — the claim offered as its own evidence.
`seal()` gates only on `proved`, so this signs into a JCR-1 receipt that
verifies under the steward key. The demonstration is a 438-byte receipt
asserting `verdict: "proved", closed_by: "T3"` for Goldbach's conjecture. It is
not forged; it is honestly signed and substantively empty, which is worse,
because it verifies.
Neither existing qualifier catches it: `Provenance` qualifies an attempt's
energy, `SpecGrounding` its intent, and neither says whether the verdict was
earned. So `Solver::is_reference_stub()` is now declared by all four
stand-ins, `CascadeResult::closed_by_stub` records whether the **closing**
solver was one, and `require_substantive_proof()` is the relying-party check.
The proof cache persists the marker, because a cache hit that dropped it would
launder an unearned proof into an unmarked one.
`closed_by_stub` is deliberately NOT in the JCR-1 wire yet. Every published
vector is generated from the all-stand-in `reference_ladder()` — including an
`("open conjecture", Hard)` case sealed as proved at T3 — so encoding it would
regenerate the entire conformance corpus. That is a decision about the standard
rather than an implementation detail, and it is left open rather than taken
quietly. Until it is, the marker is on the result and the check is available.
The trait default is "not a stand-in", which is the unsafe direction, and §5.2
says so plainly: it spares real solvers an opt-out, but it makes the declaration
a contract on the implementor rather than something the framework can infer.
Verified: 38 workspace tests pass (4 new soundness tests pinning both bugs and
the cache-laundering path), conformance passes all 10 classes, published vectors
unchanged on disk.
|
||
| .. | ||
| conformance/v1 | ||
| proof-rs | ||
| CONTRIBUTING.md | ||
| LICENSE | ||
| LICENSE-SPEC | ||
| README.md | ||
| SPEC.md | ||
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 (seeLICENSE-SPEC). - Status: v0.1.0 draft. Specification core published (
SPEC.md); reference workspaceproof-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/Estimatorwith the coupling enforced),SpecGrounding, the verdict, and theSolvertrait 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, andz3(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_ujdisclosed), 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— theHwShuntbackend): it brackets a real proof, run on every core, against an idle baseline using the platform's energy interface (IOReport viamacmonon Apple Silicon, RAPL on Linux) and returns measured microjoules, so the headlinejoules per verified proofcan be a real reading, not only a model. Returns nothing where no interface is reachable — the caller keeps the honestly-taggedModelBasedfigure rather than inventing one.proof-receipt— theproof/1JCR-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 inconformance/v1/.proof-cli— theproofreference 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 --measureadds 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_groundingrides in the signed receipt;Ungroundedis 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.