open-standards/joulespec/conformance/v1/README.md

# 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.