From 4d0729c1c1b3377c2ae9450f03544a4c03eeb115 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 14 Jun 2026 23:17:29 +0200 Subject: [PATCH] feat(network): TFA-strengthened PLP tightening to EXACT (REQ-NC-PLP-003) Adds `plp_bound_tfa_strengthened`: the polynomial LP (REQ-NC-PLP-001) with panco's per-server TFA-delay constraints (Bouillard `fifo/plpConstraints.py`, the `FifoLP(tfa=True)` path) layered on, tightening the bound toward the exact worst-case FIFO delay. The LP is fed spar's OWN independent FP-TFA per-server delays (`tfa_bound`), not panco's. Soundness is preserved because those delays are sound upper bounds (>= true), and the one-directional `t[h]-t[j] <= d[j]` constraints stay valid under any looser `d[j]`, so the strengthened bound never drops below EXACT. Adding constraints to the maximization can only lower the optimum, so strengthened <= pure PLP always. This repairs the pure-PLP / TFA incomparability (REQ-NC-PLP-MIN-001): on the converging-bridge net where pure PLP dataA 1148.33 us EXCEEDS TFA 1048.09 us (both sound, neither dominates), strengthening drives dataA to EXACT 1035.2 us - back below TFA. On three_server_line it drives the crossing flows 72.22/61.11 -> 68.4/58.4 us (= EXACT). Oracle (`nc_validation.rs::plp_str_xval`, feature milp-solver) pins the panco `tfa=True` column [68.4,58.4,57.98] and [1035.2,10030.7] under EXACT <= strengthened <= pure-PLP, plus the converge_bridge headline (strengthened dataA <= TFA where pure PLP could not). panco generator extended with the converging-bridge net (`oracles/panco/panco_bench.py`). Scope hygiene: v0.19.0 scope is now exactly {REQ-NC-PLP-CONVERGE-001, REQ-NC-PLP-003} (the implemented set); the 11 still-proposed/planned items are bumped to v0.20.0 for re-triage at v0.20.0 planning. REQ-NC-PLP-003 -> implemented; TEST-NC-PLP-STR -> passing. Co-Authored-By: Claude Opus 4.8 (1M context) --- artifacts/requirements.yaml | 37 ++- artifacts/verification.yaml | 40 +++ crates/spar-network/src/lib.rs | 2 +- crates/spar-network/src/plp.rs | 282 +++++++++++++++++- crates/spar-network/tests/nc_validation.rs | 169 +++++++++++ .../tests/oracles/panco/panco_bench.py | 26 +- 6 files changed, 521 insertions(+), 35 deletions(-) diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index dadce16..0e828b2 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -703,7 +703,7 @@ artifacts: status: planned tags: [solver, verification, v040] fields: - release: v0.19.0 + release: v0.20.0 - id: REQ-SOLVER-006 type: requirement @@ -741,7 +741,7 @@ artifacts: status: planned tags: [solver, safety, v040] fields: - release: v0.19.0 + release: v0.20.0 - id: REQ-SOLVER-009 type: requirement @@ -754,7 +754,7 @@ artifacts: status: planned tags: [solver, security, v040] fields: - release: v0.19.0 + release: v0.20.0 # ── Competitive Gap Requirements (v0.4.0+) ───────────────────────── @@ -2455,7 +2455,7 @@ artifacts: status: proposed tags: [ingest, sysml2, grammar] fields: - release: v0.19.0 + release: v0.20.0 - id: REQ-PLUGFEST-002 type: requirement @@ -2551,7 +2551,7 @@ artifacts: status: proposed tags: [trace-topology, reconciler] fields: - release: v0.19.0 + release: v0.20.0 links: - type: traces-to target: REQ-TRACE-TOPOLOGY-002 @@ -2570,7 +2570,7 @@ artifacts: status: proposed tags: [trace-topology, reconciler] fields: - release: v0.19.0 + release: v0.20.0 links: - type: traces-to target: REQ-TRACE-TOPOLOGY-005 @@ -2590,7 +2590,7 @@ artifacts: status: proposed tags: [trace-topology, reconciler, attestation] fields: - release: v0.19.0 + release: v0.20.0 links: - type: traces-to target: REQ-TRACE-TOPOLOGY-008 @@ -2639,7 +2639,7 @@ artifacts: status: proposed tags: [ingest, dbc, can, flows, tier1] fields: - release: v0.19.0 + release: v0.20.0 - id: REQ-INGEST-ARXML-001 type: requirement @@ -2657,7 +2657,7 @@ artifacts: status: proposed tags: [ingest, arxml, autosar, tier1] fields: - release: v0.19.0 + release: v0.20.0 - id: REQ-NC-TFA-001 type: requirement @@ -2799,8 +2799,19 @@ artifacts: longer build a byte-identical LP from spar's INDEPENDENT TFA engine — the oracle for this item is the pinned panco tfa=True PLP column under the sandwich EXACT ≤ plp ≤ TFA, NOT solver-precision LP identity. - [SOLID — Bouillard arXiv:2010.09263] - status: proposed + DELIVERED: `plp_bound_tfa_strengthened` (spar-network/src/plp.rs) feeds + the LP spar's OWN sound FP-TFA per-server delays (`tfa_bound`); soundness + is preserved because those delays are upper bounds (≥ true), and the + one-directional t[h]−t[j] ≤ d[j] constraints stay valid under any looser + d[j], so the bound never drops below EXACT. On the converging-bridge net + that BREAKS pure PLP (REQ-NC-PLP-MIN-001's counterexample: pure PLP dataA + 1148.33 > TFA 1048.09), strengthening drives dataA to EXACT 1035.2 — back + below TFA, restoring plp ≤ TFA where pure PLP could not. Oracle: + `nc_validation.rs::plp_str_xval` pins the panco tfa=True column + ([68.4,58.4,57.98] and [1035.2,10030.7]) under EXACT ≤ str ≤ pure-PLP, + plus the converge_bridge str-dataA ≤ TFA headline; panco generator + `oracles/panco/panco_bench.py`. [SOLID — Bouillard arXiv:2010.09263] + status: implemented tags: [network-calculus, plp, substrate, tier1] fields: release: v0.19.0 @@ -2936,7 +2947,7 @@ artifacts: status: proposed tags: [network-calculus, cbs, qav, audit, tier1] fields: - release: v0.19.0 + release: v0.20.0 # --- Tier 2: the product bet (synthesis → export), kill-gated --- @@ -2955,7 +2966,7 @@ artifacts: status: proposed tags: [tsn, synthesis, qbv, tier2] fields: - release: v0.19.0 + release: v0.20.0 - id: REQ-TSN-SYNTH-MILP-001 type: requirement diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 6be2912..355c4c3 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -1911,6 +1911,46 @@ artifacts: - type: satisfies target: REQ-NC-PLP-CONVERGE-001 + - id: TEST-NC-PLP-STR + type: feature + title: TFA-strengthened PLP — tightening to EXACT (panco tfa=True oracle) + description: > + Exercises plp_bound_tfa_strengthened (REQ-NC-PLP-003): the polynomial LP + with panco's per-server TFA-delay constraints added (Bouillard + fifo/plpConstraints.py, the FifoLP tfa=True path). Unlike TEST-NC-PLP + (a transcription of panco's PURE LP), this variant feeds the LP spar's + OWN independent FP-TFA per-server delays (tfa_bound), so reproducing + panco's tfa=True column is wiring-level agreement implied by + (LP port-fidelity from TEST-NC-PLP) ∧ (spar TFA ≈ panco TFA from + TEST-NC-VALIDATION), not a wholly independent recomputation. Two layers. + (1) plp.rs unit tests three_server_line_tfa_strengthened and + converge_bridge_tfa_strengthened pin [68.4,58.4,57.98] and + [1035.2,10030.7]. (2) the plp_str_xval module in nc_validation.rs + (feature milp-solver) pins the panco tfa=True column under three + guarantees: SOUNDNESS (strengthened ≥ panco EXACT — the strengthening + embeds sound per-server delays ≥ true, so the one-directional + t[h]−t[j] ≤ d[j] constraints keep the bound ≥ EXACT), AGREEMENT + (strengthened ≈ panco tfa=True within method tolerance), and MONOTONE + (strengthened ≤ pure PLP — adding constraints to a maximization can only + lower the optimum). converge_bridge additionally asserts the HEADLINE: + on the very net where PURE PLP exceeds TFA (dataA pure 1148.33 > TFA + 1048.09 — TEST-NC-PLP's incomparability counterexample), strengthening + drives dataA to EXACT 1035.2, BACK BELOW TFA — restoring plp ≤ TFA where + pure PLP could not. Panco generator oracles/panco/panco_bench.py + (FifoLP(polynomial=True, tfa=True)). + fields: + method: automated-test + steps: + - run: "cargo test -p spar-network --lib plp::" + - run: "cargo test -p spar-network --test nc_validation plp_str_xval" + status: passing + tags: [v0.19.0, network, network-calculus, plp, validation, oracle] + links: + - type: satisfies + target: REQ-NC-PLP-003 + - type: satisfies + target: REQ-NC-VALIDATION-001 + - id: TEST-NC-BRIDGE type: feature title: AADL instance → network-wide NC solver bridge diff --git a/crates/spar-network/src/lib.rs b/crates/spar-network/src/lib.rs index 64b51f6..1dd0beb 100644 --- a/crates/spar-network/src/lib.rs +++ b/crates/spar-network/src/lib.rs @@ -67,7 +67,7 @@ pub use curves::{ }; pub use extract::extract_network_graph; #[cfg(feature = "milp-solver")] -pub use plp::{PlpBound, PlpError, PlpFlow, plp_bound}; +pub use plp::{PlpBound, PlpError, PlpFlow, plp_bound, plp_bound_tfa_strengthened}; #[cfg(feature = "milp-solver")] pub use pmoo::{CompetingFlow, LpError, PmooBound, TaggedFlow, ludb_bound}; pub use tfa::{ diff --git a/crates/spar-network/src/plp.rs b/crates/spar-network/src/plp.rs index 517783c..8df32c9 100644 --- a/crates/spar-network/src/plp.rs +++ b/crates/spar-network/src/plp.rs @@ -7,10 +7,23 @@ //! whole aggregate (cheap, valid under cycles, but loose), and where //! [`crate::pmoo`] is a closed form restricted to tandems, PLP solves a //! *single linear program per flow* over a finite set of "interesting" -//! time instants and recovers a delay bound that is provably -//! `EXACT ≤ plp ≤ TFA` and, on feed-forward trees, materially tighter -//! than TFA on the very topologies (lines with overlapping cross-traffic) -//! where PMOO/LUDB do not apply. +//! time instants. This module exposes two variants: +//! +//! * [`plp_bound`] — the **pure** polynomial LP (REQ-NC-PLP-001). Sound +//! (`≥ EXACT`) and, on most feed-forward trees, materially tighter than +//! TFA on the very topologies (lines with overlapping cross-traffic) +//! where PMOO/LUDB do not apply. It is **not** universally `≤ TFA`, +//! though: pure PLP and TFA are *incomparable* over-approximations — +//! on a converging tree with a slow branch the cross-burst at the shared +//! sink can inflate pure PLP *above* TFA (the `converge_bridge` fixture: +//! pure PLP 1148.33 µs > TFA 1048.09 µs ≥ EXACT 1035.2). The authoritative +//! feed-forward bound is therefore `min(PLP, TFA)` (REQ-NC-PLP-MIN-001). +//! * [`plp_bound_tfa_strengthened`] — the **TFA-strengthened** LP +//! (REQ-NC-PLP-003): adds panco's `tfa=True` per-server TFA-delay +//! constraints, tightening the optimum toward the exact worst case. On +//! the validation fixtures it reaches EXACT (3-hop line 72.22 → 68.4 µs; +//! `converge_bridge` 1148.33 → 1035.2, back under TFA), restoring the +//! `EXACT ≤ plp ≤ TFA` sandwich that the *pure* LP can break. //! //! The formulation is Bouillard's polynomial-size LP (arXiv:2010.09263): //! a *time-expanded* model whose variables are the cumulative arrival @@ -33,19 +46,19 @@ //! solver precision), not an independent soundness proof of the PLP //! *method* — that is the deferred simulation floor REQ-NC-SIM-FLOOR-001. //! -//! Two deliberate scope cuts, each its own requirement: +//! [`plp_bound_tfa_strengthened`] adds the `tfa=True` strengthening on top of +//! this pure port (REQ-NC-PLP-003); it embeds spar's *own* per-server TFA +//! delays, so — unlike the pure LP — it is not byte-identical to panco and is +//! pinned against panco's `tfa=True` column under the `EXACT ≤ plp ≤ TFA` +//! sandwich rather than to solver-precision LP identity. +//! +//! One deliberate scope cut remains, its own requirement: //! //! * **Generic topology — forks and cycles** (panco's `edges_forest` //! decomposition + LP fixpoint, and the "PLP converges where TFA diverges //! at high utilization" claim) — REQ-NC-PLP-002. This build projects onto //! single-successor sink-trees, so a cycle *or* a fork (the latter still //! feed-forward) is rejected here with [`PlpError::NotFeedForward`]. -//! * **Tightening to the exact worst case** via panco's TFA-strengthened -//! LP (`tfa=True`, which embeds per-server TFA delays in the program) — -//! REQ-NC-PLP-003. The *pure* LP ported here is looser than EXACT on -//! some trees (e.g. 72.22 vs 68.4 µs on a 3-hop line) but is the only -//! variant spar can build *byte-identically* to panco from its own -//! model, which is what makes the solver-precision pin meaningful. //! //! # Units //! @@ -72,6 +85,7 @@ use good_lp::{ }; use crate::curves::{ArrivalCurve, ServiceCurve}; +use crate::tfa::{TfaError, TfaFlow, tfa_bound}; /// Per-link maximum-service ("shaping") rate, in bits/s. Matches the /// non-binding `TokenBucket(0, 1e12)` the cross-validation oracle pins for @@ -181,6 +195,40 @@ impl core::error::Error for PlpError {} /// projection. Returns the per-flow delay bounds in picoseconds, or a /// [`PlpError`]. pub fn plp_bound(flows: &[PlpFlow], services: &[ServiceCurve]) -> Result { + plp_bound_impl(flows, services, false) +} + +/// TFA-strengthened PLP delay bounds (REQ-NC-PLP-003). +/// +/// Identical to [`plp_bound`] but adds panco's `tfa=True` *TFA-delay +/// constraints* to each per-flow LP: for every server `j` the date-index +/// spread is bounded by `j`'s per-server TFA delay `D_j`, which embeds the +/// total-flow bound inside the polynomial program and tightens the optimum +/// toward the exact worst case (on the validation fixtures it drives PLP from +/// pure-LP slack to EXACT — e.g. `three_server_line` 72.22 → 68.4 µs, the +/// Bouillard–Stea ELP). +/// +/// The `D_j` are computed by spar's **own** [`crate::tfa::tfa_bound`] — an +/// *independent* sound per-server upper delay — not panco's internal `TfaLP`. +/// A sound (≥ true) `D_j` keeps the strengthened LP sound: the extra +/// constraints only forbid date spreads no real arrival can produce, so the +/// optimum stays `≥ EXACT`. Because the embedded delays come from a different +/// TFA engine, the LP is **not** byte-identical to panco's `tfa=True` program +/// (unlike [`plp_bound`] vs `tfa=False`); the oracle for this path is the +/// pinned panco `tfa=True` column under the sandwich `EXACT ≤ plp ≤ TFA`, not +/// solver-precision LP identity (see REQ-NC-PLP-003). +pub fn plp_bound_tfa_strengthened( + flows: &[PlpFlow], + services: &[ServiceCurve], +) -> Result { + plp_bound_impl(flows, services, true) +} + +fn plp_bound_impl( + flows: &[PlpFlow], + services: &[ServiceCurve], + strengthen: bool, +) -> Result { if flows.is_empty() || services.is_empty() { return Err(PlpError::EmptyNetwork); } @@ -281,11 +329,58 @@ pub fn plp_bound(flows: &[PlpFlow], services: &[ServiceCurve]) -> Result> = if strengthen { + let tfa_flows: Vec = flows + .iter() + .map(|f| TfaFlow { + alpha: f.alpha, + path: f.path.clone(), + }) + .collect(); + let res = tfa_bound(&tfa_flows, services).map_err(|e| match e { + TfaError::Unstable { + server, + agg_rate_bps, + service_rate_bps, + } => PlpError::Unstable { + server, + agg_rate_bps, + service_rate_bps, + }, + _ => PlpError::SolverFailed, + })?; + Some( + res.server_delay_ps + .iter() + .map(|&d| d as f64 / 1.0e6) + .collect(), + ) + } else { + None + }; + // ── Per-flow LP on the sink-tree projection ────────────────────────── let paths: Vec<&[usize]> = flows.iter().map(|f| f.path.as_slice()).collect(); let mut flow_delay_ps = Vec::with_capacity(flows.len()); for foi in 0..flows.len() { - let sub = SubNetwork::project(foi, flows, services, &paths, &predecessors)?; + let sub = SubNetwork::project( + foi, + flows, + services, + &paths, + &predecessors, + server_tfa_us.as_deref(), + )?; let delay_us = sub.solve()?; // Ceiling-round to ps so the reported bound never dips below the // LP's continuous optimum (pessimism direction). @@ -420,6 +515,10 @@ struct SubNetwork { t_max: Vec, /// Number of date variables `t_0 … t_{num_dates-1}`. num_dates: usize, + /// `tfa_delay_us[j]` — server `j`'s per-server TFA delay (µs) for the + /// TFA-strengthening constraints (REQ-NC-PLP-003); `None` for the pure + /// polynomial LP (REQ-NC-PLP-001). + tfa_delay_us: Option>, } impl SubNetwork { @@ -431,6 +530,7 @@ impl SubNetwork { services: &[ServiceCurve], paths: &[&[usize]], predecessors: &[Vec], + server_tfa_us: Option<&[f64]>, ) -> Result { // backward_search: all servers with a directed path to foi's sink. let sink = *paths[foi].last().expect("non-empty path checked"); @@ -521,6 +621,11 @@ impl SubNetwork { // times(num_servers, depth) → date windows and total date count. let (t_min, t_max, num_dates) = times(num_servers, &depth); + // Sub-select the global per-server TFA delays into local order + // (panco `sub_tfa_delays = [tfa_delays[j] for j in list_servers]`). + let tfa_delay_us = + server_tfa_us.map(|d| list_servers.iter().map(|&g| d[g]).collect::>()); + Ok(SubNetwork { num_servers, foi: local_foi, @@ -536,6 +641,7 @@ impl SubNetwork { t_min, t_max, num_dates, + tfa_delay_us, }) } @@ -681,9 +787,32 @@ impl SubNetwork { } } - // (arrival_shaping, sfa_delay, tfa_delay constraints are all empty - // for the pure feed-forward LP: no arrival_shaping groups, and the - // sfa/tfa delay vectors are None — see module docs.) + // /* TFA delay constraints */ (REQ-NC-PLP-003; panco `tfa=True`) + // Bound each server's date-index spread by its per-server TFA delay + // d[j] (µs), embedding the total-flow bound in the polynomial LP and + // tightening the optimum toward exact. Mirrors panco's + // `plpConstraints.tfa_delay_constraints`: + // sink j (== num_servers-1): t[0] − t[t_min[j]] ≤ d[j] + // non-sink j → h: t[t_min[h]+k] − t[t_min[j]+k] ≤ d[j] + // for k in 0..=depth[h]+1 (panco `range(depth[h]+2)`). + // Every index stays within its server's date window by construction + // (see `times`). For the pure LP (REQ-NC-PLP-001) `tfa_delay_us` is + // None and this block is skipped — the LP is then byte-identical to + // panco's `tfa=False` program. + if let Some(d) = &self.tfa_delay_us { + for j in 0..self.num_servers { + if j == self.num_servers - 1 { + cons.push(constraint!(t[0] - t[self.t_min[j]] <= d[j])); + } else { + let h = self.successor[j].expect("non-sink has a successor"); + for k in 0..=(self.depth[h] + 1) { + cons.push(constraint!( + t[self.t_min[h] + k] - t[self.t_min[j] + k] <= d[j] + )); + } + } + } + } // /* Objective */ max t_0 − t_{t_min[first server of foi]}. let src = self.t_min[self.path[self.foi][0]]; @@ -809,6 +938,129 @@ mod tests { ); } + /// Assert each TFA-strengthened bound matches the pinned panco `tfa=True` + /// column (µs, `FifoLP(polynomial=True, tfa=True)`) to solver precision, + /// and lies in the sandwich `EXACT ≤ strengthened ≤ pure-PLP` (REQ-NC-PLP-003). + fn check_strengthened( + name: &str, + flows: &[PlpFlow], + services: &[ServiceCurve], + tfa_true_us: &[f64], + exact_us: &[f64], + tol: f64, + ) { + let pure = plp_bound(flows, services).unwrap_or_else(|e| panic!("{name} pure: {e}")); + let strong = + plp_bound_tfa_strengthened(flows, services).unwrap_or_else(|e| panic!("{name}: {e}")); + assert_eq!( + strong.flow_delay_ps.len(), + tfa_true_us.len(), + "{name}: count" + ); + for (i, &got_ps) in strong.flow_delay_ps.iter().enumerate() { + let got_us = got_ps as f64 / US_PS as f64; + let exact_ps = (exact_us[i] * US_PS as f64).round() as u64; + // Soundness floor: strengthened ≥ EXACT (never undercut the truth). + assert!( + got_ps >= exact_ps, + "{name} flow {i}: UNSOUND — strengthened {got_us:.4} µs < exact {:.4} µs", + exact_us[i] + ); + // Tightening: strengthened ≤ pure-PLP (adding constraints to a + // maximising LP can only lower the optimum). + assert!( + got_ps <= pure.flow_delay_ps[i], + "{name} flow {i}: strengthened {got_us:.4} µs > pure-PLP {:.4} µs (must tighten)", + pure.flow_delay_ps[i] as f64 / US_PS as f64 + ); + // Port fidelity: match panco's tfa=True column to solver precision. + let rel = (got_us - tfa_true_us[i]).abs() / tfa_true_us[i]; + assert!( + rel <= tol, + "{name} flow {i}: strengthened {got_us:.4} µs disagrees with panco tfa=True {:.4} µs by {:.3}% (> {:.3}%)", + tfa_true_us[i], + rel * 100.0, + tol * 100.0 + ); + } + } + + /// REQ-NC-PLP-003 on `three_server_line`: TFA-strengthening drives pure + /// PLP `[72.22, 61.11, 57.98]` to panco's `tfa=True` column + /// `[68.4, 58.4, 57.98]` = the Bouillard–Stea EXACT bound. spar's own + /// independent per-server TFA delays are tight enough to reach exact here. + #[test] + fn three_server_line_tfa_strengthened() { + let services = vec![ + ServiceCurve::rate_latency(GBPS, 10 * US_PS), + ServiceCurve::rate_latency(GBPS, 10 * US_PS), + ServiceCurve::rate_latency(GBPS, 10 * US_PS), + ]; + let flows = vec![ + flow(FRAME, HUNDRED_MBPS, &[0, 1, 2]), + flow(FRAME, HUNDRED_MBPS, &[0, 1]), + flow(FRAME, HUNDRED_MBPS, &[1, 2]), + ]; + check_strengthened( + "three_server_line", + &flows, + &services, + &[68.4, 58.4, 57.98], + &[68.4, 58.4, 57.98], + 1e-4, + ); + } + + /// REQ-NC-PLP-003 on the converging-bridge net — the pathological shape + /// where *pure* PLP overshoots TFA (dataA pure 1148.33 µs > TFA 1048.09). + /// TFA-strengthening drives it back to panco's `tfa=True` column + /// `[1035.2, 10030.7]` = EXACT, restoring the `≤ TFA` sandwich that pure + /// PLP violated (1035.2 ≤ 1048.09). This is the concrete payoff: the + /// strengthened bound is the tighter, sound choice on the net that broke + /// the universal pure-PLP-≤-TFA claim (see `wctt.rs::bridge_converge_aadl`). + #[test] + fn converge_bridge_tfa_strengthened() { + use crate::tfa::{TfaFlow, tfa_bound}; + // topological order: sw_a fast [0], sw_b slow 10000µs [1], sw_c sink [2]. + let services = vec![ + ServiceCurve::rate_latency(GBPS, 5 * US_PS), + ServiceCurve::rate_latency(GBPS, 10_000 * US_PS), + ServiceCurve::rate_latency(GBPS, 5 * US_PS), + ]; + let flows = vec![ + flow(FRAME, HUNDRED_MBPS, &[0, 2]), + flow(FRAME, HUNDRED_MBPS, &[1, 2]), + ]; + check_strengthened( + "converge_bridge", + &flows, + &services, + &[1035.2, 10030.7], + &[1035.2, 10030.7], + 1e-4, + ); + // The payoff, asserted directly: strengthened dataA ≤ network-wide TFA + // dataA, even though pure PLP dataA exceeded it. + let strong = plp_bound_tfa_strengthened(&flows, &services).unwrap(); + let tfa = tfa_bound( + &flows + .iter() + .map(|f| TfaFlow { + alpha: f.alpha, + path: f.path.clone(), + }) + .collect::>(), + &services, + ) + .unwrap(); + assert!( + strong.flow_delay_ps[0] <= tfa.flow_delay_ps[0], + "strengthened dataA {} must be ≤ TFA {} (the sandwich pure PLP broke)", + strong.flow_delay_ps[0], + tfa.flow_delay_ps[0] + ); + } + /// fixture 3 — `three_server_line`: tagged `[0,1,2]`, cross1 `[0,1]`, /// cross2 `[1,2]`. The discriminating fixture: pure PLP `[72.22, 61.11, /// 57.98]` is strictly inside the sandwich (EXACT `[68.4, 58.4, 57.98]`, diff --git a/crates/spar-network/tests/nc_validation.rs b/crates/spar-network/tests/nc_validation.rs index 84b596c..30b8d94 100644 --- a/crates/spar-network/tests/nc_validation.rs +++ b/crates/spar-network/tests/nc_validation.rs @@ -400,3 +400,172 @@ mod plp_xval { ); } } + +// ─── TFA-strengthened PLP (REQ-NC-PLP-003) ────────────────────────────────── +// +// `plp_bound_tfa_strengthened` adds panco's `tfa=True` per-server TFA-delay +// constraints to the polynomial LP (Bouillard `fifo/plpConstraints.py`), +// tightening the bound toward EXACT. The LP is still spar's port of panco's +// (as in the pure-PLP block), but here it is fed spar's OWN independent FP-TFA +// per-server delays (`tfa_bound`) rather than panco's, so reproducing panco's +// `tfa=True` column is a wiring-regression pin — agreement implied by +// (LP port-fidelity, the `plp_xval` block) ∧ (spar TFA ≈ panco TFA, the TFA +// block) — not a wholly independent recomputation. Soundness is preserved +// because spar's per-server delays are themselves sound upper bounds (≥ true +// delay), and the one-directional `t[h]−t[j] ≤ d[j]` constraints stay valid +// under any looser `d[j]`. +// +// The oracle pins the panco `tfa=True` column (regenerated offline from the +// venv, `FifoLP(polynomial=True, tfa=True)`), and asserts the three guarantees +// that matter: +// (1) SOUNDNESS — strengthened ≥ panco EXACT (independent ELP floor). +// (2) AGREEMENT — strengthened ≈ panco `tfa=True` within method tolerance. +// (3) MONOTONE — strengthened ≤ pure PLP (strengthening can only tighten). +// `converge_bridge` additionally asserts the headline: strengthened dataA ≤ +// TFA, on the very net where *pure* PLP exceeds TFA (1148.33 > 1048.09). The +// strengthening drives it to EXACT (1035.2), restoring `plp ≤ TFA` — the whole +// point of REQ-NC-PLP-003. +#[cfg(feature = "milp-solver")] +mod plp_str_xval { + use super::*; + use spar_network::{PlpFlow, plp_bound, plp_bound_tfa_strengthened, tfa_bound}; + + /// Method-agreement tolerance for the strengthened LP. spar reproduces + /// panco's `tfa=True` column to the pinned 2 decimals; the slack absorbs + /// per-server ps-rounding in both spar's TFA delays and the LP (the same + /// ≤0.056 % regime as the TFA block), while still failing on any real + /// formulation drift (~200 ps at 68 µs). + const PLP_STR_TOL: f64 = 0.003; + + fn plp_flow(burst: u64, rate: u64, path: &[usize]) -> PlpFlow { + PlpFlow { + alpha: ArrivalCurve::affine(burst, rate), + path: path.to_vec(), + } + } + + /// For one fixture: the strengthened bound must (1) be `≥` panco EXACT, + /// (2) match the pinned panco `tfa=True` column within `PLP_STR_TOL`, and + /// (3) be `≤` spar's own pure PLP on the same fixture (strengthening never + /// loosens). Returns spar's strengthened per-flow delays (ps) so callers + /// can pin extra net-specific invariants. + fn check_plp_str( + name: &str, + flows: &[PlpFlow], + services: &[ServiceCurve], + panco_tfa_true_us: &[f64], + panco_exact_us: &[f64], + ) -> Vec { + let r = plp_bound_tfa_strengthened(flows, services) + .unwrap_or_else(|e| panic!("{name}: plp_bound_tfa_strengthened failed: {e}")); + let pure = plp_bound(flows, services) + .unwrap_or_else(|e| panic!("{name}: pure plp_bound failed: {e}")); + + assert_eq!( + r.flow_delay_ps.len(), + panco_tfa_true_us.len(), + "{name}: flow count" + ); + for (i, &str_ps) in r.flow_delay_ps.iter().enumerate() { + let exact_ps = (panco_exact_us[i] * US_PS as f64).round() as u64; + // (1) SOUNDNESS floor — strengthening must not undercut EXACT. + assert!( + str_ps >= exact_ps, + "{name} flow {i}: UNSOUND — strengthened {str_ps} ps < panco exact {exact_ps} ps", + ); + // (2) AGREEMENT — track panco's tfa=True column (method-level). + let str_us = str_ps as f64 / US_PS as f64; + let rel = (str_us - panco_tfa_true_us[i]).abs() / panco_tfa_true_us[i]; + assert!( + rel <= PLP_STR_TOL, + "{name} flow {i}: strengthened {str_us:.4} µs disagrees with panco tfa=True \ + {:.4} µs by {:.3}% (> {:.3}% tol)", + panco_tfa_true_us[i], + rel * 100.0, + PLP_STR_TOL * 100.0, + ); + // (3) MONOTONE — strengthened ≤ pure PLP (only tightens). + assert!( + str_ps <= pure.flow_delay_ps[i], + "{name} flow {i}: strengthened {str_ps} ps EXCEEDS pure PLP {} ps \ + (strengthening must never loosen)", + pure.flow_delay_ps[i], + ); + } + r.flow_delay_ps + } + + /// `three_server_line` — strengthening drives the two crossing flows from + /// pure PLP `[72.22, 61.11, 57.98]` down to EXACT `[68.4, 58.4, 57.98]` + /// (= panco `tfa=True`). + #[test] + fn panco_three_server_line_plp_str() { + let services = vec![ + ServiceCurve::rate_latency(GBPS, 10 * US_PS), + ServiceCurve::rate_latency(GBPS, 10 * US_PS), + ServiceCurve::rate_latency(GBPS, 10 * US_PS), + ]; + let flows = vec![ + plp_flow(FRAME, HUNDRED_MBPS, &[0, 1, 2]), + plp_flow(FRAME, HUNDRED_MBPS, &[0, 1]), + plp_flow(FRAME, HUNDRED_MBPS, &[1, 2]), + ]; + check_plp_str( + "three_server_line", + &flows, + &services, + &[68.4, 58.4, 57.98], + &[68.4, 58.4, 57.98], + ); + } + + /// `converge_bridge` (wctt.rs::bridge_converge_aadl) — THE net that breaks + /// pure PLP. Two talkers merge at a shared sink: dataA `[0,2]` (fast→fast), + /// dataB `[1,2]` (slow→fast), sink = 2. Server latencies 5 µs / 10000 µs / + /// 5 µs. Pure PLP gives dataA 1148.33 µs > TFA 1048.09 µs (both sound, but + /// incomparable). Strengthening drives dataA to EXACT 1035.2 µs, *below* + /// TFA — the REQ-NC-PLP-003 fix. Pinned panco `tfa=True` = `[1035.2, + /// 10030.7]` = EXACT. + #[test] + fn panco_converge_bridge_plp_str() { + let services = vec![ + ServiceCurve::rate_latency(GBPS, 5 * US_PS), // sw_a fast = 0 + ServiceCurve::rate_latency(GBPS, 10_000 * US_PS), // sw_b slow = 1 + ServiceCurve::rate_latency(GBPS, 5 * US_PS), // sw_c fast sink = 2 + ]; + let flows = vec![ + plp_flow(FRAME, HUNDRED_MBPS, &[0, 2]), // dataA + plp_flow(FRAME, HUNDRED_MBPS, &[1, 2]), // dataB + ]; + let str_ps = check_plp_str( + "converge_bridge", + &flows, + &services, + &[1035.2, 10030.7], + &[1035.2, 10030.7], + ); + + // Headline: strengthened dataA ≤ TFA dataA, where *pure* PLP exceeds + // it. This is the incomparability that REQ-NC-PLP-003 repairs. + let tfa_flows: Vec = flows + .iter() + .map(|f| affine_flow(f.alpha.burst_bytes, f.alpha.sustained_rate_bps, &f.path)) + .collect(); + let tfa = tfa_bound(&tfa_flows, &services).expect("tfa ceiling"); + let pure = plp_bound(&flows, &services).expect("pure plp"); + assert!( + pure.flow_delay_ps[0] > tfa.flow_delay_ps[0], + "converge_bridge: precondition broke — pure PLP dataA {} ps should EXCEED \ + TFA {} ps (the pure-PLP incomparability this fix targets)", + pure.flow_delay_ps[0], + tfa.flow_delay_ps[0], + ); + assert!( + str_ps[0] <= tfa.flow_delay_ps[0], + "converge_bridge: strengthened dataA {} ps must be ≤ TFA {} ps \ + (REQ-NC-PLP-003 restores plp ≤ TFA where pure PLP could not)", + str_ps[0], + tfa.flow_delay_ps[0], + ); + } +} diff --git a/crates/spar-network/tests/oracles/panco/panco_bench.py b/crates/spar-network/tests/oracles/panco/panco_bench.py index fb871c7..795f396 100644 --- a/crates/spar-network/tests/oracles/panco/panco_bench.py +++ b/crates/spar-network/tests/oracles/panco/panco_bench.py @@ -17,15 +17,19 @@ def bounds(net, label): sfa=SfaLP(net).all_delays # PURE polynomial PLP (no TFA strengthening): the only variant spar can # build byte-identically to this LP from its own model (REQ-NC-PLP-001). - # tfa=True drives PLP to EXACT but embeds panco's per-server TFA delays - # in the LP — that tightening is REQ-NC-PLP-003. plp=FifoLP(net,polynomial=True,tfa=False).all_delays + # TFA-STRENGTHENED PLP (tfa=True): embeds panco's per-server TFA delays in + # the LP, tightening toward EXACT. spar's plp_bound_tfa_strengthened + # (REQ-NC-PLP-003) reproduces this column using its OWN TFA delays, so the + # match is to the pinned values under EXACT <= plp <= TFA, not LP identity. + plp_str=FifoLP(net,polynomial=True,tfa=True).all_delays exact=FifoLP(net,polynomial=False).all_delays print(f"--- {label}") - print(f" TFA : {[us(x) for x in tfa]}") - print(f" SFA : {[us(x) for x in sfa]}") - print(f" PLP : {[us(x) for x in plp]}") - print(f" EXACT: {[us(x) for x in exact]}") + print(f" TFA : {[us(x) for x in tfa]}") + print(f" SFA : {[us(x) for x in sfa]}") + print(f" PLP pure : {[us(x) for x in plp]}") + print(f" PLP tfa=True: {[us(x) for x in plp_str]}") + print(f" EXACT : {[us(x) for x in exact]}") # 1) tandem_cross: tagged(0->1)+cross(0). spar TFA tagged=54.4, cross=34.0 bounds(Network([srv(GBPS,10e-6),srv(GBPS,5e-6)], @@ -44,3 +48,13 @@ def bounds(net, label): Flow([TokenBucket(1500*B,MBPS100)],[0,1]), Flow([TokenBucket(1500*B,MBPS100)],[1,2])]), "three_server_line (tagged 0->1->2 + 2 cross)") + +# 4) converging bridge (wctt.rs::bridge_converge_aadl): two talkers merge at a +# shared sink. sw_a fast 5us [0], sw_b slow 10000us [1], sw_c fast 5us sink [2]; +# dataA [0,2], dataB [1,2]. This is THE net that breaks pure PLP: dataA pure-PLP +# 1148.33 > TFA 1048.09 (both sound, incomparable). tfa=True drives it to EXACT +# 1035.2 <= TFA -> the REQ-NC-PLP-003 oracle. (1Gbps links, 1500B/100Mbps flows.) +bounds(Network([srv(GBPS,5e-6),srv(GBPS,10000e-6),srv(GBPS,5e-6)], + [Flow([TokenBucket(1500*B,MBPS100)],[0,2]), + Flow([TokenBucket(1500*B,MBPS100)],[1,2])]), + "converge_bridge (dataA[0,2] dataB[1,2], sink=2; PLP-003 oracle)")