diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index b2b2970..344d3ed 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -3452,41 +3452,53 @@ artifacts: type: requirement title: "Multi-buffer single-cycle CQF for long links (B-buffer dead-time accommodation)" description: > - ⚠ SPEC UNDER REVISION — DEFERRED to v0.23.0 (2026-06-27 fresh-context - model-pinning). The delay clause below is UNSOUND as written: it - conflates the within-cycle dead-time guard band DT (< T_c) with - multi-cycle link delay, so when the buffer clause B=ceil(DT/T_c) - activates (DT ≥ 3·T_c) the interval INVERTS (e.g. h=1, DT=3·T_c gives - D_min=3·T_c > D_max=2·T_c) and goes optimistic exactly in the - long-link regime. The SOUND model is per-hop CYCLE-QUANTIZATION: - kᵢ=ceil((dᵢ+DT)/T_c); D_max=T_c+Σkᵢ·T_c; D_min=Σ(kᵢ−1)·T_c+DT; - buffers key off JITTER Bᵢ=ceil((dᵢᵐᵃˣ−dᵢᵐⁱⁿ)/T_c)+2, B=clamp(maxᵢBᵢ, - 3,B_cap); csize=T_c·rate unchanged. Degeneracy (all dᵢ cap (never a silent down-clamp). In the synthesizer's supported + cycle-dominates regime jitter is ≤ 1 cycle, so it emits the 3-cycle + floor; the >3 arms are exercised by the standalone bound oracles. + Admission budget shrinks by the dead time: csize = (T_c − DT)·rate (only + the transmittable window; collapses to the shipped T_c·rate at DT=0). Degeneracy: every dᵢᵐᵃˣ < + DT (with DT > 0) ⇒ all kᵢ = 1 ⇒ D_max = (H+1)·T_c, D_min = (H−1)·T_c — + reproduces the shipped 24-hop/10µs → 250µs pin. IMPLEMENTATION + (crates/spar-network/src/cqf.rs): standalone bound functions + (cqf_hop_advance_cycles, cqf_delay_{max,min}_longlink_ps, + cqf_cycle_budget_bits_with_dead_time, cqf_buffer_count) + LinkDelay, + and synthesize_cqf_longlink returning CqfLongLinkSchedule. CqfFlow + gains per-hop link_delays (empty ⇒ all-short; delay+cycle degenerate to + the shipped hop-count result, though at DT>0 the csize budget is the + reduced (T_c−DT)·rate, so admission is not byte-identical to + synthesize_cqf). + SCOPE (sound baseline): synthesis serves the "cycle dominates links" + regime (T_c > every link, kᵢ ∈ {1,2}, monotonic → closed-form cycle + selection); a deadline that would need a cycle SHORTER than a link + returns LongLinkDeadlineTooTight rather than an unsound config — the + sub-link multi-cycle-per-hop regime is a documented follow-up. Wiring + the AADL bridge (cqf_synth.rs) to read per-hop Spar_Network::Latency is + a separate follow-up (the bound + synthesizer are library-complete). + Non-goal: not the heterogeneous-cycle ambition (REQ-TSN-SYNTH-CQF-001) + nor the PLP≪TFA NC-tightness wedge. + status: implemented release: v0.23.0 tags: [tsn, synthesis, cqf, longlink, detnet] diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index fdd756b..3c8bee2 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -2511,6 +2511,52 @@ artifacts: - type: satisfies target: REQ-TSN-SYNTH-CQF-BASE-001 + - id: TEST-TSN-SYNTH-CQF-LONGLINK + type: feature + title: Long-link CQF — cycle-quantized bound + dead-time synthesis, 4 non-circular oracles + description: > + Verifies the sound long-link CQF bound and synthesizer + (REQ-TSN-SYNTH-CQF-LONGLINK-001), where the shipped hop-count (H±1)·T_c + is OPTIMISTIC once a link's one-way latency is significant. The model + (draft-ietf-detnet-tcqf, cycle advance kᵢ = 2 + ⌊(dᵢ − DT)/T_c⌋) is + pinned NON-CIRCULARLY by three oracles in spar-network::cqf: (A) + DEGENERACY — every hop short (dᵢᵐᵃˣ < DT) makes the long-link + cqf_delay_{max,min}_longlink_ps EQUAL the independently-shipped, + literature-pinned hop-count cqf_delay_{max,min}_ps (24-hop → 250/230µs), + tying the new code to external ground truth without re-deriving it; (B) + DISCRIMINATION — a 3-hop [1,25,8]µs path gives D_max = 80µs while the + naive (H+1)·T_c = 40µs UNDER-bounds it 2×, proving the bound is a + strictly different, sounder computation; (C) OPTIMISM/INVERSION GUARD — + an H=2 both-15µs case gives 70µs > naive 30µs (the exact deadline-miss + the feature closes) plus a grid property asserting D_min ≤ D_max never + inverts. (D) INDEPENDENT DISCRETE-EVENT SIMULATION — (A)/(B)/(C) all + re-apply the kᵢ closed form, so a subtle optimistic error (sign, floor + direction, off-by-one) would pass them; oracle (D) plays frames through + an explicit CQF cycle timeline that derives cycle advance from + floor(arrival/T_c) — never calling the kᵢ formula — and asserts D_max + upper-bounds every observed delay across a full-cycle source-phase sweep + over profiles driving kᵢ ∈ {1..4}. This is the anti-optimism gate. + Also: csize = (T_c − DT)·rate shrinks by the dead time and + degenerates to T_c·rate at DT=0; buffer count from link jitter with a + hard cap (Err, never a silent down-clamp). The synthesizer + synthesize_cqf_longlink is covered for the cycle-dominates regime + (feasible schedule self-certifies against the exact bound), the + sub-link-cycle rejection (LongLinkDeadlineTooTight, not an unsound + config), all-short equivalence to synthesize_cqf, and the buffer-cap / + link-delay-length guards. Self-certifying: every synthesized schedule is + re-checked through the exact long-link bound before return. + fields: + method: automated-test + steps: + - run: "cargo test -p spar-network --lib -- cqf" + status: passing + tags: [v0.23.0, network, tsn, synthesis, cqf, longlink, oracle] + links: + - type: satisfies + target: REQ-TSN-SYNTH-CQF-LONGLINK-001 + - type: verifies + target: REQ-TSN-SYNTH-CQF-LONGLINK-001 + - id: TEST-TSN-SYNTH-CQF-BRIDGE type: feature title: AADL→CQF synthesis bridge — SystemInstance drives synthesize_cqf end-to-end diff --git a/crates/spar-analysis/src/cqf_synth.rs b/crates/spar-analysis/src/cqf_synth.rs index 81c232a..9730d0b 100644 --- a/crates/spar-analysis/src/cqf_synth.rs +++ b/crates/spar-analysis/src/cqf_synth.rs @@ -155,6 +155,11 @@ pub(crate) fn collect_cqf_inputs(instance: &SystemInstance) -> CqfInputs { reserved_bits_per_cycle, deadline_ps, path, + // Per-hop link latency is not yet read from the AADL bus + // properties, so every hop is treated as short (hop-count CQF). + // Populating this from Spar_Network::Latency is the follow-up that + // activates the long-link bound end-to-end. + link_delays: Vec::new(), }); out.labels.push((s.name.clone(), period_ps)); } diff --git a/crates/spar-network/src/cqf.rs b/crates/spar-network/src/cqf.rs index 320f5e3..eac46da 100644 --- a/crates/spar-network/src/cqf.rs +++ b/crates/spar-network/src/cqf.rs @@ -68,6 +68,12 @@ pub struct CqfFlow { pub deadline_ps: u64, /// Links the flow traverses, by link id. `len()` is the hop count `H`. pub path: Vec, + /// Per-hop one-way link latency, parallel to `path` (same length). EMPTY + /// means "every hop is short" — the flow is handled by the hop-count + /// [`synthesize_cqf`] exactly as before. Populated (length must equal + /// `path.len()`) it drives the long-link cycle-quantized bound in + /// [`synthesize_cqf_longlink`] (REQ-TSN-SYNTH-CQF-LONGLINK-001). + pub link_delays: Vec, } /// A synthesized standard-CQF configuration. @@ -113,6 +119,25 @@ pub enum CqfSynthError { /// The synthesized configuration failed its own re-check (a synthesis bug; /// should be unreachable). SelfCheck(&'static str), + /// Long-link only: dead time `DT` is not strictly below the cycle time + /// (`DT ≥ T_c`), so the per-hop cycle-advance formula is undefined. + DeadTimeTooLarge { dead_time_ps: u64, cycle_ps: u64 }, + /// Long-link only: a flow's `link_delays` length does not match its `path` + /// (hop count) length. + LinkDelayLenMismatch { + id: u32, + path_len: usize, + delays_len: usize, + }, + /// Long-link only: the worst hop needs more cyclic buffers than the + /// hardware cap (the draft's 7-cycle ceiling). Never silently clamped — + /// undersized buffers would drop frames. + BufferBudgetExceeded { needed: u32, cap: u32 }, + /// Long-link only: no cycle time in the "cycle dominates links" + /// (`T_c > max link delay`) regime meets this flow's deadline — the + /// deadline would require sub-link-delay cycles (the multi-cycle-per-hop + /// regime), which this sound baseline does not yet synthesize. + LongLinkDeadlineTooTight { id: u32 }, } impl fmt::Display for CqfSynthError { @@ -146,6 +171,30 @@ impl fmt::Display for CqfSynthError { but cycle budget is {csize_bits} bits" ), Self::SelfCheck(why) => write!(f, "CQF self-check failed: {why}"), + Self::DeadTimeTooLarge { + dead_time_ps, + cycle_ps, + } => write!( + f, + "dead time {dead_time_ps} ps must be strictly below cycle {cycle_ps} ps" + ), + Self::LinkDelayLenMismatch { + id, + path_len, + delays_len, + } => write!( + f, + "flow {id}: {delays_len} link delays for a {path_len}-hop path" + ), + Self::BufferBudgetExceeded { needed, cap } => write!( + f, + "long-link CQF needs {needed} cyclic buffers but the cap is {cap}" + ), + Self::LongLinkDeadlineTooTight { id } => write!( + f, + "flow {id}: deadline unmeetable with a cycle longer than every link \ + (sub-link-delay cycles are not yet synthesized)" + ), } } } @@ -179,6 +228,153 @@ pub fn cqf_cycle_budget_bits(cycle_ps: u64, link_rate_bps: u64) -> u128 { u128::from(link_rate_bps) * u128::from(cycle_ps) / 1_000_000_000_000u128 } +// ── Long-link CQF (REQ-TSN-SYNTH-CQF-LONGLINK-001) ──────────────────────── +// +// The bounds above are hop-count-only: they assume every link's one-way +// latency is negligible relative to the cycle (a frame sent in cycle c is +// received in time to be forwarded in cycle c+1). On a LONG link that no +// longer holds — the frame can miss the next cycle boundary and be delayed by +// extra whole cycles. The sound generalization (draft-ietf-detnet-tcqf, +// draft-eckert-detnet-tcqf-05; D_max soundness validated by an independent +// discrete-event cycle-timeline simulation, see the `longlink_dmax_upper_ +// bounds_discrete_event_sim` oracle) quantizes each hop's link latency into an +// integer CYCLE ADVANCE kᵢ and sums them. +// +// Dead time `DT` (0 ≤ DT < T_c) is the tcqf guard interval at the END of each +// cycle: no scheduled frame is sent in the last DT of a cycle so it is sure to +// arrive before the receiver's next boundary. Because DT sits at the cycle +// end, it makes same-cycle delivery EASIER — it enters kᵢ with a MINUS sign. + +/// One link's one-way latency window (picoseconds): propagation + PHY / +/// processing + sync-error margin. Frame serialization is charged on the send +/// side (the `csize` budget), not here. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct LinkDelay { + /// Minimum one-way latency (best case), picoseconds. + pub min_ps: u64, + /// Maximum one-way latency (worst case), picoseconds. + pub max_ps: u64, +} + +/// Per-hop CQF cycle advance `kᵢ = 2 + ⌊(dᵢ − DT) / T_c⌋`, the number of whole +/// cycles a frame advances crossing a hop of one-way latency `link_delay_ps`, +/// with dead time `dead_time_ps` (`0 ≤ DT < T_c`) and cycle `cycle_ps`. +/// +/// Uses floored (Euclidean) division so a `dᵢ < DT` short link yields exactly +/// `kᵢ = 1` (the classic single-cycle CQF hop) and a boundary `dᵢ = DT` is +/// charged pessimistically to `kᵢ = 2`. `kᵢ ≥ 1` is guaranteed by `DT < T_c`. +#[must_use] +pub fn cqf_hop_advance_cycles(link_delay_ps: u64, dead_time_ps: u64, cycle_ps: u64) -> u64 { + debug_assert!(dead_time_ps < cycle_ps, "dead time must be < cycle"); + let numerator = i128::from(link_delay_ps) - i128::from(dead_time_ps); + // div_euclid = floor for a positive divisor; numerator may be negative. + (2 + numerator.div_euclid(i128::from(cycle_ps))) as u64 +} + +/// Worst-case long-link end-to-end delay `D_max = T_c + T_c·Σᵢ kᵢ(dᵢᵐᵃˣ)`, +/// picoseconds. `link_delays_max_ps` is the per-hop MAX latency in path order +/// (its length is the hop count `H`). The leading `T_c` is the worst-case +/// source-ingress alignment wait. +/// +/// Degenerates to the shipped `(H+1)·T_c` when every hop is short +/// (`dᵢᵐᵃˣ < DT` ⇒ `kᵢ = 1`). +#[must_use] +pub fn cqf_delay_max_longlink_ps( + link_delays_max_ps: &[u64], + dead_time_ps: u64, + cycle_ps: u64, +) -> u128 { + let sum_k: u128 = link_delays_max_ps + .iter() + .map(|&d| u128::from(cqf_hop_advance_cycles(d, dead_time_ps, cycle_ps))) + .sum(); + u128::from(cycle_ps) + u128::from(cycle_ps) * sum_k +} + +/// Best-case long-link end-to-end delay +/// `D_min = ℓ_H,min + T_c·Σ_{i u128 { + let h = link_delays_min_ps.len(); + if h == 0 { + return 0; + } + let sum_k: u128 = link_delays_min_ps[..h - 1] + .iter() + .map(|&d| u128::from(cqf_hop_advance_cycles(d, dead_time_ps, cycle_ps))) + .sum(); + u128::from(cycle_ps) * sum_k // ℓ_H,min = 0 +} + +/// Cycle admission budget with dead time: `csize = (T_c − DT)·rate`, bits. +/// +/// Only the `T_c − DT` transmittable window of each cycle may be filled — a +/// frame admitted into the dead-time tail could fail to drain before the cycle +/// boundary and spill into a later cycle, breaking `D_max`. Collapses to the +/// shipped [`cqf_cycle_budget_bits`] (`T_c·rate`) when `DT = 0`. +#[must_use] +pub fn cqf_cycle_budget_bits_with_dead_time( + cycle_ps: u64, + dead_time_ps: u64, + link_rate_bps: u64, +) -> u128 { + let window_ps = cycle_ps.saturating_sub(dead_time_ps); + u128::from(link_rate_bps) * u128::from(window_ps) / 1_000_000_000_000u128 +} + +/// Per-path cyclic buffer count `B = max(3, maxᵢ((kᵢᵐᵃˣ − kᵢᵐⁱⁿ) + 2))` — +/// the tcqf 3-cycle floor plus one extra cycle per cycle of link-latency +/// jitter. `Ok(B)` when `B ≤ cap`; `Err(B)` when the needed count exceeds the +/// hardware cap (never silently clamped DOWN — undersized buffers drop frames). +/// +/// The draft mandates support for 3 and 4 cycles and a 7-cycle ceiling, so +/// `cap` is normally 7. +pub fn cqf_buffer_count( + link_delays: &[LinkDelay], + dead_time_ps: u64, + cycle_ps: u64, + cap: u32, +) -> Result { + let mut needed = 3u32; + for ld in link_delays { + let k_max = cqf_hop_advance_cycles(ld.max_ps, dead_time_ps, cycle_ps); + let k_min = cqf_hop_advance_cycles(ld.min_ps, dead_time_ps, cycle_ps); + // Advance is monotone in latency, so k_max ≥ k_min for a well-formed + // LinkDelay; saturating_sub keeps a caller-swapped (min > max) struct + // from wrapping into a bogus huge buffer count. +2 for double buffering. + let b_i = (k_max.saturating_sub(k_min)) as u32 + 2; + needed = needed.max(b_i); + } + if needed > cap { + Err(needed) + } else { + Ok(needed) + } +} + /// Synthesize a standard two-buffer CQF configuration for `flows` on links of /// uniform `link_rate_bps`. /// @@ -288,6 +484,170 @@ fn self_check(schedule: &CqfSchedule, flows: &[CqfFlow]) -> Result<(), CqfSynthE Ok(()) } +/// The draft's cyclic-buffer ceiling: "7 or fewer cycles MUST be used". +pub const CQF_DEFAULT_BUFFER_CAP: u32 = 7; + +/// A synthesized long-link CQF configuration (REQ-TSN-SYNTH-CQF-LONGLINK-001). +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct CqfLongLinkSchedule { + /// Chosen global cycle time `T_c`, picoseconds (whole ns, `> DT` and + /// `>` every link delay). + pub cycle_time_ps: u64, + /// Dead time `DT` (`0 ≤ DT < T_c`), picoseconds. + pub dead_time_ps: u64, + /// Cycle budget `csize = (T_c − DT)·rate`, bits. + pub csize_bits: u128, + /// Per-link aggregate reservation, bits/cycle (`≤ csize_bits`). + pub per_link_bits: BTreeMap, + /// Cyclic buffers required (`3..=cap`) — from the worst hop's latency + /// jitter. + pub buffers: u32, +} + +/// Synthesize a long-link-sound CQF configuration, accounting for each hop's +/// one-way link latency via the cycle-quantized bound +/// ([`cqf_delay_max_longlink_ps`]) and the dead-time budget +/// ([`cqf_cycle_budget_bits_with_dead_time`]). +/// +/// Baseline scope — the **"cycle dominates links"** regime: it selects the +/// largest whole-nanosecond `T_c` that is longer than every link delay (so each +/// hop advances one cycle if `dᵢ < DT`, else two) and meets every flow's +/// deadline `D_max ≤ deadline`, then admits flows against +/// `csize = (T_c − DT)·rate` and sizes the cyclic buffers. When a deadline can +/// only be met with a cycle *shorter* than some link (the multi-cycle-per-hop +/// regime), it returns [`CqfSynthError::LongLinkDeadlineTooTight`] rather than +/// an unsound configuration; optimal sub-link-cycle selection is a follow-up. +/// +/// A flow with empty `link_delays` is treated as all-short (every `dᵢ = 0`); +/// with `DT > 0` that reproduces the hop-count [`synthesize_cqf`] result. The +/// returned schedule self-certifies against the exact long-link bound before +/// return. +pub fn synthesize_cqf_longlink( + flows: &[CqfFlow], + link_rate_bps: u64, + dead_time_ps: u64, + buffer_cap: u32, +) -> Result { + if flows.is_empty() { + return Err(CqfSynthError::NoFlows); + } + if link_rate_bps == 0 { + return Err(CqfSynthError::ZeroLinkRate); + } + + let mut seen_ids = BTreeMap::new(); + for flow in flows { + if seen_ids.insert(flow.id, ()).is_some() { + return Err(CqfSynthError::DuplicateFlowId { id: flow.id }); + } + if flow.path.is_empty() { + return Err(CqfSynthError::EmptyPath { id: flow.id }); + } + if flow.reserved_bits_per_cycle == 0 || flow.deadline_ps == 0 { + return Err(CqfSynthError::DegenerateFlow { id: flow.id }); + } + if !flow.link_delays.is_empty() && flow.link_delays.len() != flow.path.len() { + return Err(CqfSynthError::LinkDelayLenMismatch { + id: flow.id, + path_len: flow.path.len(), + delays_len: flow.link_delays.len(), + }); + } + } + + // Max one-way latency of hop `i` (0 when a flow omits its delays). + let hop_max = + |flow: &CqfFlow, i: usize| -> u64 { flow.link_delays.get(i).map_or(0, |ld| ld.max_ps) }; + + // Cycle-dominates regime: with T_c > every dᵢ, kᵢ = 1 if dᵢ < DT else 2. + // The per-flow cycle limit is deadline / (1 + Σkᵢ); the global T_c is the + // tightest, floored to a whole ns. Track the largest link delay so we can + // enforce the regime assumption afterward. + let mut cycle_ps = u64::MAX; + let mut tightest_id = flows[0].id; + let mut max_link_delay_ps = 0u64; + for flow in flows { + let mut sum_k = 0u64; + for i in 0..flow.path.len() { + let d = hop_max(flow, i); + max_link_delay_ps = max_link_delay_ps.max(d); + sum_k += if d < dead_time_ps { 1 } else { 2 }; + } + let limit_ps = flow.deadline_ps / (1 + sum_k); + if limit_ps < cycle_ps { + cycle_ps = limit_ps; + tightest_id = flow.id; + } + } + cycle_ps = (cycle_ps / 1_000) * 1_000; // whole nanoseconds + + // Regime validity: the cycle must be longer than every link (so kᵢ ≤ 2). + if cycle_ps == 0 || cycle_ps <= max_link_delay_ps { + return Err(CqfSynthError::LongLinkDeadlineTooTight { id: tightest_id }); + } + if dead_time_ps >= cycle_ps { + return Err(CqfSynthError::DeadTimeTooLarge { + dead_time_ps, + cycle_ps, + }); + } + + // Admission against the dead-time-reduced budget. + let csize_bits = cqf_cycle_budget_bits_with_dead_time(cycle_ps, dead_time_ps, link_rate_bps); + let mut per_link_bits: BTreeMap = BTreeMap::new(); + for flow in flows { + for &link in &flow.path { + *per_link_bits.entry(link).or_insert(0) += u128::from(flow.reserved_bits_per_cycle); + } + } + for (&link, &required) in &per_link_bits { + if required > csize_bits { + return Err(CqfSynthError::Oversubscribed { + link, + required_bits: required, + csize_bits, + }); + } + } + + // Buffer sizing over every hop of every flow (empty delays ⇒ zero jitter). + let mut hops: Vec = Vec::new(); + for flow in flows { + for i in 0..flow.path.len() { + hops.push(flow.link_delays.get(i).copied().unwrap_or(LinkDelay { + min_ps: 0, + max_ps: 0, + })); + } + } + let buffers = + cqf_buffer_count(&hops, dead_time_ps, cycle_ps, buffer_cap).map_err(|needed| { + CqfSynthError::BufferBudgetExceeded { + needed, + cap: buffer_cap, + } + })?; + + // Self-certify against the EXACT long-link bound (regression guard). + for flow in flows { + let d_max: Vec = (0..flow.path.len()).map(|i| hop_max(flow, i)).collect(); + if cqf_delay_max_longlink_ps(&d_max, dead_time_ps, cycle_ps) > u128::from(flow.deadline_ps) + { + return Err(CqfSynthError::SelfCheck( + "long-link flow delay exceeds deadline", + )); + } + } + + Ok(CqfLongLinkSchedule { + cycle_time_ps: cycle_ps, + dead_time_ps, + csize_bits, + per_link_bits, + buffers, + }) +} + #[cfg(test)] mod tests { use super::*; @@ -301,6 +661,7 @@ mod tests { reserved_bits_per_cycle: bits, deadline_ps, path: path.to_vec(), + link_delays: Vec::new(), } } @@ -480,4 +841,592 @@ mod tests { Err(CqfSynthError::DuplicateFlowId { id: 1 }) ); } + + /// Admission is inclusive at the budget: a reservation EXACTLY equal to + /// csize is admitted (`required > csize`, strict). This also exercises the + /// `self_check` admission arm on the returned schedule at the boundary — + /// killing the `>` ⇒ `>=` / `==` mutants in both the admission loop and the + /// self-check (surfaced by full-file mutation of the co-located v0.20 CQF + /// baseline, hardened here since the file is under change). + #[test] + fn synth_admission_boundary_reserves_exactly_csize() { + // 1 Gbps, 1 hop, deadline 200 µs ⇒ T = 100 µs ⇒ csize = 100_000 bits. + let rate = 1_000_000_000u64; + let exact = [flow(1, 100_000, 200_000_000, &[0])]; + let sched = synthesize_cqf(&exact, rate).expect("reservation == csize is admissible"); + assert_eq!(sched.csize_bits, 100_000); + assert_eq!(sched.per_link_bits[&0], 100_000); + // One bit over the budget is rejected (the strict side of the boundary). + let over = [flow(1, 100_001, 200_000_000, &[0])]; + assert_eq!( + synthesize_cqf(&over, rate), + Err(CqfSynthError::Oversubscribed { + link: 0, + required_bits: 100_001, + csize_bits: 100_000, + }) + ); + } + + /// Every `CqfSynthError` variant renders a non-empty, distinguishing + /// `Display` string (kills the `fmt -> Ok(default)` mutant that would make + /// every error print as the empty string). + #[test] + fn cqf_synth_error_display_is_populated() { + let cases: &[(CqfSynthError, &str)] = &[ + (CqfSynthError::NoFlows, "no CQF flows"), + (CqfSynthError::EmptyPath { id: 3 }, "flow 3"), + (CqfSynthError::DegenerateFlow { id: 4 }, "zero"), + ( + CqfSynthError::DuplicateFlowId { id: 5 }, + "duplicate flow id 5", + ), + (CqfSynthError::ZeroLinkRate, "non-zero"), + ( + CqfSynthError::DeadlineTooTight { + id: 6, + hops: 3, + deadline_ps: 9, + }, + "irreducible", + ), + ( + CqfSynthError::Oversubscribed { + link: 7, + required_bits: 10, + csize_bits: 5, + }, + "oversubscribed", + ), + (CqfSynthError::SelfCheck("boom"), "boom"), + ( + CqfSynthError::DeadTimeTooLarge { + dead_time_ps: 9, + cycle_ps: 8, + }, + "dead time", + ), + ( + CqfSynthError::LinkDelayLenMismatch { + id: 8, + path_len: 2, + delays_len: 1, + }, + "link delays", + ), + ( + CqfSynthError::BufferBudgetExceeded { needed: 9, cap: 7 }, + "cyclic buffers", + ), + ( + CqfSynthError::LongLinkDeadlineTooTight { id: 9 }, + "every link", + ), + ]; + for (err, needle) in cases { + let shown = err.to_string(); + assert!(!shown.is_empty(), "{err:?} rendered empty"); + assert!( + shown.contains(needle), + "{err:?} Display {shown:?} missing {needle:?}" + ); + } + } + + // NOTE — accepted mutation survivors in the v0.20 hop-count baseline + // (`synthesize_cqf` / `self_check`), surfaced by full-file mutation: + // • line 417 (×4): the `deadline/(hops+1)` key inside `min_by_key` only + // selects WHICH flow id is NAMED in a DeadlineTooTight message when + // several flows are simultaneously infeasible — a diagnostic nicety, + // not a soundness property; the `/(H+1)` vs `/H` variant is argmin- + // equivalent for realistic inputs and the others need contrived + // picosecond-scale multi-flow inputs to distinguish. + // • `self_check` replaced whole-body with `Ok(())`: `self_check` is a + // defensive regression guard that, by construction, never returns Err + // on a reachable (already deadline- and admission-filtered) schedule, + // so the whole-body replacement is an equivalent mutant. + // These belong to REQ-TSN-SYNTH-CQF-BASE-001 (shipped v0.20.0); the + // long-link functions under REQ-TSN-SYNTH-CQF-LONGLINK-001 are 0-missed. + + // ── Long-link CQF oracles (REQ-TSN-SYNTH-CQF-LONGLINK-001) ──────────── + // + // Three NON-CIRCULAR oracles for the cycle-quantized bound. Constants: + // T_c = 10 us, DT = 2 us. Hand-computed k_i = 2 + floor((d_i - DT)/T_c). + + const DT_2US_PS: u64 = 2_000_000; + + #[test] + fn longlink_degeneracy_reproduces_shipped_hop_count_bound() { + // (A) DEGENERACY: every hop short (d_i^max < DT) ⇒ k_i = 1 ⇒ the + // long-link bound must EQUAL the independently-shipped hop-count bound + // cqf_delay_max_ps / cqf_delay_min_ps — which is externally pinned to + // the draft's 24-hop/250us example. Ties the new code to ground truth + // WITHOUT re-deriving the new formula. + let hops = 24usize; + let d_max = vec![1_000_000u64; hops]; // 1 us < DT ⇒ k=1 + let d_min = vec![1_000_000u64; hops]; + let dmax = cqf_delay_max_longlink_ps(&d_max, DT_2US_PS, TEN_US_PS); + let dmin = cqf_delay_min_longlink_ps(&d_min, DT_2US_PS, TEN_US_PS); + assert_eq!( + dmax, + cqf_delay_max_ps(hops as u32, TEN_US_PS), + "D_max ≠ (H+1)·T_c" + ); + assert_eq!( + dmin, + cqf_delay_min_ps(hops as u32, TEN_US_PS), + "D_min ≠ (H−1)·T_c" + ); + // Absolute pin: 250 us / 230 us. + assert_eq!(dmax, 250_000_000); + assert_eq!(dmin, 230_000_000); + // Every hop advances exactly one cycle. + assert_eq!(cqf_hop_advance_cycles(1_000_000, DT_2US_PS, TEN_US_PS), 1); + } + + #[test] + fn longlink_discrimination_beats_naive_hop_count() { + // (B) DISCRIMINATION: 3-hop path d = [1, 25, 8] us ⇒ k = [1, 4, 2]. + // D_max = T_c + T_c·(1+4+2) = 10 + 70 = 80 us. The naive hop-count + // bound (H+1)·T_c = 40 us UNDER-bounds the true worst case by 2× — + // proving the long-link bound is a strictly different, sounder + // computation, not a rename of the old one. + let d = [1_000_000u64, 25_000_000, 8_000_000]; + assert_eq!(cqf_hop_advance_cycles(d[0], DT_2US_PS, TEN_US_PS), 1); + assert_eq!(cqf_hop_advance_cycles(d[1], DT_2US_PS, TEN_US_PS), 4); + assert_eq!(cqf_hop_advance_cycles(d[2], DT_2US_PS, TEN_US_PS), 2); + let dmax = cqf_delay_max_longlink_ps(&d, DT_2US_PS, TEN_US_PS); + assert_eq!(dmax, 80_000_000, "D_max must be 80 us"); + let naive = cqf_delay_max_ps(d.len() as u32, TEN_US_PS); // 40 us + assert!( + naive < dmax, + "naive (H+1)T_c {naive} must UNDER-bound long-link {dmax}" + ); + // D_min sums the H−1 intermediate hops: (1+4)·10 = 50 us. + let dmin = cqf_delay_min_longlink_ps(&d, DT_2US_PS, TEN_US_PS); + assert_eq!(dmin, 50_000_000); + } + + #[test] + fn longlink_never_inverts_and_flags_naive_optimism() { + // (C) OPTIMISM/INVERSION GUARD. Edge case H=2, both links d=15 us + // (> T_c) ⇒ k = [3, 3] ⇒ D_max = 10 + 60 = 70 us, while the naive + // (H+1)·T_c = 30 us. A 40 us-deadline flow PASSES the naive test but + // its true worst case is 70 us — the exact unsoundness this feature + // closes. Also: D_min ≤ D_max must hold for ALL inputs (the prior + // spec inverted; this construction cannot). + let d = [15_000_000u64, 15_000_000]; + assert_eq!(cqf_hop_advance_cycles(15_000_000, DT_2US_PS, TEN_US_PS), 3); + let dmax = cqf_delay_max_longlink_ps(&d, DT_2US_PS, TEN_US_PS); + assert_eq!(dmax, 70_000_000); + assert!( + cqf_delay_max_ps(2, TEN_US_PS) < dmax, + "naive 30us must under-bound 70us" + ); + // Never-inverts property across a grid of hop counts, delays, DT. + for dt in [0u64, 1_000_000, 5_000_000, 9_000_000] { + for &per_hop in &[0u64, 500_000, 2_000_000, 12_000_000, 33_000_000] { + for h in 1..=6usize { + let dv = vec![per_hop; h]; + let mx = cqf_delay_max_longlink_ps(&dv, dt, TEN_US_PS); + let mn = cqf_delay_min_longlink_ps(&dv, dt, TEN_US_PS); + assert!( + mn <= mx, + "inverted: D_min {mn} > D_max {mx} (h={h}, d={per_hop}, dt={dt})" + ); + } + } + } + } + + #[test] + fn longlink_csize_shrinks_by_dead_time_and_degenerates() { + // csize = (T_c − DT)·rate. At DT=0 it equals the shipped T_c·rate; + // with DT>0 it is strictly smaller (the dead-time tail is unusable). + let rate = 1_000_000_000u64; // 1 Gbps + let full = cqf_cycle_budget_bits(TEN_US_PS, rate); + assert_eq!( + cqf_cycle_budget_bits_with_dead_time(TEN_US_PS, 0, rate), + full + ); + let with_dt = cqf_cycle_budget_bits_with_dead_time(TEN_US_PS, DT_2US_PS, rate); + // (10us−2us)·1Gbps = 8us·1e9 = 8000 bits. + assert_eq!(with_dt, 8_000); + assert!(with_dt < full); + } + + #[test] + fn longlink_buffer_count_from_jitter_and_cap() { + // B = max(3, max_i((k_i^max − k_i^min)+2)); Err(needed) past the cap. + // Hop with min=1us (k=1), max=25us (k=4): jitter 3 cycles ⇒ B_i=5. + let jittery = [LinkDelay { + min_ps: 1_000_000, + max_ps: 25_000_000, + }]; + assert_eq!(cqf_buffer_count(&jittery, DT_2US_PS, TEN_US_PS, 7), Ok(5)); + // All-short deterministic links ⇒ floor of 3. + let short = [LinkDelay { + min_ps: 0, + max_ps: 500_000, + }; 4]; + assert_eq!(cqf_buffer_count(&short, DT_2US_PS, TEN_US_PS, 7), Ok(3)); + // Exceeds the 7-cycle cap ⇒ Err(needed), never a silent down-clamp. + // max=90us ⇒ k_max=2+⌊(90−2)/10⌋=10; min=0 ⇒ k_min=1; B=(10−1)+2=11. + let huge = [LinkDelay { + min_ps: 0, + max_ps: 90_000_000, + }]; + assert_eq!(cqf_buffer_count(&huge, DT_2US_PS, TEN_US_PS, 7), Err(11)); + } + + fn ll_flow( + id: u32, + bits: u64, + deadline_ps: u64, + path: &[u32], + delays: &[(u64, u64)], + ) -> CqfFlow { + CqfFlow { + id, + reserved_bits_per_cycle: bits, + deadline_ps, + path: path.to_vec(), + link_delays: delays + .iter() + .map(|&(min_ps, max_ps)| LinkDelay { min_ps, max_ps }) + .collect(), + } + } + + #[test] + fn longlink_synth_feasible_in_cycle_dominates_regime() { + // 2-hop path, both links 5 us (> DT=2us ⇒ k=2 each), deadline 150 us. + // Σk=4 ⇒ T_c limit = 150/(1+4) = 30 us > max link 5 us ✓. D_max = + // 30·(1+4) = 150 us ≤ deadline. csize = (30−2)us·1Gbps = 28_000 bits. + let rate = 1_000_000_000u64; + let flows = [ll_flow( + 1, + 1_000, + 150_000_000, + &[0, 1], + &[(5_000_000, 5_000_000); 2], + )]; + let sched = synthesize_cqf_longlink(&flows, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP) + .expect("feasible in cycle-dominates regime"); + assert_eq!(sched.cycle_time_ps, 30_000_000); + assert_eq!(sched.dead_time_ps, DT_2US_PS); + assert_eq!(sched.csize_bits, 28_000); + assert_eq!(sched.buffers, 3, "deterministic links ⇒ 3-buffer floor"); + // The true long-link D_max at the chosen cycle meets the deadline. + let dmax = + cqf_delay_max_longlink_ps(&[5_000_000, 5_000_000], DT_2US_PS, sched.cycle_time_ps); + assert!(dmax <= 150_000_000); + } + + #[test] + fn longlink_synth_rejects_deadline_needing_sublink_cycle() { + // A 30 us link with a 60 us deadline: Σk=2 ⇒ T_c limit = 60/3 = 20 us, + // which is SHORTER than the 30 us link — the cycle-dominates regime + // cannot serve it, so we get a structured error, never an unsound + // config that silently assumes a single-cycle hop. + let rate = 1_000_000_000u64; + let flows = [ll_flow( + 7, + 1_000, + 60_000_000, + &[0], + &[(30_000_000, 30_000_000)], + )]; + assert_eq!( + synthesize_cqf_longlink(&flows, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP), + Err(CqfSynthError::LongLinkDeadlineTooTight { id: 7 }) + ); + } + + #[test] + fn longlink_synth_all_short_matches_hop_count_synthesis() { + // Every hop short (dᵢ=1us < DT) ⇒ the long-link synthesizer picks the + // SAME cycle as the hop-count synthesize_cqf and its D_max is (H+1)·T_c. + let rate = 1_000_000_000u64; + let short = &[(1_000_000u64, 1_000_000u64); 3]; + let ll = [ll_flow(1, 1_000, 80_000_000, &[0, 1, 2], short)]; + let hop = [flow(1, 1_000, 80_000_000, &[0, 1, 2])]; + let a = synthesize_cqf_longlink(&ll, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP) + .expect("feasible"); + let b = synthesize_cqf(&hop, rate).expect("feasible"); + assert_eq!( + a.cycle_time_ps, b.cycle_time_ps, + "same cycle as hop-count synth" + ); + // D_max degenerates to (H+1)·T_c. + assert_eq!( + cqf_delay_max_longlink_ps(&[1_000_000; 3], DT_2US_PS, a.cycle_time_ps), + cqf_delay_max_ps(3, a.cycle_time_ps) + ); + } + + #[test] + fn longlink_synth_flags_buffer_budget_and_len_mismatch() { + let rate = 1_000_000_000u64; + // In the cycle-dominates regime buffers are always the 3-cycle floor + // (T_c > every link ⇒ jitter ≤ 1 cycle), so the only way to trip the + // budget is a cap BELOW the draft's mandated 3 — a misconfiguration + // the synthesizer must reject, not silently under-buffer. + let f = [ll_flow( + 1, + 1_000, + 100_000_000, + &[0], + &[(1_000_000, 1_000_000)], + )]; + assert_eq!( + synthesize_cqf_longlink(&f, rate, DT_2US_PS, 2), + Err(CqfSynthError::BufferBudgetExceeded { needed: 3, cap: 2 }) + ); + // link_delays length must match the path. + let bad = [ll_flow( + 2, + 1_000, + 100_000_000, + &[0, 1], + &[(1_000_000, 1_000_000)], + )]; + assert_eq!( + synthesize_cqf_longlink(&bad, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP), + Err(CqfSynthError::LinkDelayLenMismatch { + id: 2, + path_len: 2, + delays_len: 1 + }) + ); + } + + /// Play one frame through an EXPLICIT CQF cycle timeline and return its + /// end-to-end delay in picoseconds. This is the independent ground truth + /// for the cycle-quantized bound: it derives every per-hop cycle advance + /// from `floor(arrival / T_c)` on real timestamps — it NEVER calls + /// [`cqf_hop_advance_cycles`] — so an off-by-one / floor-direction / + /// dead-time-sign error in the closed form shows up as a mismatch here. + /// + /// Model: cycles tile the timeline `[c·T_c, (c+1)·T_c)`; the transmittable + /// window is `[c·T_c, (c+1)·T_c − DT)` (dead time `DT` at the cycle END). A + /// frame that ARRIVES during cycle `a` is buffered and FORWARDED during + /// cycle `a+1`. `latest` sends at the very end of that window (worst case); + /// `!latest` sends at the window start (best case). `ready` is the source + /// presentation instant; the frame is treated as arrived in cycle + /// `⌊ready/T_c⌋`. + fn sim_longlink_delay_ps( + delays_ps: &[u64], + dt_ps: u64, + tc_ps: u64, + ready_ps: u64, + latest: bool, + ) -> u128 { + let tc = u128::from(tc_ps); + let dt = u128::from(dt_ps); + let mut arrived_cycle = u128::from(ready_ps) / tc; + let mut arrival = u128::from(ready_ps); + for &d in delays_ps { + let fwd = arrived_cycle + 1; // forwarded in the cycle after arrival + let send = if latest { + (fwd + 1) * tc - dt // last transmittable instant of the window + } else { + fwd * tc // first instant of the window + }; + arrival = send + u128::from(d); + arrived_cycle = arrival / tc; + } + arrival - u128::from(ready_ps) + } + + #[test] + fn longlink_dmax_upper_bounds_discrete_event_sim() { + // (D) INDEPENDENT ANTI-OPTIMISM ORACLE — the advisor's blocking gate. + // Oracles (A)/(B)/(C) all re-apply the k_i closed form (by hand or by + // degeneracy to the shipped hop-count bound), so a subtle optimistic + // error in k_i = 2 + ⌊(d−DT)/T_c⌋ (wrong sign, floor direction, + // off-by-one) would pass every one of them AND survive mutation. This + // oracle plays frames through a discrete-event cycle timeline that + // derives cycle advance from floor(arrival/T_c) — fully independent of + // the closed form — and asserts the analytical D_max upper-bounds EVERY + // observed delay across a full-cycle sweep of source phases. Profiles + // are chosen to drive k_i ≥ 2 (the regime (A) never exercises). + let tc = TEN_US_PS; + let dt = DT_2US_PS; + let profiles: &[&[u64]] = &[ + &[1_000_000, 25_000_000, 8_000_000], // k = [1, 4, 2] + &[15_000_000, 15_000_000], // k = [3, 3] + &[12_000_000, 3_000_000, 30_000_000], // k = [3, 2, 4] + &[1_000_000, 1_000_000, 1_000_000, 1_000_000], // k = 1 (degenerate) + ]; + let mut saw_multi_cycle = false; + for prof in profiles { + let dmax = cqf_delay_max_longlink_ps(prof, dt, tc); + let dmin = cqf_delay_min_longlink_ps(prof, dt, tc); + saw_multi_cycle |= prof.iter().any(|&d| cqf_hop_advance_cycles(d, dt, tc) >= 2); + // Sweep the source presentation phase across a full cycle. + for step in 0..(tc / 1_000_000) { + let ready = step * 1_000_000; + let observed = sim_longlink_delay_ps(prof, dt, tc, ready, true); + assert!( + dmax >= observed, + "OPTIMISTIC D_max: {dmax} < observed {observed} \ + (prof={prof:?}, ready={ready})" + ); + } + // Nominal best case: a boundary-aligned frame (ready = 0). D_min + // drops the last hop's cycle-quantization (ℓ_H,min = 0), so it is + // the ALIGNED reference, not an absolute floor over all sub-cycle + // source phases — a frame arriving just before a boundary can be + // delivered up to ~T_c sooner relative to its own `ready`. That + // asymmetry is safe: buffer sizing uses per-hop k (k_max−k_min), + // never D_min. So we only require D_min ≤ the aligned sim here. + let aligned_min = sim_longlink_delay_ps(prof, dt, tc, 0, false); + assert!( + dmin <= aligned_min, + "D_min {dmin} > aligned best-case sim {aligned_min} (prof={prof:?})" + ); + } + assert!( + saw_multi_cycle, + "sim oracle must exercise the k_i ≥ 2 multi-cycle regime" + ); + } + + #[test] + fn longlink_synth_boundary_delay_equals_dead_time() { + // A hop whose latency is EXACTLY the dead time (d == DT) must be charged + // k = 2 (Euclidean div: 2 + ⌊0/T_c⌋ = 2), NOT k = 1. If the regime's + // inline shortcut used `d <= DT ⇒ k = 1` it would pick a cycle that the + // exact self-cert then rejects. Real path: Σk = 2 ⇒ T_c = 60/3 = 20 µs, + // D_max = 20·3 = 60 µs == deadline ⇒ Ok. A `d <= DT` shortcut picks + // 30 µs, whose real D_max = 90 µs > 60 ⇒ SelfCheck error. + let rate = 1_000_000_000u64; + let f = [ll_flow( + 1, + 1_000, + 60_000_000, + &[0], + &[(DT_2US_PS, DT_2US_PS)], + )]; + let sched = synthesize_cqf_longlink(&f, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP) + .expect("d == DT is feasible at k = 2"); + assert_eq!( + sched.cycle_time_ps, 20_000_000, + "d == DT must be charged k=2" + ); + } + + #[test] + fn longlink_synth_tie_reports_first_binding_flow() { + // Two flows with an IDENTICAL cycle limit, both needing a sub-link + // cycle (infeasible). The tightest-flow tracker keeps the FIRST binding + // flow on a tie (`limit < cycle`, strict) — a `<=` would drift the id to + // the later flow. Both: deadline 60 µs, one 30 µs hop ⇒ Σk=2 ⇒ limit + // 20 µs ≤ 30 µs link ⇒ LongLinkDeadlineTooTight, and the id must be 7. + let rate = 1_000_000_000u64; + let flows = [ + ll_flow(7, 1_000, 60_000_000, &[0], &[(30_000_000, 30_000_000)]), + ll_flow(9, 1_000, 60_000_000, &[1], &[(30_000_000, 30_000_000)]), + ]; + assert_eq!( + synthesize_cqf_longlink(&flows, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP), + Err(CqfSynthError::LongLinkDeadlineTooTight { id: 7 }) + ); + } + + #[test] + fn longlink_synth_admission_oversubscribe_and_boundary() { + // Admission against csize = (T_c − DT)·rate. 1 short hop, deadline + // 40 µs ⇒ T_c = 20 µs ⇒ csize = (20−2)µs·1Gbps = 18_000 bits. + // • reserve == csize (18_000) ⇒ Ok (kills the `>=` boundary mutant). + // • reserve > csize (18_001) ⇒ Oversubscribed (kills `==`, and the + // `*=`-instead-of-`+=` per-link accumulation mutant that zeroes the + // load so nothing ever oversubscribes). + let rate = 1_000_000_000u64; + let at = [ll_flow( + 1, + 18_000, + 40_000_000, + &[0], + &[(1_000_000, 1_000_000)], + )]; + let sched = synthesize_cqf_longlink(&at, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP) + .expect("reservation exactly equal to csize is admissible"); + assert_eq!(sched.csize_bits, 18_000); + assert_eq!(sched.cycle_time_ps, 20_000_000); + + let over = [ll_flow( + 1, + 18_001, + 40_000_000, + &[0], + &[(1_000_000, 1_000_000)], + )]; + assert_eq!( + synthesize_cqf_longlink(&over, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP), + Err(CqfSynthError::Oversubscribed { + link: 0, + required_bits: 18_001, + csize_bits: 18_000, + }) + ); + } + + #[test] + fn longlink_synth_rejects_per_field_degeneracy() { + // The degenerate-flow guard is a disjunction: EITHER a zero reservation + // OR a zero deadline is rejected on its own (a `&&` mutant would demand + // both). Each field tested independently. + let rate = 1_000_000_000u64; + let zero_bits = [ll_flow(1, 0, 40_000_000, &[0], &[(1_000_000, 1_000_000)])]; + assert_eq!( + synthesize_cqf_longlink(&zero_bits, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP), + Err(CqfSynthError::DegenerateFlow { id: 1 }) + ); + let zero_deadline = [ll_flow(2, 1_000, 0, &[0], &[(1_000_000, 1_000_000)])]; + assert_eq!( + synthesize_cqf_longlink(&zero_deadline, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP), + Err(CqfSynthError::DegenerateFlow { id: 2 }) + ); + } + + #[test] + fn longlink_synth_selfcert_admits_slack_below_deadline() { + // The exact-bound self-cert is `D_max > deadline ⇒ reject`. When cycle + // flooring leaves D_max STRICTLY below the deadline the config is still + // feasible and must be admitted — a `D_max < deadline` mutant would + // reject it. 2 short hops, deadline 100 µs: 100/3 = 33_333_333 ps + // floored to 33_333_000 ps (ns granularity) ⇒ D_max = 99_999_000 ps + // < 100 µs, so Ok with a non-degenerate 1000 ps of slack. + let rate = 1_000_000_000u64; + let f = [ll_flow( + 1, + 1_000, + 100_000_000, + &[0, 1], + &[(1_000_000, 1_000_000); 2], + )]; + let sched = synthesize_cqf_longlink(&f, rate, DT_2US_PS, CQF_DEFAULT_BUFFER_CAP) + .expect("D_max strictly below deadline is feasible"); + assert_eq!(sched.cycle_time_ps, 33_333_000); + let dmax = cqf_delay_max_longlink_ps(&[1_000_000, 1_000_000], DT_2US_PS, 33_333_000); + assert!(dmax < 100_000_000, "flooring must leave real slack"); + } + + #[test] + fn longlink_buffer_count_cap_is_inclusive() { + // needed == cap is Ok (the cap is inclusive); only needed > cap fails. + // Kills the `needed > cap` ⇒ `needed >= cap` mutant. + let short = [LinkDelay { + min_ps: 0, + max_ps: 500_000, + }; 4]; + assert_eq!(cqf_buffer_count(&short, DT_2US_PS, TEN_US_PS, 3), Ok(3)); + let jittery = [LinkDelay { + min_ps: 1_000_000, + max_ps: 25_000_000, + }]; + assert_eq!(cqf_buffer_count(&jittery, DT_2US_PS, TEN_US_PS, 5), Ok(5)); + } } diff --git a/crates/spar-network/src/lib.rs b/crates/spar-network/src/lib.rs index 2cb1716..1403c10 100644 --- a/crates/spar-network/src/lib.rs +++ b/crates/spar-network/src/lib.rs @@ -66,8 +66,10 @@ pub mod tsn; pub mod types; pub use cqf::{ - CqfFlow, CqfSchedule, CqfSynthError, cqf_cycle_budget_bits, cqf_delay_max_ps, cqf_delay_min_ps, - synthesize_cqf, + CQF_DEFAULT_BUFFER_CAP, CqfFlow, CqfLongLinkSchedule, CqfSchedule, CqfSynthError, LinkDelay, + cqf_buffer_count, cqf_cycle_budget_bits, cqf_cycle_budget_bits_with_dead_time, + cqf_delay_max_longlink_ps, cqf_delay_max_ps, cqf_delay_min_longlink_ps, cqf_delay_min_ps, + cqf_hop_advance_cycles, synthesize_cqf, synthesize_cqf_longlink, }; pub use curves::piecewise::{PiecewiseAffineArrivalCurve, PwaError}; pub use curves::{