joulespec: what the prior art changed — anchoring, vacuity, footprints, a second axis #562

Merged

dcharlot merged 1 commit from joulespec/research-pass into main 2026-11-01 08:36:24 -05:00

Conversation 0 Commits 1 Files changed 8 +1722 -292

dcharlot commented 2026-11-01 08:30:11 -05:00

Owner

Copy link

A research pass over the fields joulespec/1 sits in. Four of them moved the design, one documented the failure mode it had to survive, and one named a gaming vector in a figure it seals.

v0.1 was coherent. It was also wrong in two places and unusable in a third, and the prior art is what showed that.

Anchoring — whether a check can fail is structural, not only empirical (SPEC §2.5)

v0.1 said a green check flatters because a test with no assertion passes. The sharper result: an oracle whose expected value derives from the system it judges cannot disagree with that system when a fault moves the measurement and the expectation together — the comparison cancels, and no input reveals the fault. The defect is in the oracle, not the inputs, and it is visible from the oracle's construction without running anything.

Every check now declares an anchor:

specification	Expected values fixed outside the code under test — the spec, a published procedure, a reference table.
state	Values flowing, directly or indirectly, from the code under test.
unstated	The producer has not said.

An unstated anchor caps at E2, because the answer is free to whoever wrote the check and silence is not an answer. A state-anchored check that killed a mutant did fail once and still reaches E3 — with its anchor disclosed, so the class of faults it cannot catch travels with it. Disclose, don't refuse.

Vacuity — a real hole in v0.1 (SPEC §2.5, §2.6)

v0.1's E4 required a cross-checked formalization but not that the statement could fail. A formal property can be satisfied vacuously — true because nothing ever reaches the condition it guards, so it holds of almost any implementation. Detecting it is established practice in model checking, and one industrial verification setting reported around a fifth of specifications initially passing that way.

E4 now requires the statement to have been refuted against a named counter-model. Which makes the ladder uniform, and this is the rule worth keeping:

Every rung above E2 rests on a demonstrated failure. A test earns E3 by failing against a mutant; a proof earns E4 by failing against a counter-model. Nothing reaches either on a passing run alone.

Footprints — the flaw that would have killed it in practice (SPEC §2.4)

Binding evidence to a whole-tree digest makes every commit stale every witness, so one README edit collapses a specification's grade to ungraded. That is precisely how traceability dies: the empirical literature finds trace links degrade mainly through ordinary refactoring, and reports that keeping them current can cost more than creating them. v0.1 had reproduced the documented failure however sound its addressing.

A witness now names a footprint — the addresses within the artifact its evidence depended on — and applies at any later state whose parts still contain every member. Edit the docs and the auth requirement's evidence stands; edit the auth code and that clause ages, alone. Paths never enter the mechanism: a content address is the identity of its content, so membership is the whole test.

Empty means the whole artifact — the conservative default, and what a producer that cannot enumerate its inputs must use. A narrower footprint is a stronger claim, signed, so a wrong one makes the evidence wrong rather than merely stale. SPEC §8 says plainly that this standard cannot tell what a check actually read.

A second axis (SPEC §2.8)

v0.1 folded "who says so" into "what was done": a self-review silently became E0, and a proof with a declared formalization silently became E2, indistinguishable from a passing test. Supply-chain provenance frameworks grade records on exactly that axis and are explicit that they say nothing about whether software is correct; this family's readiness standard publishes several axes with gates rather than one scalar.

So attestation is its own axis — A0:self-attested → A1:independent → A2:reproduced — derived, never declared: from whether a witness's author also authored work here, and from whether disjoint parties reported the same check at the same grade and state. Absent, not independent, where no work identifies an implementer: not knowing who built something is not evidence that someone else checked it. Both axes are minima over the owed obligations and both gate conformance.

The per-clause verdict also carries the means and the anchor, so two clauses at E2 are no longer indistinguishable.

Bidirectional traceability (SPEC §5.2)

Certified-airborne-software practice has required traceability both ways for decades, and the backward direction exists for one purpose: code with no upstream requirement is a finding even when it works correctly, because unintended function is what the argument cannot otherwise exclude. v0.1 measured unspecified energy; it now also names the work units, because a figure answers how much and only the list answers which.

Comparability — the gaming vector (SPEC §5.3)

Found in the assurance-case literature's own critique of counting resolved doubts: any evidenced-over-total figure improves when trivial items are added. Splitting one requirement into twenty trivially falsifiable ones would divide microjoules-per-obligation by twenty while establishing nothing.

