proofs(network): NC primitives min-plus theorems (Track D commit 5/6)#169
Merged
proofs(network): NC primitives min-plus theorems (Track D commit 5/6)#169
Conversation
Adds proofs/Proofs/Network/MinPlus.lean stating classical Network Calculus closed-forms mirroring crates/spar-network/src/curves.rs: - arrival_at_mono / service_at_mono: monotonicity of α(t), β(t) - service_at_zero_below_latency: β(t) = 0 for t < latency - backlog_bound_classical: σ + ρ·latency for stable affine flow - delay_bound_classical: latency + σ/rate (horizontal distance) - output_bound_rate_preserved: burst grows by ρ·latency through server - compose_delays: serial chain delay sums per-hop terms Some proofs use `sorry` and a TODO(v1.0.0) comment; statements are the load-bearing artifact, full discharge is post-MVP. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
Lean CI surfaced "Unknown constant Nat.min_le_min" at MinPlus.lean:110. The `Nat.min_le_min` qualified path doesn't exist in Mathlib v4.29.x; the unqualified `min_le_min` (defined for any LinearOrder, including Nat) discharges the same goal. Format-only edit — same proof, correct lemma name. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
CI surfaced "No goals to be solved" at MinPlus.lean:416. The `simp [hne1, hne2, h1, h2]` on line 412 fully discharges the compose_delays_zero_latency residual; the trailing `sorry` (left as a TODO during initial drafting because simp's behaviour wasn't verified locally) is therefore unreachable and Lean rejects it. Removing the sorry + its TODO comment. The proof is now complete without sorry — one fewer TODO(v1.0.0) item to chase down. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
proofs/Proofs/Network/MinPlus.lean— Lean 4 / Mathlib statements of the classical Network Calculus closed-forms that anchorcrates/spar-network/src/curves.rs(Track D commit 3, PR #161). The Lean module is wired intoproofs/Proofs.leanalongside the existingProofs.Scheduling.*modules.What is delivered
Theorems in
Spar.Network.MinPlus(mirroring Le Boudec & Thiran, Network Calculus, ch. 1, theorems 1.4.1-1.4.3):arrival_at_mono— α(t) monotone non-decreasingservice_at_mono— β(t) monotone non-decreasingservice_at_zero_below_latency— β(t) = 0 for t ≤ Tservice_at_zero_strictly_below_latency— strict variantservice_at_zero_at_zero— β(0) = 0backlog_bound_classical— B = σ + ρ·Tsorry+ TODO v1.0.0)delay_bound_classical— D = T + σ/Rsorry+ TODO v1.0.0)output_bound_rate_preserved— rate / peak preserved, burst inflated by ρ·Toutput_dominates_input— α'(t) ≥ α(t)sorry+ TODO v1.0.0)compose_delays— naive serial-chain sumcompose_delays_dominates— chained-delay dominationsorry+ TODO v1.0.0)arrival_at_zero_is_burst— α(0) = σsorryfor peak case; flags spec/impl mismatch)Plus structural lemmas (
output_preserves_*,output_stable_for_chain,backlogChained_eq_sum, etc.) and thecompose_delays_zero_latencyarithmetic identity (one residualsorryfor div_ceil normalisation).Per project policy,
sorryis acceptable here — the statements are the load-bearing artifact (they pin the math the Rust min-plus kernel commits to). Full proof discharge is scheduled for v1.0.0.Files changed
proofs/Proofs/Network/MinPlus.lean(new, 417 LOC)proofs/Proofs.lean(addimport Proofs.Network.MinPlus)artifacts/requirements.yaml(REQ-NETWORK-007)artifacts/verification.yaml(TEST-LEAN-MINPLUS→ REQ-NETWORK-007)lake buildstatusNot run locally —
lake/elanare not available in the local sandbox. The proofs CI gate from PR #151 is the verifier here. If a build break shows up there, the offending theorem will be the only one needing adjustment (the type definitions are direct mirrors of the Rust struct fields and the proofs are either trivialrflorsorry-discharged).Test plan
Proofs/Network/MinPlus.leancargo build --workspaceclean (verified locally — Lean changes don't touch Rust)rivet validateclean (verified locally — same 91 pre-existing warnings, no new ones)Proofs.Network.MinPlusnamespace is reachable from downstream Lean modules (none yet — Track D commit 6 will consume)Follow-ups (post-MVP)
sorrytheorems via real-number reasoning (Mathlibrpow,div_ceillemmas).arrival_at_zero_is_burstwith the Rust short-circuitif t_ps == 0branch — either fold into the spec or split into a separate "Rust-impl-aligned" lemma.🤖 Generated with Claude Code