Transaction-Science/open-standards
Watch
1
0
Fork
You've already forked open-standards
 0
Code Issues Pull requests Projects Releases 15 Packages Wiki Activity Actions 5

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
69 changed files with 6202 additions and 93 deletions
Download patch file Download diff file Expand all files Collapse all files

64
.github/workflows/standards-build.yml vendored
View file

@ -99,6 +99,15 @@ jobs:
# it found a test whose assertion could not fail and a branch that
# could not change a verdict.
- { name: joulespec-rs, dir: joulespec/joulespec-rs, runner: linux, clippy: true, harvest: true }
# The same workspace again on a host that has a model checker, to
# gate the proof path. The `linux` leg above cannot: with no prover
# installed the harvest reports the proof entries as not run, which
# is the right behaviour and no gate at all. `proofs: true` runs the
# harnesses live and, more importantly, checks that a
# counter-artifact still refutes one -- a proof that survives
# breaking the thing it proves is a proof of nothing, and that can
# decay silently in a way the parser's unit tests cannot see.
- { name: joulespec-proofs, dir: joulespec/joulespec-rs, runner: macos, proofs: true }
- { name: openpay, dir: openpay, runner: linux-arm64 }
- { name: joule-code-rs, dir: joule-code/joule-code-rs, runner: linux-arm64, z3: true }
- { name: map-rs, dir: map/map-rs, runner: linux-arm64, conformance: map-conformance }
@ -330,6 +339,61 @@ jobs:
exit 1
fi
# Both directions of the proof path, live.
#
# The first run must verify with every declared reachability cover
# satisfied -- a checker reports success for an over-constrained harness
# in the same words it uses for one that examined everything, so the
# cover line is what distinguishes them and is asserted here directly.
#
# The second run is the one that matters. It narrows the ratio rule's
# arithmetic from 128 bits to 64 and requires the prover to FAIL. The
# entire test suite passes under that same mutation, so this step is the
# only place in CI where the rung above `E3` is shown to be doing
# anything.
- name: Proof harnesses verify, with every cover reached
if: matrix.proofs
working-directory: ${{ matrix.dir }}
run: |
set -euo pipefail
export PATH="$HOME/.cargo/bin:$PATH"
cargo kani --version
for h in the_ratio_rule_is_total_over_every_input \
widening_a_set_can_only_lower_its_cap; do
echo "== $h =="
out="$(cargo kani -p joulespec-core --harness "$h" 2>&1)"
echo "$out" | grep -E '^ \*\* |^VERIFICATION'
echo "$out" | grep -q '^VERIFICATION:- SUCCESSFUL' \
|| { echo "$h did not verify"; exit 1; }
# "N of M cover properties satisfied". Both numbers are read with
# their own expression rather than by splitting one capture, so
# the gate does not depend on the shell's word-splitting rules.
line="$(echo "$out" | grep -E '^ \*\* [0-9]+ of [0-9]+ cover properties satisfied$' || true)"
[ -n "$line" ] || { echo "$h declared no cover"; exit 1; }
got="$(echo "$line" | sed -E 's/^ \*\* ([0-9]+) of ([0-9]+) .*$/\1/')"
want="$(echo "$line" | sed -E 's/^ \*\* ([0-9]+) of ([0-9]+) .*$/\2/')"
[ "$got" = "$want" ] \
|| { echo "$h: only $got of $want covers reached -- proved over an empty domain"; exit 1; }
done
- name: A counter-artifact still refutes a proof
if: matrix.proofs
working-directory: ${{ matrix.dir }}
run: |
set -euo pipefail
export PATH="$HOME/.cargo/bin:$PATH"
f=crates/joulespec-core/src/conform.rs
before="$(grep -c 'u128::from(part)' "$f")"
[ "$before" = "1" ] || { echo "expected one anchor, found $before"; exit 1; }
trap 'git checkout -- "$f"' EXIT
sed -i.ci -e 's|^ Some(((u128::from(part).*$| Some((part * 1_000_000) / total)|' "$f"
rm -f "$f.ci"
grep -q 'u128::from(part)' "$f" && { echo "the mutation did not apply"; exit 1; }
echo "mutation applied: the scale is now computed in 64 bits"
out="$(cargo kani -p joulespec-core --harness the_ratio_rule_is_total_over_every_input 2>&1 || true)"
echo "$out" | grep -E '^ \*\* |^VERIFICATION'
echo "$out" | grep -q '^VERIFICATION:- FAILED' \
|| { echo "the prover did not refute an overflowing ratio rule"; exit 1; }
# The NVML backends sit behind features no workspace member enables
# (jcp-energy `nvml`, eoc-meter `cuda`, jouleclaw-energy `nvml`), so the
# step above never compiles them, let alone runs their tests. Here they

2
README.md
View file

@ -185,7 +185,7 @@ derived from the evidence and never from a verdict handed in, so every claim in
one is reproducible by anyone holding the same inputs.
- **Licence:** Apache-2.0 for reference code (see [`joulespec/LICENSE`](joulespec/LICENSE)); CC-BY-4.0 for specification text (see [`joulespec/LICENSE-SPEC`](joulespec/LICENSE-SPEC)).
- **Status:** v0.2.0-draft.1. `SPEC.md` published, with §9 setting out what it takes from assurance-case structure, certified-airborne traceability, supply-chain provenance levels, mutation testing and carbon-intensity accounting, and what it adds to each; reference workspace `joulespec-rs/` — `joulespec-core` carries obligation-addressed clauses and signed revisions, the graded evidence ladder with oracle anchoring, vacuity and independence computed from key disjointness, the deterministic two-axis evaluator with both minima, the four flag conditions and footprint-aware staleness, the revision partition, and the `joulespec/1` JCR-1 receipt with its per-clause audit. `joulespec-cli` is the reference **producer**: it reads clauses from the published specification document, runs each declared check, runs it again against a declared counter-artifact, and emits a signed witness only at the rung the observations support — distinguishing a check that failed from one that did not compile from one that should not have passed. Two conformance packs: byte-stable wire vectors carrying one witness of every rung plus one bound to a superseded state, and the standard **applied to its own implementation**, where every conformance item of §7 reaches `E3` against a counter-artifact that made its check fail. That exercise found a test whose assertion could not fail and a branch that could not change a verdict, both now fixed; CI gates on it. `cargo test --workspace` green, `cargo clippy --workspace --all-targets` zero warnings and gated in CI.
- **Status:** v0.3.0-draft.1. `SPEC.md` published, with §9 setting out what it takes from requirements-traceability tooling, assurance-case structure, certified-airborne traceability, supply-chain provenance levels, mutation testing and carbon-intensity accounting, and what it adds to each. The traceability family is the nearest prior art and narrows the claim honestly: it already binds evidence to a requirement by identifier and revision, and its strongest member already requires the covering check to have *run* — so `E2` is independent convergence rather than a contribution. What it leaves open is what this standard closes: the revision is bumped by hand, where an obligation address is computed; and a passing check that asserts nothing still satisfies such a gate, with test quality deferred to human review, where `E3` makes it mechanical. Reference workspace `joulespec-rs/` — `joulespec-core` carries obligation-addressed clauses and signed revisions, the graded evidence ladder with oracle anchoring, vacuity and independence computed from key disjointness, the deterministic two-axis evaluator with both minima, the four flag conditions and footprint-aware staleness, the revision partition, and the `joulespec/1` JCR-1 receipt with its per-clause audit. `joulespec-cli` is the reference **producer**: it reads clauses from the published specification document, runs each declared check, runs it again against a declared counter-artifact, and emits a signed witness only at the rung the observations support — distinguishing a check that failed from one that did not compile from one that should not have passed. It also drives a **model checker** for the `E4` path, where it parses the property table rather than the verdict line: a checker reports success for a harness whose assumptions emptied the domain in the same words it uses for one that examined all of it, so a gate reading the verdict passes vacuous proofs. A budget per harness makes an undecided run a finding instead of a hang. Two conformance packs: byte-stable wire vectors carrying one witness of every rung plus one bound to a superseded state, and the standard **applied to its own implementation**, where every conformance item of §7 reaches `E3` against a counter-artifact that made its check fail, and two items also carry a proof discharged over their whole input domain. That exercise keeps finding real defects inspection missed — a test whose assertion could not fail, a branch that could not change a verdict, and two counter-artifacts silently aimed at text a refactor had moved, which now fails closed before anything runs. It also measured why the top rung exists: the counter-artifact that narrows the ratio rule's arithmetic to 64 bits is invisible to the whole test suite and refuted by the prover at once. `cargo test --workspace` green, `cargo clippy --workspace --all-targets` zero warnings, both gated in CI alongside the harvest and a live proof leg.
## How this is organised

54
joulespec/README.md
View file

@ -289,6 +289,27 @@ and **passed** is a finding: the check cannot see the thing it is about. The
harvester exits non-zero on findings, so a pipeline can gate on them, and CI
gates on this one.
It reads **someone else's specification**, not only this one. Requirements
live in a few conventional shapes — a numbered conformance list, a bulleted
requirement list, a heading per requirement carrying its identifier — and
which one a document uses is a fact about that 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
```
Nothing else about the extraction varies, and a heading that states no
requirement is not read as one — addressing the empty string would create an
obligation nobody wrote and then grade it. Changing the declared shape moves
every obligation address, which is correct rather than unfortunate: a
different extraction describes different obligations. It does mean the shape
is part of what an auditor needs in order to recompute them.
Three things in the manifest are declared because they are human judgements the
standard refuses to guess: which check stands for which obligation (the same
act as formalizing a clause, SPEC §2.6), each check's anchor, and each check's
@ -306,13 +327,24 @@ single member, and on a one-element footprint `all` and `any` are the same
function — so mutating the conjunction left the test green, and the conjunction
was never actually checked. And a guard in `applies_at` could not change a
single verdict: an `all` over a non-empty footprint against no enumerable parts
is already false. The guard looked like care. Both are recorded in
is already false. The guard looked like care.
Extending the standard found a third. Pulling two rules out into named
functions — so a prover could be asked about them over their whole input
domain — moved the text two existing counter-artifacts were aimed at, by a
single indentation level in one case, and both silently stopped describing any
edit at all. The harvester refused to run, which was right but late, so it now
validates every 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.
All of it is recorded in
[`conformance/v1/README.md`](conformance/v1/README.md), and that is the `E3`
rung doing the only thing it claims to do.
## Conformance packs
Two, answering different questions:
Three, answering different questions:
- [`conformance/v1/vectors/`](conformance/v1/vectors/) — **the certifiable
surface.** Fixed keys, clauses, witnesses and energy, byte-stable, carrying
@ -321,10 +353,20 @@ Two, answering different questions:
Its verdict is the doctrine in miniature: two obligations well evidenced, one
carrying only the implementer's citation, and the specification therefore
graded `E0` at `A0`.
- The self-conformance receipt beside it — **a measurement, not a vector.** Its
energy comes from a wall clock, so re-running the harvest produces different
bytes. A pack that held measured energy fixed would be publishing a figure
nobody measured.
- [`conformance/v1/evaluation/`](conformance/v1/evaluation/) — **the verdicts,
not the bytes.** Round-tripping a receipt says nothing about whether an
implementation graded correctly, because the vectors carry one scenario. Each
case here is a complete set of evaluation inputs plus the verdict §3
requires, chosen so that a plausible but generous implementation disagrees: a
mean where a minimum is required, `E3` awarded on a killed counter-artifact
whose anchor is unstated, `E4` awarded because a prover succeeded, a witness
for a clause's previous wording discarded instead of flagged. Most cases
catch over-grading; at least one catches under-grading, because an
implementation that graded nothing would pass all the others.
- The self-conformance receipt beside them — **a measurement, not a vector.**
Its energy comes from a wall clock, so re-running the harvest produces
different bytes. A pack that held measured energy fixed would be publishing a
figure nobody measured.
## Relation to existing work

168
joulespec/SPEC.md
View file

@ -3,7 +3,7 @@
| | |
|---|---|
| **Standard** | joulespec |
| **Status** | v0.2.0 draft for review |
| **Status** | v0.3.0 draft for review |
| **Profile** | `joulespec/1` |
| **Licence** | Specification text CC-BY-4.0 ([`LICENSE-SPEC`](LICENSE-SPEC)); reference code Apache-2.0 ([`LICENSE`](LICENSE)) |
| **Reference** | [`joulespec-rs/`](joulespec-rs/) |
@ -229,6 +229,26 @@ So `E4` requires the statement to have been **refuted** against a named
counter-model (§2.6), exactly as `E3` requires a check to have failed against
a counter-artifact. Nothing reaches either rung on a passing run alone.
#### A counter-artifact that does not build has demonstrated nothing
A check that "fails" because the artifact no longer compiles has not shown
that it can notice the obligation being violated. It has shown that the
toolchain can notice a broken edit, which was never in doubt. A conforming
producer MUST distinguish a check that **ran and failed** from one that could
not run, and MUST NOT credit the second toward `E3`.
The same applies to the absence of a run at all: a check harness that reports
success having executed no checks is indistinguishable, from its exit status
alone, from one that executed all of them. A conforming producer MUST observe
that at least one check ran, and not infer it from a successful exit.
Mutation tooling draws the first line already, reporting mutants that fail to
compile separately from its results rather than counting them: such a mutant
is inconclusive about the checks rather than evidence about them. This
standard needs the distinction for a different reason — not to keep a score
honest, but because crediting a failed build as a demonstrated failure would
manufacture falsifiability out of a syntax error.
#### Where the expectation comes from
A check's ability to fail is not only an empirical question. An oracle whose
@ -307,6 +327,32 @@ discarding it would lose evidence that exists.
This is the same boundary the family's verification standard draws from the
other side when it records that a proof is not a specification.
#### What refutes vacuity, for a machine-checked statement
A prover's success verdict does not refute vacuity, and a conforming producer
MUST NOT treat it as though it had. A verifier reports success for a harness
whose assumptions have eliminated the states the statement was about, and it
reports that in the same words it uses for a harness that examined all of
them. The verdict is therefore the same shape of silence as a test binary that
runs no tests and exits zero (§2.5).
Refutation requires two observations the verdict does not contain:
1. every reachability cover the harness declares is **satisfied** — each names
a state the statement is supposed to be about, and a satisfied cover is a
concrete path reaching it; and
2. a counter-artifact applied to the proved code makes the verification
**fail**, with the counterexample standing as the named counter-model.
A harness declaring no cover is `unchecked`, never `refuted`: it has offered
nothing that distinguishes an examined domain from an empty one. A conforming
producer MUST raise a flag (§3.4) on such a harness rather than grading it
quietly — something is wrong with the evidence set, not merely weak about one
obligation.
The first observation is what the prover was asked; the second is what the
ladder asks of every rung above `E2`.
### 2.7 Work
Work is a unit of effort performed against a specification — a coding
@ -667,6 +713,14 @@ figure nobody measured.
## 8. The honest limit
**An obligation address depends on how the clause was extracted.** The
address covers the clause's kind and text, and the text is whatever a producer
captured from the document. Two producers reading one document under different
conventions — a numbered list versus a heading per requirement — state
different obligations about the same prose, and both are behaving correctly. A
conforming producer MUST therefore disclose the convention it applied, because
the document alone is not enough to recompute the addresses.
**JouleSpec cannot tell whether a clause says what its author meant.** An
obligation is addressed, signed and tracked, and it may still be the wrong
requirement, badly worded, or quietly contradicted by another clause. This
@ -710,6 +764,30 @@ in the check. Reproduction of a vacuous check reproduces the vacuity.
cross-specification comparison of microjoules per obligation is not a weaker
measurement; it is not a measurement.
**`E4` is not uniformly affordable, and the ladder does not say so.** The
rungs are ordered by what they establish, which says nothing about what they
cost to reach. Measured on this standard's own implementation, over one
function and one input domain: the statement that its arithmetic is total was
discharged in under a tenth of a second, and the statement that its quotient
is bounded by the scale — which requires reasoning about the output bits of a
wide division — did not converge in twenty-four minutes.
Changing the *method* moved that wall without removing it. Re-run under a
solver reasoning with a bitvector theory rather than bit-blasting to a
propositional problem, the same statement settled most of its conditions
almost at once and then spent over fifty minutes on one. So the cost is not
simply a property of the engine either, and an operator cannot expect to buy
convergence by choosing a different one.
An operator should read two things into that. A budget belongs to a harness
rather than to a workspace, because one figure cannot be both large enough for
the statements worth proving and small enough to gate on. And a statement
reshaped until the prover converges has not become cheaper to prove — it has
become a different and usually smaller claim, reported in the same words. The
standard can require the budget to be declared and an overrun to be reported
as undecided. It cannot tell that a converging statement is the one that
mattered.
**Two of the results this standard builds on are thinly evidenced.** The
vacuity rate quoted in §2.5 comes from one industrial verification setting, and
the oracle-anchoring effect it reports comes from a single-system study by a
@ -751,10 +829,68 @@ requires both is stating two different things, and should.
deployment can carry provenance levels for its artifacts and attestation grades
for its evidence, and they answer different questions.
**Mutation testing** supplies the counter-artifact. §2.5 records why the
equivalent-mutant problem that makes mutation *scores* contested cannot
inflate a grade here, and why one killed mutant per obligation is a
deliberately cheap bar rather than an attempt at a score.
**Requirements-traceability tooling** is the nearest existing implementation
of the evaluation in §3, and the closest thing to prior art this standard has.
Tools in that family address a requirement by an identifier carrying a
**revision**, and a covering test cites that identifier and revision together.
Rewording a requirement bumps its revision, at which point citations of the
old revision stop counting toward coverage. The strongest member of the family
goes further and reads the test *runner's results*, not the sources: a
citation on a test that never ran binds nothing, and an obligation counts as
covered only once a bound test has run and passed.
That is this standard's `E2`, reached independently and from a different
direction, and it is the best evidence available that the rung is real. `E2`
is therefore not a contribution here. Two things the family leaves open are:
- **The revision is bumped by hand.** Drift detection depends on an author
recognizing that an edit changed a requirement's meaning and incrementing a
number. A reworded clause whose revision was not bumped keeps its old
evidence, and nothing notices — which is the failure §2.1's computed address
exists to remove from human hands. The field identified the right binding and
left its trigger to discipline.
- **The family documents its own limit.** A passing test that asserts nothing
still satisfies such a gate, and judging whether a test is worth anything is
deferred to a separate human review. §2.5's counter-artifact is that review
step, mechanized. This is where this standard departs, and it is the only
place at `E2`/`E3` where it does.
**Enforced spec-first agent frameworks** supply discipline the agent cannot
edit around: a deterministic orchestrator, human approval gates, and tests
held immutable through the build. Immutability is not falsifiability. An
immutable test that asserts nothing is immutably vacuous, and preventing an
agent from weakening a check says nothing about whether that check could ever
have failed. The two compose cleanly and answer different questions: a
conforming deployment can hold its checks immutable *and* grade them, and
should.
**The field states this gap about itself.** Comparative assessments of the
spec-driven frameworks find none covering the full span of a process taxonomy,
name excessive trust in generated artifacts as a standing risk, and report an
absence of benchmarks for evaluating the process as a whole. Requirements
engineering work on the same shift records that the field lacks evaluation
frameworks for verifying requirements satisfaction and traceability. Current
tool comparisons list verification as absent in the leading frameworks,
enforcement as convention, and every drift reconciliation as a manual command
someone has to remember to run. This standard does not supply the missing
benchmark. It supplies the quantity a benchmark would have to measure.
**Mutation testing** supplies the counter-artifact, and mature engines exist
for generating mutants automatically. §2.5 records why the equivalent-mutant
problem that makes mutation *scores* contested cannot inflate a grade here,
and why one killed mutant per obligation is a deliberately cheap bar rather
than an attempt at a score.
A **declared** counter-artifact is preferred here to a generated score, for
reasons of addressing rather than quality. A score is an aggregate over
mutants no particular obligation is about, so it cannot say which clause is
falsifiably evidenced; its denominator moves when unrelated code changes; and
a surviving equivalent mutant is indistinguishable from a genuine gap. A
counter-artifact named against one obligation answers one question — can this
check notice this clause being violated — and answers it per clause, which is
the granularity everything downstream of §3 needs. The two are compatible: an
engine is a good way to *find* a candidate counter-artifact that a manifest
then names.
**Carbon-intensity accounting for software** is an international standard
expressing emissions as a rate per functional unit of work. §5.3 has the same
@ -764,11 +900,23 @@ outside its scope, which is the quantity measured here. The two are
complementary rather than competing, and a deployment reporting both is
reporting a system's operation and its construction.
What is new here is the conjunction: an obligation address that survives
renaming and breaks on rewording, a grade that requires a demonstrated
failure above `E2`, a footprint that keeps evidence alive across unrelated
change, and a per-obligation energy figure. Each part has precedent; the
combination is what makes conformance a measured quantity rather than a claim.
So the claim worth making is narrow. Binding evidence to a requirement is
established practice; requiring that the bound check actually ran is too. What
is left, once the nearest neighbours are given their due, is four things and
their conjunction:
- an obligation **address** rather than a hand-maintained revision, so that
rewording invalidates evidence whether or not anyone noticed the rewording;
- a **demonstrated failure** required above `E2`, replacing the human review
step that the traceability family explicitly defers;
- a **footprint**, so that evidence survives change it did not depend on and
the previous point stays affordable; and
- a **per-obligation energy figure**, which nothing in either family reports.
Each part has precedent except the last. The combination is what makes
conformance a measured quantity rather than a claim, and the measurement is
the point: the field's own assessments say it lacks the means to evaluate
whether a specification was satisfied, not that it lacks opinions about it.
---

103
joulespec/conformance/v1/README.md
View file

@ -33,6 +33,18 @@ 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`
@ -54,6 +66,82 @@ 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
@ -80,5 +168,18 @@ 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.
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.

