feat(network): window-splitting 802.1Qbv GCL synthesis baseline (REQ-TSN-SYNTH-QBV-SPLIT-BASE-001)

Pulls the worst-case-latency lever the single-window baseline
(REQ-TSN-SYNTH-QBV-BASE-001) cannot: splitting a class's allocation into K
evenly-spaced windows cuts its worst-case gate latency to (cycle−open)/K
at the SAME bandwidth, so a port that single windows leave Oversubscribed
(each latency-bound class needing a wide window to reach a low latency)
becomes feasible.

`synthesize_gcl_split` exploits the network-calculus identity that a K-way
even split on cycle c is identical to a single window on cycle c/K (same
rate, same latency = c/K − w): it synthesizes one round on c/K with the
existing single-window search and replicates it K times, returning the
SMALLEST feasible K (fewest windows — closest to a deployable GCL). K=1
reproduces synthesize_gcl byte-for-byte. The result self-certifies on the
full multi-window schedule against the SOUND latency
(REQ-TSN-SVC-MULTIWIN-001 / min_service_latency_ps) — the regime that
makes splitting non-trivial.

NC-level baseline: the model is guard-band-free, so max_windows_per_class
caps the search off the rate-loss cliff a guard-band-aware model imposes
(deployable-claim follow-up = new REQ-TSN-SYNTH-QBV-GUARDBAND-001).
Precursor to the full dependency-aware REQ-TSN-SYNTH-QBV-001 (re-scoped to
v0.22.0). Incremental synthesis (table-stakes vs RTaW), NOT the wedge.