The figure is now normatively comparable only between evaluations carrying the same specification address — the comparison it exists for — and an implementation must not present it as a cross-specification benchmark. The grade and attestation need no such caveat: minima cannot be improved by adding obligations, and a test asserts it.

SPEC §9 — what this takes from each field, and what it adds

Assurance-case structure (whose own international standard excludes content quality — exactly the grade); certified-airborne traceability and its orthogonal structural-coverage ladder; provenance levels; mutation testing, including why the equivalent-mutant problem cannot inflate a grade here, since E3 only ever uses a mutant the check did kill; and carbon-intensity accounting, which has the same rate-per-functional-unit shape and scopes out the energy of producing software, which is the quantity measured here.

SPEC §8 — the limits these introduce

A footprint is trusted, not verified. A2 is agreement, not correctness — reproducing a vacuous check reproduces the vacuity. And two of the results relied on are thinly evidenced: the vacuity rate comes from one industrial setting, the oracle-anchoring effect from a single-system study by a single author. The design rests on the mechanisms, which stand on their own arguments, not on the magnitudes.

Verification

Wire format changed (witness footprint; anchor and vacuity in evidence), so v0.1.0-draft.1 → v0.2.0-draft.1.

On the M3 Ultra build host, all under --locked: cargo check --workspace --all-targets clean, cargo clippy --workspace --all-targets -- -D warnings zero warnings, cargo test --workspace green. Repo checks locally: no vanity metrics, every SPEC § citation resolves, every lockfile current, tests-in-CI.

Stacked on #561, which merged first; this PR carries one commit.

🤖 Generated with Claude Code