21
joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/expect.json Normal file
View file

@ -0,0 +1,21 @@
{
"intent": "One obligation at E3, one at E0.",
"trap": "Averaging the rungs, or reporting the best, gives E3 or E1 where §3.2 requires the minimum.",
"direction": "over-grading",
"grade": "cited",
"attestation": "self-attested",
"flags": [],
"clauses": [
{
"label": "C1",
"grade": "falsifiable",
"stale": 0
},
{
"label": "C2",
"grade": "cited",
"stale": 0
}
],
"conformant_at_e3": false
}

120
joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/spec.json Normal file
View file

@ -0,0 +1,120 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The first obligation is well evidenced."
},
{
"label": "C2",
"kind": "requirement",
"text": "The second obligation is only claimed."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
43,
42,
11,
171,
119,
207,
160,
61,
162,
144,
245,
20,
230,
204,
135,
222,
27,
198,
221,
151,
150,
139,
70,
10,
15,
59,
131,
156,
246,
73,
96,
74,
147,
64,
46,
226,
82,
95,
82,
156,
208,
5,
42,
73,
137,
132,
140,
67,
141,
40,
141,
18,
4,
208,
243,
54,
220,
199,
96,
189,
176,
84,
127,
9
]
}

7
joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

239
joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/witnesses.json Normal file
View file

@ -0,0 +1,239 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:cef4d60f560ca59fa02f71adc7c734f9a84f3f69278c629aec9d912d6a5ffab1",
"obligation": "b3:d35a2f3ff28be1718133d7457d98466bebd16f5ee260fab64d4482ca33c5176d",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "falsifiable",
"check": "a_named_check",
"anchor": "specification",
"counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
229,
32,
61,
59,
203,
181,
133,
53,
241,
40,
78,
229,
150,
186,
241,
117,
143,
128,
227,
64,
75,
163,
95,
205,
36,
126,
169,
34,
103,
10,
36,
35,
230,
154,
132,
78,
97,
217,
194,
209,
117,
213,
48,
254,
92,
117,
217,
242,
207,
228,
41,
161,
153,
169,
92,
104,
85,
94,
59,
249,
116,
220,
163,
0
]
},
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:cef4d60f560ca59fa02f71adc7c734f9a84f3f69278c629aec9d912d6a5ffab1",
"obligation": "b3:03ad09e8fb25c85b62516d1d12ad26d9674b06713e215790fff2fc4a91e85ec5",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "cited"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
},
"sig": [
226,
48,
153,
132,
46,
194,
110,
25,
109,
194,
27,
217,
139,
66,
55,
44,
152,
188,
42,
27,
147,
187,
97,
244,
73,
234,
205,
195,
138,
100,
51,
62,
84,
123,
198,
111,
243,
234,
41,
163,
114,
94,
156,
250,
146,
1,
43,
183,
202,
107,
44,
123,
226,
54,
17,
42,
106,
218,
127,
124,
202,
0,
94,
7
]
}
]

46
joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:d35a2f3ff28be1718133d7457d98466bebd16f5ee260fab64d4482ca33c5176d"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

21
joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/expect.json Normal file
View file

@ -0,0 +1,21 @@
{
"intent": "One obligation at E3; the other has no witness.",
"trap": "Skipping the unevidenced clause and grading the rest gives E3. Absence orders below every rung, so the grade is absent — not E0, which would claim a citation nobody made.",
"direction": "over-grading",
"grade": null,
"attestation": null,
"flags": [],
"clauses": [
{
"label": "C1",
"grade": "falsifiable",
"stale": 0
},
{
"label": "C2",
"grade": null,
"stale": 0
}
],
"conformant_at_e3": false
}

120
joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/spec.json Normal file
View file

@ -0,0 +1,120 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The first obligation is well evidenced."
},
{
"label": "C2",
"kind": "requirement",
"text": "The second obligation has no evidence at all."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
24,
240,
18,
59,
164,
67,
152,
178,
106,
233,
237,
196,
133,
34,
134,
161,
102,
182,
221,
82,
197,
127,
60,
87,
223,
174,
33,
158,
103,
38,
226,
108,
133,
29,
212,
31,
117,
225,
176,
28,
94,
209,
209,
122,
27,
98,
133,
254,
159,
181,
235,
242,
120,
166,
81,
90,
146,
230,
106,
126,
60,
212,
181,
0
]
}

7
joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

122
joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/witnesses.json Normal file
View file

@ -0,0 +1,122 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:0641fe3157ee1e83e6db71a32d9d4134609f2d758b5d09dbe06943ae61faa8fb",
"obligation": "b3:d35a2f3ff28be1718133d7457d98466bebd16f5ee260fab64d4482ca33c5176d",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "falsifiable",
"check": "a_named_check",
"anchor": "specification",
"counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
119,
170,
207,
159,
41,
140,
205,
144,
124,
120,
97,
19,
237,
207,
111,
218,
98,
85,
158,
181,
94,
228,
228,
93,
6,
32,
116,
189,
206,
250,
228,
147,
19,
218,
111,
207,
136,
160,
146,
166,
8,
90,
217,
151,
133,
237,
49,
222,
97,
197,
2,
216,
122,
203,
137,
191,
26,
140,
153,
191,
96,
234,
244,
3
]
}
]

46
joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:d35a2f3ff28be1718133d7457d98466bebd16f5ee260fab64d4482ca33c5176d"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

21
joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/expect.json Normal file
View file

@ -0,0 +1,21 @@
{
"intent": "A requirement at E3 beside an unwitnessed non-goal.",
"trap": "Treating the non-goal as an owed obligation with no evidence empties the grade. A non-goal is owed nothing, so its absence of evidence is the correct state and caps nothing.",
"direction": "under-grading",
"grade": "falsifiable",
"attestation": "independent",
"flags": [],
"clauses": [
{
"label": "C1",
"grade": "falsifiable",
"stale": 0
},
{
"label": "C2",
"grade": null,
"stale": 0
}
],
"conformant_at_e3": true
}

120
joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/spec.json Normal file
View file

@ -0,0 +1,120 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The obligation is well evidenced."
},
{
"label": "C2",
"kind": "non-goal",
"text": "This is deliberately not built."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
148,
34,
18,
119,
136,
194,
111,
179,
250,
200,
72,
216,
47,
65,
201,
173,
111,
205,
137,
157,
48,
136,
202,
31,
192,
213,
202,
244,
238,
224,
159,
203,
69,
144,
72,
131,
31,
192,
235,
61,
246,
47,
78,
143,
63,
240,
126,
85,
162,
221,
46,
196,
85,
63,
54,
129,
42,
251,
227,
224,
114,
191,
90,
9
]
}

7
joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

122
joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/witnesses.json Normal file
View file

@ -0,0 +1,122 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:ffdfffcba2e4f36037ca82c0a47700a4e564c6c4a10c46c4f8d0206f0437edcd",
"obligation": "b3:67e5769e5089a2c5457c2e0ff5f7d3305974debf4daf2d86e89c9be91529aa52",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "falsifiable",
"check": "a_named_check",
"anchor": "specification",
"counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
231,
240,
3,
175,
92,
232,
84,
168,
214,
242,
128,
109,
55,
113,
41,
32,
125,
124,
161,
115,
248,
255,
49,
84,
61,
33,
230,
6,
254,
112,
111,
13,
5,
194,
177,
86,
151,
156,
151,
92,
52,
187,
238,
41,
186,
181,
53,
164,
87,
23,
3,
65,
59,
200,
84,
224,
210,
72,
139,
166,
102,
155,
236,
10
]
}
]

46
joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:67e5769e5089a2c5457c2e0ff5f7d3305974debf4daf2d86e89c9be91529aa52"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

23
joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/expect.json Normal file
View file

@ -0,0 +1,23 @@
{
"intent": "Something implements the clause that says not to.",
"trap": "Counting the non-goal's evidence as a rung, or discarding it quietly. It is a flag, and §3.4 makes any flag block conformance even where every grade is satisfied.",
"direction": "over-grading",
"grade": "falsifiable",
"attestation": "independent",
"flags": [
"NonGoalWitnessed"
],
"clauses": [
{
"label": "C1",
"grade": "falsifiable",
"stale": 0
},
{
"label": "C2",
"grade": null,
"stale": 0
}
],
"conformant_at_e3": false
}

120
joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/spec.json Normal file
View file

@ -0,0 +1,120 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The obligation is well evidenced."
},
{
"label": "C2",
"kind": "non-goal",
"text": "This is deliberately not built."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
148,
34,
18,
119,
136,
194,
111,
179,
250,
200,
72,
216,
47,
65,
201,
173,
111,
205,
137,
157,
48,
136,
202,
31,
192,
213,
202,
244,
238,
224,
159,
203,
69,
144,
72,
131,
31,
192,
235,
61,
246,
47,
78,
143,
63,
240,
126,
85,
162,
221,
46,
196,
85,
63,
54,
129,
42,
251,
227,
224,
114,
191,
90,
9
]
}

7
joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

242
joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/witnesses.json Normal file
View file

@ -0,0 +1,242 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:ffdfffcba2e4f36037ca82c0a47700a4e564c6c4a10c46c4f8d0206f0437edcd",
"obligation": "b3:67e5769e5089a2c5457c2e0ff5f7d3305974debf4daf2d86e89c9be91529aa52",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "falsifiable",
"check": "a_named_check",
"anchor": "specification",
"counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
231,
240,
3,
175,
92,
232,
84,
168,
214,
242,
128,
109,
55,
113,
41,
32,
125,
124,
161,
115,
248,
255,
49,
84,
61,
33,
230,
6,
254,
112,
111,
13,
5,
194,
177,
86,
151,
156,
151,
92,
52,
187,
238,
41,
186,
181,
53,
164,
87,
23,
3,
65,
59,
200,
84,
224,
210,
72,
139,
166,
102,
155,
236,
10
]
},
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:ffdfffcba2e4f36037ca82c0a47700a4e564c6c4a10c46c4f8d0206f0437edcd",
"obligation": "b3:8aeed8e56271b17bb7fbb1a5a8bc814ad581e580baed6b01f8c5ff8edac61482",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "falsifiable",
"check": "a_named_check",
"anchor": "specification",
"counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
1,
144,
245,
9,
32,
177,
171,
158,
34,
33,
244,
100,
186,
237,
109,
60,
206,
17,
235,
80,
252,
249,
14,
164,
29,
150,
109,
57,
0,
82,
57,
0,
62,
235,
236,
149,
209,
92,
104,
135,
221,
67,
177,
172,
96,
246,
161,
152,
189,
54,
151,
50,
227,
237,
252,
7,
226,
2,
170,
13,
230,
177,
22,
7
]
}
]

46
joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:67e5769e5089a2c5457c2e0ff5f7d3305974debf4daf2d86e89c9be91529aa52"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

16
joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/expect.json Normal file
View file

@ -0,0 +1,16 @@
{
"intent": "A check with a killed counter-artifact but no stated anchor.",
"trap": "Reading the counter-artifact alone and awarding E3. An oracle derived from the system under test cannot disagree with it, so §2.5 caps an unstated anchor at E2 however the check behaved.",
"direction": "over-grading",
"grade": "exercised",
"attestation": "independent",
"flags": [],
"clauses": [
{
"label": "C1",
"grade": "exercised",
"stale": 0
}
],
"conformant_at_e3": false
}

115
joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/spec.json Normal file
View file

@ -0,0 +1,115 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The obligation is checked by something whose expectation is unstated."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
232,
129,
54,
56,
154,
252,
10,
27,
228,
77,
131,
255,
86,
208,
193,
211,
51,
101,
191,
130,
245,
173,
127,
222,
86,
185,
33,
142,
97,
29,
87,
128,
121,
59,
48,
83,
240,
192,
143,
134,
2,
201,
119,
57,
60,
187,
47,
173,
252,
12,
254,
177,
128,
243,
41,
150,
140,
229,
214,
167,
69,
16,
17,
11
]
}

7
joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

122
joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/witnesses.json Normal file
View file

@ -0,0 +1,122 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:dce42be27effefc874f8a4d8736726214fa4083f63a8b09f31de75bfdb2ecfac",
"obligation": "b3:1428edd294ce74bde484645da000d51e306b9461352d65d15af70d4edd1097e4",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "falsifiable",
"check": "a_named_check",
"anchor": "unstated",
"counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
30,
26,
52,
122,
153,
151,
227,
74,
32,
83,
224,
192,
214,
151,
134,
108,
196,
18,
254,
63,
94,
178,
168,
112,
217,
229,
36,
2,
89,
13,
160,
87,
58,
111,
130,
90,
18,
202,
228,
56,
156,
20,
200,
92,
8,
3,
15,
183,
239,
38,
28,
120,
212,
183,
188,
187,
255,
3,
245,
189,
28,
58,
186,
11
]
}
]

46
joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:1428edd294ce74bde484645da000d51e306b9461352d65d15af70d4edd1097e4"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

16
joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/expect.json Normal file
View file

@ -0,0 +1,16 @@
{
"intent": "A non-vacuous proof whose binding to the clause is the prover's own word.",
"trap": "Awarding E4 because a prover succeeded. The proof is real machine-checked evidence about something — E2 — and that the something is this clause is unconfirmed (§2.6).",
"direction": "over-grading",
"grade": "exercised",
"attestation": "independent",
"flags": [],
"clauses": [
{
"label": "C1",
"grade": "exercised",
"stale": 0
}
],
"conformant_at_e3": false
}

