From 9287df7a61dc49af89ac6d1771b774982a3a8d88 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 26 Jun 2026 11:17:48 +0200 Subject: [PATCH] feat(analysis): emit authoritative network-wide NC bound = min(PLP,TFA) (REQ-NC-PLP-MIN-001) network_wide_nc_bounds now emits a per-stream WcttAuthoritativeBound equal to the pointwise minimum of the network-wide TFA and PLP end-to-end delays. PLP and TFA are incomparable sound over-approximations; their min is the tightest sound per-flow bound and is itself sound (no new soundness surface). Falls back to TFA when PLP is absent (milp-solver off, or non-feed-forward). Oracle (TEST-NC-PLP-MIN): on the converging-tree counterexample where the fast stream's PLP (~1148us) exceeds its TFA (~1048us), the authoritative bound must equal TFA and sit strictly below PLP; and == min(PLP,TFA) for every stream; and == TFA when PLP is absent. Co-Authored-By: Claude Opus 4.8 (1M context) --- artifacts/requirements.yaml | 2 +- artifacts/verification.yaml | 32 +++++++++ crates/spar-analysis/src/wctt.rs | 112 ++++++++++++++++++++++++++++++- 3 files changed, 142 insertions(+), 4 deletions(-) diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index a010b72..08d0bda 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -3030,7 +3030,7 @@ artifacts: GATE: on the converging-bridge fixture the bridge's authoritative bound equals TFA (1048 µs) for the cross-burst flow, not the looser PLP. [SOLID — Bouillard arXiv:2010.09263] - status: proposed + status: implemented tags: [network-calculus, plp, bridge, substrate, tier1] fields: release: v0.22.0 diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index ec44723..44759a0 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -1911,6 +1911,38 @@ artifacts: - type: satisfies target: REQ-NC-PLP-CONVERGE-001 + - id: TEST-NC-PLP-MIN + type: feature + title: Authoritative network-wide NC bound is min(PLP, TFA) + description: > + Verifies REQ-NC-PLP-MIN-001: the bridge emits a per-stream + WcttAuthoritativeBound equal to the pointwise minimum of the + network-wide TFA and PLP end-to-end delays. The spar-analysis unit + test network_wide_authoritative_bound_is_min_of_plp_and_tfa runs the + converging-tree fixture (bridge_converge_aadl) — the documented + incomparability counterexample where the fast stream's pure PLP + (~1148µs) EXCEEDS its TFA (~1048µs) — and asserts: (1) one + authoritative bound per stream is emitted regardless of the + milp-solver feature; (2) with milp-solver, authoritative == min(PLP, + TFA) for every stream; (3) on the PLP>TFA cross-burst stream the + authoritative bound equals TFA and sits strictly below PLP, so a + regression that blindly reported the looser PLP would fail; (4) + without the milp-solver feature (PLP absent) the authoritative bound + equals TFA. Pure selection over two already-computed sound bounds — + min of two sound over-approximations is itself sound, adding no new + soundness surface; the reported bound is therefore never worse than + TFA while keeping the PLP win wherever PLP is tighter. + fields: + method: automated-test + steps: + - run: "cargo test -p spar-analysis --lib --features milp-solver network_wide_authoritative_bound" + - run: "cargo test -p spar-analysis --lib --no-default-features network_wide_authoritative_bound" + status: passing + tags: [v0.22.0, network, network-calculus, plp, tfa, bridge, oracle] + links: + - type: satisfies + target: REQ-NC-PLP-MIN-001 + - id: TEST-NC-PLP-STR type: feature title: TFA-strengthened PLP — tightening to EXACT (panco tfa=True oracle) diff --git a/crates/spar-analysis/src/wctt.rs b/crates/spar-analysis/src/wctt.rs index 3940ce2..47d5ac3 100644 --- a/crates/spar-analysis/src/wctt.rs +++ b/crates/spar-analysis/src/wctt.rs @@ -1049,16 +1049,27 @@ fn network_wide_nc_bounds( }); } + // The authoritative per-flow NC bound is min(PLP, TFA) (REQ-NC-PLP-MIN-001): + // PLP and TFA are incomparable sound over-approximations (both ≥ exact, + // neither dominates), so the tightest *sound* per-flow bound is their + // pointwise minimum. Seed with TFA (always present); the PLP arm below + // tightens it where PLP is smaller. When PLP is absent (feature off, or a + // non-feed-forward topology) the authoritative bound is TFA alone — never + // worse than TFA, with the PLP win wherever it holds. `min` over two sound + // bounds is itself sound, so this adds no new soundness surface. + #[cfg_attr(not(feature = "milp-solver"), allow(unused_mut))] + let mut authoritative_ps: Vec = tfa.flow_delay_ps.clone(); + // PLP: the polynomial-LP feed-forward bound (Bouillard arXiv:2010.09263). // Usually tighter than TFA, but PLP and TFA are *incomparable* // over-approximations — both sound (≥ exact), neither dominates: under // extreme cross-burst pure PLP can exceed TFA (see the // `network_wide_tfa_index_aligns_on_converging_tree` counterexample). We - // emit both; the authoritative per-flow bound is min(PLP, TFA). - // HiGHS/good_lp-backed, so gated behind `milp-solver` (off for wasm, + // emit the PLP line, tighten the authoritative bound, and (above) the TFA + // line. HiGHS/good_lp-backed, so gated behind `milp-solver` (off for wasm, // #259). A multi-successor / cyclic topology returns // `PlpError::NotFeedForward`; we then omit the PLP lines and the TFA - // numbers above remain the network-wide result. + // numbers stand as the authoritative result. #[cfg(feature = "milp-solver")] { use spar_network::plp::{PlpFlow, plp_bound}; @@ -1085,8 +1096,31 @@ fn network_wide_nc_bounds( analysis: analysis.to_string(), }); } + // Tighten the authoritative bound to min(PLP, TFA) per flow. + for (auth, &plp_ps) in authoritative_ps.iter_mut().zip(&plp.flow_delay_ps) { + *auth = (*auth).min(plp_ps); + } } } + + // Emit the authoritative per-flow bound = min(PLP, TFA) (REQ-NC-PLP-MIN-001). + // This is the number downstream consumers should trust: never worse than + // TFA, and the PLP win wherever PLP is tighter. + for (s, &delay_ps) in streams.iter().zip(&authoritative_ps) { + diags.push(AnalysisDiagnostic { + severity: Severity::Info, + message: format!( + "WcttAuthoritativeBound: stream '{}' network-wide authoritative \ + end-to-end delay {} ps ({} hop{})", + s.display_name(instance), + delay_ps, + s.hops.len(), + if s.hops.len() == 1 { "" } else { "s" }, + ), + path: component_path(instance, s.src_idx), + analysis: analysis.to_string(), + }); + } } /// End-to-end traversal-time bound computed by @@ -4010,4 +4044,76 @@ end NetConv; ); } } + + #[test] + fn network_wide_authoritative_bound_is_min_of_plp_and_tfa() { + // REQ-NC-PLP-MIN-001. On the converging tree the fast stream's PLP + // (~1148µs) EXCEEDS its TFA (~1048µs) — the documented incomparability + // counterexample. The authoritative bound must pick TFA for that + // stream (the min), never the looser PLP, while keeping the PLP win + // wherever PLP is tighter. min() over two sound bounds is itself sound. + let inst = instantiate(bridge_converge_aadl(), "NetConv", "Sys", "impl"); + let diags = WcttAnalysis::with_pmoo().analyze(&inst); + + let tfa = collect_delays(&diags, "WcttTfaBound"); + let auth = collect_delays(&diags, "WcttAuthoritativeBound"); + + // The authoritative bound is emitted regardless of the milp-solver + // feature (TFA-only when PLP is unavailable): one per stream. + assert_eq!( + auth.len(), + tfa.len(), + "one authoritative bound per stream: auth={auth:#?} tfa={tfa:#?}", + ); + + // Without PLP the authoritative bound is exactly TFA. + #[cfg(not(feature = "milp-solver"))] + for (name, &tfa_ps) in &tfa { + assert_eq!( + auth.get(name), + Some(&tfa_ps), + "no-PLP authoritative bound must equal TFA for '{name}'", + ); + } + + #[cfg(feature = "milp-solver")] + { + let plp = collect_delays(&diags, "WcttPlpBound"); + assert_eq!(plp.len(), tfa.len(), "one PLP bound per stream: {plp:#?}"); + + // Authoritative == min(PLP, TFA) for every stream. + for (name, &auth_ps) in &auth { + assert_eq!( + auth_ps, + tfa[name].min(plp[name]), + "authoritative for '{name}' must be min(PLP {}, TFA {})", + plp[name], + tfa[name], + ); + } + + // The counterexample stream: PLP > TFA, so the authoritative bound + // must equal TFA and sit strictly below PLP. A regression that + // blindly reported PLP would fail here. + let mut crossburst = None; + for name in auth.keys() { + if plp[name] > tfa[name] { + crossburst = Some(name.clone()); + break; + } + } + let crossburst = + crossburst.expect("converging tree must exhibit a PLP>TFA cross-burst stream"); + assert_eq!( + auth[&crossburst], tfa[&crossburst], + "for the PLP>TFA stream '{crossburst}' the authoritative bound must be TFA \ + ({}), not the looser PLP ({})", + tfa[&crossburst], plp[&crossburst], + ); + assert!( + auth[&crossburst] < plp[&crossburst], + "authoritative must be strictly below PLP on the cross-burst stream", + ); + } + } }