LeanGuard (Use Guide)
Emit legacy traces and run legacy or exact-executor Lean checkers.
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, includinglake.
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
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.tomlThe 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/binRe-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/binBy 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_aqm_check <path/to/aqm_events.csv>
./.lake/build/bin/p10c_dcqcn_check <path/to/dcqcn_events.csv>
./.lake/build/bin/p10c_collective_check <path/to/collective_events.csv>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_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/sp_check fixtures/sp/sp_priority_and_fifo_accept.csvThe 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.
Exit codes and diagnostics
0:ACCEPT1:REJECT: ..., including malformed certificate data2: 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 additionally
requires the input rows to arrive in strictly increasing key order.
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.