feat(nc): gPTP ε budget + frame quantization (v0.9.1 soundness pass) (#186)

Two pure-soundness fixes flagged by the post-v0.9.0 reviewer:

1. **gPTP synchronization-error budget (Tier 2 #5)** — adds
   `Spar_TSN::Sync_Error` (Time, ps; bus + processor) carrying the
   per-hop 802.1AS-2020 sync error ε. The TAS dispatch in `wctt.rs`
   now subtracts ε from the effective open time and adds ε to the
   worst-case gate latency. Without ε the v0.8.1 TAS bounds were
   *technically unsound* — a frame can miss its window by ε in
   silicon. ε = 0 (unset) reproduces v0.8.1 byte-identically.
   Property count: 128 → 129; Spar_TSN per-set count: 6 → 7.

2. **Atomic-frame quantization (Tier 2 #8)** — adds per-hop
   `ceil(max_frame_bytes · 8e12 / link_rate_bps)` ps on the TAS
   and FIFO/Priority arms. Bytes-level NC undercounts by up to one
   MTU per hop because frames are atomic; the kernel was previously
   slightly optimistic. CBS arm unchanged (service curve absorbs
   the term). Preemption arm unchanged (replaces with fragment
   time). New `WcttFrameQuantization` Info diagnostic.

Existing wctt test bounds updated from optimistic to sound
(e.g. single-hop 1 Gbps: 12 µs → 24.144 µs; gated TAS half-rate:
29 µs → 41.144 µs). Golden fixture `classical_ethernet.expected.json`
updated to the sound bounds.

Test count: 2772 (was 2759 at v0.9.0; +13 new tests for sync_error
accessor, sync_error TAS integration, frame_quantization helper,
and quantization integration).

Closes Tier 2 reviewer items #5 + #8.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: avrabe

artifacts/requirements.yaml

@@ -1537,6 +1537,39 @@ artifacts:
     status: implemented
     tags: [network, tsn, wctt, preemption, qbu, v081]
 
+  # ── v0.9.1 NC soundness pass ──────────────────────────────────────
+
+  - id: REQ-NETWORK-009
+    type: requirement
+    title: gPTP synchronization-error budget for TAS bounds
+    description: >
+      Spar_TSN::Sync_Error (Time, picoseconds; applies to bus,
+      processor) carries the per-hop 802.1AS-2020 synchronization
+      error ε. The TAS dispatch in wctt.rs subtracts ε from the
+      effective open time and adds ε to the worst-case gate latency,
+      restoring soundness — current TAS bounds are technically
+      unsound without ε because a frame can miss its window by ε in
+      silicon. ε = 0 (unset) reproduces v0.8.1 behaviour
+      byte-identically. Per the post-v0.9.0 reviewer's Tier 2 #5.
+    status: implemented
+    tags: [network, tsn, wctt, soundness, gptp, v091]
+
+  - id: REQ-NETWORK-010
+    type: requirement
+    title: Atomic-frame quantization in NC per-hop bound
+    description: >
+      Bytes-level NC undercounts each hop's bound by up to one MTU
+      because frames are atomic but the kernel treats packets as
+      continuous. wctt.rs adds `ceil(max_frame_bytes · 8e12 /
+      link_rate_bps)` picoseconds per hop on the TAS and FIFO/Priority
+      arms. The CBS arm's closed-form latency already absorbs the
+      max-frame term; the preemption arm replaces it with the
+      fragment-time. New `WcttFrameQuantization` Info diagnostic
+      records the correction per hop. Per the post-v0.9.0 reviewer's
+      Tier 2 #8.
+    status: implemented
+    tags: [network, wctt, soundness, v091]
+
   # ── Track G: spar-insight discrepancy assistant (v0.9.0) ──────────
 
   - id: REQ-INSIGHT-001

artifacts/verification.yaml

@@ -2040,6 +2040,44 @@ artifacts:
       - type: satisfies
         target: REQ-TSN-004
 
+  - id: TEST-NC-SOUNDNESS
+    type: feature
+    title: gPTP ε budget + atomic-frame quantization soundness tests
+    description: >
+      Unit + integration tests covering the v0.9.1 soundness pass:
+      (1) `Spar_TSN::Sync_Error` accessor handles unset / typed
+      PropertyExpr / string fallback paths and unit conversions
+      (ps, ns, us, ms);
+      (2) `tas_residual_service_with_sync_error` shrinks
+      open_fraction by ε/cycle and grows worst_case_latency by ε;
+      ε equal to or exceeding a window's open_time clamps to
+      zero (gate effectively closed); ε = 0 reproduces v0.8.1
+      byte-identically;
+      (3) `frame_quantization_ps` returns ceil(max_frame · 8e12 /
+      link_rate_bps) — 1518 B at 100 Mbps ≈ 121440 ns; 64 B at 1 Gbps
+      ≈ 512 ns; rate-divides-evenly vs ceil-rounding cases; zero-rate
+      guard;
+      (4) wctt dispatch integration: TAS / FIFO arms emit
+      `WcttFrameQuantization` Info per hop and add the correction
+      to the per-hop delay; CBS / preemption arms remain unchanged
+      (their service curves already absorb / replace the max-frame
+      term); the v0.8.0 `single_hop_classical_ethernet`,
+      `multi_hop_chain_aggregates`, and TSN/TAS bound assertions
+      were updated to the sound numbers.
+    fields:
+      method: automated-test
+      steps:
+        - run: cargo test -p spar-network --lib -- tsn
+        - run: cargo test -p spar-analysis --lib -- wctt
+        - run: cargo test -p spar-analysis --test wctt_fixtures
+    status: passing
+    tags: [v0.9.1, network, wctt, soundness, gptp, quantization]
+    links:
+      - type: satisfies
+        target: REQ-NETWORK-009
+      - type: satisfies
+        target: REQ-NETWORK-010
+
   - id: TEST-INSIGHT-DISCREPANCY
     type: feature
     title: spar-insight CTF parser + 5-kind discrepancy detection

crates/spar-analysis/src/wctt.rs

@@ -56,9 +56,10 @@ use spar_network::extract::{
     extract_network_graph, read_forwarding_latency_ps, read_output_rate_bps, read_queue_depth,
 };
 use spar_network::tsn::{
-    CbsReservation, ClassOfService, GateSchedule, cbs_residual_service,
+    CbsReservation, ClassOfService, GateSchedule, cbs_residual_service, frame_quantization_ps,
     get_bandwidth_reservation_bps, get_class_of_service, get_frame_preemption, get_gate_schedule,
-    get_max_frame_size_bytes, is_express_stream, preemption_blocking_term_ps, tas_residual_service,
+    get_max_frame_size_bytes, get_sync_error_ps, is_express_stream, preemption_blocking_term_ps,
+    tas_residual_service_with_sync_error,
 };
 use spar_network::types::{NetworkGraph, NodeKind, SwitchType};
 
@@ -275,15 +276,39 @@ impl WcttAnalysis {
                 // about *when* class-K can transmit, not about
                 // ownership of bandwidth across competing streams.
                 let mut cbs_service: Option<ServiceCurve> = None;
+                // v0.9.1 NC soundness: a hop is "quantizable" iff its
+                // service curve does not already account for the
+                // atomic-frame max-MTU blocking term. The TAS arm and
+                // the FIFO/Priority fallback arm do not — they undercount
+                // the per-hop bound by up to one MTU because the
+                // bytes-level NC kernel treats packets as continuous.
+                // The CBS arm's `cbs_residual_service` already absorbs
+                // max-frame blocking via its closed-form latency; the
+                // preemption arm's `preemption_blocking_term_ps`
+                // *replaces* the same term with the much smaller
+                // fragment-time. Both of those leave `quantization_ps = 0`.
+                let mut quantization_ps: u64 = 0;
                 let svc = if matches!(st, SwitchType::Tsn) {
                     let bus_props = instance.properties_for(*sw_idx);
                     let bus_preemption = get_frame_preemption(bus_props).unwrap_or(false);
                     if let (Some(schedule), Some(cos)) =
                         (gate_schedule_for_bus.get(sw_idx), stream.cos)
                     {
-                        // Path 1: TAS service curve.
+                        // Path 1: TAS service curve, with the v0.9.1
+                        // gPTP synchronization-error budget ε applied
+                        // (subtracted from the effective open time,
+                        // added to the worst-case gate latency). When
+                        // `Spar_TSN::Sync_Error` is unset on the bus we
+                        // pass ε = 0, which reproduces the v0.8.1
+                        // service curve byte-identically.
                         let link_rate = link_rate_for_bus.get(sw_idx).copied().unwrap_or(0);
-                        let tas_svc = tas_residual_service(schedule, cos, link_rate);
+                        let sync_error_ps = get_sync_error_ps(bus_props).unwrap_or(0);
+                        let tas_svc = tas_residual_service_with_sync_error(
+                            schedule,
+                            cos,
+                            link_rate,
+                            sync_error_ps,
+                        );
                         let (open_ps, cycle_ps) = schedule.open_fraction(cos);
                         // open_fraction is reported as a percentage
                         // (integer-rounded toward zero) for human
@@ -298,7 +323,7 @@ impl WcttAnalysis {
                             severity: Severity::Info,
                             message: format!(
                                 "WcttTasGated: stream '{}' (CoS {}) on TSN switch '{}' at hop \
-                                 {}: open fraction {}% gate latency {} ps",
+                                 {}: open fraction {}% gate latency {} ps sync_error {} ps",
                                 stream_name,
                                 cos.0,
                                 graph
@@ -308,10 +333,16 @@ impl WcttAnalysis {
                                 hop_idx,
                                 open_pct,
                                 gate_latency_ps,
+                                sync_error_ps,
                             ),
                             path: stream_path.clone(),
                             analysis: self.name().to_string(),
                         });
+                        // TAS service curve: rate = R_link · ρ_K, but the
+                        // link itself still serializes one max-frame per
+                        // hop. Apply atomic-frame quantization at link rate.
+                        let bus_max_frame = get_max_frame_size_bytes(bus_props).unwrap_or(1518);
+                        quantization_ps = frame_quantization_ps(bus_max_frame, link_rate);
                         tas_svc
                     } else if let Some(idle_slope_bps) = stream.cbs_idle_slope_bps {
                         // Path 2: CBS service curve. Stream declares
@@ -496,10 +527,16 @@ impl WcttAnalysis {
                         continue;
                     }
                 } else {
-                    match service_for_bus.get(sw_idx) {
+                    let s = match service_for_bus.get(sw_idx) {
                         Some(s) => *s,
                         None => continue,
-                    }
+                    };
+                    // FIFO / Priority hop: bytes-level NC undercounts by
+                    // up to one MTU; apply atomic-frame quantization.
+                    let bus_props = instance.properties_for(*sw_idx);
+                    let bus_max_frame = get_max_frame_size_bytes(bus_props).unwrap_or(1518);
+                    quantization_ps = frame_quantization_ps(bus_max_frame, s.rate_bps);
+                    s
                 };
 
                 if svc.rate_bps == 0 {
@@ -585,10 +622,32 @@ impl WcttAnalysis {
                 };
 
                 // Per-hop delay using the tagged stream's α and the
-                // residual service.
+                // residual service. Then add `quantization_ps` for
+                // atomic-frame correctness (zero on CBS / preemption arms,
+                // computed at link rate on TAS / FIFO arms).
                 match delay_bound(&alpha, &residual) {
                     Ok(d) => {
                         total_delay_ps = total_delay_ps.saturating_add(d);
+                        if quantization_ps > 0 {
+                            total_delay_ps = total_delay_ps.saturating_add(quantization_ps);
+                            diags.push(AnalysisDiagnostic {
+                                severity: Severity::Info,
+                                message: format!(
+                                    "WcttFrameQuantization: stream '{}' at hop {} on switch \
+                                     '{}': atomic-frame correction +{} ns (max-frame serialization \
+                                     at link rate)",
+                                    stream_name,
+                                    hop_idx,
+                                    graph
+                                        .node(*sw_idx)
+                                        .map(|n| n.name.as_str())
+                                        .unwrap_or("<unknown>"),
+                                    quantization_ps / 1_000,
+                                ),
+                                path: stream_path.clone(),
+                                analysis: self.name().to_string(),
+                            });
+                        }
                     }
                     Err(NcError::UnservableFlow) | Err(NcError::UnstableServer) => {
                         // delay_bound also returns UnstableServer when
@@ -1357,9 +1416,11 @@ end Net;
             .filter(|d| d.message.starts_with("WcttBound"))
             .collect();
         assert_eq!(info.len(), 1, "exactly one stream expected: {:#?}", diags);
+        // v0.9.1 soundness: 12 µs (NC bytes-fluid) + 12.144 µs (atomic-frame
+        // quantization at 1 Gbps for 1518-byte MTU) = 24.144 µs.
         assert!(
-            info[0].message.contains("12000000 ps"),
-            "expected 12 us bound, got: {}",
+            info[0].message.contains("24144000 ps"),
+            "expected 24.144 us bound (12 us NC + 12.144 us frame quantization), got: {}",
             info[0].message
         );
     }
@@ -1585,9 +1646,11 @@ end Net;
             "expected 3 hops in: {}",
             info.message
         );
+        // v0.9.1 soundness: 51 µs (NC) + 3 × 12.144 µs (atomic-frame
+        // quantization, one per hop) = 87.432 µs.
         assert!(
-            info.message.contains("51000000 ps"),
-            "expected 51 us bound, got: {}",
+            info.message.contains("87432000 ps"),
+            "expected 87.432 us bound (51 us NC + 36.432 us quantization), got: {}",
             info.message
         );
     }
@@ -2083,8 +2146,8 @@ end Net;
             .find(|d| d.message.starts_with("WcttBound"))
             .unwrap_or_else(|| panic!("expected WcttBound: {:#?}", diags));
         assert!(
-            bound.message.contains("29000000 ps"),
-            "expected 29 us TAS bound, got: {}",
+            bound.message.contains("41144000 ps"),
+            "expected 41.144 us TAS bound (29 us gated + 12.144 us quantization), got: {}",
             bound.message
         );
     }
@@ -2143,8 +2206,9 @@ end Net;
             .iter()
             .find(|d| d.message.starts_with("WcttBound"))
             .unwrap();
-        // 12 us = 12_000_000 ps for the ungated single hop.
-        assert!(ungated_bound.message.contains("12000000 ps"));
+        // v0.9.1 soundness: 12 µs (NC) + 12.144 µs (atomic-frame
+        // quantization, 1518 B at 1 Gbps) = 24.144 µs.
+        assert!(ungated_bound.message.contains("24144000 ps"));
 
         // Same model, but with TSN+GCL applied (50% open for CoS 7).
         // The bound must exceed the ungated 12 us.
@@ -2204,10 +2268,11 @@ end Net;
             .iter()
             .find(|d| d.message.starts_with("WcttBound"))
             .unwrap();
-        assert!(gated_bound.message.contains("29000000 ps"));
+        // v0.9.1 soundness: 29 µs gated NC + 12.144 µs quantization = 41.144 µs.
+        assert!(gated_bound.message.contains("41144000 ps"));
 
-        // Strictly: 29 us > 12 us — the gated bound is more pessimistic
-        // (and correctly so) than the ungated line-rate bound.
+        // Strictly: 41.144 µs > 24.144 µs — the gated bound is more
+        // pessimistic (and correctly so) than the ungated line-rate bound.
     }
 
     // ── Test 13: TSN switch without GCL still defers ────────────────

crates/spar-analysis/tests/fixtures/wctt/classical_ethernet.expected.json

@@ -1,4 +1,6 @@
 [
-  "WcttBound: stream 'data_a (ecu_a → ecu_sink)' end-to-end WCTT 31666668 ps (1 hop)",
-  "WcttBound: stream 'data_b (ecu_b → ecu_sink)' end-to-end WCTT 31666668 ps (1 hop)"
-]
+  "WcttBound: stream 'data_a (ecu_a → ecu_sink)' end-to-end WCTT 43810668 ps (1 hop)",
+  "WcttBound: stream 'data_b (ecu_b → ecu_sink)' end-to-end WCTT 43810668 ps (1 hop)",
+  "WcttFrameQuantization: stream 'data_a (ecu_a → ecu_sink)' at hop 0 on switch 'sw': atomic-frame correction +12144 ns (max-frame serialization at link rate)",
+  "WcttFrameQuantization: stream 'data_b (ecu_b → ecu_sink)' at hop 0 on switch 'sw': atomic-frame correction +12144 ns (max-frame serialization at link rate)"
+]

crates/spar-hir-def/src/standard_properties.rs

@@ -508,6 +508,15 @@ const SPAR_TSN: &[(&str, &str)] = &[
     // hi/lo credit slope arithmetic is computed inside the analysis.
     // Applies to bus and port.
     ("Bandwidth_Reservation", "aadlinteger units Data_Rate_Units"),
+    // Per-hop gPTP (IEEE 802.1AS) synchronization-error budget ε. In
+    // a real TSN deployment the gate-control list is enforced against
+    // the local synchronized clock, which differs from the master
+    // clock by at most ε per hop; v0.9.1 NC soundness pass subtracts
+    // ε from the effective TAS open time and adds ε to the worst-case
+    // gate latency so the bounds remain sound under realistic clock
+    // accuracy. Default unset = 0 (legacy v0.8.1 behaviour).
+    // Applies to bus and processor.
+    ("Sync_Error", "aadlinteger units Time_Units"),
 ];
 
 /// Helper: collect properties from a table into the result vector.
@@ -1089,13 +1098,14 @@ mod tests {
         assert!(is_standard_property_set("Spar_TSN"));
 
         let props = standard_properties_in_set("Spar_TSN");
-        assert_eq!(props.len(), 6);
+        assert_eq!(props.len(), 7);
         assert!(props.contains(&"Stream_ID"));
         assert!(props.contains(&"Class_of_Service"));
         assert!(props.contains(&"Gate_Control_List"));
         assert!(props.contains(&"Max_Frame_Size"));
         assert!(props.contains(&"Frame_Preemption"));
         assert!(props.contains(&"Bandwidth_Reservation"));
+        assert!(props.contains(&"Sync_Error"));
 
         // Each property resolves to its expected type.
         assert_eq!(
@@ -1122,6 +1132,10 @@ mod tests {
             standard_property_type("Spar_TSN", "Bandwidth_Reservation"),
             Some("aadlinteger units Data_Rate_Units")
         );
+        assert_eq!(
+            standard_property_type("Spar_TSN", "Sync_Error"),
+            Some("aadlinteger units Time_Units")
+        );
 
         // Deliberately-wrong name returns None.
         assert_eq!(standard_property_type("Spar_TSN", "Nonexistent"), None);
@@ -1152,6 +1166,7 @@ mod tests {
             "Max_Frame_Size",
             "Frame_Preemption",
             "Bandwidth_Reservation",
+            "Sync_Error",
         ] {
             let result = scope.resolve_property(&Name::new("Spar_TSN"), &Name::new(prop_name));
             assert!(
@@ -1195,7 +1210,7 @@ mod tests {
     #[test]
     fn test_all_standard_properties_total_count() {
         let all = all_standard_properties();
-        // 12 + 13 + 14 + 14 + 8 + 25 + 4 + 13 + 5 + 4 + 5 + 4 + 1 + 6 = 128
+        // 12 + 13 + 14 + 14 + 8 + 25 + 4 + 13 + 5 + 4 + 5 + 4 + 1 + 7 = 129
         // (Timing + Communication + Memory + Deployment + Thread + Programming
         //  + Modeling + AADL_Project + Spar_Timing + Spar_Trace + Spar_Network
         //  + Spar_Migration + Spar_Power + Spar_TSN)
@@ -1206,7 +1221,8 @@ mod tests {
         // Spar_TSN: +5 for Stream_ID, Class_of_Service, Gate_Control_List,
         //   Max_Frame_Size, Frame_Preemption (Track D Phase 2 v0.8.1 c1)
         //   +1 for Bandwidth_Reservation (Track D Phase 2 v0.8.1 c3, CBS).
-        assert_eq!(all.len(), 128);
+        //   +1 for Sync_Error (v0.9.1 NC soundness, gPTP ε budget).
+        assert_eq!(all.len(), 129);
     }
 
     #[test]