78306391a1
A producer that has only ever measured its own specification has demonstrated a format, not a method. This points it at the proof standard. `proof/conformance/v1/joulespec.toml` reads that standard's conformance items from its own published §8 — a bulleted list with bold labels, declared as such because the shape is a fact about the document — and maps each to a named check in `proof-rs`, with a counter-artifact per mapping. Every item, C1 through C5 and the negative pack, reaches `E3`: the check is on record failing against a declared edit, so its passing carries information. Attestation is reported absent rather than `A0`, because no work was declared and no implementer is therefore known. The measurement lands in its own subdirectory rather than beside that standard's vectors, which answer a different question and must not be confused with it. Its energy comes from a wall clock, so it is a measurement and not a vector: re-running changes the bytes, and its README says so. ## What producing it found The first counter-artifact for C1 aimed at `Tier::LADDER`, assuming the router iterated that constant. It does not — the constant is read only by the monotonicity checks, and the router sorts the solvers it is 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. The report was right and the manifest was wrong. That distinction is the whole reason the producer reports what it observed rather than concluding: a check that passes while something it should notice is broken is either a weak check or a mutation that missed, and only an operator can say which. Re-aimed at `Router::new`'s sort, the same check fails at once — so the check was strong all along, and C1's evidence is real rather than assumed. A hypothesis that z3's absence explained it was refuted first, with z3 on the path and the check still passing. ## CI `applied: <manifest>` is a separate step from the existing self-conformance harvest, because that one builds the producer from the workspace under test, which only works where the workspace under test *is* the producer's. This one builds the producer from its own workspace and runs it against someone else's. The build and the path lookup are separate commands: folded into one substitution, a build failure yields an empty path and the step reports "no such file" instead of the compiler error. No `--out`, since a receipt written in CI would dirty the tree and its figures differ every run. Co-Authored-By: Claude Opus 5 <[email protected]>
2.2 KiB
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.