115
joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/spec.json Normal file
View file

@ -0,0 +1,115 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The obligation is discharged as a proof under the prover's own formalization."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
230,
223,
192,
92,
86,
73,
29,
122,
19,
51,
241,
40,
231,
16,
76,
150,
148,
103,
16,
62,
242,
129,
100,
44,
166,
222,
27,
231,
71,
35,
103,
15,
120,
141,
76,
15,
72,
148,
166,
177,
220,
220,
140,
43,
144,
170,
178,
240,
14,
79,
146,
87,
125,
29,
218,
36,
240,
91,
137,
161,
25,
30,
227,
4
]
}

7
joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

129
joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/witnesses.json Normal file
View file

@ -0,0 +1,129 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:60e5ec581d01948a179d8fd98bac59e7061fa8fc15098e0f1a6b8af76883ef99",
"obligation": "b3:e535081843369fb6415f4c0c13e6568c3757123ca4e0147fdd9b905929045d69",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "proved",
"goal": "b3:bbc98522dfcf0bb13e1772dcecc655fa0c92eabacbc7a226e38ff74e5f0606ce",
"tier": "corpus",
"formalization": {
"statement": "forall x. p(x)",
"grounding": "declared"
},
"vacuity": {
"kind": "refuted",
"counter": "b3:def80a6779418b717f5b005941967d6597889e965986d59b2c55b6c0e0c5b5ae"
}
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
0,
230,
197,
84,
90,
168,
192,
148,
227,
30,
136,
67,
160,
127,
227,
253,
245,
182,
63,
145,
154,
33,
23,
38,
191,
193,
141,
169,
115,
236,
54,
145,
85,
249,
15,
173,
58,
191,
25,
146,
88,
138,
85,
208,
164,
12,
143,
101,
244,
241,
40,
119,
18,
105,
207,
239,
48,
65,
190,
21,
164,
98,
52,
15
]
}
]

46
joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:e535081843369fb6415f4c0c13e6568c3757123ca4e0147fdd9b905929045d69"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

16
joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/expect.json Normal file
View file

@ -0,0 +1,16 @@
{
"intent": "A proof with an independently cross-checked formalization, never shown capable of failing.",
"trap": "Awarding E4 because the formalization was cross-checked. A property can hold because nothing reaches the condition it guards; every rung above E2 rests on a demonstrated failure.",
"direction": "over-grading",
"grade": "exercised",
"attestation": "independent",
"flags": [],
"clauses": [
{
"label": "C1",
"grade": "exercised",
"stale": 0
}
],
"conformant_at_e3": false
}

115
joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/spec.json Normal file
View file

@ -0,0 +1,115 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The obligation is discharged as a proof nobody checked for vacuity."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
113,
95,
117,
58,
54,
173,
175,
188,
219,
96,
201,
130,
85,
193,
40,
235,
114,
127,
56,
130,
232,
129,
196,
116,
222,
78,
28,
230,
187,
100,
191,
84,
73,
174,
219,
166,
138,
218,
9,
209,
167,
43,
243,
124,
36,
53,
115,
129,
203,
95,
97,
140,
147,
238,
49,
226,
96,
172,
32,
217,
198,
126,
81,
0
]
}

7
joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

165
joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/witnesses.json Normal file
View file

@ -0,0 +1,165 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:0684fbbba22698b8874acd5de02e14d60e571595ed5667001b1eac2c65712112",
"obligation": "b3:8c38bdd6981befcc0b784b8b2861b77682fa66493ec48e80e6815e5b063940f6",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "proved",
"goal": "b3:bbc98522dfcf0bb13e1772dcecc655fa0c92eabacbc7a226e38ff74e5f0606ce",
"tier": "corpus",
"formalization": {
"statement": "forall x. p(x)",
"grounding": {
"cross-checked": {
"by": [
237,
73,
40,
198,
40,
209,
194,
198,
234,
233,
3,
56,
144,
89,
149,
97,
41,
89,
39,
58,
92,
99,
249,
54,
54,
193,
70,
20,
172,
135,
55,
209
]
}
}
},
"vacuity": {
"kind": "unchecked"
}
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
219,
188,
206,
146,
168,
110,
89,
117,
145,
154,
6,
148,
185,
190,
229,
110,
164,
234,
106,
100,
135,
158,
55,
114,
107,
7,
8,
66,
186,
255,
210,
171,
150,
88,
119,
148,
246,
243,
196,
37,
217,
70,
36,
113,
200,
248,
159,
141,
36,
116,
167,
96,
105,
40,
228,
228,
44,
169,
239,
32,
115,
127,
96,
2
]
}
]

46
joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:8c38bdd6981befcc0b784b8b2861b77682fa66493ec48e80e6815e5b063940f6"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

16
joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/expect.json Normal file
View file

@ -0,0 +1,16 @@
{
"intent": "The only witness observed a tree that is no longer the artifact, and declared no footprint.",
"trap": "Counting it because it verifies and names a stated obligation. An empty footprint means the whole artifact, so any change to the artifact invalidates it — and the clause is then unevidenced, which empties the grade rather than lowering it.",
"direction": "over-grading",
"grade": null,
"attestation": null,
"flags": [],
"clauses": [
{
"label": "C1",
"grade": null,
"stale": 1
}
],
"conformant_at_e3": false
}

115
joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/spec.json Normal file
View file

@ -0,0 +1,115 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The obligation was checked against an earlier tree."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
233,
92,
69,
171,
34,
163,
70,
150,
25,
3,
254,
136,
169,
113,
237,
212,
179,
102,
141,
221,
76,
98,
204,
56,
23,
67,
244,
77,
114,
140,
145,
1,
81,
54,
196,
231,
89,
85,
11,
58,
34,
37,
157,
85,
135,
96,
234,
24,
143,
122,
193,
175,
116,
93,
18,
180,
69,
20,
91,
116,
51,
130,
32,
5
]
}

7
joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

122
joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/witnesses.json Normal file
View file

@ -0,0 +1,122 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:aa55f1c89f6918a7a8f4f232d7d0fb5676ad97109bece106eb4cf71f656cb5fd",
"obligation": "b3:077b78197459d69d43a714aab09a4fd557e64344c5d8fcf04fe3e4b18e800a2b",
"artifact": "b3:c24c4acaeac144d5ae9a9569b55cd6aec79c38f91ded00e1e6029057aa1d1201",
"footprint": [],
"evidence": {
"kind": "falsifiable",
"check": "a_named_check",
"anchor": "specification",
"counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
29,
184,
206,
104,
136,
141,
196,
48,
217,
48,
196,
223,
113,
75,
50,
181,
206,
7,
153,
31,
216,
110,
57,
166,
18,
47,
186,
123,
205,
241,
251,
101,
252,
176,
232,
38,
145,
49,
25,
178,
112,
219,
11,
92,
153,
199,
171,
33,
112,
227,
207,
62,
202,
236,
135,
97,
121,
246,
51,
62,
212,
128,
142,
3
]
}
]

46
joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:077b78197459d69d43a714aab09a4fd557e64344c5d8fcf04fe3e4b18e800a2b"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

18
joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/expect.json Normal file
View file

@ -0,0 +1,18 @@
{
"intent": "A verifying witness whose obligation address is the clause's previous wording.",
"trap": "Discarding it silently, which is how drift stops being visible. It is reported as unbound, and the clause it used to evidence is now unevidenced.",
"direction": "over-grading",
"grade": null,
"attestation": null,
"flags": [
"Unbound"
],
"clauses": [
{
"label": "C1",
"grade": null,
"stale": 0
}
],
"conformant_at_e3": false
}

115
joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/spec.json Normal file
View file

@ -0,0 +1,115 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The obligation as the specification now words it."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
242,
243,
44,
1,
85,
35,
61,
244,
218,
15,
227,
86,
204,
185,
9,
206,
216,
76,
212,
251,
249,
121,
202,
69,
95,
183,
126,
128,
141,
20,
184,
253,
108,
233,
173,
88,
220,
92,
49,
15,
87,
155,
245,
210,
117,
73,
95,
236,
117,
233,
0,
161,
251,
72,
41,
174,
141,
57,
227,
210,
47,
23,
173,
7
]
}

7
joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

122
joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/witnesses.json Normal file
View file

@ -0,0 +1,122 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:63d4bd9c7d506a65fbe39e73c89ebe3a8791e7ebf1e67de1b400d1823fea7469",
"obligation": "b3:ed83074359c0815f20d3525c083da01ad661b06926caa583449c3ef15bb7c737",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "falsifiable",
"check": "a_named_check",
"anchor": "specification",
"counter": "b3:e34e236da4740e55ec1aaabd0d1bcfe74529fa93cde433c07966669601d72eb5"
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
129,
57,
119,
14,
168,
125,
23,
95,
86,
163,
84,
102,
195,
76,
126,
204,
203,
141,
138,
145,
180,
238,
55,
162,
93,
246,
15,
91,
143,
201,
179,
148
]
},
"sig": [
60,
248,
235,
218,
51,
26,
146,
5,
100,
146,
36,
215,
41,
171,
236,
21,
50,
168,
249,
111,
64,
215,
214,
18,
212,
37,
203,
136,
220,
181,
250,
79,
154,
206,
224,
26,
227,
82,
100,
102,
81,
115,
226,
201,
80,
103,
90,
222,
176,
69,
200,
235,
148,
102,
190,
11,
89,
8,
200,
241,
186,
18,
217,
5
]
}
]

46
joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:483ce5d0da7b89444fa282cf20196353ad87e422968355db94657869789bd48c"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
202,
147,
172,
23,
5,
24,
112,
113,
214,
123,
131,
199,
255,
14,
254,
129,
8,
232,
236,
69,
48,
87,
93,
119,
38,
135,
147,
51,
219,
218,
190,
124
]
}
]

16
joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/expect.json Normal file
View file

@ -0,0 +1,16 @@
{
"intent": "The reviewer and the specification's author are one key.",
"trap": "Awarding E1 because the evidence says `reviewed`. E1 requires a second party, and independence is computed from the keys rather than taken from the label.",
"direction": "over-grading",
"grade": "cited",
"attestation": "self-attested",
"flags": [],
"clauses": [
{
"label": "C1",
"grade": "cited",
"stale": 0
}
],
"conformant_at_e3": false
}

115
joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/spec.json Normal file
View file

@ -0,0 +1,115 @@
{
"spec": {
"profile": "joulespec/1",
"alg": 1,
"intent": "A corpus case: the clauses exist to be graded, not to be implemented.",
"clauses": [
{
"label": "C1",
"kind": "requirement",
"text": "The obligation was reviewed by the party that wrote the specification."
}
],
"parent": null,
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
22,
25,
146,
110,
125,
175,
67,
93,
121,
173,
183,
240,
187,
20,
158,
240,
234,
215,
207,
191,
34,
212,
54,
243,
70,
176,
53,
163,
4,
198,
1,
172,
185,
230,
168,
59,
242,
139,
251,
94,
165,
165,
160,
39,
73,
180,
177,
119,
168,
203,
196,
41,
100,
247,
132,
54,
94,
66,
65,
41,
168,
96,
99,
8
]
}

7
joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/state.json Normal file
View file

@ -0,0 +1,7 @@
{
"address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"parts": [
"b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b",
"b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e"
]
}

153
joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/witnesses.json Normal file
View file

