joulespec: a producer, and the standard applied to its own implementation #566
Loading…
Reference in a new issue
No description provided.
Delete branch "joulespec/self-conformance"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
v0.2 was a kernel nobody could emit into. This adds the reference producer, then points it at the implementation it describes — which found two defects inspection had not.
The producer
joulespec harvestreads the clauses from a published specification document, runs each declared check, runs it again against a counter-artifact, and emits a signed witness at the rung the observations support. Plusverify(a sealed receipt) anddrift(two revisions).Its soundness is one distinction — the three ways a run can fail to pass:
E3evidence.A test that did not run is not a test that passed — a harness filtered to a name nothing matches prints
running 0 tests, reports success and exits zero, the shape of every check that silently stopped checking, so the count is parsed and required. And treating a compile failure asE3would manufacture falsifiability out of a syntax error, which is the most misleading possible result.Exit 2 on a finding, 3 below
--require-grade. Mutations revert onDrop, so a panic cannot leave one in place, and the CI step asserts the tree is clean afterwards rather than trusting that.Three things in the manifest are declared, because they are human judgements the standard refuses to guess: which check stands for which obligation (the same act as formalizing a clause, SPEC §2.6), each check's anchor, and each check's footprint — a harness that cannot observe its own reads must not guess (SPEC §8). Everything else is computed, including the clauses: they are parsed from
SPEC.md§7 rather than copied into the manifest, so the manifest cannot drift from the specification. Reword an item and its obligation address moves. Re-wrapping a paragraph does not, because continuation lines join on one space — a standard that punishedfmtwould teach people to avoid it.What it found
Pointed at joulespec itself (SPEC §7.1,
conformance/v1/README.md):allandanyare the same function, so mutating the conjunction left it green and the conjunction was never checked. A second test now covers it.applies_atguarded on the 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. It looked like care. It is gone.A third report was a mistake in the manifest — a counter-artifact aimed at a branch its check never takes — which the harvester correctly reported as a check that cannot see its subject. Telling those two readings apart is the operator's job; the harvester reports what it observed rather than guessing which it is.
Every conformance item C1–C11 now reaches
E3against a counter-artifact that made its check fail.Attestation is reported absent, not independent: no work was declared, so no implementer is known, and the standard's own rule says absence of information about who built something is not evidence that someone else checked it. Inventing a figure there was the easy lie.
Two conformance packs, and the distinction matters
conformance/v1/vectors/— the certifiable surface the charter means. Fixed keys, clauses, witnesses and fixed energy, byte-stable, regenerable withJOULESPEC_GEN_VECTORS=1and asserted byte-for-byte otherwise. One witness of every rung the format can express, plus one bound to a superseded state, so an implementation that mishandles any rung or mishandles staleness fails the pack rather than passing it quietly — and a test asserts that coverage, because a pack exercising one rung certifies one rung. Its verdict is the doctrine in miniature: two obligations well evidenced, one carrying only the implementer's citation, specification thereforeE0atA0.Estimator, so re-running produces different bytes. A pack that held measured energy fixed would publish a figure nobody measured.CI
A
harvest: truematrix flag besideclippy: true, running the harvest on every change to this standard. It is the only gate that keeps the suite's falsifiability from decaying — which is precisely what inspection missed twice above.Verification
On the M3 Ultra build host, all under
--locked:cargo check --workspace --all-targetsclean,cargo clippy --workspace --all-targets -- -D warningszero warnings,cargo test --workspacegreen. The harvest exits 0 with the tree clean after every mutate/revert cycle. Repo checks locally: no vanity metrics, everySPEC §citation resolves, every lockfile current, tests-in-CI, workflow concurrency, advisories.🤖 Generated with Claude Code
v0.2 was a kernel nobody could emit into. This adds the reference producer and then points it at the implementation it describes -- which found two defects inspection had not. THE PRODUCER (joulespec-cli). `joulespec harvest` reads the clauses from a published specification document, runs each declared check, runs it again against a counter-artifact, and emits a signed witness at the rung the observations support. Also `verify` (a sealed receipt) and `drift` (two spec revisions). It refuses to confuse the three ways a run can fail to pass, which is the whole soundness story: * a test that did not RUN is not a test that passed. A harness filtered to a name nothing matches prints "running 0 tests", reports success and exits zero -- the shape of every check that silently stopped checking -- so the count is parsed and required; * a counter-artifact that did not COMPILE demonstrates nothing, because the check never ran. Treating it as E3 evidence would manufacture falsifiability out of a syntax error, which is the most misleading possible result; * a counter-artifact that compiled, ran and PASSED is a finding: the check cannot see the thing it is about. Exit 2 on a finding, 3 below --require-grade, so a pipeline can gate. Mutations revert on Drop, so a panic cannot leave one in place, and the CI step asserts the tree is clean afterwards rather than trusting that. Three things in the manifest are declared, because they are human judgements the standard refuses to guess: which check stands for which obligation (the same act as formalizing a clause, SPEC 2.6), each check's anchor, and each check's footprint -- a harness that cannot observe its own reads must not guess (SPEC 8). Everything else is computed, including the clauses: they are PARSED from SPEC.md 7 rather than copied into the manifest, so the manifest cannot drift from the specification. Reword an item and its obligation address moves. Re-wrapping a paragraph does not, because continuation lines join on one space -- a standard that punished `fmt` would teach people to avoid it. WHAT IT FOUND, pointed at joulespec itself (SPEC 7.1, conformance/v1/README): 1. A check whose assertion could not fail. A footprint test narrowed to a SINGLE member, and on a one-element footprint `all` and `any` are the same function -- so mutating the conjunction left it green and the conjunction was never checked. A second test now covers it. 2. Dead logic in the implementation. `applies_at` guarded on the state having no enumerable parts, and that guard could not change a single verdict: an `all` over a non-empty footprint against no parts is already false. It looked like care. It is gone. A third report was a mistake in the manifest -- a counter-artifact aimed at a branch its check never takes -- which the harvester correctly reported as a check that cannot see its subject. Telling those two readings apart is the operator's job; the harvester reports what it observed rather than guessing. Every conformance item C1-C11 now reaches E3 against a counter-artifact that made its check fail. Attestation is reported ABSENT, not independent: no work was declared, so no implementer is known, and the standard's own rule says absence of information about who built something is not evidence that someone else checked it. Inventing a figure there would have been the easy lie. TWO CONFORMANCE PACKS, and the distinction matters: * conformance/v1/vectors/ -- the certifiable surface the charter means. Fixed keys, clauses, witnesses and FIXED energy, byte-stable, regenerable with JOULESPEC_GEN_VECTORS=1 and asserted byte-for-byte otherwise. One witness of every rung the format can express, plus one bound to a superseded state, so an implementation that mishandles any rung or mishandles staleness fails the pack rather than passing it quietly. A test asserts that coverage, because a pack exercising one rung certifies one rung. Its verdict is the doctrine in miniature: two obligations well evidenced, one carrying only the implementer's citation, specification therefore E0 at A0. * the self-conformance receipt -- a MEASUREMENT, not a vector. Its energy comes from a wall clock graded Estimator, so re-running produces different bytes. A pack that held measured energy fixed would publish a figure nobody measured. CI gains a `harvest: true` matrix flag beside `clippy: true`, running the harvest on every change to this standard. It is the only gate that keeps the suite's falsifiability from decaying, which is precisely what inspection missed twice above. cargo check/clippy/test --workspace --all-targets --locked: green, zero warnings; harvest exits 0 with the tree clean after every mutation, on the M3 Ultra build host. Co-Authored-By: Claude Opus 5 <[email protected]>