From 78306391a11ba15eadcee25df1dd77375ad02c64 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Mon, 2 Nov 2026 04:27:13 -0500 Subject: [PATCH] joulespec: applied to a standard that is not its own, which found a mis-aimed mutation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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: ` 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 --- .github/workflows/standards-build.yml | 45 +- joulespec/README.md | 23 + proof/conformance/v1/joulespec.toml | 134 ++++ proof/conformance/v1/joulespec/README.md | 46 ++ proof/conformance/v1/joulespec/receipt.cbor | Bin 0 -> 2041 bytes proof/conformance/v1/joulespec/receipt.json | 85 ++ proof/conformance/v1/joulespec/spec.json | 140 ++++ proof/conformance/v1/joulespec/state.json | 29 + proof/conformance/v1/joulespec/witnesses.json | 735 ++++++++++++++++++ 9 files changed, 1236 insertions(+), 1 deletion(-) create mode 100644 proof/conformance/v1/joulespec.toml create mode 100644 proof/conformance/v1/joulespec/README.md create mode 100644 proof/conformance/v1/joulespec/receipt.cbor create mode 100644 proof/conformance/v1/joulespec/receipt.json create mode 100644 proof/conformance/v1/joulespec/spec.json create mode 100644 proof/conformance/v1/joulespec/state.json create mode 100644 proof/conformance/v1/joulespec/witnesses.json diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index 9dcb3717d..771cbf05b 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -131,7 +131,13 @@ jobs: - { name: jouledesk-rs, dir: jouledesk/jouledesk-rs, runner: macos } - { name: arl-rs, dir: arl/arl-rs, runner: linux } - { name: sense-rs, dir: sense/sense-rs, runner: linux } - - { name: proof-rs, dir: proof/proof-rs, runner: linux, z3: true, conformance: proof-conformance } + # `applied:` points the joulespec producer at this standard's own + # conformance items (SPEC §8), mapped to real checks with a + # counter-artifact each. It is the only gate that keeps those + # mappings honest: a refactor that moves the code a mutation was + # aimed at makes the harvest refuse, and a check that stops being + # able to fail becomes a finding rather than staying green. + - { name: proof-rs, dir: proof/proof-rs, runner: linux, z3: true, conformance: proof-conformance, applied: proof/conformance/v1/joulespec.toml } - { name: joulehook-rs, dir: joulehook/joulehook-rs, runner: linux } - { name: eoc-rs, dir: eoc/eoc-rs, runner: linux, feature_tests: "-p eoc-meter --features cuda" } # mesh-openai's `serve_example` test (the reference server seals what @@ -339,6 +345,43 @@ jobs: exit 1 fi + # The same producer, pointed at a *different* standard. + # + # `applied: ` names a manifest that lives with the standard it + # describes, so this measures how well that standard's own conformance + # items are evidenced. It is deliberately a separate step from the one + # above: that one builds the producer from the workspace under test, + # which only works where the workspace under test *is* the producer's. + # Here the producer is built from its own workspace and then run against + # someone else's. + # + # No `--out`: a receipt written here would dirty the tree and fail the + # revert check below, and its energy figures differ every run anyway. + - name: JouleSpec applied to this standard + if: matrix.applied + run: | + set -euo pipefail + # Built and located in separate commands on purpose: folded into + # one substitution, a build failure yields an empty path and the + # step fails with "no such file" instead of the compiler error. + ( cd joulespec/joulespec-rs && cargo build --release -p joulespec-cli ) + target="$(cd joulespec/joulespec-rs \ + && cargo metadata --no-deps --format-version 1 \ + | python3 -c 'import json,sys; print(json.load(sys.stdin)["target_directory"])')" + test -x "$target/release/joulespec" \ + || { echo "the producer did not build at $target/release/joulespec"; exit 1; } + "$target/release/joulespec" harvest \ + --manifest "${{ matrix.applied }}" --require-grade E3 + - name: The applied harvest left no mutation behind + if: matrix.applied + run: | + set -euo pipefail + if ! git diff --quiet; then + echo "the applied harvest did not revert cleanly:" + git diff --stat + exit 1 + fi + # Both directions of the proof path, live. # # The first run must verify with every declared reachability cover diff --git a/joulespec/README.md b/joulespec/README.md index f8b5fd8ba..1852312db 100644 --- a/joulespec/README.md +++ b/joulespec/README.md @@ -360,6 +360,29 @@ All of it is recorded in [`conformance/v1/README.md`](conformance/v1/README.md), and that is the `E3` rung doing the only thing it claims to do. +## Applied to a standard that is not this one + +A producer that has only ever measured its own specification has demonstrated +a format, not a method. `proof/conformance/v1/joulespec.toml` points this +producer at a sibling standard: its conformance items are read from that +standard's own published document, each is mapped to a named check in its +workspace, and each mapping declares a counter-artifact that must make that +check fail. Every item of that standard's conformance section reaches `E3`, +and CI gates it there under `applied:` — so a refactor that moves the code a +mutation was aimed at makes the harvest refuse, and a check that stops being +able to fail becomes a finding instead of staying green. + +Doing it found one thing, and the shape of the finding matters more than the +finding. The first counter-artifact for that standard's routing clause was +aimed at a constant the router turned out not to read, so the check passed +with the constant reordered and the harvester reported that the check could +not see its subject. The report was right; the manifest was wrong. A producer +can say only what it observed — that a check passed while something it was +supposed to notice was broken — and whether that means *the check is weak* or +*the mutation missed* is the operator's call. Re-aimed at the sort that +actually orders the rungs, the same check failed at once, which is how the +clause's evidence ended up real rather than assumed. + ## Conformance packs Three, answering different questions: diff --git a/proof/conformance/v1/joulespec.toml b/proof/conformance/v1/joulespec.toml new file mode 100644 index 000000000..f2dee6814 --- /dev/null +++ b/proof/conformance/v1/joulespec.toml @@ -0,0 +1,134 @@ +# JouleSpec applied to the proof standard. +# +# The first time this producer has measured a specification other than its own. +# Clauses are read from `../../SPEC.md` section 8 rather than copied here, so +# this manifest cannot drift from that document: reword an item and its +# obligation address moves, and the witness bound to the old wording stops +# applying. +# +# The three declared things are human judgements the standard refuses to guess +# (JouleSpec SPEC 2.6, 2.5, 8): which check stands for which obligation, where +# each check's expectation comes from, and which inputs it depends on. + +workspace = "../../proof-rs" +steward = "did:key:joulespec-applied-proof" + +[spec] +document = "../../SPEC.md" +section = "8. Conformance" +# This document writes its conformance items as a bulleted list with bold +# labels, which is a fact about the document rather than about this producer. +shape = "bulleted-bold-label" +# C1..C5 and C-neg. A floor, so a parser that matched fewer fails rather than +# reporting success over a shorter list. +expect_at_least = 6 +intent = "The cheapest-sufficient prover routes, accounts and seals as section 8 requires." + +[artifact] +dirs = ["crates"] +extensions = ["rs"] + +[energy] +watts = 30.0 +provenance = "estimator" + +# --------------------------------------------------------------------------- +# C1 -- cheapest-sufficient routing +# +# The first mutation written here was aimed at `Tier::LADDER`, on the +# assumption that the router iterated it. It does not: that constant is read +# only by the monotonicity checks, and the router sorts the solvers it was +# handed. So the check passed with the constant reordered, and the harvester +# reported -- correctly -- that the check could not see its subject. The +# report was right and the manifest was wrong, which is the distinction the +# operator has to make and the producer cannot. +# +# Aimed at the sort, the same check fails at once. +[[evidence]] +clause = "C1" +check = "tests::trivial_closes_at_t0_no_waste" +anchor = "specification" +footprint = [ + "crates/proof-schema/src/lib.rs", + "crates/proof-cascade/src/lib.rs", +] +[evidence.counter] +file = "crates/proof-cascade/src/lib.rs" +find = " solvers.sort_by_key(|s| s.tier());" +replace = " solvers.sort_by_key(|s| std::cmp::Reverse(s.tier()));" +breaks = "orders the router's rungs dearest-first, so a goal no longer closes at the cheapest tier that can discharge it" + +# --------------------------------------------------------------------------- +# C2 -- disclosed escalation +[[evidence]] +clause = "C2" +check = "tests::escalation_discloses_waste" +anchor = "specification" +footprint = ["crates/proof-cascade/src/lib.rs"] +[evidence.counter] +file = "crates/proof-cascade/src/lib.rs" +find = " wasted_uj = wasted_uj.saturating_add(uj);" +replace = " wasted_uj = wasted_uj.saturating_add(0);" +breaks = "stops counting a failed cheaper attempt's joules as escalation waste" + +# --------------------------------------------------------------------------- +# C3 -- energy honesty +[[evidence]] +clause = "C3" +check = "tests::ladder_is_cheapest_first_and_monotone" +anchor = "specification" +footprint = ["crates/proof-schema/src/lib.rs"] +[evidence.counter] +file = "crates/proof-schema/src/lib.rs" +find = """ pub const LADDER: [Tier; 4] = [ + Tier::Automation, + Tier::Smt,""" +replace = """ pub const LADDER: [Tier; 4] = [ + Tier::Smt, + Tier::Automation,""" +breaks = "breaks the ladder's strict monotonicity by putting a dearer rung first" + +# --------------------------------------------------------------------------- +# C4 -- the flywheel +[[evidence]] +clause = "C4" +check = "tests::cache_is_the_flywheel" +anchor = "specification" +footprint = ["crates/proof-cascade/src/lib.rs"] +[evidence.counter] +file = "crates/proof-cascade/src/lib.rs" +find = """ total_uj: 0, + wasted_uj: 0,""" +replace = """ total_uj: 1, + wasted_uj: 0,""" +breaks = "charges a joule for a proof served from cache, so re-proving is no longer free" + +# --------------------------------------------------------------------------- +# C5 -- the receipt +[[evidence]] +clause = "C5" +check = "jcr1::tests::envelope_rejects_wrong_steward" +anchor = "specification" +footprint = ["crates/proof-receipt/src/jcr1.rs"] +[evidence.counter] +file = "crates/proof-receipt/src/jcr1.rs" +find = " if kid != expected_steward {" +replace = " if false {" +breaks = "stops comparing the envelope's key id against the expected steward, so a wrong steward verifies" + +# --------------------------------------------------------------------------- +# C-neg -- the negative pack +[[evidence]] +clause = "C-neg" +check = "tests::unproved_goal_cannot_be_sealed" +anchor = "specification" +footprint = ["crates/proof-receipt/src/lib.rs"] +[evidence.counter] +file = "crates/proof-receipt/src/lib.rs" +find = """ if !r.proved { + return Err(ReceiptError::NotProved); + }""" +replace = """ if false { + return Err(ReceiptError::NotProved); + }""" +breaks = "lets a receipt be sealed for a goal nothing proved" diff --git a/proof/conformance/v1/joulespec/README.md b/proof/conformance/v1/joulespec/README.md new file mode 100644 index 000000000..3c8ffb401 --- /dev/null +++ b/proof/conformance/v1/joulespec/README.md @@ -0,0 +1,46 @@ +# 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. diff --git a/proof/conformance/v1/joulespec/receipt.cbor b/proof/conformance/v1/joulespec/receipt.cbor new file mode 100644 index 0000000000000000000000000000000000000000..51958ed18365f117f25a26508ec764b5e9c128fb GIT binary patch literal 2041 zcmbuAKZspL6vkJSBuF5T!u)Aci8j&sb7sy=s=yLa3$YMQs^y%Sb6(!=%X=^Hy-lJv z3PFe#sR9ZjVkbgKCt@WQ!AejNwH1j7v9gg^cy=R8c2i_wn|I%xd+*HrzVn@LezCYZ}=83Z>`mmo`lQ&PTPS!^9tPo^?n>XXaT_w|i; zt}Jsrl?f|AW?#I<*csJf%O#{9LaGrMQmY7!F=$ryS+s%+l*M(=m_$c3m@mm-MqT(! z9JCRw&t<-EFki@Jn)NG>+T3}XErv>MvAG|Y&{wI%5-?QALAbb#Ffuzm%RRg{xV;VOZo|!L(7ick=t;wZf7aLkxUp+ql=%>He*2fzP4Amrh zXSDU#9xsg_c(idpxev5*NoIZ67W4N$?`y+xUz^Fr_2En|$at{@FC*Lch?l($(|Eq7 zG@9EQ#3PaUf=05Wwz2b**@gd?Y_u3o#)Hel#aQO^O#y^TAaCI6NKz;Tfvg(#Q(XoU z=*jn5fMc*a)z&0g6#%oM?~T&xgh#`{=DeHpQEy2Ql0>VVI&~g3ab&QYAO*!$ji#wf zAr^-mV{DkzzA{lI&^GN3ymsQ)F8IS9_*-xtxnQH5Vo6AuO$#jGTHVTQogGwZ+El>^8(D6=wuBbkW zU^W?hNG%qH#3hre+6pNPR0o|iN1Kve&MhYMNU$IfjNAB+etGkaUGT#m_^S|k^;jBY ztW;g-#X16FG_P_c=u%5C!v>7Kqq87tntS6a0NC74e&FPNV0DmkiH)U|ic!FE5YsLs z@Q#c+7U>KnMMVtBlj|wDUUeJ)Q$OF^zYG4f2mUB7S>SbB90AOQ3f7+-Vv5y6l~%0- zRI}?~+3m6gw~dzO0$bzuhy5RwvH6V_XfBmf&E{q+Xw6cz#*7vZkudrgYZK{Ov50z0 zdNomWyZ?_K`r_y#`DOX!SO$BLz!J_3DBTW}7?YWlTt*IvnHhaR0?I~^9pwgg)oO!a zM8KSw>P`#TX@MFs1(aZgFQ}DCVm4E-WS=QU?%9EqU|Hdd6xx_FG$$n*ZnvGvuJsmxX$i2s%Qr^xZc