fix(analysis): report unmeasurable bus demand instead of silence (REQ-NC-BUS-PAYLOAD-001)

[avrabe]

What

spar-analysis::bus_bandwidth conflated "this connection uses no bandwidth"
with "I could not determine this connection's bandwidth", and reported the
second as the first. This makes the analysis honest about what it could not
measure. It deliberately does not change a single computed bandwidth number.

New: REQ-NC-BUS-PAYLOAD-001 (release: v0.35.0, the release's actual payload),
REQ-NC-BUS-PAYLOAD-002 (v0.37.0, the capability successor), and
TEST-NC-BUS-PAYLOAD.

The defect

compute_connection_demand returned 0.0 for three distinct unmeasurable
cases — unresolved source subcomponent, no findable Data_Size, no findable
Period — and the caller then dropped every demand == 0.0 connection:

let demand = compute_connection_demand(instance, src_sub_idx, &bus_map);
if demand > 0.0 {
    bound_connections.push((conn.name.as_str().to_string(), demand));
    total_demand_bps += demand;
}

Two consequences:

1. A bus on which no connection's demand could be computed left
   bound_connections empty, hit the continue, and emitted no diagnostic at
   all. A saturated bus passed clean.
2. Where some connections resolved, the utilization silently omitted the rest
   and was still printed as a bare percentage — a lower bound presented as a
   verdict.

This is the same failure direction as REQ-TSN-SVC-MULTIWIN-001 (the optimistic
longest-gap TAS bound) and REQ-CODEGEN-LAYOUT-CERT-001 (the tautological
certificate, withdrawn in #356): optimistic when the input is incomplete.
Silence is the worst possible rendering of "I don't know", because it is
indistinguishable from "I checked and it's fine".

Root cause of the dominant case

Payload size is read only from the source component's own Data_Size. The
port's data classifier — the AADL-native place to put payload size, and the one
spar's own WIT codegen relies on via resolve_data_shape — is never consulted.
A model that types its ports properly has no findable Data_Size here at
all.

Closing that is the successor REQ-NC-BUS-PAYLOAD-002: the blocker is plumbing,
not semantics — the analysis path gets a SystemInstance without the resolver
scope needed to follow a classifier reference. This PR makes the gap visible
first, because the honesty fix is sound on its own and must not wait on the
capability.

The fix

The load-bearing change is at the type level, not in the message text:

enum ConnectionDemand { Known(f64), Unknown(Unaccounted) }
enum Unaccounted { UnresolvedSource, PayloadSize, SourcePeriod }

compute_connection_demand no longer returns f64, so a caller cannot
conflate the two by testing demand > 0.0 — the old return 0.0 was a lie the
compiler could not see. Then:

• any bus with ≥1 unaccounted bound connection emits a Warning naming the
  count, the total, and the reasons grouped — even when nothing resolved,
  which is precisely the case that used to pass in silence;
• every utilization verdict (Error / Warning / Info) computed over an incomplete
  set carries an explicit LOWER BOUND: N connections unaccounted suffix;
• reasons render in a fixed order with at most MAX_NAMED_CONNECTIONS = 3 names
  before eliding, so diagnostics are stable across runs.

Oracle

Two tests, both red against the previous implementation:

• missing_data_size_no_demand — this test previously asserted silence
  ("No demand computed, so no diagnostics for this bus."). The bug was encoded
  in the oracle itself, which is why it survived. It now asserts exactly one
  Warning containing INCOMPLETE, the reason, and the connection name — and,
  as the falsification edge, that the message does not contain
  utilization:, so no verdict may be reported when nothing was measured.
• partial_demand_is_labelled_a_lower_bound — one fully-specified connection
  (8192 bps) plus one with no findable Data_Size on a 1 Mbitsps bus, i.e. a
  case that previously produced a clean sub-80% Info. Asserts the warning
  quantifies 1 of 2 bound connections and names c_b, and that the Info
  verdict carries LOWER BOUND: 1 connections unaccounted.

The remaining bus_bandwidth tests are unchanged and still pass — that is
the evidence for the SCOPE clause: where the input is complete, no computed
number moved.

Verification

• cargo test -p spar-analysis --lib bus_bandwidth — 31 passed, 0 failed
  (29 in bus_bandwidth::tests, plus the 2 resource_budget::tests that call
  into it), both oracle changes among them:

  test bus_bandwidth::tests::missing_data_size_no_demand ... ok
  test bus_bandwidth::tests::partial_demand_is_labelled_a_lower_bound ... ok
  test result: ok. 31 passed; 0 failed; 0 ignored; 884 filtered out
  

• cargo fmt --all --check — clean

• rivet validate — the three new artifacts add no new error class. The one
  status: passing error is the repo's pre-existing local-vs-CI schema skew,
  measured rather than assumed: 170 such artifacts on pristine main, 171
  with this PR. passing is the repo convention and CI's rivet accepts it.

• Link graph re-parsed across all three artifacts/*.yaml (429 artifacts): this
  PR adds zero dangling links. The 25 pre-existing ones are all STPA-*
  targets that live outside artifacts/.

• The full local cargo test --workspace was aborted, not failed, so CI is
  the workspace gate for this PR. Flagging the reason rather than papering over
  it: the host's SD build volume sat at 97% with a concurrent cargo-sweep -r
  churning it, starving rustc to 3.4% CPU (13.1s CPU over 6:29 wall, process
  state U — uninterruptible I/O wait). Re-running the targeted oracle against
  an uncontended target dir cold-built and passed in 42s, which is what
  establishes the stall as I/O contention rather than a defect in this change.

Verification-gate scope (machinery note)

Adding an explicit Verify-Filter: below, because the gate's default filter
is (or (has-tag "v093") (has-tag "v0100")) — 20 of the repo's 161
type: feature artifacts, all from the v0.9.3/v0.10.0 era. Without an override a
PR's own artifacts are never executed by the gate: PR #356 removed
TEST-LAYOUT-CERT and rewrote three requirements, and its gate comment still
read "✅ 20/20 passed" against that stale set. None of the last 10 merged PRs
(#340…#354) set Verify-Filter:, so the per-PR override the workflow was
designed around has never actually been used.

This PR sets it, keeping the existing 20 as a floor rather than replacing them,
so TEST-NC-BUS-PAYLOAD is genuinely run by the gate and not merely declared
passing.

Accuracy caveat about this very PR: the workflow reads the line from
github.event.pull_request.body, which is captured in the event payload at
trigger time. The line was added after the opened event, so the gate run that
fired on open used the default filter, and a re-run replays the original payload
rather than the edited body. It takes effect on the next synchronize. The
substance is not resting on that: the artifact's declared step
(cargo test -p spar-analysis --lib bus_bandwidth) was executed verbatim and is
the 31/31 result quoted above.

That fragility is itself the argument for the generic fix — deriving the scope
from the artifact IDs a PR's diff touches, so the scope is a function of the
commit rather than of prose a human has to remember to type into a description.
Filed separately; it should not ride along in a bug-fix PR.

Verify-Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100") (has-tag "v0350")))

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 95.65217% with 6 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/spar-analysis/src/bus_bandwidth.rs	95.65%	6 Missing ⚠️

📢 Thoughts on this report? Let us know!

[github-actions]

Rivet verification gate

✅ 21/21 passed

	count
Passed	21
Failed	0
Skipped (no steps)	0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100") (has-tag "v0350")))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}

[avrabe]

Honesty note before merge: the verification gate did not cover this PR's new artifact

The Verify-Filter: line I added to this PR's body did not take effect, because I
added it after the PR was opened. Measured, not assumed — gate run
30535183445:

== summary ==
passed:  20
failed:  0
skipped: 0

20 is the stale default scope (or (has-tag "v093") (has-tag "v0100")). The gate
resolves its filter from github.event.pull_request.body as captured in the event
payload at trigger time, so a later body edit is invisible to it and a re-run replays
the original payload.

What that means for this PR, precisely:

• ❌ The artifact-level V-model binding for this change (requirement → its verifying
  test, exercised as an artifact) was not exercised by the verification gate.
  A green passed: 20 here says nothing about REQ-NC-BUS-PAYLOAD-001.
• ✅ The code is still tested: the required Test job runs the full workspace suite,
  which includes the new tests. That is ordinary test coverage, not artifact-level
  traceability coverage.

So this is safe to merge on the strength of Test + the other required contexts, but
it should not be recorded as "verified by the verification gate" — it wasn't.
Calling that out here so the merge doesn't quietly inherit a claim it didn't earn.

The generic fix (derive gate scope from the diff, and make an under-inclusive run
loud instead of printing a clean summary) is #358, now updated with this measurement.
#359 is the control run with Verify-Filter: present at creation time.

[avrabe]

Issue-hunt cron — advancing this PR.

Prior run's CI on head 0b7cb96 was fully green (all 16 required checks incl. Mutation Testing on spar-analysis and Kani, plus Lean Proofs + Verification Gate). Independent clean-room re-verification (fresh checkout, ran the oracle rather than trusting the summary):

• cargo test -p spar-analysis --lib bus_bandwidth → 31 passed, 0 failed, both new oracles among them.
• ConnectionDemand::{Known, Unknown(Unaccounted)} enum, the INCOMPLETE warning emitted before the bound_connections.is_empty() guard (so the previously-silent path fires), and the LOWER BOUND: N connections unaccounted suffix on all three verdicts — all confirmed in code, not just prose.
• No pre-existing numeric/utilization assertion edited → the "no computed number moved" SCOPE claim holds.
• Honesty: REQ-NC-BUS-PAYLOAD-001 is implemented (not verified), successor REQ-NC-BUS-PAYLOAD-002 is proposed, TEST-NC-BUS-PAYLOAD is passing. No over-claim.

The merge was blocked only by branch protection's up-to-date requirement (base had advanced to 2af55b1 via #356). I updated the branch (72f7f0f = feature + main merged in, clean, no conflicts), which re-triggered the full required-check battery — now pending (~2h for Mutation Testing). The next cron run merges this squash once green.

Note on scope: crate version is already at 0.35.0 (bumped by #355), and v0.35.0's original payload — the layout certificate — was withdrawn in #356. This PR is v0.35.0's real payload, so no separate bump PR is needed; once merged, v0.35.0 is complete and awaits a maintainer-cut signed tag (this environment can't produce a verifiable signed tag — git tag -v fails on an absent allowedSignersFile).

Also worth flagging for a maintainer: the tag/release backlog — main is at v0.35.0 in Cargo.toml, but the last published release is v0.33.0; v0.34.0 and v0.35.0 are bumped-but-untagged. Cutting those signed tags is a maintainer action.

---

Generated by Claude Code