Feature loop: spar/AADL, WIT and witness MC/DC have been N/A for ~20 features — decide, don't keep waiving

[avrabe]

The PulseEngine feature loop runs eight steps. For varve, three have been marked N/A every single feature since the project started:

• Step 1 — spar/AADL architecture model. varve has no .aadl model.
• Step 2 — WIT generated from spar. varve exposes no WIT interface.
• Step 5 — witness MC/DC on the Wasm artifact. varve emits no wasm; it is a native Rust CLI.

Each waiver is individually correct. The skill is explicit that the pattern is not:

Recurring N/A is a backlog item, not an exemption. … If you mark either one N/A for the same reason three features running, file it — that pattern is exactly how a real-flight MC/DC gap and a missing attestation chain stayed hidden across ~20 features.

We are well past three. Filing it so the waiver is a recorded decision rather than an unexamined habit.

The question to actually answer

Is varve out of scope for the model-driven half of the methodology, permanently — or is it missing an architecture model it should have?

Arguments that it is genuinely out of scope:

• varve is a supply-chain tool, not embedded software. There is no scheduling, no partitioning, no ASIL decomposition, no timing.
• Its trust properties are about signatures and identity, not about control flow on a target. MC/DC on a decision table is not the oracle that matters; cargo mutants on the trust-critical modules is, and that gate exists and is green.
• It ships a native binary by design. Compiling it to wasm to obtain a witness truth table would be building an artifact nobody runs.

Arguments that something is missing anyway:

• varve does have an architecture worth modelling: realms, the store partition, the composition graph, the trust boundary between a realm root and what it vouches for. Several of this release's defects were boundary bugs — a realm-blind store lookup (feat: v0.14.0 — recorded independent review + registry line-status #36), a platform-blind payload read, verify --all crossing a partition it should not have (verify --all checks only the pinned realm's partition, contradicting its --help #84). A model might have made those boundaries explicit enough to check.
• "No wasm" is true today; wasm-component is already a declared payload kind.

What closing this looks like

Either:

1. Record the exemption — a decision artifact in rivet stating that steps 1, 2 and 5 do not apply to varve and why, with the compensating oracles named (mutation testing, fuzzing, Kani, the self-hosting system gate). Then the loop's N/A is traceable instead of tacit.
2. Build the model — a minimal spar model of the realm/store/composition boundaries, and see whether its analysis passes say anything the tests do not.

Option 1 is the honest default and is cheap. Option 2 is the interesting experiment, and would be evidence for or against the "MBSE is mandatory infrastructure" claim on a project that is not embedded — which is arguably a better test of the claim than another avionics example.

Related: REQ-SYSTEST-001 clause 4 has the same shape — a policy with no mechanical enforcement.

[avrabe]

Decision (maintainer, 2026-08-20): not an exemption. Build it — and MC/DC has a hard prerequisite.

Rejecting option 1 (record the waiver). The direction is:

1. An AADL model is worth defining anyway, for the analysis it enables, even though varve is not embedded software. The boundaries it would make explicit — realms, store partitions, the composition graph, which root vouches for what — are exactly where this project's defects keep landing (feat: v0.14.0 — recorded independent review + registry line-status #36 realm-blind lookup, verify --all checks only the pinned realm's partition, contradicting its --help #84 verify --all crossing a partition, the platform-blind payload read in v0.27.0). Those are architecture bugs found by testing, which is the expensive order.

2. MC/DC is in scope too, but it cannot start where varve is today: witness measures MC/DC on a Wasm artifact, and varve is a native binary. The prerequisite is a wasm32-wasip2 build of varve that actually runs — not a compile-only target, since a truth table over code nobody executes is theatre.

3. Scheduled for v0.29.0, explicitly not v0.28.0. v0.28.0 is the trust-correctness release and is already four workstreams.

What v0.29.0 has to answer

• Can varve build for wasm32-wasip2 at all? It does filesystem, network (registry), process dispatch (varve run), and signature verification. Process dispatch is the interesting one — a wasm varve cannot exec a native tool, so either the wasm build is a verification-only subset, or dispatch becomes a host import.
• If it is a subset, say which subset, because MC/DC over a subset is coverage of that subset and nothing more. Naming the boundary is the whole value.
• What does the AADL model actually assert, and does any spar analysis pass say something the existing oracles (mutation, fuzz, Kani, the self-hosting gate) do not? That is the real test of the "MBSE is mandatory infrastructure" claim on a non-embedded project — arguably a better test than another avionics example.

Keeping this issue open as the v0.29.0 anchor; a requirement will be authored against it when v0.28.0 lands.

[avrabe]

Refinement (maintainer): follow synth's approach — extract the important subset as the wasm artifact, rather than trying to wasm-ify the whole CLI. Investigation required first.

This is a better shape than what I wrote above, and it dissolves the objection I raised. I had framed the blocker as "varve does filesystem, network, and process dispatch, so a wasm32-wasip2 build is either impossible or a subset" — treating the subset as a compromise. It is not: the subset is the point.

The parts of varve whose decisions actually warrant MC/DC are exactly the parts with no I/O:

• DSSE envelope verification and signature checking
• layer-id parsing, channel and pin validation
• anti-rollback comparison (counter vs high-water) — the most defensible property in the tool
• the composition walk: cycle vs diamond, depth bounding (already the source of two shipped defects)
• platform matching (entry_matches) — the source of a third
• payload-kind and identity rules

None of those need a filesystem, a socket, or exec. They are pure functions over bytes and small structs. That is the natural wasm component, and it is also precisely where a truth table means something: these are decision-dense, branch-heavy, and every one of this release's boundary bugs lived in them.

The I/O shell — store layout, registry transport, process dispatch, terminal output — stays native and is covered by what already covers it well: the self-hosting system gate, the OCI round trip, fuzzing, and cargo mutants.

What the investigation has to establish

1. How synth actually does it — read the real structure rather than inferring it. Which crate boundary is the wasm artifact, how the native binary consumes it, whether it is a component or a core module, and how witness is pointed at it in CI.
2. Whether varve's core is already separable. varve-core is a library with #![forbid(unsafe_code)], but it is not I/O-free: it contains store, registry, archive, the export adapters. The pure-logic subset would need to be a crate (or a feature-gated slice) that genuinely compiles without std::fs and std::net — and if it does not today, that is the finding, and the refactor is the work.
3. Whether the truth table says anything the existing oracles do not. cargo mutants already runs over the trust-critical modules with zero survivors required. If MC/DC on the same code produces no gap rows that mutation testing missed, that is a real and publishable result about the two techniques — not a failure.

Point 3 is worth stating plainly: this could conclude that MC/DC adds nothing here, and that would still be worth knowing. What is not acceptable is continuing to mark step 5 N/A without ever having checked.

Still v0.29.0. v0.28.0 stays the trust-correctness release.