# JouleSpec conformance — `v1` Two packs live here. They answer different questions and only one of them is reproducible, which is the first thing to know about them. ## `vectors/` — the certifiable surface Fixed keys, fixed clauses, fixed witnesses and **fixed energy**, producing receipt bytes that must not change without a version bump. This is the pack the charter's conformance test refers to: an implementation certifies itself by round-tripping these files. The witness set carries one of every rung the format can express — `cited`, `exercised`, `falsifiable`, `proved` — plus a witness bound to an earlier artifact state, so a verifier that mishandles staleness fails the pack rather than passing it quietly. A pack that exercised one rung would certify one rung, and a test asserts the coverage. The verdict these bytes assert is worth reading, because it is the doctrine in miniature: two obligations are well evidenced, one carries only the implementer's citation, and the specification's grade is therefore **`E0`**. The attestation is `A0` for the same reason — the only surviving witness on that clause is the implementer's own. One clause is a non-goal with no evidence, which is correct and carries no grade, and a quarter of the declared work energy cites no clause at all. Regenerate with: ``` JOULESPEC_GEN_VECTORS=1 cargo test -p joulespec-core --test vectors ``` Without that variable the test asserts the committed bytes, so a change to the wire format fails in CI rather than shipping. ## `evaluation/` — the verdicts, not the bytes The vectors certify that an implementation round-trips a receipt's **bytes**. They say nothing about whether it reaches the right **verdict**, because they carry one scenario. [`evaluation/`](evaluation) is the other half: cases whose correct answer a too-generous implementation gets wrong, each with the inputs to evaluate and the verdict §3 requires. Its [README](evaluation/README.md) says what each trap is and why the expectations are written by hand rather than read back out of this implementation — a distinction that caught seven authoring errors of mine while it was being built. ## The self-conformance record `spec.json`, `witnesses.json`, `state.json`, `receipt.cbor` and `receipt.json` in this directory are **not** vectors. They are the output of running the reference producer against the reference implementation: ``` joulespec harvest --manifest conformance/v1/harvest.toml \ --out conformance/v1 --require-grade E3 ``` The clauses are the conformance items of [`SPEC.md`](../../SPEC.md) §7, read from the published document rather than copied into the manifest — so the manifest cannot drift from the specification. Reword an item and its obligation address moves, and every witness bound to the old wording stops applying. Each obligation is mapped to a check in `joulespec-rs`, and each mapping declares a **counter-artifact**: a one-occurrence edit that should make that check fail. The harvester applies it, runs the check, requires a *failure*, and reverts. Only then does the witness reach `E3`. ### Proofs, beside the checks Two obligations also carry a **proof**, discharged by a bit-precise model checker over the whole input domain rather than at sampled points. A proof entry is distinguished in the manifest by carrying a `formalization` — the binding from clause prose to formal statement — because §2.6 forbids a producer formalizing a clause itself, and making the binding the thing that selects the prover enforces that structurally rather than by a check someone could forget. The prover path refuses the same way the check path does, one rung up: | Observed | Read as | |---|---| | verified, every declared cover satisfied | the statement holds over a non-empty domain | | verified, a cover never reached | **a finding** — proved over a domain the harness's own assumptions emptied | | a property violated | the refutation a counter-artifact is applied to obtain | | undecided, or killed by the budget | **a finding** — neither verdict, and never credited as either | The second row is why the producer parses the property table instead of the verdict line. A model checker reports success for an over-constrained harness in the same words it uses for one that examined everything, so a gate reading the verdict alone passes vacuous proofs. The fourth row is why each harness carries a wall-clock budget: a solver asked a question it cannot settle does not say so, it keeps going. Both proofs sit at **`E2`, not `E4`**, and the report says so in those words. Their statements were refuted against a counter-artifact, so the vacuity axis is satisfied; what is missing is an independently cross-checked formalization. Nobody but the author has confirmed that either statement says what its clause says, and §2.6 caps that at `E2`. The rung is reachable by this producer — it needs a second party, not more code. ### What the proofs cost, and what they caught The reason the ladder has a rung above `E3` is visible here as a measurement rather than an argument. The counter-artifact on C7 narrows the ratio rule's arithmetic from 128 to 64 bits, where a large input overflows the parts-per-million scale: - the **entire test suite passes** under that mutation — 85 tests, none of which reaches an input above roughly `u64::MAX / 1_000_000`; - the **prover refutes it** in a fraction of a second. That is `E3` and `E4` disagreeing on our own code, in the direction the ladder predicts. The cost is not uniform, and that matters more for budgeting than it might seem. The same function, the same input domain and the same solver gave: - **the statement that its arithmetic is total** — no overflow, no division by zero — discharged in under a tenth of a second; - **the statement that its quotient is bounded by the scale** — which requires reasoning about the output bits of a 128-bit division — *did not converge* in twenty-four minutes. Naming a solver that reasons with a bitvector theory instead of bit-blasting moved that wall without removing it: it settled four of the statement's conditions in about eight seconds and then spent over fifty minutes on the fifth. The harness is kept, behind a `cfg` nobody sets so an ordinary run does not hang on it, as the reproducible record of a negative result. Only the first is claimed. The second is named in the harness's own documentation as deliberately unstated, because a harness that quietly narrowed its domain until it converged would report exactly the same success over a much smaller claim. The lesson for an operator is that the top rung's affordability is a property of the statement and of the method together, neither of which the ladder mentions — which is why the budget is declared per harness and not once for a workspace. A second lesson, from the same run: a wall-clock wrapper around the prover is not enough. Both abandoned runs outlived the `timeout` that was supposed to bound them, because the prover is a driver that spawns the checker and a timeout reaches only the driver. The producer kills the **process group**, which is why its budget works where the shell's did not. **These receipts are not reproducible, by construction.** Their energy figures come from a wall clock, graded `Estimator`, because no meter is wired to this harness yet. Re-running the harvest produces different microjoules and therefore different receipt bytes. That is the honest behaviour of a measured quantity and the reason the certifiable pack above holds energy fixed. ## What the harvest found Running this against the implementation it describes did what the `E3` rung exists to do, and found two things inspection had not: 1. **A check that could not see its subject.** One footprint test narrowed to a single member, and on a one-element footprint `all` and `any` are the same function — so the conjunction itself was never checked. Mutating `all` to `any` left the test passing. A second test now covers it. 2. **Dead logic in the implementation.** `applies_at` guarded on the artifact state having no enumerable parts, and that guard could not change a single verdict: an `all` over a non-empty footprint against no parts is already false. The guard looked like care. It is gone. A third report was a mistake in the manifest rather than in the code — a counter-artifact aimed at a branch its check never takes, which the harvester correctly reported as a check that cannot see its subject. The distinction between those two readings is the operator's to make, and the harvester reports what it observed rather than guessing which it is. A fourth finding came from extending this standard rather than from running it. Extracting two rules into named functions — so a prover could be asked about them — moved the text that two existing counter-artifacts were aimed at, by one indentation level in one case. Both mutations silently stopped describing any edit at all. The harvester refused to run, which is the correct outcome but a late one, so it now validates every counter-artifact's anchor **before** running anything. Tolerating a missing anchor would have been the real failure: two clauses would have gone on looking falsifiably evidenced while nothing was being mutated. The harvester exits non-zero on a finding, so a pipeline can gate on it. CI runs it on every change to this standard. Where no model checker is installed the proof entries are reported as not run — an absence, not a pass — and the clauses fall back to their check evidence. The prover's own output parsing is covered by tests in CI regardless, including both traps above.