78306391a1
All checks were successful
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 15s
standards workspaces build + test / pool-rs (pool/pool-rs, pool-rs, linux) (pull_request) Successful in 27s
standards workspaces build + test / arl-rs (arl/arl-rs, arl-rs, linux) (pull_request) Successful in 33s
standards workspaces build + test / joulehook-rs (joulehook/joulehook-rs, joulehook-rs, linux) (pull_request) Successful in 34s
standards workspaces build + test / jcp-rs (jcp-conformance, jcp/jcp-rs, -p jcp-energy --features nvml, jcp-rs, linux) (pull_request) Successful in 50s
standards workspaces build + test / jouledesk-rs (jouledesk/jouledesk-rs, jouledesk-rs, macos) (pull_request) Successful in 56s
standards workspaces build + test / sense-rs (sense/sense-rs, sense-rs, linux) (pull_request) Successful in 23s
standards workspaces build + test / proof-rs (proof/conformance/v1/joulespec.toml, proof-conformance, proof/proof-rs, proof-rs, linux, true) (pull_request) Successful in 1m3s
standards workspaces build + test / joule-ui-rs (joule-ui/joule-ui-rs, joule-ui-rs, linux) (pull_request) Successful in 1m49s
standards workspaces build + test / sandbox-rs (sandbox-conformance, sandbox/sandbox-rs, -p sandbox-tee --features amd-kds,intel-pcs, sandbox-rs, linux) (pull_request) Successful in 1m16s
standards workspaces build + test / joulespec-rs (true, joulespec/joulespec-rs, true, joulespec-rs, linux) (pull_request) Successful in 54s
standards workspaces build + test / eoc-rs (eoc/eoc-rs, -p eoc-meter --features cuda, eoc-rs, linux) (pull_request) Successful in 2m19s
standards workspaces build + test / smart-byte-rs (smart-byte/smart-byte-rs, smart-byte-rs, linux) (pull_request) Successful in 2m14s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 3m44s
standards workspaces build + test / aac-rs (aac-conformance, aac/aac-rs, aac-rs, linux-arm64) (pull_request) Successful in 4m47s
standards workspaces build + test / jouleclaw-rs (-nodebug, jouleclaw/jouleclaw-rs, -p jouleclaw-energy --features rapl,nvml, jouleclaw-rs, linux-arm64, -C target-feature=+fp16) (pull_request) Successful in 5m15s
standards workspaces build + test / joulespec-proofs (joulespec/joulespec-rs, joulespec-proofs, true, macos) (pull_request) Successful in 5m54s
standards workspaces build + test / joulecontract-rs (joulecontract/joulecontract-rs, joulecontract-rs, linux-arm64, true) (pull_request) Successful in 1m12s
standards workspaces build + test / map-rs (map-conformance, map/map-rs, map-rs, linux-arm64) (pull_request) Successful in 1m16s
standards workspaces build + test / mesh-rs (mesh/mesh-rs, -p mesh-engine-gguf -p mesh-openai --features mesh-engine-gguf/gguf,mesh-openai/server, mesh-rs, linux-arm64) (pull_request) Successful in 1m17s
standards workspaces build + test / openpay (openpay, openpay, linux-arm64) (pull_request) Successful in 4m8s
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Successful in 7m17s
standards workspaces build + test / macOS energy backends (pull_request) Successful in 11m48s
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]>
46 lines
2.2 KiB
Markdown
46 lines
2.2 KiB
Markdown
# This standard, measured by `joulespec/1`
|
|
|
|
Not part of this standard's own conformance pack. The vectors beside it
|
|
(`../meta.json`, `../receipts.jsonl`) are what an implementation of *this*
|
|
standard round-trips. These files answer a different question: **how well is
|
|
each conformance item of §8 actually evidenced, and what did establishing that
|
|
cost?**
|
|
|
|
Produced by [`../joulespec.toml`](../joulespec.toml):
|
|
|
|
```
|
|
joulespec harvest --manifest conformance/v1/joulespec.toml \
|
|
--out conformance/v1/joulespec --require-grade E3
|
|
```
|
|
|
|
The clauses are read from [`../../../SPEC.md`](../../../SPEC.md) §8 rather than
|
|
copied into the manifest, so the manifest cannot drift from the specification:
|
|
reword a conformance item and its obligation address moves, and the witness
|
|
bound to the old wording stops applying.
|
|
|
|
Every item of §8 — C1 through C5 and the negative pack — reaches **`E3`**:
|
|
each is mapped to a named check, and each check is on record *failing* against
|
|
a declared counter-artifact, so its passing carries information. Attestation
|
|
is reported **absent**, not `A0`: no work units were declared, so no
|
|
implementer is known, and absence of information about who built something is
|
|
not evidence that someone else checked it.
|
|
|
|
**These files are a measurement, not a vector.** Their energy figures come
|
|
from a wall clock and are graded `Estimator`, so re-running the harvest
|
|
produces different microjoules and therefore different receipt bytes. Nothing
|
|
here should be diffed byte-for-byte.
|
|
|
|
## What producing it found
|
|
|
|
The first counter-artifact written for C1 aimed at `Tier::LADDER`, on the
|
|
assumption that the router iterated that constant. It does not — the constant
|
|
is read only by the monotonicity checks, and the router sorts the solvers it
|
|
was 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.
|
|
|
|
That report was correct and the manifest was wrong. The distinction between
|
|
"this check is weak" and "this mutation missed the code path" is the
|
|
operator's to make; a producer can only say which it observed. Re-aimed at
|
|
`Router::new`'s sort, the same check fails immediately — so the check was
|
|
strong all along, and C1's evidence is real rather than assumed.
|