From 4286242db5940726fb312c555a6e82f67215b39a Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sun, 1 Nov 2026 18:41:37 -0500 Subject: [PATCH 1/3] =?UTF-8?q?joulespec:=20the=20E4=20rung=20reaches=20a?= =?UTF-8?q?=20real=20prover,=20and=20=C2=A79=20gives=20the=20nearest=20pri?= =?UTF-8?q?or=20art=20its=20due?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two gaps, both found by looking harder at what already exists. §9 did not mention requirements-traceability tooling, which is the nearest thing to an existing implementation of §3. That family binds evidence to a requirement by identifier and revision, and its strongest member reads the test runner's results rather than the sources, so a citation on a test that never ran binds nothing. That is this standard's E2, reached independently, and E2 is therefore not a contribution here. What the family leaves open is what this standard closes: the revision is bumped by hand, where an obligation address is computed; and its own documentation records that a passing test asserting nothing still satisfies the gate, with test quality deferred to a separate human review. The closing claim is narrowed accordingly. Also noted: immutable tests are not falsifiable tests — an immutable test that asserts nothing is immutably vacuous. E4 was specified and its logic tested, but no witness had ever come from a prover. `joulespec-cli` now drives one, and parses the property table rather than the verdict line, because a checker reports success for a harness whose assumptions emptied its domain in the same words it uses for one that examined all of it — a gate reading the verdict passes vacuous proofs. Each harness carries a wall-clock budget, so an undecided run is a finding rather than a hang, and the process group is killed rather than the driver, which was observed leaving the solver running. Two statements are discharged over their whole input domain, both refuted by a counter-artifact; both sit at E2, not E4, because nobody independent has cross-checked their formalizations, and the report says so in those words. Measured, on this workspace: the counter-artifact narrowing the ratio rule's arithmetic from 128 to 64 bits is invisible to all 85 tests and refuted by the prover at once. The cost is not uniform — the same function's totality was settled in under a tenth of a second while its quotient bound did not converge in twenty-four minutes, so the budget is declared per harness and §8 says why a statement reshaped until it converges is a different claim. Extending this found a fourth defect in the standard's own manifest: extracting two rules into named functions moved the text two counter-artifacts were aimed at, by one indentation level in one case, and both silently stopped describing any edit. The harvester refused to run, which was correct but late, so it now validates every anchor before running anything. Tolerating a missing anchor would have left two clauses looking falsifiably evidenced while nothing was being mutated. SPEC §2.5 also now states the rules the producer already followed but the standard did not: a counter-artifact that does not build has demonstrated nothing, and a harness reporting success having run no checks is not evidence that any ran. CI gains a proofs leg on a host that has a checker. The linux leg cannot gate this: with no prover installed the proof entries are correctly reported as not run, which is no gate at all. The new leg asserts every declared cover is reached and that a counter-artifact still refutes a proof; its output parsing was tested against a passing, a vacuous and a no-cover log before being trusted. Co-Authored-By: Claude Opus 5 --- .github/workflows/standards-build.yml | 64 +++ README.md | 2 +- joulespec/SPEC.md | 154 +++++- joulespec/conformance/v1/README.md | 78 ++- joulespec/conformance/v1/harvest.toml | 95 +++- joulespec/joulespec-rs/Cargo.lock | 4 +- .../crates/joulespec-cli/Cargo.toml | 2 +- .../crates/joulespec-cli/src/harvest.rs | 268 +++++++++- .../crates/joulespec-cli/src/main.rs | 1 + .../crates/joulespec-cli/src/manifest.rs | 145 ++++++ .../crates/joulespec-cli/src/prover.rs | 456 ++++++++++++++++++ .../crates/joulespec-core/Cargo.toml | 6 +- .../crates/joulespec-core/src/conform.rs | 57 ++- .../crates/joulespec-core/src/lib.rs | 3 + .../crates/joulespec-core/src/proofs.rs | 138 ++++++ 15 files changed, 1424 insertions(+), 49 deletions(-) create mode 100644 joulespec/joulespec-rs/crates/joulespec-cli/src/prover.rs create mode 100644 joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index 94350aab6..9dcb3717d 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -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 diff --git a/README.md b/README.md index e2f0444a9..aff50bc8d 100644 --- a/README.md +++ b/README.md @@ -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 diff --git a/joulespec/SPEC.md b/joulespec/SPEC.md index 9e98d4844..5c25ffd8a 100644 --- a/joulespec/SPEC.md +++ b/joulespec/SPEC.md @@ -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 @@ -710,6 +756,24 @@ 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, with one +function, one input domain and one solver: 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. +Four orders of magnitude separate two statements about the same code. + +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 +815,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 +886,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. --- diff --git a/joulespec/conformance/v1/README.md b/joulespec/conformance/v1/README.md index 8ca7c5615..1c6af140c 100644 --- a/joulespec/conformance/v1/README.md +++ b/joulespec/conformance/v1/README.md @@ -54,6 +54,69 @@ 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, and was abandoned. + +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, not of the code — which is why +the budget is declared per harness and not once for a workspace. + **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 +143,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. diff --git a/joulespec/conformance/v1/harvest.toml b/joulespec/conformance/v1/harvest.toml index fe57f532d..7e93fb180 100644 --- a/joulespec/conformance/v1/harvest.toml +++ b/joulespec/conformance/v1/harvest.toml @@ -125,12 +125,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 +185,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 +316,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" diff --git a/joulespec/joulespec-rs/Cargo.lock b/joulespec/joulespec-rs/Cargo.lock index e45e4385e..4f158e798 100644 --- a/joulespec/joulespec-rs/Cargo.lock +++ b/joulespec/joulespec-rs/Cargo.lock @@ -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", diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml b/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml index 955107c7a..dc398796e 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml +++ b/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml @@ -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 diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs index c89ba5af7..826e8eefe 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs @@ -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 { } } +/// 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 { + 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::, _>>() + .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 { match name { "estimator" => Ok(Provenance::Estimator), @@ -240,6 +347,7 @@ pub fn harvest( )?; let labels: Vec = 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 +389,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 { diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs index a70c60ce0..4f38250ac 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs @@ -22,6 +22,7 @@ mod harvest; mod manifest; +mod prover; mod runner; mod specdoc; mod tree; diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs index e612e7c89..7d455b8b4 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs @@ -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. @@ -100,6 +132,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, + /// 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, +} + /// One declared mapping from an obligation to a check. #[derive(Debug, Clone, Serialize, Deserialize)] pub struct Evidence { @@ -116,6 +179,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, + /// When present, `check` names a proof harness rather than a test, and + /// this is its binding to the clause. + pub formalization: Option, } /// The whole manifest. @@ -153,10 +219,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 +359,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); diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/prover.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/prover.rs new file mode 100644 index 000000000..aefb43c76 --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/prover.rs @@ -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, + /// 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 { + 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>| { + 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)); + let err = drain(child.stderr.take().map(|s| Box::new(s) as Box)); + + 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()); + } +} diff --git a/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml b/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml index 672b6984f..fbe3cde8d 100644 --- a/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml +++ b/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml @@ -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)'] } diff --git a/joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs b/joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs index 2dd88b2c2..d82b9894c 100644 --- a/joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs +++ b/joulespec/joulespec-rs/crates/joulespec-core/src/conform.rs @@ -298,12 +298,7 @@ impl Conformance { /// features nobody requested. #[must_use] pub fn specified_ppm(&self) -> Option { - 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>>(graded: I) -> Option { + 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 { + 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, diff --git a/joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs b/joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs index ae8df80f7..8e4739b03 100644 --- a/joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs +++ b/joulespec/joulespec-rs/crates/joulespec-core/src/lib.rs @@ -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; diff --git a/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs b/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs new file mode 100644 index 000000000..3c57d91c4 --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs @@ -0,0 +1,138 @@ +//! 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" + ); +} + +/// A symbolic grade, over the whole of the ladder. +fn any_grade() -> Grade { + match kani::any::() % 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; 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 = 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"); +} -- 2.54.0 (Apple Git-157) From 1a3cca29c2142d0d81408aee8d933ae3f475b311 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sun, 1 Nov 2026 20:57:57 -0500 Subject: [PATCH 2/3] joulespec: the producer reads someone else's specification, not only this one MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The extractor recognised exactly one document shape — a numbered list of bolded, labelled items under a named section — which made the producer a tool for documents written like this family's own. Which shape a document uses is a fact about the document, so the manifest declares it, and three shapes cover what requirements are actually written as: a numbered conformance list, a bulleted requirement list, and a heading per requirement carrying its identifier. Only the item *opener* varies. The section is still named, the floor still fails closed, continuation lines still join with one space, and a shape that matches nothing is still an error rather than an empty clause list. Under the heading shape a blank line does not close an item, because a requirement's prose runs over paragraphs; the next heading of the same depth or shallower closes it, and a heading carrying no identifier is a grouping heading rather than a requirement. A heading with no prose under it states nothing and is dropped: addressing the empty string would create an obligation nobody wrote and then grade it like any other. The load-bearing property is that none of this moved an existing obligation. The default shape is what an undeclared manifest selects, and the test pinning that is not a recording of what the new parser happens to produce — the address was computed by running the same fixture through the parser as it stood before the change, in a worktree at the previous commit, and the two agree. The reference manifest deliberately declares no shape, so it stands as that check too. SPEC §8 gains the limit this exposes: an obligation address depends on how the clause was extracted, so two producers reading one document under different conventions state different obligations about the same prose and both are correct. A conforming producer must therefore disclose the convention it applied, because the document alone is not enough to recompute the addresses. There is deliberately no shape-free convenience wrapper. A caller that did not have to name a shape would read some documents correctly and others silently wrongly, and the obligation addresses are computed from whatever it captured. Co-Authored-By: Claude Opus 5 --- joulespec/README.md | 34 +- joulespec/SPEC.md | 8 + joulespec/conformance/v1/harvest.toml | 4 + .../crates/joulespec-cli/src/harvest.rs | 5 + .../crates/joulespec-cli/src/manifest.rs | 7 + .../crates/joulespec-cli/src/specdoc.rs | 418 ++++++++++++++++-- 6 files changed, 437 insertions(+), 39 deletions(-) diff --git a/joulespec/README.md b/joulespec/README.md index a0a9959a6..61727ca55 100644 --- a/joulespec/README.md +++ b/joulespec/README.md @@ -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,7 +327,18 @@ 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. diff --git a/joulespec/SPEC.md b/joulespec/SPEC.md index 5c25ffd8a..dc95839ea 100644 --- a/joulespec/SPEC.md +++ b/joulespec/SPEC.md @@ -713,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 diff --git a/joulespec/conformance/v1/harvest.toml b/joulespec/conformance/v1/harvest.toml index 7e93fb180..00e726d43 100644 --- a/joulespec/conformance/v1/harvest.toml +++ b/joulespec/conformance/v1/harvest.toml @@ -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.\ diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs index 826e8eefe..691ab1dae 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs @@ -340,10 +340,15 @@ 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 = items.iter().map(|i| i.label.clone()).collect(); manifest.check_clauses(&labels)?; diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs index 7d455b8b4..817a44c62 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs @@ -90,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, /// The specification's intent, in the operator's words. pub intent: String, } diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs index 3710b1720..e20732309 100644 --- a/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs @@ -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 { + 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 { + 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, 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 = Vec::new(); let mut pending: Option = 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 { 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::>(), + ["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); } } -- 2.54.0 (Apple Git-157) From 06f00e619a8c3d847f4054d40a7d78340f73c046 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sun, 1 Nov 2026 21:56:22 -0500 Subject: [PATCH 3/3] joulespec: an evaluation corpus, and a measured limit on what a second solver buys MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two things asked for: a benchmark corpus, and a second verification method. ## The corpus The wire vectors certify that an implementation round-trips a receipt's bytes. They say nothing about whether it reached the right verdict, because they carry one scenario. `conformance/v1/evaluation/` is the other half: ten cases, each a complete set of evaluation inputs plus the verdict §3 requires, chosen so a plausible but generous implementation disagrees — a mean where a minimum is required, an unevidenced obligation skipped rather than emptying the grade, `E3` on a killed counter-artifact whose anchor is unstated, `E4` because a prover succeeded, a witness for a clause's previous wording discarded instead of flagged, a `reviewed` label taken at face value when the reviewer is the clause's own author. Each case states its direction. Most catch over-grading; one catches under-grading, and that one is load-bearing: an implementation that graded nothing at all would pass every over-grading case, so a corpus with one direction rewards a rule that refuses everything. A test asserts the shape of the set rather than trusting it was built as described. The expectations are written by hand from §3 and are never read back out of this implementation — a corpus whose expectations are whatever the code produced certifies agreement with itself. That earned its keep immediately: seven of the ten were wrong on first authoring, all the same mistake and mine rather than the evaluator's. They assumed the attestation axis came from who signed a witness, where §2.8 computes it from who authored the work; with no work declared it is absent. The fix was not to copy the observed value in, which would have buried the misunderstanding, but to declare work in every case so the axis is exercised at all. ## What a second method bought, and what it did not The quotient-bound statement abandoned in the previous commit was retried under a solver reasoning with a bitvector theory rather than bit-blasting to a propositional problem. It settled four of the statement's conditions in about eight seconds — where the default engine had shown no per-property progress in twenty-four minutes — and then spent over fifty minutes on the fifth. So the method moved the wall without removing it, and §8 now says that instead of implying a solver choice would fix it. The harness is kept as the reproducible record of a negative result, behind a `cfg` nobody sets so an ordinary run does not hang on it. A second finding from the same runs, recorded in `conformance/v1/README.md`: a wall-clock wrapper around a prover is not enough. Both abandoned runs outlived the `timeout` meant to bound them, because the prover is a driver that spawns the checker and a timeout reaches only the driver. The producer kills the process group, which is why its budget works where the shell's did not — the design was right for a reason that has now been observed twice. Co-Authored-By: Claude Opus 5 --- joulespec/README.md | 20 +- joulespec/SPEC.md | 18 +- joulespec/conformance/v1/README.md | 31 +- .../expect.json | 21 + .../spec.json | 120 +++ .../state.json | 7 + .../witnesses.json | 239 ++++++ .../work.json | 46 ++ .../expect.json | 21 + .../spec.json | 120 +++ .../state.json | 7 + .../witnesses.json | 122 +++ .../work.json | 46 ++ .../expect.json | 21 + .../spec.json | 120 +++ .../state.json | 7 + .../witnesses.json | 122 +++ .../work.json | 46 ++ .../expect.json | 23 + .../spec.json | 120 +++ .../state.json | 7 + .../witnesses.json | 242 ++++++ .../work.json | 46 ++ .../expect.json | 16 + .../spec.json | 115 +++ .../state.json | 7 + .../witnesses.json | 122 +++ .../work.json | 46 ++ .../expect.json | 16 + .../spec.json | 115 +++ .../state.json | 7 + .../witnesses.json | 129 +++ .../work.json | 46 ++ .../expect.json | 16 + .../spec.json | 115 +++ .../state.json | 7 + .../witnesses.json | 165 ++++ .../work.json | 46 ++ .../expect.json | 16 + .../spec.json | 115 +++ .../state.json | 7 + .../witnesses.json | 122 +++ .../work.json | 46 ++ .../expect.json | 18 + .../spec.json | 115 +++ .../state.json | 7 + .../witnesses.json | 122 +++ .../work.json | 46 ++ .../expect.json | 16 + .../spec.json | 115 +++ .../state.json | 7 + .../witnesses.json | 153 ++++ .../work.json | 46 ++ joulespec/conformance/v1/evaluation/README.md | 85 ++ .../crates/joulespec-core/Cargo.toml | 2 +- .../crates/joulespec-core/src/proofs.rs | 52 ++ .../crates/joulespec-core/tests/evaluation.rs | 736 ++++++++++++++++++ 57 files changed, 4351 insertions(+), 15 deletions(-) create mode 100644 joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/expect.json create mode 100644 joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/spec.json create mode 100644 joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/state.json create mode 100644 joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/work.json create mode 100644 joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/expect.json create mode 100644 joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/spec.json create mode 100644 joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/state.json create mode 100644 joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/work.json create mode 100644 joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/expect.json create mode 100644 joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/spec.json create mode 100644 joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/state.json create mode 100644 joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/work.json create mode 100644 joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/expect.json create mode 100644 joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/spec.json create mode 100644 joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/state.json create mode 100644 joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/work.json create mode 100644 joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/expect.json create mode 100644 joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/spec.json create mode 100644 joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/state.json create mode 100644 joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/work.json create mode 100644 joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/expect.json create mode 100644 joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/spec.json create mode 100644 joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/state.json create mode 100644 joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/work.json create mode 100644 joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/expect.json create mode 100644 joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/spec.json create mode 100644 joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/state.json create mode 100644 joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/work.json create mode 100644 joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/expect.json create mode 100644 joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/spec.json create mode 100644 joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/state.json create mode 100644 joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/work.json create mode 100644 joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/expect.json create mode 100644 joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/spec.json create mode 100644 joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/state.json create mode 100644 joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/work.json create mode 100644 joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/expect.json create mode 100644 joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/spec.json create mode 100644 joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/state.json create mode 100644 joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/witnesses.json create mode 100644 joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/work.json create mode 100644 joulespec/conformance/v1/evaluation/README.md create mode 100644 joulespec/joulespec-rs/crates/joulespec-core/tests/evaluation.rs diff --git a/joulespec/README.md b/joulespec/README.md index 61727ca55..11618ca99 100644 --- a/joulespec/README.md +++ b/joulespec/README.md @@ -344,7 +344,7 @@ 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 @@ -353,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 diff --git a/joulespec/SPEC.md b/joulespec/SPEC.md index dc95839ea..2175f6483 100644 --- a/joulespec/SPEC.md +++ b/joulespec/SPEC.md @@ -766,12 +766,18 @@ 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, with one -function, one input domain and one solver: 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. -Four orders of magnitude separate two statements about the same code. +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 diff --git a/joulespec/conformance/v1/README.md b/joulespec/conformance/v1/README.md index 1c6af140c..7fe7837f2 100644 --- a/joulespec/conformance/v1/README.md +++ b/joulespec/conformance/v1/README.md @@ -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` @@ -108,14 +120,27 @@ seem. The same function, the same input domain and the same solver gave: 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, and was abandoned. + 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, not of the code — which is why -the budget is declared per harness and not once for a workspace. +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 diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/expect.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/expect.json new file mode 100644 index 000000000..6d6594e1c --- /dev/null +++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/spec.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/spec.json new file mode 100644 index 000000000..af12c7500 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/state.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/witnesses.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/witnesses.json new file mode 100644 index 000000000..a80a163ee --- /dev/null +++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/work.json b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/work.json new file mode 100644 index 000000000..07c240e2e --- /dev/null +++ b/joulespec/conformance/v1/evaluation/01-a-mean-conceals-the-weakest-obligation/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/expect.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/expect.json new file mode 100644 index 000000000..6bbda26a6 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/spec.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/spec.json new file mode 100644 index 000000000..eae7fed2c --- /dev/null +++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/state.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/witnesses.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/witnesses.json new file mode 100644 index 000000000..290e08dc5 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/work.json b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/work.json new file mode 100644 index 000000000..07c240e2e --- /dev/null +++ b/joulespec/conformance/v1/evaluation/02-an-unevidenced-obligation-empties-the-grade/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/expect.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/expect.json new file mode 100644 index 000000000..725dfc91a --- /dev/null +++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/spec.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/spec.json new file mode 100644 index 000000000..4ab949dbe --- /dev/null +++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/state.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/witnesses.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/witnesses.json new file mode 100644 index 000000000..6825c93a0 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/work.json b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/work.json new file mode 100644 index 000000000..a63ffa498 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/03-an-unwitnessed-non-goal-does-not-cap/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/expect.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/expect.json new file mode 100644 index 000000000..84723c383 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/spec.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/spec.json new file mode 100644 index 000000000..4ab949dbe --- /dev/null +++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/state.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/witnesses.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/witnesses.json new file mode 100644 index 000000000..c258e4633 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/work.json b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/work.json new file mode 100644 index 000000000..a63ffa498 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/04-evidence-for-a-non-goal-is-a-flag/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/expect.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/expect.json new file mode 100644 index 000000000..d668cb527 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/spec.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/spec.json new file mode 100644 index 000000000..9b802235c --- /dev/null +++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/state.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/witnesses.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/witnesses.json new file mode 100644 index 000000000..9aac3ff6c --- /dev/null +++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/work.json b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/work.json new file mode 100644 index 000000000..7d5ae9465 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/05-an-unstated-anchor-caps-at-exercised/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/expect.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/expect.json new file mode 100644 index 000000000..7e3e68529 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/spec.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/spec.json new file mode 100644 index 000000000..1a23877d7 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/state.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/witnesses.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/witnesses.json new file mode 100644 index 000000000..1daa9eddb --- /dev/null +++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/work.json b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/work.json new file mode 100644 index 000000000..323ba35af --- /dev/null +++ b/joulespec/conformance/v1/evaluation/06-a-declared-formalization-caps-at-exercised/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/expect.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/expect.json new file mode 100644 index 000000000..6e6463450 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/spec.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/spec.json new file mode 100644 index 000000000..868d617e6 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/state.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/witnesses.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/witnesses.json new file mode 100644 index 000000000..64a9a1532 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/work.json b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/work.json new file mode 100644 index 000000000..dcea7b37f --- /dev/null +++ b/joulespec/conformance/v1/evaluation/07-an-unchecked-vacuity-caps-at-exercised/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/expect.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/expect.json new file mode 100644 index 000000000..feabc2ea1 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/spec.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/spec.json new file mode 100644 index 000000000..d2cff9b2e --- /dev/null +++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/state.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/witnesses.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/witnesses.json new file mode 100644 index 000000000..46f2f8891 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/work.json b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/work.json new file mode 100644 index 000000000..482b65a11 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/08-a-superseded-state-makes-a-witness-stale/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/expect.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/expect.json new file mode 100644 index 000000000..45bcdd07f --- /dev/null +++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/spec.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/spec.json new file mode 100644 index 000000000..638a992ea --- /dev/null +++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/state.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/witnesses.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/witnesses.json new file mode 100644 index 000000000..0ee024825 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/work.json b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/work.json new file mode 100644 index 000000000..09846be9d --- /dev/null +++ b/joulespec/conformance/v1/evaluation/09-a-witness-for-a-reworded-clause-is-a-flag/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/expect.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/expect.json new file mode 100644 index 000000000..b12d364bd --- /dev/null +++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/expect.json @@ -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 +} diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/spec.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/spec.json new file mode 100644 index 000000000..f8053c14e --- /dev/null +++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/spec.json @@ -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 + ] +} diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/state.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/state.json new file mode 100644 index 000000000..206d47bb2 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/state.json @@ -0,0 +1,7 @@ +{ + "address": "b3:456b08df8833870546a773201f86bf36f22c85d792ff14d2de1886247827b7f9", + "parts": [ + "b3:aaa6eaff61f2be9a63d13bf1d9d33efce0857b526c7427b452a9b060543ff52b", + "b3:ea4a5352ad16166f240fb502662dae37c55179a680933f1c32a1b3ed8f40cc8e" + ] +} diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/witnesses.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/witnesses.json new file mode 100644 index 000000000..a50bea0fa --- /dev/null +++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/witnesses.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/work.json b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/work.json new file mode 100644 index 000000000..15609ff72 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/10-a-self-review-is-the-citation-again/work.json @@ -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 + ] + } +] diff --git a/joulespec/conformance/v1/evaluation/README.md b/joulespec/conformance/v1/evaluation/README.md new file mode 100644 index 000000000..46a4747a4 --- /dev/null +++ b/joulespec/conformance/v1/evaluation/README.md @@ -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. diff --git a/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml b/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml index fbe3cde8d..9491d3f3f 100644 --- a/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml +++ b/joulespec/joulespec-rs/crates/joulespec-core/Cargo.toml @@ -18,4 +18,4 @@ 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)'] } +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)', 'cfg(joulespec_slow_proofs)'] } diff --git a/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs b/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs index 3c57d91c4..69f015aea 100644 --- a/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs +++ b/joulespec/joulespec-rs/crates/joulespec-core/src/proofs.rs @@ -59,6 +59,58 @@ fn the_ratio_rule_is_total_over_every_input() { ); } +/// **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::() % 5 { diff --git a/joulespec/joulespec-rs/crates/joulespec-core/tests/evaluation.rs b/joulespec/joulespec-rs/crates/joulespec-core/tests/evaluation.rs new file mode 100644 index 000000000..6d26db08a --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-core/tests/evaluation.rs @@ -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, + /// The specification's attestation, on the second axis. + attestation: Option, + /// Flag kinds raised, by variant name, sorted. + flags: Vec, + /// Per clause, in specification order. + clauses: Vec, + /// 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, + /// 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 = 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) -> 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 { + 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, + work: Vec, + expect: Expect, +} + +#[allow(clippy::too_many_lines)] +fn cases() -> Vec { + 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(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"); +} -- 2.54.0 (Apple Git-157)