feat(network): Spar_Network property set + spar-network crate skeleton (Track D commit 1/6)

Cargo.toml

@@ -8,6 +8,7 @@ members = [
     "crates/spar-hir-def",
     "crates/spar-hir",
     "crates/spar-analysis",
+    "crates/spar-network",
     "crates/spar-transform",
     "crates/spar-cli",
     "crates/spar-codegen",
@@ -33,6 +34,7 @@ spar-base-db = { path = "crates/spar-base-db" }
 spar-hir-def = { path = "crates/spar-hir-def" }
 spar-hir = { path = "crates/spar-hir" }
 spar-analysis = { path = "crates/spar-analysis" }
+spar-network = { path = "crates/spar-network" }
 spar-render = { path = "crates/spar-render" }
 spar-solver = { path = "crates/spar-solver" }
 spar-sysml2 = { path = "crates/spar-sysml2" }

artifacts/requirements.yaml

@@ -1071,4 +1071,45 @@ artifacts:
     status: planned
     tags: [trace, verification, v080]
 
+  # ── TSN/Ethernet WCTT analysis (Track D, v0.8.0) ───────────────────
+
+  - id: REQ-NETWORK-001
+    type: requirement
+    title: Network switch modeling via Switch_Type discriminator
+    description: >
+      System shall support modeling of network switch components via
+      Spar_Network::Switch_Type discriminator. Switches are modeled as
+      `bus implementation` (Option C from PR #152 research) carrying the
+      Switch_Type enumeration (FIFO, Priority, TSN); Phase 1 covers FIFO
+      and Priority disciplines, Phase 2 introduces TSN-specific service
+      curves under a separate Spar_TSN property set.
+    status: planned
+    tags: [network, wctt, tsn, v080]
+
+  - id: REQ-NETWORK-002
+    type: requirement
+    title: Per-bus queue depth and forwarding latency
+    description: >
+      System shall support modeling of per-bus queue depth and
+      store-and-forward latency. Exposed via Spar_Network::Queue_Depth
+      (aadlinteger; per-port frame capacity) and
+      Spar_Network::Forwarding_Latency (Time_Range; per-hop BCET..WCET
+      switch-fabric/MAC contribution). Both feed the WCTT analysis
+      pass that lands later in Track D.
+    status: planned
+    tags: [network, wctt, v080]
+
+  - id: REQ-NETWORK-003
+    type: requirement
+    title: Per-port output rate (egress bandwidth)
+    description: >
+      System shall support modeling of per-port output rate (egress
+      bandwidth). Exposed via Spar_Network::Output_Rate (Data_Rate;
+      applies to bus and port). Distinct from
+      Communication_Properties::Output_Rate, which is a producer-side
+      Rate_Spec; Spar_Network::Output_Rate is the link/port egress
+      bandwidth used by the WCTT serialization-time term.
+    status: planned
+    tags: [network, wctt, v080]
+
   # Research findings tracked separately in research/findings.yaml

artifacts/verification.yaml

@@ -1364,3 +1364,30 @@ artifacts:
         target: REQ-TIMING-IRQ-002
       - type: satisfies
         target: REQ-TIMING-IRQ-003
+
+  - id: TEST-SPAR-NETWORK-PROPS
+    type: feature
+    title: Spar_Network property set surface tests
+    description: >
+      Unit tests in spar-hir-def/src/standard_properties.rs verifying
+      that Spar_Network is a known predefined property set, that each
+      of Switch_Type, Queue_Depth, Forwarding_Latency, and Output_Rate
+      resolves to the expected AADL type, that the set resolves via the
+      GlobalScope without an explicit `with` import, and that unknown
+      names in the set return None / ResolvedProperty::Unresolved.
+      Foundation for Track D (TSN/Ethernet WCTT, v0.8.0); subsequent
+      commits add the spar-network crate's NC primitives, the wctt
+      analysis pass, and the supporting Lean theorems.
+    fields:
+      method: automated-test
+      steps:
+        - run: cargo test -p spar-hir-def -- test_standard_properties_in_spar_network test_spar_network_property_set_resolved_via_global_scope test_spar_network_unknown_property_returns_none
+    status: passing
+    tags: [v0.8.0, network, wctt, tsn, properties]
+    links:
+      - type: satisfies
+        target: REQ-NETWORK-001
+      - type: satisfies
+        target: REQ-NETWORK-002
+      - type: satisfies
+        target: REQ-NETWORK-003

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

@@ -19,11 +19,12 @@ pub struct StandardProperty {
 
 /// All standard predefined property set names.
 ///
-/// Includes the AS5506 Appendix A predeclared sets plus two non-standard
-/// spar-defined sets (`Spar_Timing`, `Spar_Trace`) that support
-/// IRQ-aware RTA (Track A, v0.7.0) and closed-loop trace verification
-/// (v0.8.0 precursor). The spar-defined sets are treated like predefined
-/// sets so they resolve without explicit `with` imports.
+/// Includes the AS5506 Appendix A predeclared sets plus three non-standard
+/// spar-defined sets (`Spar_Timing`, `Spar_Trace`, `Spar_Network`) that
+/// support IRQ-aware RTA (Track A, v0.7.0), closed-loop trace verification
+/// (v0.8.0 precursor), and TSN/Ethernet WCTT analysis (Track D, v0.8.0).
+/// The spar-defined sets are treated like predefined sets so they resolve
+/// without explicit `with` imports.
 pub const STANDARD_PROPERTY_SET_NAMES: &[&str] = &[
     "Timing_Properties",
     "Communication_Properties",
@@ -35,6 +36,7 @@ pub const STANDARD_PROPERTY_SET_NAMES: &[&str] = &[
     "AADL_Project",
     "Spar_Timing",
     "Spar_Trace",
+    "Spar_Network",
 ];
 
 // ── Timing_Properties ───────────────────────────────────────────────
@@ -334,6 +336,42 @@ const SPAR_TRACE: &[(&str, &str)] = &[
     ("Expected_Mean", "Time"),
 ];
 
+// ── Spar_Network ────────────────────────────────────────────────────
+//
+// Non-standard property set defined by spar itself (not AS5506); used
+// for TSN/Ethernet WCTT analysis (Track D, v0.8.0). Provides the AADL
+// vocabulary for switch modeling under the Option C decision in
+// research PR #152: a switched bus is modeled as
+// `bus implementation` carrying a `Switch_Type` discriminator.
+//
+// Phase 1 (this milestone) covers FIFO + Priority networks. Phase 2's
+// TSN-specific properties land in a separate `Spar_TSN::*` set.
+//
+// See `docs/designs/track-d-tsn-wctt-research.md` §5.1.
+
+const SPAR_NETWORK: &[(&str, &str)] = &[
+    // Discriminator for the bus's forwarding discipline. `FIFO` and
+    // `Priority` cover Phase 1 (classical Ethernet, CAN, FlexRay
+    // priority-based). `TSN` is reserved for Phase 2's scheduled-traffic
+    // service curves; analysis passes treat it as opaque until the
+    // Spar_TSN property set lands.
+    ("Switch_Type", "enumeration (FIFO, Priority, TSN)"),
+    // Per-port queue capacity in frames. Bounds the burst that can
+    // accumulate at a switch egress before drops; an input to the
+    // backlog bound used by the WCTT analysis.
+    ("Queue_Depth", "aadlinteger"),
+    // Store-and-forward latency: per-hop best-case .. worst-case
+    // contribution from switch fabric and MAC processing. Modeled as
+    // Time_Range so analyses can preserve BCET..WCET separation.
+    ("Forwarding_Latency", "Time_Range"),
+    // Egress link bandwidth per port. Note: AADL's `Data_Rate` is a
+    // unit-typed integer (`aadlinteger units Data_Rate_Units`) in
+    // Communication_Properties; the type description here is the
+    // human-readable form. Proper unit-aware parsing of `Data_Rate`
+    // is deferred to the WCTT analysis pass (Track D commit 4).
+    ("Output_Rate", "Data_Rate"),
+];
+
 /// Helper: collect properties from a table into the result vector.
 fn collect_properties(
     table: &[(&'static str, &'static str)],
@@ -371,6 +409,7 @@ pub fn all_standard_properties() -> Vec<StandardProperty> {
     collect_properties(AADL_PROJECT, "AADL_Project", &mut result);
     collect_properties(SPAR_TIMING, "Spar_Timing", &mut result);
     collect_properties(SPAR_TRACE, "Spar_Trace", &mut result);
+    collect_properties(SPAR_NETWORK, "Spar_Network", &mut result);
 
     result
 }
@@ -398,6 +437,7 @@ fn lookup_table(set_lower: &str) -> Option<&'static [(&'static str, &'static str
         "aadl_project" => Some(AADL_PROJECT),
         "spar_timing" => Some(SPAR_TIMING),
         "spar_trace" => Some(SPAR_TRACE),
+        "spar_network" => Some(SPAR_NETWORK),
         _ => None,
     }
 }
@@ -444,6 +484,7 @@ mod tests {
         assert!(is_standard_property_set("AADL_Project"));
         assert!(is_standard_property_set("Spar_Timing"));
         assert!(is_standard_property_set("Spar_Trace"));
+        assert!(is_standard_property_set("Spar_Network"));
 
         // Case-insensitive
         assert!(is_standard_property_set("timing_properties"));
@@ -688,6 +729,77 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_standard_properties_in_spar_network() {
+        // Spar_Network is a known property set.
+        assert!(is_standard_property_set("Spar_Network"));
+
+        let props = standard_properties_in_set("Spar_Network");
+        assert_eq!(props.len(), 4);
+        assert!(props.contains(&"Switch_Type"));
+        assert!(props.contains(&"Queue_Depth"));
+        assert!(props.contains(&"Forwarding_Latency"));
+        assert!(props.contains(&"Output_Rate"));
+
+        // Each property resolves to its expected type.
+        assert_eq!(
+            standard_property_type("Spar_Network", "Switch_Type"),
+            Some("enumeration (FIFO, Priority, TSN)")
+        );
+        assert_eq!(
+            standard_property_type("Spar_Network", "Queue_Depth"),
+            Some("aadlinteger")
+        );
+        assert_eq!(
+            standard_property_type("Spar_Network", "Forwarding_Latency"),
+            Some("Time_Range")
+        );
+        assert_eq!(
+            standard_property_type("Spar_Network", "Output_Rate"),
+            Some("Data_Rate")
+        );
+
+        // Case-insensitive.
+        assert_eq!(
+            standard_property_type("spar_network", "switch_type"),
+            Some("enumeration (FIFO, Priority, TSN)")
+        );
+    }
+
+    #[test]
+    fn test_spar_network_property_set_resolved_via_global_scope() {
+        use crate::name::Name;
+        use crate::resolver::{GlobalScope, ResolvedProperty};
+
+        let scope = GlobalScope::from_trees(vec![]);
+
+        // Spar_Network::Switch_Type is resolvable without explicit `with`.
+        let result = scope.resolve_property(&Name::new("Spar_Network"), &Name::new("Switch_Type"));
+        assert!(
+            matches!(result, ResolvedProperty::PropertyDef { .. }),
+            "expected PropertyDef for Spar_Network::Switch_Type, got {:?}",
+            result
+        );
+    }
+
+    #[test]
+    fn test_spar_network_unknown_property_returns_none() {
+        use crate::name::Name;
+        use crate::resolver::{GlobalScope, ResolvedProperty};
+
+        // Lookup-table layer: unknown property in a known spar set is None.
+        assert_eq!(standard_property_type("Spar_Network", "Nonexistent"), None);
+
+        // Resolver layer: unknown property in a known spar set is Unresolved.
+        let scope = GlobalScope::from_trees(vec![]);
+        let result = scope.resolve_property(&Name::new("Spar_Network"), &Name::new("Nonexistent"));
+        assert!(
+            matches!(result, ResolvedProperty::Unresolved),
+            "expected Unresolved for Spar_Network::Nonexistent, got {:?}",
+            result
+        );
+    }
+
     #[test]
     fn test_spar_property_sets_resolved_via_global_scope() {
         use crate::name::Name;
@@ -736,8 +848,8 @@ mod tests {
     #[test]
     fn test_all_standard_properties_total_count() {
         let all = all_standard_properties();
-        // 12 + 13 + 14 + 14 + 7 + 25 + 4 + 13 + 4 + 4 = 110
-        assert_eq!(all.len(), 110);
+        // 12 + 13 + 14 + 14 + 7 + 25 + 4 + 13 + 4 + 4 + 4 = 114
+        assert_eq!(all.len(), 114);
     }
 
     #[test]

crates/spar-network/Cargo.toml

@@ -0,0 +1,11 @@
+[package]
+name = "spar-network"
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+description = "Network Calculus primitives for AADL WCTT analysis (TSN/Ethernet, Track D)"
+
+[dependencies]
+
+[dev-dependencies]

crates/spar-network/src/lib.rs

@@ -0,0 +1,53 @@
+//! Network Calculus primitives for AADL WCTT (Worst-Case Traversal Time)
+//! analysis.
+//!
+//! This crate is the home of spar's Track D effort (issue #149,
+//! research PR #152, design doc
+//! [`docs/designs/track-d-tsn-wctt-research.md`]). Its purpose is to
+//! host network-domain types and algorithms that are reused across
+//! analyses but kept separate from `spar-analysis` for the same reason
+//! `spar-solver` is a sibling crate: the math is general, has no
+//! AADL-specific diagnostic dependencies, and is independently
+//! testable.
+//!
+//! # Phasing
+//!
+//! - **Phase 1 (this milestone, v0.8.0):** types only. The crate is a
+//!   skeleton placeholder. The Spar_Network property set surface
+//!   landed in `spar-hir-def::standard_properties` alongside this
+//!   crate. Subsequent commits in Track D add the algorithm pieces:
+//!   network-graph extraction (commit 2), Network Calculus primitives
+//!   (commit 3), the `wctt.rs` analysis pass (commit 4), and Lean
+//!   theorems (commit 5).
+//! - **Phase 2 (v0.8.x or v0.9.0):** Network Calculus primitives —
+//!   arrival/service curves, min-plus convolution and deconvolution,
+//!   horizontal/vertical distance bounds. Exposed under
+//!   [`types`] and (later) `curve` modules.
+//! - **Phase 3:** TSN-shaped service curves (TAS/Qbv, Qbu preemption,
+//!   Qcr ATS). These build on Phase 2's primitives.
+//!
+//! # What is intentionally NOT in this crate yet
+//!
+//! - No `wctt.rs` — that lives in `spar-analysis` and lands later in
+//!   Track D.
+//! - No Network Calculus algebra — Phase 2 will introduce
+//!   `ArrivalCurve`, `ServiceCurve`, and the min-plus operators.
+//! - No TSN-specific service-curve generators — Phase 3.
+//! - No AADL-specific knowledge: this crate stays free of
+//!   `spar-hir-def`/`spar-hir`/diagnostic dependencies. Adapters
+//!   between `SystemInstance` and the network graph live in
+//!   `spar-analysis`.
+//!
+//! See the design doc for the full scope and the rationale behind the
+//! crate split.
+
+#![forbid(unsafe_code)]
+
+/// Placeholder module for network-domain types.
+///
+/// Phase 1 leaves this empty. Phase 2 will introduce
+/// `ArrivalCurve`, `ServiceCurve`, server-graph node/edge types, and
+/// the WCTT result record. The module is exposed today only to fix
+/// the public path so that downstream crates can already write
+/// `use spar_network::types::*;` without a future breaking change.
+pub mod types {}