open-standards/proof/conformance/v1/joulespec
Repository files (latest commit first)
Filename Latest commit message Latest commit date
…
..
README.md joulespec: applied to a standard that is not its own, which found a mis-aimed mutation 2026-11-02 04:27:13 -05:00
receipt.cbor
receipt.json
spec.json
state.json
witnesses.json

This standard, measured by joulespec/1

Not part of this standard's own conformance pack. The vectors beside it (../meta.json, ../receipts.jsonl) are what an implementation of this standard round-trips. These files answer a different question: how well is each conformance item of §8 actually evidenced, and what did establishing that cost?

Produced by ../joulespec.toml:

joulespec harvest --manifest conformance/v1/joulespec.toml \
                  --out conformance/v1/joulespec --require-grade E3

The clauses are read from ../../../SPEC.md §8 rather than copied into the manifest, so the manifest cannot drift from the specification: reword a conformance item and its obligation address moves, and the witness bound to the old wording stops applying.

Every item of §8 — C1 through C5 and the negative pack — reaches E3: each is mapped to a named check, and each check is on record failing against a declared counter-artifact, so its passing carries information. Attestation is reported absent, not A0: no work units were declared, so no implementer is known, and absence of information about who built something is not evidence that someone else checked it.

These files are a measurement, not a vector. Their energy figures come from a wall clock and are graded Estimator, so re-running the harvest produces different microjoules and therefore different receipt bytes. Nothing here should be diffed byte-for-byte.

What producing it found

The first counter-artifact written for C1 aimed at Tier::LADDER, on the assumption that the router iterated that constant. It does not — the constant is read only by the monotonicity checks, and the router sorts the solvers it was handed. So trivial_closes_at_t0_no_waste passed with the constant reordered, and the harvester reported that the check could not see its subject.

That report was correct and the manifest was wrong. The distinction between "this check is weak" and "this mutation missed the code path" is the operator's to make; a producer can only say which it observed. Re-aimed at Router::new's sort, the same check fails immediately — so the check was strong all along, and C1's evidence is real rather than assumed.