Exact

Exact Union RegExp

Repository files (latest commit first)

Filename	Latest commit message	Latest commit date
Transaction Science 78306391a1 joulespec: applied to a standard that is not its own, which found a mis-aimed mutation ... 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]>		2026-11-02 04:27:13 -05:00
..
joulespec	joulespec: applied to a standard that is not its own, which found a mis-aimed mutation	2026-11-02 04:27:13 -05:00
joulespec.toml	joulespec: applied to a standard that is not its own, which found a mis-aimed mutation	2026-11-02 04:27:13 -05:00
meta.json
receipts.jsonl	proof: closed_by_stub rides in the signed receipt (SPEC §6.1)	2026-08-30 17:22:46 -04:00