feat(network): TFA-strengthened PLP tightening to EXACT (REQ-NC-PLP-003)

[avrabe]

What

The v0.19.0 headline. Adds plp_bound_tfa_strengthened — the polynomial LP
(REQ-NC-PLP-001) with panco's per-server TFA-delay constraints layered on
(Bouillard fifo/plpConstraints.py, the FifoLP(tfa=True) path) — tightening
the PLP bound toward the exact worst-case FIFO delay.

Why it matters: it repairs the PLP/TFA incomparability

Pure polynomial PLP and TFA are incomparable sound over-approximations
(neither dominates). On the converging-bridge net (wctt.rs::bridge_converge_aadl)
pure PLP's tagged flow exceeds TFA — dataA 1148.33 µs > TFA 1048.09 µs,
the counterexample behind REQ-NC-PLP-MIN-001. TFA-strengthening drives that
flow to EXACT 1035.2 µs — back below TFA. On three_server_line it tightens
the crossing flows 72.22/61.11 → 68.4/58.4 µs (= EXACT).

Soundness

The LP is fed spar's OWN independent FP-TFA per-server delays (tfa_bound),
not panco's. This stays sound because:

• spar's per-server delays are sound upper bounds (≥ true delay), and
• the one-directional t[h] − t[j] ≤ d[j] constraints remain valid under any
  looser d[j] — so the strengthened bound never drops below EXACT.
• Adding constraints to a maximization can only lower the optimum ⇒
  strengthened ≤ pure PLP always.

Oracle

nc_validation.rs::plp_str_xval (feature milp-solver, a default feature ⇒
runs in the CI Test job) pins the panco tfa=True column
[68.4,58.4,57.98] / [1035.2,10030.7] under EXACT ≤ strengthened ≤ pure-PLP,
plus the converge_bridge headline (strengthened dataA ≤ TFA where pure PLP
could not). panco generator oracles/panco/panco_bench.py extended with the
converging-bridge net (regenerated offline; panco is not vendored, not in CI).

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 — matching the v0.18.0 cut discipline.

Trace

• REQ-NC-PLP-003 → implemented
• TEST-NC-PLP-STR → passing (satisfies REQ-NC-PLP-003, REQ-NC-VALIDATION-001)

Falsification

A bug feeding d[j] below the true per-server delay would make the bound
drop below EXACT — caught by the soundness floor (strengthened ≥ panco EXACT)
on every fixture. A formulation drift would break the panco tfa=True
agreement pin. Both are asserted per-flow.

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 86.86131% with 18 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/spar-network/src/plp.rs	86.86%	18 Missing ⚠️

📢 Thoughts on this report? Let us know!

[github-actions]

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.}