LeanGuard (Use Guide)

Scope: Days AGO and Legacy Days. This guide builds the Lean checkers, emits Legacy Days traces, and runs the checkers for both engines.

Prerequisites

• Rust and Cargo.
• Lean 4 through elan, including lake.

The repository pins Lean in lean/lean-toolchain. Build the executor proof library and every checker from the repository root:

cd lean
lake build DaysExecutor \
  dcqcn_check pfc_check cubic_check tcp_check drr_check wfq_check sp_check \
  aqm_check aqm_dcqcn_check \
  p10c_mechanisms_check p10c_aqm_check p10c_dcqcn_check p10c_collective_check \
  p10c_roce_check
cd ..

Emit legacy traces

The legacy engine emits protocol traces with Cargo feature lean. It writes them beneath log_path and records the non-empty files in log_path/traces.json.

CSV output must be enabled. csv_logging defaults to true; if a config sets csv_logging = false, the engine creates neither the log directory nor the trace manifest.

The committed CI fixtures provide small deterministic runs:

# DCQCN and AQM (with the PFC-capable link path enabled)
RUST_LOG=info cargo run -p days-legacy --features dcqcn,lean,l2_pfc --bin days-legacy -- \
  configs/ci/leanguard_dcqcn.toml

# PFC
RUST_LOG=info cargo run -p days-legacy --features lean,l2_pfc --bin days-legacy -- \
  configs/ci/leanguard_pfc.toml

# TCP CUBIC
RUST_LOG=info cargo run -p days-legacy --features lean --bin days-legacy -- \
  configs/ci/leanguard_cubic.toml

# DRR
RUST_LOG=info cargo run -p days-legacy --features lean --bin days-legacy -- \
  configs/ci/leanguard_drr.toml

# WFQ
RUST_LOG=info cargo run -p days-legacy --features lean --bin days-legacy -- \
  configs/ci/leanguard_wfq.toml

# AQM
RUST_LOG=info cargo run -p days-legacy --features lean --bin days-legacy -- \
  configs/ci/leanguard_aqm.toml

The fixture's log_path names the output directory. A trace is useful only when its configured mechanism executes; the examples above select the matching flow or scheduler.

Simulate and check legacy traces

leanguard-run runs the separately built days-legacy binary, discovers traces from traces.json (or a known-filename fallback), and invokes the matching checkers:

cargo build -p days-legacy --features dcqcn,lean,l2_pfc --bin days-legacy
cargo run --bin leanguard-run -- \
  --config configs/ci/leanguard_dcqcn.toml \
  --legacy-runner target/debug/days-legacy \
  --checker-dir lean/.lake/build/bin

Re-check the existing log_path without rerunning the simulator:

cargo run --bin leanguard-run -- \
  --config configs/ci/leanguard_dcqcn.toml \
  --mode check-only \
  --checker-dir lean/.lake/build/bin

By default, simulate-and-check refuses threading = "multiple"; use --allow-nondeterministic only when unordered legacy emission is intentional.

Run checkers directly

After the build above, run these commands from lean/.

Legacy certificate checkers:

./.lake/build/bin/dcqcn_check <path/to/dcqcn_events.csv>
./.lake/build/bin/pfc_check <path/to/pfc_events.csv>
./.lake/build/bin/cubic_check <path/to/cubic_events.csv>
./.lake/build/bin/drr_check <path/to/drr_events.csv>
./.lake/build/bin/wfq_check <path/to/wfq_events.csv>
./.lake/build/bin/aqm_check <path/to/aqm_events.csv>
./.lake/build/bin/aqm_dcqcn_check <path/to/aqm_events.csv> <path/to/dcqcn_events.csv>

Days AGO checkers:

