Days | Discrete-Event Network Simulation on Steroids

LeanGuard is a Lean 4 checker suite under lean/ that validates protocol traces emitted by Days. The workflow is:

Build Days with trace logging enabled (Cargo feature lean).
Run a simulation that emits *_events.csv into your log_path.
Run the corresponding Lean checker on that CSV.

Prerequisites

A working Lean 4 toolchain (via elan) and lake.
A working Rust toolchain (to build and run Days).

Days pins Lean via lean/lean-toolchain.

Emit traces from Days

Traces are written to your configured log_path (default: ./output/). See /docs/configuration/logging for log_path.

Days also writes a trace manifest at log_path/traces.json listing which *_events.csv traces are non-empty.

DCQCN (`dcqcn_events.csv`)

Build and run with DCQCN + trace logging enabled:

RUST_LOG=info cargo run --features dcqcn,lean,l2_pfc -- configs/dcqcn_simple.toml

This writes dcqcn_events.csv under log_path.

PFC (`pfc_events.csv`)

Build and run with PFC + trace logging enabled:

RUST_LOG=info cargo run --features l2_pfc,lean -- configs/pfc.toml

This writes pfc_events.csv under log_path.

TCP CUBIC (`cubic_events.csv`)

CUBIC event tracing is enabled by the lean feature:

RUST_LOG=info cargo run --features lean -- configs/simple.toml

If your scenario includes TCP flows using CUBIC, Days writes cubic_events.csv under log_path.

DRR (`drr_events.csv`)

DRR event tracing is enabled by the lean feature:

RUST_LOG=info cargo run --features lean -- configs/simple.toml

If your scenario includes a DRR scheduler, Days writes drr_events.csv under log_path.

WFQ (`wfq_events.csv`)

WFQ event tracing is enabled by the lean feature:

RUST_LOG=info cargo run --features lean -- configs/simple.toml

If your scenario includes a WFQ scheduler, Days writes wfq_events.csv under log_path.

Run everything with `leanguard-run`

To run Days and then the appropriate Lean checkers based on log_path/traces.json:

cd lean
lake build
cd ..
cargo run --bin leanguard-run -- --config configs/dcqcn_simple.toml --checker-dir lean/.lake/build/bin

To re-check an existing run directory without rerunning the simulator:

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

Build and run the Lean checkers

All checkers live under lean/ and are built with lake.

cd lean
lake build

Then run one of:

./.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>

Cross-layer (AQM → DCQCN causality):

./.lake/build/bin/aqm_dcqcn_check <path/to/aqm_events.csv> <path/to/dcqcn_events.csv>

Exit codes:

0: ACCEPT
1: REJECT: ... (first violating row + message)
2: usage / parse error

What “REJECT” means (and how to debug)

LeanGuard treats the simulator and the CSV as untrusted inputs. REJECT means at least one logged transition is not consistent with the executable Lean semantics.

Diagnostics are designed to be actionable:

parsing errors point at the CSV line and field
semantic errors point at the first failing row in canonical replay order (not necessarily the physical file order)

Typical causes:

missing required fields for an event kind
inconsistent constant parameters across rows for the same endpoint/flow
violated protocol gates (cooldowns / refresh intervals)
mismatched send/receive pairing (e.g., *_recv without prior *_sent)
post-state snapshot not equal to the state computed by the Lean update equations

LeanGuard (Use Guide)