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

joulespec: what the prior art changed — anchoring, vacuity, footprints, a second axis #562

Merged
dcharlot merged 1 commit from joulespec/research-pass into main 2026-11-01 08:36:24 -05:00
Conversation 0 Commits 1 Files changed 8 +1722 -292
8 changed files with 1722 additions and 292 deletions
Download patch file Download diff file Expand all files Collapse all files

54
README.md
View file

@ -152,26 +152,40 @@ ordered by one question, *how hard would it be for this obligation to be
violated without this evidence noticing*: `E0:Cited` (testimony — where
prevailing practice lands) → `E1:Reviewed` → `E2:Exercised` (a green check,
which flatters: a test with no assertion passes) → `E3:Falsifiable` (the same
check on record **failing** against a named counter-artifact — the first rung
where green means something) → `E4:Proved`, reached only when the formalization
binding statement to clause was cross-checked by a key other than the prover's,
because a proof under a declared formalization is machine-checked evidence that
the something is this clause on the prover's word. A specification's grade is
its **weakest** owed obligation; non-goals are first-class, and evidence that
one was implemented is a flag that blocks conformance however good the rest is.
Revising a specification yields the exact partition of which evidence survives,
and a witness bound to an earlier artifact state is reported **stale** rather
than counted — so neither direction of drift needs anyone to remember to check.
Every witness and every unit of work carries its joules, so the receipt seals
the **specified share** (how much energy went into work citing no clause at
all) and **microjoules per falsifiable obligation** — the denominator
deliberately the rung whose evidence can fail, because a figure per *attempted*
obligation rewards ceremony. Receipts are derived from the evidence and never
from a verdict handed in, so every claim in one is reproducible by anyone
holding the same inputs.
check on record **failing** against a named counter-artifact) → `E4:Proved`.
**Every rung above `E2` rests on a demonstrated failure**, and the rule binds
proofs as much as tests: a formal statement can hold *vacuously*, true because
nothing ever reaches the condition it guards, so `E4` needs the statement
refuted against a counter-model and its formalization cross-checked by a key
other than the prover's. Whether a check can fail is also structural, not only
empirical — an oracle whose expected value derives from the system it judges
cannot disagree with that system when a fault moves measurement and expectation
together — so every check declares an **anchor** (`specification` / `state` /
`unstated`), and an unstated one caps at `E2` because the answer is free to
whoever wrote the check. A second axis runs beside the first: **attestation**
(`A0:self-attested` → `A1:independent` → `A2:reproduced`), derived from work
authorship and from agreement between disjoint keys, never declared, and absent
rather than independent where no implementer is known — because how strong a
check is and who vouches for it fail separately, most obviously when the
implementer and the reporter are one process. Both axes are minima over the
owed obligations and both gate conformance; non-goals are first-class, and
evidence that one was implemented is a flag that blocks conformance however
good the rest is. Revising a specification yields the exact partition of which
evidence survives, while a witness names the **footprint** it depended on and
survives any later state that still contains it — so a documentation edit does
not expire the evidence for an authentication requirement, which is how
traceability decays in practice. Every witness and every unit of work carries
its joules, so the receipt seals the **specified share** (how much energy went
into work citing no clause, with that work **named**, because unintended
function is what backward traceability exists to exclude) and **microjoules per
falsifiable obligation** — the denominator deliberately the rung whose evidence
can fail, and comparable only at a fixed specification address, since any
evidenced-over-total figure improves when trivial items are added. Receipts are
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.1.0-draft.1. `SPEC.md` published; reference workspace `joulespec-rs/` — `joulespec-core` carries obligation-addressed clauses and signed revisions, the graded evidence ladder with independence computed from key disjointness, the deterministic evaluator with the weakest-obligation cap and its four flag conditions, 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. `cargo test --workspace` green, `cargo clippy --workspace --all-targets` zero warnings and gated in CI.
## How this is organised
@ -196,7 +210,7 @@ open-standards/
├── joulecontract/ — contract cargo class: five-obligation energy-accounted interface contracts, bound + sealed receipts, adversarial-diff provenance (Apache-2.0 code / CC-BY-4.0 spec, Rust ref impl)
├── joule-os/ — the UDA reference runtime: single-level store + refine-family cascade + capability ledger, lowered per coordinate across native / PWA / bare-metal (Apache-2.0 code / CC-BY-4.0 spec, Rust ref impl)
├── mesh/ — inference serving + routing fabric: joule-ceiling × fidelity-floor requests routed cheapest-sufficient, metered, sealed as µJ-per-accepted-token receipts (Apache-2.0 code / CC-BY-4.0 spec, Rust ref impl)
└── joulespec/ — specification cargo class: obligation-addressed clauses, a graded evidence ladder from testimony to proof, deterministic drift, and the joules a specification cost to evidence (Apache-2.0 code / CC-BY-4.0 spec, Rust ref impl)```
└── joulespec/ — specification cargo class: obligation-addressed clauses, a graded evidence ladder from testimony to proof beside a derived attestation axis, deterministic drift, and the joules a specification cost to evidence (Apache-2.0 code / CC-BY-4.0 spec, Rust ref impl)```
The standards do not depend on one another. They share a steward and a doctrine — that the protocol is the public commitment and the operations are the offer. (Most also share a unit of accounting, joules; ARL is universal and tied to nothing, joules being one of its four measured axes rather than a shared substrate.)
@ -216,7 +230,7 @@ Contributions are welcome at the subdirectory level. Issues, discussions, and pu
- **JouleContract:** the in-toto/DSSE `JouleContract` predicate emission at the recognized edge; a signed conformance vector pack (`conformance/v1/`); adversarial negatives from the published diff rounds (a frame amendment racing its breach, a quorum whose members share a parent entity, an evidence bundle with one swapped attestation); meter-attestation backends (RAPL / NVML / substrate telemetry) feeding the `Metered` binding; and a fourth adversarial diff round.
- **Joule OS:** additional refine-family backends behind the cascade (real `LocalSearch` / `StateGraph` / `ConstrainedSearch` stages); per-platform measured-energy oracles feeding the work-class receipts; conformance negatives against the THEOREM I1–I20 invariants (a capability minted outside `Ledger::issue`, a single-level-store mutation that tears across an instruction boundary, an AOT/JIT divergence); and bare-metal surface drivers.
- **JouleSpec:** witness producers that emit `E3` evidence from suites already in use (a mutation runner recording the mutant each test was written against is the natural one), a bridge that turns the verification standard's discharged goals into `E4` witnesses with their formalizations carried through, adversarial negatives (a witness re-bound to a reworded obligation, a review countersigned by the citing key, a receipt sealed from a hand-built verdict), and measured-energy backends feeding the witness `HwShunt` path.
- **JouleSpec:** witness producers that emit `E3` evidence from suites already in use (a mutation runner recording the mutant each test was written against is the natural one, and a test harness that observes its own reads can emit the footprint rather than leaving it empty), a bridge that turns the verification standard's discharged goals into `E4` witnesses with their formalizations and vacuity checks carried through, adversarial negatives (a witness re-bound to a reworded obligation, a footprint widened after signing, a review countersigned by the citing key, a receipt sealed from a hand-built verdict), and measured-energy backends feeding the witness `HwShunt` path.
A `CONTRIBUTING.md` per standard captures the specifics where they diverge.

127
joulespec/README.md
View file

