Corrected RED semantics and fixed Days CUBIC trace conformance.

[baochunli]

This PR corrected RED and RED_ECN checker semantics against the source-backed RED contract, added CUBIC flight-size backoff checking, and fixed Days CUBIC trace generation so raw Days-generated CUBIC traces now replay to ACCEPT under cubic_check.

Changes

• Added a RED checker contract and validation notes covering the Floyd/Jacobson RED model, RFC 2309/RFC 3168 ECN behavior, the CSV witness contract, and intentional checker scope.

• Corrected RED threshold classification, over-max handling, stateful between-threshold probability, per-queue count derivation, fixed-point probability arithmetic, and physical overflow precedence.

• Enforced RED_ECN action and ECN transition rules so ECN-capable packets are marked to CE, Not-ECT congestion decisions drop, invalid ECN transitions reject, and physical overflow remains a hard drop.

• Added exact-output RED and RED_ECN fixture runners with coverage fixtures for threshold regions, probability hit/miss, count growth, overflow, malformed fields, and ECN transition cases.

• Extended the CUBIC trace contract with optional flight-size evidence and added checker fixtures that accept flight-size multiplicative decrease while continuing to reject cwnd-based backoff by more than one MSS.

• Made Days CUBIC congestion and timeout reductions use sender flight size for post-signal backoff while preserving current-cwnd Wmax and fast-convergence bookkeeping.

• Logged CUBIC flight size for congestion and timeout reactions, logged recovery-exit state transitions, and allowed bounded one-MSS tolerance only for float-derived byte snapshots in the Lean CUBIC checker.

• Validated the CUBIC checker against ns-3.47 scratch traces: unpatched ns-3.47 rejected because it used cwnd-based backoff, and the patched trace accepted after using flight-size backoff.

• Validated the corrected Days implementation by generating a fresh fattree CUBIC trace and checking the unmodified logs/fattree/cubic_events.csv directly with cubic_check; the trace returned ACCEPT.

Validation

• cd lean && lake build aqm_check
• bash lean/scripts/run-aqm-fixtures.sh
• bash lean/scripts/run-aqm-coverage-fixtures.sh
• bash lean/scripts/run-cubic-fixtures.sh
• cargo test --features test -- --show-output
• cargo test --features lean cubic -- --nocapture
• cargo check --features lean
• cd ../ns-3.47 && ./test.py -s tcp-abe-test
• cd ../ns-3.47 && ./ns3 build
• Ran ns-3.47 RED/ECN scratch experiments and checked generated CSVs with corrected aqm_check; the unpatched run rejected the full-queue mark_ecn row and the patched run accepted directly.
• Ran ns-3.47 CUBIC scratch experiments and checked generated CSVs with corrected cubic_check; the unpatched run rejected cwnd-based backoff and the patched run accepted flight-size backoff.
• Ran cargo run --features lean --bin days -- configs/benchmarks/topology/fattree_k4_tcp_f128_st.toml and checked logs/fattree/cubic_events.csv with lean/.lake/build/bin/cubic_check; the generated Days trace returned ACCEPT.