Conversation
… min-plus ops (Track D commit 3/6)
Adds the math kernel that v0.8.0 WCTT analysis (commit 4) will compose.
spar-network gets a curves module with:
- ArrivalCurve (leaky-bucket affine: σ + ρ·t with optional peak)
- ServiceCurve (rate-latency: rate · max(0, t − latency))
- backlog_bound (sup_t {α(t) − β(t)} closed-form)
- delay_bound (horizontal distance closed-form)
- residual_service (β minus competing flow)
- output_bound (burst inflation through a server)
All values are u64 picoseconds / bytes — no f64. Closed-form for the
affine + rate-latency case; piecewise-affine extension is a v0.8.x
follow-up.
No analysis pass, no Lean theorems, no latency.rs integration in this
commit. Those are Track D commits 4-6.
New requirement: REQ-NETWORK-005.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
AI Code Review for PR #161pulseengine/spar: SummaryThis pull request introduces a new module
Potential Bugs or Issues
Security ConcernsNone identified. Suggestions for Improvement
Overall AssessmentThe pull request introduces a robust implementation of Network Calculus primitives that are essential for the WCTT analysis pass. The code is well-structured, with clear separation of concerns between the This review was generated by a local AI model. It is advisory only and may contain inaccuracies. Reviewed at |
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
Summary
Track D commit 3 of 6 for v0.8.0. Adds the pure-math Network Calculus
kernel that the upcoming
wctt.rsanalysis pass (commit 4) willcompose. No analysis pass, no Lean theorems, no
latency.rsintegrationyet — those are commits 4, 5, and 6.
New module
crates/spar-network/src/curves.rs:ArrivalCurve— leaky-bucket affineσ + ρ·twith optional peak cap.ServiceCurve— rate-latencyR · max(0, t − T).backlog_bound(α, β)— closed-formσ + ρ·T(returnsNcError::UnstableServerwhenρ > R).delay_bound(α, β)— closed-formT + σ/Rhorizontal distance.residual_service(β, α_c)— FIFO residual: rateR − ρ_c, latencyT + σ_c/(R − ρ_c).output_bound(α, β)— burst inflation theorem: σ' = σ + ρ·T, ρ' = ρ.All values are
u64picoseconds / bytes / bits-per-second so the kernelis free of
f64drift. Internal arithmetic widens tou128for therate × time products to avoid overflow on realistic inputs (e.g. 100
Gbps × 1 ms ≈ 10⁸ bytes). Truncation rounds bytes-served down and
durations up, keeping the WCTT consumer on the safe side of every
bound.
References Le Boudec & Thiran "Network Calculus" §1.4 (the closed-form
bounds for the affine + rate-latency case) per the design doc
docs/designs/track-d-tsn-wctt-research.md§4.3-4.4.Out of scope for this commit (per the design doc): piecewise-affine
curves, TSN-specific service curves (TAS/Qbv, Qbu, Qcr ATS), PBOO
concatenation, and any AADL coupling —
curves.rsdeliberately doesnot consume from
extract.rs.New requirement:
REQ-NETWORK-005. New verification:TEST-NC-CURVES.Test plan
cargo build -p spar-networkcleancargo test -p spar-network— 14 curves tests + 12 prior tests + 6 integration tests, all greencargo clippy --workspace --all-targets -- -D warningscleancargo fmt --all -- --checkcleanrivet validatePASS (only the pre-existing schema-warning baseline)Tests added (14)
arrival_curve_at_zero_is_burstservice_curve_at_latency_is_zeroservice_curve_above_latency_grows_linearlyaffine_arrival_evalaffine_arrival_with_peakbacklog_bound_classicalbacklog_bound_unstable_when_rate_exceeds_serviceρ > R→NcError::UnstableServerdelay_bound_classicaldelay_bound_unstable_when_rate_exceeds_serviceρ > R→ errorresidual_service_two_flowsresidual_service_unservableρ_c ≥ R→NcError::UnservableFlowoutput_bound_burst_inflationoutput_bound_rate_preservedcompose_two_servers_classical🤖 Generated with Claude Code