./.lake/build/bin/tcp_check <path/to/tcp_events.csv>
./.lake/build/bin/sp_check <path/to/sp_events.csv>
./.lake/build/bin/p10c_mechanisms_check rate <path/to/rate_events.csv>
./.lake/build/bin/p10c_mechanisms_check pfc <path/to/pfc_events.csv>
./.lake/build/bin/p10c_mechanisms_check drr <path/to/drr_events.csv>
./.lake/build/bin/p10c_mechanisms_check wrr <path/to/wrr_events.csv>
./.lake/build/bin/p10c_mechanisms_check wfq <path/to/wfq_events.csv> [<path/to/pfc_events.csv>]
./.lake/build/bin/p10c_aqm_check <path/to/aqm_events.csv>
./.lake/build/bin/p10c_dcqcn_check <path/to/dcqcn_events.csv>
./.lake/build/bin/p10c_dcqcn_check trace <path/to/dcqcn_events.csv> <path/to/dcqcn_cnp_arrivals.csv>
./.lake/build/bin/p10c_collective_check <path/to/collective_events.csv>
./.lake/build/bin/p10c_roce_check receiver <path/to/roce_receiver.csv>
./.lake/build/bin/p10c_roce_check sender <path/to/roce_sender.csv> <path/to/dcqcn.csv> \
  --pfc <path/to/pfc.csv> [--horizon-ns <ns>] [<stop_time_ns>]
./.lake/build/bin/p10c_roce_check trace <path/to/roce_sender.csv> <path/to/roce_receiver.csv> \
  <path/to/dcqcn.csv> --pfc <path/to/pfc.csv> [--horizon-ns <ns>] \
  [--collective <path/to/collective.csv>] [<stop_time_ns>]

p10c_roce_check reads one sender format: the full P16 sender schema, every column the executor's roce_sender_transitions_csv writes (class_paused, data_class, the window columns, maximum_rate_bps and initial_rate_bps included). It rejects a log that lacks any of them and names the missing columns. No older sender layout is read; the committed fixtures are all in this format.

p10c_roce_check certifies RoCE queue pairs from the executor's roce_receiver_transitions_csv, roce_sender_transitions_csv and dcqcn_transitions_csv of one full-observation run:

• receiver checks each data arrival: the notification point, the in-order frontier, the ACK cadence, duplicates, and the NACK rate limit.

• sender checks each pacing tick, ACK, NACK and timeout. It needs the DCQCN log of the same run, because the controller's rate decides the sender's status. A queue pair's controller has no events of its own: each of its transitions happens inside a sender transition, and its DCQCN row carries that sender row's event key. The checker requires a DCQCN row at a sender row exactly when the row is an ACK or NACK with input_ce_echo = 1 on a pair that is not yet complete (a feedback row), the ACK that completes the pair (an advance row with frozen = 1; the controller then changes no more), or a row before whose bound a rate increase or cut is due (an advance row). A tick's rate_bps must equal the controller's rate after every instant due before time_ns + 1, and a window-blocked tick (window_blocked = 1, the pair's unacknowledged bytes at or above its window) sends nothing, adds no credit and parks. It also checks that every pending pacing tick and timeout fires before any later event of the pair.

• Host-link PFC (schema Amendments 1-3). A tick with class_paused = 1 found the pair's data class (data_class) paused on its host: it must send nothing, add no credit and park the pacer. A resume row records a PFC RESUME restarting a pacer that a paused tick parked, on its next grid point strictly after the RESUME (or stopped beyond the stop time). The rows of one RESUME share its event key, for distinct flows of one node in increasing flow_id order; no other rows may share a key. Every sender log carries data_class, so --pfc with the run's pfc_transitions_csv is required (header-only for a run without PFC), and the pauses and resumes are checked against the host PAUSE and RESUME records in it:

  • a paused tick finds its class paused at its host at its event key, and an unpaused tick finds it not paused;
  • every resume row shares the key of the host RESUME that unpaused its class at its node;
  • every host RESUME that unpauses class p at node n restarts, in resume rows at its key, every pair of class p at n that a paused tick parked and that can restart (work remaining, not complete). A missing resume row is caught at the RESUME, even when a later ACK, NACK or timeout restart would mask it.

  What this certifies, and what it trusts: it certifies the transition mechanics of a pause and a resume and their warrant and completeness against the host PFC records. It trusts the data_class value each row carries, the host PFC records themselves (checked by the P10c PFC rules for internal consistency, not against the switch threshold records that emitted the frames), and that a parked pair that cannot restart writes no resume row.

• A queue pair whose first ticks find its class paused writes no rate until its first crediting tick. Until that tick, or the pair's first DCQCN row, reveals the rate, the checker compares every field exactly except a status that depends on the rate; each such status bounds the rate, and the revealed rate must lie within the bounds. While a pair's controller is pristine (no DCQCN row yet), every rate its rows show must equal the sender log's initial_rate_bps.

• --horizon-ns <ns> checks a prefix of a run: the logs must hold exactly the run's events with time_ns < ns. Pending events at or after the horizon need not have fired; stop decisions are still checked against the run's stop time.

• --collective <path> (trace mode) joins the run's collective_transitions_csv to the queue-pair logs. A released RoCE collective stage's pair runs its first pacing tick at the release instant, from the armed status the release row records; a logged stage that is never released has no queue-pair rows; and a local completion caused by a RoCE pair shares its event key with that pair's ACK that brings its acknowledgment to the pair's total.

p10c_collective_check replays each stage's inbound rows by the transport that sent them: TCP's in-order frontier, which absorbs buffered out-of-order segments, or a RoCE queue pair's Go-back-N frontier, which advances only on the packet at the frontier and requires each packet to be the pair's packet at its PSN. A RoCE stage's rows carry its MTU; a compute stage after a RoCE collective carries the predecessor's MTU and pacing interval, which must equal a logged predecessor's. The checker knows the five Days AGO algorithms (lean/LeanGuard/P10c/Collective/): each ring's stage positions and owner recurrence per channel, with every channel required to be one ring over the collective's ranks; UniformFloor message sizes; an all-to-all's n (n - 1) pairs of floor(S / n) bytes, or, for a seeded one, the per-pair bytes re-derived from the certificate's seeded_matrix parameters by the same integer construction (SeededMatrix.lean); and a SendRecv's one message. Dependencies are counted joins: a stage's local and inbound predecessor lists are checked against its counts and against the operations the stage follows (a stage that follows a collective must wait for that collective's whole completion at its rank, a compute predecessor must sit on the same host), and each credit is tied to a logged completion or a replayed frontier reaching the predecessor's total. A stage notify's release arms its lead's timer at the sender, and its delivery lands exactly its recorded delay after the release, as one whole chunk. Every inbound claim, arrival and local completion is bound to the delivery host its row records (target_node, cause_target_node), and the rows one cause produces must agree on that host.

