feat(analysis): AADL→CQF synthesis bridge (REQ-TSN-SYNTH-CQF-BRIDGE-001)

[avrabe]

What

Extracts CQF synthesis inputs directly from an AADL SystemInstance and runs the literature-pinned synthesizer (synthesize_cqf, REQ-TSN-SYNTH-CQF-BASE-001) over them, so a real model — not a hand-built CqfFlow set — drives standard 802.1Qch CQF configuration. The synthesized schedule (or any synthesis error / soundness warning) surfaces as analysis diagnostics via a new CqfSynthAnalysis pass.

Scope — table-stakes, NOT the wedge

This is AADL→TSN-config glue: the demonstrable end-to-end ship that makes spar a configuration generator a user can run on their own model. It composes no network calculus and is explicitly NOT the PLP≪TFA strategic wedge. CQF's bounded delay depends only on (hops, cycle time) (IETF draft-eckert-detnet-tcqf-05), so the bridge needs the routing topology and a few per-flow scalars — nothing from the NC engine, no per-class composition soundness obligation.

How

• Routing reuse, not reimplementation: collect_streams (WCTT pass) is made pub(crate) and reused — the Actual_Connection_Binding resolution is the genuinely hard part and already exists.
• Per stream → CqfFlow: deadline (skip with an Info diag if absent — never an invented deadline), Spar_TSN::Max_Frame_Size × 8 (default one MTU), the bound switch sequence as the hop path, and the minimum switch Output_Rate as the conservative homogeneous link rate (slowest link binds the cycle budget).
• Soundness guard: one frame per cycle is sound only when synthesized T ≤ period. Deadline > Period is AADL-legal, so the bridge checks T ≤ period post-synthesis and emits CqfSynthUnsound rather than silently under-reserving.
• No new dependency. register_all 31→32.

Oracle / verification

Tests are mutation-complete: cargo mutants -f cqf_synth.rs → 0 survivors (12 caught, 3 unviable). spar-analysis is the mutation-gated crate, so every viable branch is killed. Highlights:

• Hand-computed schedule oracle pinned to D_max = (H+1)·T = deadline.
• CqfSynthSkipped (no timing budget), CqfSynthError (deadline below the irreducible cycle floor), link_rate None early-return, DEFAULT_FRAME_BYTES fallback.
• Soundness-guard boundary: T == period stays sound (pins >, not >=).
• Min-rate over a 2-hop path; CqfSynthUnsound on Deadline>Period; non-regression (no switched buses → no diagnostics).

Local gates: 889 spar-analysis lib tests pass; cargo fmt --all --check clean; clippy -D warnings clean.

Traceability

• REQ-TSN-SYNTH-CQF-BRIDGE-001 (requirements.yaml), TEST-TSN-SYNTH-CQF-BRIDGE (verification.yaml) — both release: v0.20.0.

Falsification statement

If an AADL model declares switched buses with Output_Rate, bound end-to-end streams with deadlines, and frame sizes, then CqfSynthAnalysis emits a CQF schedule whose structural delay (H+1)·T meets every flow's deadline and whose per-cycle reservation fits csize = T·link_rate — or a precise diagnostic (CqfSynthSkipped/CqfSynthError/CqfSynthUnsound) explaining why it cannot. It composes no network calculus and makes no PLP/TFA tightness claim.

🤖 Generated with Claude Code

[github-actions]

Rivet verification gate

✅ 20/20 passed

	count
Passed	20
Failed	0
Skipped (no steps)	0

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

Failed artifacts

(none)

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

[codecov]

Codecov Report

❌ Patch coverage is 99.86207% with 1 line in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/spar-analysis/src/lib.rs	50.00%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!