joulespec: E4 reaches a real prover, an evaluation corpus, §9 narrowed, and the producer reads other specifications #567

Merged

dcharlot merged 3 commits from joulespec/e4-bridge into main 2026-11-01 23:05:37 -05:00

Conversation 0 Commits 3 Files changed 69 +6202 -93

2026-11-01

Transaction Science

joulespec: an evaluation corpus, and a measured limit on what a second solver buys ...

Two things asked for: a benchmark corpus, and a second verification method.

## The corpus

The wire vectors certify that an implementation round-trips a receipt's
bytes. They say nothing about whether it reached the right verdict, because
they carry one scenario. `conformance/v1/evaluation/` is the other half: ten
cases, each a complete set of evaluation inputs plus the verdict §3 requires,
chosen so a plausible but generous implementation disagrees — a mean where a
minimum is required, an unevidenced obligation skipped rather than emptying
the grade, `E3` on a killed counter-artifact whose anchor is unstated, `E4`
because a prover succeeded, a witness for a clause's previous wording
discarded instead of flagged, a `reviewed` label taken at face value when the
reviewer is the clause's own author.

Each case states its direction. Most catch over-grading; one catches
under-grading, and that one is load-bearing: an implementation that graded
nothing at all would pass every over-grading case, so a corpus with one
direction rewards a rule that refuses everything. A test asserts the shape of
the set rather than trusting it was built as described.

The expectations are written by hand from §3 and are never read back out of
this implementation — a corpus whose expectations are whatever the code
produced certifies agreement with itself. That earned its keep immediately:
seven of the ten were wrong on first authoring, all the same mistake and mine
rather than the evaluator's. They assumed the attestation axis came from who
signed a witness, where §2.8 computes it from who authored the work; with no
work declared it is absent. The fix was not to copy the observed value in,
which would have buried the misunderstanding, but to declare work in every
case so the axis is exercised at all.

## What a second method bought, and what it did not

The quotient-bound statement abandoned in the previous commit was retried
under a solver reasoning with a bitvector theory rather than bit-blasting to
a propositional problem. It settled four of the statement's conditions in
about eight seconds — where the default engine had shown no per-property
progress in twenty-four minutes — and then spent over fifty minutes on the
fifth.

So the method moved the wall without removing it, and §8 now says that
instead of implying a solver choice would fix it. The harness is kept as the
reproducible record of a negative result, behind a `cfg` nobody sets so an
ordinary run does not hang on it.

A second finding from the same runs, recorded in `conformance/v1/README.md`: a
wall-clock wrapper around a prover is not enough. Both abandoned runs outlived
the `timeout` meant 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 — the
design was right for a reason that has now been observed twice.

Co-Authored-By: Claude Opus 5 <[email protected]>

06f00e619a

• View at this point in history

2026-11-01 21:56:22 -05:00

Transaction Science

joulespec: the producer reads someone else's specification, not only this one ...

The extractor recognised exactly one document shape — a numbered list of
bolded, labelled items under a named section — which made the producer a tool
for documents written like this family's own. Which shape a document uses is a
fact about the document, so the manifest declares it, and three shapes cover
what requirements are actually written as: a numbered conformance list, a
bulleted requirement list, and a heading per requirement carrying its
identifier.

Only the item *opener* varies. The section is still named, the floor still
fails closed, continuation lines still join with one space, and a shape that
matches nothing is still an error rather than an empty clause list. Under the
heading shape a blank line does not close an item, because a requirement's
prose runs over paragraphs; the next heading of the same depth or shallower
closes it, and a heading carrying no identifier is a grouping heading rather
than a requirement. A heading with no prose under it states nothing and is
dropped: addressing the empty string would create an obligation nobody wrote
and then grade it like any other.

The load-bearing property is that none of this moved an existing obligation.
The default shape is what an undeclared manifest selects, and the test pinning
that is not a recording of what the new parser happens to produce — the
address was computed by running the same fixture through the parser as it
stood before the change, in a worktree at the previous commit, and the two
agree. The reference manifest deliberately declares no shape, so it stands as
that check too.

SPEC §8 gains the limit this exposes: an obligation address depends on how the
clause was extracted, so two producers reading one document under different
conventions state different obligations about the same prose and both are
correct. A conforming producer must therefore disclose the convention it
applied, because the document alone is not enough to recompute the addresses.

There is deliberately no shape-free convenience wrapper. A caller that did not
have to name a shape would read some documents correctly and others silently
wrongly, and the obligation addresses are computed from whatever it captured.

Co-Authored-By: Claude Opus 5 <[email protected]>

1a3cca29c2

• View at this point in history

2026-11-01 20:57:57 -05:00

Transaction Science

joulespec: the E4 rung reaches a real prover, and §9 gives the nearest prior art its due ...

Two gaps, both found by looking harder at what already exists.

§9 did not mention requirements-traceability tooling, which is the nearest
thing to an existing implementation of §3. That family binds evidence to a
requirement by identifier and revision, and its strongest member reads the
test runner's results rather than the sources, so a citation on a test that
never ran binds nothing. That is this standard's E2, reached independently,
and E2 is therefore not a contribution here. What the family leaves open is
what this standard closes: the revision is bumped by hand, where an obligation
address is computed; and its own documentation records that a passing test
asserting nothing still satisfies the gate, with test quality deferred to a
separate human review. The closing claim is narrowed accordingly. Also noted:
immutable tests are not falsifiable tests — an immutable test that asserts
nothing is immutably vacuous.

E4 was specified and its logic tested, but no witness had ever come from a
prover. `joulespec-cli` now drives one, and parses the property table rather
than the verdict line, because a checker reports success for a harness whose
assumptions emptied its domain in the same words it uses for one that examined
all of it — a gate reading the verdict passes vacuous proofs. Each harness
carries a wall-clock budget, so an undecided run is a finding rather than a
hang, and the process group is killed rather than the driver, which was
observed leaving the solver running. Two statements are discharged over their
whole input domain, both refuted by a counter-artifact; both sit at E2, not
E4, because nobody independent has cross-checked their formalizations, and the
report says so in those words.

Measured, on this workspace: the counter-artifact narrowing the ratio rule's
arithmetic from 128 to 64 bits is invisible to all 85 tests and refuted by the
prover at once. The cost is not uniform — the same function's totality was
settled in under a tenth of a second while its quotient bound did not converge
in twenty-four minutes, so the budget is declared per harness and §8 says why
a statement reshaped until it converges is a different claim.

Extending this found a fourth defect in the standard's own manifest: extracting
two rules into named functions moved the text two counter-artifacts were aimed
at, by one indentation level in one case, and both silently stopped describing
any edit. The harvester refused to run, which was correct but late, so it now
validates every anchor before running anything. Tolerating a missing anchor
would have left two clauses looking falsifiably evidenced while nothing was
being mutated. SPEC §2.5 also now states the rules the producer already
followed but the standard did not: a counter-artifact that does not build has
demonstrated nothing, and a harness reporting success having run no checks is
not evidence that any ran.

CI gains a proofs leg on a host that has a checker. The linux leg cannot gate
this: with no prover installed the proof entries are correctly reported as not
run, which is no gate at all. The new leg asserts every declared cover is
reached and that a counter-artifact still refutes a proof; its output parsing
was tested against a passing, a vacuous and a no-cover log before being
trusted.

Co-Authored-By: Claude Opus 5 <[email protected]>

4286242db5

• View at this point in history

2026-11-01 18:41:37 -05:00