Oracle (4 tests): the exact oversubscribed set synth_rejects_oversubscribed_port
rejects is made feasible + self-certifies + genuinely splits; a feasible
demand stays K=1; max_windows=1 disables splitting; non-whole-ns / zero
cycle rejected up front. 148 spar-network tests pass; mutants on the new
code 12 caught / 1 unviable / 1 defensive-equivalent (the self-cert guard,
matching synthesize_gcl's pattern); fmt(nightly)+clippy clean.

Adds REQ-TSN-SYNTH-QBV-SPLIT-BASE-001 (implemented) +
REQ-TSN-SYNTH-QBV-GUARDBAND-001 (proposed, v0.22) + TEST-TSN-SYNTH-QBV-SPLIT;
REQ-TSN-SYNTH-QBV-001 re-scoped to v0.22.0 (the full dependency-aware paper).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: avrabe

artifacts/requirements.yaml

@@ -3169,6 +3169,62 @@ artifacts:
     fields:
       release: v0.20.0
 
+  - id: REQ-TSN-SYNTH-QBV-SPLIT-BASE-001
+    type: requirement
+    title: "802.1Qbv window-splitting synthesis baseline — even K-split, smallest feasible K"
+    description: >
+      spar shall synthesize a window-SPLITTING 802.1Qbv gate-control list
+      that pulls the worst-case-latency lever the single-window baseline
+      (REQ-TSN-SYNTH-QBV-BASE-001) cannot: splitting a class's allocation
+      into K evenly-spaced windows cuts its worst-case gate latency to
+      (cycle − open)/K at the SAME bandwidth, so a port that single
+      windows leave Oversubscribed (each latency-bound class needing a
+      wide window to reach a low latency) becomes feasible.
+      `synthesize_gcl_split` uses the network-calculus identity that a
+      K-way even split on cycle c is identical to a single window on cycle
+      c/K (same rate, same latency = c/K − w): it synthesizes one round on
+      c/K with the existing single-window search and replicates it K
+      times, returning the SMALLEST feasible K (fewest windows). K=1
+      reproduces synthesize_gcl exactly; the result SELF-CERTIFIES on the
+      full multi-window schedule against the SOUND latency
+      (REQ-TSN-SVC-MULTIWIN-001 / min_service_latency_ps) — the
+      counterexample regime that makes this non-trivial. NC-level baseline:
+      the model is guard-band-free, so `max_windows_per_class` caps the
+      search off the rate-loss cliff a guard-band-aware model imposes
+      (deployable claim = REQ-TSN-SYNTH-QBV-GUARDBAND-001). Precursor to
+      the full dependency-aware REQ-TSN-SYNTH-QBV-001, mirroring
+      REQ-TSN-SYNTH-QBV-BASE-001 → REQ-TSN-SYNTH-QBV-001. Incremental
+      synthesis (table-stakes vs RTaW), NOT the PLP≪TFA wedge. [SOLID]
+    status: implemented
+    tags: [tsn, synthesis, qbv, tier2]
+    fields:
+      release: v0.21.0
+
+  - id: REQ-TSN-SYNTH-QBV-GUARDBAND-001
+    type: requirement
+    title: "802.1Qbv guard-band-aware window-splitting (deployable GCL claim)"
+    description: >
+      Follow-up to REQ-TSN-SYNTH-QBV-SPLIT-BASE-001, which synthesizes
+      split GCLs over a guard-band-FREE model (sound at the NC
+      service-curve level, but NOT a deployable-hardware claim — real
+      802.1Qbv loses ~K guard bands of transmit time to frame-straddle
+      protection, which the model does not see, so the baseline can
+      over-state available rate by (K−1)·g/cycle). spar should subtract
+      the per-window guard band g (≈ Max_Frame_Size / link_rate; readers
+      exist) from effective open time and add g to latency — using the
+      already-present structural hook in
+      `tas_residual_service_with_sync_error` (the ε-subtraction pattern) —
+      so the synthesizer's "meets deadline" claim becomes
+      deployment-sound and the breakeven K (self-starvation at
+      K = 1 + cycle·ρ/g) is enforced automatically by the oracle rejecting
+      rate-starving splits. Verified-economics: latency gain ~1/K vs rate
+      loss linear in K; rich to K≈10, catastrophic past ~50 for typical
+      automotive cycles/frames. [SOLID]
+    status: proposed
+    tags: [tsn, synthesis, qbv, guard-band, tier2]
+    fields:
+      release: v0.22.0
+
   - id: REQ-TSN-SYNTH-QBV-001
     type: requirement
     title: "802.1Qbv GCL synthesis — dependency-aware, window-splitting, mixed-criticality"
@@ -3177,19 +3233,18 @@ artifacts:
       (inverse of the existing TAS checking, REQ-TSN-002) via
       dependency-aware priority adjustment with WINDOW SPLITTING
       (arXiv:2407.00987, 2024): ~300 flows, mixed-criticality, +20.6%
-      success over SOTA. Builds on the single-window baseline
-      (REQ-TSN-SYNTH-QBV-BASE-001) by splitting a class's allocation into
-      multiple windows distributed around the cycle — the only lever that
-      lowers worst-case gate latency below cycle − duration for a fixed
-      bandwidth (with one window per class, window order alone is a
-      provable no-op; splitting/placement is the paper's actual
-      contribution). KILL-GATE: kill the AADL→TSN bridge if we cannot
-      articulate why our integrated architecture-to-timing story beats
-      RTaW's already-cert-accepted ARXML→TSN+NC. [SOLID]
+      success over SOTA. The even-split LEVER shipped as the precursor
+      REQ-TSN-SYNTH-QBV-SPLIT-BASE-001 (smallest feasible K, NC-level,
+      self-certified against the sound bound); this requirement is the
+      FULL contribution that remains — dependency-aware priority/placement
+      (not just even splits) and mixed-criticality across ~300 flows.
+      KILL-GATE: kill the AADL→TSN bridge if we cannot articulate why our
+      integrated architecture-to-timing story beats RTaW's already-cert-
+      accepted ARXML→TSN+NC. [SOLID]
     status: proposed
     tags: [tsn, synthesis, qbv, tier2]
     fields:
-      release: v0.21.0
+      release: v0.22.0
 
   - id: REQ-TSN-SYNTH-MILP-001
     type: requirement

artifacts/verification.yaml

@@ -2335,6 +2335,35 @@ artifacts:
       - type: satisfies
         target: REQ-TSN-SYNTH-QBV-BASE-001
 
+  - id: TEST-TSN-SYNTH-QBV-SPLIT
+    type: feature
+    title: 802.1Qbv window-splitting synthesis baseline — splits an oversubscribed port
+    description: >
+      Verifies synthesize_gcl_split (REQ-TSN-SYNTH-QBV-SPLIT-BASE-001), the
+      smallest-feasible-K even-split synthesizer. spar-network::tsn unit
+      tests cover: (1) THE LEVER — the exact two-class latency-bound demand
+      set that synth_rejects_oversubscribed_port REJECTS with single
+      windows is made FEASIBLE by splitting; the result self-certifies
+      (each class's delay_bound over the SOUND min_service_latency curve ≤
+      its deadline) and genuinely splits (≥ 2 windows per class);
+      (2) NO-NEEDLESS-SPLIT — a comfortably feasible demand returns K=1,
+      byte-identical to synthesize_gcl; (3) K-CAP — max_windows_per_class=1
+      disables splitting, so the oversubscribed set is rejected;
+      (4) INPUT VALIDATION — a non-whole-nanosecond cycle (and cycle 0) are
+      rejected up front as CycleNotWholeNanos, not silently mis-reported.
+      Self-certifying: the full multi-window schedule is re-checked through
+      the sound checker before return, so an unsound split fails
+      construction, not just the test.
+    fields:
+      method: automated-test
+      steps:
+        - run: "cargo test -p spar-network --lib -- split_"
+    status: passing
+    tags: [v0.21.0, network, tsn, synthesis, qbv, oracle]
+    links:
+      - type: satisfies
+        target: REQ-TSN-SYNTH-QBV-SPLIT-BASE-001
+
   - id: TEST-TSN-EXPORT-YANG
     type: feature
     title: 802.1Qcw YANG/NETCONF export of a synthesized gate schedule

crates/spar-network/src/tsn.rs

@@ -1530,6 +1530,116 @@ pub fn synthesize_gcl(
     Ok(sched)
 }
 
+/// Synthesize a window-SPLITTING 802.1Qbv GCL (REQ-TSN-SYNTH-QBV-001) —
+/// the worst-case-latency lever that [`synthesize_gcl`]'s single window
+/// per class cannot pull. Splitting a class's allocation into K evenly
+/// spaced windows cuts its worst-case gate latency to `(cycle − open)/K`
+/// at the SAME bandwidth, so a port that single windows leave
+/// `Oversubscribed` (each latency-bound class needing a wide window to
+/// reach a low latency) can become feasible.
+///
+/// Key identity: a K-way even split on cycle `c` with per-round window `w`
+/// is network-calculus-identical to a SINGLE window `w` on a cycle `c/K`
+/// (same rate `R·w/(c/K)`, same latency `c/K − w`). So this tries
+/// `K = 1, 2, …, max_windows_per_class`, synthesizes ONE round on `c/K`
+/// with the existing single-window search, and replicates it K times. It
+/// returns the SMALLEST feasible K (fewest windows — closest to a
+/// deployable GCL); `K = 1` reproduces [`synthesize_gcl`] exactly. The
+/// result self-certifies on the full multi-window schedule against the
+/// SOUND latency [`GateSchedule::min_service_latency_ps`].
+///
+/// SCOPE: this is an NC-level service-curve baseline. The model does not
+/// account for 802.1Qbv guard bands, so each extra window is "free" here;
+/// `max_windows_per_class` is the cap that keeps the search off the
+/// rate-loss cliff a guard-band-aware model would impose (the deployable
+/// claim is the follow-up REQ-TSN-SYNTH-QBV-GUARDBAND-001). Not the
+/// PLP≪TFA wedge — incremental synthesis, table-stakes against RTaW.
+pub fn synthesize_gcl_split(
+    demands: &[ClassDemand],
+    cycle_ps: u64,
+    link_rate_bps: u64,
+    max_windows_per_class: u64,
+) -> Result<GateSchedule, GclSynthError> {
+    if demands.is_empty() {
+        return Err(GclSynthError::NoDemands);
+    }
+    if cycle_ps == 0 || !cycle_ps.is_multiple_of(1_000) {
+        return Err(GclSynthError::CycleNotWholeNanos { cycle_ps });
+    }
+    let kcap = max_windows_per_class.max(1);
+    let mut last_oversub = GclSynthError::Oversubscribed {
+        required_ps: 0,
+        cycle_ps,
+    };
+    for k in 1..=kcap {
+        // The round cycle `cycle_ps / k` must be a whole number of
+        // nanoseconds, i.e. K must divide the cycle in ns — skip K otherwise.
+        if !cycle_ps.is_multiple_of(k.saturating_mul(1_000)) {
+            continue;
+        }
+        let round_cycle_ps = cycle_ps / k;
+        match synthesize_gcl(demands, round_cycle_ps, link_rate_bps) {
+            Ok(round) => {
+                // K == 1 is exactly the single-window baseline.
+                if k == 1 {
+                    return Ok(round);
+                }
+                // Replicate the round K times across the full cycle.
+                let mut blob = String::new();
+                for r in 0..k {
+                    let base = r * round_cycle_ps;
+                    for w in &round.windows {
+                        if !blob.is_empty() {
+                            blob.push(';');
+                        }
+                        blob.push_str(&format!(
+                            "{}:{}:0x{:02X}",
+                            (base + w.offset_ps) / 1_000,
+                            w.duration_ps / 1_000,
+                            w.allowed_cos_mask
+                        ));
+                    }
+                }
+                let sched = GateSchedule::parse(&blob).map_err(|e| {
+                    GclSynthError::SelfCheck(format!("split re-parse failed for {:?}: {}", blob, e))
+                })?;
+                // Self-certify the FULL multi-window schedule against the
+                // SOUND latency — a failure here is a synthesizer bug, not
+                // an unsound schedule reaching the caller.
+                for d in demands {
+                    let beta = tas_residual_service(&sched, d.cos, link_rate_bps);
+                    match delay_bound(&d.arrival, &beta) {
+                        Ok(delay) if delay <= d.deadline_ps => {}
+                        Ok(delay) => {
+                            return Err(GclSynthError::SelfCheck(format!(
+                                "class {} delay {} ps exceeds deadline {} ps after {}-split",
+                                d.cos.0, delay, d.deadline_ps, k
+                            )));
+                        }
+                        Err(e) => {
+                            return Err(GclSynthError::SelfCheck(format!(
+                                "class {} unservable after {}-split: {:?}",
+                                d.cos.0, k, e
+                            )));
+                        }
+                    }
+                }
+                return Ok(sched);
+            }
+            // Oversubscribed shrinks as K grows for latency-bound classes —
+            // a finer split may fit. Keep the error and try the next K.
+            Err(e @ GclSynthError::Oversubscribed { .. }) => {
+                last_oversub = e;
+                continue;
+            }
+            // ClassInfeasible (can't be served even at rate=link, latency=0)
+            // and structural errors are K-independent — fail fast.
+            Err(other) => return Err(other),
+        }
+    }
+    Err(last_oversub)
+}
+
 /// Worst-case delay (ps) for `demand` if its class receives a single open
 /// window of `dur_ns` in a `cycle_ns` cycle on a `link_rate_bps` link,
 /// computed via the real TAS checker ([`tas_residual_service`] +
@@ -2618,6 +2728,130 @@ mod tests {
         );
     }
 
