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

dcharlot commented 2026-11-01 18:42:50 -05:00

Owner

Copy link

Two gaps, both from the same question: has the field already solved this, and does the top rung actually work?

§9 — the nearest prior art was missing

The section covered assurance cases, certified-airborne traceability, supply-chain provenance, mutation testing and carbon intensity, but not requirements-traceability tooling — which is the closest thing to an existing implementation of §3.

That family binds evidence to a requirement by identifier~revision, and its strongest member reads the test runner's results rather than the sources: a citation on a test that never ran binds nothing. That is this standard's E2, reached independently and from a different direction, so E2 is not a contribution here and §9 now says so. Two things the family leaves open are what this standard closes:

• the revision is bumped by hand, so drift detection depends on an author noticing that an edit changed meaning — the judgement §2.1's computed address removes from human hands;
• its own documentation records that a passing test which asserts nothing still satisfies the gate, deferring test quality to a separate human review. §2.5's counter-artifact is that review, mechanized.

Also added: enforced spec-first frameworks hold tests immutable, which is not falsifiability — an immutable test that asserts nothing is immutably vacuous. The closing novelty claim is narrowed to four things rather than left broad.

E4 now reaches a prover

It was specified and its logic tested, but no witness had ever come from one. joulespec-cli drives a model checker and parses the property table, not the verdict line — 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, so a gate reading the verdict passes vacuous proofs.

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 an emptied domain
a property violated	the refutation a counter-artifact seeks
undecided, or killed by the budget	a finding — never credited as either verdict

Each harness carries a wall-clock budget, so an undecided run is a finding rather than a hang. The budget kills the process group, not the driver — killing only the driver was observed leaving the solver running.

Two statements are discharged over their whole input domain and both are 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. The rung needs a second party, not more code.

What it measured

The counter-artifact narrowing the ratio rule's arithmetic from 128 to 64 bits, where a large input overflows the parts-per-million scale:

• all 85 tests pass under it — none reaches an input above roughly u64::MAX / 1_000_000;
• the prover refutes it at once.

E3 and E4 disagreeing on our own code, in the direction the ladder predicts.

The cost is not uniform. Same function, same domain, same solver: totality settled in under a tenth of a second; the quotient bound, which needs the output bits of a 128-bit division, did not converge in twenty-four minutes and was abandoned. Only the first is claimed, and the harness says the second is deliberately unstated — a harness quietly narrowed until it converges reports the same success over a smaller claim. §8 records this: the top rung's affordability is a property of the statement, not the code.

A fourth defect, from extending it

Extracting two rules into named functions moved the text two existing 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 was the real risk: two clauses would have gone on looking falsifiably evidenced while nothing was mutated.

SPEC §2.5 also now states two rules the producer already followed but the standard never wrote down: 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.

The producer now reads someone else's specification

Second commit. The extractor recognised exactly one document shape, which made this a tool for documents written like ours. Which shape a document uses is a fact about the document, so the manifest declares it:

[spec]
document = "docs/requirements.md"
section  = "2. Requirements"
shape    = "heading-label"     # or bulleted-bold-label; omitted = numbered
expect_at_least = 14           # the floor still fails closed