• trace runs both, then the cross-role checks. Every data arrival must be a packet the sender emitted. Every ACK or NACK the sender applies must have been sent earlier by the receiver, with the same acknowledgment and the same ECN echo (feedback_ce_echo on the receiver row, input_ce_echo on the sender row); a queue pair sends and receives no CNP.
• <stop_time_ns> is the image's stop_time_ns. No CSV records it, and it decides whether a pacer's next tick is armed or stopped. With it, each decision is checked exactly, no row may lie after it, and no pending event at or before it may be left unfired at the end of the log. Without it, the checker requires one stop time consistent with every armed and stopped decision in the log, and checks unfired events against the latest time the log shows to be before the stop.

Committed Days AGO certificate fixtures can be checked directly, for example:

./.lake/build/bin/p10c_aqm_check fixtures/p10c/aqm_executor_accept.csv
./.lake/build/bin/p10c_dcqcn_check fixtures/p10c/dcqcn_executor_trace_accept.csv
./.lake/build/bin/p10c_dcqcn_check trace fixtures/p10c/dcqcn_cnp_join_t26_accept.dcqcn.csv \
  fixtures/p10c/dcqcn_cnp_join_t26_accept.cnp.csv
./.lake/build/bin/p10c_mechanisms_check drr fixtures/p10c/drr_executor_accept.csv
./.lake/build/bin/p10c_collective_check fixtures/p10c/collective_allgather_executor_accept.csv
./.lake/build/bin/p10c_roce_check trace fixtures/p10c/roce_trace_timeout_executor_accept.sender.csv \
  fixtures/p10c/roce_trace_timeout_executor_accept.receiver.csv \
  fixtures/p10c/roce_trace_timeout_executor_accept.dcqcn.csv \
  --pfc fixtures/p10c/roce_trace_timeout_executor_accept.pfc.csv \
  "$(cat fixtures/p10c/roce_trace_timeout_executor_accept.stop_time_ns)"
./.lake/build/bin/sp_check fixtures/sp/sp_priority_and_fifo_accept.csv
./.lake/build/bin/sp_check fixtures/sp/sp_compiled_executor_accept.csv
./.lake/build/bin/p10c_mechanisms_check wfq fixtures/p10c/wfq_compiled_executor_accept.csv
./.lake/build/bin/tcp_check fixtures/tcp/reno-compiled-tcp-events.csv

