joulespec: a producer, and the standard applied to its own implementation #566
28 changed files with 6621 additions and 8 deletions
38
.github/workflows/standards-build.yml
vendored
38
.github/workflows/standards-build.yml
vendored
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
---
|
||||
|
||||
|
|
|
|||
84
joulespec/conformance/v1/README.md
Normal file
84
joulespec/conformance/v1/README.md
Normal file
|
|
@ -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.
|
||||
322
joulespec/conformance/v1/harvest.toml
Normal file
322
joulespec/conformance/v1/harvest.toml
Normal file
|
|
@ -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::<Obligation>())"
|
||||
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::<Vec<_>>(),'
|
||||
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"
|
||||
BIN
joulespec/conformance/v1/receipt.cbor
Normal file
BIN
joulespec/conformance/v1/receipt.cbor
Normal file
Binary file not shown.
140
joulespec/conformance/v1/receipt.json
Normal file
140
joulespec/conformance/v1/receipt.json
Normal file
|
|
@ -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
|
||||
}
|
||||
165
joulespec/conformance/v1/spec.json
Normal file
165
joulespec/conformance/v1/spec.json
Normal file
|
|
@ -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
|
||||
]
|
||||
}
|
||||
18
joulespec/conformance/v1/state.json
Normal file
18
joulespec/conformance/v1/state.json
Normal file
|
|
@ -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"
|
||||
]
|
||||
}
|
||||
BIN
joulespec/conformance/v1/vectors/receipt.cbor
Normal file
BIN
joulespec/conformance/v1/vectors/receipt.cbor
Normal file
Binary file not shown.
64
joulespec/conformance/v1/vectors/receipt.json
Normal file
64
joulespec/conformance/v1/vectors/receipt.json
Normal file
|
|
@ -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
|
||||
}
|
||||
130
joulespec/conformance/v1/vectors/spec.json
Normal file
130
joulespec/conformance/v1/vectors/spec.json
Normal file
|
|
@ -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
|
||||
]
|
||||
}
|
||||
8
joulespec/conformance/v1/vectors/state.json
Normal file
8
joulespec/conformance/v1/vectors/state.json
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
{
|
||||
"address": "b3:522f65149fd69b1b2748015af25b4891dc01b4f81dff8a7992851462e20838d0",
|
||||
"parts": [
|
||||
"b3:54db5923a1c8b004e4f93f7c848b7f5de788fd3c600ab3070f70bfb7e150fb9b",
|
||||
"b3:69bce1edec460f82fa06ad97487c1069c7d4f775b5c89dae0c21244438057151",
|
||||
"b3:8624949b04e977f3df70c21be24b552bfd25065ea7d7f2ae9f4915953b483a6b"
|
||||
]
|
||||
}
|
||||
526
joulespec/conformance/v1/vectors/witnesses.json
Normal file
526
joulespec/conformance/v1/vectors/witnesses.json
Normal file
|
|
@ -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
|
||||
]
|
||||
}
|
||||
]
|
||||
88
joulespec/conformance/v1/vectors/work.json
Normal file
88
joulespec/conformance/v1/vectors/work.json
Normal file
|
|
@ -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
|
||||
]
|
||||
}
|
||||
]
|
||||
2687
joulespec/conformance/v1/witnesses.json
Normal file
2687
joulespec/conformance/v1/witnesses.json
Normal file
File diff suppressed because it is too large
Load diff
95
joulespec/joulespec-rs/Cargo.lock
generated
95
joulespec/joulespec-rs/Cargo.lock
generated
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
23
joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml
Normal file
23
joulespec/joulespec-rs/crates/joulespec-cli/Cargo.toml
Normal file
|
|
@ -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"
|
||||
439
joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs
Normal file
439
joulespec/joulespec-rs/crates/joulespec-cli/src/harvest.rs
Normal file
|
|
@ -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<SignedWitness>,
|
||||
/// What happened to every declared mapping, in manifest order.
|
||||
pub notes: Vec<Note>,
|
||||
}
|
||||
|
||||
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<Anchor, HarvestError> {
|
||||
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<Provenance, HarvestError> {
|
||||
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<Outcome, HarvestError> {
|
||||
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<String> = 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::<Result<_, joulespec_core::Error>>()?;
|
||||
|
||||
// ── 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());
|
||||
}
|
||||
}
|
||||
311
joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs
Normal file
311
joulespec/joulespec-rs/crates/joulespec-cli/src/main.rs
Normal file
|
|
@ -0,0 +1,311 @@
|
|||
//! `joulespec` — the reference producer and checker.
|
||||
//!
|
||||
//! ```text
|
||||
//! joulespec harvest --manifest <path> --out <dir> [--require-grade E2|E3]
|
||||
//! joulespec verify --receipt <path> --steward <id> --key <hex>
|
||||
//! joulespec drift --from <spec.json> --to <spec.json>
|
||||
//! ```
|
||||
//!
|
||||
//! `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<String, String>);
|
||||
|
||||
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<Grade, String> {
|
||||
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<i32, String> {
|
||||
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<String, String> { 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<i32, String> {
|
||||
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<i32, String> {
|
||||
let read = |p: &str| -> Result<SignedSpec, String> {
|
||||
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<String, String>;
|
||||
}
|
||||
|
||||
impl<T: serde::Serialize> Json for T {
|
||||
fn to_json(&self) -> Result<String, String> {
|
||||
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 <path> [--out <dir>] [--require-grade E0..E4]
|
||||
[--author-seed N] [--witness-seed N] [--steward-seed N]
|
||||
joulespec verify --receipt <path> --steward <id> --key <64 hex chars>
|
||||
joulespec drift --from <spec.json> --to <spec.json>
|
||||
|
||||
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<String> = 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<String> = ["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<String> = ["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());
|
||||
}
|
||||
}
|
||||
287
joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs
Normal file
287
joulespec/joulespec-rs/crates/joulespec-cli/src/manifest.rs
Normal file
|
|
@ -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<String>,
|
||||
/// Individual files to include.
|
||||
#[serde(default)]
|
||||
pub files: Vec<String>,
|
||||
/// Extensions to keep while walking.
|
||||
pub extensions: Vec<String>,
|
||||
}
|
||||
|
||||
/// 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<String>,
|
||||
/// The counter-artifact that should make it fail. Without one the check
|
||||
/// cannot exceed `E2` however carefully it was written.
|
||||
pub counter: Option<Counter>,
|
||||
}
|
||||
|
||||
/// 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<Evidence>,
|
||||
}
|
||||
|
||||
impl Manifest {
|
||||
/// Read and structurally validate a manifest.
|
||||
pub fn read(path: &str) -> Result<Self, ManifestError> {
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
316
joulespec/joulespec-rs/crates/joulespec-cli/src/runner.rs
Normal file
316
joulespec/joulespec-rs/crates/joulespec-cli/src/runner.rs
Normal file
|
|
@ -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::<usize>().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<bool, RunError> {
|
||||
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<Run, RunError> {
|
||||
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<Self, RunError>
|
||||
{
|
||||
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);
|
||||
}
|
||||
}
|
||||
291
joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs
Normal file
291
joulespec/joulespec-rs/crates/joulespec-cli/src/specdoc.rs
Normal file
|
|
@ -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<Vec<Item>, 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<Item> = Vec::new();
|
||||
let mut pending: Option<Item> = None;
|
||||
for line in lines {
|
||||
// The next heading of any level ends the section.
|
||||
if line.trim_start().starts_with('#') {
|
||||
break;
|
||||
}
|
||||
let trimmed = line.trim_start();
|
||||
let numbered = trimmed
|
||||
.split_once(". ")
|
||||
.filter(|(n, _)| !n.is_empty() && n.chars().all(|c| c.is_ascii_digit()));
|
||||
|
||||
match numbered {
|
||||
Some((_, body)) => {
|
||||
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<Clause> {
|
||||
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"));
|
||||
}
|
||||
}
|
||||
204
joulespec/joulespec-rs/crates/joulespec-cli/src/tree.rs
Normal file
204
joulespec/joulespec-rs/crates/joulespec-cli/src/tree.rs
Normal file
|
|
@ -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<String, Address>,
|
||||
}
|
||||
|
||||
/// 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<Self, TreeError> {
|
||||
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, TreeError>
|
||||
{
|
||||
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<Vec<Address>, 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<String, Address>,
|
||||
) -> Result<(), TreeError> {
|
||||
let entries = std::fs::read_dir(dir)
|
||||
.map_err(|source| TreeError::Io { path: dir.to_path_buf(), source })?;
|
||||
let mut sorted: Vec<PathBuf> = 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());
|
||||
}
|
||||
}
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
243
joulespec/joulespec-rs/crates/joulespec-core/tests/vectors.rs
Normal file
243
joulespec/joulespec-rs/crates/joulespec-core/tests/vectors.rs
Normal file
|
|
@ -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<SignedWitness> {
|
||||
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<Work> {
|
||||
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<T: serde::Serialize>(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<u8>)> = 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");
|
||||
}
|
||||
}
|
||||
Loading…
Reference in a new issue