What ACCEPT certifies (DCQCN)

This page documents the legacy floating-point DCQCN certificate (lean/LeanGuard/DcqcnEventLog.lean): DCQCN-specific consequences of trace acceptance, as instances of the generic obligation templates in /docs/research/design (pairing, gates, parameter stability, bounded state), specialized to the DCQCN event vocabulary (cnp_sent, cnp_recv, timer_tick). Its pairing, gate, freeze, and bound claims below remain current.

The statements below are with respect to the canonicalized trace order (sorted by (time_ns, event_id)), not raw CSV file order.

A separate Days AGO DCQCN certificate family (p10c_dcqcn_check) covers the Days AGO DCQCN, whose controller runs in exact integer arithmetic (parts-per-billion scale, one floor per complete rational expression). It keys on the full EventKey order and is not interchangeable with the legacy (time_ns, event_id) CSV family documented here. Exact DCQCN runs on all four backends, but device runs do not return the transition records, so DCQCN certificates come from Scalar and CPU runs.

No spurious CNP receptions (pairing)

Every cnp_recv row must correspond to a distinct earlier cnp_sent row with the same (flow_id, pkt_id) key.

• A cnp_recv cannot appear without a prior matching cnp_sent.
• No single cnp_sent can be consumed by more than one cnp_recv (injective matching).
• Not every cnp_sent must be matched by the end of the trace: pending sends can remain (modeling loss or delay).

Intuition: the checker maintains a pending set/map keyed by (flow_id, pkt_id) and enforces insert/remove discipline.

Interval-gate properties

DCQCN has interval gates on both sink and source behavior:

• Sink gate: consecutive cnp_sent rows for the same sink endpoint must be separated by at least cnp_interval_ns.
• Source gate: multiplicative-decrease reaction on cnp_recv is applied at most once per cnp_interval_ns.
  • If a cnp_recv arrives "too soon" (gate blocks), the trace must log the corresponding no-op post-state snapshot (unchanged under the source-gate semantics).

Intuition: the checker stores per-endpoint "last gate time" and enforces either an update or a no-op snapshot depending on the gate outcome.

Parameter stability for endpoints

For each endpoint, DCQCN parameters are constant across all rows for that endpoint, including (representative):

• g_ppb, mi_ppb
• cnp_interval_ns
• rate bounds (min_rate_bps, max_rate_bps)

Intuition: the checker uses a freeze-on-first-use record per endpoint; later rows must match the frozen parameter block exactly.

Bounded source state

Every source snapshot row (cnp_recv and timer_tick) satisfies the bounds:

• 0 <= alpha_ppb <= 1_000_000_000
• min_rate_bps <= rate_bps <= max_rate_bps

Intuition: the executable update rules are designed to preserve these bounds, and the checker enforces snapshot equality with the computed post-state (so the logged snapshots inherit the invariant).