From 9ded4f4dad467d600b838d17be4dc26dffde4ae6 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sun, 1 Nov 2026 10:02:15 -0500 Subject: [PATCH] joulespec: a producer, and the standard applied to its own implementation v0.2 was a kernel nobody could emit into. This adds the reference producer and then points it at the implementation it describes -- which found two defects inspection had not. THE PRODUCER (joulespec-cli). `joulespec harvest` reads the clauses from a published specification document, runs each declared check, runs it again against a counter-artifact, and emits a signed witness at the rung the observations support. Also `verify` (a sealed receipt) and `drift` (two spec revisions). It refuses to confuse the three ways a run can fail to pass, which is the whole soundness story: * a test that did not RUN is not a test that passed. A harness filtered to a name nothing matches prints "running 0 tests", reports success and exits zero -- the shape of every check that silently stopped checking -- so the count is parsed and required; * a counter-artifact that did not COMPILE demonstrates nothing, because the check never ran. Treating it as E3 evidence would manufacture falsifiability out of a syntax error, which is the most misleading possible result; * a counter-artifact that compiled, ran and PASSED is a finding: the check cannot see the thing it is about. Exit 2 on a finding, 3 below --require-grade, so a pipeline can gate. Mutations revert on Drop, so a panic cannot leave one in place, and the CI step asserts the tree is clean afterwards rather than trusting that. 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 footprint -- a harness that cannot observe its own reads must not guess (SPEC 8). Everything else is computed, including the clauses: they are PARSED from SPEC.md 7 rather than copied into the manifest, so the manifest cannot drift from the specification. Reword an item and its obligation address moves. Re-wrapping a paragraph does not, because continuation lines join on one space -- a standard that punished `fmt` would teach people to avoid it. WHAT IT FOUND, pointed at joulespec itself (SPEC 7.1, conformance/v1/README): 1. A check whose assertion could not fail. A footprint test narrowed to a SINGLE member, and on a one-element footprint `all` and `any` are the same function -- so mutating the conjunction left it green and the conjunction was never checked. A second test now covers it. 2. Dead logic in the implementation. `applies_at` guarded on the state having no enumerable parts, and that guard could not change a single verdict: an `all` over a non-empty footprint against no parts is already false. It looked like care. It is gone. A third report was a mistake in the manifest -- a counter-artifact aimed at a branch its check never takes -- which the harvester correctly reported as a check that cannot see its subject. Telling those two readings apart is the operator's job; the harvester reports what it observed rather than guessing. Every conformance item C1-C11 now reaches E3 against a counter-artifact that made its check fail. Attestation is reported ABSENT, not independent: no work was declared, so no implementer is known, and the standard's own rule says absence of information about who built something is not evidence that someone else checked it. Inventing a figure there would have been the easy lie. TWO CONFORMANCE PACKS, and the distinction matters: * conformance/v1/vectors/ -- the certifiable surface the charter means. Fixed keys, clauses, witnesses and FIXED energy, byte-stable, regenerable with JOULESPEC_GEN_VECTORS=1 and asserted byte-for-byte otherwise. One witness of every rung the format can express, plus one bound to a superseded state, so an implementation that mishandles any rung or mishandles staleness fails the pack rather than passing it quietly. A test asserts that coverage, because a pack exercising one rung certifies one rung. Its verdict is the doctrine in miniature: two obligations well evidenced, one carrying only the implementer's citation, specification therefore E0 at A0. * the self-conformance receipt -- a MEASUREMENT, not a vector. Its energy comes from a wall clock graded Estimator, so re-running produces different bytes. A pack that held measured energy fixed would publish a figure nobody measured. CI gains a `harvest: true` matrix flag beside `clippy: true`, running the harvest on every change to this standard. It is the only gate that keeps the suite's falsifiability from decaying, which is precisely what inspection missed twice above. cargo check/clippy/test --workspace --all-targets --locked: green, zero warnings; harvest exits 0 with the tree clean after every mutation, on the M3 Ultra build host. Co-Authored-By: Claude Opus 5 --- .github/workflows/standards-build.yml | 38 +- README.md | 2 +- joulespec/README.md | 66 + joulespec/SPEC.md | 37 +- joulespec/conformance/v1/README.md | 84 + joulespec/conformance/v1/harvest.toml | 322 ++ joulespec/conformance/v1/receipt.cbor | Bin 0 -> 3328 bytes joulespec/conformance/v1/receipt.json | 140 + joulespec/conformance/v1/spec.json | 165 + joulespec/conformance/v1/state.json | 18 + joulespec/conformance/v1/vectors/receipt.cbor | Bin 0 -> 1489 bytes joulespec/conformance/v1/vectors/receipt.json | 64 + joulespec/conformance/v1/vectors/spec.json | 130 + joulespec/conformance/v1/vectors/state.json | 8 + .../conformance/v1/vectors/witnesses.json | 526 ++++ joulespec/conformance/v1/vectors/work.json | 88 + joulespec/conformance/v1/witnesses.json | 2687 +++++++++++++++++ joulespec/joulespec-rs/Cargo.lock | 95 + joulespec/joulespec-rs/Cargo.toml | 3 +- .../crates/joulespec-cli/Cargo.toml | 23 + .../crates/joulespec-cli/src/harvest.rs | 439 +++ .../crates/joulespec-cli/src/main.rs | 311 ++ .../crates/joulespec-cli/src/manifest.rs | 287 ++ .../crates/joulespec-cli/src/runner.rs | 316 ++ .../crates/joulespec-cli/src/specdoc.rs | 291 ++ .../crates/joulespec-cli/src/tree.rs | 204 ++ .../crates/joulespec-core/src/evidence.rs | 42 +- .../crates/joulespec-core/tests/vectors.rs | 243 ++ 28 files changed, 6621 insertions(+), 8 deletions(-) create mode 100644 joulespec/conformance/v1/README.md create mode 100644 joulespec/conformance/v1/harvest.toml create mode 100644 joulespec/conformance/v1/receipt.cbor create mode 100644 joulespec/conformance/v1/receipt.json create mode 100644 joulespec/conformance/v1/spec.json create mode 100644 joulespec/conformance/v1/state.json create mode 100644 joulespec/conformance/v1/vectors/receipt.cbor create mode 100644 joulespec/conformance/v1/vectors/receipt.json create mode 100644 joulespec/conformance/v1/vectors/spec.json create mode 100644 joulespec/conformance/v1/vectors/state.json create mode 100644 joulespec/conformance/v1/vectors/witnesses.json create mode 100644 joulespec/conformance/v1/vectors/work.json create mode 100644 joulespec/conformance/v1/witnesses.json create mode 100644 joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml create mode 100644 joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs create mode 100644 joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs create mode 100644 joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs create mode 100644 joulespec/joulespec-rs/crates/joulespec-cli/src/runner.rs create mode 100644 joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs create mode 100644 joulespec/joulespec-rs/crates/joulespec-cli/src/tree.rs create mode 100644 joulespec/joulespec-rs/crates/joulespec-core/tests/vectors.rs diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index c1cfb9908..94350aab6 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -90,7 +90,15 @@ jobs: # zero yet, and a gate that fails on arrival teaches people to pass # `--no-verify`. A workspace that reaches zero adds the flag and # cannot regress; joulespec-rs starts there. - - { name: joulespec-rs, dir: joulespec/joulespec-rs, runner: linux, clippy: true } + # `harvest: true` runs the standard against its own implementation: + # every conformance item of its SPEC §7 is mapped to a check, and + # each mapping declares a counter-artifact that must make that check + # FAIL before the evidence counts. It is slow (a rebuild per + # mutation) and it is the only gate that keeps the suite's + # falsifiability from decaying, which inspection does not catch -- + # 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 } - { 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 } @@ -294,6 +302,34 @@ jobs: RUSTFLAGS: ${{ matrix.rustflags }} run: cargo clippy --workspace --all-targets -- -D warnings + # The standard applied to its own implementation. Exits 2 on a finding + # (a check that did not run, or one that passed while its subject was + # broken) and 3 when an obligation falls below the bar, so a decayed + # suite fails here rather than being discovered by a reader. + # + # It mutates files in the checkout and reverts them; the revert runs on + # drop, so a panic cannot leave a mutation in place. The step asserts the + # tree is clean afterwards rather than trusting that. + - name: Self-conformance harvest + if: matrix.harvest + working-directory: ${{ matrix.dir }} + run: | + set -euo pipefail + cargo build --release -p joulespec-cli + target="$(cargo metadata --no-deps --format-version 1 \ + | python3 -c 'import json,sys; print(json.load(sys.stdin)["target_directory"])')" + "$target/release/joulespec" harvest \ + --manifest ../conformance/v1/harvest.toml --require-grade E3 + - name: The harvest left no mutation behind + if: matrix.harvest + run: | + set -euo pipefail + if ! git diff --quiet; then + echo "the harvest did not revert cleanly:" + git diff --stat + exit 1 + fi + # 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 6958849f3..e2f0444a9 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. `cargo test --workspace` green, `cargo clippy --workspace --all-targets` zero warnings and gated in CI. +- **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. ## How this is organised diff --git a/joulespec/README.md b/joulespec/README.md index 15e1b87b1..a0a9959a6 100644 --- a/joulespec/README.md +++ b/joulespec/README.md @@ -267,6 +267,65 @@ the witness that carried it, evidence energy, stale count — because which obligation is the weak one is the actionable fact, and it must be answerable from the receipt alone (SPEC §6.3). +## The producer, and the standard applied to itself + +A schema nobody can emit into is a schema. `joulespec-cli` is the reference +producer: it reads the clauses from a published specification document, runs +each declared check, runs it again against a **counter-artifact**, and emits a +signed witness at the rung the observations support. + +``` +joulespec harvest --manifest conformance/v1/harvest.toml \ + --out conformance/v1 --require-grade E3 +``` + +It refuses to confuse the three ways a run can fail to pass. A test that did +not run is not a test that passed — a harness filtered to a name nothing +matches prints `running 0 tests`, reports success and exits zero, so the count +is checked. A counter-artifact that did not compile demonstrates nothing, +because the check never ran; treating that as `E3` evidence would manufacture +falsifiability out of a syntax error. And a counter-artifact that compiled, ran +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. + +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 +footprint — a harness that cannot observe its own reads must not guess (SPEC +§8). Everything else is computed. + +**The standard is applied to its own implementation.** Every conformance item +of SPEC §7 is mapped to a check with a counter-artifact, and the clauses are +read from the published `SPEC.md` rather than copied into the manifest, so the +manifest cannot drift from the specification: reword an item and its obligation +address moves, invalidating the evidence bound to the old wording. + +Doing that found two things inspection had not. A footprint test narrowed to a +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 +[`conformance/v1/README.md`](conformance/v1/README.md), and that is the `E3` +rung doing the only thing it claims to do. + +## Conformance packs + +Two, answering different questions: + +- [`conformance/v1/vectors/`](conformance/v1/vectors/) — **the certifiable + surface.** Fixed keys, clauses, witnesses and energy, byte-stable, carrying + one witness of every rung plus one bound to a superseded state so an + implementation that mishandles staleness fails rather than passes quietly. + 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. + ## Relation to existing work Structured assurance cases already standardize the *shape* of the argument — @@ -317,6 +376,13 @@ deterministic two-axis evaluator with the weakest-obligation cap and footprint-aware staleness (`conform`), the revision partition (`drift`), and the `joulespec/1` JCR-1 receipt derived from its inputs (`receipt`). +[`joulespec-rs/crates/joulespec-cli`](joulespec-rs/crates/joulespec-cli) — the +reference producer: clauses parsed from a published document (`specdoc`), the +artifact state and its part addresses (`tree`), the declared mappings +(`manifest`), the check runner with its three-way distinction between a run +that failed, one that did not compile and one that should not have passed +(`runner`), and the harvest itself (`harvest`). + Prior art inside this family: `joule-code-spec` first shipped the signed, content-addressed clause and the citation binding a coding operation to it. Its citations bind by clause **label** and its audit has one notion of coverage diff --git a/joulespec/SPEC.md b/joulespec/SPEC.md index f60f37323..9e98d4844 100644 --- a/joulespec/SPEC.md +++ b/joulespec/SPEC.md @@ -629,10 +629,39 @@ An implementation conforms to `joulespec/1` when: from agreement between disjoint parties, is absent where no implementer is known, and gates conformance alongside the grade (§2.8, §3.4). -The reference implementation is conformant by construction. A third-party -implementation certifies itself by reproducing these behaviours; the reference -test suite in [`joulespec-rs/`](joulespec-rs/) is the executable form of the -list above. +A third-party implementation certifies itself by round-tripping the published +vectors in [`conformance/v1/vectors/`](conformance/v1/vectors/): fixed keys, +fixed clauses, fixed witnesses and fixed energy, carrying one witness of every +rung the format can express plus one bound to a superseded artifact state, so +an implementation that mishandles any rung or mishandles staleness fails the +pack rather than passing it quietly. + +### 7.1 The reference implementation does not certify itself by assertion + +"Conformant by construction" is the claim this standard exists to distrust, so +the reference implementation is held to its own ladder. Each item above is +mapped to a check, and each mapping declares a **counter-artifact** — a +one-occurrence edit that should make that check fail. The reference producer +applies it, runs the check, requires a *failure*, reverts, and only then emits +a witness at `E3` ([`conformance/v1/harvest.toml`](conformance/v1/harvest.toml)). + +The mapping from item to check is declared by the operator and not inferred, +for the same reason a formalization is never inferred (§2.6): deciding that a +particular check stands for a particular obligation is a human judgement, and a +tool that guessed it would be grading its own guess. + +Running this against the implementation found two things inspection had not: a +check whose assertion could not fail, because it narrowed to a single footprint +member where `all` and `any` coincide; and a guard in `applies_at` that could +not change a single verdict. Both are recorded in +[`conformance/v1/README.md`](conformance/v1/README.md). That is the `E3` rung +doing the only thing it claims to do. + +The self-conformance receipt in that directory is a **measurement, not a +vector**: its energy figures come from a wall clock, so re-running the harvest +produces different bytes. Only `vectors/` is byte-stable, and the division is +deliberate — a pack that held measured energy fixed would be publishing a +figure nobody measured. --- diff --git a/joulespec/conformance/v1/README.md b/joulespec/conformance/v1/README.md new file mode 100644 index 000000000..8ca7c5615 --- /dev/null +++ b/joulespec/conformance/v1/README.md @@ -0,0 +1,84 @@ +# JouleSpec conformance — `v1` + +Two packs live here. They answer different questions and only one of them is +reproducible, which is the first thing to know about them. + +## `vectors/` — the certifiable surface + +Fixed keys, fixed clauses, fixed witnesses and **fixed energy**, producing +receipt bytes that must not change without a version bump. This is the pack the +charter's conformance test refers to: an implementation certifies itself by +round-tripping these files. + +The witness set carries one of every rung the format can express — `cited`, +`exercised`, `falsifiable`, `proved` — plus a witness bound to an earlier +artifact state, so a verifier that mishandles staleness fails the pack rather +than passing it quietly. A pack that exercised one rung would certify one rung, +and a test asserts the coverage. + +The verdict these bytes assert is worth reading, because it is the doctrine in +miniature: two obligations are well evidenced, one carries only the +implementer's citation, and the specification's grade is therefore **`E0`**. +The attestation is `A0` for the same reason — the only surviving witness on +that clause is the implementer's own. One clause is a non-goal with no +evidence, which is correct and carries no grade, and a quarter of the declared +work energy cites no clause at all. + +Regenerate with: + +``` +JOULESPEC_GEN_VECTORS=1 cargo test -p joulespec-core --test vectors +``` + +Without that variable the test asserts the committed bytes, so a change to the +wire format fails in CI rather than shipping. + +## The self-conformance record + +`spec.json`, `witnesses.json`, `state.json`, `receipt.cbor` and `receipt.json` +in this directory are **not** vectors. They are the output of running the +reference producer against the reference implementation: + +``` +joulespec harvest --manifest conformance/v1/harvest.toml \ + --out conformance/v1 --require-grade E3 +``` + +The clauses are the conformance items of [`SPEC.md`](../../SPEC.md) §7, read +from the published document rather than copied into the manifest — so the +manifest cannot drift from the specification. Reword an item and its obligation +address moves, and every witness bound to the old wording stops applying. + +Each obligation is mapped to a check in `joulespec-rs`, and each mapping +declares a **counter-artifact**: a one-occurrence edit that should make that +check fail. The harvester applies it, runs the check, requires a *failure*, +and reverts. Only then does the witness reach `E3`. + +**These receipts are not reproducible, by construction.** Their energy figures +come from a wall clock, graded `Estimator`, because no meter is wired to this +harness yet. Re-running the harvest produces different microjoules and +therefore different receipt bytes. That is the honest behaviour of a measured +quantity and the reason the certifiable pack above holds energy fixed. + +## What the harvest found + +Running this against the implementation it describes did what the `E3` rung +exists to do, and found two things inspection had not: + +1. **A check that could not see its subject.** One footprint test narrowed to a + single member, and on a one-element footprint `all` and `any` are the same + function — so the conjunction itself was never checked. Mutating `all` to + `any` left the test passing. A second test now covers it. +2. **Dead logic in the implementation.** `applies_at` guarded on the artifact + state having no enumerable parts, and that guard could not change a single + verdict: an `all` over a non-empty footprint against no parts is already + false. The guard looked like care. It is gone. + +A third report was a mistake in the manifest rather than in the code — a +counter-artifact aimed at a branch its check never takes, which the harvester +correctly reported as a check that cannot see its subject. The distinction +between those two readings is the operator's to make, and the harvester +reports what it observed rather than guessing which it is. + +The harvester exits non-zero on a finding, so a pipeline can gate on it. CI +runs it on every change to this standard. diff --git a/joulespec/conformance/v1/harvest.toml b/joulespec/conformance/v1/harvest.toml new file mode 100644 index 000000000..fe57f532d --- /dev/null +++ b/joulespec/conformance/v1/harvest.toml @@ -0,0 +1,322 @@ +# JouleSpec applied to its own reference implementation. +# +# The clauses are the conformance items of SPEC.md §7, read from the published +# document rather than copied here, so the manifest cannot drift from the +# specification: reword an item and its obligation address moves, and every +# witness bound to the old wording stops applying (SPEC §4.2). +# +# Three things below are human judgements the standard refuses to guess: +# +# * which check stands for which obligation -- the mapping from prose to +# code, which is the same act as formalizing a clause (SPEC §2.6); +# * each check's `anchor` -- where its expected values come from, which the +# author of the check knows and nobody else can see (SPEC §2.5); +# * each check's `footprint` -- the inputs whose change could change the +# outcome, since a harness that cannot observe its own reads must not +# guess (SPEC §8). +# +# Each `counter` is a one-occurrence edit that SHOULD make the check fail. If +# it does not, the harvester reports a finding and the clause stays at E2: a +# check that passes while its subject is broken is an oracle that cannot fail. +# +# The keys are single-byte seeds so published vectors are reproducible by +# anyone. They are not secrets and a deployment must pass its own. + +workspace = "../../joulespec-rs" +steward = "did:key:joulespec-reference-steward" + +[spec] +document = "../../SPEC.md" +section = "7. Conformance" +expect_at_least = 11 +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.\ +""" + +[artifact] +dirs = ["crates"] +extensions = ["rs"] + +# No meter is wired, so energy is wall-clock times a declared draw and is +# graded `estimator`. A measured backend is the listed contributing ask; until +# one exists the figure says what it is. +[energy] +watts = 30.0 +provenance = "estimator" + +# ── C1 — Addressing ─────────────────────────────────────────────────────── +[[evidence]] +clause = "C1" +check = "spec::tests::relabelling_a_clause_moves_no_obligation" +anchor = "specification" +footprint = ["crates/joulespec-core/src/spec.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/spec.rs" +find = 'let doc = json!({ "kind": self.kind.label(), "text": self.text });' +replace = 'let doc = json!({ "label": self.label, "kind": self.kind.label(), "text": self.text });' +breaks = "puts the label back into the obligation address" + +[[evidence]] +clause = "C1" +check = "spec::tests::rewording_a_clause_moves_its_obligation" +anchor = "specification" +footprint = ["crates/joulespec-core/src/spec.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/spec.rs" +find = 'let doc = json!({ "kind": self.kind.label(), "text": self.text });' +replace = 'let doc = json!({ "kind": self.kind.label(), "text": "" });' +breaks = "drops the text from the obligation address" + +# ── C2 — Validation ─────────────────────────────────────────────────────── +[[evidence]] +clause = "C2" +check = "spec::tests::two_clauses_stating_one_obligation_are_refused" +anchor = "specification" +footprint = ["crates/joulespec-core/src/spec.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/spec.rs" +find = "return Err(Error::DuplicateObligation(first, clause.label.clone()));" +replace = "let _ = first;" +breaks = "stops refusing two clauses that state one obligation" + +# ── C3 — Signatures ─────────────────────────────────────────────────────── +[[evidence]] +clause = "C3" +check = "spec::tests::a_tampered_clause_breaks_the_signature" +anchor = "specification" +footprint = ["crates/joulespec-core/src/spec.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/spec.rs" +find = """ key.verify(&pre, &Signature::from_bytes(&sig)).map_err(|_| Error::BadSignature)?; + self.spec.spec_id()""" +replace = """ let _ = (&pre, &sig, &key); + self.spec.spec_id()""" +breaks = "stops verifying the specification signature at all" + +# ── C4 — The ladder ─────────────────────────────────────────────────────── +[[evidence]] +clause = "C4" +check = "evidence::tests::a_proof_reaches_e4_only_when_grounded_and_shown_non_vacuous" +anchor = "specification" +footprint = ["crates/joulespec-core/src/evidence.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/evidence.rs" +find = "if grounded && vacuity.is_refuted() { Grade::Proved } else { Grade::Exercised }" +replace = "if grounded { Grade::Proved } else { Grade::Exercised }" +breaks = "lets a possibly-vacuous proof reach E4" + +[[evidence]] +clause = "C4" +check = "evidence::tests::a_self_review_is_the_citation_again" +anchor = "specification" +footprint = ["crates/joulespec-core/src/evidence.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/evidence.rs" +find = "if reviewer == author { Grade::Cited } else { Grade::Reviewed }" +replace = "{ let _ = (reviewer, author); Grade::Reviewed }" +breaks = "stops computing independence from key disjointness" + +# ── C5 — Evaluation ─────────────────────────────────────────────────────── +[[evidence]] +clause = "C5" +check = "conform::tests::a_specification_is_graded_by_its_weakest_owed_obligation" +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);""" +breaks = "takes the strongest owed obligation instead of the weakest" + +[[evidence]] +clause = "C5" +check = "conform::tests::evaluation_is_deterministic_under_witness_reordering" +anchor = "specification" +footprint = ["crates/joulespec-core/src/conform.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/conform.rs" +find = "grade > current || (grade == current && &witness_id < best)" +replace = "grade >= current" +breaks = "breaks ties by input order instead of by address" + +# ── C6 — Drift ──────────────────────────────────────────────────────────── +[[evidence]] +clause = "C6" +check = "drift::tests::rewording_one_clause_invalidates_exactly_that_clauses_evidence" +anchor = "specification" +footprint = ["crates/joulespec-core/src/drift.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/drift.rs" +find = ".chain(self.reworded.iter().map(|r| r.was.clone()))" +replace = ".chain(std::iter::empty::())" +breaks = "stops counting a reworded clause's old obligation as invalidated" + +[[evidence]] +clause = "C6" +check = "drift::tests::reusing_a_freed_label_is_an_addition_not_a_rewording" +anchor = "specification" +footprint = ["crates/joulespec-core/src/drift.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/drift.rs" +find = "Some(was) if !to_by_obligation.contains_key(was) => reworded.push(Reword {" +replace = "Some(was) => reworded.push(Reword {" +breaks = "mistakes a reused label for a rewording" + +# ── C7 — Cost ───────────────────────────────────────────────────────────── +[[evidence]] +clause = "C7" +check = "conform::tests::an_aggregate_is_graded_by_the_weakest_figure_that_fed_it" +anchor = "specification" +footprint = [ + "crates/joulespec-core/src/lib.rs", + "crates/joulespec-core/src/conform.rs", +] +[evidence.counter] +file = "crates/joulespec-core/src/lib.rs" +find = " it.into_iter().min()" +replace = " it.into_iter().max()" +breaks = "grades an aggregate by its best figure instead of its worst" + +[[evidence]] +clause = "C7" +check = "conform::tests::a_ratio_with_no_work_is_absent_rather_than_zero" +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); + }""" +breaks = "reports a ratio of nothing as zero rather than absent" + +# ── C8 — Receipts ───────────────────────────────────────────────────────── +[[evidence]] +clause = "C8" +check = "receipt::tests::an_ungraded_specification_omits_the_grade_rather_than_sealing_a_floor" +anchor = "specification" +footprint = ["crates/joulespec-core/src/receipt.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/receipt.rs" +find = """ if let Some(grade) = conformance.grade { + map.insert("grade".into(), json!(grade.code())); + }""" +replace = """ map.insert("grade".into(), json!(conformance.grade.map_or("E0", Grade::code)));""" +breaks = "seals a floor grade where none was established" + +[[evidence]] +clause = "C8" +check = "receipt::tests::a_receipt_is_byte_identical_for_identical_evidence" +anchor = "specification" +footprint = ["crates/joulespec-core/src/receipt.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/receipt.rs" +find = 'map.insert("steward".into(), json!(steward));' +replace = 'map.insert("steward".into(), json!(format!("{steward}{:?}", std::time::Instant::now())));' +breaks = "makes a receipt depend on when it was sealed rather than on its evidence" + +# ── C9 — Footprints ─────────────────────────────────────────────────────── +[[evidence]] +clause = "C9" +check = "evidence::tests::the_footprint_is_part_of_what_the_signature_covers" +anchor = "specification" +footprint = ["crates/joulespec-core/src/evidence.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/evidence.rs" +find = '"footprint": self.footprint.iter().map(Address::as_str).collect::>(),' +replace = '"footprint": Vec::<&str>::new(),' +breaks = "leaves the footprint out of what the signature covers" + +[[evidence]] +clause = "C9" +check = "evidence::tests::a_narrowed_witness_survives_a_change_it_did_not_depend_on" +anchor = "specification" +footprint = ["crates/joulespec-core/src/evidence.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/evidence.rs" +find = "self.footprint.iter().all(|a| state.parts.contains(a))" +replace = "self.footprint.iter().all(|a| a == &state.address)" +breaks = "matches footprint members against the whole-state address rather than its parts" + +# Added after a harvest finding: the entry above narrows to one footprint +# member, and on a one-element footprint `all` and `any` are the same +# function, so the conjunction itself went unchecked. +[[evidence]] +clause = "C9" +check = "evidence::tests::a_witness_needs_every_footprint_member_not_merely_one" +anchor = "specification" +footprint = ["crates/joulespec-core/src/evidence.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/evidence.rs" +find = "self.footprint.iter().all(|a| state.parts.contains(a))" +replace = "self.footprint.iter().any(|a| state.parts.contains(a))" +breaks = "keeps a witness alive when only some of its footprint survives" + +[[evidence]] +clause = "C9" +check = "evidence::tests::a_footprint_that_cannot_be_checked_is_stale" +anchor = "specification" +footprint = ["crates/joulespec-core/src/evidence.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/evidence.rs" +find = " self.footprint.iter().all(|a| state.parts.contains(a))" +replace = " state.parts.is_empty() || self.footprint.iter().all(|a| state.parts.contains(a))" +breaks = "assumes a state it cannot enumerate satisfies every footprint" + +# ── C10 — Demonstrated failure ──────────────────────────────────────────── +[[evidence]] +clause = "C10" +check = "evidence::tests::an_unstated_anchor_caps_a_falsifiable_check_at_e2" +anchor = "specification" +footprint = ["crates/joulespec-core/src/evidence.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/evidence.rs" +find = " if anchor.is_stated() { Grade::Falsifiable } else { Grade::Exercised }" +replace = " { let _ = anchor; Grade::Falsifiable }" +breaks = "lets a check with no stated anchor reach E3" + +[[evidence]] +clause = "C10" +check = "evidence::tests::every_rung_above_e2_rests_on_a_demonstrated_failure" +anchor = "specification" +footprint = ["crates/joulespec-core/src/evidence.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/evidence.rs" +find = " Self::Exercised { .. } => Grade::Exercised," +replace = " Self::Exercised { .. } => Grade::Falsifiable," +breaks = "promotes a merely passing check to E3" + +# ── C11 — Attestation ───────────────────────────────────────────────────── +[[evidence]] +clause = "C11" +check = "conform::tests::with_no_work_supplied_independence_is_absent_not_assumed" +anchor = "specification" +footprint = ["crates/joulespec-core/src/conform.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/conform.rs" +find = """ let attestation = if implementers.is_empty() { + None""" +replace = """ let attestation = if implementers.is_empty() { + Some(Attestation::Independent)""" +breaks = "assumes independence where no implementer is known" + +[[evidence]] +clause = "C11" +check = "conform::tests::agreement_among_implementers_alone_is_not_reproduction" +anchor = "specification" +footprint = ["crates/joulespec-core/src/conform.rs"] +[evidence.counter] +file = "crates/joulespec-core/src/conform.rs" +find = """ let any_independent = + !implementers.is_empty() && authors.iter().any(|a| !implementers.contains(a)); + if any_independent {""" +replace = """ let any_independent = !implementers.is_empty(); + if any_independent {""" +breaks = "calls agreement among implementers reproduction" diff --git a/joulespec/conformance/v1/receipt.cbor b/joulespec/conformance/v1/receipt.cbor new file mode 100644 index 0000000000000000000000000000000000000000..cdfe5bb4512c8a23aec3dd35e33b6dea0b2d7509 GIT binary patch literal 3328 zcmbtXKd9ta6<%SBK>oNSk(d-}ND(3g@85Ip-NJv%ZXF_omlQtEJ?Gq)d2e>+WoF*) zst6X^WJ$0QwQ{kM2!fb&DQtqI351|qh@eGCI_*LVA%61`mdxA2fq{XU-`{(`^L^(# z-@NzJy{CTrg(uJNJ)sl5cw|4gcsM_q+Va@s>4gnj*i7u{<;t$}LT^2P-z$IA`LWH; z>HNCsy}G{d#-$!FR!Jk9#!!>5m69@Nr+&mjTzleNOAb*rQZBKFRJw8vIL_Ky7O^qq zgXK9pSg=~Z91mp5Crex2d+^!XH@4Z}i@aD(2FvPnPih*}xxqO~BVrePq8g1j7{v7ul64wJnVm#$?ks*Eh8J8GioR$aniH`vQVl1gj9$2M&p9j>QqhZP)}D)(d{TT!9hi-lgvD8*hQw1$@J#n(;#?|JjJ z=@$6Y4)}Xj0X@aM03FDHO0`iDw#GEP>!l>2t~pbS7KdZ>hnNc@qqe*BpQxACJ!?y0e=+-s&WBTpRf;j zK=#EmYl0SlvcT;)GX&2djjN5W=o1u&L~=UIKgo!_z);K=&V_x5u`9V0a;Pmc4q+=X z!Oz1ej6%m;T=5VS8`Zvn|H2Dj{bURLv;%%heCk*cjo&d>;8$Kctbn@9q#krPR>F`9 z9HY9CTNJ>kwz*;Mb0s_$y;dqMrO^Z-fD~QjV5V!qG*27&ANtFOf7*iox&waa#aWIJ zw87wDYA$mE21~9>FCmX!&9z;S%kffeD3z{ONnm6!2U{^la0)N{De*l<7u3#LAR-sW#@42cH)N9#y zcwWGqO0Yzz1U>S3p z1K`0gedWvB6kwMGNFzx>80+Q{O?-vxVc5miBP808hKVxv23I3%l$(YQ)ncG^5IBOK zRe(XwSN`^$m+t)C z*k2fO_VMcI&Y5rc8;_nG?jPG?|8wbg|I-lt*admwqrGq6e)#73D?g+EJp1^sKlt~z zzCU^M{e1P+Z+?8=7610{o_zV$yaA Ozj^-WzklwT^Zx_p6mJFq literal 0 HcmV?d00001 diff --git a/joulespec/conformance/v1/receipt.json b/joulespec/conformance/v1/receipt.json new file mode 100644 index 000000000..03b1a422a --- /dev/null +++ b/joulespec/conformance/v1/receipt.json @@ -0,0 +1,140 @@ +{ + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "clause_verdicts": [ + { + "anchor": "specification", + "evidence_uj": 220870549, + "grade": "E3", + "kind": "requirement", + "label": "C1", + "means": "falsifiable", + "obligation": "b3:e20e0c45fdd1f188ecc2ec14336ce8114091b7f135167354d7a0f6850e447a01", + "stale": 0, + "witness": "b3:10038b46255ddc9ae23ba69980e894d7432ac21a4bc3842be2a2d48d4ac242c8" + }, + { + "anchor": "specification", + "evidence_uj": 136337618, + "grade": "E3", + "kind": "requirement", + "label": "C2", + "means": "falsifiable", + "obligation": "b3:12f1ce65c6317d8fd546a17c8ee653cfb7a8ab554942c138aff317684eb5640d", + "stale": 0, + "witness": "b3:678f318db933498e35ac92d9cfd040d070cc39377e32c0b224eb6fe65a0c31e0" + }, + { + "anchor": "specification", + "evidence_uj": 146516332, + "grade": "E3", + "kind": "requirement", + "label": "C3", + "means": "falsifiable", + "obligation": "b3:d95410443c29a8f2b0f0b1706835b4ea0fd2f15b7e2b86e643b830e83cbb7181", + "stale": 0, + "witness": "b3:85b178284fdb56372c8f12109342e853089dbd2c571571b6b87332347921bf51" + }, + { + "anchor": "specification", + "evidence_uj": 262166629, + "grade": "E3", + "kind": "requirement", + "label": "C4", + "means": "falsifiable", + "obligation": "b3:46b79b1adb450e144c3688f0596a487e580af4eba6e7aa81917bc24e7ce6b1b7", + "stale": 0, + "witness": "b3:b8dc17c7e1c1b6ff3ce8d967cae9a6f10b774c6bd55693e3f0aba6ce02ccf898" + }, + { + "anchor": "specification", + "evidence_uj": 274341887, + "grade": "E3", + "kind": "requirement", + "label": "C5", + "means": "falsifiable", + "obligation": "b3:6cf3b7b46e17a57a1233bd604252895a23394d345cc2f7a67c3570711bfae68b", + "stale": 0, + "witness": "b3:8c03c2576f11424edc95171aad472c02c74b4a5a65aab7ea8efbd98e9a66cc54" + }, + { + "anchor": "specification", + "evidence_uj": 274388629, + "grade": "E3", + "kind": "requirement", + "label": "C6", + "means": "falsifiable", + "obligation": "b3:17565e58cd2c39ee8d68f161771b79dd7f94bbec6810007c3e75a28e2cf2f97e", + "stale": 0, + "witness": "b3:64a20e0c335abadeecc1cb3496b056d10ab9ad6f372a33d0f594f2926647814c" + }, + { + "anchor": "specification", + "evidence_uj": 331802546, + "grade": "E3", + "kind": "requirement", + "label": "C7", + "means": "falsifiable", + "obligation": "b3:3e0209539dfdce9adb3d34a9ed3a8663f31d867944f9c8646d93e0a0c6e17916", + "stale": 0, + "witness": "b3:2f60c6d0f7e131ab211da3e02c0bb0a75fc48a65c66a1a95ab60fb763f73eeb1" + }, + { + "anchor": "specification", + "evidence_uj": 241518310, + "grade": "E3", + "kind": "requirement", + "label": "C8", + "means": "falsifiable", + "obligation": "b3:4dc63e74ac96b125f6d35f3f1ab9a7d80888534c42ddceffc6c4b5a5c4d32485", + "stale": 0, + "witness": "b3:01c0e538e9e15792105a4e02e40bcb725fb8e09b7cd68ce9c84dde381986d226" + }, + { + "anchor": "specification", + "evidence_uj": 555213018, + "grade": "E3", + "kind": "requirement", + "label": "C9", + "means": "falsifiable", + "obligation": "b3:2df47b7fd601c83567401ea15235e8c1b1a47f79c151f2ebb8a5dbd148c4da29", + "stale": 0, + "witness": "b3:02e38460742ccd8c6f87bb58dd69eee51be3f238a47cab461b050814096c04da" + }, + { + "anchor": "specification", + "evidence_uj": 303373848, + "grade": "E3", + "kind": "requirement", + "label": "C10", + "means": "falsifiable", + "obligation": "b3:fdea1a57fd78b84a4b04f1b3970eb22eeef68e91c6ba42e3f84aed7512d1fe07", + "stale": 0, + "witness": "b3:8e243b644eb5adbea7a75010cbbc9cb940fd1f18ca9bd2369254594adda34f71" + }, + { + "anchor": "specification", + "evidence_uj": 277730625, + "grade": "E3", + "kind": "requirement", + "label": "C11", + "means": "falsifiable", + "obligation": "b3:e4c404541a6c954276e8b6680a8c1859439f62294203f1fac6bceec4d0c7c3c1", + "stale": 0, + "witness": "b3:6f4c7167be1a8a1856dd5539b32dd94686652d165e6e9659d2bfc6059b1f2f2d" + } + ], + "clauses": 11, + "evidence_uj": 3024259991, + "flags": 0, + "grade": "E3", + "joulespec_receipt": "joulespec/1", + "open": 0, + "owed": 11, + "provenance": "Estimator", + "spec": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "specified_uj": 0, + "steward": "did:key:joulespec-reference-steward", + "uj_per_falsifiable_clause": 274932726, + "unspecified": [], + "unspecified_uj": 0 +} \ No newline at end of file diff --git a/joulespec/conformance/v1/spec.json b/joulespec/conformance/v1/spec.json new file mode 100644 index 000000000..4b8a275f7 --- /dev/null +++ b/joulespec/conformance/v1/spec.json @@ -0,0 +1,165 @@ +{ + "spec": { + "profile": "joulespec/1", + "alg": 1, + "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.", + "clauses": [ + { + "label": "C1", + "kind": "requirement", + "text": "Addressing — Obligation addresses are computed over `{kind, text}` with the label excluded; relabelling preserves an address and rewording changes it." + }, + { + "label": "C2", + "kind": "requirement", + "text": "Validation — Specifications with a duplicate label, a duplicate obligation, an empty intent, an empty clause, or no clauses are refused, and a duplicate obligation names both clauses." + }, + { + "label": "C3", + "kind": "requirement", + "text": "Signatures — Specifications and witnesses verify over the preimages in §2.2 and §2.4, and altering any bound field invalidates the signature." + }, + { + "label": "C4", + "kind": "requirement", + "text": "The ladder — Grades are assigned per §2.5 and §2.6, with independence computed from key disjointness." + }, + { + "label": "C5", + "kind": "requirement", + "text": "Evaluation — The weakest-owed-obligation cap, the non-goal rule, the four flag conditions, staleness, and determinism under reordering all hold per §3." + }, + { + "label": "C6", + "kind": "requirement", + "text": "Drift — The §4.1 partition is computed by address, editorial revisions invalidate nothing, and a reused label is distinguished from a rewording." + }, + { + "label": "C7", + "kind": "requirement", + "text": "Cost — Aggregates carry the weakest contributing provenance; ratios are integer parts-per-million; absent figures are absent." + }, + { + "label": "C8", + "kind": "requirement", + "text": "Receipts — Receipts are derived from inputs, seal as JCR-1, omit absent fields, and carry the per-clause audit with means and anchor." + }, + { + "label": "C9", + "kind": "requirement", + "text": "Footprints — A witness applies at the state it observed, and at a later state whose parts still contain every footprint member; an empty or uncheckable footprint is stale (§2.4, §3.1). The footprint is signed, so widening it after signing invalidates the witness." + }, + { + "label": "C10", + "kind": "requirement", + "text": "Demonstrated failure — No evidence reaches `E3` without a killed counter-artifact and a stated anchor, and none reaches `E4` without both an independently cross-checked formalization and a refuted statement (§2.5, §2.6)." + }, + { + "label": "C11", + "kind": "requirement", + "text": "Attestation — The second axis is computed from work authorship and from agreement between disjoint parties, is absent where no implementer is known, and gates conformance alongside the grade (§2.8, §3.4)." + } + ], + "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, + 207, + 131, + 62, + 135, + 68, + 217, + 13, + 149, + 174, + 104, + 120, + 184, + 144, + 118, + 83, + 160, + 67, + 202, + 209, + 15, + 10, + 161, + 12, + 207, + 145, + 25, + 132, + 9, + 77, + 213, + 129, + 187, + 224, + 12, + 10, + 74, + 122, + 50, + 181, + 166, + 226, + 140, + 139, + 23, + 249, + 237, + 40, + 163, + 92, + 233, + 171, + 195, + 36, + 130, + 228, + 146, + 99, + 139, + 76, + 172, + 46, + 180, + 11 + ] +} \ No newline at end of file diff --git a/joulespec/conformance/v1/state.json b/joulespec/conformance/v1/state.json new file mode 100644 index 000000000..5eaafdd01 --- /dev/null +++ b/joulespec/conformance/v1/state.json @@ -0,0 +1,18 @@ +{ + "address": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "parts": [ + "b3:12acb39f94e62c0f951e10af1528fac38d531d4f000a1d388d00f4b5371fdda9", + "b3:24d370eeac7456d6384a0e4f693e98cbeaa6bb998597663f012c3fd5ba2844a2", + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9", + "b3:533973fda5dc5abd8a43dd1098505b56ac832cafa752caa492f1a076af342581", + "b3:76b49720a8bdc6b032fbbbaa13a750aa90f56eda0ceaf0476a30ff55c57d8d46", + "b3:78597bbf23ba8adef3d9ebf0048716f9dde330aad1c912ae7bb2704ac5e76fe1", + "b3:7b4a1ce7142ae0096d550c907df51cb37c58adcdc66b179bb67c2a53ca0c40a2", + "b3:950ddcffa72e1e7e935ae20de39f15da8d2d0713abcda0b1e3fcd8709d99b786", + "b3:b8b878c60d4da537c92cf3d8b10a8ade5fbff37c4e5ebf763459895f9dee90ec", + "b3:d42d371c28766af667aa4b55f398023c0c126b898c86009a623751ad454c9283", + "b3:d4e17e53ee429ecd404d72b1123d0c802b08aa33ed42187a44ff144dce283c26", + "b3:e294488af9bacf39bad6d40c40cd8d5abb67a76147c197ac0707eafd291fb418", + "b3:f97e43caa2984aafee912d22d7e04efbddd91111599bf30897a9fec9f17065ca" + ] +} \ No newline at end of file diff --git a/joulespec/conformance/v1/vectors/receipt.cbor b/joulespec/conformance/v1/vectors/receipt.cbor new file mode 100644 index 0000000000000000000000000000000000000000..08085564e167394144061b0ff66c6a6de00dc671 GIT binary patch literal 1489 zcmah}JBwsh5bkkD1WjDnz+Dtg+>Hk7yw90vWLVJEKvsk?kmj7KIz6|$=iZ)sZ_kX0 z;<{jz(5eh{RJilCYlI_p6Pk)^njW*)pbwR_o`oRZ(aR#<=X1j zQ&iFVgkN7DH}ffXGsd+&#=dFSx}NuAOCP`bVEl%f8P_Y+>@!`U!={7Hq}Cy1<&5?* z5o3U)V?>X_V9YV)>{y~vLa{&t$+1n4z~wB7H9};^c^XIEfJbd4PS;_C(>U+ATOA$G zKKS45wqx5@Iby$9$Vi#35jteDA&DfN_8?5m(j@JJAOw+g_JVTu(S;y=>9&$3c;yMk zv$omeI@ZY5^{%gWVj*G@`<}Z#_El4-XJNv76>;ep&c~N8{Wh7`hkR7IVtQ+_go7jm z2Eh)KOxYQ7AhL+sS+F5{C$))+a{$tb9VrsZd+nqYw-Jejcc^VT>)21lpSa*2=oDN}5 zc`(|q`kK3L0mo*BEF@|fbh1in4H+4|L6;roNM4v!l#Y%gu*wCqvJ?)#@;Z1LH)&dp z7VItFBMZ?)kuns2NC%#b2hBkTvfi0OMex>Qir_+y>`^(*%7AuWI#zO74zVQ1quXCD zAdj)ByS|OpeZ=Ynu{=UN$#L2h)nc0RG3;D)-)`CywsEoZ5*H=_Lr@wLLV#!)G+{CT zg1uD1WTzm7geaWWnzoQ$^obk52coIQ_NYbstT?V7dA0VSIpN^Gfw!&_G@5oC#OQZZOW zDAT1n{4e^Type7h@lqHclb#c_ZPXMaAA4LM>wA8eki3wYR1UV-PD?Kl4G~yT z_F(U9@Zg=#DoYKvq&Nj%?g=_D<+w?8)_Q~8)B8DWxtxz#KRK;DBMvUl$HN)7!!xcM z9>w*_;GwVXY;C-8Yxl=@*MAyc`~15b4}bK>1Fzl0w>K``ec^|@H@kZ;-MaY1(^nsV k^PLZW{r&mBH|~A%++Qz0`Te)AT$Fe0dpAD#bGkYB2iMs9=l}o! literal 0 HcmV?d00001 diff --git a/joulespec/conformance/v1/vectors/receipt.json b/joulespec/conformance/v1/vectors/receipt.json new file mode 100644 index 000000000..744ea4967 --- /dev/null +++ b/joulespec/conformance/v1/vectors/receipt.json @@ -0,0 +1,64 @@ +{ + "artifact": "b3:522f65149fd69b1b2748015af25b4891dc01b4f81dff8a7992851462e20838d0", + "attestation": "A0", + "clause_verdicts": [ + { + "attestation": "A1", + "evidence_uj": 4200, + "grade": "E4", + "kind": "requirement", + "label": "C1", + "means": "proved", + "obligation": "b3:d60a5a1bf07e22708d5804e949d68753889866cba079fae8c374e35047827e32", + "stale": 0, + "witness": "b3:6fe0f12c4294b632440fcec85c7f7cfad815be2ca7ea0e3fb2b36d9fe0f8498d" + }, + { + "anchor": "specification", + "attestation": "A1", + "evidence_uj": 1100, + "grade": "E3", + "kind": "constraint", + "label": "C2", + "means": "falsifiable", + "obligation": "b3:86c8c620f1b4cbd79fb510114ce0b0a11eeb71d8c69c914ad7b1c841cb9d17e6", + "stale": 0, + "witness": "b3:590e09340bc090a6e04dcb5001e82395f730b9bcc17444eeb2756c9667d9cc1b" + }, + { + "attestation": "A0", + "evidence_uj": 50, + "grade": "E0", + "kind": "requirement", + "label": "C3", + "means": "cited", + "obligation": "b3:44de2cb174e47f9c2e5f9522d7608677e29269bb3a96cc089723d760a8938527", + "stale": 1, + "witness": "b3:d897c982f31cd2ddc3a3ebef3abe5d63cfceeedb178ce6b6372a68ce7762a976" + }, + { + "evidence_uj": 0, + "kind": "non-goal", + "label": "C4", + "obligation": "b3:9b812fd3f965384282cc5dd06177ee876980878f3f2406d70b98480c705ff723", + "stale": 0 + } + ], + "clauses": 4, + "evidence_uj": 5350, + "flags": 0, + "grade": "E0", + "joulespec_receipt": "joulespec/1", + "open": 1, + "owed": 3, + "provenance": "Estimator", + "spec": "b3:09f37548abdec90b4aac8c15cafabff7e2c5313e1c50b7e6b0b07ff2de4c0ae7", + "specified_ppm": 750000, + "specified_uj": 750000, + "steward": "did:key:joulespec-vector-steward", + "uj_per_falsifiable_clause": 502675, + "unspecified": [ + "b3:70b11c91e7cb2bf75d701f1a476069f87245a3ef90d4be7d3d138847221d80db" + ], + "unspecified_uj": 250000 +} diff --git a/joulespec/conformance/v1/vectors/spec.json b/joulespec/conformance/v1/vectors/spec.json new file mode 100644 index 000000000..eb73c4cfa --- /dev/null +++ b/joulespec/conformance/v1/vectors/spec.json @@ -0,0 +1,130 @@ +{ + "spec": { + "profile": "joulespec/1", + "alg": 1, + "intent": "A metered endpoint that refuses what it cannot charge for.", + "clauses": [ + { + "label": "C1", + "kind": "requirement", + "text": "The endpoint rejects unauthenticated requests." + }, + { + "label": "C2", + "kind": "constraint", + "text": "A request is decided before any side effect runs." + }, + { + "label": "C3", + "kind": "requirement", + "text": "Every decision seals a receipt." + }, + { + "label": "C4", + "kind": "non-goal", + "text": "The endpoint does not implement its own retry policy." + } + ], + "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": [ + 141, + 120, + 240, + 2, + 220, + 25, + 193, + 121, + 12, + 97, + 82, + 103, + 203, + 191, + 105, + 163, + 190, + 107, + 249, + 174, + 236, + 107, + 173, + 224, + 4, + 239, + 55, + 52, + 38, + 192, + 173, + 238, + 14, + 180, + 97, + 128, + 112, + 223, + 149, + 213, + 180, + 87, + 23, + 36, + 80, + 87, + 54, + 72, + 117, + 250, + 93, + 219, + 203, + 152, + 28, + 240, + 231, + 65, + 113, + 173, + 191, + 71, + 36, + 2 + ] +} diff --git a/joulespec/conformance/v1/vectors/state.json b/joulespec/conformance/v1/vectors/state.json new file mode 100644 index 000000000..ca139ecb4 --- /dev/null +++ b/joulespec/conformance/v1/vectors/state.json @@ -0,0 +1,8 @@ +{ + "address": "b3:522f65149fd69b1b2748015af25b4891dc01b4f81dff8a7992851462e20838d0", + "parts": [ + "b3:54db5923a1c8b004e4f93f7c848b7f5de788fd3c600ab3070f70bfb7e150fb9b", + "b3:69bce1edec460f82fa06ad97487c1069c7d4f775b5c89dae0c21244438057151", + "b3:8624949b04e977f3df70c21be24b552bfd25065ea7d7f2ae9f4915953b483a6b" + ] +} diff --git a/joulespec/conformance/v1/vectors/witnesses.json b/joulespec/conformance/v1/vectors/witnesses.json new file mode 100644 index 000000000..3db918f17 --- /dev/null +++ b/joulespec/conformance/v1/vectors/witnesses.json @@ -0,0 +1,526 @@ +[ + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:09f37548abdec90b4aac8c15cafabff7e2c5313e1c50b7e6b0b07ff2de4c0ae7", + "obligation": "b3:d60a5a1bf07e22708d5804e949d68753889866cba079fae8c374e35047827e32", + "artifact": "b3:522f65149fd69b1b2748015af25b4891dc01b4f81dff8a7992851462e20838d0", + "footprint": [ + "b3:8624949b04e977f3df70c21be24b552bfd25065ea7d7f2ae9f4915953b483a6b" + ], + "evidence": { + "kind": "proved", + "goal": "b3:0e6cc1d5165db3c20269e67feb1931f29223f944f87298c1e9097525f0bc3399", + "tier": "T1", + "formalization": { + "statement": "forall r. !authenticated(r) -> rejected(r)", + "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": "refuted", + "counter": "b3:c236fcc067c11bc153de8d8e4a745a94fe7154700a6d3a57e981719e75caa72a" + } + }, + "energy": { + "uj": 4200, + "provenance": "model-based" + }, + "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": [ + 194, + 136, + 217, + 129, + 252, + 187, + 46, + 229, + 50, + 3, + 62, + 244, + 40, + 182, + 38, + 130, + 244, + 112, + 246, + 94, + 252, + 248, + 73, + 88, + 227, + 223, + 163, + 138, + 65, + 137, + 78, + 16, + 160, + 22, + 64, + 26, + 106, + 29, + 116, + 62, + 216, + 56, + 80, + 230, + 100, + 130, + 215, + 148, + 252, + 63, + 53, + 221, + 17, + 84, + 31, + 40, + 103, + 21, + 0, + 43, + 206, + 230, + 71, + 15 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:09f37548abdec90b4aac8c15cafabff7e2c5313e1c50b7e6b0b07ff2de4c0ae7", + "obligation": "b3:86c8c620f1b4cbd79fb510114ce0b0a11eeb71d8c69c914ad7b1c841cb9d17e6", + "artifact": "b3:522f65149fd69b1b2748015af25b4891dc01b4f81dff8a7992851462e20838d0", + "footprint": [ + "b3:54db5923a1c8b004e4f93f7c848b7f5de788fd3c600ab3070f70bfb7e150fb9b" + ], + "evidence": { + "kind": "falsifiable", + "check": "decided_before_side_effect", + "anchor": "specification", + "counter": "b3:6d5c6d2500a21a27aa9bddc2fc5948b85f2da6a24d0a26a5a3852508976c0e2c" + }, + "energy": { + "uj": 1100, + "provenance": "hw-shunt" + }, + "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": [ + 8, + 20, + 33, + 220, + 253, + 24, + 96, + 253, + 230, + 10, + 201, + 203, + 116, + 111, + 108, + 93, + 242, + 115, + 96, + 248, + 141, + 253, + 130, + 235, + 71, + 213, + 242, + 219, + 127, + 21, + 195, + 68, + 38, + 212, + 88, + 242, + 160, + 65, + 238, + 110, + 186, + 67, + 246, + 144, + 88, + 81, + 37, + 109, + 9, + 239, + 116, + 240, + 156, + 73, + 63, + 108, + 19, + 46, + 211, + 27, + 223, + 58, + 3, + 3 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:09f37548abdec90b4aac8c15cafabff7e2c5313e1c50b7e6b0b07ff2de4c0ae7", + "obligation": "b3:44de2cb174e47f9c2e5f9522d7608677e29269bb3a96cc089723d760a8938527", + "artifact": "b3:522f65149fd69b1b2748015af25b4891dc01b4f81dff8a7992851462e20838d0", + "footprint": [], + "evidence": { + "kind": "cited" + }, + "energy": { + "uj": 50, + "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": [ + 11, + 162, + 11, + 245, + 114, + 113, + 174, + 192, + 241, + 8, + 139, + 146, + 45, + 175, + 116, + 48, + 59, + 87, + 12, + 83, + 180, + 187, + 63, + 1, + 60, + 229, + 224, + 234, + 42, + 86, + 39, + 143, + 114, + 130, + 139, + 175, + 152, + 173, + 34, + 39, + 73, + 227, + 180, + 20, + 15, + 88, + 124, + 146, + 98, + 1, + 175, + 105, + 235, + 49, + 255, + 37, + 231, + 214, + 66, + 136, + 181, + 235, + 66, + 14 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:09f37548abdec90b4aac8c15cafabff7e2c5313e1c50b7e6b0b07ff2de4c0ae7", + "obligation": "b3:44de2cb174e47f9c2e5f9522d7608677e29269bb3a96cc089723d760a8938527", + "artifact": "b3:bf7e8cba19fd565845d65bfed3e7ba82e5af26fe417ebd96e7a5d97042fa2542", + "footprint": [], + "evidence": { + "kind": "exercised", + "check": "seals_a_receipt", + "anchor": "state" + }, + "energy": { + "uj": 900, + "provenance": "hw-shunt" + }, + "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": [ + 172, + 5, + 92, + 174, + 225, + 120, + 35, + 107, + 19, + 167, + 22, + 45, + 93, + 244, + 81, + 170, + 213, + 56, + 129, + 73, + 184, + 201, + 83, + 164, + 123, + 135, + 138, + 28, + 234, + 194, + 34, + 128, + 204, + 191, + 18, + 50, + 157, + 114, + 115, + 179, + 0, + 15, + 209, + 208, + 228, + 96, + 249, + 151, + 162, + 230, + 75, + 144, + 115, + 37, + 223, + 185, + 101, + 10, + 133, + 201, + 147, + 43, + 29, + 10 + ] + } +] diff --git a/joulespec/conformance/v1/vectors/work.json b/joulespec/conformance/v1/vectors/work.json new file mode 100644 index 000000000..1f934d525 --- /dev/null +++ b/joulespec/conformance/v1/vectors/work.json @@ -0,0 +1,88 @@ +[ + { + "id": "b3:c91a66ba27cd0f22ea5e7e18b5cf2e8a7e2da57ce0aefa28fb3f0d3631980b15", + "cites": [ + "b3:d60a5a1bf07e22708d5804e949d68753889866cba079fae8c374e35047827e32" + ], + "energy": { + "uj": 750000, + "provenance": "hw-shunt" + }, + "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 + ] + }, + { + "id": "b3:70b11c91e7cb2bf75d701f1a476069f87245a3ef90d4be7d3d138847221d80db", + "cites": [], + "energy": { + "uj": 250000, + "provenance": "hw-shunt" + }, + "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/witnesses.json b/joulespec/conformance/v1/witnesses.json new file mode 100644 index 000000000..8e3d10a0e --- /dev/null +++ b/joulespec/conformance/v1/witnesses.json @@ -0,0 +1,2687 @@ +[ + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:e20e0c45fdd1f188ecc2ec14336ce8114091b7f135167354d7a0f6850e447a01", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:533973fda5dc5abd8a43dd1098505b56ac832cafa752caa492f1a076af342581" + ], + "evidence": { + "kind": "falsifiable", + "check": "spec::tests::relabelling_a_clause_moves_no_obligation", + "anchor": "specification", + "counter": "b3:f51011f062073ca8723a12e6ab9a3ba6a200622b8cdec91175fd726aa7ce30d8" + }, + "energy": { + "uj": 81886536, + "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": [ + 157, + 233, + 88, + 119, + 118, + 24, + 244, + 123, + 6, + 226, + 170, + 219, + 14, + 113, + 159, + 105, + 22, + 153, + 191, + 28, + 17, + 19, + 34, + 96, + 122, + 199, + 188, + 65, + 211, + 7, + 116, + 29, + 176, + 254, + 73, + 158, + 144, + 92, + 128, + 68, + 248, + 155, + 34, + 67, + 9, + 90, + 249, + 197, + 34, + 139, + 179, + 179, + 196, + 131, + 37, + 111, + 103, + 7, + 34, + 194, + 125, + 8, + 210, + 10 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:e20e0c45fdd1f188ecc2ec14336ce8114091b7f135167354d7a0f6850e447a01", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:533973fda5dc5abd8a43dd1098505b56ac832cafa752caa492f1a076af342581" + ], + "evidence": { + "kind": "falsifiable", + "check": "spec::tests::rewording_a_clause_moves_its_obligation", + "anchor": "specification", + "counter": "b3:baadb16428aa942dc24bfd55d6aebc5ffa55984beeea6dea3b0e7c07710e963e" + }, + "energy": { + "uj": 138984013, + "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": [ + 208, + 5, + 225, + 230, + 227, + 88, + 175, + 36, + 198, + 19, + 24, + 122, + 49, + 249, + 193, + 174, + 188, + 0, + 170, + 56, + 228, + 197, + 30, + 253, + 143, + 94, + 239, + 180, + 218, + 218, + 197, + 119, + 87, + 61, + 15, + 82, + 4, + 240, + 32, + 27, + 111, + 24, + 39, + 138, + 58, + 243, + 150, + 48, + 190, + 167, + 79, + 139, + 124, + 15, + 185, + 85, + 162, + 85, + 49, + 227, + 115, + 109, + 224, + 11 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:12f1ce65c6317d8fd546a17c8ee653cfb7a8ab554942c138aff317684eb5640d", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:533973fda5dc5abd8a43dd1098505b56ac832cafa752caa492f1a076af342581" + ], + "evidence": { + "kind": "falsifiable", + "check": "spec::tests::two_clauses_stating_one_obligation_are_refused", + "anchor": "specification", + "counter": "b3:396c1bd6b162468d4f965af0b66943a11b9a73dbe9377eb58be3b5ed27b441e3" + }, + "energy": { + "uj": 136337618, + "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": [ + 132, + 250, + 62, + 239, + 67, + 253, + 165, + 136, + 128, + 93, + 171, + 36, + 163, + 201, + 133, + 53, + 177, + 252, + 227, + 21, + 28, + 179, + 219, + 182, + 228, + 66, + 217, + 15, + 188, + 52, + 233, + 241, + 112, + 130, + 200, + 109, + 241, + 254, + 83, + 69, + 65, + 255, + 48, + 111, + 225, + 174, + 221, + 205, + 57, + 6, + 150, + 62, + 187, + 41, + 214, + 2, + 179, + 233, + 5, + 226, + 105, + 22, + 15, + 9 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:d95410443c29a8f2b0f0b1706835b4ea0fd2f15b7e2b86e643b830e83cbb7181", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:533973fda5dc5abd8a43dd1098505b56ac832cafa752caa492f1a076af342581" + ], + "evidence": { + "kind": "falsifiable", + "check": "spec::tests::a_tampered_clause_breaks_the_signature", + "anchor": "specification", + "counter": "b3:2a7cb187ec6564c2257dfb593b2b95ad34f64763acff21272cfa7907e0a5b58f" + }, + "energy": { + "uj": 146516332, + "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": [ + 48, + 42, + 65, + 44, + 221, + 87, + 61, + 12, + 159, + 237, + 38, + 16, + 89, + 243, + 87, + 7, + 79, + 213, + 126, + 68, + 234, + 8, + 219, + 117, + 80, + 152, + 232, + 241, + 25, + 103, + 65, + 125, + 228, + 48, + 193, + 128, + 229, + 160, + 180, + 174, + 53, + 144, + 179, + 62, + 152, + 244, + 180, + 182, + 2, + 102, + 171, + 59, + 211, + 79, + 42, + 21, + 188, + 80, + 72, + 165, + 224, + 194, + 179, + 1 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:46b79b1adb450e144c3688f0596a487e580af4eba6e7aa81917bc24e7ce6b1b7", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9" + ], + "evidence": { + "kind": "falsifiable", + "check": "evidence::tests::a_proof_reaches_e4_only_when_grounded_and_shown_non_vacuous", + "anchor": "specification", + "counter": "b3:2a083ec804637f34e1fafeb8d7d198a26b75c63385059429fb7757e7cedaaad8" + }, + "energy": { + "uj": 135825112, + "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": [ + 97, + 100, + 173, + 145, + 147, + 241, + 141, + 143, + 128, + 155, + 238, + 95, + 35, + 114, + 17, + 182, + 81, + 2, + 57, + 55, + 242, + 7, + 53, + 222, + 174, + 56, + 211, + 244, + 111, + 233, + 174, + 221, + 116, + 49, + 27, + 204, + 67, + 27, + 45, + 105, + 242, + 89, + 194, + 192, + 176, + 121, + 14, + 107, + 169, + 53, + 218, + 152, + 14, + 149, + 179, + 121, + 128, + 20, + 63, + 215, + 133, + 49, + 190, + 4 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:46b79b1adb450e144c3688f0596a487e580af4eba6e7aa81917bc24e7ce6b1b7", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9" + ], + "evidence": { + "kind": "falsifiable", + "check": "evidence::tests::a_self_review_is_the_citation_again", + "anchor": "specification", + "counter": "b3:8ca2e8b5fd2b37703aef219466449cc15449fadbe68960a91994fe551ca0bbb6" + }, + "energy": { + "uj": 126341517, + "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": [ + 113, + 114, + 60, + 228, + 85, + 104, + 117, + 200, + 104, + 42, + 185, + 101, + 47, + 68, + 60, + 174, + 242, + 48, + 220, + 166, + 117, + 248, + 135, + 204, + 231, + 97, + 247, + 152, + 213, + 171, + 251, + 36, + 62, + 56, + 169, + 114, + 138, + 38, + 146, + 129, + 224, + 62, + 109, + 246, + 239, + 71, + 38, + 214, + 105, + 179, + 141, + 151, + 239, + 218, + 26, + 82, + 75, + 187, + 80, + 249, + 195, + 132, + 104, + 1 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:6cf3b7b46e17a57a1233bd604252895a23394d345cc2f7a67c3570711bfae68b", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:d42d371c28766af667aa4b55f398023c0c126b898c86009a623751ad454c9283" + ], + "evidence": { + "kind": "falsifiable", + "check": "conform::tests::a_specification_is_graded_by_its_weakest_owed_obligation", + "anchor": "specification", + "counter": "b3:6dfb470122fc023bcb7b50af6f3ff40eb6f2d4e736c77ac477725a4e89d67988" + }, + "energy": { + "uj": 135389083, + "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": [ + 65, + 92, + 220, + 173, + 59, + 206, + 165, + 144, + 240, + 165, + 54, + 91, + 150, + 15, + 197, + 250, + 99, + 159, + 118, + 192, + 237, + 162, + 34, + 181, + 213, + 194, + 23, + 120, + 169, + 99, + 213, + 202, + 228, + 184, + 54, + 253, + 23, + 167, + 211, + 231, + 164, + 49, + 136, + 34, + 54, + 82, + 107, + 198, + 202, + 42, + 102, + 47, + 127, + 232, + 26, + 7, + 214, + 223, + 38, + 111, + 187, + 14, + 101, + 15 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:6cf3b7b46e17a57a1233bd604252895a23394d345cc2f7a67c3570711bfae68b", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:d42d371c28766af667aa4b55f398023c0c126b898c86009a623751ad454c9283" + ], + "evidence": { + "kind": "falsifiable", + "check": "conform::tests::evaluation_is_deterministic_under_witness_reordering", + "anchor": "specification", + "counter": "b3:037c212599d46eac2a6a56daef9a8050cbf550528384e9e38e8c51c1d5d80f88" + }, + "energy": { + "uj": 138952804, + "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": [ + 117, + 227, + 135, + 189, + 81, + 77, + 224, + 37, + 89, + 48, + 174, + 14, + 57, + 97, + 131, + 233, + 179, + 20, + 88, + 9, + 171, + 236, + 105, + 189, + 177, + 128, + 116, + 98, + 115, + 174, + 14, + 125, + 227, + 77, + 9, + 221, + 214, + 0, + 120, + 252, + 62, + 78, + 95, + 61, + 119, + 49, + 32, + 236, + 239, + 41, + 210, + 94, + 44, + 172, + 149, + 77, + 222, + 125, + 19, + 193, + 64, + 127, + 242, + 2 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:17565e58cd2c39ee8d68f161771b79dd7f94bbec6810007c3e75a28e2cf2f97e", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:76b49720a8bdc6b032fbbbaa13a750aa90f56eda0ceaf0476a30ff55c57d8d46" + ], + "evidence": { + "kind": "falsifiable", + "check": "drift::tests::rewording_one_clause_invalidates_exactly_that_clauses_evidence", + "anchor": "specification", + "counter": "b3:b0bfee47b4c91a32becbbb90a87f19b0324df915c77c8d856e13f65dd49e7ca0" + }, + "energy": { + "uj": 149517380, + "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": [ + 149, + 239, + 87, + 65, + 63, + 38, + 82, + 157, + 162, + 76, + 32, + 51, + 233, + 40, + 62, + 171, + 97, + 105, + 149, + 99, + 121, + 153, + 99, + 177, + 120, + 200, + 223, + 213, + 147, + 128, + 208, + 241, + 174, + 215, + 149, + 164, + 255, + 23, + 195, + 77, + 218, + 57, + 122, + 83, + 3, + 149, + 130, + 155, + 186, + 124, + 138, + 110, + 69, + 236, + 202, + 63, + 57, + 198, + 232, + 30, + 212, + 176, + 222, + 8 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:17565e58cd2c39ee8d68f161771b79dd7f94bbec6810007c3e75a28e2cf2f97e", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:76b49720a8bdc6b032fbbbaa13a750aa90f56eda0ceaf0476a30ff55c57d8d46" + ], + "evidence": { + "kind": "falsifiable", + "check": "drift::tests::reusing_a_freed_label_is_an_addition_not_a_rewording", + "anchor": "specification", + "counter": "b3:12e8f3303789c16919a0bbf0af5e16916bbdddcbe6ba8f7c1d49c4741a209e65" + }, + "energy": { + "uj": 124871249, + "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": [ + 62, + 164, + 42, + 119, + 165, + 198, + 166, + 182, + 184, + 108, + 248, + 39, + 71, + 199, + 220, + 155, + 134, + 151, + 55, + 195, + 192, + 188, + 14, + 222, + 76, + 247, + 63, + 77, + 99, + 199, + 175, + 17, + 8, + 0, + 78, + 86, + 163, + 78, + 53, + 209, + 64, + 239, + 146, + 102, + 148, + 163, + 32, + 9, + 83, + 187, + 115, + 110, + 148, + 13, + 114, + 152, + 159, + 255, + 245, + 159, + 56, + 241, + 14, + 8 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:3e0209539dfdce9adb3d34a9ed3a8663f31d867944f9c8646d93e0a0c6e17916", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:7b4a1ce7142ae0096d550c907df51cb37c58adcdc66b179bb67c2a53ca0c40a2", + "b3:d42d371c28766af667aa4b55f398023c0c126b898c86009a623751ad454c9283" + ], + "evidence": { + "kind": "falsifiable", + "check": "conform::tests::an_aggregate_is_graded_by_the_weakest_figure_that_fed_it", + "anchor": "specification", + "counter": "b3:bfa5ccd566c2505662f2dbbfce7e46b217c23dcea623f5319752989d1fa925a6" + }, + "energy": { + "uj": 165155412, + "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": [ + 157, + 153, + 153, + 226, + 127, + 245, + 20, + 156, + 35, + 121, + 196, + 159, + 173, + 218, + 81, + 47, + 4, + 95, + 130, + 138, + 110, + 29, + 106, + 59, + 123, + 9, + 200, + 52, + 240, + 187, + 232, + 92, + 173, + 174, + 89, + 207, + 242, + 101, + 163, + 35, + 241, + 236, + 134, + 202, + 23, + 51, + 221, + 237, + 162, + 132, + 232, + 155, + 180, + 145, + 189, + 132, + 198, + 235, + 43, + 87, + 50, + 72, + 230, + 8 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:3e0209539dfdce9adb3d34a9ed3a8663f31d867944f9c8646d93e0a0c6e17916", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:d42d371c28766af667aa4b55f398023c0c126b898c86009a623751ad454c9283" + ], + "evidence": { + "kind": "falsifiable", + "check": "conform::tests::a_ratio_with_no_work_is_absent_rather_than_zero", + "anchor": "specification", + "counter": "b3:90d7a6669a55659d6e1b4df1925ebb5aaace6703c74153f3f62ce63d27968214" + }, + "energy": { + "uj": 166647134, + "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": [ + 129, + 182, + 12, + 168, + 244, + 232, + 161, + 83, + 131, + 249, + 246, + 176, + 186, + 147, + 156, + 15, + 136, + 67, + 196, + 143, + 154, + 136, + 24, + 210, + 207, + 98, + 37, + 200, + 74, + 135, + 226, + 29, + 26, + 126, + 187, + 85, + 11, + 230, + 39, + 70, + 170, + 228, + 254, + 118, + 181, + 101, + 249, + 51, + 133, + 229, + 228, + 209, + 125, + 131, + 119, + 175, + 66, + 200, + 61, + 218, + 133, + 232, + 57, + 7 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:4dc63e74ac96b125f6d35f3f1ab9a7d80888534c42ddceffc6c4b5a5c4d32485", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:b8b878c60d4da537c92cf3d8b10a8ade5fbff37c4e5ebf763459895f9dee90ec" + ], + "evidence": { + "kind": "falsifiable", + "check": "receipt::tests::an_ungraded_specification_omits_the_grade_rather_than_sealing_a_floor", + "anchor": "specification", + "counter": "b3:7ee6a27115dc0b31f9166746b6a09387655f6a69ff03a7d9052f9d18c95f8f58" + }, + "energy": { + "uj": 132646817, + "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": [ + 173, + 89, + 110, + 28, + 236, + 118, + 233, + 230, + 253, + 184, + 36, + 49, + 24, + 118, + 151, + 205, + 35, + 142, + 68, + 26, + 116, + 109, + 230, + 250, + 111, + 88, + 43, + 150, + 161, + 126, + 183, + 141, + 194, + 112, + 244, + 65, + 109, + 44, + 127, + 203, + 110, + 8, + 4, + 253, + 32, + 91, + 173, + 169, + 123, + 28, + 49, + 166, + 78, + 132, + 179, + 246, + 244, + 81, + 91, + 96, + 115, + 69, + 98, + 5 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:4dc63e74ac96b125f6d35f3f1ab9a7d80888534c42ddceffc6c4b5a5c4d32485", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:b8b878c60d4da537c92cf3d8b10a8ade5fbff37c4e5ebf763459895f9dee90ec" + ], + "evidence": { + "kind": "falsifiable", + "check": "receipt::tests::a_receipt_is_byte_identical_for_identical_evidence", + "anchor": "specification", + "counter": "b3:88b3f9f79738b53f2b838e75c533ef8f7173da0e9c714760095776434c116a11" + }, + "energy": { + "uj": 108871493, + "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": [ + 129, + 50, + 176, + 31, + 203, + 178, + 35, + 85, + 167, + 253, + 109, + 27, + 116, + 160, + 36, + 28, + 100, + 150, + 175, + 111, + 148, + 169, + 15, + 172, + 140, + 81, + 229, + 192, + 225, + 255, + 252, + 27, + 30, + 212, + 22, + 39, + 31, + 196, + 235, + 196, + 233, + 54, + 48, + 14, + 29, + 204, + 17, + 34, + 12, + 77, + 77, + 141, + 177, + 245, + 75, + 143, + 177, + 152, + 22, + 182, + 127, + 171, + 53, + 10 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:2df47b7fd601c83567401ea15235e8c1b1a47f79c151f2ebb8a5dbd148c4da29", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9" + ], + "evidence": { + "kind": "falsifiable", + "check": "evidence::tests::the_footprint_is_part_of_what_the_signature_covers", + "anchor": "specification", + "counter": "b3:5aba85ebfb77f1cd0a18511ef41cd1d1dcf2c1e66f20c5aa7c994a97a7715afa" + }, + "energy": { + "uj": 111799750, + "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": [ + 76, + 37, + 169, + 255, + 253, + 89, + 58, + 13, + 193, + 145, + 9, + 156, + 167, + 177, + 226, + 108, + 189, + 121, + 17, + 163, + 222, + 226, + 246, + 106, + 140, + 165, + 72, + 199, + 41, + 61, + 40, + 78, + 116, + 217, + 62, + 53, + 58, + 98, + 225, + 195, + 189, + 14, + 43, + 240, + 105, + 199, + 85, + 56, + 200, + 102, + 204, + 174, + 127, + 8, + 188, + 98, + 171, + 44, + 170, + 73, + 12, + 2, + 195, + 1 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:2df47b7fd601c83567401ea15235e8c1b1a47f79c151f2ebb8a5dbd148c4da29", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9" + ], + "evidence": { + "kind": "falsifiable", + "check": "evidence::tests::a_narrowed_witness_survives_a_change_it_did_not_depend_on", + "anchor": "specification", + "counter": "b3:dadca3ce741248fbd1e4bcbe1ae1beff7d8ae1062eca3c7132118c908d045662" + }, + "energy": { + "uj": 176341976, + "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": [ + 163, + 247, + 29, + 193, + 25, + 124, + 39, + 188, + 240, + 183, + 19, + 13, + 81, + 58, + 136, + 141, + 181, + 113, + 209, + 176, + 77, + 133, + 195, + 233, + 83, + 43, + 119, + 104, + 36, + 97, + 16, + 117, + 242, + 215, + 142, + 76, + 174, + 186, + 65, + 17, + 13, + 159, + 3, + 33, + 228, + 35, + 192, + 229, + 253, + 3, + 67, + 29, + 170, + 151, + 30, + 238, + 245, + 219, + 159, + 106, + 160, + 145, + 110, + 1 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:2df47b7fd601c83567401ea15235e8c1b1a47f79c151f2ebb8a5dbd148c4da29", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9" + ], + "evidence": { + "kind": "falsifiable", + "check": "evidence::tests::a_witness_needs_every_footprint_member_not_merely_one", + "anchor": "specification", + "counter": "b3:eafe7e39906ae69d87a4627c7913a63a87aa6756493edb3534a38a4c28741509" + }, + "energy": { + "uj": 147942981, + "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": [ + 19, + 228, + 149, + 136, + 159, + 193, + 33, + 76, + 208, + 170, + 101, + 21, + 140, + 73, + 117, + 60, + 100, + 1, + 89, + 137, + 223, + 90, + 49, + 103, + 247, + 152, + 132, + 207, + 235, + 173, + 152, + 94, + 218, + 180, + 137, + 87, + 237, + 224, + 216, + 18, + 227, + 44, + 146, + 10, + 62, + 52, + 108, + 219, + 101, + 193, + 66, + 90, + 12, + 105, + 183, + 143, + 111, + 191, + 9, + 21, + 131, + 244, + 210, + 5 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:2df47b7fd601c83567401ea15235e8c1b1a47f79c151f2ebb8a5dbd148c4da29", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9" + ], + "evidence": { + "kind": "falsifiable", + "check": "evidence::tests::a_footprint_that_cannot_be_checked_is_stale", + "anchor": "specification", + "counter": "b3:62bef405b1cc420e3b14906d5d15fd6b33483e7531d143ed5d39174c3d7f16bd" + }, + "energy": { + "uj": 119128311, + "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": [ + 187, + 127, + 32, + 71, + 136, + 202, + 45, + 241, + 203, + 175, + 153, + 112, + 156, + 206, + 196, + 190, + 35, + 209, + 87, + 237, + 1, + 67, + 183, + 144, + 10, + 39, + 108, + 182, + 12, + 222, + 240, + 38, + 113, + 205, + 201, + 216, + 109, + 81, + 159, + 202, + 152, + 171, + 186, + 143, + 58, + 220, + 145, + 142, + 101, + 57, + 135, + 108, + 82, + 160, + 45, + 188, + 238, + 248, + 53, + 243, + 129, + 183, + 219, + 12 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:fdea1a57fd78b84a4b04f1b3970eb22eeef68e91c6ba42e3f84aed7512d1fe07", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9" + ], + "evidence": { + "kind": "falsifiable", + "check": "evidence::tests::an_unstated_anchor_caps_a_falsifiable_check_at_e2", + "anchor": "specification", + "counter": "b3:09bad3cb2a4bac2067c4a8aadbec64c31363b2d215a2775e8043a90d1ea08c87" + }, + "energy": { + "uj": 154962199, + "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": [ + 211, + 147, + 94, + 12, + 242, + 193, + 26, + 132, + 33, + 155, + 31, + 19, + 114, + 237, + 61, + 155, + 206, + 183, + 152, + 70, + 216, + 43, + 200, + 254, + 72, + 145, + 135, + 49, + 35, + 126, + 33, + 58, + 159, + 174, + 12, + 38, + 155, + 221, + 66, + 86, + 25, + 155, + 146, + 102, + 217, + 162, + 201, + 201, + 145, + 34, + 16, + 103, + 77, + 135, + 19, + 220, + 59, + 48, + 130, + 75, + 77, + 169, + 115, + 0 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:fdea1a57fd78b84a4b04f1b3970eb22eeef68e91c6ba42e3f84aed7512d1fe07", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:393a521a589101b03a67a39a1fc778913f05a6262be342b4bc0819f0395a9ba9" + ], + "evidence": { + "kind": "falsifiable", + "check": "evidence::tests::every_rung_above_e2_rests_on_a_demonstrated_failure", + "anchor": "specification", + "counter": "b3:55ab60bca17630cbf62c776b9d4f1773c08730c977064d73c2abb340ea8b2cf3" + }, + "energy": { + "uj": 148411649, + "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": [ + 88, + 36, + 57, + 95, + 191, + 54, + 6, + 93, + 67, + 92, + 194, + 175, + 42, + 147, + 150, + 34, + 25, + 134, + 58, + 168, + 31, + 213, + 107, + 59, + 78, + 251, + 135, + 81, + 67, + 44, + 180, + 208, + 150, + 166, + 77, + 99, + 0, + 203, + 185, + 6, + 0, + 172, + 146, + 55, + 218, + 20, + 86, + 218, + 213, + 91, + 230, + 64, + 214, + 135, + 120, + 184, + 216, + 218, + 109, + 162, + 165, + 31, + 137, + 11 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:e4c404541a6c954276e8b6680a8c1859439f62294203f1fac6bceec4d0c7c3c1", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:d42d371c28766af667aa4b55f398023c0c126b898c86009a623751ad454c9283" + ], + "evidence": { + "kind": "falsifiable", + "check": "conform::tests::with_no_work_supplied_independence_is_absent_not_assumed", + "anchor": "specification", + "counter": "b3:9957ce94757f3b54e38ca876778651a0974a731abfb1f8d4ece6d67cd084ca34" + }, + "energy": { + "uj": 124748708, + "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": [ + 99, + 116, + 79, + 167, + 72, + 75, + 92, + 146, + 107, + 23, + 196, + 228, + 134, + 210, + 159, + 244, + 35, + 76, + 41, + 185, + 30, + 206, + 222, + 129, + 188, + 215, + 197, + 254, + 154, + 130, + 32, + 19, + 219, + 254, + 46, + 3, + 191, + 179, + 234, + 46, + 47, + 245, + 227, + 236, + 135, + 0, + 6, + 118, + 157, + 134, + 193, + 176, + 88, + 202, + 109, + 19, + 151, + 243, + 13, + 36, + 53, + 106, + 85, + 5 + ] + }, + { + "witness": { + "profile": "joulespec-witness/1", + "alg": 1, + "spec_id": "b3:8c4f5ed328418864daa50d1f376a8b4a587523dd36573b247bda82dd35d995cc", + "obligation": "b3:e4c404541a6c954276e8b6680a8c1859439f62294203f1fac6bceec4d0c7c3c1", + "artifact": "b3:ded2d00fa53c966a0214683cbf03f95da93f320fcdda7004eddae4b4f55e723a", + "footprint": [ + "b3:d42d371c28766af667aa4b55f398023c0c126b898c86009a623751ad454c9283" + ], + "evidence": { + "kind": "falsifiable", + "check": "conform::tests::agreement_among_implementers_alone_is_not_reproduction", + "anchor": "specification", + "counter": "b3:cd9d9f72e19cc485045db38588270c58096f8e0fa1b07bcc4e71171370835b03" + }, + "energy": { + "uj": 152981917, + "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": [ + 235, + 179, + 145, + 224, + 92, + 106, + 203, + 146, + 244, + 17, + 45, + 114, + 194, + 247, + 73, + 53, + 237, + 0, + 158, + 104, + 158, + 1, + 106, + 242, + 229, + 136, + 207, + 25, + 51, + 170, + 130, + 3, + 241, + 70, + 93, + 93, + 127, + 137, + 79, + 25, + 200, + 184, + 240, + 250, + 178, + 232, + 194, + 227, + 70, + 221, + 165, + 52, + 131, + 91, + 182, + 96, + 175, + 231, + 26, + 88, + 114, + 190, + 112, + 14 + ] + } +] \ No newline at end of file diff --git a/joulespec/joulespec-rs/Cargo.lock b/joulespec/joulespec-rs/Cargo.lock index 96ea68aff..e45e4385e 100644 --- a/joulespec/joulespec-rs/Cargo.lock +++ b/joulespec/joulespec-rs/Cargo.lock @@ -164,6 +164,12 @@ dependencies = [ "zeroize", ] +[[package]] +name = "equivalent" +version = "1.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "00d174d5400e5e8fd687ad1049e2f578285fa914201b1af7e8b112a4546bd826" + [[package]] name = "fiat-crypto" version = "0.2.9" @@ -197,12 +203,41 @@ dependencies = [ "wasi", ] +[[package]] +name = "hashbrown" +version = "0.17.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" + +[[package]] +name = "indexmap" +version = "2.14.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cc4e190f5d26ca7051642629da2c52fc03bde85a03197c99408dcd291734c855" +dependencies = [ + "equivalent", + "hashbrown", +] + [[package]] name = "itoa" version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" +[[package]] +name = "joulespec-cli" +version = "0.2.0" +dependencies = [ + "blake3", + "ed25519-dalek", + "joulespec-core", + "serde", + "serde_json", + "thiserror", + "toml", +] + [[package]] name = "joulespec-core" version = "0.2.0" @@ -321,6 +356,15 @@ dependencies = [ "zmij", ] +[[package]] +name = "serde_spanned" +version = "1.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4e7523beb55eece201a2356bee0bbca0d1ab466c14c07703b2e0ee6d42cb0c2c" +dependencies = [ + "serde_core", +] + [[package]] name = "sha2" version = "0.10.9" @@ -405,6 +449,45 @@ dependencies = [ "syn 3.0.9", ] +[[package]] +name = "toml" +version = "0.9.12+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf92845e79fc2e2def6a5d828f0801e29a2f8acc037becc5ab08595c7d5e9863" +dependencies = [ + "indexmap", + "serde_core", + "serde_spanned", + "toml_datetime", + "toml_parser", + "toml_writer", + "winnow 0.7.15", +] + +[[package]] +name = "toml_datetime" +version = "0.7.5+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "92e1cfed4a3038bc5a127e35a2d360f145e1f4b971b551a2ba5fd7aedf7e1347" +dependencies = [ + "serde_core", +] + +[[package]] +name = "toml_parser" +version = "1.1.5+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "baa693a8032d7e1cada7d0041e96126df243179ff061456783ac7f12bda4744c" +dependencies = [ + "winnow 1.0.4", +] + +[[package]] +name = "toml_writer" +version = "1.1.3+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06bdbd8cfc056b8d2e2e85f29b56a3bdbecb527cef81eb39e3e7b98af4652770" + [[package]] name = "typenum" version = "1.20.1" @@ -429,6 +512,18 @@ version = "0.11.1+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" +[[package]] +name = "winnow" +version = "0.7.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "df79d97927682d2fd8adb29682d1140b343be4ac0f08fd68b7765d9c059d3945" + +[[package]] +name = "winnow" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "23b97319f7b8343df12cc98938e5c3eb436064524c8d2b4e30a1d3a36eecdf81" + [[package]] name = "zeroize" version = "1.9.1" diff --git a/joulespec/joulespec-rs/Cargo.toml b/joulespec/joulespec-rs/Cargo.toml index bc2162fa8..46c218ef9 100644 --- a/joulespec/joulespec-rs/Cargo.toml +++ b/joulespec/joulespec-rs/Cargo.toml @@ -1,6 +1,6 @@ [workspace] resolver = "3" -members = ["crates/joulespec-core"] +members = ["crates/joulespec-core", "crates/joulespec-cli"] [workspace.package] edition = "2024" @@ -13,3 +13,4 @@ serde_json = "1" blake3 = "1" ed25519-dalek = { version = "2", features = ["rand_core"] } thiserror = "2" +toml = "0.9" diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml b/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml new file mode 100644 index 000000000..955107c7a --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml @@ -0,0 +1,23 @@ +[package] +name = "joulespec-cli" +version = "0.2.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 +repository.workspace = true + +[[bin]] +name = "joulespec" +path = "src/main.rs" + +[dependencies] +joulespec-core = { path = "../joulespec-core" } +serde = { workspace = true } +serde_json = { workspace = true } +toml = { workspace = true } +blake3 = { workspace = true } +ed25519-dalek = { workspace = true } +thiserror = { workspace = true } + +[lints.rust] +missing_docs = "warn" diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs new file mode 100644 index 000000000..c89ba5af7 --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs @@ -0,0 +1,439 @@ +//! Harvesting witnesses from a project's own test suite. +//! +//! The harvester does the bookkeeping a producer would otherwise do by hand: +//! read the clauses from the specification document, address the tree, run +//! each declared check, run it again against its counter-artifact, and emit a +//! signed witness at whatever rung the observations support. +//! +//! ## It reports what it could not establish +//! +//! Every declared mapping produces a [`Note`], including the ones that yielded +//! no witness. Two of those notes are the reason to run this at all: +//! +//! - [`Note::CounterDidNotFail`] — the check passed while the thing it is +//! supposed to be about was broken. That is a finding about the suite, not a +//! missing feature, and it is the only cheap way to discover an oracle that +//! cannot fail. +//! - [`Note::CheckDidNotRun`] — the name matched nothing. A harness reports +//! this as success, so without the count it reads as a passing check. +//! +//! ## Grades it can and cannot reach +//! +//! `E2` from a check observed to run and pass; `E3` when a counter-artifact +//! made it fail and the manifest stated an anchor. `E4` is out of reach here +//! by construction: it needs a discharged proof obligation and a formalization +//! someone independent cross-checked, neither of which a test runner can +//! produce (SPEC §2.6). + +use std::path::Path; + +use ed25519_dalek::SigningKey; +use joulespec_core::conform::ArtifactState; +use joulespec_core::evidence::{Anchor, Evidence, SignedWitness, Witness}; +use joulespec_core::spec::{Obligation, SignedSpec, Spec}; +use joulespec_core::{Energy, Provenance}; + +use crate::manifest::{Manifest, ManifestError}; +use crate::runner::{self, RunError}; +use crate::specdoc::{self, SpecDocError}; +use crate::tree::{Tree, TreeError}; + +/// Why a harvest could not complete. +#[derive(Debug, thiserror::Error)] +pub enum HarvestError { + /// The manifest is unusable. + #[error(transparent)] + Manifest(#[from] ManifestError), + /// The specification document is unusable. + #[error(transparent)] + SpecDoc(#[from] SpecDocError), + /// The tree is unreadable. + #[error(transparent)] + Tree(#[from] TreeError), + /// A check could not be run. + #[error(transparent)] + Run(#[from] RunError), + /// The core refused an artifact this harvester built. + #[error(transparent)] + Core(#[from] joulespec_core::Error), + /// The specification document could not be read. + #[error("cannot read specification document {path}: {source}")] + Io { + /// The path. + path: String, + /// The underlying error. + source: std::io::Error, + }, + /// The workspace did not build, so nothing can be observed about it. + #[error("the workspace does not build; no check can be observed")] + WorkspaceBroken, + /// The artifact state holds no parts, so every narrowed witness would be + /// stale and the whole measurement would be about nothing. + #[error("the manifest's artifact declares no files")] + EmptyArtifact, + /// The manifest named an anchor this profile does not define. + #[error("unknown anchor {0:?} (specification, state, or unstated)")] + BadAnchor(String), + /// The manifest claimed a measured energy grade the harvester cannot + /// support. + #[error("provenance {0:?} is not available to a harness with no meter")] + BadProvenance(String), +} + +/// What happened to one declared mapping. +#[derive(Debug, Clone)] +pub enum Note { + /// A witness was emitted. + Witnessed { + /// The clause. + clause: String, + /// The check. + check: String, + /// The rung reached. + grade: &'static str, + /// What was observed. + detail: String, + }, + /// The check did not run at all. + CheckDidNotRun { + /// The clause. + clause: String, + /// The check. + check: String, + }, + /// The check ran and did not pass, so it witnesses nothing. + CheckDidNotPass { + /// The clause. + clause: String, + /// The check. + check: String, + /// What was observed. + detail: String, + }, + /// **A finding.** The check passed while its subject was broken. + CounterDidNotFail { + /// The clause. + clause: String, + /// The check. + check: String, + /// What the mutation was supposed to break. + breaks: String, + }, + /// The counter-artifact did not compile, so nothing was demonstrated. + CounterInconclusive { + /// The clause. + clause: String, + /// The check. + check: String, + /// What was observed. + detail: String, + }, + /// No counter-artifact was declared, so the check cannot exceed `E2`. + NoCounterDeclared { + /// The clause. + clause: String, + /// The check. + check: 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 { .. }) + } + + /// A line for the report. + #[must_use] + pub fn line(&self) -> String { + match self { + Self::Witnessed { clause, check, grade, detail } => { + format!("{clause:<5} {grade} {check} ({detail})") + } + Self::CheckDidNotRun { clause, check } => { + format!("{clause:<5} -- {check}: NO TEST RAN -- the name matched nothing") + } + Self::CheckDidNotPass { clause, check, detail } => { + format!("{clause:<5} -- {check}: did not pass ({detail})") + } + Self::CounterDidNotFail { clause, check, breaks } => format!( + "{clause:<5} E2 {check}: FINDING -- passed while the counter-artifact \ + {breaks}; the check cannot see its subject" + ), + Self::CounterInconclusive { clause, check, detail } => format!( + "{clause:<5} E2 {check}: counter-artifact inconclusive ({detail})" + ), + Self::NoCounterDeclared { clause, check } => { + format!("{clause:<5} E2 {check}: no counter-artifact declared") + } + } + } +} + +/// The result of a harvest. +pub struct Outcome { + /// The specification, built from the document and signed. + pub spec: SignedSpec, + /// The artifact state the checks were run against. + pub state: ArtifactState, + /// The witnesses emitted. + pub witnesses: Vec, + /// What happened to every declared mapping, in manifest order. + pub notes: Vec, +} + +impl Outcome { + /// The notes that report something to act on. + #[must_use] + pub fn findings(&self) -> Vec<&Note> { + self.notes.iter().filter(|n| n.is_finding()).collect() + } +} + +fn anchor_of(name: &str) -> Result { + match name { + "specification" => Ok(Anchor::Specification), + "state" => Ok(Anchor::State), + "unstated" => Ok(Anchor::Unstated), + other => Err(HarvestError::BadAnchor(other.to_string())), + } +} + +fn provenance_of(name: &str) -> Result { + match name { + "estimator" => Ok(Provenance::Estimator), + "model-based" => Ok(Provenance::ModelBased), + // A harness that times a run and multiplies by a declared wattage has + // not read a counter, whatever the manifest would like to say. + other => Err(HarvestError::BadProvenance(other.to_string())), + } +} + +/// Microjoules for a run, from its wall-clock and the declared power. +fn microjoules(seconds: f64, watts: f64) -> u64 { + let uj = seconds.max(0.0) * watts.max(0.0) * 1_000_000.0; + if uj.is_finite() { uj as u64 } else { 0 } +} + +/// Harvest witnesses for one manifest. +pub fn harvest( + manifest_path: &str, + author: &SigningKey, + witness_key: &SigningKey, +) -> Result { + let manifest = Manifest::read(manifest_path)?; + let base = Path::new(manifest_path).parent().unwrap_or(Path::new(".")); + let workspace = base.join(&manifest.workspace); + let provenance = provenance_of(&manifest.energy.provenance)?; + + // ── the clauses, from the published document ──────────────────────── + let doc_path = base.join(&manifest.spec.document); + let document = std::fs::read_to_string(&doc_path).map_err(|source| HarvestError::Io { + path: doc_path.to_string_lossy().into_owned(), + source, + })?; + let items = specdoc::items( + &document, + &manifest.spec.section, + manifest.spec.expect_at_least, + )?; + let labels: Vec = items.iter().map(|i| i.label.clone()).collect(); + manifest.check_clauses(&labels)?; + + let spec = Spec::new( + manifest.spec.intent.clone(), + specdoc::clauses(&items), + author.verifying_key().to_bytes(), + ) + .sign(author)?; + let spec_id = spec.verify()?; + let by_label: std::collections::BTreeMap<&str, Obligation> = spec + .spec + .clauses + .iter() + .map(|c| Ok((c.label.as_str(), c.obligation()?))) + .collect::>()?; + + // ── the tree, and a warm build so a measurement times the check ───── + let tree = Tree::read( + &workspace, + &manifest.artifact.dirs, + &manifest.artifact.files, + &manifest.artifact.extensions, + )?; + if tree.is_empty() { + return Err(HarvestError::EmptyArtifact); + } + let state = tree.state(); + if !runner::warm(&workspace)? { + return Err(HarvestError::WorkspaceBroken); + } + + let mut witnesses = Vec::new(); + let mut notes = Vec::new(); + + for entry in &manifest.evidence { + let obligation = by_label + .get(entry.clause.as_str()) + .cloned() + .ok_or_else(|| ManifestError::UnknownClause(entry.clause.clone()))?; + let anchor = anchor_of(&entry.anchor)?; + let footprint = tree.footprint(&entry.footprint)?; + + let baseline = runner::run_check(&workspace, &entry.check)?; + if baseline.compiled && baseline.ran == 0 { + notes.push(Note::CheckDidNotRun { + clause: entry.clause.clone(), + check: entry.check.clone(), + }); + continue; + } + if !baseline.demonstrates_pass() { + notes.push(Note::CheckDidNotPass { + clause: entry.clause.clone(), + check: entry.check.clone(), + detail: baseline.describe(), + }); + continue; + } + + let mut uj = microjoules(baseline.seconds, manifest.energy.watts); + let mut evidence = Evidence::Exercised { check: entry.check.clone(), anchor }; + 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, + )?; + // Address the mutated tree while the mutation is in place, so + // the counter-artifact in the witness is the state that + // actually produced the failure. + let mutated = tree.reread( + &manifest.artifact.dirs, + &manifest.artifact.files, + &manifest.artifact.extensions, + )?; + (runner::run_check(&workspace, &entry.check)?, mutated.address()) + }; + uj = uj.saturating_add(microjoules(run.seconds, manifest.energy.watts)); + + if run.demonstrates_failure() { + evidence = Evidence::Falsifiable { + check: entry.check.clone(), + anchor, + counter: counter_address, + }; + note = Note::Witnessed { + clause: entry.clause.clone(), + check: entry.check.clone(), + grade: "E3", + detail: format!("failed when {}", counter.breaks), + }; + } else if !run.compiled { + note = Note::CounterInconclusive { + clause: entry.clause.clone(), + check: entry.check.clone(), + detail: run.describe(), + }; + } 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", + detail: "no counter-artifact declared".to_string(), + }; + } + + let witness = Witness::new( + spec_id.clone(), + obligation, + state.address.clone(), + evidence, + Energy::new(uj, provenance), + witness_key.verifying_key().to_bytes(), + ) + .with_footprint(footprint) + .sign(witness_key)?; + witnesses.push(witness); + notes.push(note); + } + + Ok(Outcome { spec, state, witnesses, notes }) +} + +/// A deterministic key from a single-byte seed. +/// +/// Published conformance vectors are signed with keys everyone has, so anyone +/// can reproduce the bytes. These are **not** secrets and a deployment must +/// not reuse them. +#[must_use] +pub fn vector_key(seed: u8) -> SigningKey { + SigningKey::from_bytes(&[seed; 32]) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn a_harness_with_no_meter_cannot_claim_a_reading() { + assert!(matches!(provenance_of("hw-shunt"), Err(HarvestError::BadProvenance(_)))); + assert_eq!(provenance_of("estimator").unwrap(), Provenance::Estimator); + assert_eq!(provenance_of("model-based").unwrap(), Provenance::ModelBased); + } + + #[test] + fn an_unknown_anchor_is_refused_rather_than_defaulted() { + assert!(matches!(anchor_of("vibes"), Err(HarvestError::BadAnchor(_)))); + assert_eq!(anchor_of("unstated").unwrap(), Anchor::Unstated); + } + + #[test] + fn microjoules_are_finite_and_monotone() { + assert_eq!(microjoules(1.0, 30.0), 30_000_000); + assert_eq!(microjoules(0.0, 30.0), 0); + assert_eq!(microjoules(-1.0, 30.0), 0, "a negative duration is not a credit"); + assert_eq!(microjoules(f64::INFINITY, 30.0), 0, "and an unbounded one is not a figure"); + assert!(microjoules(2.0, 30.0) > microjoules(1.0, 30.0)); + } + + #[test] + fn the_two_notes_worth_running_this_for_are_findings() { + let f = Note::CounterDidNotFail { + clause: "C1".into(), + check: "c".into(), + breaks: "the thing".into(), + }; + assert!(f.is_finding()); + assert!(f.line().contains("FINDING")); + + let r = Note::CheckDidNotRun { clause: "C1".into(), check: "c".into() }; + assert!(r.is_finding()); + assert!(r.line().contains("NO TEST RAN")); + + let ok = Note::Witnessed { + clause: "C1".into(), + check: "c".into(), + grade: "E3", + detail: "d".into(), + }; + assert!(!ok.is_finding()); + } +} diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs new file mode 100644 index 000000000..a70c60ce0 --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs @@ -0,0 +1,311 @@ +//! `joulespec` — the reference producer and checker. +//! +//! ```text +//! joulespec harvest --manifest --out [--require-grade E2|E3] +//! joulespec verify --receipt --steward --key +//! joulespec drift --from --to +//! ``` +//! +//! `harvest` reads the clauses from a published specification document, runs +//! each declared check, runs it again against its counter-artifact, emits +//! signed witnesses at the rung the observations support, evaluates them and +//! seals a `joulespec/1` receipt. +//! +//! It exits non-zero when it has a **finding** — a check that did not run, or +//! one that passed while its subject was broken — so a harvest can gate a +//! pipeline. `--require-grade` additionally fails the run when any owed +//! obligation falls below a bar. +//! +//! Normative: SPEC §2.4, SPEC §2.5, SPEC §3, SPEC §6. + +#![forbid(unsafe_code)] + +mod harvest; +mod manifest; +mod runner; +mod specdoc; +mod tree; + +use joulespec_core::evidence::{Attestation, Grade}; +use joulespec_core::spec::SignedSpec; +use joulespec_core::receipt; + +/// Parsed command line. +struct Args(std::collections::BTreeMap); + +impl Args { + fn parse(argv: &[String]) -> Self { + let mut map = std::collections::BTreeMap::new(); + let mut i = 0; + while i < argv.len() { + if let Some(name) = argv[i].strip_prefix("--") { + let value = argv.get(i + 1).filter(|v| !v.starts_with("--")); + match value { + Some(v) => { + map.insert(name.to_string(), v.clone()); + i += 2; + } + None => { + map.insert(name.to_string(), "true".to_string()); + i += 1; + } + } + } else { + i += 1; + } + } + Self(map) + } + + fn get(&self, name: &str) -> Option<&str> { + self.0.get(name).map(String::as_str) + } + + fn need(&self, name: &str) -> Result<&str, String> { + self.get(name).ok_or_else(|| format!("missing --{name}")) + } +} + +fn grade_of(code: &str) -> Result { + match code { + "E0" => Ok(Grade::Cited), + "E1" => Ok(Grade::Reviewed), + "E2" => Ok(Grade::Exercised), + "E3" => Ok(Grade::Falsifiable), + "E4" => Ok(Grade::Proved), + other => Err(format!("unknown grade {other:?} (E0..E4)")), + } +} + +fn hex32(s: &str) -> Result<[u8; 32], String> { + if s.len() != 64 { + return Err(format!("expected 64 hex characters, got {}", s.len())); + } + let mut out = [0u8; 32]; + for (i, byte) in out.iter_mut().enumerate() { + *byte = u8::from_str_radix(&s[i * 2..i * 2 + 2], 16) + .map_err(|_| "not hexadecimal".to_string())?; + } + Ok(out) +} + +fn cmd_harvest(args: &Args) -> Result { + let manifest = args.need("manifest")?; + let out = args.get("out"); + // Published vectors are signed with keys everyone holds, so the bytes are + // reproducible. A deployment passes its own. + let author = harvest::vector_key( + args.get("author-seed").map_or(Ok(1), |s| s.parse()).map_err(|_| "bad seed")?, + ); + let witness_key = harvest::vector_key( + args.get("witness-seed").map_or(Ok(2), |s| s.parse()).map_err(|_| "bad seed")?, + ); + let steward_key = harvest::vector_key( + args.get("steward-seed").map_or(Ok(3), |s| s.parse()).map_err(|_| "bad seed")?, + ); + + let outcome = harvest::harvest(manifest, &author, &witness_key).map_err(|e| e.to_string())?; + let m = manifest::Manifest::read(manifest).map_err(|e| e.to_string())?; + + println!("clauses {}", outcome.spec.spec.clauses.len()); + println!("artifact {}", outcome.state.address); + println!("parts {}", outcome.state.parts.len()); + println!("witnesses {}", outcome.witnesses.len()); + println!(); + for note in &outcome.notes { + println!(" {}", note.line()); + } + println!(); + + let (envelope, conformance) = receipt::seal( + &outcome.spec, + &outcome.state, + &outcome.witnesses, + &[], + &m.steward, + &steward_key, + ) + .map_err(|e| e.to_string())?; + + let grade = conformance.grade.map_or("--".to_string(), |g| g.code().to_string()); + let attestation = + conformance.attestation.map_or("absent".to_string(), |a| a.code().to_string()); + println!("grade {grade}"); + println!("attestation {attestation}"); + println!("open at E3 {}", conformance.open(Grade::Falsifiable).len()); + println!("flags {}", conformance.flags.len()); + println!("evidence {} uj", conformance.evidence_uj); + match conformance.uj_per_evidenced_clause(Grade::Falsifiable) { + Some(uj) => println!("uj/E3 clause {uj}"), + None => println!("uj/E3 clause absent (nothing reaches the bar)"), + } + + if let Some(dir) = out { + let dir = std::path::Path::new(dir); + std::fs::create_dir_all(dir).map_err(|e| e.to_string())?; + let write = |name: &str, bytes: &[u8]| -> Result<(), String> { + std::fs::write(dir.join(name), bytes).map_err(|e| format!("{name}: {e}")) + }; + let json = |v: &dyn erased::Json| -> Result { v.to_json() }; + write("spec.json", json(&outcome.spec)?.as_bytes())?; + write("witnesses.json", json(&outcome.witnesses)?.as_bytes())?; + write("state.json", json(&outcome.state)?.as_bytes())?; + write("receipt.cbor", &envelope)?; + write( + "receipt.json", + serde_json::to_string_pretty(&receipt::wire(&conformance, &m.steward)) + .map_err(|e| e.to_string())? + .as_bytes(), + )?; + println!("\nwrote {}", dir.display()); + } + + let findings = outcome.findings(); + if !findings.is_empty() { + eprintln!("\n{} finding(s):", findings.len()); + for f in &findings { + eprintln!(" {}", f.line()); + } + return Ok(2); + } + if let Some(bar) = args.get("require-grade") { + let bar = grade_of(bar)?; + if !conformance.is_conformant(bar, Attestation::SelfAttested) { + eprintln!("\nbelow the required bar {}", bar.code()); + for open in conformance.open(bar) { + eprintln!( + " {} {}", + open.label, + open.grade.map_or("unevidenced".to_string(), |g| g.code().to_string()) + ); + } + return Ok(3); + } + } + Ok(0) +} + +fn cmd_verify(args: &Args) -> Result { + let path = args.need("receipt")?; + let steward = args.need("steward")?; + let key = hex32(args.need("key")?)?; + let envelope = std::fs::read(path).map_err(|e| e.to_string())?; + let doc = receipt::verify(&envelope, steward, &key).map_err(|e| e.to_string())?; + println!("{}", serde_json::to_string_pretty(&doc).map_err(|e| e.to_string())?); + Ok(0) +} + +fn cmd_drift(args: &Args) -> Result { + let read = |p: &str| -> Result { + let text = std::fs::read_to_string(p).map_err(|e| format!("{p}: {e}"))?; + serde_json::from_str(&text).map_err(|e| format!("{p}: {e}")) + }; + let from = read(args.need("from")?)?; + let to = read(args.need("to")?)?; + let d = joulespec_core::drift::diff(&from, &to).map_err(|e| e.to_string())?; + + println!("chained {}", d.chained); + println!("editorial {}", d.is_editorial()); + println!("kept {}", d.kept.len()); + println!("relabelled {}", d.relabelled.len()); + println!("reworded {}", d.reworded.len()); + println!("added {}", d.added.len()); + println!("removed {}", d.removed.len()); + println!("invalidated {}", d.invalidated().len()); + println!("unevidenced {}", d.unevidenced().len()); + for r in &d.reworded { + println!(" reworded {} — evidence for the old wording no longer applies", r.label); + } + for r in &d.relabelled { + println!(" relabelled {} -> {} — editorial, no evidence lost", r.was, r.now); + } + Ok(0) +} + +/// Serialising without naming every concrete type at each call site. +mod erased { + pub trait Json { + fn to_json(&self) -> Result; + } + + impl Json for T { + fn to_json(&self) -> Result { + serde_json::to_string_pretty(self).map_err(|e| e.to_string()) + } + } +} + +const USAGE: &str = "\ +joulespec — the reference producer and checker for joulespec/1 + + joulespec harvest --manifest [--out ] [--require-grade E0..E4] + [--author-seed N] [--witness-seed N] [--steward-seed N] + joulespec verify --receipt --steward --key <64 hex chars> + joulespec drift --from --to + +harvest exits 2 when it has a finding (a check that did not run, or one that +passed while its subject was broken) and 3 when an owed obligation falls below +--require-grade. +"; + +fn main() { + let argv: Vec = std::env::args().skip(1).collect(); + let command = argv.first().cloned().unwrap_or_default(); + let args = Args::parse(&argv); + let result = match command.as_str() { + "harvest" => cmd_harvest(&args), + "verify" => cmd_verify(&args), + "drift" => cmd_drift(&args), + "" | "help" | "--help" | "-h" => { + print!("{USAGE}"); + Ok(0) + } + other => Err(format!("unknown command {other:?}\n\n{USAGE}")), + }; + match result { + Ok(code) => std::process::exit(code), + Err(message) => { + eprintln!("joulespec: {message}"); + std::process::exit(1); + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn arguments_parse_as_flags_and_values() { + let argv: Vec = ["harvest", "--manifest", "a.toml", "--require-grade", "E3"] + .iter() + .map(|s| (*s).to_string()) + .collect(); + let args = Args::parse(&argv); + assert_eq!(args.get("manifest"), Some("a.toml")); + assert_eq!(args.get("require-grade"), Some("E3")); + assert!(args.need("missing").is_err()); + } + + #[test] + fn a_valueless_flag_reads_as_set() { + let argv: Vec = ["harvest", "--dry-run"].iter().map(|s| (*s).to_string()).collect(); + assert_eq!(Args::parse(&argv).get("dry-run"), Some("true")); + } + + #[test] + fn grades_round_trip_their_codes() { + for code in ["E0", "E1", "E2", "E3", "E4"] { + assert_eq!(grade_of(code).unwrap().code(), code); + } + assert!(grade_of("E9").is_err()); + } + + #[test] + fn a_key_must_be_exactly_thirty_two_bytes_of_hex() { + assert_eq!(hex32(&"00".repeat(32)).unwrap(), [0u8; 32]); + assert_eq!(hex32(&"ff".repeat(32)).unwrap(), [255u8; 32]); + assert!(hex32("00").is_err(), "a short key must not be padded"); + assert!(hex32(&"zz".repeat(32)).is_err()); + } +} diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs new file mode 100644 index 000000000..e612e7c89 --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs @@ -0,0 +1,287 @@ +//! The harvest manifest: what the operator declares, and what is computed. +//! +//! The division of labour here is the whole point of the file. Three things +//! are human judgements and are **declared**: +//! +//! - which check stands for which obligation — the mapping prose to code that +//! this standard refuses to guess, for the same reason it never formalizes a +//! clause (SPEC §2.6); +//! - where a check's expected values come from — its anchor, which the author +//! of the check knows and nobody else can see (SPEC §2.5); +//! - which inputs the check depends on — its footprint, since a test harness +//! that cannot observe its own reads must not guess (SPEC §8). +//! +//! Everything else is computed: clause text and obligation addresses from the +//! specification document, part addresses from the tree, grades from the +//! evidence, attestation from authorship, and the receipt from all of it. + +use serde::{Deserialize, Serialize}; + +/// Why a manifest could not be used. +#[derive(Debug, thiserror::Error)] +pub enum ManifestError { + /// The file could not be read. + #[error("cannot read manifest {path}: {source}")] + Io { + /// The path given. + path: String, + /// The underlying error. + source: std::io::Error, + }, + /// The file is not valid TOML, or does not match this schema. + #[error("manifest is not a joulespec harvest manifest: {0}")] + Parse(#[from] toml::de::Error), + /// An evidence entry names a clause the specification does not state. + #[error("evidence names clause {0:?}, which the specification does not state")] + UnknownClause(String), + /// Two evidence entries name the same clause and check. + #[error("duplicate evidence for clause {clause:?} check {check:?}")] + DuplicateEvidence { + /// The clause. + clause: String, + /// The check. + check: String, + }, + /// No evidence at all. Harvesting nothing and sealing a receipt is the + /// failure this standard exists to surface. + #[error("the manifest declares no evidence")] + NoEvidence, +} + +/// Where the clauses come from. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct SpecSource { + /// Path to the specification document, relative to the manifest. + pub document: String, + /// The section heading to read, as the document writes it. + pub section: String, + /// The floor on item count. A parser that matched nothing would otherwise + /// report success having checked nothing. + pub expect_at_least: usize, + /// The specification's intent, in the operator's words. + pub intent: String, +} + +/// Which files make up the artifact state. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct ArtifactSource { + /// Directories to walk, relative to the workspace. + #[serde(default)] + pub dirs: Vec, + /// Individual files to include. + #[serde(default)] + pub files: Vec, + /// Extensions to keep while walking. + pub extensions: Vec, +} + +/// How a run's energy is turned into microjoules. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct EnergySource { + /// The platform's power draw while running checks. + pub watts: f64, + /// The honest grade of that figure: `estimator` for a declared default, + /// `model-based` for a curve this host calibrated. A harness with no + /// meter MUST NOT claim `hw-shunt`. + pub provenance: String, +} + +/// A counter-artifact: an edit that should make the check fail. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Counter { + /// The file to edit, relative to the workspace. + pub file: String, + /// The exact text to replace. It must occur exactly once, so a mutation + /// cannot silently hit the wrong place or nothing at all. + pub find: String, + /// What to put there. + pub replace: String, + /// What the mutation breaks, for the report. + pub breaks: String, +} + +/// One declared mapping from an obligation to a check. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Evidence { + /// The clause label, as the specification document writes it. + pub clause: String, + /// The check's exact test path. + pub check: String, + /// Where the check's expected values come from: `specification`, `state`, + /// or `unstated`. + pub anchor: String, + /// The inputs the check depends on, as workspace-relative paths. + #[serde(default)] + pub footprint: Vec, + /// The counter-artifact that should make it fail. Without one the check + /// cannot exceed `E2` however carefully it was written. + pub counter: Option, +} + +/// The whole manifest. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Manifest { + /// Where to run cargo, relative to the manifest. + pub workspace: String, + /// The steward sealing the receipt. + pub steward: String, + /// Where the clauses come from. + pub spec: SpecSource, + /// Which files make up the artifact state. + pub artifact: ArtifactSource, + /// How to price a run. + pub energy: EnergySource, + /// The declared mappings. + #[serde(default, rename = "evidence")] + pub evidence: Vec, +} + +impl Manifest { + /// Read and structurally validate a manifest. + pub fn read(path: &str) -> Result { + let text = std::fs::read_to_string(path) + .map_err(|source| ManifestError::Io { path: path.to_string(), source })?; + let manifest: Self = toml::from_str(&text)?; + if manifest.evidence.is_empty() { + return Err(ManifestError::NoEvidence); + } + let mut seen = std::collections::BTreeSet::new(); + for e in &manifest.evidence { + if !seen.insert((e.clause.as_str(), e.check.as_str())) { + return Err(ManifestError::DuplicateEvidence { + clause: e.clause.clone(), + check: e.check.clone(), + }); + } + } + Ok(manifest) + } + + /// Check every evidence entry names a clause the specification states. + /// + /// An entry for an unknown clause would otherwise become an `unbound` + /// flag at evaluation — a correct outcome, but one the operator should + /// hear about before a receipt is sealed rather than after. + pub fn check_clauses(&self, labels: &[String]) -> Result<(), ManifestError> { + for e in &self.evidence { + if !labels.iter().any(|l| l == &e.clause) { + return Err(ManifestError::UnknownClause(e.clause.clone())); + } + } + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + const MANIFEST: &str = r#" +workspace = "." +steward = "did:key:zExample" + +[spec] +document = "../SPEC.md" +section = "7. Conformance" +expect_at_least = 11 +intent = "The reference implementation does what the specification says." + +[artifact] +dirs = ["crates"] +extensions = ["rs"] + +[energy] +watts = 30.0 +provenance = "estimator" + +[[evidence]] +clause = "C1" +check = "spec::tests::relabelling_a_clause_moves_no_obligation" +anchor = "specification" +footprint = ["crates/joulespec-core/src/spec.rs"] + +[evidence.counter] +file = "crates/joulespec-core/src/spec.rs" +find = "\"kind\": self.kind.label(), \"text\": self.text" +replace = "\"label\": self.label, \"kind\": self.kind.label(), \"text\": self.text" +breaks = "puts the label back into the obligation address" +"#; + + fn write(text: &str) -> (tempdir::Dir, String) { + let dir = tempdir::Dir::new(); + let path = dir.path().join("harvest.toml"); + std::fs::write(&path, text).unwrap(); + (dir, path.to_string_lossy().into_owned()) + } + + #[test] + fn a_manifest_round_trips_its_declared_fields() { + let (_d, path) = write(MANIFEST); + let m = Manifest::read(&path).expect("parses"); + assert_eq!(m.spec.expect_at_least, 11); + assert_eq!(m.evidence.len(), 1); + assert_eq!(m.evidence[0].anchor, "specification"); + let counter = m.evidence[0].counter.as_ref().expect("counter"); + assert!(counter.replace.contains("\"label\"")); + assert_eq!(m.energy.provenance, "estimator"); + } + + #[test] + fn a_manifest_with_no_evidence_is_refused() { + let text = MANIFEST.split("[[evidence]]").next().unwrap(); + let (_d, path) = write(text); + assert!(matches!(Manifest::read(&path), Err(ManifestError::NoEvidence))); + } + + #[test] + fn duplicate_evidence_is_refused() { + let entry = &MANIFEST[MANIFEST.find("[[evidence]]").unwrap()..]; + let text = format!("{MANIFEST}{entry}"); + let (_d, path) = write(&text); + assert!(matches!( + Manifest::read(&path), + Err(ManifestError::DuplicateEvidence { .. }) + )); + } + + #[test] + fn evidence_for_an_unstated_clause_is_caught_before_sealing() { + let (_d, path) = write(MANIFEST); + let m = Manifest::read(&path).unwrap(); + assert!(m.check_clauses(&["C1".to_string()]).is_ok()); + assert!(matches!( + m.check_clauses(&["C2".to_string()]), + Err(ManifestError::UnknownClause(c)) if c == "C1" + )); + } + + /// A directory that removes itself, so the tests need no dev-dependency. + mod tempdir { + use std::path::{Path, PathBuf}; + + pub struct Dir(PathBuf); + + impl Dir { + pub fn new() -> Self { + let unique = format!( + "joulespec-manifest-test-{}-{:?}", + std::process::id(), + std::thread::current().id() + ); + let path = std::env::temp_dir().join(unique.replace(['(', ')'], "")); + std::fs::create_dir_all(&path).expect("temp dir"); + Self(path) + } + + pub fn path(&self) -> &Path { + &self.0 + } + } + + impl Drop for Dir { + fn drop(&mut self) { + let _ = std::fs::remove_dir_all(&self.0); + } + } + } +} diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/runner.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/runner.rs new file mode 100644 index 000000000..03074ce64 --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/runner.rs @@ -0,0 +1,316 @@ +//! Running a check, and running it against a counter-artifact. +//! +//! ## What counts as having run +//! +//! A test harness that filters to a name nothing matches prints `running 0 +//! tests`, reports success, and exits zero. Taking that as evidence is the +//! exact failure this standard exists to surface, so a [`Run`] carries the +//! number of tests observed to run and a caller must check it. A check that +//! did not run is not a check that passed. +//! +//! ## What counts as having failed +//! +//! For a counter-artifact the distinction matters more, because three +//! different things look like "the check did not pass": +//! +//! | Outcome | Meaning | +//! |---|---| +//! | ran and failed | The check can fail. This is the `E3` evidence. | +//! | did not compile | The mutation broke the build. The check never ran, so nothing was demonstrated. | +//! | ran and passed | **A finding**: the check cannot see the thing it is supposed to be about. | +//! +//! Conflating the second with the first would manufacture `E3` evidence out of +//! a syntax error, which is the most misleading possible result — so +//! [`Run::demonstrates_failure`] requires a test to have run *and* failed. + +use std::path::{Path, PathBuf}; +use std::process::Command; +use std::time::Instant; + +/// Why a check could not be run. +#[derive(Debug, thiserror::Error)] +pub enum RunError { + /// cargo could not be launched. + #[error("cannot run cargo in {dir}: {source}")] + Spawn { + /// The working directory. + dir: PathBuf, + /// The underlying error. + source: std::io::Error, + }, + /// A file could not be read or written while mutating. + #[error("cannot mutate {path}: {source}")] + Mutate { + /// The file. + path: PathBuf, + /// The underlying error. + source: std::io::Error, + }, + /// The text to replace does not occur exactly once. + #[error("{path}: the text to replace occurs {found} times, not once")] + NotUnique { + /// The file. + path: PathBuf, + /// How many times it was found. + found: usize, + }, +} + +/// The observed outcome of one check run. +#[derive(Debug, Clone, PartialEq)] +pub struct Run { + /// How many tests the harness reported running. + pub ran: usize, + /// Whether the named check reported `ok`. + pub passed: bool, + /// Whether the named check reported `FAILED`. + pub failed: bool, + /// Whether the workspace compiled at all. + pub compiled: bool, + /// Wall-clock seconds for the run. + pub seconds: f64, +} + +impl Run { + /// Whether this run is evidence that the check passes. + #[must_use] + pub fn demonstrates_pass(&self) -> bool { + self.compiled && self.ran >= 1 && self.passed && !self.failed + } + + /// Whether this run is evidence that the check *can fail*. + /// + /// A build that did not compile does not qualify: the check never ran, so + /// nothing about it was demonstrated. + #[must_use] + pub fn demonstrates_failure(&self) -> bool { + self.compiled && self.ran >= 1 && self.failed + } + + /// A one-line account for the report. + #[must_use] + pub fn describe(&self) -> String { + if !self.compiled { + return "did not compile".to_string(); + } + if self.ran == 0 { + return "no test ran (the name matched nothing)".to_string(); + } + match (self.passed, self.failed) { + (true, false) => format!("ran {} and passed", self.ran), + (false, true) => format!("ran {} and failed", self.ran), + _ => format!("ran {}, outcome unclear", self.ran), + } + } +} + +fn parse(check: &str, output: &str, seconds: f64) -> Run { + let compiled = !output.contains("could not compile") + && !output.contains("error: expected") + && !output.contains("error[E"); + let mut ran = 0usize; + let mut passed = false; + let mut failed = false; + for line in output.lines() { + let line = line.trim(); + if let Some(rest) = line.strip_prefix("running ") + && let Some(n) = rest.split_whitespace().next() + { + ran += n.parse::().unwrap_or(0); + } + // `test some::path::name ... ok` — match the exact name, so a + // differently-named test passing nearby cannot stand in for this one. + if let Some(rest) = line.strip_prefix("test ") + && let Some(result) = rest.strip_prefix(check) + { + let result = result.trim_start_matches([' ', '.']); + if result.starts_with("ok") { + passed = true; + } else if result.starts_with("FAILED") { + failed = true; + } + } + } + Run { ran, passed, failed, compiled, seconds } +} + +/// Build the test binaries without running anything, so a later measurement +/// times the check rather than the compiler. +pub fn warm(workspace: &Path) -> Result { + let out = Command::new("cargo") + .args(["test", "--workspace", "--no-run"]) + .current_dir(workspace) + .output() + .map_err(|source| RunError::Spawn { dir: workspace.to_path_buf(), source })?; + Ok(out.status.success()) +} + +/// Run exactly one check and report what was observed. +pub fn run_check(workspace: &Path, check: &str) -> Result { + let started = Instant::now(); + let out = Command::new("cargo") + .args(["test", "--workspace", "--", "--exact", check]) + .current_dir(workspace) + .output() + .map_err(|source| RunError::Spawn { dir: workspace.to_path_buf(), source })?; + let seconds = started.elapsed().as_secs_f64(); + let mut text = String::from_utf8_lossy(&out.stdout).into_owned(); + text.push('\n'); + text.push_str(&String::from_utf8_lossy(&out.stderr)); + Ok(parse(check, &text, seconds)) +} + +/// A file edit that restores itself. +/// +/// The revert runs on drop, so an error or a panic between apply and revert +/// still leaves the tree as it was found. A harvester that left a mutation in +/// place would poison every later measurement in the run. +pub struct Mutation { + path: PathBuf, + original: String, +} + +impl Mutation { + /// Apply a single-occurrence replacement. + pub fn apply(workspace: &Path, file: &str, find: &str, replace: &str) + -> Result + { + let path = workspace.join(file); + let original = std::fs::read_to_string(&path) + .map_err(|source| RunError::Mutate { path: path.clone(), source })?; + let found = original.matches(find).count(); + if found != 1 { + return Err(RunError::NotUnique { path, found }); + } + let mutated = original.replace(find, replace); + std::fs::write(&path, &mutated) + .map_err(|source| RunError::Mutate { path: path.clone(), source })?; + Ok(Self { path, original }) + } +} + +impl Drop for Mutation { + fn drop(&mut self) { + // Best effort by necessity: there is nowhere to report an error from + // a destructor. A failure here is visible immediately, because the + // working tree stays dirty. + let _ = std::fs::write(&self.path, &self.original); + } +} + +#[cfg(test)] +mod tests { + use super::*; + + const PASS: &str = "\ + Compiling joulespec-core v0.2.0 + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.42s + Running unittests src/lib.rs + +running 1 test +test spec::tests::relabelling_a_clause_moves_no_obligation ... ok + +test result: ok. 1 passed; 0 failed; 0 ignored; 63 filtered out + Running unittests src/main.rs + +running 0 tests + +test result: ok. 0 passed; 0 failed +"; + + const FAIL: &str = "\ +running 1 test +test spec::tests::relabelling_a_clause_moves_no_obligation ... FAILED + +failures: + spec::tests::relabelling_a_clause_moves_no_obligation + +test result: FAILED. 0 passed; 1 failed; 0 ignored; 63 filtered out +"; + + const NOTHING_MATCHED: &str = "\ +running 0 tests + +test result: ok. 0 passed; 0 failed; 0 ignored; 64 filtered out +"; + + const BROKEN: &str = "\ +error[E0425]: cannot find value `labl` in this scope +error: could not compile `joulespec-core` (lib) due to 1 previous error +"; + + const CHECK: &str = "spec::tests::relabelling_a_clause_moves_no_obligation"; + + #[test] + fn a_passing_run_is_recognised_and_counted() { + let r = parse(CHECK, PASS, 0.4); + assert_eq!(r.ran, 1, "the 0-test binaries add nothing"); + assert!(r.demonstrates_pass()); + assert!(!r.demonstrates_failure()); + } + + #[test] + fn a_failing_run_demonstrates_that_the_check_can_fail() { + let r = parse(CHECK, FAIL, 0.4); + assert!(r.demonstrates_failure()); + assert!(!r.demonstrates_pass()); + assert_eq!(r.describe(), "ran 1 and failed"); + } + + #[test] + fn a_run_where_nothing_matched_is_not_a_pass() { + // `running 0 tests` with `test result: ok` and exit status zero: the + // shape of every check that silently stopped checking. + let r = parse(CHECK, NOTHING_MATCHED, 0.1); + assert_eq!(r.ran, 0); + assert!(!r.demonstrates_pass(), "exit zero having done nothing is not evidence"); + assert!(!r.demonstrates_failure()); + assert_eq!(r.describe(), "no test ran (the name matched nothing)"); + } + + #[test] + fn a_mutation_that_breaks_the_build_demonstrates_nothing() { + let r = parse(CHECK, BROKEN, 0.2); + assert!(!r.compiled); + assert!( + !r.demonstrates_failure(), + "manufacturing E3 evidence from a syntax error would be the worst possible result" + ); + assert_eq!(r.describe(), "did not compile"); + } + + #[test] + fn another_tests_result_cannot_stand_in_for_this_one() { + let other = "running 1 test\ntest spec::tests::something_else ... ok\n"; + let r = parse(CHECK, other, 0.1); + assert_eq!(r.ran, 1); + assert!(!r.passed, "the name must match exactly"); + assert!(!r.demonstrates_pass()); + } + + #[test] + fn a_mutation_reverts_itself_and_refuses_an_ambiguous_target() { + let dir = std::env::temp_dir().join(format!("joulespec-mutation-{}", std::process::id())); + std::fs::create_dir_all(&dir).unwrap(); + let file = "subject.rs"; + let path = dir.join(file); + std::fs::write(&path, "let a = 1;\nlet b = 2;\n").unwrap(); + + { + let _m = Mutation::apply(&dir, file, "let a = 1;", "let a = 99;").expect("applies"); + assert!(std::fs::read_to_string(&path).unwrap().contains("99")); + } + assert_eq!( + std::fs::read_to_string(&path).unwrap(), + "let a = 1;\nlet b = 2;\n", + "the revert runs on drop, so a panic cannot leave the tree mutated" + ); + + std::fs::write(&path, "x;\nx;\n").unwrap(); + assert!(matches!( + Mutation::apply(&dir, file, "x;", "y;"), + Err(RunError::NotUnique { found: 2, .. }) + )); + let _ = std::fs::remove_dir_all(&dir); + } +} diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs new file mode 100644 index 000000000..3710b1720 --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs @@ -0,0 +1,291 @@ +//! Clauses parsed from a published specification document. +//! +//! The alternative — copying clause text into the manifest — puts the +//! obligations in two places, and the one an auditor reads is not the one the +//! evidence binds to. Parsing the document means the manifest **cannot** drift +//! from the specification: reword a conformance item and its obligation +//! 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 +//! named section, which is how this family's specifications write their +//! conformance lists: +//! +//! ```text +//! ## 7. Conformance +//! +//! 1. **C1 — Addressing.** Obligation addresses are computed over `{kind, +//! text}` with the label excluded. +//! 2. **C2 — Validation.** Specifications with a duplicate label are refused. +//! ``` +//! +//! Continuation lines are joined with single spaces, so re-wrapping a +//! paragraph does not change the obligation while editing a word does. +//! Without that normalisation the standard would punish `fmt`, and a standard +//! that punishes formatting teaches people to avoid it. + +use joulespec_core::spec::{Clause, ClauseKind}; + +/// Why a specification document could not be read as clauses. +#[derive(Debug, thiserror::Error)] +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), + /// Fewer items than the caller said to expect. + #[error("expected at least {expected} items in section {section:?}, found {found}")] + TooFew { + /// What the caller required. + expected: usize, + /// What the parser found. + found: usize, + /// The section searched. + section: String, + }, + /// Two items share a label. + #[error("duplicate item label {0:?}")] + DuplicateLabel(String), +} + +/// One parsed conformance item. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Item { + /// The label, as the document writes it (`"C1"`). + pub label: String, + /// The item's short name (`"Addressing"`). + pub name: String, + /// The requirement text, re-wrapped to one line. + pub text: String, +} + +fn is_section_heading(line: &str, section: &str) -> bool { + let t = line.trim_start(); + if !t.starts_with('#') { + return false; + } + let body = t.trim_start_matches('#').trim(); + body == section || body.starts_with(&format!("{section} ")) +} + +/// Split `**C1 — Addressing.** rest…` into its three parts. +/// +/// The em dash is required: it is what distinguishes a labelled conformance +/// item from an ordinary bolded sentence in a numbered list. +fn split_item(body: &str) -> Option<(String, String, String)> { + let rest = body.strip_prefix("**")?; + let (head, tail) = rest.split_once("**")?; + let (label, name) = head.split_once(" — ")?; + let name = name.trim().trim_end_matches('.'); + if label.trim().is_empty() || name.is_empty() { + return None; + } + Some((label.trim().to_string(), name.to_string(), tail.trim().to_string())) +} + +/// Parse the numbered items of one section. +/// +/// `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. +pub fn items( + document: &str, + section: &str, + expect_at_least: usize, +) -> Result, SpecDocError> { + let mut lines = document.lines(); + let mut found_section = false; + for line in lines.by_ref() { + if is_section_heading(line, section) { + found_section = true; + break; + } + } + if !found_section { + return Err(SpecDocError::NoSection(section.to_string())); + } + + 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)) => { + if let Some(item) = pending.take() { + out.push(item); + } + if let Some((label, name, text)) = split_item(body) { + pending = Some(Item { label, name, text }); + } + } + None if pending.is_some() => { + let continuation = line.trim(); + if continuation.is_empty() { + if 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(' '); + item.text.push_str(continuation); + } + } + None => {} + } + } + if let Some(item) = pending { + out.push(item); + } + + if out.is_empty() { + return Err(SpecDocError::NoItems(section.to_string())); + } + if out.len() < expect_at_least { + return Err(SpecDocError::TooFew { + expected: expect_at_least, + found: out.len(), + section: section.to_string(), + }); + } + let mut seen = std::collections::BTreeSet::new(); + for item in &out { + if !seen.insert(item.label.as_str()) { + return Err(SpecDocError::DuplicateLabel(item.label.clone())); + } + } + Ok(out) +} + +/// The clauses of a parsed section: each item is a requirement whose text is +/// its name and body, so the obligation covers both. +#[must_use] +pub fn clauses(items: &[Item]) -> Vec { + items + .iter() + .map(|i| { + Clause::new( + i.label.clone(), + ClauseKind::Requirement, + format!("{} — {}", i.name, i.text), + ) + }) + .collect() +} + +#[cfg(test)] +mod tests { + use super::*; + + const DOC: &str = "\ +# A Standard + +## 6. Something else + +1. **X1 — Decoy.** Not in the section we asked for. + +## 7. Conformance + +An implementation conforms when: + +1. **C1 — Addressing.** Obligation addresses are computed over `{kind, text}` + with the label excluded; relabelling preserves an address. +2. **C2 — Validation.** Specifications with a duplicate label are refused. +10. **C10 — Demonstrated failure.** No evidence reaches `E3` without a killed + counter-artifact. + +The reference implementation is conformant by construction. + +## 8. The honest limit + +1. **Z1 — Decoy.** After the section ends. +"; + + #[test] + fn items_are_read_from_the_named_section_only() { + let got = items(DOC, "7. Conformance", 3).expect("parses"); + assert_eq!(got.len(), 3, "{got:#?}"); + assert_eq!(got[0].label, "C1"); + assert_eq!(got[0].name, "Addressing"); + assert_eq!(got[2].label, "C10", "a two-digit item and its deeper indent"); + } + + #[test] + fn continuation_lines_join_with_one_space() { + let got = items(DOC, "7. Conformance", 3).unwrap(); + assert_eq!( + got[0].text, + "Obligation addresses are computed over `{kind, text}` with the label excluded; \ + relabelling preserves an address." + ); + assert!(!got[0].text.contains(" "), "re-wrapping must not change the obligation"); + } + + #[test] + fn a_reworded_item_is_a_different_obligation_but_a_rewrapped_one_is_not() { + let rewrapped = DOC.replace( + "1. **C1 — Addressing.** Obligation addresses are computed over `{kind, text}`\n with the label excluded; relabelling preserves an address.", + "1. **C1 — Addressing.** Obligation addresses are computed over\n `{kind, text}` with the label excluded; relabelling\n preserves an address.", + ); + 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()); + + assert_eq!( + base[0].obligation().unwrap(), + wrapped[0].obligation().unwrap(), + "a standard that punished re-wrapping would teach people to avoid fmt" + ); + assert_ne!( + base[0].obligation().unwrap(), + changed[0].obligation().unwrap(), + "one changed word is a changed obligation" + ); + } + + #[test] + fn a_missing_section_is_an_error_not_an_empty_list() { + assert!(matches!(items(DOC, "99. Nowhere", 1), 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(_)))); + } + + #[test] + fn finding_fewer_items_than_expected_fails_closed() { + // 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(); + 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(_)))); + } + + #[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")); + } +} diff --git a/joulespec/joulespec-rs/crates/joulespec-cli/src/tree.rs b/joulespec/joulespec-rs/crates/joulespec-cli/src/tree.rs new file mode 100644 index 000000000..aaeb5c5da --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-cli/src/tree.rs @@ -0,0 +1,204 @@ +//! The artifact state of a source tree, and the addresses its footprints use. +//! +//! A part address covers a file's **path and its contents**, so a file renamed +//! without being edited is a different part. That is the conservative +//! direction: moving code can change what it means, and a footprint that +//! followed content across renames would keep evidence alive through a +//! refactor the evidence never saw. +//! +//! The whole-state address covers the canonical list of parts, so any edit +//! anywhere moves it — which is exactly why footprints exist (SPEC §2.4). + +use std::path::{Path, PathBuf}; + +use joulespec_core::Address; +use joulespec_core::conform::ArtifactState; + +/// Why a tree could not be read. +#[derive(Debug, thiserror::Error)] +pub enum TreeError { + /// A declared path is missing, unreadable, or outside the root. + #[error("cannot read {path}: {source}")] + Io { + /// The offending path. + path: PathBuf, + /// The underlying error. + source: std::io::Error, + }, + /// A declared directory held no files, so the state would be empty. + #[error("{0} contains no files with a listed extension")] + Empty(PathBuf), + /// A footprint names a path the state does not contain. Silently dropping + /// it would produce a witness whose footprint is narrower than declared. + #[error("footprint path {0} is not part of the artifact state")] + NotInState(String), +} + +/// A source tree read as an addressable state. +#[derive(Debug, Clone)] +pub struct Tree { + root: PathBuf, + /// Repository-relative path to the part's address, in sorted order. + parts: std::collections::BTreeMap, +} + +/// The address of one part: its path and its contents together. +fn part_address(rel: &str, contents: &[u8]) -> Address { + let mut buf = Vec::with_capacity(rel.len() + 1 + contents.len()); + buf.extend_from_slice(rel.as_bytes()); + buf.push(0); + buf.extend_from_slice(contents); + Address::of_bytes(&buf) +} + +impl Tree { + /// Read every file under `dirs` whose extension is listed, plus `files`. + pub fn read( + root: &Path, + dirs: &[String], + files: &[String], + extensions: &[String], + ) -> Result { + let mut parts = std::collections::BTreeMap::new(); + for dir in dirs { + let before = parts.len(); + walk(root, &root.join(dir), extensions, &mut parts)?; + if parts.len() == before { + return Err(TreeError::Empty(PathBuf::from(dir))); + } + } + for file in files { + let path = root.join(file); + let contents = std::fs::read(&path) + .map_err(|source| TreeError::Io { path: path.clone(), source })?; + parts.insert(file.clone(), part_address(file, &contents)); + } + Ok(Self { root: root.to_path_buf(), parts }) + } + + /// Re-read the tree from disk — used to address a mutated state. + pub fn reread(&self, dirs: &[String], files: &[String], extensions: &[String]) + -> Result + { + Self::read(&self.root, dirs, files, extensions) + } + + /// The evaluable state: the whole-tree address plus every part. + #[must_use] + pub fn state(&self) -> ArtifactState { + ArtifactState::new(self.address(), self.parts.values().cloned()) + } + + /// The whole-tree address: the canonical list of `path address` lines. + #[must_use] + pub fn address(&self) -> Address { + let mut buf = Vec::new(); + for (path, address) in &self.parts { + buf.extend_from_slice(path.as_bytes()); + buf.push(b' '); + buf.extend_from_slice(address.as_str().as_bytes()); + buf.push(b'\n'); + } + Address::of_bytes(&buf) + } + + /// The addresses of the named paths, for a witness footprint. + /// + /// A path the state does not hold is an error rather than an omission: a + /// footprint quietly narrowed by a typo would outlive changes to the file + /// the author meant to name. + pub fn footprint(&self, paths: &[String]) -> Result, TreeError> { + paths + .iter() + .map(|p| { + self.parts + .get(p) + .cloned() + .ok_or_else(|| TreeError::NotInState(p.clone())) + }) + .collect() + } + + /// Whether the state holds no parts. + #[must_use] + pub fn is_empty(&self) -> bool { + self.parts.is_empty() + } +} + +fn walk( + root: &Path, + dir: &Path, + extensions: &[String], + out: &mut std::collections::BTreeMap, +) -> Result<(), TreeError> { + let entries = std::fs::read_dir(dir) + .map_err(|source| TreeError::Io { path: dir.to_path_buf(), source })?; + let mut sorted: Vec = Vec::new(); + for entry in entries { + let entry = entry.map_err(|source| TreeError::Io { path: dir.to_path_buf(), source })?; + sorted.push(entry.path()); + } + sorted.sort(); + for path in sorted { + if path.is_dir() { + if path.file_name().is_some_and(|n| n == "target") { + continue; + } + walk(root, &path, extensions, out)?; + continue; + } + let keep = path + .extension() + .and_then(|e| e.to_str()) + .is_some_and(|e| extensions.iter().any(|want| want == e)); + if !keep { + continue; + } + let rel = path + .strip_prefix(root) + .unwrap_or(&path) + .to_string_lossy() + .replace('\\', "/"); + let contents = std::fs::read(&path) + .map_err(|source| TreeError::Io { path: path.clone(), source })?; + out.insert(rel.clone(), part_address(&rel, &contents)); + } + Ok(()) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn a_part_address_covers_the_path_as_well_as_the_contents() { + let same = part_address("a/x.rs", b"fn main() {}"); + let moved = part_address("b/x.rs", b"fn main() {}"); + assert_ne!( + same, moved, + "moving code can change what it means, so a rename ages the evidence" + ); + assert_eq!(same, part_address("a/x.rs", b"fn main() {}"), "and it is stable"); + } + + #[test] + fn the_whole_address_moves_when_any_part_does() { + let mut a = std::collections::BTreeMap::new(); + a.insert("x".to_string(), part_address("x", b"one")); + let t1 = Tree { root: PathBuf::from("."), parts: a.clone() }; + a.insert("x".to_string(), part_address("x", b"two")); + let t2 = Tree { root: PathBuf::from("."), parts: a }; + assert_ne!(t1.address(), t2.address()); + } + + #[test] + fn a_footprint_path_the_state_lacks_is_an_error() { + let t = Tree { root: PathBuf::from("."), parts: std::collections::BTreeMap::new() }; + assert!(matches!( + t.footprint(&["nope.rs".to_string()]), + Err(TreeError::NotInState(p)) if p == "nope.rs" + )); + assert!(t.is_empty()); + } +} diff --git a/joulespec/joulespec-rs/crates/joulespec-core/src/evidence.rs b/joulespec/joulespec-rs/crates/joulespec-core/src/evidence.rs index 540f87f3c..7a3c80c4d 100644 --- a/joulespec/joulespec-rs/crates/joulespec-core/src/evidence.rs +++ b/joulespec/joulespec-rs/crates/joulespec-core/src/evidence.rs @@ -581,9 +581,13 @@ impl Witness { if self.artifact == state.address { return true; } - if self.footprint.is_empty() || state.parts.is_empty() { + if self.footprint.is_empty() { return false; } + // A state whose parts cannot be enumerated needs no special case: an + // `all` over a non-empty footprint against no parts is already false, + // which is the conservative answer. An explicit guard here looked + // like care and could not change a single verdict. self.footprint.iter().all(|a| state.parts.contains(a)) } @@ -910,6 +914,42 @@ mod tests { assert!(!w.witness.applies_at(&after_auth_edit)); } + #[test] + fn a_witness_needs_every_footprint_member_not_merely_one() { + // Harvesting found this gap: the test above narrows to a single + // member, and on a one-element footprint `all` and `any` are the same + // function -- so the conjunction itself was never checked. + let k = key(1); + let auth = Address::of_bytes(b"auth@v1"); + let token = Address::of_bytes(b"token@v1"); + let w = Witness::new( + Address::of_bytes(b"spec"), + obligation(), + Address::of_bytes(b"tree-v1"), + falsifiable("rejects_anon", Anchor::Specification), + Energy::estimated(10), + k.verifying_key().to_bytes(), + ) + .with_footprint([auth.clone(), token.clone()]) + .sign(&k) + .unwrap(); + + let both = crate::conform::ArtifactState::new( + Address::of_bytes(b"tree-v2"), + [auth.clone(), token.clone(), Address::of_bytes(b"README@v2")], + ); + assert!(w.witness.applies_at(&both), "nothing it depended on moved"); + + let one_moved = crate::conform::ArtifactState::new( + Address::of_bytes(b"tree-v3"), + [auth, Address::of_bytes(b"token@v2")], + ); + assert!( + !w.witness.applies_at(&one_moved), + "one surviving member is not enough: every input the evidence read must still hold" + ); + } + #[test] fn a_footprint_that_cannot_be_checked_is_stale() { let k = key(1); diff --git a/joulespec/joulespec-rs/crates/joulespec-core/tests/vectors.rs b/joulespec/joulespec-rs/crates/joulespec-core/tests/vectors.rs new file mode 100644 index 000000000..4793b1122 --- /dev/null +++ b/joulespec/joulespec-rs/crates/joulespec-core/tests/vectors.rs @@ -0,0 +1,243 @@ +//! The published wire vectors. +//! +//! The charter's conformance test is that an implementation round-trips the +//! published vectors, so these files are the certifiable surface: fixed keys, +//! fixed clauses, fixed witnesses and **fixed energy**, producing receipt bytes +//! that must not change without a version bump. +//! +//! They are deliberately separate from the self-conformance record in +//! `conformance/v1/`, which is a *measurement* — its energy figures come from a +//! wall clock and are reproducible by nobody. One pack certifies the format; +//! the other reports what the reference implementation's own checks establish. +//! +//! Regenerate with `JOULESPEC_GEN_VECTORS=1 cargo test -p joulespec-core +//! --test vectors`, and commit the result. Without that variable the test +//! asserts the committed bytes, so a change to the wire format fails here +//! rather than silently shipping. + +use std::path::{Path, PathBuf}; + +use ed25519_dalek::SigningKey; +use joulespec_core::conform::{ArtifactState, Work}; +use joulespec_core::evidence::{ + Anchor, Evidence, Formalization, Grounding, SignedWitness, Vacuity, Witness, +}; +use joulespec_core::receipt; +use joulespec_core::spec::{Clause, SignedSpec, Spec}; +use joulespec_core::{Address, Energy, Provenance}; + +/// Published vectors are signed with keys everyone holds, so the bytes are +/// reproducible. They are not secrets. +fn key(seed: u8) -> SigningKey { + SigningKey::from_bytes(&[seed; 32]) +} + +const STEWARD: &str = "did:key:joulespec-vector-steward"; + +fn dir() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../conformance/v1/vectors") +} + +fn artifact() -> ArtifactState { + ArtifactState::new( + Address::of_bytes(b"vector-tree-v1"), + [ + Address::of_bytes(b"vector-part-auth"), + Address::of_bytes(b"vector-part-decide"), + Address::of_bytes(b"vector-part-docs"), + ], + ) +} + +fn spec() -> SignedSpec { + let author = key(1); + Spec::new( + "A metered endpoint that refuses what it cannot charge for.", + vec![ + Clause::requirement("C1", "The endpoint rejects unauthenticated requests."), + Clause::constraint("C2", "A request is decided before any side effect runs."), + Clause::requirement("C3", "Every decision seals a receipt."), + Clause::non_goal("C4", "The endpoint does not implement its own retry policy."), + ], + author.verifying_key().to_bytes(), + ) + .sign(&author) + .expect("vector spec signs") +} + +/// One witness per rung the format can carry, so a verifier that mishandles +/// any of them fails the pack. +fn witnesses(spec: &SignedSpec) -> Vec { + let spec_id = spec.spec.spec_id().unwrap(); + let state = artifact(); + let obligation = |label: &str| { + spec.spec + .clauses + .iter() + .find(|c| c.label == label) + .expect("label") + .obligation() + .unwrap() + }; + let auditor = key(2); + let implementer = key(4); + + vec![ + // C1 at E4: a cross-checked formalization, refuted against a + // counter-model, witnessed by a key that authored no work. + Witness::new( + spec_id.clone(), + obligation("C1"), + state.address.clone(), + Evidence::Proved { + goal: Address::of_bytes(b"vector-goal-auth"), + tier: "T1".into(), + formalization: Formalization { + statement: "forall r. !authenticated(r) -> rejected(r)".into(), + grounding: Grounding::CrossChecked { by: key(3).verifying_key().to_bytes() }, + }, + vacuity: Vacuity::Refuted { counter: Address::of_bytes(b"vector-counter-model") }, + }, + Energy::new(4_200, Provenance::ModelBased), + auditor.verifying_key().to_bytes(), + ) + .with_footprint([Address::of_bytes(b"vector-part-auth")]) + .sign(&auditor) + .unwrap(), + // C2 at E3: a specification-anchored check with a killed + // counter-artifact. + Witness::new( + spec_id.clone(), + obligation("C2"), + state.address.clone(), + Evidence::Falsifiable { + check: "decided_before_side_effect".into(), + anchor: Anchor::Specification, + counter: Address::of_bytes(b"vector-mutant-decide"), + }, + Energy::new(1_100, Provenance::HwShunt), + auditor.verifying_key().to_bytes(), + ) + .with_footprint([Address::of_bytes(b"vector-part-decide")]) + .sign(&auditor) + .unwrap(), + // C3 at E0: the implementer says so. The rung the state of the art + // produces, carried as the testimony it is. + Witness::new( + spec_id.clone(), + obligation("C3"), + state.address.clone(), + Evidence::Cited, + Energy::new(50, Provenance::Estimator), + implementer.verifying_key().to_bytes(), + ) + .sign(&implementer) + .unwrap(), + // A stale witness: bound to an earlier state, with no footprint, so + // it is reported rather than counted. + Witness::new( + spec_id, + obligation("C3"), + Address::of_bytes(b"vector-tree-v0"), + Evidence::Exercised { check: "seals_a_receipt".into(), anchor: Anchor::State }, + Energy::new(900, Provenance::HwShunt), + auditor.verifying_key().to_bytes(), + ) + .sign(&auditor) + .unwrap(), + ] +} + +fn work(spec: &SignedSpec) -> Vec { + let implementer = key(4).verifying_key().to_bytes(); + let c1 = spec.spec.clauses[0].obligation().unwrap(); + vec![ + Work::new( + Address::of_bytes(b"vector-op-auth"), + vec![c1], + Energy::new(750_000, Provenance::HwShunt), + implementer, + ), + // Work that cites no clause: the unspecified share, named. + Work::new( + Address::of_bytes(b"vector-op-unasked"), + vec![], + Energy::new(250_000, Provenance::HwShunt), + implementer, + ), + ] +} + +fn json(value: &T) -> String { + let mut s = serde_json::to_string_pretty(value).expect("serialises"); + s.push('\n'); + s +} + +#[test] +fn published_vectors_are_byte_stable() { + let spec = spec(); + let state = artifact(); + let witnesses = witnesses(&spec); + let work = work(&spec); + let (envelope, conformance) = + receipt::seal(&spec, &state, &witnesses, &work, STEWARD, &key(9)).expect("seals"); + + // The verdict the pack asserts, stated here so a reader sees what these + // bytes are supposed to mean. + assert_eq!(conformance.grade, Some(joulespec_core::evidence::Grade::Cited), + "C3's citation caps a specification whose other clauses are proved"); + assert_eq!(conformance.attestation, Some(joulespec_core::evidence::Attestation::SelfAttested), + "C3's only surviving witness is the implementer's own"); + assert_eq!(conformance.specified_ppm(), Some(750_000)); + assert_eq!(conformance.unspecified.len(), 1); + assert_eq!(conformance.clauses[3].grade, None, "the non-goal is unwitnessed, which is correct"); + assert!(conformance.flags.is_empty()); + assert_eq!(conformance.clauses[2].stale.len(), 1, "the earlier state's witness is reported"); + + let files: Vec<(&str, Vec)> = vec![ + ("spec.json", json(&spec).into_bytes()), + ("witnesses.json", json(&witnesses).into_bytes()), + ("state.json", json(&state).into_bytes()), + ("work.json", json(&work).into_bytes()), + ("receipt.json", json(&receipt::wire(&conformance, STEWARD)).into_bytes()), + ("receipt.cbor", envelope.clone()), + ]; + + let dir = dir(); + if std::env::var_os("JOULESPEC_GEN_VECTORS").is_some() { + std::fs::create_dir_all(&dir).expect("vector directory"); + for (name, bytes) in &files { + std::fs::write(dir.join(name), bytes).expect("writes vector"); + } + return; + } + + for (name, bytes) in &files { + let path = dir.join(name); + let committed = std::fs::read(&path).unwrap_or_else(|e| { + panic!("{}: {e}. Regenerate with JOULESPEC_GEN_VECTORS=1", path.display()) + }); + assert_eq!( + &committed, bytes, + "{} differs from what this implementation produces; the wire format changed", + path.display() + ); + } + + // And the sealed envelope verifies under the published key. + let doc = receipt::verify(&envelope, STEWARD, &key(9).verifying_key().to_bytes()) + .expect("the published receipt verifies"); + assert_eq!(doc["joulespec_receipt"], serde_json::json!("joulespec/1")); +} + +#[test] +fn the_pack_covers_every_rung_the_format_can_carry() { + // A pack that exercised only one rung would certify only one rung. + let spec = spec(); + let kinds: std::collections::BTreeSet<&str> = + witnesses(&spec).iter().map(|w| w.witness.evidence.label()).collect(); + for want in ["proved", "falsifiable", "exercised", "cited"] { + assert!(kinds.contains(want), "the vectors carry no {want} witness"); + } +} -- 2.54.0 (Apple Git-157)