leanguard-run

leanguard-run is the orchestration binary for trace-certificate checking:

• (optionally) runs Days on a config
• discovers which *_events.csv traces were produced
• runs the matching LeanGuard checker executables
• prints a machine-readable JSON summary to stdout

Source: days/src/bin/leanguard-run.rs

Basic usage

# Build the Lean checkers once
cd lean && lake build && cd ..

# Run simulation + checkers
cargo run --bin leanguard-run -- \
  --config configs/dcqcn_simple.toml \
  --checker-dir lean/.lake/build/bin

Re-check an existing run directory (no simulation rerun):

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

Flags

• --config <path> (required)
• --mode <simulate-and-check|check-only> (default: simulate-and-check)
• --checker-dir <path> (default: lean/.lake/build/bin)
• --allow-nondeterministic (default: false)
  • Refuses to run when the config contains threading = "multiple" unless this flag is set.
• --coverage (default: false)
  • Enable semantic coverage collection (if supported by the checker binaries).
• --coverage-dir <path> (optional)
  • If set (or if --coverage is set), leanguard-run writes per-checker coverage files under this directory.
  • Default when coverage is enabled: <log_path>/coverage/

When coverage is enabled, leanguard-run passes a --coverage-out <file> argument to each checker and reads the resulting JSON coverage list back into the final run summary (coverage.union and coverage.per_checker).

How traces are discovered

leanguard-run prefers the trace manifest written by Days at:

• <log_path>/traces.json

If the manifest is missing or invalid, it falls back to scanning for known filenames such as pfc_events.csv, dcqcn_events.csv, etc.

See /docs/reference/traces/manifest.

Output and exit codes

leanguard-run always prints a JSON document (RunSummaryV1) to stdout.

• exit code 0: overall accept=true
• exit code 1: accept=false (some checker rejected / simulation failed)

The JSON summary includes (among other fields):

• days: ok|panic|error|skipped
• checker_results[]: one entry per invoked checker
• coverage (optional)
• accept: final boolean

This makes it suitable for CI pipelines.