Requirement percolation and coverage

Most requirement trackers answer “what did we say we’d build?” Supernova’s requirement graph answers a harder question: “what is actually proven to work, right now?” Every requirement is a node in one rooted DAG, every code line is annotated back to a requirement, every requirement declares typed proof, and “done” is a computed state that can be revoked. The mechanism runs in the predecessor platform today [live in automatt]; the Rust rewrite is the trace gate on Supernova’s own repository — self-hosting proof, not a deployed service.

One graph, one root

Each source file’s spec (see docs as an enforced contract for the deterministic spec mapping) contains numbered requirements — R0, R1, R2… Each R# carries five fixed fields: Status, Origin (the immutable “why does this exist?” pointer), Evidence (the typed “what would prove it?” declaration), and reciprocal Depends on / Subtasks edges. The edges form a DAG: cycles are rejected, and every R# must have a path to its spec’s R0. File specs chain upward via covers: references to system-level design requirements, which chain to a systems-registry root. The result is one connected graph from an individual code line to “the platform works”:

flowchart TD
    L["code line"] -- "// @R3 span" --> R3["file spec R3"]
    R3 -- "Depends on / Subtasks" --> R0f["file spec R0"]
    R0f -- "covers:" --> RS["system requirement R#"]
    RS -- "Depends on / Subtasks" --> R0s["system root R0"]
    R0s -- "registry" --> ROOT["registry root"]
    T["named unit test"] -- "evidence" --> R3
    E2E["integration E2E"] -- "evidence" --> RS

Percolation is the operation that keeps this graph well-formed and rolls proof up it. sun wiki percolate repairs reciprocal edges, rejects cycles, verifies root paths, and is idempotent — it edits DAG edges in place, never requirement text. Evidence percolates the same way: a parent is satisfied partly by its children’s evidence and never re-proves the leaf; its own obligation is only the increment. The kind of claim escalates with altitude — correct at the file-spec leaf, integrated at the system, landed at the feature, used/valued at the exercised user journey — so total proof cost stays bounded.

Annotation spans in source

Rust code carries requirement annotations as comments: // @R3, multiple IDs (// @R1 @R3), or ranges (// @R1-R3). An annotation on its own line opens an active span covering the following block, and stays active while brace depth remains open; a same-line annotation covers just that line; a blank line outside a block clears the span. Blanks, comments, attributes, and use/mod lines are exempt.

The coverage rule is two-sided:

• every code-bearing line must sit under an active span for a live file-local R# — no unowned code;
• every live R# must cover at least one source line — no phantom requirements.

The no-phantom-requirements direction is a blocking validation error; the no-unowned-code direction is currently surfaced as a non-blocking warning, delta-scoped to changed lines while an admitted ~798-line annotation backlog burns down (D75). The gate runs error-clean today; the measured numbers live on the Rust page.

Typed evidence

The per-requirement Test: field was replaced by Evidence: in a 2026-06-23 ruling. Matt, verbatim: “test is now basically evidence and every requirement has to provide some form of it but it’s not necessarily a unit test, it might be e2e integration or some monitoring requirement or something else entirely.” Evidence is the forward dual of Origin — Origin points backward at why the requirement exists; Evidence points forward at why we believe it holds, and whether that is still true.

Two rules do the anti-gaming work. First, the obligation is filer-authored at filing — the assignee cannot lower the bar, and the kind is fixed (only a numeric threshold may be sharpened, and only before evidence is evaluated against it). Second, there is no none: every live R# must declare evidence, even aspirationally. The 2026-06-24 ruling puts it plainly — Matt: “Requirements are very much ‘I want this to be true’ not ‘this is true’.” Declaration and satisfaction are separate checks — a missing declaration is always an error; red or pending evidence merely blocks done.

“It exists” is not “it works”

Status is derived, not asserted. You cannot mark an R# done; it becomes done when its accrued evidence matches its declared obligation — the validator rejects any status: done requirement whose evidence isn’t present, green, and fresh, the exact forward dual of the Origin check. Closure-by-checkbox is structurally impossible, a rule bought with scar tissue: the predecessor platform once closed a bug with all requirement checkboxes unchecked, and batch-moved fourteen work items to done with no validation.

