joulespec: what the prior art changed — anchoring, vacuity, footprints, a second axis #562
2026-11-01
joulespec: what the prior art changed — anchoring, vacuity, footprints, a second axis
All checks were successful
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 8s
standards workspaces build + test / macOS energy backends (pull_request) Has been skipped
standards workspaces build + test / joulespec-rs (true, joulespec/joulespec-rs, joulespec-rs, linux) (pull_request) Successful in 29s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 3m23s
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]>