Ported CUBIC, DRR, and WFQ checkers onto the generic TraceSpec interface.

[baochunli]

Summary

Ports the remaining three LeanGuard checkers — CUBIC, DRR, and WFQ — onto the generic LeanGuard.Shared.TraceSpec interface, matching AQM, PFC, and DCQCN (the latter merged in #98). This closes the mechanization item called out in the paper's conclusion — "extending per-protocol mechanization from AQM, PFC, and DCQCN to the CUBIC, WFQ, and DRR checkers" — so all six protocol checkers now share the same replay interface and delegate their soundness/preservation lemmas to the once-and-for-all generic proofs in TraceSpec.lean.

This is a behavior-preserving structural refactor, not new proof work. Each checker's hand-rolled recursive go loop is replaced by a ReplayState/TraceSpec instantiation. The hard semantic content — step (transition semantics), recordCover (coverage), key, and canonicalizeRows ordering — is reused unchanged. No protocol instantiates the preservation lemma with a concrete invariant, so there are no bespoke proofs to discharge; a green lake build is the proof check (the theorems elaborate at build time).

Commits (one per protocol)

1. Port CUBIC — step takes Row directly; recordCover(cov, r). Simplest case.
2. Port DRR — step fed via toEvent; recordCover(cov, g, r) reads the pre-step Global.
3. Port WFQ (+ shared Coverage.lean) — see design note below.

All three follow the DCQCN ReplayState { g, lastKey } template rather than the AQM/PFC no-wrapper template, because each currently performs a per-row keyLt "global key went backwards" monotonicity check; that check is preserved inside stepRow.

Design note: WFQ's observer accumulator → CoverageState

WFQ's coverage observer threads a distinct-class accumulator (seenClasses) that lived outside both Global and CoverageState, returning CoverageState × List Nat. The generic observer signature CoverageState → State → Row → CoverageState has no room for it. Rather than putting coverage bookkeeping into the trusted replay state, this PR adds a generic seen : Std.HashSet Nat scratch field to the shared CoverageState (plus covSeen and a covMerge union). This keeps WFQ's observeCoverage self-contained and its stepRow uniform with the other five checkers, and preserves the observation-vs-replay separation that replayWithObserverM_agrees formalizes.

The field is never serialized (covList/CoverageReport.toJson only emit points/counts), so coverage reports and golden fixtures are unchanged, and the cross-layer aqm_dcqcn_check merge is unaffected (AQM/DCQCN leave seen empty). class_count_ge_2 now gates on cov.seen.size >= 2, equivalent to the old distinct-list length; the now-dead listContains helper is removed.

Preserved (no external change)

checkRowsWithCoverage / checkRows keep their signatures, so CubicMain / DrrMain / WfqMain, the composite AqmDcqcnMain, lakefile.lean, CI, configs/ci/*.toml, and all fixtures/golden files are untouched.

Verification

• Build: lake build of all 7 checkers — green, no warnings / sorry / errors. Since Coverage.lean is shared, this recompiles every protocol + aqm_dcqcn_check, and elaborates all soundness/preservation proofs.
• Golden fixtures: CUBIC 5/5 (behavior unchanged), AQM 38/38 + AQM coverage 8/8 (regression check for the shared Coverage.lean edit; confirms seen is not leaked into reports).
• Conformance matrix (leanguard-run drives the Days simulator, then runs the checkers on emitted traces — the only end-to-end coverage DRR/WFQ have):
  • leanguard_cubic.toml → accept: true (aqm_check, cubic_check)
  • leanguard_drr.toml → accept: true (aqm_check, drr_check)
  • leanguard_wfq.toml → accept: true (aqm_check, wfq_check)

Out of scope (possible follow-ups)

• Dedicated golden fixtures + run-drr-fixtures.sh / run-wfq-fixtures.sh + CI steps for DRR/WFQ (they have none today; only the conformance matrix exercises them).
• Harmonizing the keyLt check across all six checkers (AQM/PFC dropped it and rely on canonicalizeRows sorting alone).
• Proving concrete protocol invariants via replayM_preserves (a much larger effort that no existing checker attempts).

🤖 Generated with Claude Code