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

dcharlot commented 2026-11-02 04:27:45 -05:00

Owner

Copy link

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.

C1     E3  tests::trivial_closes_at_t0_no_waste            (failed when the router's rungs are ordered dearest-first)
C2     E3  tests::escalation_discloses_waste               (failed when a failed cheaper attempt's joules stop counting as waste)
C3     E3  tests::ladder_is_cheapest_first_and_monotone    (failed when a dearer rung is put first)
C4     E3  tests::cache_is_the_flywheel                    (failed when a cache hit is charged a joule)
C5     E3  jcr1::tests::envelope_rejects_wrong_steward     (failed when the key id stops being compared)
C-neg  E3  tests::unproved_goal_cannot_be_sealed           (failed when an unproved goal can be sealed)

grade E3 · attestation absent · open at E3: 0 · flags: 0

Attestation is reported absent, not A0: no work was declared, so no implementer is known, and absence of information about who built something is not evidence that someone else checked it.

The measurement lands in its own subdirectory rather than beside that standard's vectors, which answer a different question. Its energy comes from a wall clock, so it is a measurement, 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 first hypothesis, that z3's absence from the harvest's PATH explained it, was refuted before the real cause was found: with z3 on the path the check still passed.

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 deliberately 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. The exact sequence the step runs was executed on the build host before being committed: E3, 0 open, 0 flags, clean tree.

🤖 Generated with Claude Code

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. ``` C1 E3 tests::trivial_closes_at_t0_no_waste (failed when the router's rungs are ordered dearest-first) C2 E3 tests::escalation_discloses_waste (failed when a failed cheaper attempt's joules stop counting as waste) C3 E3 tests::ladder_is_cheapest_first_and_monotone (failed when a dearer rung is put first) C4 E3 tests::cache_is_the_flywheel (failed when a cache hit is charged a joule) C5 E3 jcr1::tests::envelope_rejects_wrong_steward (failed when the key id stops being compared) C-neg E3 tests::unproved_goal_cannot_be_sealed (failed when an unproved goal can be sealed) grade E3 · attestation absent · open at E3: 0 · flags: 0 ``` Attestation is reported **absent**, not `A0`: no work was declared, so no implementer is known, and absence of information about who built something is not evidence that someone else checked it. The measurement lands in its own subdirectory rather than beside that standard's vectors, which answer a different question. Its energy comes from a wall clock, so it is a **measurement, 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 first hypothesis, that z3's absence from the harvest's `PATH` explained it, was **refuted** before the real cause was found: with z3 on the path the check still passed. ## 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 deliberately 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. The exact sequence the step runs was executed on the build host before being committed: `E3`, 0 open, 0 flags, clean tree. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-11-02 04:27:45 -05:00

joulespec: applied to a standard that is not its own, which found a mis-aimed mutation ... 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]>

dcharlot merged commit 73f2f5b0a8 into main 2026-11-02 04:40:10 -05:00

dcharlot referenced this pull request from a commit 2026-11-02 04:40:11 -05:00

Merge pull request 'joulespec: applied to a standard that is not its own, which found a mis-aimed mutation' (#570) from joulespec/applied into main

dcharlot referenced this pull request from a commit 2026-11-02 08:07:53 -05:00

standards-build: the proof gate read `echo | grep -q` under pipefail, a 1-in-20 flake

dcharlot referenced this pull request from a commit 2026-11-03 00:53:10 -05:00

standards-build: the proof gate read `echo | grep -q` under pipefail, a 1-in-20 flake

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!570

No description provided.