A research pass over the fields `joulespec/1` sits in. Four of them moved the design, one documented the failure mode it had to survive, and one named a gaming vector in a figure it seals. v0.1 was coherent. It was also **wrong in two places and unusable in a third**, and the prior art is what showed that. ## Anchoring — whether a check can fail is structural, not only empirical (SPEC §2.5) v0.1 said a green check flatters because a test with no assertion passes. The sharper result: **an oracle whose expected value derives from the system it judges cannot disagree with that system when a fault moves the measurement and the expectation together** — the comparison cancels, and no input reveals the fault. The defect is in the oracle, not the inputs, and it is visible from the oracle's construction without running anything. Every check now declares an **anchor**: | `specification` | Expected values fixed outside the code under test — the spec, a published procedure, a reference table. | |---|---| | `state` | Values flowing, directly or indirectly, from the code under test. | | `unstated` | The producer has not said. | An unstated anchor **caps at `E2`**, because the answer is free to whoever wrote the check and silence is not an answer. A state-anchored check that killed a mutant did fail once and still reaches `E3` — with its anchor disclosed, so the class of faults it cannot catch travels with it. Disclose, don't refuse. ## Vacuity — a real hole in v0.1 (SPEC §2.5, §2.6) v0.1's `E4` required a cross-checked formalization but **not that the statement could fail**. A formal property can be satisfied *vacuously* — true because nothing ever reaches the condition it guards, so it holds of almost any implementation. Detecting it is established practice in model checking, and one industrial verification setting reported around a fifth of specifications initially passing that way. `E4` now requires the statement to have been **refuted against a named counter-model**. Which makes the ladder uniform, and this is the rule worth keeping: > **Every rung above `E2` rests on a demonstrated failure.** A test earns `E3` by failing against a mutant; a proof earns `E4` by failing against a counter-model. Nothing reaches either on a passing run alone. ## Footprints — the flaw that would have killed it in practice (SPEC §2.4) Binding evidence to a whole-tree digest makes **every commit stale every witness**, so one README edit collapses a specification's grade to ungraded. That is precisely how traceability dies: the empirical literature finds trace links degrade mainly through ordinary refactoring, and reports that keeping them current can cost more than creating them. v0.1 had reproduced the documented failure however sound its addressing. A witness now names a **footprint** — the addresses within the artifact its evidence depended on — and applies at any later state whose parts still contain every member. Edit the docs and the auth requirement's evidence stands; edit the auth code and that clause ages, alone. Paths never enter the mechanism: a content address *is* the identity of its content, so membership is the whole test. Empty means the whole artifact — the conservative default, and what a producer that cannot enumerate its inputs must use. A narrower footprint is a **stronger** claim, signed, so a wrong one makes the evidence wrong rather than merely stale. SPEC §8 says plainly that this standard cannot tell what a check actually read. ## A second axis (SPEC §2.8) v0.1 folded "who says so" into "what was done": a self-review silently became `E0`, and a proof with a declared formalization silently became `E2`, **indistinguishable from a passing test**. Supply-chain provenance frameworks grade records on exactly that axis and are explicit that they say nothing about whether software is correct; this family's readiness standard publishes several axes with gates rather than one scalar. So attestation is its own axis — `A0:self-attested` → `A1:independent` → `A2:reproduced` — **derived, never declared**: from whether a witness's author also authored work here, and from whether disjoint parties reported the same check at the same grade and state. **Absent, not independent**, where no work identifies an implementer: not knowing who built something is not evidence that someone else checked it. Both axes are minima over the owed obligations and both gate conformance. The per-clause verdict also carries the **means** and the anchor, so two clauses at `E2` are no longer indistinguishable. ## Bidirectional traceability (SPEC §5.2) Certified-airborne-software practice has required traceability both ways for decades, and the backward direction exists for one purpose: **code with no upstream requirement is a finding even when it works correctly**, because unintended function is what the argument cannot otherwise exclude. v0.1 measured unspecified *energy*; it now also **names** the work units, because a figure answers *how much* and only the list answers *which*. ## Comparability — the gaming vector (SPEC §5.3) Found in the assurance-case literature's own critique of counting resolved doubts: any *evidenced-over-total* figure improves when trivial items are added. Splitting one requirement into twenty trivially falsifiable ones would divide microjoules-per-obligation by twenty while establishing nothing. The figure is now normatively comparable **only between evaluations carrying the same specification address** — the comparison it exists for — and an implementation must not present it as a cross-specification benchmark. The grade and attestation need no such caveat: minima cannot be improved by adding obligations, and a test asserts it. ## SPEC §9 — what this takes from each field, and what it adds Assurance-case structure (whose own international standard **excludes content quality** — exactly the grade); certified-airborne traceability and its orthogonal structural-coverage ladder; provenance levels; mutation testing, including why the equivalent-mutant problem **cannot** inflate a grade here, since `E3` only ever uses a mutant the check *did* kill; and carbon-intensity accounting, which has the same rate-per-functional-unit shape and scopes out the energy of *producing* software, which is the quantity measured here. ## SPEC §8 — the limits these introduce A footprint is trusted, not verified. `A2` is agreement, not correctness — reproducing a vacuous check reproduces the vacuity. And **two of the results relied on are thinly evidenced**: the vacuity rate comes from one industrial setting, the oracle-anchoring effect from a single-system study by a single author. The design rests on the mechanisms, which stand on their own arguments, not on the magnitudes. ## Verification Wire format changed (witness footprint; anchor and vacuity in evidence), so **v0.1.0-draft.1 → v0.2.0-draft.1**. On the M3 Ultra build host, all under `--locked`: `cargo check --workspace --all-targets` clean, `cargo clippy --workspace --all-targets -- -D warnings` zero warnings, `cargo test --workspace` green. Repo checks locally: no vanity metrics, every `SPEC §` citation resolves, every lockfile current, tests-in-CI. Stacked on #561, which merged first; this PR carries one commit. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-11-01 08:30:11 -05:00

joulespec: what the prior art changed — anchoring, vacuity, footprints, a second axis ... 214d8e5945

A research pass over the fields joulespec/1 sits in. Four of them moved the
design, one documented the failure mode it had to survive, and one named a
gaming vector in a figure it seals. v0.1 was coherent; it was also wrong in
two places and unusable in a third.

ANCHORING (SPEC 2.5). v0.1 said a green check flatters because a test with no
assertion passes. The sharper result: an oracle whose expected value derives
from the system it judges cannot disagree with that system when a fault moves
the measurement and the expectation together -- the comparison cancels, and no
input reveals the fault. That is a property of how the check was written,
visible without running anything.

So every check now declares an anchor: `specification` (expected values fixed
outside the code under test), `state` (values flowing from it), or `unstated`.
An unstated anchor caps at E2, because the answer is free to whoever wrote the
check and silence is not an answer. A state-anchored check that killed a
mutant did fail once and still reaches E3, with its anchor disclosed -- the
class of faults it cannot catch travels with it. Disclose, don't refuse.

VACUITY (SPEC 2.5, 2.6). A real hole in v0.1: E4 required a cross-checked
formalization but not that the statement could fail. A formal property can be
satisfied vacuously -- true because nothing ever reaches the condition it
guards, so it holds of almost any implementation. Detecting it is established
practice in model checking, and one industrial setting reported around a fifth
of specifications initially passing that way.