The legacy checkers, tcp_check, and sp_check also accept --coverage-out <path>. leanguard-run --coverage uses that option and aggregates returned coverpoints. The p10c_* executables do not expose the coverage flag.

Days AGO AQM rows

p10c_aqm_check replays aqm_transitions_csv: one row per admission decision at a switch queue with an ECN ramp (Lean rules: the Aqm namespace of lean/LeanGuard/P10c/Semantics.lean and lean/LeanGuard/P10c/AqmEventLog.lean). Each row names the packet's kind (packet_kind: data, tcp_data, roce_data, tcp_ack, roce_ack, roce_nack, dcqcn_cnp, feedback, pfc, roce_pacing_timer or stage_notify), which the writer takes from the run's observed packets, its byte depth before admission and its size, the run's seed, and the queue's ramp (capacity_bytes, kmin_bytes, kmax_bytes, pmax_numerator, pmax_denominator).

• The checker recomputes every decision. It derives the draw from the seed, the queue (node_id, queue_id) and the payload, exactly as the executor does (the switch configuration), and applies the ramp in integer arithmetic. It also checks that the policy is well formed, that each queue's policy and the run's seed stay constant, and that the ECN bit changes exactly on a mark.
• Days AGO marks only data packets (data, tcp_data, roce_data). Any other packet is admitted unmarked at any depth below the byte capacity, so an ACK inside or above the ramp must show enqueue and an unchanged ECN bit.
• A packet's kind is the same on every row of its payload (one row per queue it crosses); a kind that changes between rows is rejected.
• What remains trusted is the kind itself: a packet relabelled consistently on all of its rows cannot be told from a packet of that kind, as RoCE senders' data_class and WFQ's PFC classes are trusted. aqm_roce_acks_whole_packet_relabel_trusted_limit_accept.csv pins this limit: a marked data packet relabelled roce_ack on all of its rows, its mark removed, is accepted.

The CI fixtures aqm_roce_acks_compiled_executor_accept.csv (configs/leanguard/aqm_roce_acks.toml, a byte step) and aqm_roce_acks_ramp_compiled_executor_accept.csv (aqm_roce_acks_ramp.toml, a ramp with pmax = 4/5) have RoCE ACKs admitted unmarked in a queue that marks data, and the ramp fixture has data both marked and unmarked between its thresholds. Their mutations must be rejected: a data packet left unmarked, a marked ACK, a relabel that keeps a mark, a draw flipped either way, a changed seed, and a kind changed on one row of a packet. The AQM differential's reference decides independently: it writes SplitMix64 out and applies the ramp in its rational form, with no high multiply.

Days AGO WFQ and SP rows

p10c_mechanisms_check wfq replays wfq_transitions_csv: one row per transition of a WFQ switch egress queue, at the event key of the event that performs it (Lean rules: the Wfq namespace of lean/LeanGuard/P10c/Semantics.lean and WfqLog in MechanismEventLog.lean). Virtual time and finish tags are exact rationals, written numerator/denominator in lowest terms and normalized by the egress link's rate: a packet's service is size_bytes * 8 / weight, and virtual time advances by elapsed_ns * rate_bps / (10^9 * W) over the active classes' weight sum W. A packet's class is flow_id % class_count.

• enqueue (phase 0): an admitted arrival. An idle scheduler resets virtual time and every class's finish tag to zero; otherwise virtual time advances. virtual_start must be the later of virtual time and the class's last finish tag, and finish_tag the start plus the packet's service.
• select (phase 2): a service start. The scheduler state is unchanged. queued_packets must be exactly the packets waiting (served one included), each with its enqueue's finish tag and its PFC class, and the served packet must have the least finish tag, the earliest enqueue among equal tags, among the packets whose class is not in paused_priorities.
• complete (phase 1): a service completion. Virtual time advances over the active set that still holds the packet; the class then loses it, and a scheduler left idle resets its virtual time and that class's finish tag.