And closure is non-monotonic — the substrate doc’s phrasing is “done is rented, not owned — you do not finish a requirement, you keep it satisfied”:

stateDiagram-v2
    draft --> ready : evidence declared
    ready --> done : obligation satisfied, computed
    done --> ready : evidence decays
    done --> draft : requirement text edited
    ready --> retired : intentional tombstone

Decay is per-kind, so it is proportionate: isolated test evidence falls only on a breaking code change; field evidence falls on live-signal regression; attestations mostly don’t decay (a created OAuth app stays created). When a leaf goes red, the response is trigger-and-recheck, not propagate-the-verdict: the parent’s own covering proof is re-run, targeted through the annotation and percolation maps — “blast radius is computed by re-proof, not assumed.” What happens to in-flight work when a requirement decays — wires reverting, features gaining an at-risk overlay — is the delivery lifecycle’s slice of the design; the delivery page covers the analogous test-triggered boot-back. The decay and recovery reactors that drive this loop are [engineered, not deployed]; today’s enforcement is the validator gate, not a standing ledger.

The coverage join

The strictest check joins three artifacts: the R#’s declared evidence test, the R#’s annotated source lines, and a per-test LCOV shard. The rule — named the “Automatt parity rule” after the predecessor’s behavior (Matt, 2026-06-25) — is that a line counts as covered only when the requirement’s own declared test executes the requirement’s own annotated lines. A passing test symbol plus a whole-suite coverage hit is not enough; unrelated test coverage is explicitly rejected (there is a test named for exactly that case). An evidence target whose LCOV record has no execution counters fails closed as malformed evidence rather than passing as “not instrumented.” This join is implemented and tested in the workspace [built in-repo], invoked via strict per-test LCOV flags on the validator; it runs delta-scoped while an admitted ~798-line annotation backlog burns down (D75, 2026-07-03).

D75 also added a counterfactual flag for correctness tests: when set, the declared test must be green at the landing commit and red at the pre-fix merge-base — the gate runs both, proving the test actually detects the bug it claims to.

Staleness

Even a cleanly validating repo can rot, so a scoring design (2026-06-26) treats truth decay as a first-class signal across three lanes: InternalDrift (one of a code/spec/design pair moved and its partner didn’t), ExternalDrift (a claim depends on an outside fact — an SDK, a price, an advisory), and ImprovementReaudit (“‘not known stale’ is not the same as ‘still the best design’”). A weighted score prioritizes requirement and interface movement over raw line churn, and Git time is authoritative over frontmatter — a timestamp-only edit cannot launder a stale spec. The trace-unit producer and the scorer are implemented with unit and E2E tests; the full rollout — review-gate blocking, external verification receipts — is further along the design than the deployment [engineered, not deployed].

What this costs

• The annotation tax is real. Every code-bearing line needs an active span; every R# needs five fields and typed evidence — the same agent-labor bet the wiki page names. And even here, the ~798-line backlog means the absolute coverage invariant is itself aspirational today.
• The model is only as honest as its weakest evidence producer. D82 (2026-07-03) is blunt about this: the E2E harness was assessed at roughly 12% real, with always-green stubs — and under a percolating model, a fake producer poisons everything above it. A planned reconciliation of ~390 requirements is deliberately frozen until real E2E and the D75 validator both land — the freeze is Matt’s own ruling, quoted on the long view.
• The most striking part is the least deployed part. The durable, decaying evidence ledger, field metrics, and the revert/at-risk reactors are the substrate’s architecture, not its running state. Most wiki-system R#s read done on unit evidence — in-repo proof of the mechanism, not production deployment.
• Hand-tuned knobs. The staleness weights and age bands are asserted, not calibrated from data.
• Superseded designs along the way: a none evidence kind (abolished 2026-06-24), the evidence ledger initially drafted into the wiki system (overruled — monitor owns it), and type-keyed gate profiles (superseded by D75 obligation inheritance). The decision ledger carries the tombstones.