@ -0,0 +1,153 @@
[
{
"witness": {
"profile": "joulespec-witness/1",
"alg": 1,
"spec_id": "b3:5d33c00c7f19db758ce990bdfdeb777fb700d05965cf1708ccf2c411c5bacce4",
"obligation": "b3:fadbf5bf4219d3004b998eee6e2d4b77049554a2be7c5ab804a681f6ecffbe7c",
"artifact": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9",
"footprint": [],
"evidence": {
"kind": "reviewed",
"reviewer": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"energy": {
"uj": 1000,
"provenance": "estimator"
},
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
},
"sig": [
6,
174,
38,
158,
207,
238,
36,
163,
130,
113,
167,
65,
163,
195,
243,
17,
72,
83,
233,
98,
9,
19,
172,
179,
63,
97,
132,
67,
84,
141,
99,
6,
135,
67,
191,
206,
94,
142,
107,
222,
117,
161,
254,
221,
213,
29,
212,
9,
215,
10,
188,
39,
151,
11,
63,
217,
192,
24,
108,
107,
20,
114,
190,
10
]
}
]

46
joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/work.json Normal file
View file

@ -0,0 +1,46 @@
[
{
"id": "b3:78ec055c7256fd5dfc25ab756441f9895afef0dc4a35e15c05dd8a07ae8e0e35",
"cites": [
"b3:fadbf5bf4219d3004b998eee6e2d4b77049554a2be7c5ab804a681f6ecffbe7c"
],
"energy": {
"uj": 500000,
"provenance": "estimator"
},
"author": [
138,
136,
227,
221,
116,
9,
241,
149,
253,
82,
219,
45,
60,
186,
93,
114,
202,
103,
9,
191,
29,
148,
18,
27,
243,
116,
136,
1,
180,
15,
111,
92
]
}
]

85
joulespec/conformance/v1/evaluation/README.md Normal file
View file

@ -0,0 +1,85 @@
# The evaluation corpus
Cases a too-generous implementation passes incorrectly.
The wire vectors in [`../vectors/`](../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.
This corpus is the other half.
Each case directory holds five files. Read the first four, evaluate, and
compare against the fifth:
| File | What it is |
|---|---|
| `spec.json` | the signed specification |
| `state.json` | the artifact state the witnesses were observed at |
| `witnesses.json` | the signed witnesses |
| `work.json` | the declared work, which is what the attestation axis is computed from |
| `expect.json` | the verdict §3 requires, with the trap it sets |
`expect.json` carries its own `intent` and `trap` in prose, so a failing case
says what it was for rather than only which field differed.
## Why the cases are shaped the way they are
Every case states a **direction**. Most are `over-grading`: an
implementation that reports conformance never established, which is the
failure this standard exists to stop. At least one is `under-grading`,
because an implementation that graded nothing at all would pass every
over-grading case — a corpus with only one direction rewards a rule that
refuses everything. A test asserts that both directions are present, that
every over-grading case's correct verdict falls short of the bar or is
blocked by a flag, and that every under-grading case's correct verdict
reaches it.
The traps are the ones that are reachable by accident rather than by
carelessness:
- a **mean** instead of a minimum, which lets well-evidenced obligations
conceal one nobody looked at;
- **skipping** an unevidenced obligation rather than letting its absence
empty the grade — and reporting `E0` there, which would claim a citation
nobody made;
- treating an **unwitnessed non-goal** as an owed obligation with no
evidence, which is the under-grading case;
- grading a **witnessed non-goal**'s evidence, or discarding it quietly,
instead of raising the flag that blocks conformance;
- awarding `E3` on a killed counter-artifact alone, where the check's
**anchor is unstated**;
- awarding `E4` because a prover succeeded, where the **formalization is the
prover's own word** or its **vacuity was never checked** — two independent
ways a proof establishes nothing about a clause;
- counting a witness bound to a **superseded state**, which an empty
footprint makes stale on any change at all;
- silently discarding a witness whose obligation address is a clause's
**previous wording**, which is exactly how drift stops being visible;
- reading `reviewed` off the evidence label when the **reviewer is the
clause's own author**.
## Where the expected verdicts come from
They are written by hand from §3 of the specification. They are **not**
read back out of this implementation: a corpus whose expectations are
whatever the code produced would certify agreement with itself and nothing
else.
That distinction earned its keep while this corpus was being written. Seven
of the ten expectations were wrong on first authoring — all the same mistake,
and the author's rather than the evaluator's. They assumed the attestation
axis was computed from who signed a *witness*, when §2.8 computes it from who
authored the *work*; with no work declared, attestation is absent. The fix was
not to copy the observed value into the expectation, which would have hidden
the misunderstanding, but to declare work in every case so that the axis is
actually exercised.
## Regenerating
```
JOULESPEC_GEN_EVALUATION=1 cargo test -p joulespec-core --test evaluation
```
That republishes the input files and the expectations **as the test states
them**. Without the variable the test reads the published expectation back and
asserts it still agrees with the test's own, so an expectation edited in one
place and not the other fails rather than drifting.

99
joulespec/conformance/v1/harvest.toml
View file

@ -29,6 +29,10 @@ steward = "did:key:joulespec-reference-steward"
document = "../../SPEC.md"
section = "7. Conformance"
expect_at_least = 11
# `shape` is deliberately not declared here. Omitting it selects the numbered
# conformance list this family's specifications use, which is what this
# manifest was written against -- so this file also stands as the check that a
# manifest predating the declared shape keeps every obligation address it had.
intent = """
The joulespec/1 reference implementation does what SPEC.md §7 says it does, \
and each claim is evidenced by a check demonstrated capable of failing.\
@ -125,12 +129,8 @@ anchor = "specification"
footprint = ["crates/joulespec-core/src/conform.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = """ .map(|c| c.grade)
.min()
.unwrap_or(None);"""
replace = """ .map(|c| c.grade)
.max()
.unwrap_or(None);"""
find = " graded.into_iter().min().unwrap_or(None)"
replace = " graded.into_iter().max().unwrap_or(None)"
breaks = "takes the strongest owed obligation instead of the weakest"
[[evidence]]
@ -189,12 +189,12 @@ anchor = "specification"
footprint = ["crates/joulespec-core/src/conform.rs"]
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = """ if total == 0 {
return None;
}"""
replace = """ if total == 0 {
return Some(0);
}"""
find = """ if total == 0 {
return None;
}"""
replace = """ if total == 0 {
return Some(0);
}"""
breaks = "reports a ratio of nothing as zero rather than absent"
# ── C8 — Receipts ─────────────────────────────────────────────────────────
@ -320,3 +320,78 @@ find = """ let any_independent =
replace = """ let any_independent = !implementers.is_empty();
if any_independent {"""
breaks = "calls agreement among implementers reproduction"
# A proof, not a check. C7 says ratios are integer parts-per-million; the two
# checks above cover the provenance rule and the absent-not-zero rule, and
# neither covers whether the arithmetic on the way to the ratio is defined at
# all. That is the half sampling cannot reach: the inputs that break it are a
# `part` above roughly u64::MAX / 1_000_000, which no hand-written case picks.
#
# Measured on this workspace: the mutation below is invisible to the entire
# test suite and refuted by the prover in a fraction of a second. That gap is
# the reason the ladder has a rung above E3.
#
# The grounding is `declared`, so this witness is graded `E2` and not `E4`
# (SPEC §2.6). Nobody independent of its author has confirmed that the
# statement below says what C7 says, and recording the proof at its real rung
# is the point of having the axis.
[[evidence]]
clause = "C7"
check = "proofs::the_ratio_rule_is_total_over_every_input"
anchor = "specification"
footprint = [
"crates/joulespec-core/src/conform.rs",
"crates/joulespec-core/src/proofs.rs",
]
[evidence.formalization]
package = "joulespec-core"
grounding = "declared"
budget_seconds = 300
statement = """
For all part, rest : u64 --- every arithmetic operation performed by
conform::ppm(part, rest) is defined: none overflows and none divides by zero.
Discharged over the whole input domain by the checker's arithmetic checks,
with reachability covers for the absent case, the computed case, the
overflowing-whole case, and a part large enough to overflow the scale in 64
bits.
The companion statement --- that the quotient is bounded by the scale --- is
deliberately not made here. It requires the solver to reason about the output
bits of a 128-bit division and did not converge; see the README.
"""
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = " Some(((u128::from(part) * 1_000_000) / u128::from(total)) as u64)"
replace = " Some((part * 1_000_000) / total)"
breaks = "computes the scale in 64 bits, where a large part overflows it"
# A second proof, on the property an adversary has the clearest incentive to
# break. The statement is about `cap` itself -- the function the evaluator
# calls -- so the counter-artifact below is an edit to the artifact, not to a
# copy of the rule living inside the harness.
[[evidence]]
clause = "C5"
check = "proofs::widening_a_set_can_only_lower_its_cap"
anchor = "specification"
footprint = [
"crates/joulespec-core/src/conform.rs",
"crates/joulespec-core/src/proofs.rs",
]
[evidence.formalization]
package = "joulespec-core"
grounding = "declared"
budget_seconds = 300
statement = """
For every set of at most four graded figures and one added figure ---
conform::cap(set) is None whenever any member is None; otherwise it is Some(b)
for some b belonging to the set, and cap(set + extra) <= b; and cap can empty
only because the added figure was itself absent. Discharged over every
combination of ladder rungs and absences a set of that size admits, with
reachability covers for the strictly-lower, unchanged, emptied and
already-empty cases.
"""
[evidence.counter]
file = "crates/joulespec-core/src/conform.rs"
find = " graded.into_iter().min().unwrap_or(None)"
replace = " graded.into_iter().max().unwrap_or(None)"
breaks = "caps a set by its best figure instead of its worst"

4
joulespec/joulespec-rs/Cargo.lock generated
View file

@ -227,7 +227,7 @@ checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
[[package]]
name = "joulespec-cli"
version = "0.2.0"
version = "0.3.0"
dependencies = [
"blake3",
"ed25519-dalek",
@ -240,7 +240,7 @@ dependencies = [
[[package]]
name = "joulespec-core"
version = "0.2.0"
version = "0.3.0"
dependencies = [
"blake3",
"ed25519-dalek",

2
joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml
View file

@ -1,6 +1,6 @@
[package]
name = "joulespec-cli"
version = "0.2.0"
version = "0.3.0"
description = "JouleSpec reference producer and checker: harvests signed witnesses from a project's own test suite, demonstrates each check against a counter-artifact, and seals a joulespec/1 receipt."
edition.workspace = true
license.workspace = true

273
joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs
View file

@ -29,11 +29,14 @@ use std::path::Path;
use ed25519_dalek::SigningKey;
use joulespec_core::conform::ArtifactState;
use joulespec_core::evidence::{Anchor, Evidence, SignedWitness, Witness};
use joulespec_core::evidence::{
Anchor, Evidence, Formalization, Grounding, SignedWitness, Vacuity, Witness,
};
use joulespec_core::spec::{Obligation, SignedSpec, Spec};
use joulespec_core::{Energy, Provenance};
use joulespec_core::{Address, Energy, Provenance};
use crate::manifest::{Manifest, ManifestError};
use crate::prover::{self, ProveError};
use crate::runner::{self, RunError};
use crate::specdoc::{self, SpecDocError};
use crate::tree::{Tree, TreeError};
@ -78,6 +81,12 @@ pub enum HarvestError {
/// support.
#[error("provenance {0:?} is not available to a harness with no meter")]
BadProvenance(String),
/// The prover could not be run.
#[error(transparent)]
Prove(#[from] ProveError),
/// A cross-checking key is not 32 bytes of hex.
#[error("cross-checking key {0:?} is not 32 bytes of hex")]
BadKey(String),
}
/// What happened to one declared mapping.
@ -135,13 +144,71 @@ pub enum Note {
/// The check.
check: String,
},
/// No model checker is installed, so a declared proof could not be run.
///
/// Recorded rather than skipped: an absent prover is why an obligation
/// has no proof evidence, and a report that omitted it would read like a
/// manifest that never declared one.
ProverAbsent {
/// The clause.
clause: String,
/// The harness.
check: String,
},
/// **A finding.** The harness declares no reachability cover, so its
/// success distinguishes an examined domain from an empty one (SPEC §2.6).
ProofDeclaresNoCover {
/// The clause.
clause: String,
/// The harness.
check: String,
},
/// **A finding.** The prover did not decide, so the declared evidence
/// does not exist — whatever the reason, the operator must either fix the
/// harness or stop claiming it.
ProofInconclusive {
/// The clause.
clause: String,
/// The harness.
check: String,
/// What was observed.
detail: String,
},
/// **A finding.** The statement holds, but over an empty domain: a cover
/// the harness declared names states that never occur.
ProofVacuous {
/// The clause.
clause: String,
/// The harness.
check: String,
/// How many declared covers were never reached.
unreached: usize,
},
/// The prover found the statement false. Either the artifact violates the
/// clause or the statement is not the clause; both need a human.
ProofDidNotHold {
/// The clause.
clause: String,
/// The harness.
check: String,
/// What was observed.
detail: String,
},
}
impl Note {
/// Whether this note reports something the operator must act on.
#[must_use]
pub const fn is_finding(&self) -> bool {
matches!(self, Self::CounterDidNotFail { .. } | Self::CheckDidNotRun { .. })
matches!(
self,
Self::CounterDidNotFail { .. }
| Self::CheckDidNotRun { .. }
| Self::ProofDeclaresNoCover { .. }
| Self::ProofInconclusive { .. }
| Self::ProofVacuous { .. }
| Self::ProofDidNotHold { .. }
)
}
/// A line for the report.
@ -167,6 +234,23 @@ impl Note {
Self::NoCounterDeclared { clause, check } => {
format!("{clause:<5} E2 {check}: no counter-artifact declared")
}
Self::ProverAbsent { clause, check } => {
format!("{clause:<5} -- {check}: no model checker installed; proof not run")
}
Self::ProofDeclaresNoCover { clause, check } => format!(
"{clause:<5} -- {check}: FINDING -- the harness declares no cover, so \
its success shows nothing was examined"
),
Self::ProofInconclusive { clause, check, detail } => format!(
"{clause:<5} -- {check}: FINDING -- the prover did not decide ({detail})"
),
Self::ProofVacuous { clause, check, unreached } => format!(
"{clause:<5} -- {check}: FINDING -- proved over an empty domain; \
{unreached} declared cover(s) never reached"
),
Self::ProofDidNotHold { clause, check, detail } => format!(
"{clause:<5} -- {check}: FINDING -- the statement does not hold ({detail})"
),
}
}
}
@ -200,6 +284,29 @@ fn anchor_of(name: &str) -> Result<Anchor, HarvestError> {
}
}
/// Read a declared grounding, with the key it names.
///
/// The manifest schema has already refused an unknown grounding and a
/// cross-check with no key, so the only work left is decoding the key.
fn grounding_of(f: &crate::manifest::Formalization) -> Result<Grounding, HarvestError> {
match f.grounding.as_str() {
"cross-checked" => {
let hex = f.by.as_deref().unwrap_or_default();
let raw = (0..hex.len())
.step_by(2)
.map(|i| u8::from_str_radix(hex.get(i..i + 2).unwrap_or("zz"), 16))
.collect::<Result<Vec<u8>, _>>()
.map_err(|_| HarvestError::BadKey(hex.to_string()))?;
let by: [u8; 32] = raw
.try_into()
.map_err(|_| HarvestError::BadKey(hex.to_string()))?;
Ok(Grounding::CrossChecked { by })
}
// `declared` is the only other value the schema admits.
_ => Ok(Grounding::Declared),
}
}
fn provenance_of(name: &str) -> Result<Provenance, HarvestError> {
match name {
"estimator" => Ok(Provenance::Estimator),
@ -233,13 +340,19 @@ pub fn harvest(
path: doc_path.to_string_lossy().into_owned(),
source,
})?;
let shape = match manifest.spec.shape.as_deref() {
Some(name) => specdoc::Shape::parse(name)?,
None => specdoc::Shape::default(),
};
let items = specdoc::items(
&document,
&manifest.spec.section,
manifest.spec.expect_at_least,
shape,
)?;
let labels: Vec<String> = items.iter().map(|i| i.label.clone()).collect();
manifest.check_clauses(&labels)?;
manifest.check_counters(&workspace)?;
let spec = Spec::new(
manifest.spec.intent.clone(),
@ -281,6 +394,160 @@ pub fn harvest(
let anchor = anchor_of(&entry.anchor)?;
let footprint = tree.footprint(&entry.footprint)?;
// ── a declared proof takes the prover, not the test harness ──────
//
// The two paths stay separate rather than sharing a "run it" step,
// because what counts as having established something differs: a
// test must have run, a proof must have examined a non-empty domain.
// Collapsing them would lose exactly that distinction.
if let Some(f) = &entry.formalization {
if !prover::available(&workspace) {
notes.push(Note::ProverAbsent {
clause: entry.clause.clone(),
check: entry.check.clone(),
});
continue;
}
let budget = std::time::Duration::from_secs(f.budget_seconds.unwrap_or(1800));
let baseline = prover::prove(&workspace, &f.package, &entry.check, &[], budget)?;
let mut uj = microjoules(baseline.seconds, manifest.energy.watts);
if baseline.declares_no_cover() {
notes.push(Note::ProofDeclaresNoCover {
clause: entry.clause.clone(),
check: entry.check.clone(),
});
continue;
}
if baseline.is_inconclusive() {
notes.push(Note::ProofInconclusive {
clause: entry.clause.clone(),
check: entry.check.clone(),
detail: format!(
"{} undecided, verdict {}, budget {}s",
baseline.undetermined,
baseline.verdict.map_or("none", |v| if v { "success" } else { "failure" }),
budget.as_secs()
),
});
continue;
}
if baseline.covers_unreached() > 0 {
notes.push(Note::ProofVacuous {
clause: entry.clause.clone(),
check: entry.check.clone(),
unreached: baseline.covers_unreached(),
});
continue;
}
if !baseline.demonstrates_proof() {
notes.push(Note::ProofDidNotHold {
clause: entry.clause.clone(),
check: entry.check.clone(),
detail: format!("{} assertion(s) violated", baseline.assertions_failed),
});
continue;
}
// The goal the prover decided. Addressing the harness identity
// together with the statement names what was actually decided —
// it is not a stand-in for a decision that did not happen, and
// the artifact state the witness carries pins the code it ran on.
let goal = Address::of(&serde_json::json!({
"package": f.package,
"harness": entry.check,
"statement": f.statement,
}))?;
let grounding = grounding_of(f)?;
let mut vacuity = Vacuity::Unchecked;
let mut note = Note::NoCounterDeclared {
clause: entry.clause.clone(),
check: entry.check.clone(),
};
if let Some(counter) = &entry.counter {
let (run, counter_address) = {
let _mutation = runner::Mutation::apply(
&workspace,
&counter.file,
&counter.find,
&counter.replace,
)?;
let mutated = tree.reread(
&manifest.artifact.dirs,
&manifest.artifact.files,
&manifest.artifact.extensions,
)?;
(
prover::prove(&workspace, &f.package, &entry.check, &[], budget)?,
mutated.address(),
)
};
uj = uj.saturating_add(microjoules(run.seconds, manifest.energy.watts));
if run.demonstrates_refutation() {
vacuity = Vacuity::Refuted { counter: counter_address };
note = Note::Witnessed {
clause: entry.clause.clone(),
check: entry.check.clone(),
grade: if matches!(grounding, Grounding::CrossChecked { .. }) {
"E4"
} else {
// §2.6: a formalization nobody independent read
// leaves machine-checked evidence about something,
// which is `E2`. Reported here so the demotion is
// visible rather than surprising in the receipt.
"E2 (proof, declared grounding)"
},
detail: format!("refuted when {}", counter.breaks),
};
} else if run.is_inconclusive() {
note = Note::CounterInconclusive {
clause: entry.clause.clone(),
check: entry.check.clone(),
detail: "the prover did not decide the mutated statement".to_string(),
};
} else {
note = Note::CounterDidNotFail {
clause: entry.clause.clone(),
check: entry.check.clone(),
breaks: counter.breaks.clone(),
};
}
}
if matches!(note, Note::NoCounterDeclared { .. }) {
note = Note::Witnessed {
clause: entry.clause.clone(),
check: entry.check.clone(),
grade: "E2 (proof, vacuity unchecked)",
detail: "no counter-artifact declared".to_string(),
};
}
let witness = Witness::new(
spec_id.clone(),
obligation,
state.address.clone(),
Evidence::Proved {
goal,
tier: "bit-precise-model-check".to_string(),
formalization: Formalization {
statement: f.statement.clone(),
grounding,
},
vacuity,
},
Energy::new(uj, provenance),
witness_key.verifying_key().to_bytes(),
)
.with_footprint(footprint)
.sign(witness_key)?;
witnesses.push(witness);
notes.push(note);
continue;
}
let baseline = runner::run_check(&workspace, &entry.check)?;
if baseline.compiled && baseline.ran == 0 {
notes.push(Note::CheckDidNotRun {

1
joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs
View file

@ -22,6 +22,7 @@
mod harvest;
mod manifest;
mod prover;
mod runner;
mod specdoc;
mod tree;

152
joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs
View file

@ -46,6 +46,38 @@ pub enum ManifestError {
/// failure this standard exists to surface.
#[error("the manifest declares no evidence")]
NoEvidence,
/// A formalization declares a grounding this standard does not define.
#[error("clause {clause:?} declares grounding {grounding:?}, which is neither `declared` nor `cross-checked`")]
UnknownGrounding {
/// The clause.
clause: String,
/// The grounding as written.
grounding: String,
},
/// A counter-artifact's anchor text is not in the file exactly once, so
/// the mutation it describes cannot be applied where it was meant to go.
#[error(
"clause {clause:?} check {check:?}: the counter-artifact anchor occurs \
{found} times in {file}, not once"
)]
CounterAnchorMissing {
/// The clause.
clause: String,
/// The check.
check: String,
/// The file.
file: String,
/// How many times the anchor was found.
found: usize,
},
/// A cross-checked formalization names no confirming key, so there is
/// nothing to compare against the witness author and no way to tell
/// independent confirmation from self-assertion.
#[error("clause {clause:?} is cross-checked but names no confirming key")]
UnnamedCrossCheck {
/// The clause.
clause: String,
},
}
/// Where the clauses come from.
@ -58,6 +90,13 @@ pub struct SpecSource {
/// The floor on item count. A parser that matched nothing would otherwise
/// report success having checked nothing.
pub expect_at_least: usize,
/// Which conventional shape the document writes its requirements in.
///
/// Declared because it is a fact about the document, not about this
/// producer. Omitted means a numbered list of bolded, labelled items —
/// what this family's own specifications use — so an existing manifest
/// keeps its obligation addresses unchanged.
pub shape: Option<String>,
/// The specification's intent, in the operator's words.
pub intent: String,
}
@ -100,6 +139,37 @@ pub struct Counter {
pub breaks: String,
}
/// The binding from clause prose to a formal statement.
///
/// Supplied by the operator, never derived: SPEC §2.6 forbids a producer
/// formalizing a clause on its own initiative, because the binding between
/// prose and a formal statement is a human act and the weakest link in any
/// claim of proved conformance.
///
/// Its **presence is what makes an entry a proof**. The schema offers no way
/// to declare a proof without one, which is how the §2.6 rule is enforced
/// structurally rather than by a check that could be forgotten.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct Formalization {
/// The statement the harness discharges, in the operator's words.
pub statement: String,
/// `declared`, or `cross-checked` when an independent party confirmed the
/// statement says what the clause says.
pub grounding: String,
/// The confirming party's verifying key, hex, when cross-checked.
pub by: Option<String>,
/// The package holding the harness.
pub package: String,
/// The wall-clock budget for the prover, in seconds.
///
/// Per harness, because the cost of discharging a statement varies by
/// orders of magnitude with what it quantifies over, and a single
/// workspace-wide figure would be either too small for the statements
/// worth proving or too large to be a gate. Exceeding it is reported as
/// an undecided run, never as a pass or a refutation.
pub budget_seconds: Option<u64>,
}
/// One declared mapping from an obligation to a check.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct Evidence {
@ -116,6 +186,9 @@ pub struct Evidence {
/// The counter-artifact that should make it fail. Without one the check
/// cannot exceed `E2` however carefully it was written.
pub counter: Option<Counter>,
/// When present, `check` names a proof harness rather than a test, and
/// this is its binding to the clause.
pub formalization: Option<Formalization>,
}
/// The whole manifest.
@ -153,10 +226,59 @@ impl Manifest {
check: e.check.clone(),
});
}
if let Some(f) = &e.formalization {
match f.grounding.as_str() {
"declared" => {}
"cross-checked" => {
if f.by.is_none() {
return Err(ManifestError::UnnamedCrossCheck {
clause: e.clause.clone(),
});
}
}
other => {
return Err(ManifestError::UnknownGrounding {
clause: e.clause.clone(),
grounding: other.to_string(),
});
}
}
}
}
Ok(manifest)
}
/// Check every counter-artifact's anchor text is present exactly once,
/// before anything is run.
///
/// A refactor can move the code a mutation was aimed at without touching
/// the manifest, which leaves the counter-artifact pointing at text that
/// no longer exists. Discovering that part-way through a harvest wastes
/// the runs already done; discovering it by *tolerating* it would be
/// worse, because a clause would quietly stop being falsifiably evidenced
/// while its entry still looked present. This has happened once in this
/// repository, to two entries, from one extraction of a function.
pub fn check_counters(&self, workspace: &std::path::Path) -> Result<(), ManifestError> {
for e in &self.evidence {
let Some(counter) = &e.counter else { continue };
let path = workspace.join(&counter.file);
let text = std::fs::read_to_string(&path).map_err(|source| ManifestError::Io {
path: path.to_string_lossy().into_owned(),
source,
})?;
let found = text.matches(&counter.find).count();
if found != 1 {
return Err(ManifestError::CounterAnchorMissing {
clause: e.clause.clone(),
check: e.check.clone(),
file: counter.file.clone(),
found,
});
}
}
Ok(())
}
/// Check every evidence entry names a clause the specification states.
///
/// An entry for an unknown clause would otherwise become an `unbound`
@ -244,6 +366,36 @@ breaks = "puts the label back into the obligation address"
));
}
/// The incident this guards against: a refactor moves the code a
/// mutation was aimed at, and the manifest still names the old text.
#[test]
fn a_counter_artifact_aimed_at_vanished_text_is_caught_before_anything_runs() {
let (dir, path) = write(MANIFEST);
let m = Manifest::read(&path).unwrap();
let src = dir.path().join("crates/joulespec-core/src");
std::fs::create_dir_all(&src).unwrap();
let file = src.join("spec.rs");
std::fs::write(&file, "x\n\"kind\": self.kind.label(), \"text\": self.text\ny\n").unwrap();
assert!(m.check_counters(dir.path()).is_ok(), "the anchor is present once");
// The same edit a refactor would make: the text moves or changes.
std::fs::write(&file, "x\nthe anchor is gone\ny\n").unwrap();
assert!(matches!(
m.check_counters(dir.path()),
Err(ManifestError::CounterAnchorMissing { found: 0, .. })
));
// Two copies are refused too: a mutation that could land in either
// place has not described one artifact state.
let twice = "\"kind\": self.kind.label(), \"text\": self.text";
std::fs::write(&file, format!("{twice}\n{twice}\n")).unwrap();
assert!(matches!(
m.check_counters(dir.path()),
Err(ManifestError::CounterAnchorMissing { found: 2, .. })
));
}
#[test]
fn evidence_for_an_unstated_clause_is_caught_before_sealing() {
let (_d, path) = write(MANIFEST);

456
joulespec/joulespec-rs/crates/joulespec-cli/src/prover.rs Normal file
View file

@ -0,0 +1,456 @@
//! Running a proof harness, and running it against a counter-artifact.
//!
//! This is [`runner`](crate::runner) one rung up, and the reasoning is
//! deliberately the same shape — because the failure it guards against is the
//! same one.
//!
//! ## Why a success verdict is not enough
//!
//! A model checker reports success for a harness whose assumptions have
//! eliminated the states the statement was about, in the same words it uses
//! for a harness that examined all of them. An over-constrained harness is
//! the proof-level equivalent of `running 0 tests`: the tool is not lying,
//! it is answering a question nobody meant to ask.
//!
//! A reachability **cover** is how a harness says which states its statement
//! is supposed to be about. Covers are reported per property as `SATISFIED`,
//! `UNSATISFIABLE`, `UNREACHABLE` or `UNDETERMINED` — and an unreachable
//! cover does *not* fail the run. A gate reading only the final verdict line
//! therefore passes vacuous proofs, which is why this module parses the
//! property table and requires every declared cover to be satisfied.
//!
//! ## The four outcomes
//!
//! | Outcome | Meaning |
//! |---|---|
//! | verified, every cover satisfied | The statement holds over the examined domain, and the domain is not empty. |
//! | verified, a cover unsatisfied | **A flag**: the harness proved something about nothing. |
//! | a property failed | The statement does not hold. Against a counter-artifact, this is the refutation. |
//! | undetermined, or no verdict | **A flag**: the prover did not decide. Neither success nor failure, and never credited as either. |
//!
//! The fourth row is the one a tested-against-success-only parser gets wrong.
//! A solver that runs out of time or meets an unsupported construct has
//! established nothing, and treating it as a refutation would hand out `E4`
//! for a timeout.
use std::io::Read;
use std::os::unix::process::CommandExt;
use std::path::PathBuf;
use std::process::Command;
use std::time::{Duration, Instant};
/// Why a proof could not be run.
#[derive(Debug, thiserror::Error)]
pub enum ProveError {
/// The prover could not be launched.
#[error("cannot run the prover in {dir}: {source}")]
Spawn {
/// The working directory.
dir: PathBuf,
/// The underlying error.
source: std::io::Error,
},
}
/// How one property was decided.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
enum Status {
/// An assertion held, or a cover was satisfied.
Good,
/// An assertion was violated.
Failed,
/// A cover could not be reached, so the states it names never occur.
Unreached,
/// The prover did not decide.
Undetermined,
}
/// The observed outcome of one proof run.
#[derive(Debug, Clone, PartialEq)]
pub struct Proof {
/// Assertions the prover decided favourably.
pub assertions_held: usize,
/// Assertions the prover found violated.
pub assertions_failed: usize,
/// Properties of either kind the prover could not decide.
pub undetermined: usize,
/// Reachability covers the harness declared.
pub covers: usize,
/// Covers shown to be reachable.
pub covers_satisfied: usize,
/// The final verdict line, when the prover printed one.
pub verdict: Option<bool>,
/// Wall-clock seconds for the run.
pub seconds: f64,
}
impl Proof {
/// Whether this run establishes the statement over a non-empty domain.
///
/// Every condition is load-bearing. Dropping the cover conditions admits
/// an over-constrained harness; dropping the undetermined condition
/// admits a partial decision; dropping the verdict condition trusts a
/// property table that may have been truncated by a crash.
#[must_use]
pub fn demonstrates_proof(&self) -> bool {
self.verdict == Some(true)
&& self.assertions_failed == 0
&& self.undetermined == 0
&& self.assertions_held >= 1
&& self.covers >= 1
&& self.covers_satisfied == self.covers
}
/// Whether this run refutes the statement — the signal a counter-artifact
/// is applied to obtain.
///
/// A violated assertion, not merely the absence of success: a prover that
/// timed out has demonstrated nothing, and crediting that as a refutation
/// would award `E4` for running out of time.
#[must_use]
pub fn demonstrates_refutation(&self) -> bool {
self.assertions_failed >= 1 && self.verdict == Some(false)
}
/// Whether the harness declared no cover, and so offered nothing to
/// distinguish an examined domain from an empty one.
#[must_use]
pub fn declares_no_cover(&self) -> bool {
self.covers == 0
}
/// Whether the prover failed to decide, by any of the ways it can.
#[must_use]
pub fn is_inconclusive(&self) -> bool {
self.verdict.is_none() || self.undetermined >= 1
}
/// Covers the harness declared that name states which never occur.
#[must_use]
pub fn covers_unreached(&self) -> usize {
self.covers.saturating_sub(self.covers_satisfied)
}
}
/// Parse a prover's property table and verdict out of its output.
///
/// Written against the documented table rather than the verdict line, for the
/// reason in the module header. Unknown statuses count as undetermined: a
/// status this parser does not recognize is a property it cannot vouch for,
/// and the conservative reading is the one that refuses to grade.
#[must_use]
pub fn parse(output: &str) -> Proof {
let mut p = Proof {
assertions_held: 0,
assertions_failed: 0,
undetermined: 0,
covers: 0,
covers_satisfied: 0,
verdict: None,
seconds: 0.0,
};
// Which kind of property the next `Status:` line belongs to. The check
// line names it; the status arrives on a later line.
let mut pending_cover = false;
for line in output.lines() {
let t = line.trim();
if let Some(rest) = t.strip_prefix("Check ") {
// `Check 3: harness.cover.2`, `...assertion.1`,
// `...arithmetic_overflow.1`, and others.
//
// Only covers are identified positively. Every other property
// class is read as a check, because the classes are open-ended
// and the interesting failures do not all arrive as assertions:
// a counter-artifact that introduces an integer overflow is
// reported as `arithmetic_overflow`, and a parser matching only
// `assertion` would see a clean table and call the mutated run
// inconclusive — or worse, proved.
pending_cover = rest.contains(".cover.");
if pending_cover {
p.covers += 1;
}
continue;
}
if let Some(status) = t.strip_prefix("- Status: ") {
let s = match status.trim() {
"SUCCESS" | "SATISFIED" => Status::Good,
"FAILURE" => Status::Failed,
"UNREACHABLE" | "UNSATISFIABLE" => Status::Unreached,
_ => Status::Undetermined,
};
match (pending_cover, s) {
(true, Status::Good) => p.covers_satisfied += 1,
// An unreachable cover is the vacuity signal, not a failure:
// it is counted by its absence from `covers_satisfied`.
(true, Status::Unreached) => {}
(true, Status::Undetermined | Status::Failed) => p.undetermined += 1,
(false, Status::Good) => p.assertions_held += 1,
(false, Status::Failed) => p.assertions_failed += 1,
// An unreachable *assertion* is dead code under the harness's
// assumptions, not a decision about the statement.
(false, Status::Unreached) => {}
(false, Status::Undetermined) => p.undetermined += 1,
}
continue;
}
if let Some(v) = t.strip_prefix("VERIFICATION:- ") {
p.verdict = Some(v.trim() == "SUCCESSFUL");
}
}
p
}
/// Run one proof harness in `dir` under a wall-clock budget, and parse what
/// the prover decided.
///
/// The budget is not a convenience. A solver asked a question it cannot
/// settle does not report that — it keeps going, and an unbounded producer
/// stops being a gate and becomes a hang. Exceeding the budget leaves no
/// verdict line, so the run reads as inconclusive, which is the honest
/// answer: nothing was established, within this budget, about this statement.
///
/// Output is drained by a thread per stream rather than written to a file. A
/// prover emits a great deal on its way to a verdict, so a pipe nobody reads
/// fills and blocks the child — which looks exactly like the hang the budget
/// exists to prevent. A temporary file would do as well until the host it
/// runs on has no space for one, and then it would fail in a way that reads
/// like the prover declining to answer.
pub fn prove(
dir: &std::path::Path,
package: &str,
harness: &str,
extra: &[String],
budget: Duration,
) -> Result<Proof, ProveError> {
let started = Instant::now();
let spawned = |source| ProveError::Spawn {
dir: dir.to_path_buf(),
source,
};
let mut child = Command::new("cargo")
.current_dir(dir)
.arg("kani")
.args(["-p", package, "--harness", harness])
.args(extra)
.stdout(std::process::Stdio::piped())
.stderr(std::process::Stdio::piped())
// Its own group, so the budget can reach the solver. The prover is a
// driver that spawns the checker, and killing only the driver leaves
// the expensive process running — observed, not hypothesized.
.process_group(0)
.spawn()
.map_err(spawned)?;
let drain = |stream: Option<Box<dyn std::io::Read + Send>>| {
std::thread::spawn(move || {
let mut buf = String::new();
if let Some(mut s) = stream {
let _ = s.read_to_string(&mut buf);
}
buf
})
};
let out = drain(child.stdout.take().map(|s| Box::new(s) as Box<dyn std::io::Read + Send>));
let err = drain(child.stderr.take().map(|s| Box::new(s) as Box<dyn std::io::Read + Send>));
let mut over_budget = false;
loop {
if child.try_wait().map_err(spawned)?.is_some() {
break;
}
if started.elapsed() > budget {
let _ = Command::new("kill")
.arg("-9")
.arg(format!("-{}", child.id()))
.status();
let _ = child.wait();
over_budget = true;
break;
}
std::thread::sleep(Duration::from_millis(250));
}
let mut text = out.join().unwrap_or_default();
text.push_str(&err.join().unwrap_or_default());
let mut p = parse(&text);
p.seconds = started.elapsed().as_secs_f64();
if over_budget {
// A killed run can leave a property table that looks healthy as far
// as it got. Clearing the verdict is what makes `is_inconclusive`
// true, and the budget is the reason there is no verdict to report.
p.verdict = None;
}
Ok(p)
}
/// Whether a model checker is available to run at all.
#[must_use]
pub fn available(dir: &std::path::Path) -> bool {
Command::new("cargo")
.current_dir(dir)
.args(["kani", "--version"])
.output()
.is_ok_and(|o| o.status.success())
}
#[cfg(test)]
mod tests {
use super::*;
/// A harness that examined its domain and held.
const HELD: &str = "\
RESULTS:
Check 1: ppm.assertion.1
- Status: SUCCESS
- Description: \"a share of a whole cannot exceed the whole\"
Check 2: ppm.cover.1
- Status: SATISFIED
- Description: \"cover condition: the whole-scale case\"
- Location: src/proofs.rs:40:5
Check 3: ppm.cover.2
- Status: SATISFIED
- Description: \"cover condition: the none-of-it case\"
- Location: src/proofs.rs:41:5
SUMMARY:
** 0 of 3 failed
** 2 of 2 cover properties satisfied
VERIFICATION:- SUCCESSFUL
";
#[test]
fn a_harness_that_examined_its_domain_and_held_is_usable() {
let p = parse(HELD);
assert_eq!(p.covers, 2);
assert_eq!(p.covers_satisfied, 2);
assert_eq!(p.assertions_held, 1);
assert!(p.demonstrates_proof());
assert!(!p.demonstrates_refutation());
assert!(!p.is_inconclusive());
assert!(!p.declares_no_cover());
}
/// The trap this module exists for: the verdict line says success while a
/// declared cover was never reached, so the statement holds over a domain
/// the harness's own assumptions emptied.
#[test]
fn a_successful_verdict_with_an_unreachable_cover_proves_nothing() {
let log = HELD.replace(
"Check 3: ppm.cover.2\n - Status: SATISFIED",
"Check 3: ppm.cover.2\n - Status: UNREACHABLE",
);
let p = parse(&log);
assert_eq!(p.verdict, Some(true), "the prover still reports success");
assert_eq!(p.covers, 2);
assert_eq!(p.covers_satisfied, 1);
assert_eq!(p.covers_unreached(), 1);
assert!(
!p.demonstrates_proof(),
"a vacuous harness must not be usable as evidence"
);
}
/// An unsatisfiable cover is the same failure wearing a different word.
#[test]
fn an_unsatisfiable_cover_is_treated_as_unreached() {
let log = HELD.replace("- Status: SATISFIED", "- Status: UNSATISFIABLE");
let p = parse(&log);
assert_eq!(p.covers_satisfied, 0);
assert!(!p.demonstrates_proof());
}
#[test]
fn a_violated_assertion_is_the_refutation_a_counter_artifact_seeks() {
let log = HELD
.replace("- Status: SUCCESS", "- Status: FAILURE")
.replace("VERIFICATION:- SUCCESSFUL", "VERIFICATION:- FAILED");
let p = parse(&log);
assert_eq!(p.assertions_failed, 1);
assert!(p.demonstrates_refutation());
assert!(!p.demonstrates_proof());
}
/// Not every refutation arrives as an assertion. A counter-artifact that
/// narrows an integer type is refuted by an overflow check, which is a
/// different property class — and a parser that matched only `assertion`
/// would read this table as clean.
#[test]
fn a_refutation_in_another_property_class_is_still_a_refutation() {
let log = "\
RESULTS:
Check 1: ppm.arithmetic_overflow.1
- Status: FAILURE
- Description: \"attempt to multiply with overflow\"
Check 2: ppm.cover.1
- Status: SATISFIED
- Description: \"cover condition: the whole-scale case\"
VERIFICATION:- FAILED
";
let p = parse(log);
assert_eq!(p.assertions_failed, 1, "the overflow check must be counted");
assert!(p.demonstrates_refutation());
assert!(!p.demonstrates_proof());
}
/// The costliest confusion available: a prover that ran out of resources
/// has established nothing, and crediting it as a refutation would hand
/// out the top rung for a timeout.
#[test]
fn an_undecided_property_is_neither_a_proof_nor_a_refutation() {
let log = HELD.replace("- Status: SUCCESS", "- Status: UNDETERMINED");
let p = parse(&log);
assert_eq!(p.undetermined, 1);
assert!(p.is_inconclusive());
assert!(!p.demonstrates_proof());
assert!(
!p.demonstrates_refutation(),
"an undecided property is not a refutation"
);
}
/// A prover killed mid-run leaves a property table with no verdict. The
/// table may look entirely healthy, which is why the verdict is required
/// rather than inferred from the checks that did print.
#[test]
fn a_run_with_no_verdict_line_is_inconclusive() {
let truncated = HELD.split("SUMMARY:").next().unwrap();
let p = parse(truncated);
assert_eq!(p.verdict, None);
assert_eq!(p.covers_satisfied, 2, "the table itself looks healthy");
assert!(p.is_inconclusive());
assert!(!p.demonstrates_proof());
assert!(!p.demonstrates_refutation());
}
#[test]
fn a_harness_declaring_no_cover_is_caught_before_it_is_graded() {
let log = "\
RESULTS:
Check 1: ppm.assertion.1
- Status: SUCCESS
- Description: \"holds\"
VERIFICATION:- SUCCESSFUL
";
let p = parse(log);
assert!(p.declares_no_cover());
assert!(!p.demonstrates_proof());
}
/// A status this parser does not know is a property it cannot vouch for.
#[test]
fn an_unrecognized_status_is_read_conservatively() {
let log = HELD.replace("- Status: SUCCESS", "- Status: SOMETHING_NEW");
let p = parse(&log);
assert_eq!(p.undetermined, 1);
assert!(p.is_inconclusive());
assert!(!p.demonstrates_proof());
}
}

418
joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs
View file

@ -7,7 +7,24 @@
//! address moves, so every witness bound to the old wording stops applying,
//! automatically (SPEC §4.2).
//!
//! The format recognised is a numbered list of bolded, labelled items under a
//! ## The shape is declared, not assumed
//!
//! A producer that could only read documents written like this family's own
//! specifications would be a tool for one organisation. Requirements live in
//! several conventional shapes — numbered conformance lists, bulleted
//! requirement tables, a heading per requirement carrying its identifier —
//! and which one a document uses is a fact about the document, so the
//! manifest declares it (see [`Shape`]). Nothing else about the extraction
//! varies: the section is still named, the floor still fails closed, and
//! continuation lines still join the same way.
//!
//! Changing the declared shape changes which text is captured, and therefore
//! moves every obligation address. That is correct rather than unfortunate —
//! a different extraction really does describe different obligations — but it
//! means the shape is part of what an auditor needs in order to recompute the
//! addresses, alongside the document itself.
//!
//! The default shape is a numbered list of bolded, labelled items under a
//! named section, which is how this family's specifications write their
//! conformance lists:
//!
@ -32,11 +49,24 @@ pub enum SpecDocError {
/// The named section is not in the document.
#[error("the document has no section headed {0:?}")]
NoSection(String),
/// The section is there and holds no recognisable items. Fail closed: a
/// parser that returns an empty clause list would make every obligation
/// vacuously satisfied.
#[error("section {0:?} contains no numbered `**Cn — Name.** text` items")]
NoItems(String),
/// The section is there and holds no items of the declared shape. Fail
/// closed: a parser that returns an empty clause list would make every
/// obligation vacuously satisfied.
#[error("section {section:?} contains no items of shape {shape:?}")]
NoItems {
/// The section searched.
section: String,
/// The shape that matched nothing.
shape: &'static str,
},
/// The declared shape is not one this producer implements.
#[error("unknown clause shape {got:?}; expected one of {known}")]
UnknownShape {
/// The shape as declared.
got: String,
/// The shapes available.
known: String,
},
/// Fewer items than the caller said to expect.
#[error("expected at least {expected} items in section {section:?}, found {found}")]
TooFew {
@ -63,6 +93,67 @@ pub struct Item {
pub text: String,
}
/// Which conventional shape a document writes its requirements in.
///
/// Three, because three are what documents actually use. Each one names how
/// an item *opens*; how a label, a name and a body are then separated is
/// shared, so a document is read by declaring its list style rather than by
/// describing its punctuation.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
pub enum Shape {
/// `1. **C1 — Addressing.** text` — a numbered conformance list. The
/// default, and what this family's own specifications use.
#[default]
NumberedBold,
/// `- **FR-1 — Addressing.** text` — the same item in a bulleted list,
/// which is how requirements more often appear outside a formal spec.
BulletedBold,
/// `### REQ-7 — Addressing` followed by prose — one heading per
/// requirement, carrying its identifier. Common wherever requirements are
/// kept as documentation rather than as a list.
Heading,
}
impl Shape {
/// The shapes this producer implements, for an error message.
pub const KNOWN: &'static str =
"numbered-bold-label, bulleted-bold-label, heading-label";
/// Read a declared shape.
pub fn parse(name: &str) -> Result<Self, SpecDocError> {
match name {
"numbered-bold-label" => Ok(Self::NumberedBold),
"bulleted-bold-label" => Ok(Self::BulletedBold),
"heading-label" => Ok(Self::Heading),
other => Err(SpecDocError::UnknownShape {
got: other.to_string(),
known: Self::KNOWN.to_string(),
}),
}
}
/// The name this shape is declared by.
#[must_use]
pub const fn label(self) -> &'static str {
match self {
Self::NumberedBold => "numbered-bold-label",
Self::BulletedBold => "bulleted-bold-label",
Self::Heading => "heading-label",
}
}
}
/// How deep a markdown heading is, or `None` if the line is not one.
fn heading_depth(line: &str) -> Option<usize> {
let t = line.trim_start();
if !t.starts_with('#') {
return None;
}
let depth = t.chars().take_while(|c| *c == '#').count();
// `#hashtag` is not a heading; a heading has whitespace after its hashes.
t[depth..].starts_with(char::is_whitespace).then_some(depth)
}
fn is_section_heading(line: &str, section: &str) -> bool {
let t = line.trim_start();
if !t.starts_with('#') {
@ -87,20 +178,102 @@ fn split_item(body: &str) -> Option<(String, String, String)> {
Some((label.trim().to_string(), name.to_string(), tail.trim().to_string()))
}
/// Parse the numbered items of one section.
/// Split a heading's text into `label`, `name` on either an em dash or a
/// colon, which are the two ways an identifier is conventionally separated
/// from its title.
fn split_heading(body: &str) -> Option<(String, String)> {
let (label, name) = body
.split_once(" — ")
.or_else(|| body.split_once(": "))
.or_else(|| body.split_once(" - "))?;
let label = label.trim();
let name = name.trim().trim_end_matches('.');
(!label.is_empty() && !name.is_empty())
.then(|| (label.to_string(), name.to_string()))
}
/// What one line is, under a given shape.
enum Line<'a> {
/// This line ends the section.
SectionEnd,
/// This line opens an item.
Opens(String, String, String),
/// This line continues the open item, or closes it if blank.
Body(&'a str),
}
/// Classify one line. The shape decides only what *opens* an item and what
/// *ends* the section; everything else is body.
fn classify<'a>(line: &'a str, shape: Shape, section_depth: usize) -> Line<'a> {
let trimmed = line.trim_start();
let depth = heading_depth(line);
match shape {
// For list shapes any heading ends the section, which is the rule
// this parser has always applied.
Shape::NumberedBold | Shape::BulletedBold => {
if depth.is_some() {
return Line::SectionEnd;
}
let body = match shape {
Shape::NumberedBold => trimmed
.split_once(". ")
.filter(|(n, _)| !n.is_empty() && n.chars().all(|c| c.is_ascii_digit()))
.map(|(_, b)| b),
// A bullet marker, not a line that merely begins with a dash:
// `- ` and `* ` both open a list item in markdown.
_ => trimmed
.strip_prefix("- ")
.or_else(|| trimmed.strip_prefix("* ")),
};
match body.and_then(split_item) {
Some((label, name, text)) => Line::Opens(label, name, text),
// A list item that does not carry a label is body: it may be
// a sub-list under the open item.
None => Line::Body(line),
}
}
// Here the items *are* headings, so the section ends only at a
// heading no deeper than the section's own.
Shape::Heading => match depth {
Some(d) if d <= section_depth => Line::SectionEnd,
Some(_) => {
let body = trimmed.trim_start_matches('#').trim();
match split_heading(body) {
Some((label, name)) => Line::Opens(label, name, String::new()),
// A heading with no identifier is a grouping heading, not
// a requirement. Treating it as one would invent an
// obligation nobody wrote.
None => Line::Body(line),
}
}
None => Line::Body(line),
},
}
}
/// Parse the items of one section, in the document's declared shape.
///
/// `expect_at_least` is a floor the caller states: a parser that silently
/// matched nothing would report success having checked nothing, which is the
/// failure mode this whole standard exists to make visible.
///
/// 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.
pub fn items(
document: &str,
section: &str,
expect_at_least: usize,
shape: Shape,
) -> Result<Vec<Item>, SpecDocError> {
let mut lines = document.lines();
let mut section_depth = 0usize;
let mut found_section = false;
for line in lines.by_ref() {
if is_section_heading(line, section) {
section_depth = heading_depth(line).unwrap_or(0);
found_section = true;
break;
}
@ -112,46 +285,49 @@ pub fn items(
let mut out: Vec<Item> = Vec::new();
let mut pending: Option<Item> = None;
for line in lines {
// The next heading of any level ends the section.
if line.trim_start().starts_with('#') {
break;
}
let trimmed = line.trim_start();
let numbered = trimmed
.split_once(". ")
.filter(|(n, _)| !n.is_empty() && n.chars().all(|c| c.is_ascii_digit()));
match numbered {
Some((_, body)) => {
match classify(line, shape, section_depth) {
Line::SectionEnd => break,
Line::Opens(label, name, text) => {
if let Some(item) = pending.take() {
out.push(item);
}
if let Some((label, name, text)) = split_item(body) {
pending = Some(Item { label, name, text });
}
pending = Some(Item { label, name, text });
}
None if pending.is_some() => {
let continuation = line.trim();
Line::Body(raw) => {
if pending.is_none() {
continue;
}
let continuation = raw.trim();
if continuation.is_empty() {
if let Some(item) = pending.take() {
// A blank line closes a list item. Under `heading-label`
// a requirement's prose runs over paragraphs, so it does
// not: the next heading closes it instead.
if shape != Shape::Heading && let Some(item) = pending.take() {
out.push(item);
}
} else if let Some(item) = pending.as_mut() {
// Re-wrapping must not change the obligation, so
// continuation lines join with exactly one space.
item.text.push(' ');
if !item.text.is_empty() {
item.text.push(' ');
}
item.text.push_str(continuation);
}
}
None => {}
}
}
if let Some(item) = pending {
out.push(item);
}
// A heading with no prose under it states no requirement; keeping it
// would address the empty string and grade an obligation nobody wrote.
out.retain(|i| !i.text.is_empty());
if out.is_empty() {
return Err(SpecDocError::NoItems(section.to_string()));
return Err(SpecDocError::NoItems {
section: section.to_string(),
shape: shape.label(),
});
}
if out.len() < expect_at_least {
return Err(SpecDocError::TooFew {
@ -189,7 +365,7 @@ pub fn clauses(items: &[Item]) -> Vec<Clause> {
mod tests {
use super::*;
const DOC: &str = "\
pub(super) const DOC: &str = "\
# A Standard
## 6. Something else
@ -215,7 +391,7 @@ The reference implementation is conformant by construction.
#[test]
fn items_are_read_from_the_named_section_only() {
let got = items(DOC, "7. Conformance", 3).expect("parses");
let got = items(DOC, "7. Conformance", 3, Shape::default()).expect("parses");
assert_eq!(got.len(), 3, "{got:#?}");
assert_eq!(got[0].label, "C1");
assert_eq!(got[0].name, "Addressing");
@ -224,7 +400,7 @@ The reference implementation is conformant by construction.
#[test]
fn continuation_lines_join_with_one_space() {
let got = items(DOC, "7. Conformance", 3).unwrap();
let got = items(DOC, "7. Conformance", 3, Shape::default()).unwrap();
assert_eq!(
got[0].text,
"Obligation addresses are computed over `{kind, text}` with the label excluded; \
@ -241,9 +417,9 @@ The reference implementation is conformant by construction.
);
let reworded = DOC.replace("relabelling preserves an address", "relabelling may preserve an address");
let base = clauses(&items(DOC, "7. Conformance", 3).unwrap());
let wrapped = clauses(&items(&rewrapped, "7. Conformance", 3).unwrap());
let changed = clauses(&items(&reworded, "7. Conformance", 3).unwrap());
let base = clauses(&items(DOC, "7. Conformance", 3, Shape::default()).unwrap());
let wrapped = clauses(&items(&rewrapped, "7. Conformance", 3, Shape::default()).unwrap());
let changed = clauses(&items(&reworded, "7. Conformance", 3, Shape::default()).unwrap());
assert_eq!(
base[0].obligation().unwrap(),
@ -259,13 +435,13 @@ The reference implementation is conformant by construction.
#[test]
fn a_missing_section_is_an_error_not_an_empty_list() {
assert!(matches!(items(DOC, "99. Nowhere", 1), Err(SpecDocError::NoSection(_))));
assert!(matches!(items(DOC, "99. Nowhere", 1, Shape::default()), Err(SpecDocError::NoSection(_))));
}
#[test]
fn a_section_with_no_items_is_an_error() {
let doc = "## 7. Conformance\n\nProse only, no list.\n";
assert!(matches!(items(doc, "7. Conformance", 1), Err(SpecDocError::NoItems(_))));
assert!(matches!(items(doc, "7. Conformance", 1, Shape::default()), Err(SpecDocError::NoItems { .. })));
}
#[test]
@ -273,19 +449,185 @@ The reference implementation is conformant by construction.
// The guard that matters: a parser that quietly matched two of eleven
// items would report every unmatched obligation as unevidenced, or --
// worse, with a narrower specification, as fully covered.
let err = items(DOC, "7. Conformance", 11).unwrap_err();
let err = items(DOC, "7. Conformance", 11, Shape::default()).unwrap_err();
assert!(matches!(err, SpecDocError::TooFew { found: 3, expected: 11, .. }), "{err}");
}
#[test]
fn an_unlabelled_numbered_line_is_not_an_item() {
let doc = "## 7. Conformance\n\n1. **Bolded but unlabelled.** No em dash.\n";
assert!(matches!(items(doc, "7. Conformance", 1), Err(SpecDocError::NoItems(_))));
assert!(matches!(items(doc, "7. Conformance", 1, Shape::default()), Err(SpecDocError::NoItems { .. })));
}
#[test]
fn a_duplicate_label_is_refused() {
let doc = "## 7. C\n\n1. **C1 — A.** One.\n2. **C1 — B.** Two.\n";
assert!(matches!(items(doc, "7. C", 2), Err(SpecDocError::DuplicateLabel(l)) if l == "C1"));
assert!(matches!(items(doc, "7. C", 2, Shape::default()), Err(SpecDocError::DuplicateLabel(l)) if l == "C1"));
}
}
#[cfg(test)]
mod shaped {
use super::*;
/// The shape an existing manifest gets when it declares none. If this
/// ever changes, every obligation address in every deployment moves.
#[test]
fn the_default_shape_is_the_numbered_list() {
assert_eq!(Shape::default(), Shape::NumberedBold);
assert_eq!(Shape::default().label(), "numbered-bold-label");
assert_eq!(Shape::parse("numbered-bold-label").unwrap(), Shape::default());
}
/// The load-bearing regression: generalising the parser must not change
/// what the default shape extracts, because the obligation address is
/// computed from exactly that text. The hex below is the address of a
/// fixture clause, so a change of a single character in how the default
/// shape captures text fails here rather than silently invalidating the
/// evidence of every deployment that upgrades.
#[test]
fn generalising_the_parser_moved_no_obligation_under_the_default_shape() {
use joulespec_core::spec::{Clause, ClauseKind};
let got = items(super::tests::DOC, "7. Conformance", 3, Shape::default()).unwrap();
let clause = Clause::new(
got[0].label.clone(),
ClauseKind::Requirement,
format!("{} — {}", got[0].name, got[0].text),
);
assert_eq!(
clause.obligation().unwrap().as_str(),
// Computed by running this same fixture through the parser as it
// stood before the shape generalisation, not by recording what
// the new one happens to produce.
"b3:71447ade934b77d80fb3816d198c675821b2a99e88b60174190ad35064121060",
"the default shape's extraction changed; every deployment's \
obligation addresses would move"
);
}
const BULLETED: &str = "\
## Requirements
- **FR-1 — Addressing.** Obligation addresses are computed over `{kind, text}`
with the label excluded.
- a sub-point that carries no label, which is body rather than an item
* **FR-2 — Validation.** Duplicate labels are refused.
## Next
";
#[test]
fn a_bulleted_requirement_list_is_read_with_both_markers() {
let got =
items(BULLETED, "Requirements", 2, Shape::BulletedBold).unwrap();
assert_eq!(got.len(), 2, "{got:#?}");
assert_eq!(got[0].label, "FR-1");
assert_eq!(got[1].label, "FR-2", "an asterisk opens a list item too");
assert!(
got[0].text.ends_with("body rather than an item"),
"an unlabelled bullet is body, not an item: {:?}",
got[0].text
);
}
const HEADINGS: &str = "\
# A Requirements Document
## 2. Requirements
Some preamble that belongs to no requirement.
### REQ-1: Addressing
Obligation addresses are computed over the kind and text,
with the label excluded.
A second paragraph of the same requirement.
### Grouping heading with no identifier
### REQ-2 — Validation
Duplicate labels are refused.
### REQ-3: Nothing is stated here
## 3. Afterwards
### REQ-9: A decoy past the section end
Not a requirement of section 2.
";
#[test]
fn a_heading_per_requirement_is_read_with_either_separator() {
let got = items(HEADINGS, "2. Requirements", 2, Shape::Heading).unwrap();
assert_eq!(
got.iter().map(|i| i.label.as_str()).collect::<Vec<_>>(),
["REQ-1", "REQ-2"],
"{got:#?}"
);
assert_eq!(got[0].name, "Addressing", "a colon separates too");
assert_eq!(got[1].name, "Validation", "and so does an em dash");
}
/// Prose under one of these headings runs over paragraphs, so a blank
/// line must not close the item the way it does in a list.
#[test]
fn a_requirement_heading_holds_its_whole_prose() {
let got = items(HEADINGS, "2. Requirements", 2, Shape::Heading).unwrap();
assert!(
got[0].text.contains("second paragraph"),
"a blank line closed the item early: {:?}",
got[0].text
);
assert!(!got[0].text.contains("preamble"), "preamble belongs to nothing");
}
/// A heading that states nothing is not a requirement with empty text —
/// addressing the empty string would create an obligation nobody wrote,
/// and it would be graded like any other.
#[test]
fn a_heading_with_no_prose_states_no_requirement() {
let got = items(HEADINGS, "2. Requirements", 2, Shape::Heading).unwrap();
assert!(
!got.iter().any(|i| i.label == "REQ-3"),
"an empty heading became an obligation: {got:#?}"
);
assert!(
!got.iter().any(|i| i.label == "REQ-9"),
"the section end was not respected: {got:#?}"
);
}
/// A heading no deeper than the section's own ends it. Under the list
/// shapes any heading does, which is the older and stricter rule.
#[test]
fn a_shape_that_matches_nothing_fails_closed() {
// The heading document read as a numbered list finds no items at all.
assert!(matches!(
items(HEADINGS, "2. Requirements", 1, Shape::NumberedBold),
Err(SpecDocError::NoItems { .. })
));
// And the floor still bites when the shape matches too little.
assert!(matches!(
items(HEADINGS, "2. Requirements", 3, Shape::Heading),
Err(SpecDocError::TooFew { found: 2, .. })
));
}
#[test]
fn an_unimplemented_shape_is_refused_by_name() {
assert!(matches!(
Shape::parse("whatever-the-operator-hoped"),
Err(SpecDocError::UnknownShape { .. })
));
}
#[test]
fn a_hashtag_is_not_a_heading() {
assert_eq!(heading_depth("### REQ-1: x"), Some(3));
assert_eq!(heading_depth("#notaheading"), None);
assert_eq!(heading_depth("plain text"), None);
}
}

6
joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml
View file

@ -1,6 +1,6 @@
[package]
name = "joulespec-core"
version = "0.2.0"
version = "0.3.0"
description = "JouleSpec — the reference conformance kernel for energy-accounted specifications (joulespec/1): obligation-addressed clauses, a graded evidence ladder from testimony to proof, deterministic drift, and the joules a specification cost to evidence."
edition.workspace = true
license.workspace = true
@ -15,3 +15,7 @@ thiserror = { workspace = true }
[lints.rust]
missing_docs = "warn"
# The proof harnesses in src/proofs.rs compile only under the model checker,
# which sets this cfg itself. Declaring it here keeps `cargo check` from
# warning about a cfg it has no way to know about.
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)', 'cfg(joulespec_slow_proofs)'] }

57
joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs
View file

@ -298,12 +298,7 @@ impl Conformance {
/// features nobody requested.
#[must_use]
pub fn specified_ppm(&self) -> Option<u64> {
let total = self.specified_uj.checked_add(self.unspecified_uj)?;
if total == 0 {
return None;
}
// u128 so a specified figure near u64::MAX cannot overflow the scale.
Some(((u128::from(self.specified_uj) * 1_000_000) / u128::from(total)) as u64)
ppm(self.specified_uj, self.unspecified_uj)
}
/// Total energy attributed to this specification: the work plus the
@ -356,6 +351,42 @@ impl Conformance {
}
}
/// The §3.2 cap: the minimum over a set of graded figures, absent when any
/// member has no figure at all.
///
/// `None` orders below every `Some`, and that is the whole mechanism: an
/// obligation with no surviving evidence caps the composite rather than being
/// skipped over, so nine proved obligations cannot conceal one nobody looked
/// at. An empty set has nothing to cap and is absent.
///
/// Generic because §3.2 applies the identical rule twice — once to grades and
/// once to attestations — and two copies of a rule are two places for it to
/// drift. Stated as a named function so a prover can be asked about every
/// combination of members, including the ones where absence meets the top
/// rung.
#[must_use]
pub fn cap<T: Ord, I: IntoIterator<Item = Option<T>>>(graded: I) -> Option<T> {
graded.into_iter().min().unwrap_or(None)
}
/// The §5 ratio rule: an integer parts-per-million share of a whole, absent
/// when there is no whole to take a share of.
///
/// Stated as a free function over two plain integers so it can be handed to a
/// prover across its entire input domain rather than sampled at a handful of
/// points. The `u128` widening is load-bearing and not decoration: a `part`
/// anywhere near `u64::MAX` overflows the parts-per-million scale in 64 bits,
/// and the inputs that expose it are far outside the range any hand-written
/// case would think to pick.
#[must_use]
pub fn ppm(part: u64, rest: u64) -> Option<u64> {
let total = part.checked_add(rest)?;
if total == 0 {
return None;
}
Some(((u128::from(part) * 1_000_000) / u128::from(total)) as u64)
}
/// Evaluate a specification at one artifact state.
///
/// Every witness is verified here; none is taken on trust and none is
@ -506,12 +537,7 @@ pub fn evaluate(
}
flags.sort();
let grade = verdicts
.iter()
.filter(|c| c.kind.is_owed())
.map(|c| c.grade)
.min()
.unwrap_or(None);
let grade = cap(verdicts.iter().filter(|c| c.kind.is_owed()).map(|c| c.grade));
let mut specified_uj = 0u64;
let mut unspecified_uj = 0u64;
@ -534,12 +560,7 @@ pub fn evaluate(
let provenance =
worst_provenance(evidence_provenances.into_iter().chain(work_provenances));
let attestation = verdicts
.iter()
.filter(|c| c.kind.is_owed())
.map(|c| c.attestation)
.min()
.unwrap_or(None);
let attestation = cap(verdicts.iter().filter(|c| c.kind.is_owed()).map(|c| c.attestation));
Ok(Conformance {
spec_id,

3
joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs
View file

@ -77,6 +77,9 @@ pub mod conform;
pub mod drift;
pub mod evidence;
pub mod jcr1;
#[cfg(kani)]
mod proofs;
pub mod receipt;
pub mod spec;

190
joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs Normal file
View file

@ -0,0 +1,190 @@
//! Machine-checked statements about this implementation, for the `E4` rung.
//!
//! These are not tests. A test samples the input domain; a proof here is
//! discharged over the whole of it, which is the only thing `E4` claims over
//! `E3`. They compile only under the model checker (`cfg(kani)`), so an
//! ordinary `cargo test` neither runs nor type-checks them — see
//! `conformance/v1/README.md` for how the harvest reaches them.
//!
//! Every harness carries at least one reachability cover. A model checker
//! reports success for a harness whose assumptions have eliminated the states
//! the property was about, so success alone is not evidence that anything was
//! checked: it is the same shape of silence as a test binary that runs zero
//! tests and exits zero. The covers are what distinguish the two, and the
//! producer refuses a harness that declares none.
use crate::conform::{cap, ppm};
use crate::evidence::Grade;
/// **C7 — Cost.** The ratio rule is arithmetically total: for no pair of
/// inputs does it overflow or divide by zero.
///
/// This is what the `u128` widening in [`ppm`] exists for, and it is the half
/// of C7 that sampling cannot reach. The inputs that break it are a `part`
/// above roughly `u64::MAX / 1_000_000`, which no hand-written case picks and
/// no realistic fixture contains — so a suite can pass indefinitely over an
/// implementation that computes the scale in 64 bits and overflows.
///
/// The statement is discharged by the checker's own arithmetic checks rather
/// than by an assertion written here. That is the precise claim: not that the
/// quotient has some value, but that every operation on the way to it is
/// defined for every input. The covers below are what make the claim mean
/// something, by showing each branch is reached.
///
/// The companion statement — that the quotient is bounded by the scale — is
/// deliberately *not* made here. It requires the solver to reason about the
/// output bits of a 128-bit division, and it did not converge; see
/// `conformance/v1/README.md`. Leaving it unstated is the honest shape, since
/// a harness that quietly narrowed its domain to converge would report the
/// same success over a smaller claim.
#[kani::proof]
fn the_ratio_rule_is_total_over_every_input() {
let part: u64 = kani::any();
let rest: u64 = kani::any();
let share = ppm(part, rest);
// Each cover names a branch the statement is about. Without them, a
// harness whose assumptions had emptied the domain would report the same
// success as this one.
kani::cover!(share.is_none(), "no whole to take a share of");
kani::cover!(share.is_some(), "a whole exists and a share was computed");
kani::cover!(
part.checked_add(rest).is_none(),
"the whole itself overflows, which is the absent case"
);
kani::cover!(
part > u64::MAX / 1_000_000 && share.is_some(),
"a part large enough to overflow the scale in 64 bits"
);
}
/// **C7 — Cost.** The quotient itself is bounded by the scale, is the full
/// scale exactly when nothing is left over, and is none of it when there is no
/// part.
///
/// **This harness does not converge, and is kept as the record of that.** It
/// is behind a `cfg` nobody sets, so an ordinary run of this package does not
/// hang on it; reproduce with
/// `RUSTFLAGS='--cfg joulespec_slow_proofs' cargo kani -p joulespec-core
/// --harness a_share_never_exceeds_the_scale_it_is_measured_on`.
///
/// Measured twice, on one host, over the same input domain:
///
/// | Method | Outcome |
/// |---|---|
/// | bit-blasting to SAT (the default engine) | no per-property progress in 24 minutes |
/// | an SMT bitvector theory | 4 of ~51 conditions in about 8 seconds, then over 50 minutes on the 5th |
///
/// The second is the interesting one. Naming a solver that reasons about the
/// operation rather than its output bits moved the wall — it settles most of
/// the conditions almost at once — but it did not remove it: one condition
/// about a wide division's quotient remains out of reach. So the cost of a
/// statement is not simply a property of the engine, and an operator cannot
/// expect to buy convergence by changing solver. [`the_ratio_rule_is_total_over_every_input`]
/// states the part of C7 that *is* reachable, which is also the part a
/// counter-artifact refutes.
#[cfg(joulespec_slow_proofs)]
#[kani::proof]
#[kani::solver(z3)]
fn a_share_never_exceeds_the_scale_it_is_measured_on() {
let part: u64 = kani::any();
let rest: u64 = kani::any();
if let Some(share) = ppm(part, rest) {
assert!(share <= 1_000_000, "a share cannot exceed the whole scale");
assert!(
rest > 0 || share == 1_000_000,
"with nothing left over the share is the whole scale"
);
assert!(
part > 0 || share == 0,
"with no part the share is none of the scale"
);
}
kani::cover!(ppm(part, rest) == Some(1_000_000), "the whole-scale case");
kani::cover!(ppm(part, rest) == Some(0), "the none-of-it case");
kani::cover!(
matches!(ppm(part, rest), Some(s) if s > 0 && s < 1_000_000),
"an interior share"
);
}
/// A symbolic grade, over the whole of the ladder.
fn any_grade() -> Grade {
match kani::any::<u8>() % 5 {
0 => Grade::Cited,
1 => Grade::Reviewed,
2 => Grade::Exercised,
3 => Grade::Falsifiable,
_ => Grade::Proved,
}
}
/// **C5 — Evaluation.** The cap is a minimum, and widening a set can only
/// lower it.
///
/// §3.2 states this as the reason a grade is not gameable by adding clauses,
/// and it is the one property an adversary has a direct incentive to break.
/// A test samples it; this settles it over every combination of grades a set
/// of this size can hold, including the ones where an absent grade meets a
/// proved one.
///
/// The statement is about [`cap`] itself — the function the evaluator calls —
/// and not about a restatement of the rule inside the harness. A proof of a
/// property of its own local copy of the logic would establish nothing about
/// the artifact, and no counter-artifact to the artifact could refute it.
///
/// The bound on set size is part of the statement rather than a concession
/// hidden in the harness: the minimum is determined by one member and the
/// ordering of the rest, so a set of four exhibits every arrangement the rule
/// can meet.
#[kani::proof]
fn widening_a_set_can_only_lower_its_cap() {
let held: [Option<Grade>; 4] = [
if kani::any() { Some(any_grade()) } else { None },
if kani::any() { Some(any_grade()) } else { None },
if kani::any() { Some(any_grade()) } else { None },
if kani::any() { Some(any_grade()) } else { None },
];
let extra: Option<Grade> = if kani::any() { Some(any_grade()) } else { None };
let before = cap(held);
let widened = [held[0], held[1], held[2], held[3], extra];
let after = cap(widened);
match (before, after) {
(Some(b), Some(a)) => {
assert!(a <= b, "widening a set cannot raise its cap");
assert!(
held.contains(&Some(b)),
"a cap is one of the figures that fed it, not a value of its own"
);
}
(None, a) => assert!(
a.is_none(),
"a set with an unevidenced member cannot become evidenced by growing"
),
// Widening with an unevidenced member empties the cap. That is the
// rule working, and it is the direction §3.2 relies on.
(Some(_), None) => assert!(
extra.is_none(),
"the cap can only empty because the added member was unevidenced"
),
}
kani::cover!(
matches!((before, after), (Some(b), Some(a)) if a < b),
"the added member strictly lowers the cap"
);
kani::cover!(
matches!((before, after), (Some(b), Some(a)) if a == b),
"the added member leaves the cap alone"
);
kani::cover!(
matches!((before, after), (Some(_), None)),
"the added member is unevidenced and empties the cap"
);
kani::cover!(before.is_none(), "the set was already unevidenced");
}

736
joulespec/joulespec-rs/crates/joulespec-core/tests/evaluation.rs Normal file
View file

@ -0,0 +1,736 @@
//! The published **evaluation** corpus: cases an over-grading implementation
//! passes incorrectly.
//!
//! The wire vectors in `tests/vectors.rs` 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. This corpus is the
//! other half: each case is a complete set of evaluation inputs plus the
//! verdict §3 requires, chosen so that a plausible but wrong evaluator
//! disagrees.
//!
//! Every case names the **trap** it sets and the **direction** of the error
//! it catches. Most are over-grading: an implementation that reports
//! conformance never established, which is the failure this standard exists
//! to stop. At least one is under-grading, because a rule that refuses
//! everything is also wrong and an implementation can satisfy every
//! over-grading case by grading nothing at all.
//!
//! ## Where the expected verdicts come from
//!
//! They are written by hand from §3 of the specification, and they are
//! **not** regenerated from this implementation's output — a corpus whose
//! expectations are whatever the code produced would certify agreement with
//! itself. Setting `JOULESPEC_GEN_EVALUATION=1` republishes the input files
//! and the expectations as this test states them; it never reads a verdict
//! back out of the evaluator to decide what to expect.
//!
//! ## How another implementation uses it
//!
//! Each case directory holds `spec.json`, `state.json`, `witnesses.json`,
//! `work.json` and `expect.json`. Read the first four, evaluate, and compare
//! against the fifth.
use std::path::{Path, PathBuf};
use ed25519_dalek::SigningKey;
use joulespec_core::conform::{self, ArtifactState, Conformance, Work};
use joulespec_core::evidence::{
Anchor, Attestation, Evidence, Formalization, Grade, Grounding, SignedWitness, Vacuity,
Witness,
};
use joulespec_core::spec::{Clause, SignedSpec, Spec};
use joulespec_core::{Address, Energy, Provenance};
use serde::{Deserialize, Serialize};
fn key(seed: u8) -> SigningKey {
SigningKey::from_bytes(&[seed; 32])
}
fn dir() -> PathBuf {
Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../conformance/v1/evaluation")
}
/// What a conforming evaluator must report for one case.
///
/// Deliberately small: the fields an over-generous implementation gets wrong.
/// Energy is omitted because these cases are about grading, and a corpus that
/// pinned microjoules would stop being reproducible for the reasons the
/// self-conformance record is not.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
struct Expect {
/// What the case is for, in one line.
intent: String,
/// What a wrong implementation does here instead.
trap: String,
/// `over-grading` or `under-grading`: which way the wrong answer errs.
direction: String,
/// The specification's grade, absent where §3.2 requires absence.
grade: Option<Grade>,
/// The specification's attestation, on the second axis.
attestation: Option<Attestation>,
/// Flag kinds raised, by variant name, sorted.
flags: Vec<String>,
/// Per clause, in specification order.
clauses: Vec<ExpectClause>,
/// Whether the case conforms at `E3` and `A0`.
conformant_at_e3: bool,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
struct ExpectClause {
label: String,
grade: Option<Grade>,
/// How many of its witnesses were set aside as bound to another state.
stale: usize,
}
fn flag_kind(f: &conform::Flag) -> String {
match f {
conform::Flag::NonGoalWitnessed { .. } => "NonGoalWitnessed",
conform::Flag::Unbound { .. } => "Unbound",
conform::Flag::ForeignSpec { .. } => "ForeignSpec",
conform::Flag::Unverifiable { .. } => "Unverifiable",
}
.to_string()
}
fn observed(c: &Conformance, like: &Expect) -> Expect {
let mut flags: Vec<String> = c.flags.iter().map(flag_kind).collect();
flags.sort();
Expect {
intent: like.intent.clone(),
trap: like.trap.clone(),
direction: like.direction.clone(),
grade: c.grade,
attestation: c.attestation,
flags,
clauses: c
.clauses
.iter()
.map(|v| ExpectClause {
label: v.label.clone(),
grade: v.grade,
stale: v.stale.len(),
})
.collect(),
conformant_at_e3: c.is_conformant(Grade::Falsifiable, Attestation::SelfAttested),
}
}
// ── case construction ────────────────────────────────────────────────────
fn state() -> ArtifactState {
ArtifactState::new(
Address::of_bytes(b"eval-tree-v1"),
[
Address::of_bytes(b"eval-part-a"),
Address::of_bytes(b"eval-part-b"),
],
)
}
fn spec_of(clauses: Vec<Clause>) -> SignedSpec {
let author = key(1);
Spec::new(
"A corpus case: the clauses exist to be graded, not to be implemented.",
clauses,
author.verifying_key().to_bytes(),
)
.sign(&author)
.expect("signs")
}
fn obligation(spec: &SignedSpec, label: &str) -> joulespec_core::spec::Obligation {
spec.spec
.clauses
.iter()
.find(|c| c.label == label)
.expect("label is in the specification")
.obligation()
.expect("addresses")
}
/// A witness carrying `evidence` for `label`, at `at` (the current state
/// unless a case is about staleness), signed by `signer`.
fn witness(
spec: &SignedSpec,
label: &str,
evidence: Evidence,
signer: &SigningKey,
at: Address,
) -> SignedWitness {
Witness::new(
spec.spec.spec_id().unwrap(),
obligation(spec, label),
at,
evidence,
Energy::new(1_000, Provenance::Estimator),
signer.verifying_key().to_bytes(),
)
.sign(signer)
.expect("signs")
}
/// One unit of work by `author`, citing `label`.
///
/// Every case declares work, because the attestation axis is computed from
/// **work** authorship: with no implementer known, §2.8 makes attestation
/// absent, and a corpus of cases that all declared none would exercise one
/// axis and certify two.
fn work_by(spec: &SignedSpec, label: &str, author: &SigningKey) -> Vec<Work> {
vec![Work::new(
Address::of_bytes(b"eval-work"),
vec![obligation(spec, label)],
Energy::new(500_000, Provenance::Estimator),
author.verifying_key().to_bytes(),
)]
}
fn falsifiable(anchor: Anchor) -> Evidence {
Evidence::Falsifiable {
check: "a_named_check".into(),
anchor,
counter: Address::of_bytes(b"eval-counter"),
}
}
fn proved(grounding: Grounding, vacuity: Vacuity) -> Evidence {
Evidence::Proved {
goal: Address::of_bytes(b"eval-goal"),
tier: "corpus".into(),
formalization: Formalization { statement: "forall x. p(x)".into(), grounding },
vacuity,
}
}
struct Case {
name: &'static str,
spec: SignedSpec,
state: ArtifactState,
witnesses: Vec<SignedWitness>,
work: Vec<Work>,
expect: Expect,
}
#[allow(clippy::too_many_lines)]
fn cases() -> Vec<Case> {
let auditor = key(2);
let implementer = key(4);
let crosschecker = key(3);
let mut out = Vec::new();
// 1 ── The minimum, not the mean.
{
let spec = spec_of(vec![
Clause::requirement("C1", "The first obligation is well evidenced."),
Clause::requirement("C2", "The second obligation is only claimed."),
]);
let ws = vec![
witness(&spec, "C1", falsifiable(Anchor::Specification), &auditor, state().address),
witness(&spec, "C2", Evidence::Cited, &implementer, state().address),
];
out.push(Case {
name: "01-a-mean-conceals-the-weakest-obligation",
expect: Expect {
intent: "One obligation at E3, one at E0.".into(),
trap: "Averaging the rungs, or reporting the best, gives E3 or E1 \
where §3.2 requires the minimum."
.into(),
direction: "over-grading".into(),
grade: Some(Grade::Cited),
attestation: Some(Attestation::SelfAttested),
flags: vec![],
clauses: vec![
ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
ExpectClause { label: "C2".into(), grade: Some(Grade::Cited), stale: 0 },
],
conformant_at_e3: false,
},
work: work_by(&spec, "C1", &implementer),
spec,
state: state(),
witnesses: ws,
});
}
// 2 ── An obligation nobody looked at empties the grade.
{
let spec = spec_of(vec![
Clause::requirement("C1", "The first obligation is well evidenced."),
Clause::requirement("C2", "The second obligation has no evidence at all."),
]);
let ws = vec![witness(
&spec,
"C1",
falsifiable(Anchor::Specification),
&auditor,
state().address,
)];
out.push(Case {
name: "02-an-unevidenced-obligation-empties-the-grade",
expect: Expect {
intent: "One obligation at E3; the other has no witness.".into(),
trap: "Skipping the unevidenced clause and grading the rest gives E3. \
Absence orders below every rung, so the grade is absent — not E0, \
which would claim a citation nobody made."
.into(),
direction: "over-grading".into(),
grade: None,
attestation: None,
flags: vec![],
clauses: vec![
ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
ExpectClause { label: "C2".into(), grade: None, stale: 0 },
],
conformant_at_e3: false,
},
work: work_by(&spec, "C1", &implementer),
spec,
state: state(),
witnesses: ws,
});
}
// 3 ── A non-goal is not owed, and does not cap.
{
let spec = spec_of(vec![
Clause::requirement("C1", "The obligation is well evidenced."),
Clause::non_goal("C2", "This is deliberately not built."),
]);
let ws = vec![witness(
&spec,
"C1",
falsifiable(Anchor::Specification),
&auditor,
state().address,
)];
out.push(Case {
name: "03-an-unwitnessed-non-goal-does-not-cap",
expect: Expect {
intent: "A requirement at E3 beside an unwitnessed non-goal.".into(),
trap: "Treating the non-goal as an owed obligation with no evidence \
empties the grade. A non-goal is owed nothing, so its absence \
of evidence is the correct state and caps nothing."
.into(),
direction: "under-grading".into(),
grade: Some(Grade::Falsifiable),
attestation: Some(Attestation::Independent),
flags: vec![],
clauses: vec![
ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
ExpectClause { label: "C2".into(), grade: None, stale: 0 },
],
conformant_at_e3: true,
},
work: work_by(&spec, "C1", &implementer),
spec,
state: state(),
witnesses: ws,
});
}
// 4 ── A witnessed non-goal is a flag, and flags block conformance.
{
let spec = spec_of(vec![
Clause::requirement("C1", "The obligation is well evidenced."),
Clause::non_goal("C2", "This is deliberately not built."),
]);
let ws = vec![
witness(&spec, "C1", falsifiable(Anchor::Specification), &auditor, state().address),
witness(&spec, "C2", falsifiable(Anchor::Specification), &auditor, state().address),
];
out.push(Case {
name: "04-evidence-for-a-non-goal-is-a-flag",
expect: Expect {
intent: "Something implements the clause that says not to.".into(),
trap: "Counting the non-goal's evidence as a rung, or discarding it \
quietly. It is a flag, and §3.4 makes any flag block conformance \
even where every grade is satisfied."
.into(),
direction: "over-grading".into(),
grade: Some(Grade::Falsifiable),
attestation: Some(Attestation::Independent),
flags: vec!["NonGoalWitnessed".into()],
clauses: vec![
ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
ExpectClause { label: "C2".into(), grade: None, stale: 0 },
],
conformant_at_e3: false,
},
work: work_by(&spec, "C1", &implementer),
spec,
state: state(),
witnesses: ws,
});
}
// 5 ── An unstated anchor caps a falsifiable check at E2.
{
let spec = spec_of(vec![Clause::requirement(
"C1",
"The obligation is checked by something whose expectation is unstated.",
)]);
let ws = vec![witness(
&spec,
"C1",
falsifiable(Anchor::Unstated),
&auditor,
state().address,
)];
out.push(Case {
name: "05-an-unstated-anchor-caps-at-exercised",
expect: Expect {
intent: "A check with a killed counter-artifact but no stated anchor."
.into(),
trap: "Reading the counter-artifact alone and awarding E3. An oracle \
derived from the system under test cannot disagree with it, so \
§2.5 caps an unstated anchor at E2 however the check behaved."
.into(),
direction: "over-grading".into(),
grade: Some(Grade::Exercised),
attestation: Some(Attestation::Independent),
flags: vec![],
clauses: vec![ExpectClause {
label: "C1".into(),
grade: Some(Grade::Exercised),
stale: 0,
}],
conformant_at_e3: false,
},
work: work_by(&spec, "C1", &implementer),
spec,
state: state(),
witnesses: ws,
});
}
// 6 ── A proof nobody independent read is E2, not E4.
{
let spec = spec_of(vec![Clause::requirement(
"C1",
"The obligation is discharged as a proof under the prover's own formalization.",
)]);
let ws = vec![witness(
&spec,
"C1",
proved(
Grounding::Declared,
Vacuity::Refuted { counter: Address::of_bytes(b"eval-counter-model") },
),
&auditor,
state().address,
)];
out.push(Case {
name: "06-a-declared-formalization-caps-at-exercised",
expect: Expect {
intent: "A non-vacuous proof whose binding to the clause is the \
prover's own word."
.into(),
trap: "Awarding E4 because a prover succeeded. The proof is real \
machine-checked evidence about something — E2 — and that the \
something is this clause is unconfirmed (§2.6)."
.into(),
direction: "over-grading".into(),
grade: Some(Grade::Exercised),
attestation: Some(Attestation::Independent),
flags: vec![],
clauses: vec![ExpectClause {
label: "C1".into(),
grade: Some(Grade::Exercised),
stale: 0,
}],
conformant_at_e3: false,
},
work: work_by(&spec, "C1", &implementer),
spec,
state: state(),
witnesses: ws,
});
}
// 7 ── A possibly-vacuous proof is E2, even cross-checked.
{
let spec = spec_of(vec![Clause::requirement(
"C1",
"The obligation is discharged as a proof nobody checked for vacuity.",
)]);
let ws = vec![witness(
&spec,
"C1",
proved(
Grounding::CrossChecked { by: crosschecker.verifying_key().to_bytes() },
Vacuity::Unchecked,
),
&auditor,
state().address,
)];
out.push(Case {
name: "07-an-unchecked-vacuity-caps-at-exercised",
expect: Expect {
intent: "A proof with an independently cross-checked formalization, \
never shown capable of failing."
.into(),
trap: "Awarding E4 because the formalization was cross-checked. A \
property can hold because nothing reaches the condition it \
guards; every rung above E2 rests on a demonstrated failure."
.into(),
direction: "over-grading".into(),
grade: Some(Grade::Exercised),
attestation: Some(Attestation::Independent),
flags: vec![],
clauses: vec![ExpectClause {
label: "C1".into(),
grade: Some(Grade::Exercised),
stale: 0,
}],
conformant_at_e3: false,
},
work: work_by(&spec, "C1", &implementer),
spec,
state: state(),
witnesses: ws,
});
}
// 8 ── A witness bound to a superseded state does not count.
{
let spec = spec_of(vec![Clause::requirement(
"C1",
"The obligation was checked against an earlier tree.",
)]);
let ws = vec![witness(
&spec,
"C1",
falsifiable(Anchor::Specification),
&auditor,
Address::of_bytes(b"eval-tree-v0"),
)];
out.push(Case {
name: "08-a-superseded-state-makes-a-witness-stale",
expect: Expect {
intent: "The only witness observed a tree that is no longer the \
artifact, and declared no footprint."
.into(),
trap: "Counting it because it verifies and names a stated obligation. \
An empty footprint means the whole artifact, so any change to \
the artifact invalidates it — and the clause is then unevidenced, \
which empties the grade rather than lowering it."
.into(),
direction: "over-grading".into(),
grade: None,
attestation: None,
flags: vec![],
clauses: vec![ExpectClause {
label: "C1".into(),
grade: None,
stale: 1,
}],
conformant_at_e3: false,
},
work: work_by(&spec, "C1", &implementer),
spec,
state: state(),
witnesses: ws,
});
}
// 9 ── A witness naming an obligation nobody stated is a flag.
{
let stated = spec_of(vec![Clause::requirement(
"C1",
"The obligation as the specification now words it.",
)]);
// A witness bound to the wording the clause used to have.
let older = spec_of(vec![Clause::requirement(
"C1",
"The obligation as the specification used to word it.",
)]);
let ws = vec![Witness::new(
stated.spec.spec_id().unwrap(),
obligation(&older, "C1"),
state().address,
falsifiable(Anchor::Specification),
Energy::new(1_000, Provenance::Estimator),
auditor.verifying_key().to_bytes(),
)
.sign(&auditor)
.expect("signs")];
out.push(Case {
name: "09-a-witness-for-a-reworded-clause-is-a-flag",
expect: Expect {
intent: "A verifying witness whose obligation address is the clause's \
previous wording."
.into(),
trap: "Discarding it silently, which is how drift stops being visible. \
It is reported as unbound, and the clause it used to evidence \
is now unevidenced."
.into(),
direction: "over-grading".into(),
grade: None,
attestation: None,
flags: vec!["Unbound".into()],
clauses: vec![ExpectClause {
label: "C1".into(),
grade: None,
stale: 0,
}],
conformant_at_e3: false,
},
work: work_by(&stated, "C1", &implementer),
spec: stated,
state: state(),
witnesses: ws,
});
}
// 10 ── A review by the clause's own author is a citation again.
{
let spec = spec_of(vec![Clause::requirement(
"C1",
"The obligation was reviewed by the party that wrote the specification.",
)]);
let ws = vec![witness(
&spec,
"C1",
Evidence::Reviewed { reviewer: key(1).verifying_key().to_bytes() },
&key(1),
state().address,
)];
out.push(Case {
name: "10-a-self-review-is-the-citation-again",
expect: Expect {
intent: "The reviewer and the specification's author are one key."
.into(),
trap: "Awarding E1 because the evidence says `reviewed`. E1 requires a \
second party, and independence is computed from the keys rather \
than taken from the label."
.into(),
direction: "over-grading".into(),
grade: Some(Grade::Cited),
attestation: Some(Attestation::SelfAttested),
flags: vec![],
clauses: vec![ExpectClause {
label: "C1".into(),
grade: Some(Grade::Cited),
stale: 0,
}],
conformant_at_e3: false,
},
work: work_by(&spec, "C1", &key(1)),
spec,
state: state(),
witnesses: ws,
});
}
out
}
fn json<T: Serialize>(value: &T) -> String {
let mut s = serde_json::to_string_pretty(value).expect("serialises");
s.push('\n');
s
}
#[test]
fn every_case_reaches_the_verdict_the_specification_requires() {
let generate = std::env::var("JOULESPEC_GEN_EVALUATION").is_ok();
let mut mismatched = Vec::new();
for case in cases() {
let got = conform::evaluate(&case.spec, &case.state, &case.witnesses, &case.work)
.unwrap_or_else(|e| panic!("{}: evaluation failed: {e}", case.name));
let seen = observed(&got, &case.expect);
if seen != case.expect {
mismatched.push(format!(
"{}\n expected {:#?}\n observed {:#?}",
case.name, case.expect, seen
));
}
let into = dir().join(case.name);
if generate {
std::fs::create_dir_all(&into).expect("case directory");
for (name, body) in [
("spec.json", json(&case.spec)),
("state.json", json(&case.state)),
("witnesses.json", json(&case.witnesses)),
("work.json", json(&case.work)),
// The expectation as this test *states* it, never as the
// evaluator produced it.
("expect.json", json(&case.expect)),
] {
std::fs::write(into.join(name), body).expect("writes");
}
} else {
let published = std::fs::read_to_string(into.join("expect.json")).unwrap_or_else(|e| {
panic!("{}: cannot read published expectation: {e}", case.name)
});
let published: Expect =
serde_json::from_str(&published).expect("published expectation parses");
assert_eq!(
published, case.expect,
"{}: the published expectation and this test disagree",
case.name
);
}
}
assert!(
mismatched.is_empty(),
"the evaluator disagrees with the specification on {} case(s):\n\n{}",
mismatched.len(),
mismatched.join("\n\n")
);
}
/// A corpus that tested one direction would certify one direction, so this
/// asserts the shape of the set rather than trusting that it was built as
/// described.
///
/// Both directions have to be present. An implementation that graded nothing
/// at all would pass every over-grading case — the under-grading cases are
/// what stop a corpus from rewarding a rule that simply refuses everything.
#[test]
fn the_corpus_tests_both_directions_and_says_which() {
let all = cases();
assert!(all.len() >= 10, "the corpus has shrunk: {}", all.len());
let mut over = 0;
let mut under = 0;
for case in &all {
assert!(
!case.expect.trap.is_empty() && !case.expect.intent.is_empty(),
"{}: a case without a stated trap documents nothing",
case.name
);
match case.expect.direction.as_str() {
"over-grading" => {
over += 1;
// The correct verdict must fall short of the bar, or be
// blocked by a flag. A case that conformed cleanly would be
// passed by a generous implementation for the wrong reason.
assert!(
!case.expect.conformant_at_e3 || !case.expect.flags.is_empty(),
"{}: labelled over-grading but conforms at E3 with no flag",
case.name
);
}
"under-grading" => {
under += 1;
// The correct verdict must *reach* the bar, or the case
// cannot catch an implementation that is too strict.
assert!(
case.expect.conformant_at_e3,
"{}: labelled under-grading but does not conform at E3, so a \
refuse-everything implementation passes it",
case.name
);
}
other => panic!("{}: unknown direction {other:?}", case.name),
}
}
assert!(over >= 8, "too few over-grading cases: {over}");
assert!(under >= 1, "no under-grading case: a refuse-everything evaluator passes");
}