A queue that does not start empty and idle (a run resumed from a checkpoint) opens with an initial row whose event-key columns are empty. It gives the starting scheduler state, the waiting packets in queue order with their finish tags and PFC classes, the in-service packet (payload, finish_tag, pfc_priority; empty when there is none) and the starting paused priorities. Their counts by class must equal the starting active counts. Other queues start from the empty state.

Each row's before state must equal the queue's replayed state, and its after state the reference update. The executor records each transition's after state from its own scheduler, after the event; wfq_transitions_csv writes before as the queue's state after its previous row (its starting state before the first) and a completion's finish tag as its packet's at selection, or in the starting state. A change to the scheduler between two rows would therefore show in the second row's after, which the checker recomputes. These are the rules of the legacy wfq_check (Demers, Keshav and Shenker, with the same idle resets) up to the rate normalization; wfq_check still certifies days-legacy.

PFC classes and pauses:

• A packet's PFC class is fixed for its lifetime: its enqueue row (pfc_priority) or the initial row gives it, and every select listing must repeat it.
• pfc_monitor (on every row) says whether the queue has a PFC monitor. Without one, every class is zero and no select may list a paused priority.
• With one, the checker needs the run's PFC certificate (pfc_transitions_csv) as its second argument, checks it with the P10c PFC rules, and requires each select's paused_priorities to be the queue's pause state at the select's event key: the controller sets of the queue's control rows before that key. A priority the initial row starts paused must have a non-empty controller set before its first control row; any other, an empty one.
• What remains trusted is each packet's class itself (its flow's packet priority, written at enqueue), as RoCE senders' data_class is.

The checker does not certify timing: a completion's time is not checked against the packet's serialization time on the link, and service starts are not checked for work conservation. Virtual time depends on those times, so the certificate holds for the event times the run recorded.

