From 2895211f74c42bf00106bd3e64a82422f917af07 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 25 Apr 2026 11:39:06 +0200 Subject: [PATCH] feat(network): Spar_Network property set + spar-network crate skeleton (Track D commit 1/6) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Foundation for v0.8.0 Track D (TSN/Ethernet WCTT analysis, #149). This commit adds surface only — the new spar-network crate is a skeleton placeholder, and the Spar_Network property set provides the AADL vocabulary for switch modeling per the Option C decision in PR #152's research (`bus implementation` + `Switch_Type` discriminator). Spar_Network::{Switch_Type, Queue_Depth, Forwarding_Latency, Output_Rate} covers Phase 1 (FIFO + Priority networks). Phase 2 TSN-specific properties (Spar_TSN::*) land later. No analysis wiring, no Network Calculus primitives, no Lean theorems in this commit — those are Track D commits 2-5. New requirements: REQ-NETWORK-{001,002,003}. Co-Authored-By: Claude Opus 4.7 (1M context) --- Cargo.lock | 4 + Cargo.toml | 2 + artifacts/requirements.yaml | 41 ++++++ artifacts/verification.yaml | 27 ++++ .../spar-hir-def/src/standard_properties.rs | 126 +++++++++++++++++- crates/spar-network/Cargo.toml | 11 ++ crates/spar-network/src/lib.rs | 53 ++++++++ 7 files changed, 257 insertions(+), 7 deletions(-) create mode 100644 crates/spar-network/Cargo.toml create mode 100644 crates/spar-network/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index afc932d..f140fbc 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1296,6 +1296,10 @@ dependencies = [ "spar-syntax", ] +[[package]] +name = "spar-network" +version = "0.6.0" + [[package]] name = "spar-parser" version = "0.6.0" diff --git a/Cargo.toml b/Cargo.toml index 7635253..052b351 100644 --- a/Cargo.toml +++ b/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" } diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index 026d29d..c45cf13 100644 --- a/artifacts/requirements.yaml +++ b/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 diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 93f5ba9..d821d5e 100644 --- a/artifacts/verification.yaml +++ b/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 diff --git a/crates/spar-hir-def/src/standard_properties.rs b/crates/spar-hir-def/src/standard_properties.rs index cb13995..627ee8b 100644 --- a/crates/spar-hir-def/src/standard_properties.rs +++ b/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 { 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] diff --git a/crates/spar-network/Cargo.toml b/crates/spar-network/Cargo.toml new file mode 100644 index 0000000..1bb9936 --- /dev/null +++ b/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] diff --git a/crates/spar-network/src/lib.rs b/crates/spar-network/src/lib.rs new file mode 100644 index 0000000..51b1c87 --- /dev/null +++ b/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 {}