Only the item opener varies. Under heading-label a blank line does not close an item (a requirement's prose runs over paragraphs — the next heading of equal or shallower depth closes it); a heading with no identifier is a grouping heading, not a requirement; and a heading with no prose under it is dropped, because addressing the empty string would create an obligation nobody wrote and then grade it.

The load-bearing property is that no existing obligation moved. The pinned address in that test is not a recording of what the new parser produces — it was computed by running the same fixture through the parser as it stood at the previous commit, in a separate worktree, and the two agree. The reference manifest declares no shape on purpose, so it stands as that check too.

§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 disclose the convention it applied.

An evaluation corpus

Third commit. The wire vectors certify a receipt's bytes; they say nothing about whether an implementation reached the right verdict, because they carry one scenario. conformance/v1/evaluation/ is the other half — ten cases, each a full 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 instead of emptying the grade · E3 on a killed counter-artifact whose anchor is unstated · E4 because a prover succeeded (declared grounding, and separately unchecked vacuity) · a witness bound to a superseded state counted · 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 single-direction corpus 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 hand-written from §3 and never read back out of the implementation. A corpus whose expectations are whatever the code produced certifies agreement with itself. That earned its keep at once: 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 solver bought, and what it did not

The quotient-bound statement abandoned above was retried under a solver reasoning with a bitvector theory instead of bit-blasting to a propositional problem:

Method	Outcome
bit-blasting to SAT (default engine)	no per-property progress in 24 minutes
SMT bitvector theory	4 of ~51 conditions in ~8 seconds, then over 50 minutes on the 5th

So the method moved the wall without removing it, and §8 now says that rather than 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 those runs: 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 — the design was right for a reason now observed twice.

Verification

On the build host, all under --locked:

cargo check --workspace --all-targets                 Finished
cargo clippy --workspace --all-targets -D warnings    zero warnings
cargo test --workspace                                48 + 85 + 2 + 2 passed, 0 failed
proofs live                                           4 of 4 covers satisfied, SUCCESSFUL (both)
harvest --require-grade E3                            grade E3, 0 flags, 0 open, exit 0
                                                      24 witnesses (22 checks + 2 proofs)

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 under bash against a passing, a vacuous and a no-cover log before being trusted — an earlier version of that gate was wrong, and only the negative logs showed it.

🤖 Generated with Claude Code

Two gaps, both from the same question: has the field already solved this, and does the top rung actually work? ## §9 — the nearest prior art was missing The section covered assurance cases, certified-airborne traceability, supply-chain provenance, mutation testing and carbon intensity, but not **requirements-traceability tooling** — which is the closest thing to an existing implementation of §3. That family binds evidence to a requirement by `identifier~revision`, and its strongest member reads the **test runner's results** rather than the sources: a citation on a test that never ran binds nothing. That is this standard's `E2`, reached independently and from a different direction, so `E2` is not a contribution here and §9 now says so. Two things the family leaves open are what this standard closes: - the revision is **bumped by hand**, so drift detection depends on an author noticing that an edit changed meaning — the judgement §2.1's computed address removes from human hands; - its own documentation records that **a passing test which asserts nothing still satisfies the gate**, deferring test quality to a separate human review. §2.5's counter-artifact is that review, mechanized. Also added: enforced spec-first frameworks hold tests **immutable**, which is not falsifiability — an immutable test that asserts nothing is immutably vacuous. The closing novelty claim is narrowed to four things rather than left broad. ## `E4` now reaches a prover It was specified and its logic tested, but no witness had ever come from one. `joulespec-cli` drives a model checker and **parses the property table, not the verdict line** — 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, so a gate reading the verdict passes vacuous proofs. | 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 an emptied domain | | a property violated | the refutation a counter-artifact seeks | | undecided, or killed by the budget | **a finding** — never credited as either verdict | Each harness carries a wall-clock budget, so an undecided run is a finding rather than a hang. The budget kills the **process group**, not the driver — killing only the driver was observed leaving the solver running. Two statements are discharged over their whole input domain and both are 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. The rung needs a second party, not more code. ## What it measured The counter-artifact narrowing the ratio rule's arithmetic from 128 to 64 bits, where a large input overflows the parts-per-million scale: - **all 85 tests pass** under it — none reaches an input above roughly `u64::MAX / 1_000_000`; - **the prover refutes it** at once. `E3` and `E4` disagreeing on our own code, in the direction the ladder predicts. The cost is not uniform. Same function, same domain, same solver: **totality** settled in under a tenth of a second; the **quotient bound**, which needs the output bits of a 128-bit division, *did not converge in twenty-four minutes* and was abandoned. Only the first is claimed, and the harness says the second is deliberately unstated — a harness quietly narrowed until it converges reports the same success over a smaller claim. §8 records this: the top rung's affordability is a property of the statement, not the code. ## A fourth defect, from extending it Extracting two rules into named functions moved the text two existing 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 was the real risk: two clauses would have gone on looking falsifiably evidenced while nothing was mutated. SPEC §2.5 also now states two rules the producer already followed but the standard never wrote down: 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. ## The producer now reads someone else's specification Second commit. The extractor recognised exactly one document shape, which made this a tool for documents written like ours. Which shape a document uses is a fact about the document, so the manifest declares it: ```toml [spec] document = "docs/requirements.md" section = "2. Requirements" shape = "heading-label" # or bulleted-bold-label; omitted = numbered expect_at_least = 14 # the floor still fails closed ``` Only the item *opener* varies. Under `heading-label` a blank line does not close an item (a requirement's prose runs over paragraphs — the next heading of equal or shallower depth closes it); a heading with no identifier is a grouping heading, not a requirement; and a heading with no prose under it is dropped, because addressing the empty string would create an obligation nobody wrote and then grade it. **The load-bearing property is that no existing obligation moved.** The pinned address in that test is not a recording of what the new parser produces — it was computed by running the same fixture through the parser as it stood at the previous commit, in a separate worktree, and the two agree. The reference manifest declares no shape on purpose, so it stands as that check too. §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 disclose the convention it applied. ## An evaluation corpus Third commit. The wire vectors certify a receipt's **bytes**; they say nothing about whether an implementation reached the right **verdict**, because they carry one scenario. `conformance/v1/evaluation/` is the other half — ten cases, each a full 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 instead of emptying the grade · `E3` on a killed counter-artifact whose anchor is unstated · `E4` because a prover succeeded (declared grounding, and separately unchecked vacuity) · a witness bound to a superseded state counted · 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 single-direction corpus 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 hand-written from §3 and never read back out of the implementation.** A corpus whose expectations are whatever the code produced certifies agreement with itself. That earned its keep at once: 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 solver bought, and what it did not The quotient-bound statement abandoned above was retried under a solver reasoning with a **bitvector theory** instead of bit-blasting to a propositional problem: | Method | Outcome | |---|---| | bit-blasting to SAT (default engine) | no per-property progress in 24 minutes | | SMT bitvector theory | 4 of ~51 conditions in ~8 seconds, then **over 50 minutes** on the 5th | So the method moved the wall without removing it, and §8 now says that rather than 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 those runs: **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* — the design was right for a reason now observed twice. ## Verification On the build host, all under `--locked`: ``` cargo check --workspace --all-targets Finished cargo clippy --workspace --all-targets -D warnings zero warnings cargo test --workspace 48 + 85 + 2 + 2 passed, 0 failed proofs live 4 of 4 covers satisfied, SUCCESSFUL (both) harvest --require-grade E3 grade E3, 0 flags, 0 open, exit 0 24 witnesses (22 checks + 2 proofs) ``` 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 under `bash` against a passing, a vacuous and a no-cover log before being trusted — an earlier version of that gate was wrong, and only the negative logs showed it. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-11-01 18:42:50 -05:00

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

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]>

dcharlot added 1 commit 2026-11-01 20:58:03 -05:00

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

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]>

dcharlot changed title from joulespec: the E4 rung reaches a real prover, and §9 gives the nearest prior art its due to joulespec: E4 reaches a real prover, §9 gives the nearest prior art its due, and the producer reads other specifications 2026-11-01 20:58:20 -05:00

dcharlot added 1 commit 2026-11-01 21:56:32 -05:00

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

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]>

dcharlot changed title from joulespec: E4 reaches a real prover, §9 gives the nearest prior art its due, and the producer reads other specifications to joulespec: E4 reaches a real prover, an evaluation corpus, §9 narrowed, and the producer reads other specifications 2026-11-01 21:56:49 -05:00

dcharlot merged commit 16e17cc81d into main 2026-11-01 23:05:37 -05:00

dcharlot referenced this pull request from a commit 2026-11-01 23:05:38 -05:00

Merge pull request 'joulespec: E4 reaches a real prover, an evaluation corpus, §9 narrowed, and the producer reads other specifications' (#567) from joulespec/e4-bridge into main

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!567

No description provided.