@ -1,6 +1,6 @@
# JouleSpec — Energy-Accounted Specification Conformance
**Version:** 0.1.0-draft.1 · **Status:** Draft · **Profile:** `joulespec/1`
**Version:** 0.2.0-draft.1 · **Status:** Draft · **Profile:** `joulespec/1`
**Specification text:** CC-BY-4.0 · **Reference code (`joulespec-rs/`):** Apache-2.0
JouleSpec is the open standard for **stating what software owes and measuring
@ -66,7 +66,16 @@ noticing?**
| `E1` | `reviewed` | A second party read the artifact, once. |
| `E2` | `exercised` | A named check ran against the artifact and passed. |
| `E3` | `falsifiable` | The same check is on record *failing* against a named counter-artifact. |
| `E4` | `proved` | No input violates it, under a formalization someone independent checked. |
| `E4` | `proved` | No input violates it, under a formalization someone independent checked, shown not to hold vacuously. |
**Every rung above `E2` rests on a demonstrated failure**, and the rule binds
proofs as much as tests. A formal property can be satisfied *vacuously* — true
because nothing ever reaches the condition it guards, so it would hold of
almost any implementation; detecting that is established practice in model
checking, and one industrial setting reported around a fifth of specifications
initially passing that way. So `E4` requires the statement to have been
**refuted** against a named counter-model, exactly as `E3` requires a check to
have failed against a counter-artifact.
**`E0` is where prevailing practice lands**, and it is testimony from the party
being evaluated. Much of it is true; it is still testimony, and reporting it as
@ -89,6 +98,65 @@ kind of evidence survives the next commit and the other does not.
**Independence is computed, never declared.** A review signed by the key that
made the citation is the citation again, and grades `E0` (SPEC §2.5).
## Where the expectation comes from
Whether a check *can* fail is not only an empirical question. An oracle whose
expected value is derived from the system it judges cannot disagree with that
system when a fault moves the measurement and the expectation together — the
comparison cancels, and no input reveals the fault. The defect is in the
oracle, not the inputs, and it is visible from the oracle's construction
without running anything.
So every check declares an **anchor**: `specification` (expected values fixed
outside the code under test — the spec, a published procedure, a reference
table), `state` (values flowing from the code under test), or `unstated`. An
unstated anchor caps a check at `E2`, because whether an oracle reads its
expectation from its own subject is knowable to whoever wrote it at no cost,
and silence is not an answer. A state-anchored check that killed a mutant did
fail once and reaches `E3` — with its anchor disclosed, because the class of
faults it cannot catch is disclosed with it (SPEC §2.5).
## Evidence that survives a change it did not depend on
Binding evidence to a whole-tree digest alone would make every commit stale
every witness. That is the documented way traceability dies: the empirical
literature finds trace links degrade mainly through ordinary refactoring, and
reports that keeping them current can cost more than creating them. A standard
whose evidence expires on every unrelated edit has reproduced that failure
however sound its addressing.
A witness therefore names a **footprint** — the addresses within the artifact
it actually depended on — and applies at any later state whose parts still
contain every member (SPEC §2.4). Edit the documentation and the evidence for
the auth requirement stands; edit the auth code and that clause ages, alone.
Paths never enter the mechanism: a content address *is* the identity of its
content.
A footprint is a producer's claim that nothing else mattered, signed with the
rest of the witness, and a narrower one is a **stronger** claim — so a wrong
footprint makes the evidence wrong rather than merely stale. An empty footprint
means the whole artifact, which is what a producer that cannot enumerate its
inputs must use.
## Two axes, because they fail separately
How strong a check is and how independent the party reporting it is are
different questions. Collapsing them loses the one that matters most where the
implementer and the reporter are the same process — the normal case for an
agent that writes code and then reports that it works.
| | | |
|---|---|---|
| `A0` | `self-attested` | The party reporting the result did the work. |
| `A1` | `independent` | Signed by a key that authored none of the work. |
| `A2` | `reproduced` | Two disjoint parties reported the same check at the same grade and state, at least one independent of the work. |
Both axes gate conformance (SPEC §3.4). Attestation is **derived** from work
authorship and from agreement between disjoint keys — never declared — and
where no work was supplied it is **absent** rather than independent: absence of
information about who built something is not evidence that someone else checked
it.
## What an `E4` actually claims
A proof discharges a formal statement, and the statement is not the clause. The
@ -148,9 +216,12 @@ nothing else in this space can state:
- **The specified share** — how much of the work energy went into work citing
an obligation this specification actually states, in parts-per-million (SPEC
§5.2). This is the measured form of an observation the field makes
qualitatively: that agents produce features nobody requested. A run where a
quarter of the energy implemented no clause has a number saying so.
§5.2), with the work that cites nothing **named** rather than only counted.
Certified-airborne-software practice has required traceability in both
directions for decades, and the backward direction exists for one purpose:
code with no upstream requirement is a finding even when it works correctly,
because unintended function is what the argument cannot otherwise exclude. A
figure answers *how much*; only the list answers *which*.
- **Microjoules per falsifiable obligation** — total attributed energy over the
count of owed obligations evidenced at `E3` or better (SPEC §5.3). The
denominator is deliberately the rung whose evidence can fail: a figure per
@ -165,6 +236,16 @@ more energy to get there — that is not a matter of taste.
Where nothing reaches the bar the figure is **absent**, not zero. A cost per
unit of nothing is not a small number.
And it is **comparable only at a fixed specification address** (SPEC §5.3).
Any figure of the form *things evidenced over things total* improves when you
add trivial things — the standing objection to counting resolved doubts in
assurance argumentation — so splitting one requirement into twenty trivially
falsifiable ones would divide this figure by twenty while establishing nothing.
The receipt seals the specification's address precisely so a reader can tell
whether two figures are comparable at all. The grade and the attestation carry
no such caveat: both are minima, and a minimum cannot be improved by adding
obligations.
## The receipt is derived, never signed on request
A receipt is sealed from the specification, the artifact, the witnesses and the
@ -186,6 +267,24 @@ 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).
## Relation to existing work
Structured assurance cases already standardize the *shape* of the argument —
claims decomposed to sub-claims until each links to evidence — and the
international standard for their structure is explicit that it does not set
quality requirements for the content. The grade of a piece of evidence is
exactly that content question, so `joulespec/1` adopts the vocabulary and
supplies the part left open. Certified-airborne-software practice supplies the
bidirectional rule, and grades *structural* coverage on a ladder of its own
that composes with this one rather than competing: coverage says how thoroughly
a check exercises the code, an anchor and a killed mutant say whether it can
fail at all. Supply-chain provenance frameworks grade the build record and say
nothing about correctness — that is the `A` axis, not duplicated here.
Carbon-intensity accounting for software is an international standard shaped as
a rate per functional unit of work, which is the shape of §5.3, and it covers
the energy of *running* software where this covers the energy of *producing*
it. Full treatment in SPEC §9.
## What it does not do
JouleSpec does not write specifications, run checks, formalize clauses, or
@ -198,13 +297,25 @@ purpose, because the specification was incomplete — and an incomplete
specification is exactly the case where every clause is covered. A grade is a
property of evidence, not of software (SPEC §8).
Three limits are worth stating here because they bound what the mechanisms
above can establish. A **footprint is trusted, not verified** — a producer that
narrows a witness to inputs its check did not read gets evidence outliving the
change that invalidated it; the claim is signed and attributable, and this
standard cannot tell what a check actually read. **`A2` is agreement, not
correctness**: reproducing a vacuous check reproduces the vacuity. And two of
the results this design builds on are thinly evidenced — the vacuity rate comes
from one industrial setting and the oracle-anchoring effect from a
single-system study — so the design rests on the mechanisms, which stand on
their own, rather than on the magnitudes.
## Reference
[`joulespec-rs/crates/joulespec-core`](joulespec-rs/crates/joulespec-core) —
obligation-addressed clauses and signed revisions (`spec`), the graded evidence
ladder with computed independence (`evidence`), the deterministic evaluator
with the weakest-obligation cap (`conform`), the revision partition (`drift`),
and the `joulespec/1` JCR-1 receipt derived from its inputs (`receipt`).
ladder with anchoring, vacuity and computed independence (`evidence`), the
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`).
Prior art inside this family: `joule-code-spec` first shipped the signed,
content-addressed clause and the citation binding a coding operation to it.

297
joulespec/SPEC.md
View file

@ -1,9 +1,9 @@
# JouleSpec v0.1 — A Standard for Energy-Accounted Specification Conformance
# JouleSpec v0.2 — A Standard for Energy-Accounted Specification Conformance
| | |
|---|---|
| **Standard** | joulespec |
| **Status** | v0.1.0 draft for review |
| **Status** | v0.2.0 draft for review |
| **Profile** | `joulespec/1` |
| **Licence** | Specification text CC-BY-4.0 ([`LICENSE-SPEC`](LICENSE-SPEC)); reference code Apache-2.0 ([`LICENSE`](LICENSE)) |
| **Reference** | [`joulespec-rs/`](joulespec-rs/) |
@ -151,6 +151,29 @@ does not name the state it observed cannot be aged out. In practice this is a
tree digest, a build output address, or a commit — JouleSpec does not care
which, only that it is an address.
A witness also names a **footprint**: the addresses *within* that state the
evidence depended on.
This is not an optimisation. Binding evidence to a whole-tree digest alone
makes every commit stale every witness, and that is the documented way
traceability dies: the empirical literature on trace links finds they degrade
mainly through ordinary refactoring, and reports that keeping them current can
cost more than creating them. A standard whose evidence expires on every
unrelated edit has reproduced that failure exactly, however sound its
addressing.
A witness applies at a state when the state is the one it observed, or when
every footprint member is still present in it (§3.1). Paths are deliberately
absent from the mechanism: a content address *is* the identity of its content,
so membership answers "is this input still what the evidence saw" without the
standard having to agree with anyone about file naming.
A footprint is a producer's claim that nothing else mattered. It is signed with
the rest of the witness, and a narrower footprint is a **stronger** claim — so
a wrong one makes the evidence wrong rather than merely stale. An **empty**
footprint means the whole artifact, which is the conservative reading and the
one a producer that cannot enumerate its inputs MUST use.
### 2.5 The evidence ladder
Every rung answers one question: **how hard would it be for this obligation to
@ -186,7 +209,67 @@ projects can reach with tests they already have.
is bound to the state a person looked at and cannot notice a violation
introduced afterwards; a named check can run again against any later state.
That ordering says nothing about how carefully anyone read the code — it says
that one kind of evidence survives the next commit and the other does not.
that one kind of evidence survives the next commit and the other does not. It
has a second consequence worth stating: the higher rungs are also the cheapest
to **refresh** when a footprint member moves, because a named check can simply
be run again.
#### Every rung above `E2` rests on a demonstrated failure
That rule is uniform, and it binds proofs as much as tests. A formal property
can be satisfied **vacuously** — true because nothing in the model ever
reaches the condition it guards, so it would hold of almost any
implementation. Detecting this is established practice in model checking,
where a property is understood as vacuous when it can be replaced by a
constant without changing its value in the model, and one industrial
verification setting reported around a fifth of specifications initially
passing that way.
So `E4` requires the statement to have been **refuted** against a named
counter-model (§2.6), exactly as `E3` requires a check to have failed against
a counter-artifact. Nothing reaches either rung on a passing run alone.
#### Where the expectation comes from
A check's ability to fail is not only an empirical question. An oracle whose
expected value is derived from the system it is judging cannot disagree with
that system when a fault moves the measurement and the expectation together —
the comparison cancels, and no input reveals the fault. The defect is in the
oracle rather than in the inputs, and it is visible from the oracle's
construction without running anything.
Every check therefore declares an **anchor**:
| Anchor | Meaning |
|---|---|
| `specification` | Expected values are fixed outside the code under test — the specification, a published procedure, a reference table, an independently computed model. |
| `state` | Expected values flow, directly or indirectly, from the code under test. |
| `unstated` | The producer has not said. |
An **unstated** anchor caps a check at `E2`, because whether an oracle reads
its expectation from its own subject is knowable to whoever wrote it at no
cost, and silence is not an answer. A **state**-anchored check that killed a
counter-artifact really did fail once and reaches `E3`, with its anchor
disclosed — the class of faults it cannot catch is disclosed with it. This
standard does not refuse state-anchored evidence; it refuses to report it as
indistinguishable from the other kind.
The anchor is part of the signed witness, so two anchors are two different
claims and two different witnesses.
#### What the equivalent-mutant problem does not cost
Mutation scoring is noisy and contested because a mutant semantically
identical to the original cannot be killed, so it depresses a score without
indicating any weakness; reported rates range from a few per cent to roughly a
third of mutants, and one large-scale industrial account found most generated
mutants unproductive until mutation was restricted to changed lines.
`E3` is immune in the direction that matters: it only ever uses a mutant the
check **did** kill as positive evidence. An equivalent mutant cannot produce an
`E3` witness at all, so the problem that makes scores expensive cannot inflate
a grade here. The cost of the rung is correspondingly low — one killed mutant
per obligation, which a project can harvest from tests it already has.
**Independence is computed, never declared.** A review signed by the key that
made the citation is the citation again, and grades `E0`. A conforming
@ -200,11 +283,20 @@ binding between them is a human act, and it is the weakest link in any claim of
proved conformance. A conforming implementation MUST NOT formalize a clause on
its own initiative: a formalization is supplied, and it carries a grounding.
| Grounding | Reached grade |
|---|---|
| `cross-checked` by a key other than the witness author's | `E4` |
| `declared` | `E2` |
| `cross-checked` by the witness author's own key | `E2` |
A proof also carries a **vacuity** state: `refuted` against a named
counter-model, or `unchecked`.
| Grounding | Vacuity | Reached grade |
|---|---|---|
| `cross-checked` by a key other than the witness author's | `refuted` | `E4` |
| `cross-checked` by another key | `unchecked` | `E2` |
| `declared` | any | `E2` |
| `cross-checked` by the witness author's own key | any | `E2` |
There are two independent ways a proof can establish nothing about a clause:
the statement may not be the clause (ungrounded), or it may hold of almost
anything (vacuous). Either leaves real mechanical evidence about *something*,
which is `E2` — the same rung as a green check, for the same reason.
A proof under a formalization nobody independent read is machine-checked
evidence about *something*; that the something is this clause is the prover's
@ -226,6 +318,39 @@ a witness is what *observed* something. Conflating them hides the question this
standard exists to answer, which is whether the evidence was worth what it
cost.
### 2.8 Attestation: the second axis
How strong a check is and how independent the party reporting it is are
different questions. Collapsing them loses the one that matters most where the
implementer and the reporter are the same process — the normal case for an
agent that writes code and then reports that it works.
A verdict therefore carries a grade **and** an attestation:
| | Attestation | Meaning |
|---|---|---|
| `A0` | `self-attested` | The party reporting the result is a party that did the work. |
| `A1` | `independent` | Signed by a key that authored none of the work on this specification. |
| `A2` | `reproduced` | Two parties with disjoint keys reported the same check at the same grade and artifact state, at least one of them independent of the work. |
Attestation is **derived, never declared**: from whether a witness's author
also authored work on this specification, and from whether disjoint parties
reported the same check. A conforming implementation MUST compute it and MUST
NOT read it from a field a producer set.
Where **no work was supplied**, no party is known to be an implementer, and
attestation is **absent** rather than assumed independent. Absence of
information about who built something is not evidence that someone else
checked it.
Supply-chain provenance frameworks grade build records on exactly this axis —
whether provenance merely exists, is signed by a hosted builder, or comes from
a hardened one — and are explicit that they say nothing about whether the
software is correct. That is the right division: those levels grade the
*record* while this ladder grades the *evidence*, and a complete claim needs
both. This family's readiness standard likewise publishes several axes with
gates between them rather than one scalar, for the same reason.
---
## 3. Evaluation
@ -244,13 +369,20 @@ other outcome is reported, and none is discarded:
| Its signature and structure verify | `unverifiable` flag, by input position |
| It names this specification | `foreign-spec` flag |
| It names an obligation this specification states | `unbound` flag |
| It was observed at this artifact state | recorded as **stale** on that clause |
| It applies at this artifact state (§2.4) | recorded as **stale** on that clause |
A witness naming an obligation the specification does not state is the normal
aftermath of a rewording, and it MUST NOT be dropped quietly — it is the
clearest available signal that evidence and specification have parted company.
A clause's grade is the strongest grade among its contributing witnesses. Where
A witness **applies** at a state when the state is the one it observed, or
when it narrowed itself to a footprint whose every member is still present. A
footprint that cannot be checked — because the caller cannot enumerate the
current state — is stale, which is the conservative direction.
A clause's grade is the strongest grade among its contributing witnesses, and
its attestation the strongest among them (§2.8), with the whole clause's
attestation absent where no work identifies an implementer. Where
several witnesses tie, the one with the lowest address is named, so two
evaluations over the same inputs produce the same verdict.
@ -263,6 +395,15 @@ Averaging would let nine proved obligations conceal one nobody looked at, which
is precisely the failure a grade exists to surface. This family applies the
same rule wherever a composite claim meets a weak component.
The **attestation** is capped the same way and separately: a specification's
attestation is the minimum over its owed obligations. The two minima are taken
independently, because a specification can be uniformly well checked by the
party that wrote it, or uniformly witnessed by an auditor who only read it.
A grade is not gameable by adding clauses, and in the direction that matters:
adding an obligation can only lower a minimum. §5.3 records the figure where
this does not hold.
### 3.3 Non-goals
Non-goals are excluded from the cap: there is nothing to evidence about
@ -278,7 +419,14 @@ and something says it exists; no amount of evidence elsewhere settles that.
A flag is something wrong with the evidence set, as distinct from a weakly
evidenced obligation. An implementation reports conformance at a requested bar
only when every owed obligation reaches it **and** no flag is raised.
only when every owed obligation reaches it on **both** axes and no flag is
raised.
Both axes gate because they fail separately: a proof nobody independent of the
implementer ever saw, and a citation from an independent auditor, are each
strong on one axis and weakest on the other. An **absent** attestation cannot
satisfy a bar above `A0` — absence of information about who built something is
not evidence that someone else checked it.
### 3.5 Determinism
@ -349,6 +497,14 @@ that agents produce features nobody requested. A run in which a quarter of the
energy went into work citing no clause has a number saying so, and that number
is in the receipt.
Unspecified work is also reported as a **named list**, not only as a figure.
Certified-airborne-software practice has required traceability in both
directions for decades, and the backward direction exists for one purpose:
code with no upstream requirement is a finding even when it works correctly,
because unintended function is what the argument cannot otherwise exclude. A
figure answers *how much*; only the list answers *which*, and only the list
can be acted on.
Ratios are integers in parts-per-million because the canonical core admits no
floats (§6.2), and a ppm figure survives the round trip exactly where a rounded
percentage would not.
@ -367,6 +523,24 @@ rather than attempts.
Where nothing reaches the bar the figure is **absent**, not zero. A cost per
unit of nothing is not a small number.
#### Comparable only at a fixed specification
Any figure of the form *things evidenced over things total* can be improved by
adding trivial things. This is the standing objection to counting resolved
doubts in assurance argumentation, where confidence can be inflated by raising
and then dismissing easy ones. Here the denominator is a clause count, so
splitting one requirement into twenty trivially falsifiable ones divides the
figure by twenty while establishing nothing new.
The figure is therefore comparable **only between evaluations carrying the same
specification address**, which is the comparison it exists for: two processes
against one specification. A receipt seals that address (§6.3) precisely so a
reader can tell whether two figures are comparable at all, and an
implementation MUST NOT present the figure as a cross-specification benchmark.
The grade and the attestation carry no such caveat; both are minima, and a
minimum cannot be improved by adding obligations.
This figure is what makes the field's central argument decidable. Whether
specification-driven practice earns its overhead is currently settled by
anecdote in both directions. Two processes applied to the same specification,
@ -403,9 +577,15 @@ would believe one was.
### 6.3 The per-clause audit
A receipt carries one entry per clause — label, kind, obligation, grade where
established, the witness that carried it, evidence energy, and the count of
stale witnesses — alongside the specification-level summary.
A receipt carries one entry per clause — label, kind, obligation, grade and
attestation where established, the **means** (the kind of evidence that
carried the grade), its **anchor** where its kind declares one, the witness
that carried it, evidence energy, and the count of stale witnesses — alongside
the specification-level summary and the named list of unspecified work.
The means is load-bearing, not decoration: two clauses at `E2` can be a green
check and a proof whose statement nobody tied to the clause, and a grade alone
cannot tell a reader which it is looking at.
Which obligation is the weak one is the actionable fact. It must be answerable
from the receipt alone, rather than by re-running an evaluation whose inputs
@ -436,7 +616,18 @@ An implementation conforms to `joulespec/1` when:
7. **C7 — Cost.** Aggregates carry the weakest contributing provenance; ratios
are integer parts-per-million; absent figures are absent.
8. **C8 — Receipts.** Receipts are derived from inputs, seal as JCR-1, omit
absent fields, and carry the per-clause audit.
absent fields, and carry the per-clause audit with means and anchor.
9. **C9 — 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.
10. **C10 — 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).
11. **C11 — 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).
The reference implementation is conformant by construction. A third-party
implementation certifies itself by reproducing these behaviours; the reference
@ -474,6 +665,82 @@ guess is a guess no matter how precisely it is reported, which is why the grade
travels with the number and why an aggregate never claims better than its
weakest part.
**A footprint is trusted, not verified.** A producer that narrows a witness to
inputs the check did not really depend on gets evidence that outlives the
change which invalidated it. The footprint is signed and disclosed, so the
claim is attributable and reviewable, but this standard cannot tell what a
check actually read. An implementation that can observe its own reads should
emit the footprint it observed; one that cannot MUST leave it empty rather
than guess.
**`A2` is agreement, not correctness.** Two parties running the same check and
getting the same answer have excluded a mistake in the running, not a mistake
in the check. Reproduction of a vacuous check reproduces the vacuity.
**The cost figure is comparable only at a fixed specification** (§5.3). A
cross-specification comparison of microjoules per obligation is not a weaker
measurement; it is not a measurement.
**Two of the results this standard builds on are thinly evidenced.** The
vacuity rate quoted in §2.5 comes from one industrial verification setting, and
the oracle-anchoring effect it reports comes from a single-system study by a
single author. The *mechanisms* stand on their own — an expectation derived
from the system cannot disagree with it when both move; a property replaceable
by a constant constrains nothing — and the design rests on those arguments
rather than on the magnitudes.
---
## 9. Relation to existing work
JouleSpec is not the first attempt to tie claims to evidence. It is narrow
about what it adds, and the things it does not re-invent are worth naming.
**Structured assurance cases** already standardize the shape of the argument: a
claim decomposed into sub-claims until each is linked to evidence, with the
inference between them stated. The international standard for assurance-case
structure and content is explicit that it sets requirements for structure and
contents and **not** quality requirements for the content — and the grade of a
piece of evidence is exactly that content question. `joulespec/1` adopts the
vocabulary (a clause is a claim; a witness is evidence; an obligation with no
evidence is undeveloped) and supplies the part left open: an ordered,
mechanically computed grade, and a cap that makes the composite no stronger
than its weakest link.
**Certified-airborne-software practice** supplies the bidirectional rule
(§5.2): code with no upstream requirement is a finding even when it works.
It also grades *structural* coverage — statement, decision, modified
condition/decision — on a ladder of its own, by criticality level. That ladder
is orthogonal to this one and composes with it: a check's coverage criterion
describes how thoroughly it exercises the code, where an anchor and a killed
counter-artifact describe whether it can fail at all. A deployment that
requires both is stating two different things, and should.
**Supply-chain provenance frameworks** grade the trustworthiness of the build
*record* and say nothing about whether the software is correct. That is the
`A` axis of §2.8 and this standard does not duplicate it: a conforming
deployment can carry provenance levels for its artifacts and attestation grades
for its evidence, and they answer different questions.
**Mutation testing** supplies the counter-artifact. §2.5 records why the
equivalent-mutant problem that makes mutation *scores* contested cannot
inflate a grade here, and why one killed mutant per obligation is a
deliberately cheap bar rather than an attempt at a score.
**Carbon-intensity accounting for software** is an international standard
expressing emissions as a rate per functional unit of work. §5.3 has the same
shape, with an evidenced obligation as the functional unit. That standard
covers the energy of *running* software; the energy of *producing* it is
outside its scope, which is the quantity measured here. The two are
complementary rather than competing, and a deployment reporting both is
reporting a system's operation and its construction.
What is new here is the conjunction: an obligation address that survives
renaming and breaks on rewording, a grade that requires a demonstrated
failure above `E2`, a footprint that keeps evidence alive across unrelated
change, and a per-obligation energy figure. Each part has precedent; the
combination is what makes conformance a measured quantity rather than a claim.
---
*JouleSpec is stewarded by [Transaction Science](https://transaction.science).

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

@ -205,7 +205,7 @@ checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
[[package]]
name = "joulespec-core"
version = "0.1.0"
version = "0.2.0"
dependencies = [
"blake3",
"ed25519-dalek",

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

@ -1,6 +1,6 @@
[package]
name = "joulespec-core"
version = "0.1.0"
version = "0.2.0"
description = "JouleSpec — the reference conformance kernel for energy-accounted specifications (joulespec/1): obligation-addressed clauses, a graded evidence ladder from testimony to proof, deterministic drift, and the joules a specification cost to evidence."
edition.workspace = true
license.workspace = true

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

@ -33,22 +33,88 @@
//! to evidence about behaviour that should not exist, and evidence that it
//! *does* exist is a different kind of problem.
//!
//! ## Two axes, because they fail separately
//!
//! How strong a check is and how independent the party reporting it is are
//! different questions. Collapsing them loses the one that matters most where
//! the implementer and the reporter are the same process — which is the normal
//! case for an agent that writes code and then reports that it works.
//!
//! So a verdict carries a [`Grade`] *and* an
//! [`Attestation`](crate::evidence::Attestation), and conformance takes a bar
//! on both ([`Conformance::is_conformant`]). Supply-chain provenance grades
//! records on the second axis alone and is explicit that it says nothing about
//! whether the software is correct; this family's readiness standard already
//! publishes several axes with gates between them for the same reason.
//!
//! Attestation is **derived**, never declared: from whether a witness's author
//! also authored work on this specification, and from whether disjoint parties
//! reported the same check at the same state. Where no work was supplied,
//! nobody's identity as implementer is known, so attestation is **absent**
//! rather than assumed independent.
//!
//! ## Work with no clause is a finding, not a statistic
//!
//! Certified-avionics practice has required traceability in *both* directions
//! for decades, and the backward direction exists for one purpose: code with
//! no upstream requirement is a finding even when it works correctly, because
//! unintended function is what the argument cannot otherwise exclude.
//!
//! So unspecified work is reported two ways — as energy, which answers *how
//! much*, and as a **named list**, which answers *which*
//! ([`Conformance::unspecified`]). A figure alone cannot be acted on.
//!
//! ## Why the ratio is parts-per-million
//!
//! JCR-1's canonical core admits no floats, so every ratio this standard seals
//! is an integer. A fraction is reported in parts-per-million rather than as a
//! rounded percentage so it survives the round trip exactly.
//!
//! Normative: SPEC §3.1 (what counts), SPEC §3.2 (the cap), SPEC §3.3
//! (non-goals), SPEC §3.4 (flags), SPEC §3.5 (determinism), SPEC §5.1 and
//! SPEC §5.2 (cost).
//! Normative: SPEC §2.8 (attestation), SPEC §3.1 (what counts), SPEC §3.2
//! (the cap on both axes), SPEC §3.3 (non-goals), SPEC §3.4 (flags and the
//! gate), SPEC §3.5 (determinism), SPEC §5.1 and SPEC §5.2 (cost),
//! SPEC §5.3 (comparability).
use serde::{Deserialize, Serialize};
use crate::evidence::{Grade, SignedWitness};
use crate::evidence::{Anchor, Attestation, Grade, SignedWitness};
use crate::spec::{ClauseKind, Obligation, SignedSpec};
use crate::{Address, Energy, Error, Provenance, worst_provenance};
/// The artifact state a specification is evaluated against.
///
/// The whole-state address is what a witness binds to exactly. `parts` is the
/// set of addresses the state is composed of, where the caller can enumerate
/// them — file digests, module digests, build-input addresses. It is what lets
/// a narrowed witness survive a change it did not depend on
/// ([`crate::evidence::Witness::applies_at`]).
///
/// Paths are deliberately absent: a content address *is* the identity of its
/// content, so membership answers "is this input still what the evidence saw"
/// without the standard having to agree with anyone about file naming.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct ArtifactState {
/// The address of the whole state.
pub address: Address,
/// The addresses it is composed of, where they can be enumerated. Empty
/// means only the whole-state address is known, and every narrowed witness
/// is then stale.
pub parts: std::collections::BTreeSet<Address>,
}
impl ArtifactState {
/// A state known only by its whole-tree address.
#[must_use]
pub fn whole(address: Address) -> Self {
Self { address, parts: std::collections::BTreeSet::new() }
}
/// A state whose parts the caller can enumerate.
pub fn new(address: Address, parts: impl IntoIterator<Item = Address>) -> Self {
Self { address, parts: parts.into_iter().collect() }
}
}
/// One unit of work performed against a specification: a coding operation, a
/// build, a benchmark run.
///
@ -64,12 +130,21 @@ pub struct Work {
pub cites: Vec<Obligation>,
/// What the work cost.
pub energy: Energy,
/// The party that performed it. A witness signed by one of these keys is
/// self-attested, which is how the attestation axis is derived rather than
/// declared.
pub author: [u8; 32],
}
impl Work {
/// A work unit.
pub fn new(id: Address, cites: Vec<Obligation>, energy: Energy) -> Self {
Self { id, cites, energy }
pub fn new(
id: Address,
cites: Vec<Obligation>,
energy: Energy,
author: [u8; 32],
) -> Self {
Self { id, cites, energy, author }
}
}
@ -126,6 +201,15 @@ pub struct ClauseVerdict {
/// The witness carrying that grade — lowest address among ties, so the
/// verdict is reproducible.
pub best: Option<Address>,
/// The kind of the evidence carrying the grade. Two clauses at `E2` can
/// be a green check and a proof whose statement nobody tied to the clause;
/// a grade alone cannot tell them apart.
pub means: Option<String>,
/// The anchor that evidence declared, where its kind has one.
pub anchor: Option<Anchor>,
/// How independent the parties behind the surviving evidence are. `None`
/// when no work was supplied, so no implementer is known.
pub attestation: Option<Attestation>,
/// Witnesses for this obligation bound to some *other* artifact state.
/// Evidence that was true once and says nothing about now.
pub stale: Vec<Address>,
@ -162,22 +246,42 @@ pub struct Conformance {
pub specified_uj: u64,
/// Energy spent on work that cites none of them.
pub unspecified_uj: u64,
/// The work units that cite no obligation of this specification, named.
/// Unintended function is what backward traceability exists to exclude,
/// and a figure cannot be acted on.
pub unspecified: Vec<Address>,
/// Energy spent producing the surviving evidence.
pub evidence_uj: u64,
/// The weakest provenance across every figure contributing above.
pub provenance: Option<Provenance>,
/// The weakest attestation across the owed obligations — the second axis
/// of the verdict. `None` when no work was supplied, or when any owed
/// obligation has no surviving evidence.
pub attestation: Option<Attestation>,
}
impl Conformance {
/// Whether every owed obligation reaches `min` and the evidence set is
/// clean.
/// Whether every owed obligation reaches both bars and the evidence set
/// is clean.
///
/// Flags block conformance regardless of grade: a specification whose
/// Both axes gate, because they fail separately: a proof nobody
/// independent of the implementer ever saw and a citation from an
/// independent auditor are each strong on one axis and weak on the other.
/// An absent attestation — no work supplied, so no implementer known —
/// cannot satisfy a bar above [`Attestation::SelfAttested`].
///
/// Flags block conformance regardless of either: a specification whose
/// non-goal somebody implemented has a problem no amount of evidence
/// elsewhere settles.
#[must_use]
pub fn is_conformant(&self, min: Grade) -> bool {
self.flags.is_empty() && self.grade.is_some_and(|g| g >= min)
pub fn is_conformant(&self, min: Grade, min_attestation: Attestation) -> bool {
if !self.flags.is_empty() || !self.grade.is_some_and(|g| g >= min) {
return false;
}
match self.attestation {
Some(a) => a >= min_attestation,
None => min_attestation == Attestation::SelfAttested,
}
}
/// The owed obligations that do not reach `min`, in clause order.
@ -219,6 +323,25 @@ impl Conformance {
/// per-unit figures count accepted tokens and verified proofs rather than
/// attempts. `None` when nothing reaches the bar: a cost per unit of
/// nothing is not a small number, it is not a number.
///
/// # Comparable only at a fixed specification
///
/// Any figure of the form *things evidenced over things total* can be
/// improved by adding trivial things — the known objection to counting
/// resolved doubts in assurance argumentation, where one can inflate
/// confidence by raising and dismissing easy ones. Here the denominator is
/// the clause count, so splitting one requirement into twenty trivially
/// falsifiable ones divides the figure by twenty while establishing
/// nothing new.
///
/// The figure is therefore comparable **only between evaluations carrying
/// the same `spec_id`**, which is the comparison it exists for: two
/// processes against one specification. A receipt seals the specification's
/// address precisely so that a reader can tell whether two figures are
/// comparable at all.
///
/// The grade is not gameable this way, and in the opposite direction:
/// adding a clause can only lower a minimum.
#[must_use]
pub fn uj_per_evidenced_clause(&self, min: Grade) -> Option<u64> {
let n = self
@ -243,7 +366,7 @@ impl Conformance {
/// flag.
pub fn evaluate(
spec: &SignedSpec,
artifact: &Address,
state: &ArtifactState,
witnesses: &[SignedWitness],
work: &[Work],
) -> Result<Conformance, Error> {
@ -258,6 +381,9 @@ pub fn evaluate(
kind: *kind,
grade: None,
best: None,
means: None,
anchor: None,
attestation: None,
stale: Vec::new(),
evidence_uj: 0,
provenance: None,
@ -269,6 +395,19 @@ pub fn evaluate(
let mut flags = Vec::new();
let mut evidence_provenances = Vec::new();
// Who did the work. A witness signed by one of these keys reports on its
// own work; with no work supplied, nobody is known to be an implementer
// and the axis stays absent rather than defaulting to independent.
let implementers: std::collections::BTreeSet<[u8; 32]> =
work.iter().map(|w| w.author).collect();
// (clause slot, check, grade) -> the distinct authors that reported it.
// Two disjoint parties reporting the same check at the same state is
// reproduction, and it is computed here rather than claimed.
let mut reports: std::collections::BTreeMap<
(usize, String, Grade),
std::collections::BTreeSet<[u8; 32]>,
> = std::collections::BTreeMap::new();
for (i, signed) in witnesses.iter().enumerate() {
let Ok(witness_id) = signed.verify() else {
flags.push(Flag::Unverifiable { index: i as u64 });
@ -286,7 +425,7 @@ pub fn evaluate(
});
continue;
};
if &w.artifact != artifact {
if !w.applies_at(state) {
verdicts[slot].stale.push(witness_id);
continue;
}
@ -303,6 +442,28 @@ pub fn evaluate(
}
let grade = w.grade();
if let Some(check) = w.evidence.check() {
reports
.entry((slot, check.to_string(), grade))
.or_default()
.insert(w.author);
}
// An independent witness is one whose author did none of the work.
let attestation = if implementers.is_empty() {
None
} else if implementers.contains(&w.author) {
Some(Attestation::SelfAttested)
} else {
Some(Attestation::Independent)
};
verdict.attestation = match (verdict.attestation, attestation) {
// The strongest attestation among the surviving evidence, and
// absent if any contributing figure leaves it unknown.
(Some(current), Some(new)) => Some(current.max(new)),
(None, new) if verdict.grade.is_none() => new,
(current, _) => current,
};
// Strongest grade wins; the lowest address breaks a tie so two runs
// over the same inputs name the same witness.
let replace = match (verdict.grade, &verdict.best) {
@ -315,6 +476,8 @@ pub fn evaluate(
if replace {
verdict.grade = Some(grade);
verdict.best = Some(witness_id);
verdict.means = Some(w.evidence.label().to_string());
verdict.anchor = w.evidence.anchor();
}
verdict.evidence_uj = verdict.evidence_uj.saturating_add(w.energy.uj);
verdict.provenance = Some(match verdict.provenance {
@ -324,6 +487,20 @@ pub fn evaluate(
evidence_provenances.push(w.energy.provenance);
}
// Reproduction: two parties with disjoint keys reported the same check at
// the same grade, at least one of them independent of the work. Strictly
// stronger than a lone independent report, which is why it ranks above it.
for ((slot, _, _), authors) in &reports {
if authors.len() < 2 {
continue;
}
let any_independent =
!implementers.is_empty() && authors.iter().any(|a| !implementers.contains(a));
if any_independent {
verdicts[*slot].attestation = Some(Attestation::Reproduced);
}
}
for verdict in &mut verdicts {
verdict.stale.sort();
}
@ -338,6 +515,7 @@ pub fn evaluate(
let mut specified_uj = 0u64;
let mut unspecified_uj = 0u64;
let mut unspecified = Vec::new();
let mut work_provenances = Vec::new();
for unit in work {
let specified = unit.cites.iter().any(|o| index.contains_key(o));
@ -345,36 +523,52 @@ pub fn evaluate(
specified_uj = specified_uj.saturating_add(unit.energy.uj);
} else {
unspecified_uj = unspecified_uj.saturating_add(unit.energy.uj);
unspecified.push(unit.id.clone());
}
work_provenances.push(unit.energy.provenance);
}
unspecified.sort();
unspecified.dedup();
let evidence_uj = verdicts.iter().map(|c| c.evidence_uj).fold(0u64, u64::saturating_add);
let provenance =
worst_provenance(evidence_provenances.into_iter().chain(work_provenances));
let attestation = verdicts
.iter()
.filter(|c| c.kind.is_owed())
.map(|c| c.attestation)
.min()
.unwrap_or(None);
Ok(Conformance {
spec_id,
artifact: artifact.clone(),
artifact: state.address.clone(),
clauses: verdicts,
grade,
flags,
specified_uj,
unspecified_uj,
unspecified,
evidence_uj,
provenance,
attestation,
})
}
#[cfg(test)]
mod tests {
use super::*;
use crate::evidence::{Evidence, Witness};
use crate::evidence::{Anchor, Evidence, Formalization, Grounding, Vacuity, Witness};
use crate::spec::fixtures::{key, spec};
use ed25519_dalek::SigningKey;
fn artifact() -> Address {
Address::of_bytes(b"artifact-v1")
const IMPL: u8 = 1;
const AUDITOR: u8 = 2;
const OTHER_AUDITOR: u8 = 3;
fn state() -> ArtifactState {
ArtifactState::whole(Address::of_bytes(b"artifact-v1"))
}
fn witness_for(
@ -408,92 +602,187 @@ mod tests {
fn falsifiable(check: &str) -> Evidence {
Evidence::Falsifiable {
check: check.into(),
anchor: Anchor::Specification,
counter: Address::of_bytes(b"mutant"),
}
}
fn exercised(check: &str) -> Evidence {
Evidence::Exercised { check: check.into(), anchor: Anchor::Specification }
}
/// Work by the implementer, citing `labels`.
fn work_for(spec: &SignedSpec, labels: &[&str], uj: u64) -> Work {
let cites = labels
.iter()
.map(|l| {
spec.spec
.clauses
.iter()
.find(|c| &c.label == l)
.unwrap()
.obligation()
.unwrap()
})
.collect();
Work::new(
Address::of_bytes(format!("op-{}", labels.join("-")).as_bytes()),
cites,
Energy::new(uj, Provenance::HwShunt),
key(IMPL).verifying_key().to_bytes(),
)
}
// ── the cap ─────────────────────────────────────────────────────────
#[test]
fn a_specification_is_graded_by_its_weakest_owed_obligation() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let st = state();
let ws = vec![
witness_for(&s, "C1", &a, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C2", &a, Evidence::Cited, 10, &k),
witness_for(&s, "C1", &st.address, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C2", &st.address, Evidence::Cited, 10, &k),
];
let c = evaluate(&s, &a, &ws, &[]).unwrap();
let c = evaluate(&s, &st, &ws, &[]).unwrap();
assert_eq!(c.grade, Some(Grade::Cited), "one cited clause caps the whole specification");
assert_eq!(c.clauses[0].grade, Some(Grade::Falsifiable));
assert_eq!(c.clauses[1].grade, Some(Grade::Cited));
assert!(!c.is_conformant(Grade::Exercised));
assert!(c.is_conformant(Grade::Cited));
assert!(!c.is_conformant(Grade::Exercised, Attestation::SelfAttested));
assert!(c.is_conformant(Grade::Cited, Attestation::SelfAttested));
assert_eq!(c.open(Grade::Exercised).len(), 1);
assert_eq!(c.open(Grade::Exercised)[0].label, "C2");
}
#[test]
fn an_unwitnessed_requirement_leaves_the_specification_ungraded() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let ws = vec![witness_for(&s, "C1", &a, falsifiable("rejects_anon"), 900, &k)];
let c = evaluate(&s, &a, &ws, &[]).unwrap();
let st = state();
let ws = vec![witness_for(&s, "C1", &st.address, falsifiable("rejects_anon"), 900, &k)];
let c = evaluate(&s, &st, &ws, &[]).unwrap();
assert_eq!(c.grade, None, "C2 has no evidence at all");
assert!(!c.is_conformant(Grade::Cited));
assert!(!c.is_conformant(Grade::Cited, Attestation::SelfAttested));
assert_eq!(c.open(Grade::Cited).len(), 1);
}
#[test]
fn a_non_goal_never_counts_as_coverage_and_never_blocks_the_grade() {
let k = key(1);
fn adding_a_clause_can_only_lower_the_grade() {
// The anti-gaming direction: a minimum cannot be improved by adding
// obligations, which is what makes the grade sound where a ratio is
// not.
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
// C3 is the non-goal. Nothing witnesses it, and that is correct.
let st = state();
let ws = vec![
witness_for(&s, "C1", &a, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C2", &a, falsifiable("decided_first"), 800, &k),
witness_for(&s, "C1", &st.address, falsifiable("a"), 10, &k),
witness_for(&s, "C2", &st.address, falsifiable("b"), 10, &k),
];
let c = evaluate(&s, &a, &ws, &[]).unwrap();
let before = evaluate(&s, &st, &ws, &[]).unwrap();
assert_eq!(before.grade, Some(Grade::Falsifiable));
let mut wider = s.spec.revise(k.verifying_key().to_bytes()).unwrap();
wider.clauses.push(crate::spec::Clause::requirement("C9", "Something unevidenced."));
let wider = wider.sign(&k).unwrap();
let after = evaluate(&wider, &st, &[], &[]).unwrap();
assert_eq!(after.grade, None);
}
// ── non-goals and flags ─────────────────────────────────────────────
#[test]
fn a_non_goal_never_counts_as_coverage_and_never_blocks_the_grade() {
let k = key(IMPL);
let s = spec(&k);
let st = state();
let ws = vec![
witness_for(&s, "C1", &st.address, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C2", &st.address, falsifiable("decided_first"), 800, &k),
];
let c = evaluate(&s, &st, &ws, &[]).unwrap();
assert_eq!(c.grade, Some(Grade::Falsifiable));
assert!(c.flags.is_empty());
assert!(c.is_conformant(Grade::Falsifiable));
assert!(c.is_conformant(Grade::Falsifiable, Attestation::SelfAttested));
}
#[test]
fn evidence_that_a_non_goal_was_built_is_a_flag_that_blocks_conformance() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let st = state();
let ws = vec![
witness_for(&s, "C1", &a, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C2", &a, falsifiable("decided_first"), 800, &k),
witness_for(&s, "C3", &a, Evidence::Exercised { check: "retry_backoff".into() }, 50, &k),
witness_for(&s, "C1", &st.address, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C2", &st.address, falsifiable("decided_first"), 800, &k),
witness_for(&s, "C3", &st.address, exercised("retry_backoff"), 50, &k),
];
let c = evaluate(&s, &a, &ws, &[]).unwrap();
let c = evaluate(&s, &st, &ws, &[]).unwrap();
assert_eq!(c.grade, Some(Grade::Falsifiable), "the owed clauses are still well evidenced");
assert!(
matches!(c.flags.as_slice(), [Flag::NonGoalWitnessed { label, .. }] if label == "C3")
);
assert!(
!c.is_conformant(Grade::Falsifiable),
"a flag blocks conformance however good the rest of the evidence is"
);
assert!(!c.is_conformant(Grade::Falsifiable, Attestation::SelfAttested));
}
#[test]
fn a_mis_bound_witness_is_a_finding_not_a_no_op() {
let k = key(IMPL);
let s = spec(&k);
let st = state();
let stray = Witness::new(
s.spec.spec_id().unwrap(),
crate::spec::Clause::requirement("C9", "A clause this specification never stated.")
.obligation()
.unwrap(),
st.address.clone(),
Evidence::Cited,
Energy::estimated(5),
k.verifying_key().to_bytes(),
)
.sign(&k)
.unwrap();
let c = evaluate(&s, &st, &[stray], &[]).unwrap();
assert!(matches!(c.flags.as_slice(), [Flag::Unbound { .. }]));
}
#[test]
fn a_witness_for_another_specification_is_flagged() {
let k = key(IMPL);
let s = spec(&k);
let st = state();
let mut foreign = witness_for(&s, "C1", &st.address, Evidence::Cited, 5, &k);
foreign.witness.spec_id = Address::of_bytes(b"some-other-spec");
let foreign = foreign.witness.clone().sign(&k).unwrap();
let c = evaluate(&s, &st, &[foreign], &[]).unwrap();
assert!(matches!(c.flags.as_slice(), [Flag::ForeignSpec { .. }]));
}
#[test]
fn an_unverifiable_witness_is_reported_by_position() {
let k = key(IMPL);
let s = spec(&k);
let st = state();
let mut tampered = witness_for(&s, "C1", &st.address, Evidence::Cited, 5, &k);
tampered.sig = vec![0u8; 64];
let c = evaluate(&s, &st, &[tampered], &[]).unwrap();
assert_eq!(c.flags, vec![Flag::Unverifiable { index: 0 }]);
}
// ── staleness and the footprint ─────────────────────────────────────
#[test]
fn evidence_from_another_artifact_state_is_stale_not_counted() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let old = Address::of_bytes(b"artifact-v0");
let new = artifact();
let st = state();
let ws = vec![
witness_for(&s, "C1", &old, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C2", &new, falsifiable("decided_first"), 800, &k),
witness_for(&s, "C2", &st.address, falsifiable("decided_first"), 800, &k),
];
let c = evaluate(&s, &new, &ws, &[]).unwrap();
let c = evaluate(&s, &st, &ws, &[]).unwrap();
assert_eq!(c.clauses[0].grade, None);
assert_eq!(c.clauses[0].stale.len(), 1, "reported, not dropped");
@ -502,122 +791,258 @@ mod tests {
}
#[test]
fn a_mis_bound_witness_is_a_finding_not_a_no_op() {
let k = key(1);
fn a_narrowed_witness_survives_a_change_outside_its_footprint() {
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let stray = Witness::new(
s.spec.spec_id().unwrap(),
crate::spec::Clause::requirement("C9", "A clause this specification never stated.")
let auth = Address::of_bytes(b"auth@v1");
let decide = Address::of_bytes(b"decide@v1");
let doc_v1 = Address::of_bytes(b"docs@v1");
let mk = |label: &str, dep: &Address, check: &str| {
let obligation = s
.spec
.clauses
.iter()
.find(|c| c.label == label)
.unwrap()
.obligation()
.unwrap(),
a.clone(),
Evidence::Cited,
Energy::estimated(5),
k.verifying_key().to_bytes(),
)
.sign(&k)
.unwrap();
let c = evaluate(&s, &a, &[stray], &[]).unwrap();
assert!(matches!(c.flags.as_slice(), [Flag::Unbound { .. }]));
.unwrap();
Witness::new(
s.spec.spec_id().unwrap(),
obligation,
Address::of_bytes(b"tree-v1"),
falsifiable(check),
Energy::new(500, Provenance::HwShunt),
k.verifying_key().to_bytes(),
)
.with_footprint([dep.clone()])
.sign(&k)
.unwrap()
};
let ws = vec![mk("C1", &auth, "rejects_anon"), mk("C2", &decide, "decided_first")];
// The whole tree moved because the docs changed.
let after_docs = ArtifactState::new(
Address::of_bytes(b"tree-v2"),
[auth.clone(), decide.clone(), Address::of_bytes(b"docs@v2")],
);
let c = evaluate(&s, &after_docs, &ws, &[]).unwrap();
assert_eq!(
c.grade,
Some(Grade::Falsifiable),
"a documentation edit must not expire every piece of evidence"
);
assert!(c.clauses.iter().all(|v| v.stale.is_empty()));
// Now auth.rs itself changed: that clause, and only that clause, ages.
let after_auth = ArtifactState::new(
Address::of_bytes(b"tree-v3"),
[Address::of_bytes(b"auth@v2"), decide, doc_v1],
);
let c = evaluate(&s, &after_auth, &ws, &[]).unwrap();
assert_eq!(c.clauses[0].grade, None, "C1 depended on what changed");
assert_eq!(c.clauses[0].stale.len(), 1);
assert_eq!(c.clauses[1].grade, Some(Grade::Falsifiable), "C2 did not");
assert_eq!(c.grade, None);
}
#[test]
fn a_witness_for_another_specification_is_flagged() {
let k = key(1);
let s = spec(&k);
let a = artifact();
let mut foreign = witness_for(&s, "C1", &a, Evidence::Cited, 5, &k);
foreign.witness.spec_id = Address::of_bytes(b"some-other-spec");
let foreign = foreign.witness.clone().sign(&k).unwrap();
let c = evaluate(&s, &a, &[foreign], &[]).unwrap();
assert!(matches!(c.flags.as_slice(), [Flag::ForeignSpec { .. }]));
}
// ── the attestation axis ────────────────────────────────────────────
#[test]
fn an_unverifiable_witness_is_reported_by_position() {
let k = key(1);
fn evidence_from_the_party_that_did_the_work_is_self_attested() {
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let mut tampered = witness_for(&s, "C1", &a, Evidence::Cited, 5, &k);
tampered.sig = vec![0u8; 64];
let c = evaluate(&s, &a, &[tampered], &[]).unwrap();
assert_eq!(c.flags, vec![Flag::Unverifiable { index: 0 }]);
}
#[test]
fn the_strongest_surviving_witness_sets_the_grade() {
let k = key(1);
let s = spec(&k);
let a = artifact();
let st = state();
let ws = vec![
witness_for(&s, "C1", &a, Evidence::Cited, 5, &k),
witness_for(&s, "C1", &a, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C2", &a, falsifiable("decided_first"), 800, &k),
witness_for(&s, "C1", &st.address, falsifiable("a"), 10, &k),
witness_for(&s, "C2", &st.address, falsifiable("b"), 10, &k),
];
let c = evaluate(&s, &a, &ws, &[]).unwrap();
assert_eq!(c.clauses[0].grade, Some(Grade::Falsifiable));
assert_eq!(c.clauses[0].evidence_uj, 905, "every surviving witness cost something");
let work = vec![work_for(&s, &["C1", "C2"], 1_000)];
let c = evaluate(&s, &st, &ws, &work).unwrap();
assert_eq!(c.grade, Some(Grade::Falsifiable));
assert_eq!(c.attestation, Some(Attestation::SelfAttested));
assert!(
!c.is_conformant(Grade::Falsifiable, Attestation::Independent),
"strong on one axis, weakest on the other -- the gate must hold"
);
assert!(c.is_conformant(Grade::Falsifiable, Attestation::SelfAttested));
}
#[test]
fn work_citing_nothing_is_counted_against_the_specified_share() {
let k = key(1);
let s = spec(&k);
let a = artifact();
let c1 = s.spec.clauses[0].obligation().unwrap();
let work = vec![
Work::new(Address::of_bytes(b"op1"), vec![c1], Energy::new(750_000, Provenance::HwShunt)),
Work::new(Address::of_bytes(b"op2"), vec![], Energy::new(250_000, Provenance::HwShunt)),
fn a_witness_from_a_key_that_did_no_work_is_independent() {
let implementer = key(IMPL);
let auditor = key(AUDITOR);
let s = spec(&implementer);
let st = state();
let ws = vec![
witness_for(&s, "C1", &st.address, falsifiable("a"), 10, &auditor),
witness_for(&s, "C2", &st.address, falsifiable("b"), 10, &auditor),
];
let c = evaluate(&s, &a, &[], &work).unwrap();
let work = vec![work_for(&s, &["C1", "C2"], 1_000)];
let c = evaluate(&s, &st, &ws, &work).unwrap();
assert_eq!(c.attestation, Some(Attestation::Independent));
assert!(c.is_conformant(Grade::Falsifiable, Attestation::Independent));
}
#[test]
fn two_disjoint_parties_reporting_one_check_is_reproduction() {
let implementer = key(IMPL);
let auditor = key(AUDITOR);
let s = spec(&implementer);
let st = state();
let ws = vec![
// C1: the implementer ran it, and an independent party agreed.
witness_for(&s, "C1", &st.address, falsifiable("a"), 10, &implementer),
witness_for(&s, "C1", &st.address, falsifiable("a"), 10, &auditor),
witness_for(&s, "C2", &st.address, falsifiable("b"), 10, &auditor),
];
let work = vec![work_for(&s, &["C1", "C2"], 1_000)];
let c = evaluate(&s, &st, &ws, &work).unwrap();
assert_eq!(c.clauses[0].attestation, Some(Attestation::Reproduced));
assert_eq!(c.clauses[1].attestation, Some(Attestation::Independent));
assert_eq!(c.attestation, Some(Attestation::Independent), "the weakest owed clause again");
}
#[test]
fn agreement_among_implementers_alone_is_not_reproduction() {
let implementer = key(IMPL);
let colleague = key(OTHER_AUDITOR);
let s = spec(&implementer);
let st = state();
let ws = vec![
witness_for(&s, "C1", &st.address, falsifiable("a"), 10, &implementer),
witness_for(&s, "C1", &st.address, falsifiable("a"), 10, &colleague),
witness_for(&s, "C2", &st.address, falsifiable("b"), 10, &implementer),
];
// Both keys authored work, so neither is independent of it.
let mut work = vec![work_for(&s, &["C1", "C2"], 1_000)];
work.push(Work::new(
Address::of_bytes(b"op-2"),
vec![s.spec.clauses[0].obligation().unwrap()],
Energy::estimated(5),
colleague.verifying_key().to_bytes(),
));
let c = evaluate(&s, &st, &ws, &work).unwrap();
assert_eq!(c.clauses[0].attestation, Some(Attestation::SelfAttested));
}
#[test]
fn with_no_work_supplied_independence_is_absent_not_assumed() {
let k = key(IMPL);
let s = spec(&k);
let st = state();
let ws = vec![
witness_for(&s, "C1", &st.address, falsifiable("a"), 10, &key(AUDITOR)),
witness_for(&s, "C2", &st.address, falsifiable("b"), 10, &key(AUDITOR)),
];
let c = evaluate(&s, &st, &ws, &[]).unwrap();
assert_eq!(c.attestation, None, "nobody is known to have implemented anything");
assert!(
!c.is_conformant(Grade::Falsifiable, Attestation::Independent),
"an absent axis cannot satisfy a bar above the floor"
);
assert!(c.is_conformant(Grade::Falsifiable, Attestation::SelfAttested));
}
// ── the means and the anchor travel with the grade ──────────────────
#[test]
fn two_clauses_at_one_grade_can_be_told_apart() {
let k = key(IMPL);
let s = spec(&k);
let st = state();
let deficient_proof = Evidence::Proved {
goal: Address::of_bytes(b"goal"),
tier: "T1".into(),
formalization: Formalization {
statement: "p".into(),
grounding: Grounding::Declared,
},
vacuity: Vacuity::Unchecked,
};
let ws = vec![
witness_for(&s, "C1", &st.address, exercised("smoke"), 10, &k),
witness_for(&s, "C2", &st.address, deficient_proof, 10, &k),
];
let c = evaluate(&s, &st, &ws, &[]).unwrap();
assert_eq!(c.clauses[0].grade, Some(Grade::Exercised));
assert_eq!(c.clauses[1].grade, Some(Grade::Exercised));
assert_eq!(c.clauses[0].means.as_deref(), Some("exercised"));
assert_eq!(c.clauses[1].means.as_deref(), Some("proved"));
assert_eq!(c.clauses[0].anchor, Some(Anchor::Specification));
assert_eq!(c.clauses[1].anchor, None, "a proof declares no oracle anchor");
}
// ── cost ────────────────────────────────────────────────────────────
#[test]
fn work_citing_nothing_is_named_as_well_as_counted() {
let k = key(IMPL);
let s = spec(&k);
let st = state();
let stray = Work::new(
Address::of_bytes(b"op-unasked"),
vec![],
Energy::new(250_000, Provenance::HwShunt),
k.verifying_key().to_bytes(),
);
let work = vec![work_for(&s, &["C1"], 750_000), stray];
let c = evaluate(&s, &st, &[], &work).unwrap();
assert_eq!(c.specified_uj, 750_000);
assert_eq!(c.unspecified_uj, 250_000);
assert_eq!(c.specified_ppm(), Some(750_000), "three quarters of the energy was asked for");
assert_eq!(c.specified_ppm(), Some(750_000));
assert_eq!(
c.unspecified,
vec![Address::of_bytes(b"op-unasked")],
"which work implements nothing is the actionable half"
);
}
#[test]
fn work_citing_an_obligation_this_specification_lacks_is_unspecified() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let elsewhere = crate::spec::Clause::requirement("X", "Something else.")
.obligation()
.unwrap();
let elsewhere =
crate::spec::Clause::requirement("X", "Something else.").obligation().unwrap();
let work = vec![Work::new(
Address::of_bytes(b"op1"),
vec![elsewhere],
Energy::estimated(1_000),
k.verifying_key().to_bytes(),
)];
let c = evaluate(&s, &a, &[], &work).unwrap();
let c = evaluate(&s, &state(), &[], &work).unwrap();
assert_eq!(c.specified_uj, 0);
assert_eq!(c.unspecified_uj, 1_000);
assert_eq!(c.specified_ppm(), Some(0));
assert_eq!(c.unspecified.len(), 1);
}
#[test]
fn a_ratio_with_no_work_is_absent_rather_than_zero() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let c = evaluate(&s, &artifact(), &[], &[]).unwrap();
let c = evaluate(&s, &state(), &[], &[]).unwrap();
assert_eq!(c.specified_ppm(), None, "no work is not zero specified work");
assert_eq!(c.uj_per_evidenced_clause(Grade::Falsifiable), None);
assert!(c.unspecified.is_empty());
}
#[test]
fn the_wedge_figure_counts_only_obligations_whose_evidence_can_fail() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let st = state();
let ws = vec![
witness_for(&s, "C1", &a, falsifiable("rejects_anon"), 1_000, &k),
witness_for(&s, "C2", &a, Evidence::Exercised { check: "smoke".into() }, 1_000, &k),
witness_for(&s, "C1", &st.address, falsifiable("rejects_anon"), 1_000, &k),
witness_for(&s, "C2", &st.address, exercised("smoke"), 1_000, &k),
];
let work =
vec![Work::new(Address::of_bytes(b"op"), vec![s.spec.clauses[0].obligation().unwrap()],
Energy::new(98_000, Provenance::HwShunt))];
let c = evaluate(&s, &a, &ws, &work).unwrap();
let work = vec![work_for(&s, &["C1"], 98_000)];
let c = evaluate(&s, &st, &ws, &work).unwrap();
assert_eq!(c.total_uj(), 100_000);
assert_eq!(
@ -634,33 +1059,36 @@ mod tests {
#[test]
fn an_aggregate_is_graded_by_the_weakest_figure_that_fed_it() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let measured = witness_for(&s, "C1", &a, falsifiable("rejects_anon"), 900, &k);
let mut guessed = witness_for(&s, "C2", &a, falsifiable("decided_first"), 800, &k);
let st = state();
let measured = witness_for(&s, "C1", &st.address, falsifiable("a"), 900, &k);
let mut guessed = witness_for(&s, "C2", &st.address, falsifiable("b"), 800, &k);
guessed.witness.energy = Energy::estimated(800);
let guessed = guessed.witness.clone().sign(&k).unwrap();
let c = evaluate(&s, &a, &[measured, guessed], &[]).unwrap();
let c = evaluate(&s, &st, &[measured, guessed], &[]).unwrap();
assert_eq!(c.provenance, Some(Provenance::Estimator));
assert_eq!(c.clauses[0].provenance, Some(Provenance::HwShunt));
assert_eq!(c.clauses[1].provenance, Some(Provenance::Estimator));
}
// ── determinism ─────────────────────────────────────────────────────
#[test]
fn evaluation_is_deterministic_under_witness_reordering() {
let k = key(1);
let k = key(IMPL);
let s = spec(&k);
let a = artifact();
let st = state();
let mut ws = vec![
witness_for(&s, "C1", &a, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C1", &a, falsifiable("rejects_anon_too"), 900, &k),
witness_for(&s, "C2", &a, Evidence::Cited, 1, &k),
witness_for(&s, "C1", &st.address, falsifiable("rejects_anon"), 900, &k),
witness_for(&s, "C1", &st.address, falsifiable("rejects_anon_too"), 900, &k),
witness_for(&s, "C2", &st.address, Evidence::Cited, 1, &k),
];
let first = evaluate(&s, &a, &ws, &[]).unwrap();
let work = vec![work_for(&s, &["C1"], 10)];
let first = evaluate(&s, &st, &ws, &work).unwrap();
ws.reverse();
let second = evaluate(&s, &a, &ws, &[]).unwrap();
let second = evaluate(&s, &st, &ws, &work).unwrap();
assert_eq!(first, second, "ties break on address, not on input order");
}
}

614
joulespec/joulespec-rs/crates/joulespec-core/src/evidence.rs
View file

@ -33,6 +33,46 @@
//! passing on the real artifact carries information. This is the cheapest
//! strong rung and the one most projects can reach today.
//!
//! ## Every rung above `E2` requires a demonstrated failure
//!
//! That rule is uniform, and it applies to proofs as much as to tests. A
//! formal property can be satisfied *vacuously* — true because nothing in the
//! model ever reaches the condition it guards, so it would hold of almost any
//! implementation. Detecting this is standard practice in model checking and
//! it is cheap relative to the proof itself; one industrial report put the
//! share of specifications initially passing vacuously at around a fifth. So
//! an `E4` claim requires the statement to have been **refuted** against a
//! named counter-model ([`Vacuity`]), exactly as `E3` requires a check to have
//! failed against a counter-artifact.
//!
//! ## Where the expectation comes from
//!
//! A check's ability to fail is not only an empirical question. An oracle
//! whose expected value is derived from the system it is judging cannot
//! disagree with that system when a fault moves the measurement and the
//! expectation together — the comparison cancels, and no input reveals the
//! fault. The defect is in the oracle, not in the inputs, and it is visible
//! from the oracle's construction without running anything.
//!
//! So [`Anchor`] is a declared property of every check: whether its expected
//! values are fixed **outside** the code under test (a specification, a
//! published procedure, a reference table) or flow **from** it. An unstated
//! anchor caps a check at `E2`, because whether the oracle derives its
//! expectation from its subject is knowable at no cost to whoever wrote it. A
//! state-anchored check that killed a counter-artifact really did fail once
//! and reaches `E3` — with its anchor disclosed, because the class of faults
//! it cannot catch is disclosed with it.
//!
//! ## What the equivalent-mutant problem does not cost us
//!
//! Mutation scoring is noisy because a mutant semantically identical to the
//! original cannot be killed, so it depresses a score without indicating any
//! weakness; reported rates run from a few per cent to a third of mutants.
//! `E3` is immune in the direction that matters: it only ever uses a mutant
//! the check **did** kill as positive evidence. An equivalent mutant cannot
//! produce an `E3` witness at all, so the problem that makes scores expensive
//! and contested cannot inflate a grade here.
//!
//! ## Why a machine check outranks a human review
//!
//! The ladder is ordered by *re-checkability*, not by diligence. A review is
@ -50,8 +90,9 @@
//! and neither is accepted at face value: independence is key disjointness,
//! and it is computed here rather than read off a flag the producer set.
//!
//! Normative: SPEC §2.4 (the witness), SPEC §2.5 (the ladder), SPEC §2.6
//! (formalization).
//! Normative: SPEC §2.4 (the witness and its footprint), SPEC §2.5 (the
//! ladder, the demonstrated-failure rule, and anchoring), SPEC §2.6
//! (formalization and vacuity), SPEC §2.8 (attestation).
use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey};
use serde::{Deserialize, Serialize};
@ -104,6 +145,119 @@ impl Grade {
}
}
/// Where a check's expected values come from.
///
/// An oracle anchored to the state of the system it judges is blind to any
/// fault that moves its measurement and its expectation together. That is a
/// property of how the check was written, not of how it was run, so this
/// standard asks for it to be stated rather than inferred.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
#[serde(rename_all = "kebab-case")]
pub enum Anchor {
/// Expected values are fixed outside the code under test — in the
/// specification, a published procedure, a reference table, an
/// independently computed model.
Specification,
/// Expected values flow, directly or indirectly, from the code under
/// test. The check can still fail, and cannot fail for the class of
/// faults that move expectation and measurement together.
State,
/// Not stated. The producer has not said, and this is knowable to them at
/// no cost.
Unstated,
}
impl Anchor {
/// Whether the producer said where the expectation comes from.
#[must_use]
pub const fn is_stated(self) -> bool {
!matches!(self, Self::Unstated)
}
/// The wire label.
#[must_use]
pub const fn label(self) -> &'static str {
match self {
Self::Specification => "specification",
Self::State => "state",
Self::Unstated => "unstated",
}
}
}
/// Whether a formal statement was shown to be capable of failing.
///
/// A property satisfied vacuously — because the model never reaches the
/// condition it guards — holds of almost any implementation. Showing the
/// statement fails against a named counter-model establishes that it is not
/// satisfied by construction.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "kebab-case", tag = "kind")]
pub enum Vacuity {
/// The statement was refuted against this counter-model, so it is not
/// vacuously true.
Refuted {
/// The counter-model the statement failed against.
counter: Address,
},
/// Nobody checked. The proof may hold because the obligation is
/// unreachable rather than because it is met.
Unchecked,
}
impl Vacuity {
/// Whether the statement was shown capable of failing.
#[must_use]
pub const fn is_refuted(&self) -> bool {
matches!(self, Self::Refuted { .. })
}
/// The wire label.
#[must_use]
pub const fn label(&self) -> &'static str {
match self {
Self::Refuted { .. } => "refuted",
Self::Unchecked => "unchecked",
}
}
}
/// Who vouches for a piece of evidence — the axis orthogonal to [`Grade`].
///
/// The strength of a check and the independence of the party reporting it are
/// different questions, and collapsing them loses the one that matters most
/// where the implementer and the reporter are the same process. Supply-chain
/// provenance grades records on exactly this axis and says nothing about
/// whether the software is correct; this standard grades the evidence and
/// needs the other axis beside it.
///
/// This is **derived**, never declared: from whether a witness's author also
/// authored work on this specification, and from whether disjoint parties
/// witnessed the same check at the same artifact state.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
#[serde(rename_all = "kebab-case")]
pub enum Attestation {
/// The party reporting the result is a party that did the work.
SelfAttested,
/// Signed by a key that authored none of the work on this specification.
Independent,
/// Two parties with disjoint keys ran the same named check at the same
/// artifact state and reported the same grade.
Reproduced,
}
impl Attestation {
/// The short wire form (`"A0"` … `"A2"`).
#[must_use]
pub const fn code(self) -> &'static str {
match self {
Self::SelfAttested => "A0",
Self::Independent => "A1",
Self::Reproduced => "A2",
}
}
}
/// How a clause's text was turned into a formal statement.
///
/// This crate never formalizes a clause. A formalization is supplied by
@ -149,12 +303,17 @@ pub enum Evidence {
/// How the check is invoked — a test name, a lint, a conformance
/// vector id. Recorded so a reader can run it again.
check: String,
/// Where the check's expected values come from.
anchor: Anchor,
},
/// A named check passed against the artifact and is on record failing
/// against a counter-artifact.
Falsifiable {
/// The check, as in [`Evidence::Exercised`].
check: String,
/// Where the check's expected values come from. An unstated anchor
/// caps this evidence at `E2`.
anchor: Anchor,
/// The artifact state against which the same check failed — a mutant,
/// a reverted fix, a deliberately broken build.
counter: Address,
@ -169,6 +328,8 @@ pub enum Evidence {
tier: String,
/// The binding from clause prose to formal statement.
formalization: Formalization,
/// Whether the statement was shown to be capable of failing.
vacuity: Vacuity,
},
}
@ -186,14 +347,25 @@ impl Evidence {
if reviewer == author { Grade::Cited } else { Grade::Reviewed }
}
Self::Exercised { .. } => Grade::Exercised,
Self::Falsifiable { .. } => Grade::Falsifiable,
Self::Proved { formalization, .. } => match &formalization.grounding {
Grounding::CrossChecked { by } if by != author => Grade::Proved,
// A proof under a formalization nobody independent read is a
// machine-checked statement of an unverified reading of the
// clause: real, mechanical evidence about *something*.
_ => Grade::Exercised,
},
// A check that killed a counter-artifact has failed once. Whether
// it can fail *structurally* is a different question, answered by
// the anchor — and an anchor the producer did not state is not an
// answer, so it caps here.
Self::Falsifiable { anchor, .. } => {
if anchor.is_stated() { Grade::Falsifiable } else { Grade::Exercised }
}
Self::Proved { formalization, vacuity, .. } => {
let grounded = match &formalization.grounding {
Grounding::CrossChecked { by } => by != author,
Grounding::Declared => false,
};
// Two independent ways a proof can establish nothing about
// the clause: the statement may not be the clause
// (ungrounded), or it may hold of anything (vacuous). Either
// leaves real mechanical evidence about *something*, which is
// E2 — the same rung as a green check, for the same reason.
if grounded && vacuity.is_refuted() { Grade::Proved } else { Grade::Exercised }
}
}
}
@ -201,13 +373,20 @@ impl Evidence {
pub fn validate(&self) -> Result<(), Error> {
match self {
Self::Cited | Self::Reviewed { .. } => Ok(()),
Self::Exercised { check } | Self::Falsifiable { check, .. } => {
Self::Exercised { check, .. } | Self::Falsifiable { check, .. } => {
if check.trim().is_empty() {
return Err(Error::IncompleteEvidence("a check must be named"));
}
Ok(())
}
Self::Proved { tier, formalization, .. } => {
Self::Proved { tier, formalization, vacuity, .. } => {
if let Vacuity::Refuted { counter } = vacuity
&& counter.as_str().is_empty()
{
return Err(Error::IncompleteEvidence(
"a refuted statement must name its counter-model",
));
}
if tier.trim().is_empty() {
return Err(Error::IncompleteEvidence("a proof must name its tier"));
}
@ -231,13 +410,16 @@ impl Evidence {
Self::Reviewed { reviewer } => {
json!({ "kind": self.label(), "reviewer": crate::hex32(reviewer) })
}
Self::Exercised { check } => json!({ "kind": self.label(), "check": check }),
Self::Falsifiable { check, counter } => json!({
Self::Exercised { check, anchor } => {
json!({ "kind": self.label(), "check": check, "anchor": anchor.label() })
}
Self::Falsifiable { check, anchor, counter } => json!({
"kind": self.label(),
"check": check,
"anchor": anchor.label(),
"counter": counter.as_str(),
}),
Self::Proved { goal, tier, formalization } => {
Self::Proved { goal, tier, formalization, vacuity } => {
let mut grounding = serde_json::Map::new();
match &formalization.grounding {
Grounding::Declared => {
@ -248,17 +430,43 @@ impl Evidence {
grounding.insert("by".into(), json!(crate::hex32(by)));
}
}
let mut vac = serde_json::Map::new();
vac.insert("kind".into(), json!(vacuity.label()));
if let Vacuity::Refuted { counter } = vacuity {
vac.insert("counter".into(), json!(counter.as_str()));
}
json!({
"kind": self.label(),
"goal": goal.as_str(),
"tier": tier,
"statement": formalization.statement,
"grounding": Value::Object(grounding),
"vacuity": Value::Object(vac),
})
}
}
}
/// The anchor this evidence declares, where the kind has one.
#[must_use]
pub const fn anchor(&self) -> Option<Anchor> {
match self {
Self::Exercised { anchor, .. } | Self::Falsifiable { anchor, .. } => Some(*anchor),
_ => None,
}
}
/// The named check this evidence ran, where the kind has one. Two
/// witnesses naming the same check are candidates for reproduction.
#[must_use]
pub fn check(&self) -> Option<&str> {
match self {
Self::Exercised { check, .. } | Self::Falsifiable { check, .. } => Some(check),
Self::Proved { goal, .. } => Some(goal.as_str()),
_ => None,
}
}
/// The wire label of the evidence kind.
#[must_use]
pub const fn label(&self) -> &'static str {
@ -279,6 +487,27 @@ impl Evidence {
/// observed, and *what it cost* to observe. The artifact binding is what makes
/// staleness computable — evidence gathered against one state says nothing
/// about another.
///
/// # The footprint, and why the whole tree is the wrong unit
///
/// Binding evidence to a whole-tree digest alone makes every commit stale
/// every witness. That is the documented way traceability dies: the empirical
/// literature finds trace links degrade mainly through ordinary refactoring,
/// and that keeping them current can cost more than creating them. A standard
/// whose evidence expires on every unrelated edit has reproduced that failure
/// exactly, however sound its addressing.
///
/// So a witness also names a **footprint**: the addresses within the artifact
/// the evidence actually depended on. A state that moves without disturbing
/// any footprint member leaves the evidence current ([`Witness::applies_at`]).
/// The higher rungs are the cheapest to refresh anyway — a named check can
/// simply be run again, where a human review cannot.
///
/// A footprint is a producer's claim that nothing else mattered; it is signed
/// with the rest of the witness, and a narrower one is a *stronger* claim, so
/// a wrong footprint makes the evidence wrong rather than merely stale. An
/// **empty** footprint means the whole artifact — the conservative reading,
/// and the one a producer that cannot enumerate its inputs should use.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct Witness {
/// The profile (`joulespec-witness/1`).
@ -293,6 +522,9 @@ pub struct Witness {
/// The artifact state the evidence was observed against: a tree digest, a
/// build output address, a commit.
pub artifact: Address,
/// The addresses within that state the evidence depended on. Empty means
/// the whole artifact, so any change stales the witness.
pub footprint: Vec<Address>,
/// What was observed.
pub evidence: Evidence,
/// What producing this evidence cost, with its provenance.
@ -302,7 +534,8 @@ pub struct Witness {
}
impl Witness {
/// A witness at an artifact state.
/// A witness at an artifact state, with the whole artifact as its
/// footprint.
pub fn new(
spec_id: Address,
obligation: Obligation,
@ -317,12 +550,43 @@ impl Witness {
spec_id,
obligation,
artifact,
footprint: Vec::new(),
evidence,
energy,
author,
}
}
/// Narrow this witness to the inputs the evidence actually depended on.
///
/// The footprint is sorted and deduplicated, so two producers enumerating
/// the same inputs in different orders sign the same witness.
#[must_use]
pub fn with_footprint(mut self, footprint: impl IntoIterator<Item = Address>) -> Self {
let mut parts: Vec<Address> = footprint.into_iter().collect();
parts.sort();
parts.dedup();
self.footprint = parts;
self
}
/// Whether this witness still applies at `state`.
///
/// Exactly at the state it observed, or — where it narrowed itself and the
/// caller can enumerate the current state — where every footprint member
/// is still present. A footprint that cannot be checked is stale, which is
/// the conservative direction.
#[must_use]
pub fn applies_at(&self, state: &crate::conform::ArtifactState) -> bool {
if self.artifact == state.address {
return true;
}
if self.footprint.is_empty() || state.parts.is_empty() {
return false;
}
self.footprint.iter().all(|a| state.parts.contains(a))
}
/// Structural validation.
pub fn validate(&self) -> Result<(), Error> {
if self.profile != WITNESS_PROFILE {
@ -344,6 +608,7 @@ impl Witness {
"spec": self.spec_id.as_str(),
"obligation": self.obligation.as_str(),
"artifact": self.artifact.as_str(),
"footprint": self.footprint.iter().map(Address::as_str).collect::<Vec<_>>(),
"evidence": self.evidence.canonical(),
"energy": json!({
"uj": self.energy.uj,
@ -428,6 +693,36 @@ mod tests {
.unwrap()
}
fn exercised(check: &str, anchor: Anchor) -> Evidence {
Evidence::Exercised { check: check.into(), anchor }
}
fn falsifiable(check: &str, anchor: Anchor) -> Evidence {
Evidence::Falsifiable {
check: check.into(),
anchor,
counter: Address::of_bytes(b"mutant-auth-removed"),
}
}
fn proved(grounding: Grounding, vacuity: Vacuity) -> Evidence {
Evidence::Proved {
goal: Address::of_bytes(b"goal"),
tier: "T1".into(),
formalization: Formalization {
statement: "forall r. !authenticated(r) -> rejected(r)".into(),
grounding,
},
vacuity,
}
}
fn refuted() -> Vacuity {
Vacuity::Refuted { counter: Address::of_bytes(b"counter-model") }
}
// ── the ladder ──────────────────────────────────────────────────────
#[test]
fn the_ladder_is_ordered_from_testimony_to_proof() {
assert!(Grade::Cited < Grade::Reviewed);
@ -436,6 +731,7 @@ mod tests {
assert!(Grade::Falsifiable < Grade::Proved);
assert!(!Grade::Exercised.is_falsifiable(), "a green check may be vacuous");
assert!(Grade::Falsifiable.is_falsifiable());
assert!(Grade::Proved.is_falsifiable());
}
#[test]
@ -450,7 +746,8 @@ mod tests {
fn a_review_by_someone_else_outranks_a_citation() {
let author = key(1);
let reviewer = key(2);
let w = witness(Evidence::Reviewed { reviewer: reviewer.verifying_key().to_bytes() }, &author);
let w =
witness(Evidence::Reviewed { reviewer: reviewer.verifying_key().to_bytes() }, &author);
assert_eq!(w.witness.grade(), Grade::Reviewed);
}
@ -468,49 +765,79 @@ mod tests {
#[test]
fn a_check_that_can_fail_outranks_one_that_merely_passed() {
let k = key(1);
let passed = witness(Evidence::Exercised { check: "rejects_anon".into() }, &k);
let can_fail = witness(
Evidence::Falsifiable {
check: "rejects_anon".into(),
counter: Address::of_bytes(b"mutant-auth-removed"),
},
&k,
);
let passed = witness(exercised("rejects_anon", Anchor::Specification), &k);
let can_fail = witness(falsifiable("rejects_anon", Anchor::Specification), &k);
assert_eq!(passed.witness.grade(), Grade::Exercised);
assert_eq!(can_fail.witness.grade(), Grade::Falsifiable);
}
// ── anchoring ───────────────────────────────────────────────────────
#[test]
fn a_proof_reaches_e4_only_when_its_formalization_was_cross_checked() {
fn an_unstated_anchor_caps_a_falsifiable_check_at_e2() {
let k = key(1);
let w = witness(falsifiable("rejects_anon", Anchor::Unstated), &k);
assert_eq!(
w.witness.grade(),
Grade::Exercised,
"whether the oracle reads its expectation from its subject is \
knowable to whoever wrote it at no cost, so silence caps"
);
}
#[test]
fn a_state_anchored_check_that_killed_a_mutant_still_reaches_e3() {
// It failed once, so it can fail. The class of faults it cannot catch
// is disclosed by the anchor rather than used to refuse the rung.
let k = key(1);
let w = witness(falsifiable("rejects_anon", Anchor::State), &k);
assert_eq!(w.witness.grade(), Grade::Falsifiable);
assert_eq!(w.witness.evidence.anchor(), Some(Anchor::State));
}
#[test]
fn the_anchor_is_part_of_what_the_signature_covers() {
let k = key(1);
let spec_anchored = witness(falsifiable("c", Anchor::Specification), &k);
let state_anchored = witness(falsifiable("c", Anchor::State), &k);
assert_ne!(
spec_anchored.verify().unwrap(),
state_anchored.verify().unwrap(),
"two anchors are two different claims and two different witnesses"
);
}
// ── vacuity ─────────────────────────────────────────────────────────
#[test]
fn a_proof_reaches_e4_only_when_grounded_and_shown_non_vacuous() {
let author = key(1);
let other = key(2);
let proved = |grounding| {
witness(
Evidence::Proved {
goal: Address::of_bytes(b"goal"),
tier: "T1".into(),
formalization: Formalization {
statement: "forall r. !authenticated(r) -> rejected(r)".into(),
grounding,
},
},
&author,
)
};
let other = key(2).verifying_key().to_bytes();
let mine = author.verifying_key().to_bytes();
assert_eq!(
proved(Grounding::CrossChecked { by: other.verifying_key().to_bytes() })
witness(proved(Grounding::CrossChecked { by: other }, refuted()), &author)
.witness
.grade(),
Grade::Proved
);
assert_eq!(
proved(Grounding::Declared).witness.grade(),
witness(proved(Grounding::Declared, refuted()), &author).witness.grade(),
Grade::Exercised,
"the proof is real; that it proves THIS clause is the prover's word"
"non-vacuous, and the statement may still not be this clause"
);
assert_eq!(
proved(Grounding::CrossChecked { by: author.verifying_key().to_bytes() })
witness(
proved(Grounding::CrossChecked { by: other }, Vacuity::Unchecked),
&author
)
.witness
.grade(),
Grade::Exercised,
"the statement is the clause, and may hold of anything"
);
assert_eq!(
witness(proved(Grounding::CrossChecked { by: mine }, refuted()), &author)
.witness
.grade(),
Grade::Exercised,
@ -518,13 +845,146 @@ mod tests {
);
}
#[test]
fn every_rung_above_e2_rests_on_a_demonstrated_failure() {
let author = key(1);
let other = key(2).verifying_key().to_bytes();
// The rule is uniform: a test earns E3 by failing against a mutant, a
// proof earns E4 by failing against a counter-model. Nothing reaches
// either rung on a passing run alone.
for evidence in [
exercised("c", Anchor::Specification),
proved(Grounding::CrossChecked { by: other }, Vacuity::Unchecked),
] {
assert!(
!witness(evidence, &author).witness.grade().is_falsifiable(),
"a rung above E2 must rest on something having failed"
);
}
}
// ── the footprint ───────────────────────────────────────────────────
#[test]
fn a_witness_applies_exactly_at_the_state_it_observed() {
let k = key(1);
let w = witness(Evidence::Cited, &k);
let same = crate::conform::ArtifactState::whole(Address::of_bytes(b"artifact-v1"));
let moved = crate::conform::ArtifactState::whole(Address::of_bytes(b"artifact-v2"));
assert!(w.witness.applies_at(&same));
assert!(!w.witness.applies_at(&moved), "no footprint means the whole tree");
}
#[test]
fn a_narrowed_witness_survives_a_change_it_did_not_depend_on() {
let k = key(1);
let auth_rs = Address::of_bytes(b"src/auth.rs@v1");
let readme = Address::of_bytes(b"README@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_rs.clone()])
.sign(&k)
.unwrap();
// The README moved; auth.rs did not.
let after_readme_edit = crate::conform::ArtifactState::new(
Address::of_bytes(b"tree-v2"),
[auth_rs.clone(), Address::of_bytes(b"README@v2")],
);
assert!(
w.witness.applies_at(&after_readme_edit),
"an unrelated edit must not expire evidence -- this is how traceability dies"
);
// auth.rs moved; the evidence is stale.
let after_auth_edit = crate::conform::ArtifactState::new(
Address::of_bytes(b"tree-v3"),
[Address::of_bytes(b"src/auth.rs@v2"), readme],
);
assert!(!w.witness.applies_at(&after_auth_edit));
}
#[test]
fn a_footprint_that_cannot_be_checked_is_stale() {
let k = key(1);
let part = Address::of_bytes(b"part");
let w = Witness::new(
Address::of_bytes(b"spec"),
obligation(),
Address::of_bytes(b"tree-v1"),
Evidence::Cited,
Energy::estimated(1),
k.verifying_key().to_bytes(),
)
.with_footprint([part])
.sign(&k)
.unwrap();
let opaque = crate::conform::ArtifactState::whole(Address::of_bytes(b"tree-v2"));
assert!(
!w.witness.applies_at(&opaque),
"a caller that cannot enumerate the state gets the conservative answer"
);
}
#[test]
fn a_footprint_is_canonicalised_so_input_order_cannot_change_the_witness() {
let k = key(1);
let a = Address::of_bytes(b"a");
let b = Address::of_bytes(b"b");
let mk = |parts: [Address; 3]| {
Witness::new(
Address::of_bytes(b"spec"),
obligation(),
Address::of_bytes(b"tree"),
Evidence::Cited,
Energy::estimated(1),
k.verifying_key().to_bytes(),
)
.with_footprint(parts)
.witness_id()
.unwrap()
};
assert_eq!(
mk([a.clone(), b.clone(), a.clone()]),
mk([b.clone(), a.clone(), a.clone()]),
"sorted and deduplicated"
);
}
#[test]
fn the_footprint_is_part_of_what_the_signature_covers() {
let k = key(1);
let mut w = Witness::new(
Address::of_bytes(b"spec"),
obligation(),
Address::of_bytes(b"tree"),
Evidence::Cited,
Energy::estimated(1),
k.verifying_key().to_bytes(),
)
.with_footprint([Address::of_bytes(b"narrow")])
.sign(&k)
.unwrap();
// Widening the footprint after signing would let a producer claim
// evidence covered inputs it never read.
w.witness.footprint.push(Address::of_bytes(b"also-this"));
assert!(matches!(w.verify(), Err(Error::BadSignature)));
}
// ── signature binding and structural refusals ───────────────────────
#[test]
fn swapping_the_obligation_under_a_signature_is_caught() {
let k = key(1);
let mut w = witness(Evidence::Cited, &k);
w.witness.obligation = Clause::requirement("C1", "Something else entirely.")
.obligation()
.unwrap();
w.witness.obligation =
Clause::requirement("C1", "Something else entirely.").obligation().unwrap();
assert!(matches!(w.verify(), Err(Error::BadSignature)));
}
@ -539,31 +999,45 @@ mod tests {
#[test]
fn evidence_without_its_payload_is_refused() {
let k = key(1);
let w = Witness::new(
Address::of_bytes(b"spec"),
obligation(),
Address::of_bytes(b"a"),
Evidence::Exercised { check: " ".into() },
Energy::estimated(1),
k.verifying_key().to_bytes(),
);
assert!(matches!(w.validate(), Err(Error::IncompleteEvidence(_))));
let mk = |evidence| {
Witness::new(
Address::of_bytes(b"spec"),
obligation(),
Address::of_bytes(b"a"),
evidence,
Energy::estimated(1),
k.verifying_key().to_bytes(),
)
};
assert!(matches!(
mk(exercised(" ", Anchor::Specification)).validate(),
Err(Error::IncompleteEvidence(_))
));
assert!(matches!(
mk(proved(Grounding::Declared, Vacuity::Unchecked)).validate(),
Ok(())
));
let no_statement = Witness::new(
Address::of_bytes(b"spec"),
obligation(),
Address::of_bytes(b"a"),
Evidence::Proved {
goal: Address::of_bytes(b"g"),
tier: "T1".into(),
formalization: Formalization {
statement: String::new(),
grounding: Grounding::Declared,
},
let no_statement = mk(Evidence::Proved {
goal: Address::of_bytes(b"g"),
tier: "T1".into(),
formalization: Formalization {
statement: String::new(),
grounding: Grounding::Declared,
},
Energy::estimated(1),
k.verifying_key().to_bytes(),
);
vacuity: Vacuity::Unchecked,
});
assert!(matches!(no_statement.validate(), Err(Error::IncompleteEvidence(_))));
let unnamed_counter = mk(Evidence::Proved {
goal: Address::of_bytes(b"g"),
tier: "T1".into(),
formalization: Formalization {
statement: "p".into(),
grounding: Grounding::Declared,
},
vacuity: Vacuity::Refuted { counter: Address::from_string(String::new()) },
});
assert!(matches!(unnamed_counter.validate(), Err(Error::IncompleteEvidence(_))));
}
}

250
joulespec/joulespec-rs/crates/joulespec-core/src/receipt.rs
View file

@ -37,16 +37,23 @@
use ed25519_dalek::SigningKey;
use serde_json::{Map, Value, json};
use crate::conform::{Conformance, Work, evaluate};
use crate::evidence::{Grade, SignedWitness};
use crate::conform::{ArtifactState, Conformance, Work, evaluate};
use crate::evidence::{Attestation, Grade, SignedWitness};
use crate::jcr1;
use crate::spec::SignedSpec;
use crate::{Address, Error, PROFILE};
use crate::{Error, PROFILE};
/// The grade whose evidence can fail, and therefore the denominator of the
/// headline cost figure.
pub const HEADLINE_BAR: Grade = Grade::Falsifiable;
/// The attestation a receipt reports against when counting open obligations.
///
/// The floor, deliberately: the receipt states the attestation it achieved
/// rather than judging it against a bar, because the bar belongs to whoever
/// is relying on the receipt.
pub const HEADLINE_ATTESTATION: Attestation = Attestation::SelfAttested;
/// Build the canonical wire document for an evaluation.
///
/// Public so a verifier in another language can be checked against the same
@ -72,6 +79,18 @@ pub fn wire(conformance: &Conformance, steward: &str) -> Value {
if let Some(grade) = c.grade {
entry.insert("grade".into(), json!(grade.code()));
}
// The means and the anchor travel with the grade: two clauses at
// E2 can be a green check and a proof nobody tied to the clause,
// and a grade alone cannot tell a reader which.
if let Some(means) = &c.means {
entry.insert("means".into(), json!(means));
}
if let Some(anchor) = c.anchor {
entry.insert("anchor".into(), json!(anchor.label()));
}
if let Some(attestation) = c.attestation {
entry.insert("attestation".into(), json!(attestation.code()));
}
if let Some(best) = &c.best {
entry.insert("witness".into(), json!(best.as_str()));
}
@ -90,6 +109,14 @@ pub fn wire(conformance: &Conformance, steward: &str) -> Value {
map.insert("flags".into(), json!(conformance.flags.len()));
map.insert("specified_uj".into(), json!(conformance.specified_uj));
map.insert("unspecified_uj".into(), json!(conformance.unspecified_uj));
// Named, not only counted: unintended function is what backward
// traceability exists to exclude, and a count cannot be acted on.
map.insert(
"unspecified".into(),
Value::Array(
conformance.unspecified.iter().map(|a| json!(a.as_str())).collect::<Vec<_>>(),
),
);
map.insert("evidence_uj".into(), json!(conformance.evidence_uj));
map.insert("steward".into(), json!(steward));
@ -106,6 +133,9 @@ pub fn wire(conformance: &Conformance, steward: &str) -> Value {
if let Some(provenance) = conformance.provenance {
map.insert("provenance".into(), json!(provenance.label()));
}
if let Some(attestation) = conformance.attestation {
map.insert("attestation".into(), json!(attestation.code()));
}
Value::Object(map)
}
@ -116,13 +146,13 @@ pub fn wire(conformance: &Conformance, steward: &str) -> Value {
/// can report the detail while publishing the receipt.
pub fn seal(
spec: &SignedSpec,
artifact: &Address,
state: &ArtifactState,
witnesses: &[SignedWitness],
work: &[Work],
steward: &str,
key: &SigningKey,
) -> Result<(Vec<u8>, Conformance), Error> {
let conformance = evaluate(spec, artifact, witnesses, work)?;
let conformance = evaluate(spec, state, witnesses, work)?;
let core = jcr1::signed_core_bytes(&wire(&conformance, steward))?;
Ok((jcr1::cose_sign1_envelope(&core, key, steward), conformance))
}
@ -137,14 +167,16 @@ pub fn verify(envelope: &[u8], steward: &str, public_key: &[u8; 32]) -> Result<V
mod tests {
use super::*;
use crate::conform::Flag;
use crate::evidence::{Evidence, Witness};
use crate::evidence::{Anchor, Evidence, Formalization, Grounding, Vacuity, Witness};
use crate::spec::fixtures::{key, spec};
use crate::{Energy, Provenance};
use crate::{Address, Energy, Provenance};
const STEWARD: &str = "did:key:z6MkExample";
const IMPL: u8 = 1;
const AUDITOR: u8 = 2;
fn artifact() -> Address {
Address::of_bytes(b"artifact-v1")
fn state() -> ArtifactState {
ArtifactState::whole(Address::of_bytes(b"artifact-v1"))
}
fn witness(
@ -153,8 +185,9 @@ mod tests {
evidence: Evidence,
uj: u64,
provenance: Provenance,
author: u8,
) -> SignedWitness {
let k = key(1);
let k = key(author);
let obligation = s
.spec
.clauses
@ -166,7 +199,7 @@ mod tests {
Witness::new(
s.spec.spec_id().unwrap(),
obligation,
artifact(),
state().address,
evidence,
Energy::new(uj, provenance),
k.verifying_key().to_bytes(),
@ -176,47 +209,58 @@ mod tests {
}
fn falsifiable(check: &str) -> Evidence {
Evidence::Falsifiable { check: check.into(), counter: Address::of_bytes(b"mutant") }
Evidence::Falsifiable {
check: check.into(),
anchor: Anchor::Specification,
counter: Address::of_bytes(b"mutant"),
}
}
fn work(s: &SignedSpec, uj: u64, author: u8) -> Work {
Work::new(
Address::of_bytes(b"op1"),
vec![s.spec.clauses[0].obligation().unwrap()],
Energy::new(uj, Provenance::HwShunt),
key(author).verifying_key().to_bytes(),
)
}
fn fully_evidenced() -> (SignedSpec, Vec<SignedWitness>, Vec<Work>) {
let s = spec(&key(1));
let s = spec(&key(IMPL));
let ws = vec![
witness(&s, "C1", falsifiable("rejects_anon"), 1_000, Provenance::HwShunt),
witness(&s, "C2", falsifiable("decided_first"), 1_000, Provenance::HwShunt),
witness(&s, "C1", falsifiable("rejects_anon"), 1_000, Provenance::HwShunt, AUDITOR),
witness(&s, "C2", falsifiable("decided_first"), 1_000, Provenance::HwShunt, AUDITOR),
];
let work = vec![Work::new(
Address::of_bytes(b"op1"),
vec![s.spec.clauses[0].obligation().unwrap()],
Energy::new(48_000, Provenance::HwShunt),
)];
let work = vec![work(&s, 48_000, IMPL)];
(s, ws, work)
}
#[test]
fn a_sealed_receipt_verifies_and_carries_the_evaluation() {
let (s, ws, work) = fully_evidenced();
let (s, ws, wk) = fully_evidenced();
let k = key(9);
let (env, conformance) =
seal(&s, &artifact(), &ws, &work, STEWARD, &k).expect("seals");
let (env, conformance) = seal(&s, &state(), &ws, &wk, STEWARD, &k).expect("seals");
assert!(conformance.is_conformant(Grade::Falsifiable));
assert!(conformance.is_conformant(Grade::Falsifiable, Attestation::Independent));
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).expect("verifies");
assert_eq!(doc["joulespec_receipt"], json!("joulespec/1"));
assert_eq!(doc["grade"], json!("E3"));
assert_eq!(doc["attestation"], json!("A1"), "both axes are sealed");
assert_eq!(doc["owed"], json!(2));
assert_eq!(doc["open"], json!(0));
assert_eq!(doc["flags"], json!(0));
assert_eq!(doc["provenance"], json!("HwShunt"));
assert_eq!(doc["uj_per_falsifiable_clause"], json!(25_000));
assert_eq!(doc["specified_ppm"], json!(1_000_000));
assert_eq!(doc["unspecified"], json!([]));
// The per-clause audit: a reader finds the weak obligation here
// without holding the original evidence set.
let verdicts = doc["clause_verdicts"].as_array().expect("array");
assert_eq!(verdicts.len(), 3);
assert_eq!(verdicts[0]["label"], json!("C1"));
assert_eq!(verdicts[0]["grade"], json!("E3"));
assert_eq!(verdicts[0]["means"], json!("falsifiable"));
assert_eq!(verdicts[0]["anchor"], json!("specification"));
assert_eq!(verdicts[0]["attestation"], json!("A1"));
assert_eq!(verdicts[0]["evidence_uj"], json!(1_000));
assert_eq!(verdicts[2]["kind"], json!("non-goal"));
assert!(
@ -227,20 +271,20 @@ mod tests {
#[test]
fn a_receipt_is_byte_identical_for_identical_evidence() {
let (s, ws, work) = fully_evidenced();
let (s, ws, wk) = fully_evidenced();
let k = key(9);
let (first, _) = seal(&s, &artifact(), &ws, &work, STEWARD, &k).unwrap();
let (second, _) = seal(&s, &artifact(), &ws, &work, STEWARD, &k).unwrap();
let (first, _) = seal(&s, &state(), &ws, &wk, STEWARD, &k).unwrap();
let (second, _) = seal(&s, &state(), &ws, &wk, STEWARD, &k).unwrap();
assert_eq!(first, second, "the receipt is a function of the evidence");
}
#[test]
fn an_ungraded_specification_omits_the_grade_rather_than_sealing_a_floor() {
let s = spec(&key(1));
// C2 unevidenced.
let ws = vec![witness(&s, "C1", falsifiable("rejects_anon"), 10, Provenance::HwShunt)];
let s = spec(&key(IMPL));
let ws =
vec![witness(&s, "C1", falsifiable("rejects_anon"), 10, Provenance::HwShunt, IMPL)];
let k = key(9);
let (env, conformance) = seal(&s, &artifact(), &ws, &[], STEWARD, &k).unwrap();
let (env, conformance) = seal(&s, &state(), &ws, &[], STEWARD, &k).unwrap();
assert_eq!(conformance.grade, None);
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).unwrap();
@ -248,6 +292,10 @@ mod tests {
doc.get("grade").is_none(),
"a reader must not find a grade where none was established: {doc}"
);
assert!(
doc.get("attestation").is_none(),
"nor an attestation, with no work supplied to derive it from"
);
assert_eq!(doc["open"], json!(1));
let verdicts = doc["clause_verdicts"].as_array().unwrap();
assert_eq!(verdicts[0]["grade"], json!("E3"), "C1 is evidenced");
@ -255,72 +303,160 @@ mod tests {
}
#[test]
fn one_guessed_figure_degrades_the_whole_receipt() {
let s = spec(&key(1));
fn a_self_attested_run_seals_the_weaker_axis() {
let s = spec(&key(IMPL));
let ws = vec![
witness(&s, "C1", falsifiable("rejects_anon"), 1_000, Provenance::HwShunt),
witness(&s, "C2", falsifiable("decided_first"), 1_000, Provenance::Estimator),
witness(&s, "C1", falsifiable("a"), 10, Provenance::HwShunt, IMPL),
witness(&s, "C2", falsifiable("b"), 10, Provenance::HwShunt, IMPL),
];
let wk = vec![work(&s, 1_000, IMPL)];
let k = key(9);
let (env, _) = seal(&s, &artifact(), &ws, &[], STEWARD, &k).unwrap();
let (env, conformance) = seal(&s, &state(), &ws, &wk, STEWARD, &k).unwrap();
assert!(conformance.is_conformant(Grade::Falsifiable, Attestation::SelfAttested));
assert!(!conformance.is_conformant(Grade::Falsifiable, Attestation::Independent));
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).unwrap();
assert_eq!(doc["grade"], json!("E3"));
assert_eq!(
doc["provenance"],
json!("Estimator"),
"a sum containing a guess is a guess"
doc["attestation"],
json!("A0"),
"the party that did the work is the party reporting it, and the receipt says so"
);
}
#[test]
fn a_flagged_evidence_set_seals_the_flag_rather_than_refusing() {
let s = spec(&key(1));
fn a_deficient_proof_is_distinguishable_from_a_green_check_in_the_receipt() {
let s = spec(&key(IMPL));
let deficient = Evidence::Proved {
goal: Address::of_bytes(b"goal"),
tier: "T1".into(),
formalization: Formalization {
statement: "forall r. rejected(r)".into(),
grounding: Grounding::Declared,
},
vacuity: Vacuity::Unchecked,
};
let ws = vec![
witness(&s, "C1", falsifiable("rejects_anon"), 1_000, Provenance::HwShunt),
witness(&s, "C2", falsifiable("decided_first"), 1_000, Provenance::HwShunt),
// Something implements the non-goal.
witness(&s, "C3", Evidence::Exercised { check: "retry".into() }, 10, Provenance::HwShunt),
witness(&s, "C1", Evidence::Exercised { check: "smoke".into(), anchor: Anchor::State }, 10, Provenance::HwShunt, IMPL),
witness(&s, "C2", deficient, 10, Provenance::HwShunt, IMPL),
];
let k = key(9);
let (env, conformance) = seal(&s, &artifact(), &ws, &[], STEWARD, &k).unwrap();
let (env, _) = seal(&s, &state(), &ws, &[], STEWARD, &k).unwrap();
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).unwrap();
let verdicts = doc["clause_verdicts"].as_array().unwrap();
assert_eq!(doc["grade"], json!("E2"), "both clauses land on the same rung");
assert_eq!(verdicts[0]["means"], json!("exercised"));
assert_eq!(verdicts[0]["anchor"], json!("state"), "an oracle reading its own subject");
assert_eq!(verdicts[1]["means"], json!("proved"));
assert!(
verdicts[1].get("anchor").is_none(),
"a proof has no oracle anchor, and the absence is not a default"
);
}
#[test]
fn one_guessed_figure_degrades_the_whole_receipt() {
let s = spec(&key(IMPL));
let ws = vec![
witness(&s, "C1", falsifiable("a"), 1_000, Provenance::HwShunt, IMPL),
witness(&s, "C2", falsifiable("b"), 1_000, Provenance::Estimator, IMPL),
];
let k = key(9);
let (env, _) = seal(&s, &state(), &ws, &[], STEWARD, &k).unwrap();
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).unwrap();
assert_eq!(doc["provenance"], json!("Estimator"), "a sum containing a guess is a guess");
}
#[test]
fn a_flagged_evidence_set_seals_the_flag_rather_than_refusing() {
let s = spec(&key(IMPL));
let ws = vec![
witness(&s, "C1", falsifiable("a"), 1_000, Provenance::HwShunt, IMPL),
witness(&s, "C2", falsifiable("b"), 1_000, Provenance::HwShunt, IMPL),
witness(
&s,
"C3",
Evidence::Exercised { check: "retry".into(), anchor: Anchor::Specification },
10,
Provenance::HwShunt,
IMPL,
),
];
let k = key(9);
let (env, conformance) = seal(&s, &state(), &ws, &[], STEWARD, &k).unwrap();
assert!(matches!(conformance.flags.as_slice(), [Flag::NonGoalWitnessed { .. }]));
assert!(!conformance.is_conformant(Grade::Falsifiable));
assert!(!conformance.is_conformant(Grade::Falsifiable, Attestation::SelfAttested));
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).unwrap();
assert_eq!(doc["flags"], json!(1), "disclosed in the sealed artifact");
assert_eq!(doc["grade"], json!("E3"), "the owed clauses really are evidenced");
}
#[test]
fn unspecified_work_is_named_in_the_receipt() {
let s = spec(&key(IMPL));
let stray = Work::new(
Address::of_bytes(b"op-unasked"),
vec![],
Energy::new(5_000, Provenance::HwShunt),
key(IMPL).verifying_key().to_bytes(),
);
let k = key(9);
let (env, _) =
seal(&s, &state(), &[], &[work(&s, 5_000, IMPL), stray], STEWARD, &k).unwrap();
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).unwrap();
assert_eq!(doc["unspecified_uj"], json!(5_000));
assert_eq!(doc["specified_ppm"], json!(500_000));
assert_eq!(
doc["unspecified"].as_array().unwrap().len(),
1,
"which work implements no clause, by address"
);
}
#[test]
fn a_receipt_cannot_be_sealed_for_an_unsigned_specification() {
let (mut s, ws, work) = fully_evidenced();
let (mut s, ws, wk) = fully_evidenced();
s.sig = vec![0u8; 64];
let k = key(9);
assert!(matches!(
seal(&s, &artifact(), &ws, &work, STEWARD, &k),
seal(&s, &state(), &ws, &wk, STEWARD, &k),
Err(Error::BadSignature)
));
}
#[test]
fn a_receipt_does_not_verify_under_another_steward_or_key() {
let (s, ws, work) = fully_evidenced();
let (s, ws, wk) = fully_evidenced();
let k = key(9);
let (env, _) = seal(&s, &artifact(), &ws, &work, STEWARD, &k).unwrap();
let (env, _) = seal(&s, &state(), &ws, &wk, STEWARD, &k).unwrap();
assert!(verify(&env, "did:key:someone-else", &k.verifying_key().to_bytes()).is_err());
assert!(verify(&env, STEWARD, &key(8).verifying_key().to_bytes()).is_err());
}
#[test]
fn evidence_from_a_stale_artifact_state_cannot_be_sealed_as_current() {
let (s, ws, work) = fully_evidenced();
let (s, ws, wk) = fully_evidenced();
let k = key(9);
// The same witnesses, evaluated against a later artifact state.
let (env, conformance) =
seal(&s, &Address::of_bytes(b"artifact-v2"), &ws, &work, STEWARD, &k).unwrap();
let later = ArtifactState::whole(Address::of_bytes(b"artifact-v2"));
let (env, conformance) = seal(&s, &later, &ws, &wk, STEWARD, &k).unwrap();
assert_eq!(conformance.grade, None, "nothing witnesses the new state");
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).unwrap();
assert!(doc.get("grade").is_none());
assert_eq!(doc["open"], json!(2));
}
#[test]
fn the_specification_address_is_sealed_so_two_figures_can_be_told_apart() {
// The cost figure is comparable only at a fixed specification, so the
// receipt must carry the address a reader compares on.
let (s, ws, wk) = fully_evidenced();
let k = key(9);
let (env, _) = seal(&s, &state(), &ws, &wk, STEWARD, &k).unwrap();
let doc = verify(&env, STEWARD, &k.verifying_key().to_bytes()).unwrap();
assert_eq!(doc["spec"], json!(s.spec.spec_id().unwrap().as_str()));
}
}