+    // ── REQ-TSN-SYNTH-QBV-001: window-splitting synthesis ────────────────
+
+    #[test]
+    fn split_fits_an_oversubscribed_latency_bound_port() {
+        // The exact demand set synth_rejects_oversubscribed_port rejects:
+        // two latency-bound classes that one window per class oversubscribes.
+        // Splitting cuts each class's worst-case latency at the SAME
+        // bandwidth, so a finer split fits where single windows did not.
+        let link = 1_000_000_000u64;
+        let cycle_ps = 10_000_000u64;
+        let demands = vec![
+            ClassDemand {
+                cos: cos(7),
+                arrival: ArrivalCurve::affine(125, 100_000_000),
+                deadline_ps: 5_500_000,
+            },
+            ClassDemand {
+                cos: cos(3),
+                arrival: ArrivalCurve::affine(125, 100_000_000),
+                deadline_ps: 5_500_000,
+            },
+        ];
+        // One window per class oversubscribes (the QBV-BASE limit).
+        assert!(matches!(
+            synthesize_gcl(&demands, cycle_ps, link),
+            Err(GclSynthError::Oversubscribed { .. })
+        ));
+        // Window-splitting finds a feasible schedule.
+        let sched = synthesize_gcl_split(&demands, cycle_ps, link, 8).expect("split feasible");
+        // SOUND self-check: each class meets its deadline under the exact
+        // min-service latency on the resulting multi-window schedule.
+        for d in &demands {
+            let beta = tas_residual_service(&sched, d.cos, link);
+            let delay = delay_bound(&d.arrival, &beta).expect("servable");
+            assert!(
+                delay <= d.deadline_ps,
+                "class {} delay {} > deadline {}",
+                d.cos.0,
+                delay,
+                d.deadline_ps
+            );
+        }
+        // It genuinely SPLIT — at least two windows for each class.
+        for d in &demands {
+            let n = sched
+                .windows
+                .iter()
+                .filter(|w| w.allowed_cos_mask & (1 << d.cos.0) != 0)
+                .count();
+            assert!(n >= 2, "class {} not split: {} window(s)", d.cos.0, n);
+        }
+    }
+
+    #[test]
+    fn split_uses_single_window_when_feasible() {
+        // A comfortably feasible demand needs no splitting: K=1, and the
+        // result is byte-identical to synthesize_gcl (no needless windows).
+        let link = 1_000_000_000u64;
+        let cycle_ps = 10_000_000u64;
+        let demands = vec![
+            ClassDemand {
+                cos: cos(7),
+                arrival: ArrivalCurve::affine(125, 100_000_000),
+                deadline_ps: 8_000_000,
+            },
+            ClassDemand {
+                cos: cos(3),
+                arrival: ArrivalCurve::affine(125, 100_000_000),
+                deadline_ps: 9_000_000,
+            },
+        ];
+        let base = synthesize_gcl(&demands, cycle_ps, link).expect("feasible");
+        let split = synthesize_gcl_split(&demands, cycle_ps, link, 8).expect("feasible");
+        assert_eq!(
+            base.to_gcl_blob(),
+            split.to_gcl_blob(),
+            "K=1 must reproduce synthesize_gcl byte-for-byte"
+        );
+    }
+
+    #[test]
+    fn split_caps_at_max_windows() {
+        // With max_windows_per_class = 1, splitting is disabled, so the
+        // oversubscribed set is rejected (same as the single-window path).
+        let link = 1_000_000_000u64;
+        let cycle_ps = 10_000_000u64;
+        let demands = vec![
+            ClassDemand {
+                cos: cos(7),
+                arrival: ArrivalCurve::affine(125, 100_000_000),
+                deadline_ps: 5_500_000,
+            },
+            ClassDemand {
+                cos: cos(3),
+                arrival: ArrivalCurve::affine(125, 100_000_000),
+                deadline_ps: 5_500_000,
+            },
+        ];
+        assert!(matches!(
+            synthesize_gcl_split(&demands, cycle_ps, link, 1),
+            Err(GclSynthError::Oversubscribed { .. })
+        ));
+    }
+
+    #[test]
+    fn split_rejects_non_whole_nanosecond_cycle() {
+        // A non-whole-ns cycle is rejected up front (not silently skipped
+        // into a misleading Oversubscribed) — and cycle 0 likewise.
+        let link = 1_000_000_000u64;
+        let demands = vec![ClassDemand {
+            cos: cos(7),
+            arrival: ArrivalCurve::affine(125, 100_000_000),
+            deadline_ps: 5_000_000,
+        }];
+        assert!(matches!(
+            synthesize_gcl_split(&demands, 1_500, link, 8),
+            Err(GclSynthError::CycleNotWholeNanos { cycle_ps: 1_500 })
+        ));
+        assert!(matches!(
+            synthesize_gcl_split(&demands, 0, link, 8),
+            Err(GclSynthError::CycleNotWholeNanos { .. })
+        ));
+    }
+
     #[test]
     fn synth_input_validation() {
         let link = 1_000_000_000u64;