sp_check reads sp_transitions_csv, the same schema as its hand-written fixtures: enqueue (phase 0), schedule (phase 2, with the transmission's completion time) and depart (phase 1). It keys a scheduler by one number, so a Days AGO SP queue writes scheduler_id = node_id * 2^32 + queue_id and repeats node_id and queue_id. A queue that starts non-empty opens with an initial_in_service row for the packet it is transmitting (with the time of its pending TxComplete) and an initial_queued row per waiting packet in queue order; their event-key columns are empty, and sp_check applies them before the events. sp_check has no pause model, so it certifies SP only without PFC: under PFC, a Days AGO SP queue serves the first packet whose class is not paused, which sp_check rejects as an SP order violation.

Days AGO DCQCN rows

p10c_dcqcn_check replays dcqcn_transitions_csv: one row per controller transition of an unreliable DCQCN flow or a RoCE queue pair (schema: days-gpu/plans/briefs/p16/dcqcn-schema.md; Lean rules: lean/LeanGuard/P10c/Dcqcn/Semantics.lean and DcqcnEventLog.lean). The Mellanox-form controller owns no events, so each row sits at the event key of the flow transition that applied its timers, and bound_ns is the exclusive bound of the instants applied: the event's time at a feedback arrival (phase 0), one nanosecond later at a pacing tick or timeout (phase 1). The arithmetic is exact: a 63-bit fixed-point alpha, integer rates, one floor per update, a cut of R - ceil(R * alpha / 2^64), and an average of floor(R_C / 2) + floor(R_T / 2).

• feedback: a CNP arrival at an unreliable flow, or an ACK or NACK with its ECN echo set at a queue pair that is not complete after it. after must equal on_feedback(before, time_ns).
• tick: every pacing tick of an unreliable flow, emitting or not. after must equal materialize(before, time_ns + 1), and after_current_rate_bps is the rate the tick read.
• advance: any other transition that applied a rate increase or a cut, or the ACK that completes a queue pair.

A row with frozen = 1 (the completing ACK of a queue pair, or the tick that emits an unreliable flow's last byte) is replayed by settle, which applies the instants due before the bound and stops the controller; the flow has no later row.

Each row's before must equal the flow's previous after; the first row's before is the pristine controller of the row's configuration. Rows must arrive in strictly increasing EventKey order. In trace mode the checker also reads dcqcn_cnp_arrivals_csv (time_ns,flow_id,payload, one row per CNP delivered to a reaction point): a CNP at or before its unreliable flow's freeze must be exactly one feedback row of that flow at its time; every feedback row of an unreliable flow must be such a CNP; and a CNP addressed to a flow without tick rows is rejected, because a queue pair receives no CNP. A queue pair's ticks have no tick row: p10c_roce_check ties each tick's rate_bps to the controller instead, as described above.

Continuous integration

.github/workflows/leanguard.yml has two jobs.

lean-fixtures builds the checkers, audits the DaysExecutor axioms (lean/scripts/audit-days-executor-axioms.sh), and runs these scripts under lean/scripts/, each on committed fixtures: accept fixtures, plus mutations each checker must reject with a named message.

• Days AGO certificates:
  • the P10c collective, DCQCN and RoCE campaigns (run-p10c-collective-campaign.sh, run-p10c-dcqcn-campaign.sh, run-p10c-roce-campaign.sh);
  • the P10c switch-mechanism campaign (run-p10c-mechanism-campaign.sh): rate, switch-link PFC, DRR, WRR and WFQ;
  • Static Priority (run-sp-campaign.sh, with coverage);
  • TCP Reno and CUBIC (run-tcp-campaign.sh lean/fixtures/tcp, which builds its mutations);
  • the collective differential and budget and the AQM differential (below). The P10c AQM campaign (run-p10c-aqm-campaign.sh) runs in CI only inside the AQM differential, through the differential checker.
• Legacy certificates: the AQM, CUBIC, DRR and WFQ fixture and coverage scripts (run-aqm-fixtures.sh, run-aqm-coverage-fixtures.sh, run-cubic-fixtures.sh, run-drr-fixtures.sh, run-drr-coverage-fixtures.sh, run-wfq-fixtures.sh, run-wfq-coverage-fixtures.sh), on hand-written legacy-schema fixtures.

protocol-traces runs the legacy engine (days-legacy) on the configs/ci/ fixtures and the legacy checkers on its traces. It certifies Legacy Days only.

Where the Days AGO certificates come from

Every Days AGO certificate is the full-observation output of a Scalar run; device runs return no diagnostic planes, so no certificate comes from Metal or CUDA, and device identity rests on the byte-identity tests, not on certificates. Many of the committed accept fixtures are regenerated by a Rust test in CI's test job, which fails on any difference:

• tests/leanguard_certificates.rs lowers the scenarios in configs/leanguard/ through the Days AGO compiler (compile_config), writes the Scalar certificate, and requires a two-worker CPU run to write the same bytes: TCP Reno and CUBIC (tcp_reno.toml, tcp_cubic.toml: fan-in losses, fast recovery and timeouts), switch-link PFC (pfc_switch.toml), DRR, WRR, WFQ and SP (sched_*.toml), and WFQ under switch-link PFC (wfq_pfc.toml). It also resumes sched_wfq.toml and sched_sp.toml from a checkpoint with packets queued and in service, and the WFQ incast (wfq_incast.toml) from a checkpoint taken while a switch queue is paused. A WFQ certificate under PFC has its run's PFC certificate beside it (<name>.pfc.csv), which the campaign passes to the checker. It also writes the two AQM certificates of aqm_roce_acks.toml (an ECN step on a queue that RoCE ACKs share with data) and aqm_roce_acks_ramp.toml (the ramp), which pin that ACKs stay unmarked and that every data packet's decision follows the draw. The fixtures are lean/fixtures/tcp/*-compiled-*.csv, lean/fixtures/p10c/*_compiled_executor_accept.csv, the *_resumed_executor_accept.csv files and lean/fixtures/sp/sp_compiled_executor_accept.csv.
• Executor tests build images by hand for cases a scenario cannot reach directly: the adversarial TCP recovery, timeout and saturation traces (executor/tests/tcp_semantics.rs); the rate_executor_accept, pfc_executor_accept, drr_executor_accept and wrr_executor_accept certificates (rate_source.rs, pfc_semantics.rs, scalar_switch_schedulers.rs); and the aqm_executor_accept, aqm_ramp_executor_accept and aqm_ramp_byte_overflow_executor_accept AQM certificates (aqm_semantics.rs).
• The collective certificates are the Scalar traces of the scenarios in tests/collective_certificates.rs (the four P14 fixtures), tests/p16_collops.rs (collective_collops_*), tests/p16_collops_rail.rs (the rail fixtures among them) and tests/p16_hostafter.rs (collective_hostafter_*); tests/dcqcn_lowering.rs regenerates dcqcn_executor_trace_accept.csv.

The remaining accept fixtures are committed outputs that no Rust test regenerates: the roce_trace_*_executor_accept logs (Scalar runs of configs/p15/ and configs/p16/ scenarios, written by days-gpu tooling), the four collective_roce_*_executor_accept P15 traces, and the DCQCN queue-pair, tick-grid, coincident-prefix and CNP-join fixtures. The hand-written fixtures are wrr_wrap_after_saturated_class_accept.csv, the SP fixtures without compiled in their names, the roce_sender_* and roce_receiver_* fixtures, and the *_hand_* collective fixtures.

DAYS_UPDATE_LEANGUARD_FIXTURES=1 rewrites the TCP and compiled-scenario fixtures, DAYS_UPDATE_COLLECTIVE_TRACE_FIXTURES=1 the collective certificates, and DAYS_UPDATE_DCQCN_TRACE_FIXTURE=1 the DCQCN trace certificate.

Coverage by mechanism

The matrix lists what each Days AGO checker certifies, which certificates CI checks and where they come from, and the recorded limits. One limit is common to every row: a checker reads a certificate without the scenario, so a certificate that consistently rewrites every record of a run describes a different scenario and is accepted. Every CI step below is in .github/workflows/leanguard.yml and runs a script under lean/scripts/.

Remaining gaps:

• FIFO scheduling and constant traffic have no checker on either engine.
• Static Priority under PFC: sp_check has no pause model (see Days AGO WFQ and SP rows).
• AQM packet kind: p10c_aqm_check trusts each packet's kind; only a kind that changes between a packet's rows is rejected (see Days AGO AQM rows).
• WFQ timing: the wfq mode does not check completion times against serialization or service starts for work conservation (no link-busy model, no transmission time); it takes the run's event times as given, so the certificate holds only if they are correct.
• Two inputs the PFC rules and the WFQ PFC join do not check: a made-up PFC control row that names a controller and link the run does not have (the rules check the certificate's internal consistency, as the existing PFC rules always did), and a resumed queue's starting pause on a priority that no later control row names (inherent to certifying from a checkpoint).
• Rate sources: no scenario lowers a standalone rate generator (the compiler builds one only inside a DCQCN flow, whose rows p10c_dcqcn_check certifies), so the rate certificate comes from a hand-built image.
• Backends: certificates come from Scalar runs only (the configs/leanguard/ ones also require a two-worker CPU run to write the same bytes), because device runs return no diagnostic planes.
• Ungated roots in the collective certificate: see the Send/Recv and all-to-all rows above.
• The AQM certificate's packet kind is writer-trusted: see the ECN row above.

The P10c collective, DCQCN, RoCE and AQM checkers are linear in the row count, except the collective checker's TCP replay, which keeps a per-flow frontier in an ordered map and is n log n: per-flow, per-queue and per-stage state lives in hash maps, and no check searches earlier rows per row. Where P16 replaced such a search, the old list-scan functions stayed in a test-only module (lean/LeanGuard/P10c/Test/), and three lean-fixtures steps keep the two in agreement:

• run-p10c-collective-differential.sh and run-p10c-aqm-differential.sh run the shipped checker and the reference on every campaign fixture and on generated single-row mutants (p10c_collective_diff, p10c_aqm_diff in lean/lakefile.lean), and fail on any case where the two results differ;
• run-p10c-collective-budget.sh counts the shipped collective checker's small allocations (Lean heartbeats) across a size step of its fixtures and fails when the count grows faster than the rows allow, or when the shipped source contains a whole-trace list scan.

Exit codes and diagnostics

• 0: ACCEPT
• 1: REJECT: ..., including malformed certificate data
• 2: invalid command-line usage

Legacy checkers report failures in their canonical replay order, which may differ from physical CSV order. Days AGO diagnostics use the complete EventKey; p10c_dcqcn_check and p10c_roce_check additionally require the input rows to arrive in strictly increasing key order. A p10c_roce_check diagnostic names the log it refers to (sender:, receiver: or dcqcn:) in sender and trace modes.

Common rejection causes include malformed or out-of-domain integers, duplicate keys, parameter or state discontinuity, an illegal queue/protocol action, unmatched paired events, and a post-state that does not equal the executable reference update.