06f00e619a
Two things asked for: a benchmark corpus, and a second verification method. ## The corpus The wire vectors certify that an implementation round-trips a receipt's bytes. They say nothing about whether it reached the right verdict, because they carry one scenario. `conformance/v1/evaluation/` is the other half: ten cases, each a complete set of evaluation inputs plus the verdict §3 requires, chosen so a plausible but generous implementation disagrees — a mean where a minimum is required, an unevidenced obligation skipped rather than emptying the grade, `E3` on a killed counter-artifact whose anchor is unstated, `E4` because a prover succeeded, a witness for a clause's previous wording discarded instead of flagged, a `reviewed` label taken at face value when the reviewer is the clause's own author. Each case states its direction. Most catch over-grading; one catches under-grading, and that one is load-bearing: an implementation that graded nothing at all would pass every over-grading case, so a corpus with one direction rewards a rule that refuses everything. A test asserts the shape of the set rather than trusting it was built as described. The expectations are written by hand from §3 and are never read back out of this implementation — a corpus whose expectations are whatever the code produced certifies agreement with itself. That earned its keep immediately: seven of the ten were wrong on first authoring, all the same mistake and mine rather than the evaluator's. They assumed the attestation axis came from who signed a witness, where §2.8 computes it from who authored the work; with no work declared it is absent. The fix was not to copy the observed value in, which would have buried the misunderstanding, but to declare work in every case so the axis is exercised at all. ## What a second method bought, and what it did not The quotient-bound statement abandoned in the previous commit was retried under a solver reasoning with a bitvector theory rather than bit-blasting to a propositional problem. It settled four of the statement's conditions in about eight seconds — where the default engine had shown no per-property progress in twenty-four minutes — and then spent over fifty minutes on the fifth. So the method moved the wall without removing it, and §8 now says that instead of implying a solver choice would fix it. The harness is kept as the reproducible record of a negative result, behind a `cfg` nobody sets so an ordinary run does not hang on it. A second finding from the same runs, recorded in `conformance/v1/README.md`: a wall-clock wrapper around a prover is not enough. Both abandoned runs outlived the `timeout` meant to bound them, because the prover is a driver that spawns the checker and a timeout reaches only the driver. The producer kills the process group, which is why its budget works where the shell's did not — the design was right for a reason that has now been observed twice. Co-Authored-By: Claude Opus 5 <[email protected]>
9.5 KiB
JouleSpec conformance — v1
Two packs live here. They answer different questions and only one of them is reproducible, which is the first thing to know about them.
vectors/ — the certifiable surface
Fixed keys, fixed clauses, fixed witnesses and fixed energy, producing receipt bytes that must not change without a version bump. This is the pack the charter's conformance test refers to: an implementation certifies itself by round-tripping these files.
The witness set carries one of every rung the format can express — cited,
exercised, falsifiable, proved — plus a witness bound to an earlier
artifact state, so a verifier that mishandles staleness fails the pack rather
than passing it quietly. A pack that exercised one rung would certify one rung,
and a test asserts the coverage.
The verdict these bytes assert is worth reading, because it is the doctrine in
miniature: two obligations are well evidenced, one carries only the
implementer's citation, and the specification's grade is therefore E0.
The attestation is A0 for the same reason — the only surviving witness on
that clause is the implementer's own. One clause is a non-goal with no
evidence, which is correct and carries no grade, and a quarter of the declared
work energy cites no clause at all.
Regenerate with:
JOULESPEC_GEN_VECTORS=1 cargo test -p joulespec-core --test vectors
Without that variable the test asserts the committed bytes, so a change to the wire format fails in CI rather than shipping.
evaluation/ — the verdicts, not the bytes
The vectors certify that an implementation round-trips a receipt's bytes.
They say nothing about whether it reaches the right verdict, because they
carry one scenario. evaluation/ is the other half: cases whose
correct answer a too-generous implementation gets wrong, each with the inputs
to evaluate and the verdict §3 requires. Its
README says what each trap is and why the expectations
are written by hand rather than read back out of this implementation — a
distinction that caught seven authoring errors of mine while it was being
built.
The self-conformance record
spec.json, witnesses.json, state.json, receipt.cbor and receipt.json
in this directory are not vectors. They are the output of running the
reference producer against the reference implementation:
joulespec harvest --manifest conformance/v1/harvest.toml \
--out conformance/v1 --require-grade E3
The clauses are the conformance items of SPEC.md §7, read
from the published document rather than copied into the manifest — so the
manifest cannot drift from the specification. Reword an item and its obligation
address moves, and every witness bound to the old wording stops applying.
Each obligation is mapped to a check in joulespec-rs, and each mapping
declares a counter-artifact: a one-occurrence edit that should make that
check fail. The harvester applies it, runs the check, requires a failure,
and reverts. Only then does the witness reach E3.
Proofs, beside the checks
Two obligations also carry a proof, discharged by a bit-precise model
checker over the whole input domain rather than at sampled points. A proof
entry is distinguished in the manifest by carrying a formalization — the
binding from clause prose to formal statement — because §2.6 forbids a
producer formalizing a clause itself, and making the binding the thing that
selects the prover enforces that structurally rather than by a check someone
could forget.
The prover path refuses the same way the check path does, one rung up:
| Observed | Read as |
|---|---|
| verified, every declared cover satisfied | the statement holds over a non-empty domain |
| verified, a cover never reached | a finding — proved over a domain the harness's own assumptions emptied |
| a property violated | the refutation a counter-artifact is applied to obtain |
| undecided, or killed by the budget | a finding — neither verdict, and never credited as either |
The second row is why the producer parses the property table instead of the verdict line. A model checker reports success for an over-constrained harness in the same words it uses for one that examined everything, so a gate reading the verdict alone passes vacuous proofs. The fourth row is why each harness carries a wall-clock budget: a solver asked a question it cannot settle does not say so, it keeps going.
Both proofs sit at E2, not E4, and the report says so in those words.
Their statements were refuted against a counter-artifact, so the vacuity axis
is satisfied; what is missing is an independently cross-checked formalization.
Nobody but the author has confirmed that either statement says what its clause
says, and §2.6 caps that at E2. The rung is reachable by this producer — it
needs a second party, not more code.
What the proofs cost, and what they caught
The reason the ladder has a rung above E3 is visible here as a measurement
rather than an argument. The counter-artifact on C7 narrows the ratio rule's
arithmetic from 128 to 64 bits, where a large input overflows the
parts-per-million scale:
- the entire test suite passes under that mutation — 85 tests, none of
which reaches an input above roughly
u64::MAX / 1_000_000; - the prover refutes it in a fraction of a second.
That is E3 and E4 disagreeing on our own code, in the direction the ladder
predicts.
The cost is not uniform, and that matters more for budgeting than it might seem. The same function, the same input domain and the same solver gave:
- the statement that its arithmetic is total — no overflow, no division by zero — discharged in under a tenth of a second;
- the statement that its quotient is bounded by the scale — which requires reasoning about the output bits of a 128-bit division — did not converge in twenty-four minutes.
Naming a solver that reasons with a bitvector theory instead of bit-blasting
moved that wall without removing it: it settled four of the statement's
conditions in about eight seconds and then spent over fifty minutes on the
fifth. The harness is kept, behind a cfg nobody sets so an ordinary run does
not hang on it, as the reproducible record of a negative result.
Only the first is claimed. The second is named in the harness's own documentation as deliberately unstated, because a harness that quietly narrowed its domain until it converged would report exactly the same success over a much smaller claim. The lesson for an operator is that the top rung's affordability is a property of the statement and of the method together, neither of which the ladder mentions — which is why the budget is declared per harness and not once for a workspace.
A second lesson, from the same run: a wall-clock wrapper around the prover is
not enough. Both abandoned runs outlived the timeout that was supposed to
bound them, because the prover is a driver that spawns the checker and a
timeout reaches only the driver. The producer kills the process group,
which is why its budget works where the shell's did not.
These receipts are not reproducible, by construction. Their energy figures
come from a wall clock, graded Estimator, because no meter is wired to this
harness yet. Re-running the harvest produces different microjoules and
therefore different receipt bytes. That is the honest behaviour of a measured
quantity and the reason the certifiable pack above holds energy fixed.
What the harvest found
Running this against the implementation it describes did what the E3 rung
exists to do, and found two things inspection had not:
- A check that could not see its subject. One footprint test narrowed to a
single member, and on a one-element footprint
allandanyare the same function — so the conjunction itself was never checked. Mutatingalltoanyleft the test passing. A second test now covers it. - Dead logic in the implementation.
applies_atguarded on the artifact state having no enumerable parts, and that guard could not change a single verdict: anallover a non-empty footprint against no parts is already false. The guard looked like care. It is gone.
A third report was a mistake in the manifest rather than in the code — a counter-artifact aimed at a branch its check never takes, which the harvester correctly reported as a check that cannot see its subject. The distinction between those two readings is the operator's to make, and the harvester reports what it observed rather than guessing which it is.
A fourth finding came from extending this standard rather than from running it. Extracting two rules into named functions — so a prover could be asked about them — moved the text that two existing counter-artifacts were aimed at, by one indentation level in one case. Both mutations silently stopped describing any edit at all. The harvester refused to run, which is the correct outcome but a late one, so it now validates every counter-artifact's anchor before running anything. Tolerating a missing anchor would have been the real failure: two clauses would have gone on looking falsifiably evidenced while nothing was being mutated.
The harvester exits non-zero on a finding, so a pipeline can gate on it. CI runs it on every change to this standard. Where no model checker is installed the proof entries are reported as not run — an absence, not a pass — and the clauses fall back to their check evidence. The prover's own output parsing is covered by tests in CI regardless, including both traps above.