E4 now requires the statement to have been refuted against a named
counter-model. Which makes the ladder uniform, and this is the rule worth
keeping: EVERY RUNG ABOVE E2 RESTS ON A DEMONSTRATED FAILURE. A test earns E3
by failing against a mutant; a proof earns E4 by failing against a
counter-model. Nothing reaches either on a passing run alone.

FOOTPRINTS (SPEC 2.4). The usability flaw that would have killed it in
practice: binding evidence to a whole-tree digest makes every commit stale
every witness, so one README edit collapses a specification's grade to
ungraded. That is precisely how traceability dies -- the empirical literature
finds trace links degrade mainly through ordinary refactoring, and that
keeping them current can cost more than creating them.

A witness now names a footprint, the addresses within the artifact its
evidence depended on, and applies at any later state whose parts still contain
every member. Edit the docs and the auth requirement's evidence stands; edit
the auth code and that clause ages, alone. Paths never enter the mechanism: a
content address IS the identity of its content, so membership is the whole
test. Empty means the whole artifact -- the conservative default, and what a
producer that cannot enumerate its inputs must use. A narrower footprint is a
STRONGER claim, signed, so a wrong one makes the evidence wrong rather than
merely stale (and SPEC 8 says plainly that this standard cannot tell what a
check actually read).

A SECOND AXIS (SPEC 2.8). v0.1 folded "who says so" into "what was done": a
self-review silently became E0, and a proof with a declared formalization
silently became E2, indistinguishable from a passing test. Supply-chain
provenance frameworks grade records on exactly that axis and are explicit that
they say nothing about correctness; this family's readiness standard publishes
several axes with gates rather than one scalar.

So attestation is its own axis -- A0 self-attested, A1 independent, A2
reproduced -- DERIVED, never declared: from whether a witness's author also
authored work here, and from whether disjoint parties reported the same check
at the same grade and state. Absent, not independent, where no work identifies
an implementer: not knowing who built something is not evidence that someone
else checked it. Both axes are minima over the owed obligations and both gate.
The per-clause verdict also carries the MEANS and the anchor, so two clauses
at E2 are no longer indistinguishable.

BIDIRECTIONAL TRACEABILITY (SPEC 5.2). Certified-airborne-software practice
has required traceability both ways for decades, and the backward direction
exists for one purpose: code with no upstream requirement is a finding even
when it works correctly, because unintended function is what the argument
cannot otherwise exclude. v0.1 measured unspecified ENERGY; it now also names
the work units, because a figure answers how much and only the list answers
which.

COMPARABILITY (SPEC 5.3). The gaming vector, found in the assurance-case
literature's own critique of counting resolved doubts: any evidenced-over-total
figure improves when trivial items are added, so splitting one requirement into
twenty trivially falsifiable ones would divide microjoules-per-obligation by
twenty while establishing nothing. The figure is now normatively comparable
ONLY between evaluations carrying the same specification address -- which is
the comparison it exists for -- and an implementation must not present it as a
cross-specification benchmark. The grade and attestation need no such caveat:
minima cannot be improved by adding obligations, and a test asserts it.

Also SPEC 9, on what this takes from each neighbouring field and what it adds:
assurance-case structure (whose own standard excludes content quality, which is
exactly the grade), certified-airborne traceability and its orthogonal
structural-coverage ladder, provenance levels, mutation testing (including why
the equivalent-mutant problem cannot inflate a grade here -- E3 only ever uses
a mutant the check DID kill), and carbon-intensity accounting (same rate-per-
functional-unit shape, and it scopes out the energy of producing software,
which is the quantity measured here).

SPEC 8 gains the limits these introduce: a footprint is trusted not verified,
A2 is agreement not correctness, and two of the results relied on are thinly
evidenced -- one industrial setting, one single-system single-author study --
so the design rests on the mechanisms, which stand on their own, not on the
magnitudes.

Wire format changed (witness footprint; anchor and vacuity in evidence), so
v0.1.0-draft.1 -> v0.2.0-draft.1.

cargo check/clippy/test --workspace --all-targets --locked: green, zero
warnings, on the M3 Ultra build host.

Co-Authored-By: Claude Opus 5 <[email protected]>

dcharlot merged commit 2f7121841a into main 2026-11-01 08:36:24 -05:00

dcharlot referenced this pull request from a commit 2026-11-01 08:36:24 -05:00

Merge pull request 'joulespec: what the prior art changed — anchoring, vacuity, footprints, a second axis' (#562) from joulespec/research-pass into main

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!562

No description provided.