feat(network): guard-band-aware 802.1Qbv GCL splitting (REQ-TSN-SYNTH-QBV-GUARDBAND-001)

artifacts/requirements.yaml

@@ -3210,19 +3210,36 @@ artifacts:
       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
+      protection per IEEE 802.1Q §8.6.8.4 TransmissionOverrun, which the
+      baseline model does not see, so it can over-state available rate by
+      ~N·K·g/cycle). spar shall charge the per-window guard band
+      g (≈ queueMaxSDU·8 / link_rate) so the synthesizer's
+      "meets deadline" claim becomes deployment-sound.
+      Implementation (synthesize_gcl_split_guarded): each class's USABLE
+      open window is sized by the same validated single-window search the
+      guard-free path uses (the guard does not change the service a class
+      receives — open w, latency cycle/K − w — only the PACKING budget),
+      then the emitter reserves an explicit trailing closed guard window
+      of g after every class window so the budget becomes Σwᵢ + N·g ≤
+      cycle/K and the DEPLOYED GCL physically contains the guards a switch
+      enforces. The breakeven/self-starvation cliff (guards growing as
+      N·K·g while latency benefit shrinks as 1/K) is enforced
+      automatically: when no split fits, the oracle returns
+      GuardOversubscribed rather than an unsound GCL. Model soundness is
+      pinned non-circularly by TEST-TSN-GUARDBAND's K=1 anchor — "emit a
+      (D−g)-open window" is proven algebraically identical to the shipped
+      tas_residual_service_with_sync_error at ε = g (open D−g, latency
+      C−D+g, rate R·(D−g)/C from two independent derivations). g rounds UP
+      to a whole ns (sound direction); g = 0 reproduces
+      REQ-TSN-SYNTH-QBV-SPLIT-BASE-001 byte-for-byte. NO new dependency
+      (existing tsn.rs + curves.rs). Precursor to the full
+      dependency-aware REQ-TSN-SYNTH-QBV-001. SCOPE: this is the
+      deployment-sound GCL PRODUCER — the GateSchedule it returns
+      physically carries the guard bands a switch enforces. Like the whole
+      synthesize_gcl* family it is library API; no synthesizer is yet wired
+      into a CLI / AADL→Qbv consumer, so this REQ makes no end-to-end
+      pipeline claim — consumer wiring is separate future work. [SOLID]
+    status: implemented
     tags: [tsn, synthesis, qbv, guard-band, tier2]
     fields:
       release: v0.22.0

artifacts/verification.yaml

@@ -2396,6 +2396,47 @@ artifacts:
       - type: satisfies
         target: REQ-TSN-SYNTH-QBV-SPLIT-BASE-001
 
+  - id: TEST-TSN-GUARDBAND
+    type: feature
+    title: 802.1Qbv guard-band-aware splitting — deployment-sound GCL synthesis
+    description: >
+      Verifies synthesize_gcl_split_guarded (REQ-TSN-SYNTH-QBV-GUARDBAND-001),
+      the deployment-sound splitter that charges the IEEE 802.1Q §8.6.8.4
+      transmission-overrun guard band the guard-free
+      REQ-TSN-SYNTH-QBV-SPLIT-BASE-001 ignores. spar-network::tsn unit
+      tests cover: (1) THE MODEL ANCHOR (go/no-go) —
+      guard_band_k1_equals_sync_error_at_eps_g pins the guard construction
+      NON-CIRCULARLY: for a single window, "emit a (D−g)-open window plus a
+      trailing closed g guard" yields a service curve BYTE-IDENTICAL to the
+      independently-derived tas_residual_service_with_sync_error at ε = g
+      (open D−g, latency C−D+g, rate R·(D−g)/C) — two derivations from
+      different premises agreeing is the evidence the guard is modelled
+      right; (2) DEGENERACY — guard_band_ps = 0 reproduces
+      synthesize_gcl_split byte-for-byte (no spurious zero-width windows);
+      (3) FEASIBLE SPLIT — a modest guard still splits, inserts explicit
+      closed guard windows of exactly g between class windows, tiles
+      [0,cycle), and meets every deadline under the SOUND
+      min_service_latency bound; (4) SOUND ROUNDING — a sub-nanosecond
+      guard rounds UP (never under-charges) and stays ns-exact in the
+      emitted blob; (5) THE RATE-LOSS CLIFF — a guard so wide that N·g
+      exceeds every round returns the structured GuardOversubscribed
+      (with the charged guard_ps), NOT a silently rate-starved/unsound GCL;
+      (6) MONOTONE — the guarded schedule is never COARSER (fewer windows)
+      than the guard-free one for the same demands; (7) INPUT VALIDATION —
+      empty demands and non-whole-ns/zero cycles rejected up front.
+      Self-certifying: the full guarded multi-window schedule is re-checked
+      through tas_residual_service + delay_bound before return, so an
+      unsound guard emission fails construction, not just the test.
+    fields:
+      method: automated-test
+      steps:
+        - run: "cargo test -p spar-network --lib -- guard"
+    status: passing
+    tags: [v0.22.0, network, tsn, synthesis, qbv, guard-band, oracle]
+    links:
+      - type: satisfies
+        target: REQ-TSN-SYNTH-QBV-GUARDBAND-001
+
   - id: TEST-TSN-EXPORT-YANG
     type: feature
     title: 802.1Qcw YANG/NETCONF export of a synthesized gate schedule