joulespec: applied to a standard that is not its own, which found a mis-aimed mutation #570

Merged

dcharlot merged 1 commit from joulespec/applied into main 2026-11-02 04:40:10 -05:00

Conversation 0 Commits 1 Files changed 9 +1236 -1

2026-11-02

Transaction Science

joulespec: applied to a standard that is not its own, which found a mis-aimed mutation ...

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]>

78306391a1

• View at this point in history

2026-11-02 04:27:13 -05:00