Skip to content

feat(analysis): authoritative network-wide NC bound = min(PLP,TFA) (REQ-NC-PLP-MIN-001)#307

Merged
avrabe merged 1 commit into
mainfrom
feat/nc-plp-min
Jun 26, 2026
Merged

feat(analysis): authoritative network-wide NC bound = min(PLP,TFA) (REQ-NC-PLP-MIN-001)#307
avrabe merged 1 commit into
mainfrom
feat/nc-plp-min

Conversation

@avrabe

@avrabe avrabe commented Jun 26, 2026

Copy link
Copy Markdown
Contributor

First v0.22.0 feature ("Deployable TSN synthesis" theme). Closes the V for REQ-NC-PLP-MIN-001.

What

network_wide_nc_bounds now emits a per-stream WcttAuthoritativeBound = min(TFA, PLP) — the tightest sound per-flow network-calculus bound. PLP and TFA are incomparable sound over-approximations (both ≥ exact, neither dominates), so their pointwise minimum is the number downstream consumers should trust: never worse than TFA, with the PLP win wherever PLP is tighter.

  • Seeds the authoritative vector from TFA (always computed); the milp-solver PLP arm tightens it via min.
  • When PLP is absent (feature off, or a non-feed-forward topology) the authoritative bound is TFA alone.
  • min over two sound bounds is itself sound → no new soundness surface; this is pure presentation/selection and does not change either engine.

Oracle — TEST-NC-PLP-MIN

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, 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 (a regression that blindly reported PLP fails here);
  4. without milp-solver, the authoritative bound equals TFA.

Genuinely red→green (WcttAuthoritativeBound did not exist before).

Gates (local)

  • 893 spar-analysis lib tests pass (milp-solver); no-default-features path compiles + passes.
  • clippy -D warnings clean; nightly fmt clean.
  • mutation --in-diff: 1/1 caught (the .min mutant is killed by the counterexample oracle).

Falsification

If WcttAuthoritativeBound ever exceeds either the TFA or the PLP bound for a stream, or omits a stream that has a TFA bound, the selection is wrong.

🤖 Generated with Claude Code

…A) (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) <noreply@anthropic.com>
@avrabe avrabe enabled auto-merge (squash) June 26, 2026 12:30
@codecov

codecov Bot commented Jun 26, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 90.47619% with 4 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/spar-analysis/src/wctt.rs 90.47% 4 Missing ⚠️

📢 Thoughts on this report? Let us know!

@github-actions

Copy link
Copy Markdown

Rivet verification gate

20/20 passed

count
Passed 20
Failed 0
Skipped (no steps) 0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.

@avrabe avrabe merged commit 211f627 into main Jun 26, 2026
18 checks passed
@avrabe avrabe deleted the feat/nc-plp-min branch June 26, 2026 14:59
avrabe added a commit that referenced this pull request Jun 30, 2026
v0.22.0 — "Deployable TSN synthesis". Three features shipped since v0.21.0:
- REQ-NC-PLP-MIN-001 (#307) — authoritative per-flow NC bound = min(PLP, TFA).
- REQ-WRPC-BINDING-003 (#308) — verify Actual_Connection_Binding resolves to a bus.
- REQ-TSN-SYNTH-QBV-GUARDBAND-001 (#309) — guard-band-aware 802.1Qbv GCL
  splitting (deployment-sound; charges the §8.6.8.4 transmission-overrun guard).

Release-handling: adopts rivet 0.22's `release` flow. The three features carry a
top-level `release: v0.22.0` field and are advanced to `verified` (each now has a
`verifies` link from its TEST-* feature); `rivet release status v0.22.0` reports
cuttable (every scoped artifact verified). Stale `fields.release` entries removed
on the migrated artifacts. Cross-version-checked: CI rivet v0.4.3 (merge gate) and
v0.7.0 (verification gate) both PASS with unchanged warning counts.

Scope correction (clean-room audit blocker): REQ-TSN-SYNTH-CQF-LONGLINK-001 moved
to v0.23.0 via `rivet release move` — its committed spec is unsound (delay interval
inverts on long links) and is deferred for a sound cycle-quantized rewrite; a
SPEC-UNDER-REVISION marker + the corrected model are recorded in the artifact.

Bumps workspace 0.21.0 → 0.22.0 (Cargo.toml, Cargo.lock, vscode-spar/package.json).

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant