diff --git a/.gitignore b/.gitignore index d11ed3ff..8d333e4e 100644 --- a/.gitignore +++ b/.gitignore @@ -12,9 +12,23 @@ logs/** # RepoPrompt .repoprompt/** +# Python bytecode +**/__pycache__/ +**/*.pyc + # MkDocs build output site/** docs/site/** # Leanguard leanguard_corpus/** + +# Local toolchains / external jars (keep uncommitted) +tools/tla2tools.jar +tools/CommunityModules-deps.jar + +# TLC generated artifacts (manual runs) +tla/states/** + +# Paper draft is a separate repo and should not be committed here. +lean-paper/ diff --git a/configs/benchmarks/leanguard/drr_micro.toml b/configs/benchmarks/leanguard/drr_micro.toml new file mode 100644 index 00000000..076e4ec8 --- /dev/null +++ b/configs/benchmarks/leanguard/drr_micro.toml @@ -0,0 +1,39 @@ +# Micro benchmark for LeanGuard DRR/AQM trace checking. +# +# Similar to wfq_micro.toml, but uses Deficit Round Robin scheduling. + +seed = 42 +edges = [[0, 1]] +hosts = [0, 1] +duration = 0.5 +threading = "single" +log_path = "logs/bench/leanguard_drr_micro" +ui_interval = 1e9 + +[switch] + port_rate = 1000000000 # 1 Gbps + capacity = 1024 + weights = [1, 2] + discipline = "DRR" + drop = "TailDrop" + run_batch_size = 64 + +[[flow]] + flow_type = "PacketDistribution" + graph = [[0, 1]] + + [flow.traffic] + initial_delay = 0.0 + size = 1000000 + arr_dist = { type = "Uniform", low = 0.0001, high = 0.0001 } + pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } + +[[flow]] + flow_type = "PacketDistribution" + graph = [[0, 1]] + + [flow.traffic] + initial_delay = 0.0 + size = 1000000 + arr_dist = { type = "Uniform", low = 0.0001, high = 0.0001 } + pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } diff --git a/configs/benchmarks/leanguard/tcp_cubic_micro.toml b/configs/benchmarks/leanguard/tcp_cubic_micro.toml new file mode 100644 index 00000000..99fe0de9 --- /dev/null +++ b/configs/benchmarks/leanguard/tcp_cubic_micro.toml @@ -0,0 +1,35 @@ +# Micro benchmark for LeanGuard CUBIC/AQM trace checking. + +seed = 42 +edges = [[0, 1]] +hosts = [0, 1] +duration = 0.5 +threading = "single" +log_path = "logs/bench/leanguard_tcp_cubic_micro" +ui_interval = 1e9 + +[switch] + port_rate = 1000000000 # 1 Gbps + capacity = 1024 + weights = [1] + discipline = "FIFO" + drop = "TailDrop" + +[[flow]] + flow_type = "TCP" + graph = [[0, 1]] + routing = "ECMP" + + [flow.traffic] + initial_delay = 0.0 + size = 5000000 + arr_dist = { type = "Uniform", low = 0.0001, high = 0.0001 } + pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } + + [flow.traffic.tcp] + cc_algorithm = "CUBIC" + + [flow.traffic.tcp.cubic] + beta = 0.7 + c = 0.4 + fast_convergence = true diff --git a/configs/benchmarks/leanguard/wfq_micro.toml b/configs/benchmarks/leanguard/wfq_micro.toml new file mode 100644 index 00000000..f6fca2e5 --- /dev/null +++ b/configs/benchmarks/leanguard/wfq_micro.toml @@ -0,0 +1,39 @@ +# Micro benchmark for LeanGuard WFQ/AQM trace checking. +# +# Topology: two switches (0 and 1), each with a host attached, connected by one link. +# Traffic: two packet-distribution flows sharing the same output port so WFQ has real scheduling work. + +seed = 42 +edges = [[0, 1]] +hosts = [0, 1] +duration = 0.5 +threading = "single" +log_path = "logs/bench/leanguard_wfq_micro" +ui_interval = 1e9 + +[switch] + port_rate = 1000000000 # 1 Gbps + capacity = 1024 + weights = [1, 2] + discipline = "WFQ" + drop = "TailDrop" + +[[flow]] + flow_type = "PacketDistribution" + graph = [[0, 1]] + + [flow.traffic] + initial_delay = 0.0 + size = 1000000 + arr_dist = { type = "Uniform", low = 0.0001, high = 0.0001 } + pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } + +[[flow]] + flow_type = "PacketDistribution" + graph = [[0, 1]] + + [flow.traffic] + initial_delay = 0.0 + size = 1000000 + arr_dist = { type = "Uniform", low = 0.0001, high = 0.0001 } + pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } diff --git a/configs/cubic_simple.toml b/configs/cubic_simple.toml new file mode 100644 index 00000000..b2c8306c --- /dev/null +++ b/configs/cubic_simple.toml @@ -0,0 +1,31 @@ +# Simple TCP CUBIC example configuration (single flow, small transfer). + +seed = 1000 +edges = [[0, 1]] +hosts = [0, 1] +duration = 10.0 +log_path = "logs/cubic_simple" + +[switch] +port_rate = 4096 +capacity = 100 +weights = [1] +discipline = "FIFO" +drop = "RED" + +[link] +mode = "None" + +[[flow]] +flow_type = "TCP" +graph = [[0, 1]] +routing = "ECMP" + +[flow.traffic] +initial_delay = 0.0 +size = 3000 +arr_dist = { type = "Uniform", low = 1, high = 1 } +pkt_size_dist = { type = "DiscreteUniform", low = 512, high = 512 } + +[flow.traffic.tcp] +cc_algorithm = "CUBIC" diff --git a/configs/drr_simple.toml b/configs/drr_simple.toml new file mode 100644 index 00000000..3b96a5d2 --- /dev/null +++ b/configs/drr_simple.toml @@ -0,0 +1,37 @@ +# Simple DRR example configuration (two classes). + +seed = 42 +edges = [[0, 1]] +hosts = [0, 1] +duration = 0.2 +log_path = "logs/drr_simple" + +[switch] +port_rate = 10000000000 +capacity = 512 +weights = [1, 2] +discipline = "DRR" +drop = "TailDrop" + +[link] +mode = "None" + +[[flow]] +flow_type = "PacketDistribution" +graph = [[0, 1]] + +[flow.traffic] +initial_delay = 0.0 +size = 200000 +arr_dist = { type = "Uniform", low = 0.001, high = 0.001 } +pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } + +[[flow]] +flow_type = "PacketDistribution" +graph = [[0, 1]] + +[flow.traffic] +initial_delay = 0.0 +size = 200000 +arr_dist = { type = "Uniform", low = 0.001, high = 0.001 } +pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } diff --git a/configs/wfq_simple.toml b/configs/wfq_simple.toml new file mode 100644 index 00000000..12761347 --- /dev/null +++ b/configs/wfq_simple.toml @@ -0,0 +1,37 @@ +# Simple WFQ example configuration (two classes). + +seed = 42 +edges = [[0, 1]] +hosts = [0, 1] +duration = 0.2 +log_path = "logs/wfq_simple" + +[switch] +port_rate = 10000000000 +capacity = 512 +weights = [1, 2] +discipline = "WFQ" +drop = "TailDrop" + +[link] +mode = "None" + +[[flow]] +flow_type = "PacketDistribution" +graph = [[0, 1]] + +[flow.traffic] +initial_delay = 0.0 +size = 200000 +arr_dist = { type = "Uniform", low = 0.001, high = 0.001 } +pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } + +[[flow]] +flow_type = "PacketDistribution" +graph = [[0, 1]] + +[flow.traffic] +initial_delay = 0.0 +size = 200000 +arr_dist = { type = "Uniform", low = 0.001, high = 0.001 } +pkt_size_dist = { type = "DiscreteUniform", low = 1000, high = 1000 } diff --git a/ideas/benefits-over-tla.md b/ideas/benefits-over-tla.md index d71acc4f..c000134a 100644 --- a/ideas/benefits-over-tla.md +++ b/ideas/benefits-over-tla.md @@ -10,7 +10,7 @@ Here are the main benefits you should reasonably expect to see, and why they fol **LeanGuard expectation** -* Runtime is essentially **O(number of trace rows)**, with low constant factors, because each row is replayed once in a deterministic order and checked locally (including snapshot equality). +* Runtime is **O(n log n)** due to canonicalization (sorting by `(time_ns, event_id)`), plus **O(n)** deterministic replay with low constant factors (including snapshot equality). * This is exactly the “trace-certificate” design: the trace is intended to carry enough information (witnesses + post-state snapshots) so the checker doesn’t need to guess anything. **TLA+/TLC baseline expectation** @@ -26,6 +26,8 @@ Here are the main benefits you should reasonably expect to see, and why they fol * LeanGuard is likely to have **lower time/event** and **lower memory** for the same trace length when both are given the same information, especially on longer traces or many tests in CI. +*Concretely in this repo today (Jan 30, 2026, `task.md`):* with the replay-like TLC baseline (generated `TraceData.tla` + `INVARIANT ProgressOk`), TLC end-to-end time is roughly **40×–110×** the Lean checker time on most configs/protocols (e.g., DCQCN is ~**40×–50×** from 10k–100k events), with some specs exhibiting larger overhead (notably DRR in our current model). + ## 2) Better failure localization: first bad row vs model-checker counterexample **LeanGuard expectation** @@ -105,6 +107,7 @@ Here are the main benefits you should reasonably expect to see, and why they fol * TLA+ *can* model integer encodings well, but: * implementing fixed-point arithmetic and matching the logging conventions can be more awkward, + * practical TLC runs may require rescaling to fit TLC’s integer limits (and can therefore force small equality tolerances), * and TLC’s performance can suffer with heavy arithmetic on large integers/records if you’re not careful. **What you should see** @@ -199,4 +202,3 @@ If you implement a fair TLC baseline (same traces, same canonicalization, same p * **much easier integration with semantic coverage and coverage-guided test generation**. Those are exactly the dimensions your codebase (Days + `leanguard-run` + `leanguard-testgen`) is already structured to exploit. - diff --git a/ideas/comparison.md b/ideas/comparison.md index 0e2fba99..2c524c27 100644 --- a/ideas/comparison.md +++ b/ideas/comparison.md @@ -6,8 +6,8 @@ Below is a concrete “apples-to-apples” comparison plan for **LeanGuard vs a I’m going to treat the baseline as: -* **TLC-based trace validation** (the established TLA+ workflow), as described in the TLA+ trace-validation guidance and in recent research on trace validation with TLC. ([docs.tlapl.us][1]) -* And I’ll call out **TraceLink** as the “SOTA+” version of this line of work (automated mapping + causal-trace support), even if you don’t fully reimplement TraceLink for Days. ([fhackett.com][2]) +* **TLC-based trace validation** (the established TLA+ workflow), as described in the TLA+ trace-validation guidance and in recent research on trace validation with TLC. ([TLA+ trace validation guide][tla-trace-validation]) +* And I’ll call out **TraceLink** as the “SOTA+” version of this line of work (automated mapping + causal-trace support), even if you don’t fully reimplement TraceLink for Days. ([TraceLink][tracelink]) --- @@ -17,7 +17,7 @@ To keep the study fair, you want to control two big confounders: ### A. Equal information given to both checkers -LeanGuard’s checkers typically consume a trace row that already contains **the “witness” post-state snapshot** (e.g., alpha/rate/etc. in DCQCN). A lot of TLA+ trace-validation work can operate on *partial* traces and let TLC infer missing values (which changes both logging cost and checker power). ([conf.tlapl.us][3]) +LeanGuard’s checkers typically consume a trace row that already contains **the “witness” post-state snapshot** (e.g., alpha/rate/etc. in DCQCN). A lot of TLA+ trace-validation work can operate on *partial* traces and let TLC infer missing values (which changes both logging cost and checker power). ([Merz 2024 trace-validation slides][merz-trace-validation-slides]) So, define two modes, but make **Mode 1** the core “fair” one: @@ -39,20 +39,15 @@ TLC trace validation also consumes a **sequence** of steps, so you should: ### Baseline (recommended): **Manual TLC trace validation** -This is “classic” trace validation with TLA+/TLC: the trace is ingested, and TLC checks that each recorded step corresponds to a valid spec step (and optionally checks state equality against logged snapshots). This is exactly the “manual mapping” the TraceLink paper describes as the status quo in TLA+ trace validation priorandroid approachproduction.stüt - -[1]: https://docs.tlapl.us/using%3Atlc%3Atrace_validation?utm_source=chatgpt.com "using:tlc:trace_validation - TLA+ Wiki" -[2]: https://fhackett.com/files/oopsla25-tracelink.pdf "TraceLinking Implementations with Their Verified Designs" -[3]: https://conf.tlapl.us/2024-fm/slides-merz.pdf "Validating Traces of Distributed Systems Against [+]Specifications" - +This is “classic” trace validation with TLA+/TLC: the trace is ingested, and TLC checks that each recorded step corresponds to a valid spec step (and optionally checks state equality against logged snapshots). This is exactly the “manual mapping” the TraceLink paper describes as the status quo in TLA+ trace validation. It’s also aligned with the general “trace validation with TLC” workflow described on the TLA+ trace-validation guidance page. ### SOTA baseline (optional, if you want to claim “best known”): **TraceLink-style trace validation** -TraceLink is explicitly positioned as a **push-button** approach that “automatically maps a trace … to a formal model,” supports causal tracing / multiple in([docs.tlapl.us][1]) 2025. +TraceLink is explicitly positioned as a **push-button** approach that “automatically maps a trace … to a formal model,” and supports causal tracing / multiple interpretations. ([TraceLink][tracelink]) -But: TraceLink’s automation relies heavily on the PGo/MPCal toolchain integration, so for Days you’d likely be re-implementing *ideas* rather than using Tr([fhackett.com][2]) +But: TraceLink’s automation relies heavily on the PGo/MPCal toolchain integration, so for Days you’d likely be re-implementing *ideas* rather than using their tooling directly. For a LeanGuard paper comparison, I’d phrase it as: * **Primary baseline:** manual TLC trace validation (fair + portable) @@ -65,7 +60,7 @@ For a LeanGuard paper comparison, I’d phrase it as: ### Step 3.1 — A shared trace artifact and canonicalization pipeline **Input:** Days already produces `*_events.csv` (one per component/algorithm). -**Goa([conf.tlapl.us][3])canonical representation that both LeanGuard and TLC-based baseline will consume. +**Goal:** produce a canonical representation that both LeanGuard and the TLC-based baseline will consume. Concretely: @@ -74,18 +69,19 @@ Concretely: * Sort by `(time_ns, event_id)` * Check uniqueness (reject duplicates) -3. **Convert to TLC-friendly format** +3. **Convert to a TLC-friendly representation** - * The “standard” recent setup is **NDJSON** (one JSON object per line), because it plays well with TLC’s IO/JSON utilities shown in practical trace-validation setups. ([docs.tlapl.us][4]) + Some TLC builds used in trace-validation research can internalize JSON/NDJSON traces into **TLA+ values** (e.g., `Trace == ndJsonDeserialize(...)` via the `Json`/`IOUtils` modules). However, released `tla2tools.jar` versions do not reliably ship these modules, and TLC’s integer arithmetic is practically limited to 32-bit signed integers. In practice, a reproducible baseline often needs a generated trace module and (for Days) a rescaling step for large fields like `*_bps` and `*_ns`. -Example output line (NDJSON): + * **Option A (recommended for reproducibility):** export a generated `.tla` module (or a `.cfg` constant) that defines `Trace` as a sequence of records. + * **Option B (if your TLC build supports it):** export JSON/NDJSON (one object per row) and let TLC deserialize it (as in trace-validation research). ([trace validation paper][traceval-arxiv]) + +Example NDJSON line (Option B): ```json -{"time_ns":123456,"event_id":17,"kind":"CnpRecv","endpoint_id":0,"flow_id":1,"alpha_ppb":12000,"rate_bps":5000000000,"cnp_seen":true,"last_cnp_ns":123400,...} +{"time_ns":123456,"event_id":17,"kind":"cnp_recv","endpoint_id":0,"flow_id":1,"alpha_ppb":12000,"rate_bps":5000000000,"cnp_seen":true,"last_cnp_ns":123400} ``` -Why NDJSON? Because many TLC trace-validation “load trace” harnesses are built around deserializing JSON/NDJSON into a sequence of records. ([docs.tlapl.us][4]) - > Fairness note: This conversion is “infrastructure,” not advantage to either side, because both can consume the same canonicalized trace. --- @@ -99,7 +95,7 @@ Create a small reusable TLA+ module that: * at each step, reads `e == Trace[l]` and applies a spec action based on `e.kind` * increments `l` -This is the “generic setup” style demonstrated in practical TLA+ trace-validation material. ([docs.tlapl.us][4]) +This is the “generic setup” style demonstrated in practical TLA+ trace-validation material. ([TLA+ trace validation guide][tla-trace-validation]) Pseudo-skeleton (illustrative): @@ -174,7 +170,7 @@ A common pitfall is benchmarking TLC in a mode that’s not representative. If your trace-check harness is deterministic (Mode 1), TLC’s explored state-space is essentially O(length(trace)). -To keep TLC overhead reasonable, use recommended configuration tricks for trace validation (e.g., DFS queue optimizations) as documented in the TLA+ trace validation guidance. ([docs.tlapl.us][1]) +To keep TLC overhead reasonable, use recommended configuration tricks for trace validation (e.g., DFS queue optimizations) as documented in the TLA+ trace validation guidance. ([TLA+ trace validation guide][tla-trace-validation]) This matters because otherwise you’re measuring “TLC default queue behavior” more than “TLA+ trace validation as practiced.” @@ -245,7 +241,7 @@ If Days can produce nondeterministic ordering, measure: * without canonicalization, how fragile is each approach? * with canonicalization, do both become stable? -If you want to bring in TraceLink ideas here, TraceLink explicitly addresses causal tracing / multiple allowed interpretations. ([fhackett.com][2]) +If you want to bring in TraceLink ideas here, TraceLink explicitly addresses causal tracing / multiple allowed interpretations. ([TraceLink][tracelink]) But again: treat that as a “SOTA+” discussion unless you truly implement it. --- @@ -276,17 +272,12 @@ That directly compares: * LeanGuard’s executable checker approach * vs. TLC’s spec-based trace replay approach -…and avoids “TLA+ got an advantage because it didn’t require logging X” arguments. (You can still report that as a separate experiment, but don’t mix it into the main head-to-head.) ([conf.tlapl.us][3]) +…and avoids “TLA+ got an advantage because it didn’t require logging X” arguments. (You can still report that as a separate experiment, but don’t mix it into the main head-to-head.) ([Merz 2024 trace-validation slides][merz-trace-validation-slides]) --- If you want, I can turn the above into a concrete checklist keyed to your repo layout (e.g., “add `tla/` directory with `TraceHarness.tla`, add a `trace_convert` tool, add a `--baseline` flag to `leanguard-run` / `leanguard-testgen`, and define the JSON schema for baseline results”), but the core outline above is the conceptual minimum that makes the study fair and defensible. -[1]: https://docs.tlapl.us/using%3Atlc%3Atrace_validation?utm_source=chatgpt.com "using:tlc:trace_validation - TLA+ Wiki" -[2]: https://fhackett.com/files/oopsla25-tracelink.pdf "TraceLinking Implementations with Their Verified Designs" -[3]: https://conf.tlapl.us/2024-fm/slides-merz.pdf "Validating Traces of Distributed Systems Against [+]Specifications" -[4]: https://docs.tlapl.us/using%3Atlc%3Atrace_validation "using:tlc:trace_validation - TLA+ Wiki" - --- @@ -296,7 +287,7 @@ What is the classic trace validation with TLA+/TLC, how should it be implemented “TLA+/TLC trace validation” is the classic *model-based* way to check that a concrete execution produced by an implementation is consistent with a TLA+ spec—without proving the whole implementation correct. -It’s a good baseline to compare LeanGuard against because it’s the best-known “trusted checker over untrusted execution” workflow in the formal methods community, and it’s used in serious systems (e.g., Microsoft’s CCF). ([TLA+ Wiki][1]) +It’s a good baseline to compare LeanGuard against because it’s the best-known “trusted checker over untrusted execution” workflow in the formal methods community, and it’s used in serious systems (e.g., Microsoft’s CCF). ([TLA+ trace validation guide][tla-trace-validation]) Below is what it is (algorithmically), and how I’d implement it **specifically for Days** given your current trace + CLI architecture. @@ -317,7 +308,7 @@ You then build a *trace-constrained* TLA+ model (often called a **trace spec**) TLC then does *constrained exploration*: it attempts to find *some* behavior consistent with the trace. If it can, you accept the trace; if it cannot, it rejects (and can give a counterexample prefix / last consistent state). -This is exactly the philosophy you summarized in the paper’s generation section: checker is an oracle + diagnostics, and traces are certificates—except TLC can allow partial observation (missing variables, unknown internal actions), which turns checking into search. ([arXiv][2]) +This is exactly the philosophy you summarized in the paper’s generation section: checker is an oracle + diagnostics, and traces are certificates—except TLC can allow partial observation (missing variables, unknown internal actions), which turns checking into search. ([trace validation paper][traceval-arxiv]) ### What’s “classic” about it @@ -333,14 +324,14 @@ Two “classic” patterns exist: * unobserved internal actions / stuttering steps, * and sometimes different action interleavings. -This is powerful but can explode combinatorially if the trace is too “thin”; the literature explicitly warns that “less information in the trace increases nondeterminism and may lead to combinatorial explosion,” and recommends strategies like **DFS bounded by the trace length** to find a matching behavior quickly. ([arXiv][2]) +This is powerful but can explode combinatorially if the trace is too “thin”; the literature explicitly warns that “less information in the trace increases nondeterminism and may lead to combinatorial explosion,” and recommends strategies like **DFS bounded by the trace length** to find a matching behavior quickly. ([trace validation paper][traceval-arxiv]) ### How TLC is used in trace validation There are two main operational setups: * **Encode the trace as a constant / sequence** in the TLC model, then model check a “TraceSpec” that walks through it (works but can be awkward/large). -* **Read the trace from a file (often NDJSON)** and validate it (this is how modern trace validation workflows are typically scripted in practice, including CCF). ([arXiv][2]) +* **Read the trace from a file** and internalize it into TLA+ values (often NDJSON via `ndJsonDeserialize` in some TLC builds), or fall back to generating a `TraceData.tla` module that defines `Trace == << ... >>`. ([trace validation paper][traceval-arxiv]) --- @@ -365,7 +356,7 @@ Add a parallel “baseline checker” path next to LeanGuard: ``` Days run → *_events.csv (+ traces.json) - → (export) → TLC trace input (NDJSON or TLA constants) + → (export) → TLC trace input (NDJSON) → TLC validates against TLA+ spec → JSON summary alongside LeanGuard results ``` @@ -399,7 +390,7 @@ Only constrain TLC using: * event names (`kind`), ids (`endpoint_id`, `flow_id`, …), and maybe a few key state vars, * let the rest of spec variables be inferred by TLC search. -This is “closer” to the general trace validation literature, but can become infeasible quickly unless traces are very informative (and for fairness you’d need to argue why you chose a given observation level). ([arXiv][2]) +This is “closer” to the general trace validation literature, but can become infeasible quickly unless traces are very informative (and for fairness you’d need to argue why you chose a given observation level). ([trace validation paper][traceval-arxiv]) **Recommendation for Days:** Start with Baseline A for a fair comparison and practical runtimes; optionally report Baseline B as a secondary experiment showing the tradeoff between trace richness and validator complexity. @@ -407,11 +398,12 @@ This is “closer” to the general trace validation literature, but can become ## Step 2: Define the trace format TLC will consume -### Use NDJSON (recommended) +TLC needs the trace represented as **TLA+ values** (records/sequences). NDJSON deserialization exists in some TLC builds used by trace-validation work, but it is not reliably available in released `tla2tools.jar` distributions, and TLC is practically limited to 32-bit integers. So pick either: -A common practice is **one JSON object per step**, and it aligns with existing trace validation tooling scripts. ([arXiv][2]) +* **Option A (recommended for reproducibility):** export a generated TLA module/config that defines `Trace == << ... >>` as a sequence of records. +* **Option B (if supported in your TLC build):** export JSON/NDJSON (one object per step) and let TLC deserialize it (e.g., via `ndJsonDeserialize`). ([trace validation paper][traceval-arxiv]) -For each Days trace row, emit a line like: +If you choose Option B, for each Days trace row emit something like: ```json { @@ -426,8 +418,8 @@ For each Days trace row, emit a line like: Notes: -* Keep **integer encodings** exactly as in LeanGuard traces (ppb, bps, ns). This avoids floating point differences and makes TLC comparisons exact. -* Preserve canonical order (sort by `(time_ns, event_id)` before emitting NDJSON), or emit in that order directly. +* If you use a released TLC jar, you may need to **rescale** large numeric fields (e.g., `*_bps`, `*_ns`) to fit TLC’s integer limits, and (depending on your scaling) allow small tolerances for snapshot equality. +* Preserve canonical order (sort by `(time_ns, event_id)` before exporting), or export in that order directly. ### Where to implement the exporter @@ -437,7 +429,7 @@ You have two choices: Pro: doesn’t touch simulation; easy to iterate. Con: adds a conversion step. -2. **Emit NDJSON directly** from the logger path when a `tlc_trace = true` config flag is set. +2. **Emit JSON/NDJSON directly** from the logger path when a `tlc_trace = true` config flag is set. Pro: simpler pipeline, fewer moving parts. Con: touches logger & feature gates. @@ -449,11 +441,11 @@ Given your existing CSV-based ecosystem (LeanGuard, plotting, etc.), I’d do ** You need a TLA+ module per trace family: -* `DCQCN.tla` (or `SpecDCQCN.tla`) -* `PFC.tla` -* `WFQ.tla` -* `DRR.tla` -* `AQM.tla` +* `DcqcnTrace.tla` (DCQCN baseline; in this repo it includes both the trace harness and the per-step reference semantics) +* `PfcTrace.tla` +* `WfqTrace.tla` +* `DrrTrace.tla` +* `AqmTrace.tla` * (optional) a cross-layer `AQM_DCQCN.tla` These specs are the baseline’s “reference semantics,” analogous to your Lean semantics. @@ -480,12 +472,18 @@ This is exactly the kind of “component-local state + global replay loop” str ## Step 4: Write the *trace wrapper* module (the heart of “trace validation”) -For each protocol, create a `TraceValidateX.tla` module that: +For each protocol, create a trace-validation module that: -1. Loads the trace (`Trace`) from NDJSON (or via a constant). +1. Loads the trace (`Trace`) via a generated TLA module/constant (and optionally via NDJSON ingestion if your TLC build supports it). 2. Introduces a trace pointer variable `i`. 3. Defines `Next` to enforce that the `i`‑th trace entry corresponds to a valid step of the spec. +In this repo, we currently keep this as **one module per protocol** (e.g., `tla/DcqcnTrace.tla`) plus a `.cfg` file +that sets `SPECIFICATION TraceSpec`, checks an explicit progress invariant (`INVARIANT ProgressOk`), and disables deadlock checking (`CHECK_DEADLOCK FALSE`). + +* **Acceptance:** TLC exits cleanly with no invariant violations (the trace can be replayed through the full length). +* **Rejection:** if the trace cannot advance at some step, TLC violates `ProgressOk` (meaning “before end-of-trace, `Next` must be enabled”) and returns a counterexample. For diagnostics, we still parse TLC’s reported depth/diameter to compute the longest matched prefix and map that back to a failing CSV row. + ### Skeleton (DCQCN example) At a high level: @@ -502,14 +500,14 @@ At a high level: * `TraceAccepted`: `i = Len(Trace) + 1` (or equivalent), meaning all steps were validated. -This is the standard “walk the trace and constrain `Next`” approach described in trace validation literature and practice. ([TLA+ Wiki][1]) +This is the standard “walk the trace and constrain `Next`” approach described in trace validation literature and practice. ([TLA+ trace validation guide][tla-trace-validation]) ### Handling “partial observation” if you want Baseline B Instead of equating the entire post-state, you only equate observed fields and let TLC infer the rest. But that’s where state explosion can happen, and you’ll want: * strong constraints (log more), -* and/or DFS bounded by trace length. ([arXiv][2]) +* and/or DFS bounded by trace length. ([trace validation paper][traceval-arxiv]) --- @@ -519,18 +517,19 @@ Instead of equating the entire post-state, you only equate observed fields and l Add flags like: -* `--baseline tlc` (or `--tlc-check`) +* `--tlc-check` * `--tlc-spec-dir tla/` (where the `.tla` files live) -* `--tlc-bin ` (TLC jar or `tlc2.TLC`) -* `--tlc-mode {full_snapshot, partial}` +* `--tlc-bin ` (optional; run a wrapper executable directly) +* `--tlc-jar ` (path to `tla2tools.jar`, if not using `--tlc-bin`) +* `--tlc-no-dfs` (disable the DFS queue optimization used for trace validation) Flow: 1. Existing `discover_traces(log_path)` gives you the list of trace CSVs (via manifest or scan). 2. For each trace type: - * convert its CSV → NDJSON - * invoke TLC with the correct `TraceValidate*.tla` module + * export its CSV → a generated `TraceData.tla` module (and optionally also export a lossless `*.ndjson` for diagnostics) + * invoke TLC with the correct `*.tla` module + `.cfg` model config in a workspace where `TraceData.tla` is visible 3. Record results in the same JSON summary schema you already output for LeanGuard checkers (Accept/Reject/Error + stdout/stderr). This keeps the “one entrypoint per scenario” design you already have with `leanguard-run`. @@ -543,14 +542,14 @@ Either is fine; Option 1 is less plumbing. ### How to run TLC in practice -CCF’s docs show a practical pattern: a wrapper script (`tlc.py`) that runs TLC with a specific trace file as input for validation. ([arXiv][2]) +CCF’s docs show a practical pattern: a wrapper script (`tlc.py`) that runs TLC with a specific trace file as input for validation. ([trace validation paper][traceval-arxiv]) For Days, you can do the equivalent: -* Have `leanguard-run` call something like: +* Have `leanguard-run` call something like (Option A / generated trace module): - * `java -cp tla2tools.jar tlc2.TLC -modelcheck ... TraceValidateDCQCN.tla` - * with the trace path passed as a constant or env var (depending on how you read NDJSON). + * `java -Dtlc2.tool.queue.IStateQueue=StateDeque -cp path/to/tla2tools.jar tlc2.TLC -config /DcqcnTrace.cfg /DcqcnTrace.tla` + * where `/` contains `DcqcnTrace.tla`, `DcqcnTrace.cfg`, and a generated `TraceData.tla`. * Parse TLC’s exit code / output to decide Accept vs Reject. --- @@ -559,7 +558,7 @@ For Days, you can do the equivalent: To be a fair comparison study, align the interfaces: -* **Same trace source:** the exact `*_events.csv` Days already emits (or a lossless NDJSON conversion of it). +* **Same trace source:** the exact `*_events.csv` Days already emits (canonicalized), with a single conversion step for the baseline (e.g., generate `TraceData.tla` for TLC, and optionally also export lossless NDJSON for diagnostics). * **Same canonicalization order:** use `(time_ns, event_id)` ordering before feeding to TLC (since LeanGuard canonicalizes too). * **Same notion of “acceptance”:** for Baseline A, acceptance means “every logged step matches the reference semantics and snapshot.” * **Same determinism discipline:** run with `threading="single"` for both baselines by default (you already enforce this in `leanguard-run` unless `--allow-nondeterministic`). @@ -576,11 +575,11 @@ To be a fair comparison study, align the interfaces: * missing/unobserved variables, * stuttering/internal actions, * nondeterminism due to partial logging, - * some degrees of concurrency/interleaving (especially when trace is an observation, not full state). ([TLA+ Wiki][1]) + * some degrees of concurrency/interleaving (especially when trace is an observation, not full state). ([TLA+ trace validation guide][tla-trace-validation]) ### Expected pain points (where LeanGuard will likely look better) -* If you log less than full state, TLC can blow up quickly; the literature explicitly documents state explosion as trace precision decreases. ([arXiv][2]) +* If you log less than full state, TLC can blow up quickly; the literature explicitly documents state explosion as trace precision decreases. ([trace validation paper][traceval-arxiv]) * Getting good diagnostics can be harder than a purpose-built “first failing row” replay checker, because TLC’s counterexamples are model-checking counterexamples (though you can structure them to point to the offending trace index). * Implementing protocol arithmetic carefully in TLA+ (fixed-point) is work you already did in Lean. @@ -590,7 +589,7 @@ To be a fair comparison study, align the interfaces: 1. Add `tla/` directory to the repo with: - * `SpecDCQCN.tla`, `TraceValidateDCQCN.tla`, etc. + * `DcqcnTrace.tla` + `DcqcnTrace.cfg` (and additional modules/configs for other protocols). 2. Add `src/bin/days-trace-export.rs` that: * reads `*_events.csv`, @@ -609,6 +608,7 @@ To be a fair comparison study, align the interfaces: If you want, I can also sketch what the **DCQCN trace wrapper** should look like in TLA+ in more detail (variables, action definitions, and exactly how to use the post-state snapshot fields you already log), but the blueprint above is the “classic TLC trace validation” story and the most direct way to implement it cleanly in Days. -[1]: https://docs.tlapl.us/using%3Atlc%3Atrace_validation "using:tlc:trace_validation - TLA+ Wiki" -[2]: https://arxiv.org/html/2404.16075v2 "Validating Traces of Distributed Programs Against \tlaplusSpecificationsThis work was partly supported by a grant from Oracle Corporation." - +[tla-trace-validation]: https://docs.tlapl.us/using%3Atlc%3Atrace_validation "using:tlc:trace_validation - TLA+ Wiki" +[tracelink]: https://fhackett.com/files/oopsla25-tracelink.pdf "TraceLinking Implementations with Their Verified Designs" +[merz-trace-validation-slides]: https://conf.tlapl.us/2024-fm/slides-merz.pdf "Validating Traces of Distributed Systems Against [+]Specifications" +[traceval-arxiv]: https://arxiv.org/html/2404.16075v2 "Validating Traces of Distributed Programs Against TLA+ Specifications" diff --git a/ideas/coverage-experiments-report.md b/ideas/coverage-experiments-report.md new file mode 100644 index 00000000..3eddd94c --- /dev/null +++ b/ideas/coverage-experiments-report.md @@ -0,0 +1,401 @@ +# Investigation: Coverage-guided test generation experiments feasible **now** (Phase 0 complete) + +## Summary +With Phase 0 plumbing completed (Lean checker coverpoints → `leanguard-run --coverage` → `leanguard-testgen` metadata + `global_coverage.json`), you can run **coverage-measured** and partially **goal-directed** experiments today: + +- Coverage growth and redundancy measurements under `fuzz` and `campaign`. +- A/B comparison of semantic coverpoints vs the `trace_signature` fallback (`--no-coverage`). +- DCQCN goal-directed campaigns with calibration loops (trace-analyzer-driven) to hit specific semantic coverpoints. +- Offline corpus minimization (select minimal subset of accepted cases preserving semantic coverage). +- Failing-case minimization (TOML shrinkers) evaluation across a set of rejects. + +Current limitations: `fuzz`/`campaign` **do not yet discard** redundant accepted cases based on coverage novelty (they only record novelty), accepted-case *config* minimization is not implemented, and targeted campaign logic is currently DCQCN-only. + +## Symptoms / Constraints +- Phase 0 fixed the silent failure mode where Lean JSON coverage blobs were interpreted as one “coverage point”, and ensured `leanguard-testgen` passes `--coverage` by default. +- Experiments must be runnable now (no new feature work). +- We want semantic coverage (`checker_coverpoints`) and corpus growth, plus automated minimization of failing cases. + +## Investigation Log + +### 2026-02-01 / Phase 1 — Initial assessment +**Hypothesis:** After Phase 0, semantic coverpoints should flow end-to-end and can drive experiments. +**Findings:** Confirmed that Phase 0 is implemented (see `ideas/coverage-plumbing.md`). +**Evidence:** `ideas/coverage-plumbing.md`. + +### 2026-02-01 / Phase 2 — RepoPrompt `context_builder` +**Hypothesis:** Testgen already stores coverage and global novelty; identify experiments and limitations. +**Findings:** `leanguard-testgen` produces per-case metadata including `coverage.mode/observed/novelty` and maintains `metadata/global_coverage.json`. Trace-signature fallback exists. +**Evidence:** `src/utils/testgen.rs`, `src/bin/leanguard-testgen.rs`, `src/bin/leanguard-run.rs`, `lean/LeanGuard/Shared/Coverage.lean`, `lean/LeanGuard/*EventLog.lean`. + +### 2026-02-01 / Phase 3 — Follow-up deep dives (chat_send) +**Hypothesis:** Maybe fuzz/campaign already discard redundant accepted cases. +**Findings:** No—today they keep all accepted cases; novelty is informational. +**Evidence:** `src/utils/testgen.rs` fuzz/campaign finalization paths; only `if accept && novelty=="new"` updates `global_coverage.json`. + +### 2026-02-01 / Phase 4 — Evidence gathering (manual code reading) +**Findings:** +- `CoverageInfo`: + - mode is `checker_coverpoints` if RunSummary contains coverage union, else `trace_signature` (hash of `kind` column sequence per trace file), else `stub`. + - novelty is computed only for accepted cases and only when a mutable global set is passed. +- `trace_signature` is computed via `DefaultHasher` over the `kind` column sequence using naive `split(',')` CSV parsing. +- `campaign` calibration loops are DCQCN-only and use the DCQCN trace analyzer (not semantic coverage) to decide knob adjustments. +- `minimize` only accepts failing cases (`accept=false`) and preserves only “still failing”. + +**Evidence:** +- `src/utils/testgen.rs`: + - `build_coverage_info` and `trace_signature_entries`. + - `hash_trace_kind_sequence`. + - `campaign_with_options` + `calibrate_dcqcn`. + - `minimize` shrinkers list. + +## What we can run right now (experiments) + +See the “Experiments” section below for commands and metrics. + +## Limitations / gotchas (important for interpreting results) +1. **Not truly coverage-guided generation yet**: coverage is measured and recorded; generation isn’t actively steered by global coverage (except DCQCN goal/calibration). +2. **Retention is not coverage-based**: redundant accepted cases are retained; you must do offline minimization/selection if you want a small CI corpus. +3. **Minimization is failing-only**: accepted-case minimization (preserve coverage while shrinking config) is not implemented. +4. **`trace_signature` is coarse and potentially noisy**: hashes only `kind` sequence; sensitive to row order; uses `DefaultHasher`. +5. **Coverage depends on building the right checkers**: if a checker is missing or does not emit coverage, `CoverageInfo.mode` will degrade. + +## Recommended experiments (detailed) + +### Experiment A — Coverage growth curve under `fuzz` +- Run fuzz with a fixed budget/seed and compute coverage growth over accepted cases. +- Primary metrics: coverage-union size vs accepted index; novelty rate; plateau point. + +### Experiment B — A/B: semantic coverpoints vs `trace_signature` +- Run identical fuzz budgets with and without `--coverage` (`--no-coverage` in testgen). +- Compare novelty rate and “coverage size” under the two modes. + +### Experiment C — DCQCN goal campaigns with calibration (on/off) +- Use `leanguard-testgen campaign --protocol dcqcn --goal --max-calibration-iters K`. +- Measure goal hit rate and calibration steps. + +### Experiment D — Offline corpus minimization (set-cover selection) +- Given an accepted corpus with semantic coverpoints, greedily select minimal accepted cases that preserve the same coverpoint union. + +### Experiment E — Failing-case minimization quality +- Sample rejected cases and run `leanguard-testgen minimize ...`. +- Metrics: config size reduction, iterations kept, and failure stability. + +### Experiment F — Coverage plumbing integrity / determinism check +- Verify end-to-end consistency across three layers: + - checker `--coverage-out` JSON + - `leanguard-run` RunSummary `.coverage.*` + - `leanguard-testgen` metadata `coverage.*` + + +--- + +## Experiments (commands + artifacts + metrics) + +### Common setup + +Build the Lean checkers: + +```bash +cd lean +lake build +cd .. + +# If some checker binaries are missing under lean/.lake/build/bin, build them explicitly: +# cd lean && lake build dcqcn_check aqm_check aqm_dcqcn_check pfc_check wfq_check drr_check cubic_check && cd .. +``` + +Build the CLIs with the features needed by the stock `configs/` seeds: + +```bash +cargo build --features lean,dcqcn,l2_pfc --bin leanguard-run --bin leanguard-testgen + +export LEANGUARD_RUN="$PWD/target/debug/leanguard-run" +export TG="$PWD/target/debug/leanguard-testgen" +``` + +Sanity check that `leanguard-run` produces coverage in its JSON summary: + +```bash +$LEANGUARD_RUN --config configs/dcqcn_simple.toml --checker-dir lean/.lake/build/bin --coverage | head +``` + +Expected: +- Summary JSON contains `.coverage.union` and `.coverage.per_checker`. +- Under the case’s `log_path`, coverage files exist at `logs/coverage/*_coverage.json`. + +Key artifact locations during testgen: +- Per-case logs: `/{accepted|rejected}//logs/` +- Per-case coverage files: `.../logs/coverage/_coverage.json` +- Per-case RunSummary: `.../run_summary.json` +- Per-case metadata (includes CoverageInfo): `/metadata/.json` +- Global coverage set: `/metadata/global_coverage.json` + +--- + +### Experiment 1 — Coverage growth curve (semantic coverpoints) under `fuzz` + +**Goal:** quantify semantic coverage growth vs case budget and measure redundancy. + +```bash +rm -rf leanguard_corpus_exp1 + +$TG --corpus-root leanguard_corpus_exp1 --leanguard-run "$LEANGUARD_RUN" seed-index configs + +$TG --corpus-root leanguard_corpus_exp1 --leanguard-run "$LEANGUARD_RUN" \ + fuzz --budget 200 --rng-seed 1 +``` + +**Metrics to compute:** +- `|global_coverage|` (size of `metadata/global_coverage.json.observed`) +- novelty rate among accepted cases: fraction with `metadata.coverage.novelty == "new"` +- growth curve: cumulative union size vs accepted-case index + +**Sanity checks:** +- In `metadata/.json`, ensure `coverage.mode == "checker_coverpoints"` and `coverage.observed` contains real semantic names (e.g. `cnp_apply`, `red_under_min`, `pause_assert`, ...). + +--- + +### Experiment 2 — A/B comparison: `checker_coverpoints` vs `trace_signature` fallback + +**Goal:** quantify how the fallback behaves vs real semantic coverpoints. + +```bash +rm -rf leanguard_corpus_cov leanguard_corpus_sig + +$TG --corpus-root leanguard_corpus_cov --leanguard-run "$LEANGUARD_RUN" seed-index configs +$TG --corpus-root leanguard_corpus_sig --leanguard-run "$LEANGUARD_RUN" seed-index configs + +# Semantic coverpoints (coverage enabled by default) +$TG --corpus-root leanguard_corpus_cov --leanguard-run "$LEANGUARD_RUN" \ + fuzz --budget 200 --rng-seed 1 + +# Force fallback: do NOT pass --coverage to leanguard-run +$TG --no-coverage --corpus-root leanguard_corpus_sig --leanguard-run "$LEANGUARD_RUN" \ + fuzz --budget 200 --rng-seed 1 +``` + +**Metrics:** +- coverage mode distribution (how often `checker_coverpoints` vs `trace_signature` vs `stub` appears) +- novelty rate and final coverage size under each mode +- stability: rerun with same `--rng-seed` and compare `global_coverage.json` and the accepted/rejected split + +**Notes / pitfalls:** +- `trace_signature` hashes only the CSV `kind` column sequence per trace file (`trace_kind_hash::`), so it is coarse and sensitive to row ordering. + +--- + +### Experiment 3 — DCQCN goal-directed campaigns: calibration OFF vs ON + +**Goal:** quantify whether the DCQCN calibration loop improves hit-rate for rare semantic coverpoints. + +Example goal set (from `lean/LeanGuard/DcqcnEventLog.lean`): +- `cnp_ignored_due_to_interval` +- `alpha_above_0p1` +- `alpha_below_0p1` +- `rate_clamped_min` +- `rate_clamped_max` + +Commands: + +```bash +rm -rf leanguard_corpus_dcqcn_cal0 leanguard_corpus_dcqcn_cal5 + +$TG --corpus-root leanguard_corpus_dcqcn_cal0 --leanguard-run "$LEANGUARD_RUN" seed-index configs +$TG --corpus-root leanguard_corpus_dcqcn_cal5 --leanguard-run "$LEANGUARD_RUN" seed-index configs + +# Calibration OFF +$TG --corpus-root leanguard_corpus_dcqcn_cal0 --leanguard-run "$LEANGUARD_RUN" \ + campaign --protocol dcqcn --budget 50 --rng-seed 1 \ + --goal cnp_ignored_due_to_interval --max-calibration-iters 0 + +# Calibration ON +$TG --corpus-root leanguard_corpus_dcqcn_cal5 --leanguard-run "$LEANGUARD_RUN" \ + campaign --protocol dcqcn --budget 50 --rng-seed 1 \ + --goal cnp_ignored_due_to_interval --max-calibration-iters 5 +``` + +**Metrics:** +- goal hit rate among accepted cases: fraction where `coverage.observed` contains the goal +- calibration effort: count of `Mutation::CalibrationStep` in `mutations.json` per case +- acceptance vs reject rate + +**Notes:** +- Goal satisfaction prefers semantic coverpoints from RunSummary; if absent, DCQCN falls back to the DCQCN CSV analyzer (`src/utils/testgen/dcqcn.rs`). + +--- + +### Experiment 4 — Offline corpus minimization (accepted cases), preserving semantic coverage + +**Goal:** produce a small “CI-friendly” accepted subset that preserves the same semantic coverpoint union. + +Prereq: run Experiment 1 or 3 to generate accepted cases with `checker_coverpoints`. + +Greedy set cover script (prints chosen case IDs): + +```bash +python3 - <<'PY' +import glob, json + +corpus="leanguard_corpus_exp1" +meta_dir=f"{corpus}/metadata" +paths=[p for p in glob.glob(meta_dir+"/*.json") if not p.endswith(("seeds_index.json","global_coverage.json"))] + +accepted=[] +universe=set() +for p in paths: + m=json.load(open(p)) + if not m.get("result",{}).get("accept",False): + continue + if m.get("coverage",{}).get("mode") != "checker_coverpoints": + continue + pts=set(m["coverage"]["observed"]) + if not pts: + continue + accepted.append((m["case_id"], pts)) + universe |= pts + +chosen=[] +covered=set() +remaining=accepted[:] +while covered != universe: + best=None + for cid, pts in remaining: + gain=len(pts - covered) + if best is None or gain > best[0]: + best=(gain, cid, pts) + if best is None or best[0]==0: + break + _, cid, pts = best + chosen.append(cid) + covered |= pts + remaining=[x for x in remaining if x[0]!=cid] + +print("universe_points", len(universe)) +print("chosen_cases", len(chosen)) +for cid in chosen: + print(cid) +PY +``` + +**Metrics:** +- compression ratio: `chosen_cases / total_accepted` +- verify preserved coverage by replaying only chosen cases into an empty corpus and comparing `global_coverage.json`. + +--- + +### Experiment 5 — Failing-case minimization (current shrinkers) + +**Goal:** measure how well the built-in TOML shrinkers reduce failing configs while keeping them failing. + +Workflow: + +1) Generate a corpus with rejects: + +```bash +rm -rf leanguard_corpus_fail +$TG --corpus-root leanguard_corpus_fail --leanguard-run "$LEANGUARD_RUN" seed-index configs +$TG --corpus-root leanguard_corpus_fail --leanguard-run "$LEANGUARD_RUN" fuzz --budget 1000 --rng-seed 1 +``` + +2) Pick a rejected case directory: + +```bash +ls leanguard_corpus_fail/rejected | head +``` + +3) Minimize it (works only for `accept=false` cases): + +```bash +$TG --corpus-root leanguard_corpus_fail --leanguard-run "$LEANGUARD_RUN" \ + minimize leanguard_corpus_fail/rejected/ --max-iters 25 + +# Re-run to confirm it still fails +$TG --corpus-root leanguard_corpus_fail --leanguard-run "$LEANGUARD_RUN" \ + replay leanguard_corpus_fail/rejected/ +``` + +**Metrics:** +- byte-size reduction of `config.toml` vs `config.orig.toml` +- number of shrink iterations kept (`minimize` summary) +- failure stability: same `days_error` or same rejecting checker (not guaranteed) + +**Notes / limitation:** +- `minimize` preserves only “still failing” (`accept=false`), not a specific failure signature. + +--- + +### Experiment 6 — Coverage plumbing integrity (3-layer consistency) + +**Goal:** ensure coverpoints are not silently garbage and are consistent across: +1) checker `--coverage-out` file +2) `leanguard-run` RunSummary JSON +3) `leanguard-testgen` metadata + +```bash +rm -rf leanguard_corpus_plumb +$TG --corpus-root leanguard_corpus_plumb --leanguard-run "$LEANGUARD_RUN" seed-index configs +$TG --corpus-root leanguard_corpus_plumb --leanguard-run "$LEANGUARD_RUN" fuzz --budget 1 --rng-seed 123 +``` + +Then inspect the generated case under `accepted/` or `rejected/`: +- `.../logs/coverage/_coverage.json` should be a JSON object with a `cover` array. +- `.../run_summary.json` should have `coverage.union`/`coverage.per_checker` reflecting those files. +- `metadata/.json` should have `coverage.mode == "checker_coverpoints"` and a sorted/deduped `coverage.observed`. + + +--- + +### Experiment 7 — Per-protocol coverpoint reachability (campaign as protocol-filtered fuzz) + +**Goal:** for each protocol, measure which semantic coverpoints are reachable with the current seeds + generic mutations. + +Even though only DCQCN has targeted mutations/calibration today, `campaign --protocol ` still: +- selects seeds tagged for that protocol, +- applies generic mutations, +- runs Days + checkers + coverage, +- records semantic coverpoints in metadata. + +Commands: + +```bash +for proto in aqm pfc wfq drr cubic; do + rm -rf "leanguard_corpus_${proto}" + $TG --corpus-root "leanguard_corpus_${proto}" --leanguard-run "$LEANGUARD_RUN" seed-index configs + $TG --corpus-root "leanguard_corpus_${proto}" --leanguard-run "$LEANGUARD_RUN" \ + campaign --protocol "$proto" --budget 200 --rng-seed 1 +done +``` + +Metrics: +- unique coverpoints per protocol corpus (union over accepted cases) +- coverage growth vs budget +- acceptance/reject/error rates + +Interpretation: +- This tells you which coverpoints are “easy” vs “hard” to hit with today’s config surface. +- Hard-to-hit coverpoints are candidates for future targeted mutators/calibrators (Phase 1+ work), but the reachability data itself is an experiment you can run now. + + +--- + +### Experiment 8 — Cost of enabling coverage (overhead) + +**Goal:** quantify runtime overhead of collecting semantic coverpoints (writing coverage sidecars + parsing them) vs disabling coverage. + +Method: +- Run identical `fuzz` budgets with and without `--coverage` (`--no-coverage`), and compare total wall-clock time. + +Example: + +```bash +/usr/bin/time -l $TG --corpus-root leanguard_corpus_timing_cov --leanguard-run "$LEANGUARD_RUN" \ + fuzz --budget 200 --rng-seed 1 + +/usr/bin/time -l $TG --no-coverage --corpus-root leanguard_corpus_timing_nocov --leanguard-run "$LEANGUARD_RUN" \ + fuzz --budget 200 --rng-seed 1 +``` + +Notes: +- This includes Days simulation time, checker time, and coverage file I/O. If you want just checker overhead, run `leanguard-run` directly on an existing log directory via `--mode check-only`. + diff --git a/ideas/coverage-plan.md b/ideas/coverage-plan.md new file mode 100644 index 00000000..a041e655 --- /dev/null +++ b/ideas/coverage-plan.md @@ -0,0 +1,175 @@ +# coverage-plan.md (reconstructed) + +> NOTE: This file was **reconstructed after accidental deletion**. It is a best-effort recovery based on the console snippet +> we still had, the conversation summary, and the current repo state. +> It may not match the original byte-for-byte, but it should capture the same intent and details. + +Phase 0 = (1) fix coverage ingestion in `leanguard-run`, and (2) ensure `leanguard-testgen` actually enables coverage so +semantic coverpoints flow into the corpus metadata. + +You currently have all the semantic coverpoints implemented in Lean, and all the coverage bookkeeping implemented in +Rust, but there are two plumbing breaks: + +- `leanguard-run` reads coverage as `Vec` or line-split, but Lean writes a JSON object with a `cover` field. +- `leanguard-testgen` never passes `--coverage` to `leanguard-run`. + +At the time this plan was written, plan mode was active, so the intent was to specify the exact edits required to +complete Phase 0 and add a regression test. + +--- + +## Phase 0.1 — Fix coverage ingestion in `leanguard-run` + +### File: `src/bin/leanguard-run.rs` + +#### Change A: import `Deserialize` + +Currently: + +```rust +use serde::Serialize; +``` + +Change to: + +```rust +use serde::{Deserialize, Serialize}; +``` + +#### Change B: parse Lean’s JSON object format in `read_coverage_points` + +At the bottom of the file, update coverage parsing to: + +1. Try parsing a Lean-style object: + +```json +{"checker":"dcqcn_check","accept":true,"cover":["cp_a","cp_b"],"stats":{"rows":123,"processed_rows":123}} +``` + +2. Fall back to a bare JSON array of strings. +3. Fall back to newline-separated points. +4. **Do not** treat `{...}` / `[...]` blobs as a single “coverage point” in the fallback. + +Canonical implementation sketch: + +```rust +fn read_coverage_points(path: &Path) -> Option> { + let content = fs::read_to_string(path).ok()?; + + #[derive(Debug, Deserialize)] + struct CoverageReportJson { + cover: Vec, + } + + if let Ok(mut report) = serde_json::from_str::(&content) { + report.cover.sort(); + report.cover.dedup(); + return Some(report.cover); + } + + if let Ok(mut points) = serde_json::from_str::>(&content) { + points.sort(); + points.dedup(); + return Some(points); + } + + let trimmed = content.trim_start(); + if trimmed.starts_with('{') || trimmed.starts_with('[') { + return None; + } + + let mut points = content + .lines() + .map(|line| line.trim()) + .filter(|line| !line.is_empty()) + .map(|line| line.to_string()) + .collect::>(); + if points.is_empty() { + return None; + } + points.sort(); + points.dedup(); + Some(points) +} +``` + +--- + +## Phase 0.2 — Ensure `leanguard-testgen` enables coverage + +### File: `src/utils/testgen.rs` + +#### Change A: add a switch to the options struct + +```rust +pub struct TestGenOptions { + // ... + pub coverage: bool, + // ... +} +``` + +#### Change B: thread coverage into `run_leanguard(...)` + +- Add a `coverage: bool` argument to `run_leanguard(...)`. +- When `coverage == true`, include `--coverage` when invoking `leanguard-run`. + +```rust +if coverage { + cmd.arg("--coverage"); +} +``` + +- Update all call sites (fuzz, campaign loop, replay, minimize, etc.) to pass `opts.coverage`. + +### File: `src/bin/leanguard-testgen.rs` + +#### Change A: add a CLI flag to disable coverage + +Default should be **coverage enabled**, with an escape hatch. + +Example: + +```rust +#[arg(long, default_value_t = false)] +no_coverage: bool, +``` + +Then: + +```rust +coverage: !cli.no_coverage, +``` + +--- + +## Phase 0.3 — Add a regression test + +### File: `tests/leanguard_run.rs` + +Add an integration test that: + +- Creates a stub checker script that accepts and writes a Lean-style JSON coverage object to the `--coverage-out` path. +- Runs `leanguard-run --mode check-only --coverage ...`. +- Asserts coverage is correctly surfaced: + - `coverage.union` contains `cp_a`, `cp_b`. + - `coverage.per_checker["dcqcn_check"]` contains the same. + - `checker_results[0].coverage` contains the same. + +--- + +## Phase 0.4 — Update existing testgen tests + +Any test constructing `TestGenOptions { ... }` must be updated to initialize the new `coverage` field. + +--- + +## After Phase 0 + +Once end-to-end coverpoints are flowing: + +- Run short fuzz/campaign trials and verify corpus metadata uses: + - `coverage.mode == "checker_coverpoints"` + - `coverage.observed` grows over time +- Only then proceed to Phase 1/2 experiments (coverage-guided generation quality, corpus minimization while preserving + coverage, etc.). diff --git a/ideas/coverage-plumbing.md b/ideas/coverage-plumbing.md new file mode 100644 index 00000000..befb2b0d --- /dev/null +++ b/ideas/coverage-plumbing.md @@ -0,0 +1,54 @@ + Implemented Phase 0 end-to-end semantic coverage plumbing in ~/Playground/days: + + 1) `leanguard-run` now parses Lean coverage JSON correctly + + File: src/bin/leanguard-run.rs + + - read_coverage_points() now tries (in order): + 1. Lean CoverageReport JSON object: { "cover": ["cp1", ...], ... } + 2. Legacy JSON array: ["cp1", "cp2"] + 3. Fallback newline-separated points, but avoids treating {...} / [...] blobs as a single “point” + - Coverage points are sorted + deduped. + + 2) leanguard-testgen now actually enables coverage (by default) + + Files: src/utils/testgen.rs, src/bin/leanguard-testgen.rs + + - Added coverage: bool to TestGenOptions. + - run_leanguard(...) now takes a coverage: bool and passes --coverage to leanguard-run when enabled. + - All call sites now thread opts.coverage. + - leanguard-testgen CLI now has: + - --no-coverage (disables passing --coverage to leanguard-run) + - default behavior is coverage enabled (coverage: !cli.no_coverage) + + 3) Regression test added (prevents coverage JSON format regressions) + + File: tests/leanguard_run.rs + + - New integration test: leanguard_run_parses_lean_coverage_report_json + - Creates a stub checker that writes a Lean-style coverage JSON object to the --coverage-out path. + - Runs leanguard-run --coverage and asserts coverpoints appear in: + - coverage.union + - coverage.per_checker["dcqcn_check"] + - checker_results[0].coverage + + Also updated the existing testgen tests to include the new coverage field: + - tests/testgen_seed_index.rs + - tests/testgen_campaign_dcqcn.rs + + Verification + + Ran successfully: + - cargo fmt --all + - cargo test --features test -- --show-output + + How to use + + - Coverage-enabled by default: + - leanguard-testgen seed-index configs/ + - leanguard-testgen fuzz --budget 5 + - Disable if needed: + - leanguard-testgen --no-coverage fuzz --budget 5 + + Coverage should now flow Lean checker → coverage JSON file → leanguard-run summary JSON → testgen metadata/global + coverage tracking, enabling the follow-up coverage-guided experiments. diff --git a/ideas/coverage.md b/ideas/coverage.md new file mode 100644 index 00000000..8fd11086 --- /dev/null +++ b/ideas/coverage.md @@ -0,0 +1,109 @@ +# Investigation: Follow-up experiments — semantic coverpoints + coverage-guided corpus + shrinking (LeanGuard vs TLA+/TLC) + +## Summary + +LeanGuard already *implements* semantic coverpoints across protocols (in the Lean event logs) and can emit them as JSON, +and the Rust `leanguard-testgen` tool already has corpus/coverage bookkeeping. + +The main blocker to running the proposed “coverpoints + coverage-guided generation + shrinking” experiments was +*plumbing*: + +1. `leanguard-run` could not parse the Lean coverage JSON shape. +2. `leanguard-testgen` did not request coverage. + +Additionally, shrinking/minimization existed only for **failing configs** (and only at the TOML level), so +“CI-friendly corpus” (shrink **accepted** cases while preserving coverage) required a follow-up extension. + +## Symptoms + +- Semantic coverpoints exist in Lean, but they were not usable end-to-end by the generator. +- `leanguard-testgen` could not actually run in “semantic coverage guided” mode because it didn’t enable coverage. +- Existing minimization/shrinking is **failing-only**, and does **not** shrink accepted cases while preserving coverage + (which is what “CI-friendly corpus” needs). + +## Investigation Log + +### 2026-02-01 / Phase 2 (context_builder) — Testgen + coverage plumbing + +**Hypothesis:** Semantic coverpoints already exist; the generator is missing wiring. + +**Findings:** Confirmed. + +- Lean event logs already call `covHit` for protocol-specific coverpoints. +- Checkers accept `--coverage-out` and write a coverage report. +- Rust testgen already records/compares coverage, but couldn’t get correct points at the time. + +**Evidence:** + +- Lean coverage JSON format is an **object** (not `Vec`): + - `lean/LeanGuard/Shared/Coverage.lean` (`CoverageReport.toJson`) +- DCQCN coverpoints are implemented and named like the paper examples: + - `lean/LeanGuard/DcqcnEventLog.lean` (`recordCover` hits e.g. `cnp_apply`, `cnp_ignored_due_to_interval`, + `timer_with_cnp_seen`, `timer_without_cnp_seen`, `alpha_{below,above}_0p1`, `rate_clamped_{min,max}`, + `alpha_updated_nontrivial`, ...) +- Testgen prefers semantic coverpoints when present, else falls back: + - `src/utils/testgen.rs` (`build_coverage_info`, `goals_satisfied`) + +### 2026-02-01 / Phase 3 (deep dive) — Coverage format mismatch + +**Hypothesis:** `leanguard-run` can’t ingest Lean’s coverage JSON correctly. + +**Findings:** Confirmed. + +At the time: + +- `leanguard-run` only parsed `Vec` or line-split. +- Lean emits a single-line JSON **object**, so it was interpreted as one giant bogus “coverage point”. + +**Evidence:** + +- Lean JSON object schema: + - `lean/LeanGuard/Shared/Coverage.lean` (`CoverageReport.toJson` includes fields like `checker`, `accept`, + `cover:[...]`, `stats:{rows, processed_rows}`, optional `error`) +- `leanguard-run` parsing (pre-fix): + - `src/bin/leanguard-run.rs` `read_coverage_points` parsed `Vec` else `content.lines()` + +## Phase 0: required to unlock follow-up experiments + +Phase 0 was defined as: + +1. Parse the Lean coverage report JSON correctly in `leanguard-run`. +2. Make `leanguard-testgen` actually request coverage (`--coverage`) so coverpoints flow into: + - `leanguard-run` JSON summaries (`coverage.union` / `coverage.per_checker`) + - corpus metadata (`leanguard_corpus/metadata/*.json`) + - global novelty tracking (`global_coverage.json`) + +A dedicated regression test is important because the failure mode is silent (coverage “works” but is garbage). + +## Follow-up experiment ideas (post-Phase-0) + +Once semantic coverpoints flow end-to-end, the experiments become practical: + +1. **Coverage growth curves** + - Run `leanguard-testgen fuzz` for a fixed budget. + - Track |coverage| over accepted cases. + - Compare: + - `checker_coverpoints` vs `trace_signature` fallback + +2. **Corpus quality / CI-friendly corpus** + - Define a target coverage set (union over a run). + - Try to minimize the *set of configs* while preserving that coverage. + - This requires an “accepted-case minimizer” (distinct from failing-only shrinker). + +3. **Goal-directed campaigns** + - Use `leanguard-testgen campaign --protocol dcqcn --goal ...` (goal coverpoints) + - Measure success rate/time-to-hit goal points. + +4. **TLC-in-the-loop baseline (oracle cost comparison, not coverage-guided)** + - TLC is viable as an ACCEPT/REJECT oracle for trace validation. + - But TLC is not a practical inner-loop *coverage sensor* (too expensive, no semantic coverpoints). + +## Known limitation: shrinking + +Current `minimize` assumes a failing case: + +- `"Case is already accepted; minimize expects a failing case."` + +For “CI-friendly corpus”, a different workflow is needed: + +- Shrink accepted configs while preserving a desired coverage set, and/or while keeping acceptance. diff --git a/ideas/formal-verification.md b/ideas/formal-verification.md index bb693888..62e933c5 100644 --- a/ideas/formal-verification.md +++ b/ideas/formal-verification.md @@ -14,14 +14,14 @@ Yes—in principle you can verify “RFC compliance” in Lean, but there’s no What’s more common in the literature (non-Lean) - - Refinement-based verification of protocol implementations (e.g., IronFleet in Dafny). (microsoft.com (https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/?utm_source=openai)) - - Coq frameworks for verified distributed systems (e.g., Verdi). (github.com (https://github.com/uwplse/verdi?utm_source=openai)) - - Automated noncompliance finding via learned models / blackbox checking (common for real protocol stacks; e.g., QUICtester, Prognosis). (arxiv.org (https://arxiv.org/abs/2505.12690?utm_source=openai)) + - Refinement-based verification of protocol implementations (e.g., IronFleet in Dafny). (microsoft.com (https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/)) + - Coq frameworks for verified distributed systems (e.g., Verdi). (github.com (https://github.com/uwplse/verdi)) + - Automated noncompliance finding via learned models / blackbox checking (common for real protocol stacks; e.g., QUICtester, Prognosis). (arxiv.org (https://arxiv.org/abs/2505.12690)) How to proceed with your objective (Lean + Rust simulator) 1. Define “adheres to the RFC” precisely: usually either (a) trace refinement (“every observable behavior of the simulator is allowed by the spec”) or (b) a checklist of RFC “MUST/SHOULD” properties as invariants/temporal properties. - 2. Formalize the RFC subset you implement as a transition system in Lean (endpoints + network events). For ECN, this includes the IP ECN field behavior and TCP signaling/negotiation rules as you model them. (datatracker.ietf.org (https://datatracker.ietf.org/doc/html/rfc3168?utm_source=openai)) + 2. Formalize the RFC subset you implement as a transition system in Lean (endpoints + network events). For ECN, this includes the IP ECN field behavior and TCP signaling/negotiation rules as you model them. (datatracker.ietf.org (https://datatracker.ietf.org/doc/html/rfc3168)) 3. Prove compliance properties in Lean (invariants, and possibly liveness under explicit fairness assumptions). A practical workflow is “model check to find inductive invariants, then prove them in Lean,” as in the 2PC Lean work. (protocols-made-fun.com (https://protocols-made-fun.com/lean/2025/05/10/lean-two-phase-proofs.html)) 4. Connect Lean ↔ Rust via one of these realistic bridges: - Twin model + differential testing: keep a Lean executable spec and a Rust implementation; compare traces on randomized/bounded scenarios (good bug-finder; not a full proof). diff --git a/ideas/results.md b/ideas/results.md new file mode 100644 index 00000000..3d3113ea --- /dev/null +++ b/ideas/results.md @@ -0,0 +1,102 @@ +# Experiment results + +## Reproducing + +Prereqs: + +- Build LeanGuard checkers: `cd lean && lake build` (expects binaries under `lean/.lake/build/bin/`). +- Have TLC jar available (e.g. `/path/to/tla2tools.jar`) or set `TLA2TOOLS_JAR`. + +1) Generate (or regenerate) the trace logs used by the experiments. + +These configs write under their own `log_path` (see each TOML). **Important:** the CSV logger appends, so use a fresh `log_path` (or delete the old directory) if you want clean runs. + +```bash +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/dcqcn_simple.toml +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/dcqcn_multi.toml +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/dcqcn_1s.toml +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/dcqcn_2s.toml +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/dcqcn_10s.toml +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/pfc.toml +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/wfq_simple.toml +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/drr_simple.toml +cargo run --features lean,dcqcn,l2_pfc --bin days -- configs/cubic_simple.toml +``` + +2) Benchmark LeanGuard vs TLC: + +```bash +python3 utils/bench_leanguard_vs_tlc.py \ + --reps 5 \ + --checker-dir lean/.lake/build/bin \ + --tlc-jar /path/to/tla2tools.jar +``` + +3) Fault-injection agreement suite: + +```bash +python3 utils/fault_injection_agreement.py \ + --checker-dir lean/.lake/build/bin \ + --tlc-jar /path/to/tla2tools.jar +``` + +4) Export the latest JSON runs to Markdown + CSV: + +```bash +python3 utils/export_experiment_results.py --out-md ideas/results.md --out-dir logs +``` + +## Benchmarks (LeanGuard vs TLC) + +- Timestamp: `2026-01-30T16:21:24` +- Raw data: `logs/bench_leanguard_vs_tlc_2026-01-30.json` +- CSV (runs): `logs/bench_leanguard_vs_tlc_2026-01-30_runs.csv` +- CSV (summary): `logs/bench_leanguard_vs_tlc_2026-01-30_summary.csv` + +| Protocol | Config | Events | checker_ms | tlc_total_ms | tlc_cmd_ms | tlc_total/checker | TLC statuses | +|---|---|---:|---:|---:|---:|---:|---| +| aqm | configs/cubic_simple.toml | 12 | 9.8 ± 1.9 | 601.4 ± 16.4 | 597.8 ± 16.9 | 63.7 | accept | +| aqm | configs/dcqcn_10s.toml | 242 | 22.0 ± 9.6 | 663.2 ± 8.2 | 650.0 ± 7.8 | 46.5 | accept | +| aqm | configs/dcqcn_1s.toml | 242 | 6.6 ± 1.3 | 689.6 ± 22.6 | 676.8 ± 22.8 | 108.0 | accept | +| aqm | configs/dcqcn_2s.toml | 242 | 5.8 ± 1.3 | 664.8 ± 12.6 | 651.8 ± 12.6 | 118.6 | accept | +| aqm | configs/dcqcn_multi.toml | 1151 | 10.0 ± 2.1 | 871.6 ± 39.9 | 815.0 ± 39.2 | 89.8 | accept | +| aqm | configs/dcqcn_simple.toml | 242 | 14.2 ± 10.5 | 685.8 ± 72.9 | 670.2 ± 68.6 | 60.5 | accept | +| aqm | configs/drr_simple.toml | 400 | 9.2 ± 2.8 | 701.0 ± 18.5 | 678.6 ± 19.6 | 84.5 | accept | +| aqm | configs/pfc.toml | 4002 | 28.2 ± 8.6 | 1292.6 ± 10.5 | 1112.4 ± 11.0 | 49.5 | accept | +| aqm | configs/wfq_simple.toml | 400 | 9.2 ± 3.1 | 699.2 ± 11.8 | 676.8 ± 9.7 | 83.3 | accept | +| cubic | configs/cubic_simple.toml | 6 | 12.2 ± 8.9 | 694.8 ± 26.2 | 688.4 ± 25.2 | 73.2 | accept | +| dcqcn | configs/dcqcn_10s.toml | 100084 | 598.4 ± 15.3 | 25082.6 ± 1285.8 | 20251.0 ± 1304.6 | 42.0 | accept | +| dcqcn | configs/dcqcn_1s.toml | 10084 | 67.2 ± 9.0 | 2814.4 ± 132.1 | 2288.2 ± 121.6 | 42.4 | accept | +| dcqcn | configs/dcqcn_2s.toml | 20084 | 117.2 ± 2.4 | 4594.4 ± 76.1 | 3600.2 ± 79.4 | 39.2 | accept | +| dcqcn | configs/dcqcn_multi.toml | 4298 | 32.4 ± 3.4 | 1880.8 ± 66.8 | 1641.8 ± 62.7 | 58.5 | accept | +| dcqcn | configs/dcqcn_simple.toml | 2084 | 26.6 ± 10.2 | 1273.0 ± 36.1 | 1137.2 ± 37.0 | 52.3 | accept | +| drr | configs/drr_simple.toml | 800 | 14.8 ± 12.1 | 4502.6 ± 63.2 | 4442.0 ± 63.4 | 437.7 | accept | +| pfc | configs/pfc.toml | 104 | 14.2 ± 7.9 | 639.4 ± 10.2 | 626.8 ± 10.8 | 53.7 | accept | +| wfq | configs/wfq_simple.toml | 1200 | 16.8 ± 12.6 | 1594.2 ± 16.4 | 1526.2 ± 9.7 | 127.2 | accept | + +## Fault-injection agreement (LeanGuard vs TLC) + +- Timestamp: `2026-01-30T16:15:57` +- Raw data: `logs/fault_injection_agreement_2026-01-30.json` +- CSV: `logs/fault_injection_agreement_2026-01-30.csv` + +| Protocol | Case | Lean | TLC | Lean first failure | TLC first failure | +|---|---|---|---|---|---| +| aqm | accept_smoke | accept | accept | | | +| aqm | invalid_ecn_mark | reject | reject | line 2 (0,0,decision) | idx 1 (0,0,decision) | +| pfc | accept_smoke | accept | accept | | | +| pfc | pfc_recv_sender_mismatch | reject | reject | line 4 (256000000,2,pfc_recv) | idx 3 (256000000,2,pfc_recv) | +| dcqcn | accept_smoke | accept | accept | | | +| dcqcn | alpha_mismatch_first_row | reject | reject | line 2 (100000,0,timer_tick) | idx 1 (100000,0,timer_tick) | +| dcqcn | cnp_size_mismatch | reject | reject | line 11 (952000,9,cnp_sent) | idx 10 (952000,9,cnp_sent) | +| wfq | accept_smoke | accept | accept | | | +| wfq | finish_time_mismatch | reject | reject | line 3 (0,1,schedule) | idx 2 (0,1,schedule) | +| drr | accept_smoke | accept | accept | | | +| drr | deficit_mismatch | reject | reject | line 3 (0,1,schedule) | idx 2 (0,1,schedule) | +| cubic | accept_smoke | accept | accept | | | +| cubic | cwnd_mismatch | reject | reject | line 2 (1000000000,0,timeout) | idx 1 (1000000000,0,timeout) | + +## Notes / caveats + +- The TLC baseline for `CubicTrace.tla` is validated against `configs/cubic_simple.toml`. +- `configs/benchmarks/leanguard/tcp_cubic_micro.toml` currently produces a TLC **reject** for `CubicTrace.tla` (the fixed-point approximation drifts on longer traces), so it should not be used as an “accept” benchmark without adjusting either the config or the spec. diff --git a/ideas/task.md b/ideas/task.md new file mode 100644 index 00000000..773c9153 --- /dev/null +++ b/ideas/task.md @@ -0,0 +1,176 @@ +# Task Tracker: LeanGuard vs. TLC Baseline (Days) + +Last updated: 2026-01-30 + +This file tracks ongoing work to implement the comparison plan in `ideas/comparison.md` and to realize the expected outcomes in `ideas/benefits-over-tla.md`. + +## High-level goal + +Build a **TLA+/TLC trace-validation baseline** that consumes the **same Days traces** as LeanGuard (after the same canonicalization) and integrates into the existing workflow (`leanguard-run`, `leanguard-testgen`) so we can measure: + +- agreement/disagreement on ACCEPT/REJECT +- runtime + memory +- diagnostic quality (first failing step) +- engineering effort (spec + mapping + conversion) + +## Status + +### Done + +- Cleaned `ideas/comparison.md` to remove garbled text, consolidate references, and clarify trace ingestion options (generated TLA module vs JSON/NDJSON + loader). +- Updated `ideas/benefits-over-tla.md` to account for canonicalization cost (`O(n log n)` + replay `O(n)`). +- Removed `utm_source=...` URL artifacts from `ideas/formal-verification.md`. +- Added TLC baseline scaffolding: + - `src/utils/trace_export.rs`: + - lossless `*_events.csv` → `*.ndjson` export (canonicalized by `(time_ns, event_id)`), + - `*_events.csv` → generated `TraceData.tla` export (rescaled to fit TLC’s 32-bit integers), + - unit test that enforces “NDJSON is lossless, TLA trace is scaled”. + - `src/bin/days-trace-export.rs` exports either: + - `--format ndjson` (lossless), or + - `--format tla` (rescaled `TraceData.tla` module for TLC). + - Added protocol-specific TLC trace validators under `tla/` (one spec per `*_events.csv`): + - `tla/DcqcnTrace.tla` (DCQCN) + - `tla/AqmTrace.tla` (AQM) + - `tla/PfcTrace.tla` (PFC) + - `tla/WfqTrace.tla` (WFQ) + - `tla/DrrTrace.tla` (DRR) + - `tla/CubicTrace.tla` (TCP CUBIC; congestion-avoidance ACK growth via fixed-point approximation + small `cwnd_bytes` tolerance) +- Integrated TLC baseline runs into `src/bin/leanguard-run.rs`: + - Flags: `--tlc-check`, `--tlc-spec-dir`, `--tlc-bin`, `--tlc-jar`, `--tlc-no-dfs`. + - Added optional memory sampling: `--measure-rss` records `peak_rss_kb` for each checker and TLC run (polls `ps`, so keep off for timing benchmarks). + - Output: optional `tlc_results` and `tlc_accept` fields in the JSON summary. + - Diagnostics: parses TLC output (`Diameter:` / “depth of the complete state graph search”) to estimate the longest matched prefix, and reports the next failing NDJSON row (by `(time_ns,event_id,kind)` when present). + - Made TLC “reject” less heuristic: each baseline `.cfg` checks `INVARIANT ProgressOk` (“before end-of-trace, `Next` must be enabled”), so trace mismatch produces an explicit TLC counterexample/invariant violation (classified as `reject`). + - End-to-end verified: `configs/dcqcn_simple.toml` + TLC 2.19 (`/tmp/leanguard_refs/tla2tools_v1.7.4.jar`) produces `tlc_results[0].status = accept` and `matched_prefix == trace_len` on the shipped trace. +- Added a minimal fault-injection agreement suite: `python3 utils/fault_injection_agreement.py` (generates small corruptions per protocol and compares Lean vs TLC REJECT + first-failure key). + +### In progress + +- Broaden memory reporting: + - aggregate `peak_rss_kb` across protocols/configs for plots, + - optionally add JVM heap/GC telemetry (beyond RSS) if reviewers ask for it. + +### Next (implementation work) + +- Tighten/justify numeric tolerances (DCQCN `±1` scaled unit; CUBIC `CWND_BYTES_TOL`). +- Add a small “protocol baseline suite” doc section that explains which configs are representative for each protocol. + +## References to read (and what we need from them) + +### Core (TLA+/TLC trace validation) + +- [x] TLA+ trace validation guide (workflow + DFS queue setting + positioning). (`ideas/comparison.md` ref: `tla-trace-validation`) +- [x] Merz trace-validation slides (practical guidance + harness sketch). (`ideas/comparison.md` ref: `merz-trace-validation-slides`) +- [x] “Validating Traces of Distributed Programs Against TLA+ Specifications” (NDJSON ingestion, TraceSpec pattern, TraceAccepted condition). (`ideas/comparison.md` ref: `traceval-arxiv`) +- [x] “Verifying Software Traces Against a Formal Specification with TLA+ and TLC” (classic “trace as constraint” pattern). + +### Stretch / “SOTA+” positioning + +- [x] TraceLink paper (automation/mapping + causal trace validation; what we do *not* claim to reimplement). (`ideas/comparison.md` ref: `tracelink`) + +### Protocol / algorithm references (for step-semantics alignment) + +- [x] DCQCN SIGCOMM 2015 (“Congestion Control for Large-Scale RDMA Deployments”): confirm the RP/NP update equations and the intended parameters (`g`, `K`, rate increase phases). (Paper key equations match the Rust implementation order: update `alpha`, then apply multiplicative decrease using the updated `alpha`.) +- [x] WFQ (Demers/Keshav/Shenker): virtual finish tags `F_i = max(F_{i-1}, R(t_i)) + P_i` and “pick smallest finish tag” scheduling rule. +- [x] DRR (Shreedhar/Varghese): per-queue deficit counters, per-round quantum, and eligibility (`size <= deficit`) / counter update semantics. +- [x] CUBIC (RFC 8312): the sender-side cubic window growth function and state machine, as a stable reference for the variant implemented in Days. +- [x] RED / RED-ECN (Floyd/Jacobson 1993): average queue computation, min/max thresholds, and probability regions. + +### Additional references already mentioned in `ideas/` (may inform future phases) + +- [x] Lean 4 two-phase-commit proof writeup (inductive invariants workflow; uses Apalache to check inductiveness). +- [x] IronFleet (refinement-based verification and “prove practical distributed systems correct” framing). +- [x] Verdi (Coq distributed systems verification; plus related Raft proof work). +- [x] QUICtester / Prognosis (automated blackbox noncompliance checking via learned models). +- [x] RFC 3168 (ECN). + +## Open questions / decisions + +- **Baseline definition:** For the “fair” baseline, do we constrain TLC to a replay-like mode (post-state equality on every step), or do we also run a partial-observation mode as a secondary experiment? +- **Trace ingestion:** released `tla2tools.jar` (TLC) is practically constrained (32-bit integers; NDJSON ingestion modules are not reliably available). Current baseline uses generated `TraceData.tla` (rescaled) for reproducibility; NDJSON is retained losslessly for diagnostics only. +- **Diagnostics parity:** How exactly to map TLC failures to “first failing row” in the same terms LeanGuard reports (file, canonical index, `(time_ns, event_id)`, `kind`)? + +## Reference notes (actionable takeaways) + +- TLC trace validation commonly uses a reusable TLA module (often called `TraceSpec`) with: + - a trace constant/value `Trace`, + - a line counter `l`, + - and `Next` that reads `e == Trace[l]`, checks constraints, applies a step rule, and increments `l`. +- Deadlock checking is not helpful for trace validation; the baseline uses `CHECK_DEADLOCK FALSE`. +- For principled failure signaling, the baseline also checks `INVARIANT ProgressOk` (a state predicate using `ENABLED Next`) so “cannot advance the trace” becomes a standard TLC safety violation with a counterexample. +- Practical performance tip: run DFS for trace validation via: + - `JVM_OPTIONS=-Dtlc2.tool.queue.IStateQueue=StateDeque` + - (per the TLA+ trace-validation guide; `StateDeque` was added in Jan 2024). +- Trace validation supports partial observability (existential matching) but can blow up when traces are “thin”; for a fair LeanGuard baseline, we should primarily run a replay-like mode that constrains next-state values to match logged witness/snapshots. + +### Notes on current baseline compromises + +Because `TraceData.tla` is rescaled (to fit TLC’s integer limits), the DCQCN spec uses a small tolerance for snapshot equality on scaled `alpha_ppb` and `rate_bps` (currently `±1` in the scaled units). This is sufficient to make the TLC baseline agree on `dcqcn_simple.toml`; whether we can tighten this (or avoid it via different scaling) is an open question for the paper methodology. + +## Benchmark results (LeanGuard vs. TLC baseline) + +Timestamp: 2026-01-30 (local) + +Notes: + +- `checker_ms_mean±stdev` is the runtime of the LeanGuard checker process for the protocol (e.g., `dcqcn_check`, `wfq_check`). +- `tlc_total_ms_mean±stdev` is end-to-end TLC baseline time per run (export `TraceData.tla` + stage workspace + run TLC). +- `tlc_cmd_ms_mean±stdev` is just the TLC process runtime (excludes export/staging overhead). +- TLC runs include `INVARIANT ProgressOk` (uses `ENABLED Next`) to get principled REJECT counterexamples; this can noticeably increase TLC runtime for some specs (notably DRR). +- All runs below had `tlc_status = accept`. +- Raw per-run data (do not commit): `logs/bench_leanguard_vs_tlc_2026-01-30.json` +- To rerun: `python3 utils/bench_leanguard_vs_tlc.py --reps 5` +- To export to Markdown + CSV: `python3 utils/export_experiment_results.py --out-md ideas/results.md --out-dir logs` + +| Protocol | Config | Events | checker_ms (mean±stdev) | tlc_total_ms (mean±stdev) | tlc_cmd_ms (mean±stdev) | tlc_total / checker | +|---|---|---:|---:|---:|---:|---:| +| `aqm` | `configs/cubic_simple.toml` | 12 | 9.0 ± 0.7 | 610.0 ± 18.9 | 606.2 ± 19.1 | 68.2× | +| `aqm` | `configs/dcqcn_simple.toml` | 242 | 14.6 ± 12.6 | 708.4 ± 80.3 | 692.4 ± 74.8 | 67.2× | +| `aqm` | `configs/dcqcn_multi.toml` | 1,151 | 10.4 ± 2.3 | 940.2 ± 155.1 | 882.6 ± 155.7 | 94.5× | +| `aqm` | `configs/dcqcn_1s.toml` | 242 | 8.0 ± 1.0 | 675.0 ± 23.0 | 661.8 ± 23.4 | 85.6× | +| `aqm` | `configs/dcqcn_2s.toml` | 242 | 6.4 ± 1.1 | 682.8 ± 29.3 | 669.8 ± 29.3 | 109.3× | +| `aqm` | `configs/dcqcn_10s.toml` | 242 | 23.4 ± 9.2 | 687.8 ± 10.2 | 674.4 ± 10.4 | 39.6× | +| `aqm` | `configs/wfq_simple.toml` | 400 | 12.0 ± 1.7 | 721.4 ± 13.2 | 696.6 ± 12.6 | 61.5× | +| `aqm` | `configs/drr_simple.toml` | 400 | 10.0 ± 1.6 | 701.8 ± 13.6 | 677.4 ± 13.4 | 71.7× | +| `aqm` | `configs/pfc.toml` | 4,002 | 32.8 ± 5.7 | 1,288.4 ± 20.1 | 1,108.4 ± 17.4 | 40.2× | +| `dcqcn` | `configs/dcqcn_simple.toml` | 2,084 | 27.4 ± 9.0 | 1,269.6 ± 43.7 | 1,140.0 ± 40.4 | 49.4× | +| `dcqcn` | `configs/dcqcn_multi.toml` | 4,298 | 34.4 ± 3.0 | 1,857.6 ± 50.2 | 1,617.6 ± 51.6 | 54.2× | +| `dcqcn` | `configs/dcqcn_1s.toml` | 10,084 | 69.4 ± 9.0 | 2,838.6 ± 21.9 | 2,322.0 ± 24.3 | 41.4× | +| `dcqcn` | `configs/dcqcn_2s.toml` | 20,084 | 123.0 ± 4.8 | 4,951.6 ± 197.3 | 3,957.8 ± 198.9 | 40.3× | +| `dcqcn` | `configs/dcqcn_10s.toml` | 100,084 | 610.6 ± 17.0 | 30,278.8 ± 3,723.6 | 25,383.4 ± 3,667.9 | 49.6× | +| `pfc` | `configs/pfc.toml` | 104 | 23.4 ± 27.8 | 646.4 ± 15.6 | 635.2 ± 14.3 | 49.4× | +| `wfq` | `configs/wfq_simple.toml` | 1,200 | 26.8 ± 27.5 | 1,634.0 ± 34.9 | 1,570.6 ± 37.5 | 95.0× | +| `drr` | `configs/drr_simple.toml` | 800 | 15.6 ± 9.7 | 4,532.4 ± 85.2 | 4,470.0 ± 83.4 | 351.6× | +| `cubic` | `configs/cubic_simple.toml` | 6 | 21.4 ± 27.7 | 710.2 ± 16.5 | 703.6 ± 15.9 | 65.7× | + +## Fault-injection agreement (Lean vs. TLC) + +Timestamp: 2026-01-30 (local) + +We ran a small corruption suite across all 6 protocols using `python3 utils/fault_injection_agreement.py` (raw output: `logs/fault_injection_agreement_2026-01-30.json`). + +Results: + +- ACCEPT smoke tests: 6/6 agree on ACCEPT. +- Injected faults: 7/7 agree on REJECT, and the first-failure key `(time_ns,event_id)` matches for all cases. + +| Protocol | Case | Lean | TLC | First-failure key | +|---|---|---|---|---| +| `aqm` | invalid ECN mark | reject | reject | `(0,0)` | +| `pfc` | recv sender mismatch | reject | reject | `(256000000,2)` | +| `dcqcn` | alpha mismatch (first row) | reject | reject | `(100000,0)` | +| `dcqcn` | CNP size mismatch | reject | reject | `(952000,9)` | +| `wfq` | finish-time mismatch | reject | reject | `(0,1)` | +| `drr` | deficit mismatch | reject | reject | `(0,1)` | +| `cubic` | cwnd mismatch | reject | reject | `(1000000000,0)` | + +## Memory snapshots (peak RSS) + +These are sampled via `leanguard-run --measure-rss` (polls `ps`, so it adds overhead; treat as approximate). + +- `configs/dcqcn_simple.toml`: + - `dcqcn_check` peak RSS ≈ 10,624 KB + - `DcqcnTrace.tla` peak RSS ≈ 339,248 KB +- `configs/dcqcn_10s.toml`: + - `dcqcn_check` peak RSS ≈ 56,416 KB + - `DcqcnTrace.tla` peak RSS ≈ 3,142,112 KB diff --git a/ideas/testgen_ci_timings.md b/ideas/testgen_ci_timings.md new file mode 100644 index 00000000..00b0aca5 --- /dev/null +++ b/ideas/testgen_ci_timings.md @@ -0,0 +1,76 @@ +# Local “CI-style” test-generation timings (LeanPaper support) + +This note records a local run of the **test-generation pipeline** for multiple protocols so the paper (in `lean-paper/`) can cite/track end-to-end costs without relying on GitHub Actions. + +## What we are measuring + +For each target protocol we run the `leanguard-testgen` pipeline end-to-end: + +1. `leanguard-testgen seed-index` — index a seed TOML into a fresh corpus. +2. `leanguard-testgen campaign` — generate and execute `--budget` mutated cases. + - `campaign` invokes `leanguard-run` to run **Days simulation + LeanGuard checker(s)**. + - We use the default settings in `utils/ci_testgen_timings.py` (`--budget 1`, `--max-calibration-iters 0`). + +The per-protocol runner writes one CSV row with: +- `seed_index_s`, `campaign_s`, `total_s` (wall-clock seconds) +- `accepted/rejected/errors` (from the campaign summary) + +## Why this exists (relation to GitHub workflow) + +The GitHub Actions workflow `.github/workflows/testgen-timings.yml` runs the same per-protocol script in CI and uploads CSVs as artifacts. For LeanPaper work, we run the same steps locally to obtain CSVs without GitHub. + +## Commands (run locally) + +From repo root: + +1) Build LeanGuard checker binaries (all needed executables): + +```bash +cd lean +lake build dcqcn_check pfc_check cubic_check drr_check wfq_check aqm_check aqm_dcqcn_check +cd .. +``` + +2) Build the Rust runners used by test generation: + +```bash +cargo build --release --features lean,dcqcn,l2_pfc --bin leanguard-run --bin leanguard-testgen +``` + +3) Run all protocol “CI tests” locally (writes 1 CSV per protocol): + +```bash +mkdir -p artifacts +for p in aqm dcqcn pfc wfq drr cubic; do + python3 utils/ci_testgen_timings.py --protocol "$p" --out "artifacts/testgen_${p}.csv" +done +``` + +## This run (results + environment) + +- Git commit: `09caa054bce58096eeef7ead80f87b7a74aa56df` +- Toolchain: + - `rustc 1.92.0`, `cargo 1.92.0` + - `Python 3.12.7` + - `Lake 5.0.0` (Lean 4.26.0) + +### Output CSVs + +- `artifacts/testgen_aqm.csv` +- `artifacts/testgen_dcqcn.csv` +- `artifacts/testgen_pfc.csv` +- `artifacts/testgen_wfq.csv` +- `artifacts/testgen_drr.csv` +- `artifacts/testgen_cubic.csv` + +### Summary (latest row per CSV) + +| protocol | seed_config | seed_index_s | campaign_s | total_s | accepted | rejected | errors | +|---|---|---:|---:|---:|---:|---:|---:| +| aqm | `configs/simple.toml` | 0.16579 | 0.394072 | 0.559862 | 1 | 0 | 0 | +| dcqcn | `configs/dcqcn_simple.toml` | 0.003621 | 0.494983 | 0.498605 | 1 | 0 | 0 | +| pfc | `configs/pfc.toml` | 0.004261 | 0.295637 | 0.299898 | 1 | 0 | 0 | +| wfq | `configs/wfq_simple.toml` | 0.003482 | 0.432893 | 0.436374 | 1 | 0 | 0 | +| drr | `configs/drr_simple.toml` | 0.003481 | 0.264849 | 0.26833 | 1 | 0 | 0 | +| cubic | `configs/cubic_simple.toml` | 0.003608 | 0.241207 | 0.244815 | 1 | 0 | 0 | + diff --git a/ideas/tla-tlc-experiments.md b/ideas/tla-tlc-experiments.md new file mode 100644 index 00000000..9b791554 --- /dev/null +++ b/ideas/tla-tlc-experiments.md @@ -0,0 +1,187 @@ + 1) What’s in the current merge branch (Days repo) relevant to TLA+/TLC + + In /Users/bli/Playground/days the local branch merge tracks origin/merge and contains a complete TLC baseline + implementation and experiment harness. The main additions are: + + ### A. TLC baseline specs (tla/) + + A new tla/ directory with protocol-specific trace validators + configs: + + - tla/DcqcnTrace.tla + .cfg + - tla/AqmTrace.tla + .cfg + - tla/PfcTrace.tla + .cfg + - tla/WfqTrace.tla + .cfg + - tla/DrrTrace.tla + .cfg + - tla/CubicTrace.tla + .cfg + - tla/README.md explains how the baseline works and how to run it. + + Key design constraint (per tla/README.md): released TLC uses 32-bit integers, so the baseline avoids raw *_bps/*_ns + values and instead generates a scaled TraceData.tla. + + ### B. Trace export pipeline (CSV → NDJSON + TraceData.tla) + + New Rust utility code + a CLI tool: + + - src/utils/trace_export.rs (core conversion logic) + - src/bin/days-trace-export.rs (standalone exporter) + + Exports: + - *_events.csv → *_events.ndjson (lossless, canonicalized) + - *_events.csv → TraceData.tla (scaled for TLC) + + Scaling rules (from tla/README.md): + - *_ns stored in microseconds (ns/1_000) + - *_bps stored in 10 Mbps units (bps/10_000_000) + - *_ppb stored in permille (ppb/1_000_000) + + ### C. TLC integrated into the normal runner + + src/bin/leanguard-run.rs gains TLC integration (flags like --tlc-check, --tlc-jar, optional DFS control, and RSS + sampling). It stages a TLC workspace under: + /tlc//spec/ + + ### D. Experiment harness + result export scripts + + - utils/bench_leanguard_vs_tlc.py (benchmarks checker vs TLC across configs) + - utils/fault_injection_agreement.py (inject faults; compare ACCEPT/REJECT + first-failure key) + - utils/export_experiment_results.py (summaries to Markdown + CSV) + - task.md (acts as the “oracle” checklist: what’s implemented, how to run, and what to report) + + 2) “Consulting the oracle”: how to proceed to run the TLC experiments + + The branch itself spells out the intended workflow in two places: + + - tla/README.md = how the TLC baseline works + how to run it + - task.md = experiment plan + what results to extract/report + + Following that plan, the reproducible pipeline is: + + ### Step 0: Get TLC (tla2tools.jar) + + I downloaded TLC v1.7.4 to match the branch assumptions: + + ```bash + mkdir -p /tmp/leanguard_refs + curl -L -o /tmp/leanguard_refs/tla2tools_v1.7.4.jar \ + https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar + ``` + + ### Step 1: Build Days + Lean checkers + + ```bash + cd /Users/bli/Playground/days + cargo build --features lean,dcqcn,l2_pfc --bin days --bin leanguard-run --bin days-trace-export + + cd lean + lake build + # important: build these explicitly (lake build does not build all exes by default) + lake build pfc_check drr_check cubic_check + ``` + + ### Step 2: Generate fresh logs for the experiment configs + + Because the CSV logger appends, delete the old log directories first (or change log_path), then rerun: + + ```bash + cd /Users/bli/Playground/days + rm -rf logs/dcqcn_simple logs/dcqcn_multi logs/dcqcn_1s logs/dcqcn_2s logs/dcqcn_10s \ + logs/pfc logs/wfq_simple logs/drr_simple logs/cubic_simple + + for c in \ + configs/dcqcn_simple.toml configs/dcqcn_multi.toml configs/dcqcn_1s.toml \ + configs/dcqcn_2s.toml configs/dcqcn_10s.toml configs/pfc.toml \ + configs/wfq_simple.toml configs/drr_simple.toml configs/cubic_simple.toml + do + cargo run --quiet --features lean,dcqcn,l2_pfc --bin days -- "$c" + done + ``` + + ### Step 3: Run the benchmark suite (LeanGuard vs TLC) + + ```bash + cd /Users/bli/Playground/days + python3 utils/bench_leanguard_vs_tlc.py \ + --reps 5 \ + --checker-dir lean/.lake/build/bin \ + --tlc-jar /tmp/leanguard_refs/tla2tools_v1.7.4.jar + ``` + + ### Step 4: Run fault-injection agreement + + Important nuance: `utils/fault_injection_agreement.py` selects the smallest trace under `--logs-root`. If your `logs/` + contains many old fixtures, it may pick the wrong one. I ran it against a controlled directory: + + ```bash + cd /Users/bli/Playground/days + rm -rf logs_paper + mkdir -p logs_paper/{aqm_src,pfc_src,dcqcn_src,wfq_src,drr_src,cubic_src} + cp logs/dcqcn_simple/aqm_events.csv logs_paper/aqm_src/ + cp logs/pfc/pfc_events.csv logs_paper/pfc_src/ + cp logs/dcqcn_simple/dcqcn_events.csv logs_paper/dcqcn_src/ + cp logs/wfq_simple/wfq_events.csv logs_paper/wfq_src/ + cp logs/drr_simple/drr_events.csv logs_paper/drr_src/ + cp logs/cubic_simple/cubic_events.csv logs_paper/cubic_src/ + + python3 utils/fault_injection_agreement.py \ + --logs-root logs_paper \ + --checker-dir lean/.lake/build/bin \ + --tlc-jar /tmp/leanguard_refs/tla2tools_v1.7.4.jar + ``` + + ### Step 5: Export results + + ```bash + cd /Users/bli/Playground/days + python3 utils/export_experiment_results.py --out-md /tmp/results_2026-01-31.md --out-dir logs + ``` + + 3) The results I obtained (what to report) + + ### A. DCQCN: Lean vs TLC time (means over 5 runs) + + From the latest utils/bench_leanguard_vs_tlc.py run: + + - dcqcn_simple (2,084 rows): Lean 18 ms vs TLC 1,501 ms (~82×) + - dcqcn_10s (100,084 rows): Lean 711 ms vs TLC 23,800 ms (~34×) + + (Full table is now embedded into the paper; see next section.) + + ### B. Agreement + diagnostics (fault injection) + + On our controlled suite (AQM/PFC/DCQCN/WFQ/DRR/CUBIC), Lean and TLC: + + - agree on ACCEPT for the unmodified traces, + - agree on REJECT for 7 injected corruptions, + - and identify the same first-failing key (time_ns, event_id). + + ### C. Memory (peak RSS snapshots; approximate) + + Using target/debug/leanguard-run --measure-rss: + + - dcqcn_simple: TLC peak RSS ~ 0.4 GB + - dcqcn_10s (100k rows): TLC peak RSS ~ 7+ GB + + This matches the “oracle” expectation in task.md: TLC pays substantial overhead for explicit-state machinery even in + “replay-like” trace validation. + +4) Paper update: experimental results section written in `~/Playground/lean-paper` + + I updated: + + - `~/Playground/lean-paper/experiments.tex` + + by adding: + + - `\subsection{Comparison with TLA+/TLC trace validation}` (label sec:experiments:tlc) + - a new table `\label{tab:tlc}` containing the DCQCN Lean-vs-TLC timing results + - text describing: + - how the TLC baseline is constructed (generated TraceData.tla, scaling to avoid 32-bit overflow), + - deterministic replay + “must advance” invariant, + - agreement and first-failure parity, + - and memory overhead. + + I also ran make in `~/Playground/lean-paper` to ensure the draft builds successfully with the new section. + + If you want, I can also (a) wire the LaTeX table numbers directly from the generated CSV, or (b) tighten the wording to + better match whatever camera-ready space constraints you’re targeting (e.g., compress the methodology paragraph and + keep only the headline ratio + memory point). diff --git a/lean/LeanGuard/AqmDcqcnMain.lean b/lean/LeanGuard/AqmDcqcnMain.lean index 91e2df08..cfa9d06d 100644 --- a/lean/LeanGuard/AqmDcqcnMain.lean +++ b/lean/LeanGuard/AqmDcqcnMain.lean @@ -71,7 +71,9 @@ private def checkAll (aqmRows : List LeanGuard.AqmEventLog.Row) | .error (e, _) => throw e private def usage : String := - "usage: aqm_dcqcn_check [--coverage-out ] " + "usage:\n" + ++ " aqm_dcqcn_check [--coverage-out ] \n" + ++ " aqm_dcqcn_check --emit-coverpoint-catalog" def main (args : List String) : IO UInt32 := do match parseCoverageOut args with @@ -79,8 +81,18 @@ def main (args : List String) : IO UInt32 := do IO.eprintln usage pure 2 | .ok parsed => - match parsed.inputs with - | [aqmPath, dcqcnPath] => + if parsed.emitCoverpointCatalog then + let cat := + sortStrings + (LeanGuard.AqmEventLog.coverpointCatalog + ++ LeanGuard.DcqcnEventLog.coverpointCatalog) + |>.eraseDups + for cp in cat do + IO.println cp + pure 0 + else + match parsed.inputs with + | [aqmPath, dcqcnPath] => let aqmContent ← IO.FS.readFile aqmPath let dcqcnContent ← IO.FS.readFile dcqcnPath match LeanGuard.AqmEventLog.parseCsv aqmContent, @@ -167,6 +179,6 @@ def main (args : List String) : IO UInt32 := do | .error we => IO.eprintln we pure 2 - | _ => - IO.eprintln usage - pure 2 + | _ => + IO.eprintln usage + pure 2 diff --git a/lean/LeanGuard/AqmEventLog.lean b/lean/LeanGuard/AqmEventLog.lean index 02efa58b..973df1d1 100644 --- a/lean/LeanGuard/AqmEventLog.lean +++ b/lean/LeanGuard/AqmEventLog.lean @@ -298,4 +298,20 @@ def checkRows (rows : List Row) : Except String Unit := do | .ok _ => pure () | .error (e, _) => throw e + +/-- Enumerates all semantic coverpoints this checker may record via `covHit`. -/ +def coverpointCatalog : List String := + [ "ecn_threshold_drop_overflow" + , "ecn_threshold_mark" + , "ecn_threshold_pass" + , "mark_non_ecn_packet_drop" + , "red_between" + , "red_over_max" + , "red_should_drop" + , "red_should_mark" + , "red_under_min" + , "taildrop_enqueue" + , "taildrop_overflow_drop" + ] + end LeanGuard.AqmEventLog diff --git a/lean/LeanGuard/AqmMain.lean b/lean/LeanGuard/AqmMain.lean index 886a5434..459159de 100644 --- a/lean/LeanGuard/AqmMain.lean +++ b/lean/LeanGuard/AqmMain.lean @@ -6,7 +6,9 @@ open LeanGuard.AqmEventLog open LeanGuard.Shared def usage : String := - "usage: aqm_check [--coverage-out ] " + "usage:\n" + ++ " aqm_check [--coverage-out ] \n" + ++ " aqm_check --emit-coverpoint-catalog" def main (args : List String) : IO UInt32 := do match parseCoverageOut args with @@ -14,72 +16,77 @@ def main (args : List String) : IO UInt32 := do IO.eprintln usage pure 2 | .ok parsed => - match parsed.inputs with - | [path] => - let content ← IO.FS.readFile path - match parseCsv content with - | .error e => - let report : CoverageReport := - { checker := "aqm_check" - accept := false - cover := [] - rows := 0 - processedRows := 0 - error := some e } - match parsed.coverageOut with - | none => - IO.eprintln e - pure 2 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.eprintln e - pure 2 - | .error we => - IO.eprintln we - pure 2 - | .ok rows => - let rowCount := rows.length - match checkRowsWithCoverage rows with - | .ok cov => - let report : CoverageReport := - { checker := "aqm_check" - accept := true - cover := covList cov - rows := rowCount - processedRows := cov.processedRows } - match parsed.coverageOut with - | none => - IO.println "ACCEPT" - pure 0 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.println "ACCEPT" - pure 0 - | .error we => - IO.eprintln we - pure 2 - | .error (e, cov) => - let report : CoverageReport := - { checker := "aqm_check" - accept := false - cover := covList cov - rows := rowCount - processedRows := cov.processedRows - error := some e } - match parsed.coverageOut with - | none => - IO.eprintln s!"REJECT: {e}" - pure 1 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.eprintln s!"REJECT: {e}" - pure 1 - | .error we => - IO.eprintln we - pure 2 - | _ => - IO.eprintln usage - pure 2 + if parsed.emitCoverpointCatalog then + for cp in sortStrings coverpointCatalog do + IO.println cp + pure 0 + else + match parsed.inputs with + | [path] => + let content ← IO.FS.readFile path + match parseCsv content with + | .error e => + let report : CoverageReport := + { checker := "aqm_check" + accept := false + cover := [] + rows := 0 + processedRows := 0 + error := some e } + match parsed.coverageOut with + | none => + IO.eprintln e + pure 2 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.eprintln e + pure 2 + | .error we => + IO.eprintln we + pure 2 + | .ok rows => + let rowCount := rows.length + match checkRowsWithCoverage rows with + | .ok cov => + let report : CoverageReport := + { checker := "aqm_check" + accept := true + cover := covList cov + rows := rowCount + processedRows := cov.processedRows } + match parsed.coverageOut with + | none => + IO.println "ACCEPT" + pure 0 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.println "ACCEPT" + pure 0 + | .error we => + IO.eprintln we + pure 2 + | .error (e, cov) => + let report : CoverageReport := + { checker := "aqm_check" + accept := false + cover := covList cov + rows := rowCount + processedRows := cov.processedRows + error := some e } + match parsed.coverageOut with + | none => + IO.eprintln s!"REJECT: {e}" + pure 1 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.eprintln s!"REJECT: {e}" + pure 1 + | .error we => + IO.eprintln we + pure 2 + | _ => + IO.eprintln usage + pure 2 diff --git a/lean/LeanGuard/DcqcnEventLog.lean b/lean/LeanGuard/DcqcnEventLog.lean index 2976a86f..e30b07a2 100644 --- a/lean/LeanGuard/DcqcnEventLog.lean +++ b/lean/LeanGuard/DcqcnEventLog.lean @@ -419,6 +419,20 @@ def checkRows (rows : List Row) : Except String Unit := do | .ok _ => pure () | .error (e, _) => throw e + +/-- Enumerates all semantic coverpoints this checker may record via `covHit`. -/ +def coverpointCatalog : List String := + [ "alpha_above_0p1" + , "alpha_below_0p1" + , "alpha_updated_nontrivial" + , "cnp_apply" + , "cnp_ignored_due_to_interval" + , "rate_clamped_max" + , "rate_clamped_min" + , "timer_with_cnp_seen" + , "timer_without_cnp_seen" + ] + def dummyRow (timeNs eventId srcLine : Nat) : Row := { timeNs eventId diff --git a/lean/LeanGuard/Main.lean b/lean/LeanGuard/Main.lean index 728acd95..93790f48 100644 --- a/lean/LeanGuard/Main.lean +++ b/lean/LeanGuard/Main.lean @@ -6,7 +6,9 @@ open LeanGuard.DcqcnEventLog open LeanGuard.Shared def usage : String := - "usage: dcqcn_check [--coverage-out ] " + "usage:\n" + ++ " dcqcn_check [--coverage-out ] \n" + ++ " dcqcn_check --emit-coverpoint-catalog" def main (args : List String) : IO UInt32 := do match parseCoverageOut args with @@ -14,72 +16,77 @@ def main (args : List String) : IO UInt32 := do IO.eprintln usage pure 2 | .ok parsed => - match parsed.inputs with - | [path] => - let content ← IO.FS.readFile path - match parseCsv content with - | .error e => - let report : CoverageReport := - { checker := "dcqcn_check" - accept := false - cover := [] - rows := 0 - processedRows := 0 - error := some e } - match parsed.coverageOut with - | none => - IO.eprintln e - pure 2 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.eprintln e - pure 2 - | .error we => - IO.eprintln we - pure 2 - | .ok rows => - let rowCount := rows.length - match checkRowsWithCoverage rows with - | .ok cov => - let report : CoverageReport := - { checker := "dcqcn_check" - accept := true - cover := covList cov - rows := rowCount - processedRows := cov.processedRows } - match parsed.coverageOut with - | none => - IO.println "ACCEPT" - pure 0 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.println "ACCEPT" - pure 0 - | .error we => - IO.eprintln we - pure 2 - | .error (e, cov) => - let report : CoverageReport := - { checker := "dcqcn_check" - accept := false - cover := covList cov - rows := rowCount - processedRows := cov.processedRows - error := some e } - match parsed.coverageOut with - | none => - IO.eprintln s!"REJECT: {e}" - pure 1 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.eprintln s!"REJECT: {e}" - pure 1 - | .error we => - IO.eprintln we - pure 2 - | _ => - IO.eprintln usage - pure 2 + if parsed.emitCoverpointCatalog then + for cp in sortStrings coverpointCatalog do + IO.println cp + pure 0 + else + match parsed.inputs with + | [path] => + let content ← IO.FS.readFile path + match parseCsv content with + | .error e => + let report : CoverageReport := + { checker := "dcqcn_check" + accept := false + cover := [] + rows := 0 + processedRows := 0 + error := some e } + match parsed.coverageOut with + | none => + IO.eprintln e + pure 2 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.eprintln e + pure 2 + | .error we => + IO.eprintln we + pure 2 + | .ok rows => + let rowCount := rows.length + match checkRowsWithCoverage rows with + | .ok cov => + let report : CoverageReport := + { checker := "dcqcn_check" + accept := true + cover := covList cov + rows := rowCount + processedRows := cov.processedRows } + match parsed.coverageOut with + | none => + IO.println "ACCEPT" + pure 0 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.println "ACCEPT" + pure 0 + | .error we => + IO.eprintln we + pure 2 + | .error (e, cov) => + let report : CoverageReport := + { checker := "dcqcn_check" + accept := false + cover := covList cov + rows := rowCount + processedRows := cov.processedRows + error := some e } + match parsed.coverageOut with + | none => + IO.eprintln s!"REJECT: {e}" + pure 1 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.eprintln s!"REJECT: {e}" + pure 1 + | .error we => + IO.eprintln we + pure 2 + | _ => + IO.eprintln usage + pure 2 diff --git a/lean/LeanGuard/PfcEventLog.lean b/lean/LeanGuard/PfcEventLog.lean index 35551589..e6b74a04 100644 --- a/lean/LeanGuard/PfcEventLog.lean +++ b/lean/LeanGuard/PfcEventLog.lean @@ -187,4 +187,24 @@ def checkRows (rows : List Row) : Except String Unit := do | .ok _ => pure () | .error (e, _) => throw e + +/-- Enumerates all semantic coverpoints this checker may record via `covHit`. -/ +def coverpointCatalog : List String := + [ "occ_eq_xoff" + , "occ_eq_xon" + , "occ_gt_xoff" + , "occ_lt_xon" + , "pause_assert" + , "pause_refresh" + , "prio_0_seen" + , "prio_1_seen" + , "prio_2_seen" + , "prio_3_seen" + , "prio_4_seen" + , "prio_5_seen" + , "prio_6_seen" + , "prio_7_seen" + , "resume" + ] + end LeanGuard.PfcEventLog diff --git a/lean/LeanGuard/PfcMain.lean b/lean/LeanGuard/PfcMain.lean index fd5d68e2..7f605de3 100644 --- a/lean/LeanGuard/PfcMain.lean +++ b/lean/LeanGuard/PfcMain.lean @@ -6,7 +6,9 @@ open LeanGuard.PfcEventLog open LeanGuard.Shared def usage : String := - "usage: pfc_check [--coverage-out ] " + "usage:\n" + ++ " pfc_check [--coverage-out ] \n" + ++ " pfc_check --emit-coverpoint-catalog" def main (args : List String) : IO UInt32 := do match parseCoverageOut args with @@ -14,72 +16,77 @@ def main (args : List String) : IO UInt32 := do IO.eprintln usage pure 2 | .ok parsed => - match parsed.inputs with - | [path] => - let content ← IO.FS.readFile path - match parseCsv content with - | .error e => - let report : CoverageReport := - { checker := "pfc_check" - accept := false - cover := [] - rows := 0 - processedRows := 0 - error := some e } - match parsed.coverageOut with - | none => - IO.eprintln e - pure 2 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.eprintln e - pure 2 - | .error we => - IO.eprintln we - pure 2 - | .ok rows => - let rowCount := rows.length - match checkRowsWithCoverage rows with - | .ok cov => - let report : CoverageReport := - { checker := "pfc_check" - accept := true - cover := covList cov - rows := rowCount - processedRows := cov.processedRows } - match parsed.coverageOut with - | none => - IO.println "ACCEPT" - pure 0 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.println "ACCEPT" - pure 0 - | .error we => - IO.eprintln we - pure 2 - | .error (e, cov) => - let report : CoverageReport := - { checker := "pfc_check" - accept := false - cover := covList cov - rows := rowCount - processedRows := cov.processedRows - error := some e } - match parsed.coverageOut with - | none => - IO.eprintln s!"REJECT: {e}" - pure 1 - | some out => - match (← writeCoverageFile out report) with - | .ok _ => - IO.eprintln s!"REJECT: {e}" - pure 1 - | .error we => - IO.eprintln we - pure 2 - | _ => - IO.eprintln usage - pure 2 + if parsed.emitCoverpointCatalog then + for cp in sortStrings coverpointCatalog do + IO.println cp + pure 0 + else + match parsed.inputs with + | [path] => + let content ← IO.FS.readFile path + match parseCsv content with + | .error e => + let report : CoverageReport := + { checker := "pfc_check" + accept := false + cover := [] + rows := 0 + processedRows := 0 + error := some e } + match parsed.coverageOut with + | none => + IO.eprintln e + pure 2 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.eprintln e + pure 2 + | .error we => + IO.eprintln we + pure 2 + | .ok rows => + let rowCount := rows.length + match checkRowsWithCoverage rows with + | .ok cov => + let report : CoverageReport := + { checker := "pfc_check" + accept := true + cover := covList cov + rows := rowCount + processedRows := cov.processedRows } + match parsed.coverageOut with + | none => + IO.println "ACCEPT" + pure 0 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.println "ACCEPT" + pure 0 + | .error we => + IO.eprintln we + pure 2 + | .error (e, cov) => + let report : CoverageReport := + { checker := "pfc_check" + accept := false + cover := covList cov + rows := rowCount + processedRows := cov.processedRows + error := some e } + match parsed.coverageOut with + | none => + IO.eprintln s!"REJECT: {e}" + pure 1 + | some out => + match (← writeCoverageFile out report) with + | .ok _ => + IO.eprintln s!"REJECT: {e}" + pure 1 + | .error we => + IO.eprintln we + pure 2 + | _ => + IO.eprintln usage + pure 2 diff --git a/lean/LeanGuard/Shared/Cli.lean b/lean/LeanGuard/Shared/Cli.lean index 2511e1ac..32b3c209 100644 --- a/lean/LeanGuard/Shared/Cli.lean +++ b/lean/LeanGuard/Shared/Cli.lean @@ -4,6 +4,7 @@ namespace LeanGuard.Shared structure ParsedArgs where coverageOut : Option String := none + emitCoverpointCatalog : Bool := false inputs : List String := [] deriving Repr @@ -13,23 +14,34 @@ def parseCoverageOut (args : List String) : Except String ParsedArgs := do match s.toList with | '-' :: '-' :: _ => true | _ => false - let rec go (rest : List String) (cov : Option String) (inputsRev : List String) : - Except String ParsedArgs := do + + let rec go (rest : List String) (cov : Option String) (emitCatalog : Bool) + (inputsRev : List String) : Except String ParsedArgs := do match rest with | [] => - pure { coverageOut := cov, inputs := inputsRev.reverse } + pure { + coverageOut := cov + emitCoverpointCatalog := emitCatalog + inputs := inputsRev.reverse + } | "--coverage-out" :: tail => match tail with | [] => throw "missing path for --coverage-out" | path :: tail' => match cov with | some _ => throw "duplicate --coverage-out" - | none => go tail' (some path) inputsRev + | none => go tail' (some path) emitCatalog inputsRev + | "--emit-coverpoint-catalog" :: tail => + if emitCatalog then + throw "duplicate --emit-coverpoint-catalog" + else + go tail cov true inputsRev | arg :: tail => if startsWithDashDash arg then throw s!"unknown flag: {arg}" else - go tail cov (arg :: inputsRev) - go args none [] + go tail cov emitCatalog (arg :: inputsRev) + + go args none false [] end LeanGuard.Shared diff --git a/lean/LeanGuard/Shared/Coverage.lean b/lean/LeanGuard/Shared/Coverage.lean index 0c886fd9..8058c6ec 100644 --- a/lean/LeanGuard/Shared/Coverage.lean +++ b/lean/LeanGuard/Shared/Coverage.lean @@ -37,6 +37,10 @@ def stringLt (a b : String) : Bool := | Ordering.lt => true | _ => false +def sortStrings (xs : List String) : List String := + xs.toArray.qsort stringLt |>.toList + + def covList (cov : CoverageState) : List String := cov.points.toList.toArray.qsort stringLt |>.toList diff --git a/pyproject.toml b/pyproject.toml index d3c61e7f..b7a02dae 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,9 @@ [project] name = "days" version = "0.3.4" +dependencies = [ + "tomli>=2.4.0", +] [build-system] requires = ["maturin>=1.0,<2.0"] diff --git a/src/bin/days-trace-export.rs b/src/bin/days-trace-export.rs new file mode 100644 index 00000000..efa1cc48 --- /dev/null +++ b/src/bin/days-trace-export.rs @@ -0,0 +1,68 @@ +use clap::{Parser, ValueEnum}; +use std::path::PathBuf; + +#[derive(ValueEnum, Debug, Clone, Copy)] +enum ExportFormat { + /// Export as newline-delimited JSON (lossless). + Ndjson, + /// Export as a generated `.tla` module defining `Trace == << ... >>` (rescaled for TLC). + Tla, +} + +#[derive(Parser, Debug)] +#[command(name = "days-trace-export")] +struct Cli { + /// Input `*_events.csv` file produced by Days. + #[arg(long)] + input: PathBuf, + + /// Output file path. + /// + /// Defaults: + /// - `--format ndjson`: `--input` with extension replaced by `.ndjson` + /// - `--format tla`: `/.tla` + #[arg(long)] + output: Option, + + /// Export format. + #[arg(long, value_enum, default_value_t = ExportFormat::Ndjson)] + format: ExportFormat, + + /// TLA module name when `--format tla` is used. + #[arg(long, default_value = "TraceData")] + module_name: String, + + /// Disable canonical sorting by `(time_ns, event_id)` before exporting. + #[arg(long, default_value_t = false)] + no_sort: bool, +} + +fn main() { + let cli = Cli::parse(); + + let output = cli.output.unwrap_or_else(|| match cli.format { + ExportFormat::Ndjson => days::utils::trace_export::default_ndjson_output_path(&cli.input), + ExportFormat::Tla => cli + .input + .parent() + .unwrap_or_else(|| std::path::Path::new(".")) + .join(format!("{}.tla", cli.module_name)), + }); + + let result = match cli.format { + ExportFormat::Ndjson => { + days::utils::trace_export::export_csv_to_ndjson(&cli.input, &output, !cli.no_sort) + } + ExportFormat::Tla => days::utils::trace_export::export_csv_to_tla_trace_module( + &cli.input, + &output, + !cli.no_sort, + &cli.module_name, + ), + }; + + if let Err(e) = result { + eprintln!("{e}"); + std::process::exit(1); + } +} diff --git a/src/bin/leanguard-run.rs b/src/bin/leanguard-run.rs index e56c16da..eb015f7f 100644 --- a/src/bin/leanguard-run.rs +++ b/src/bin/leanguard-run.rs @@ -1,10 +1,18 @@ use clap::{Parser, ValueEnum}; -use serde::Serialize; +use serde::{Deserialize, Serialize}; use std::collections::{BTreeMap, BTreeSet}; -use std::fs; +use std::env; +use std::fs::{self, File}; +use std::io::BufRead; use std::path::{Path, PathBuf}; use std::process::Command; +use std::process::Stdio; +use std::sync::Arc; +use std::sync::atomic::{AtomicBool, Ordering}; +use std::time::Duration; +use std::time::Instant; +use days::utils::trace_export; use days::utils::trace_manifest::{self, TraceManifestV1}; #[derive(Debug, Clone, Copy, ValueEnum)] @@ -33,6 +41,38 @@ struct Cli { #[arg(long)] coverage_dir: Option, + + /// Run the TLA+/TLC trace-validation baseline (in addition to LeanGuard checkers). + #[arg(long, default_value_t = false)] + tlc_check: bool, + + /// If set, require TLC baseline acceptance in addition to LeanGuard checkers. + #[arg(long, default_value_t = false)] + require_tlc_accept: bool, + + /// Directory containing baseline `.tla` modules and `.cfg` model configs. + #[arg(long, default_value = "tla")] + tlc_spec_dir: PathBuf, + + /// Optional TLC runner executable. If provided, this binary is executed directly. + /// + /// If omitted, `leanguard-run` runs TLC via `java -cp tlc2.TLC ...`. + #[arg(long)] + tlc_bin: Option, + + /// Path to `tla2tools.jar` (required unless `--tlc-bin` is provided). + #[arg(long)] + tlc_jar: Option, + + /// Disable the DFS state queue optimization recommended for trace validation. + #[arg(long, default_value_t = false)] + tlc_no_dfs: bool, + + /// Sample peak RSS (KB) for checker and TLC subprocesses. + /// + /// This adds overhead (polling `ps`), so keep it off for performance benchmarks. + #[arg(long, default_value_t = false)] + measure_rss: bool, } #[derive(Debug, Clone, Serialize)] @@ -44,6 +84,50 @@ enum CheckerStatus { MissingChecker, } +#[derive(Debug, Clone, Serialize)] +#[serde(rename_all = "snake_case")] +enum TlcStatus { + Accept, + Reject, + Error, + MissingRunner, +} + +#[derive(Debug, Clone, Serialize)] +struct TlcFirstFailure { + trace_file: String, + index: u64, + time_ns: Option, + event_id: Option, + kind: Option, +} + +#[derive(Debug, Clone, Serialize)] +struct TlcResult { + module: String, + cfg: String, + trace_csv: String, + trace_ndjson: String, + trace_tla: String, + argv: Vec, + status: TlcStatus, + exit_code: Option, + stdout: String, + stderr: String, + #[serde(skip_serializing_if = "Option::is_none")] + runtime_ms: Option, + #[serde(skip_serializing_if = "Option::is_none")] + total_runtime_ms: Option, + #[serde(skip_serializing_if = "Option::is_none")] + diameter: Option, + #[serde(skip_serializing_if = "Option::is_none")] + matched_prefix: Option, + #[serde(skip_serializing_if = "Option::is_none")] + first_failure: Option, + #[serde(skip_serializing_if = "Option::is_none")] + peak_rss_kb: Option, +} + #[derive(Debug, Clone, Serialize)] struct CheckerResult { checker: String, @@ -53,6 +137,10 @@ struct CheckerResult { stdout: String, stderr: String, #[serde(skip_serializing_if = "Option::is_none")] + runtime_ms: Option, + #[serde(skip_serializing_if = "Option::is_none")] + peak_rss_kb: Option, + #[serde(skip_serializing_if = "Option::is_none")] coverage_path: Option, #[serde(skip_serializing_if = "Option::is_none")] coverage: Option>, @@ -100,6 +188,10 @@ struct RunSummaryV1 { trace_discovery: TraceDiscoverySummary, checker_results: Vec, #[serde(skip_serializing_if = "Option::is_none")] + tlc_results: Option>, + #[serde(skip_serializing_if = "Option::is_none")] + tlc_accept: Option, + #[serde(skip_serializing_if = "Option::is_none")] coverage: Option, accept: bool, } @@ -129,6 +221,8 @@ fn main() { traces: Vec::new(), }, checker_results: Vec::new(), + tlc_results: None, + tlc_accept: None, coverage: None, accept: false, }; @@ -249,9 +343,30 @@ fn main() { let invocations = select_checkers(&log_path, &summary.trace_discovery.traces); for inv in invocations { - summary - .checker_results - .push(run_checker(&cli.checker_dir, inv, coverage_dir.as_deref())); + summary.checker_results.push(run_checker( + &cli.checker_dir, + inv, + coverage_dir.as_deref(), + cli.measure_rss, + )); + } + + if cli.tlc_check { + let tlc_invocations = select_tlc_specs( + &log_path, + &summary.trace_discovery.traces, + &cli.tlc_spec_dir, + ); + let mut results = Vec::new(); + for inv in tlc_invocations { + results.push(run_tlc(&cli, &log_path, inv)); + } + summary.tlc_accept = Some( + results + .iter() + .all(|r| matches!(r.status, TlcStatus::Accept)), + ); + summary.tlc_results = Some(results); } summary.coverage = aggregate_coverage(&summary.checker_results); @@ -262,6 +377,9 @@ fn main() { .checker_results .iter() .all(|r| matches!(r.status, CheckerStatus::Accept)); + if summary.accept && cli.tlc_check && cli.require_tlc_accept { + summary.accept = summary.tlc_accept.unwrap_or(false); + } } let exit_code = if summary.accept { 0 } else { 1 }; @@ -381,10 +499,68 @@ fn select_checkers(log_path: &Path, traces: &[String]) -> Vec invocations } +#[derive(Debug, Clone)] +struct TlcInvocation { + module: PathBuf, + cfg: PathBuf, + trace_csv: PathBuf, +} + +fn select_tlc_specs(log_path: &Path, traces: &[String], spec_dir: &Path) -> Vec { + let has = |name: &str| traces.iter().any(|t| t == name); + let mut invocations = Vec::new(); + + if has("aqm_events.csv") { + invocations.push(TlcInvocation { + module: spec_dir.join("AqmTrace.tla"), + cfg: spec_dir.join("AqmTrace.cfg"), + trace_csv: log_path.join("aqm_events.csv"), + }); + } + if has("pfc_events.csv") { + invocations.push(TlcInvocation { + module: spec_dir.join("PfcTrace.tla"), + cfg: spec_dir.join("PfcTrace.cfg"), + trace_csv: log_path.join("pfc_events.csv"), + }); + } + if has("dcqcn_events.csv") { + invocations.push(TlcInvocation { + module: spec_dir.join("DcqcnTrace.tla"), + cfg: spec_dir.join("DcqcnTrace.cfg"), + trace_csv: log_path.join("dcqcn_events.csv"), + }); + } + if has("wfq_events.csv") { + invocations.push(TlcInvocation { + module: spec_dir.join("WfqTrace.tla"), + cfg: spec_dir.join("WfqTrace.cfg"), + trace_csv: log_path.join("wfq_events.csv"), + }); + } + if has("drr_events.csv") { + invocations.push(TlcInvocation { + module: spec_dir.join("DrrTrace.tla"), + cfg: spec_dir.join("DrrTrace.cfg"), + trace_csv: log_path.join("drr_events.csv"), + }); + } + if has("cubic_events.csv") { + invocations.push(TlcInvocation { + module: spec_dir.join("CubicTrace.tla"), + cfg: spec_dir.join("CubicTrace.cfg"), + trace_csv: log_path.join("cubic_events.csv"), + }); + } + + invocations +} + fn run_checker( checker_dir: &Path, inv: CheckerInvocation, coverage_dir: Option<&Path>, + measure_rss: bool, ) -> CheckerResult { let (exe, args) = match inv { CheckerInvocation::One { exe, args } => (exe, args), @@ -409,6 +585,8 @@ fn run_checker( exit_code: None, stdout: String::new(), stderr: format!("Missing checker binary: {}", exe_path.display()), + runtime_ms: None, + peak_rss_kb: None, coverage_path: coverage_path_str, coverage: None, }; @@ -419,9 +597,11 @@ fn run_checker( if let Some(path) = &coverage_path { cmd.arg("--coverage-out").arg(path); } - let output = cmd.output(); + let start = Instant::now(); + let output = run_command_with_peak_rss(&mut cmd, measure_rss); + let runtime_ms = start.elapsed().as_millis(); match output { - Ok(output) => { + Ok((output, peak_rss_kb)) => { let exit_code = output.status.code(); let stdout = String::from_utf8_lossy(&output.stdout).to_string(); let stderr = String::from_utf8_lossy(&output.stderr).to_string(); @@ -438,6 +618,8 @@ fn run_checker( exit_code, stdout, stderr, + runtime_ms: Some(runtime_ms), + peak_rss_kb, coverage_path: coverage_path_str, coverage: coverage_path .as_ref() @@ -451,19 +633,504 @@ fn run_checker( exit_code: None, stdout: String::new(), stderr: format!("Failed to execute checker: {e}"), + runtime_ms: Some(runtime_ms), + peak_rss_kb: None, coverage_path: coverage_path_str, coverage: None, }, } } +fn run_tlc(cli: &Cli, log_path: &Path, inv: TlcInvocation) -> TlcResult { + let start_total = Instant::now(); + let module_str = inv.module.display().to_string(); + let cfg_str = inv.cfg.display().to_string(); + let trace_csv_str = inv.trace_csv.display().to_string(); + + let trace_ndjson = trace_export::default_ndjson_output_path(&inv.trace_csv); + let trace_ndjson_str = trace_ndjson.display().to_string(); + + if let Err(e) = trace_export::export_csv_to_ndjson(&inv.trace_csv, &trace_ndjson, true) { + return TlcResult { + module: module_str, + cfg: cfg_str, + trace_csv: trace_csv_str, + trace_ndjson: trace_ndjson_str, + trace_tla: String::new(), + argv: Vec::new(), + status: TlcStatus::Error, + exit_code: None, + stdout: String::new(), + stderr: format!("Failed to export CSV to NDJSON: {e}"), + runtime_ms: None, + total_runtime_ms: Some(start_total.elapsed().as_millis()), + diameter: None, + matched_prefix: None, + first_failure: None, + peak_rss_kb: None, + }; + } + + let meta_root = match env::var_os("TLC_METADIR") { + Some(v) if !v.is_empty() => PathBuf::from(v), + _ => log_path.join("tlc"), + }; + let _ = fs::create_dir_all(&meta_root); + let meta_dir = meta_root.join( + inv.module + .file_stem() + .and_then(|s| s.to_str()) + .unwrap_or("tlc"), + ); + let _ = fs::create_dir_all(&meta_dir); + + let spec_dir = meta_dir.join("spec"); + let _ = fs::create_dir_all(&spec_dir); + + let module_file = spec_dir.join(Path::new( + inv.module + .file_name() + .expect("TLC module path has no filename"), + )); + let cfg_file = spec_dir.join(Path::new( + inv.cfg.file_name().expect("TLC cfg path has no filename"), + )); + let trace_tla = spec_dir.join("TraceData.tla"); + let trace_tla_str = trace_tla.display().to_string(); + + if let Err(e) = fs::copy(&inv.module, &module_file) { + return TlcResult { + module: module_str, + cfg: cfg_str, + trace_csv: trace_csv_str, + trace_ndjson: trace_ndjson_str, + trace_tla: trace_tla_str, + argv: Vec::new(), + status: TlcStatus::Error, + exit_code: None, + stdout: String::new(), + stderr: format!("Failed to copy TLA module into TLC workspace: {e}"), + runtime_ms: None, + total_runtime_ms: Some(start_total.elapsed().as_millis()), + diameter: None, + matched_prefix: None, + first_failure: None, + peak_rss_kb: None, + }; + } + if let Err(e) = fs::copy(&inv.cfg, &cfg_file) { + return TlcResult { + module: module_str, + cfg: cfg_str, + trace_csv: trace_csv_str, + trace_ndjson: trace_ndjson_str, + trace_tla: trace_tla_str, + argv: Vec::new(), + status: TlcStatus::Error, + exit_code: None, + stdout: String::new(), + stderr: format!("Failed to copy TLC config into workspace: {e}"), + runtime_ms: None, + total_runtime_ms: Some(start_total.elapsed().as_millis()), + diameter: None, + matched_prefix: None, + first_failure: None, + peak_rss_kb: None, + }; + } + if let Err(e) = + trace_export::export_csv_to_tla_trace_module(&inv.trace_csv, &trace_tla, true, "TraceData") + { + return TlcResult { + module: module_str, + cfg: cfg_str, + trace_csv: trace_csv_str, + trace_ndjson: trace_ndjson_str, + trace_tla: trace_tla_str, + argv: Vec::new(), + status: TlcStatus::Error, + exit_code: None, + stdout: String::new(), + stderr: format!("Failed to export CSV to TLA trace module: {e}"), + runtime_ms: None, + total_runtime_ms: Some(start_total.elapsed().as_millis()), + diameter: None, + matched_prefix: None, + first_failure: None, + peak_rss_kb: None, + }; + } + + let mut cmd = if let Some(bin) = &cli.tlc_bin { + Command::new(bin) + } else { + let jar = cli + .tlc_jar + .clone() + .or_else(|| env::var_os("TLA2TOOLS_JAR").map(PathBuf::from)); + let Some(jar) = jar.as_ref() else { + return TlcResult { + module: module_str, + cfg: cfg_str, + trace_csv: trace_csv_str, + trace_ndjson: trace_ndjson_str, + trace_tla: String::new(), + argv: Vec::new(), + status: TlcStatus::MissingRunner, + exit_code: None, + stdout: String::new(), + stderr: "Missing TLC runner: pass --tlc-bin (wrapper) or --tlc-jar /path/to/tla2tools.jar (or set TLA2TOOLS_JAR)" + .to_string(), + runtime_ms: None, + total_runtime_ms: Some(start_total.elapsed().as_millis()), + diameter: None, + matched_prefix: None, + first_failure: None, + peak_rss_kb: None, + }; + }; + + let java = find_java_binary().unwrap_or_else(|| PathBuf::from("java")); + let mut cmd = Command::new(&java); + if !cli.tlc_no_dfs { + cmd.arg("-Dtlc2.tool.queue.IStateQueue=StateDeque"); + } + cmd.arg("-cp").arg(jar).arg("tlc2.TLC"); + cmd + }; + + cmd.arg("-workers").arg("1"); + cmd.arg("-metadir").arg(&meta_dir); + cmd.arg("-config").arg(&cfg_file); + cmd.arg(&module_file); + + let argv = std::iter::once(cmd.get_program().to_string_lossy().to_string()) + .chain( + cmd.get_args() + .map(|a| a.to_string_lossy().to_string()) + .collect::>(), + ) + .collect::>(); + + let start = Instant::now(); + let output = run_command_with_peak_rss(&mut cmd, cli.measure_rss); + let runtime_ms = start.elapsed().as_millis(); + + match output { + Ok((output, peak_rss_kb)) => { + let exit_code = output.status.code(); + let stdout = String::from_utf8_lossy(&output.stdout).to_string(); + let stderr = String::from_utf8_lossy(&output.stderr).to_string(); + + let combined = format!("{stdout}\n{stderr}"); + let diameter = parse_tlc_diameter(&combined); + let trace_len = count_nonempty_lines(&trace_ndjson).ok(); + let matched_prefix = diameter + .map(|d| d.saturating_sub(1)) + .or_else(|| parse_tlc_last_l(&combined).map(|l| l.saturating_sub(1))); + + let status = match exit_code { + Some(0) => match (trace_len, matched_prefix) { + (Some(len), Some(prefix)) if prefix == len => TlcStatus::Accept, + (Some(_), Some(_)) => TlcStatus::Reject, + _ => TlcStatus::Error, + }, + Some(_) => { + if tlc_output_indicates_reject(&combined) { + TlcStatus::Reject + } else { + TlcStatus::Error + } + } + None => TlcStatus::Error, + }; + + let first_failure = match (status.clone(), trace_len, matched_prefix) { + (TlcStatus::Reject, Some(len), Some(prefix)) if prefix < len => { + let idx = prefix + 1; + let (time_ns, event_id, kind) = + read_trace_fields_at_index(&trace_ndjson, idx).unwrap_or_default(); + Some(TlcFirstFailure { + trace_file: inv + .trace_csv + .file_name() + .map(|s| s.to_string_lossy().to_string()) + .unwrap_or_else(|| inv.trace_csv.display().to_string()), + index: idx, + time_ns, + event_id, + kind, + }) + } + _ => None, + }; + + TlcResult { + module: module_str, + cfg: cfg_str, + trace_csv: trace_csv_str, + trace_ndjson: trace_ndjson_str, + trace_tla: trace_tla_str, + argv, + status, + exit_code, + stdout, + stderr, + runtime_ms: Some(runtime_ms), + total_runtime_ms: Some(start_total.elapsed().as_millis()), + diameter, + matched_prefix, + first_failure, + peak_rss_kb, + } + } + Err(e) => TlcResult { + module: module_str, + cfg: cfg_str, + trace_csv: trace_csv_str, + trace_ndjson: trace_ndjson_str, + trace_tla: trace_tla_str, + argv, + status: TlcStatus::Error, + exit_code: None, + stdout: String::new(), + stderr: format!("Failed to execute TLC runner: {e}"), + runtime_ms: Some(runtime_ms), + total_runtime_ms: Some(start_total.elapsed().as_millis()), + diameter: None, + matched_prefix: None, + first_failure: None, + peak_rss_kb: None, + }, + } +} + +fn find_java_binary() -> Option { + if let Ok(home) = env::var("JAVA_HOME") { + let candidate = PathBuf::from(home).join("bin").join("java"); + if candidate.is_file() { + return Some(candidate); + } + } + + for candidate in [ + "/opt/homebrew/opt/openjdk/bin/java", + "/usr/local/opt/openjdk/bin/java", + ] { + let path = PathBuf::from(candidate); + if path.is_file() { + return Some(path); + } + } + + find_in_path("java") +} + +fn find_in_path(exe: &str) -> Option { + let path = env::var_os("PATH")?; + for dir in env::split_paths(&path) { + let candidate = dir.join(exe); + if candidate.is_file() { + return Some(candidate); + } + } + None +} + +fn parse_tlc_diameter(text: &str) -> Option { + let mut last = None; + for line in text.lines() { + let line = line.trim(); + if let Some((_, rest)) = line.split_once("Diameter:") { + if let Some(v) = parse_first_u64(rest) { + last = Some(v); + } + continue; + } + + let needle = "The depth of the complete state graph search is"; + let rest = match line.split_once(needle) { + Some((_, rest)) => rest, + None => continue, + }; + + if let Some(v) = parse_first_u64(rest) { + last = Some(v); + } + } + last +} + +fn parse_first_u64(text: &str) -> Option { + let start = text.find(|c: char| c.is_ascii_digit())?; + let digits = text[start..] + .chars() + .take_while(|c| c.is_ascii_digit()) + .collect::(); + digits.parse::().ok() +} + +fn parse_tlc_last_l(text: &str) -> Option { + let mut last = None; + for line in text.lines() { + let mut line = line.trim(); + if let Some(rest) = line.strip_prefix("/\\") { + line = rest.trim(); + } + if let Some(rest) = line.strip_prefix("l =") { + let n = rest.trim().split_whitespace().next()?; + if let Ok(v) = n.parse::() { + last = Some(v); + } + } + } + last +} + +fn tlc_output_indicates_reject(text: &str) -> bool { + // TLC uses non-zero exit codes for most errors. For our baseline, treat + // "spec says trace can't proceed" errors as REJECT (not ERROR). + if text.contains("Invariant") && text.contains("is violated") { + return true; + } + if text.contains("The model has no initial states") { + return true; + } + false +} + +fn run_command_with_peak_rss( + cmd: &mut Command, + measure_rss: bool, +) -> std::io::Result<(std::process::Output, Option)> { + if !measure_rss { + return cmd.output().map(|out| (out, None)); + } + + cmd.stdout(Stdio::piped()); + cmd.stderr(Stdio::piped()); + + let child = cmd.spawn()?; + let pid = child.id(); + let stop = Arc::new(AtomicBool::new(false)); + let stop_reader = Arc::clone(&stop); + + let sampler = std::thread::spawn(move || { + let mut max_rss = 0u64; + while !stop_reader.load(Ordering::Relaxed) { + if let Some(rss_kb) = get_rss_kb(pid) { + max_rss = max_rss.max(rss_kb); + } + std::thread::sleep(Duration::from_millis(50)); + } + max_rss + }); + + let output = child.wait_with_output(); + stop.store(true, Ordering::Relaxed); + let peak_rss_kb = sampler.join().ok(); + + output.map(|out| { + let peak = peak_rss_kb.and_then(|v| if v == 0 { None } else { Some(v) }); + (out, peak) + }) +} + +fn get_rss_kb(pid: u32) -> Option { + // `ps` rss is KB on macOS and Linux. + let output = Command::new("ps") + .arg("-o") + .arg("rss=") + .arg("-p") + .arg(pid.to_string()) + .output() + .ok()?; + if !output.status.success() { + return None; + } + let s = String::from_utf8_lossy(&output.stdout); + s.split_whitespace().next()?.parse::().ok() +} + +fn count_nonempty_lines(path: &Path) -> Result { + let f = + File::open(path).map_err(|e| format!("Failed to open trace {}: {e}", path.display()))?; + let reader = std::io::BufReader::new(f); + let mut count = 0u64; + for line in reader.lines() { + let line = line.map_err(|e| format!("Failed to read trace {}: {e}", path.display()))?; + if !line.trim().is_empty() { + count += 1; + } + } + Ok(count) +} + +fn read_trace_fields_at_index( + path: &Path, + index_1_based: u64, +) -> Result<(Option, Option, Option), String> { + let f = + File::open(path).map_err(|e| format!("Failed to open trace {}: {e}", path.display()))?; + let reader = std::io::BufReader::new(f); + for (i, line) in reader.lines().enumerate() { + let line = line.map_err(|e| format!("Failed to read trace {}: {e}", path.display()))?; + let i1 = (i as u64) + 1; + if i1 != index_1_based { + continue; + } + + let v: serde_json::Value = + serde_json::from_str(&line).map_err(|e| format!("Invalid NDJSON at line {i1}: {e}"))?; + let obj = v + .as_object() + .ok_or_else(|| format!("NDJSON line {i1} is not an object"))?; + + let time_ns = obj.get("time_ns").and_then(|v| v.as_u64()); + let event_id = obj.get("event_id").and_then(|v| v.as_u64()); + let kind = obj + .get("kind") + .and_then(|v| v.as_str()) + .map(|s| s.to_string()); + return Ok((time_ns, event_id, kind)); + } + + Err(format!( + "Trace {} has no line {}", + path.display(), + index_1_based + )) +} + fn read_coverage_points(path: &Path) -> Option> { let content = fs::read_to_string(path).ok()?; + + // Preferred: LeanGuard checkers write a JSON object (CoverageReport) with a `cover` field. + // See: days/lean/LeanGuard/Shared/Coverage.lean + #[derive(Debug, Deserialize)] + struct CoverageReportJson { + cover: Vec, + } + + if let Ok(mut report) = serde_json::from_str::(&content) { + report.cover.sort(); + report.cover.dedup(); + return Some(report.cover); + } + + // Backward-compatible: allow a bare JSON array of strings. if let Ok(mut points) = serde_json::from_str::>(&content) { points.sort(); points.dedup(); return Some(points); } + + // Fallback: newline-separated points, but avoid treating JSON blobs as a single “point”. + let trimmed = content.trim_start(); + if trimmed.starts_with('{') || trimmed.starts_with('[') { + return None; + } + let mut points = content .lines() .map(|line| line.trim()) diff --git a/src/bin/leanguard-testgen.rs b/src/bin/leanguard-testgen.rs index c0740095..df4e1c7f 100644 --- a/src/bin/leanguard-testgen.rs +++ b/src/bin/leanguard-testgen.rs @@ -20,6 +20,35 @@ struct Cli { #[arg(long, default_value_t = false)] allow_nondeterministic: bool, + /// Disable passing `--coverage` to `leanguard-run` (semantic coverpoints). + #[arg(long, default_value_t = false)] + no_coverage: bool, + /// Also run a TLC-based trace-validation baseline via leanguard-run. + #[arg(long, default_value_t = false)] + tlc_check: bool, + + /// If set, require TLC baseline acceptance in addition to LeanGuard checkers. + #[arg(long, default_value_t = false)] + require_tlc_accept: bool, + + /// Directory containing baseline `.tla` modules and `.cfg` model configs. + #[arg(long, default_value = "tla")] + tlc_spec_dir: PathBuf, + + /// Optional TLC runner executable. If provided, this binary is executed directly. + /// + /// If omitted, leanguard-run runs TLC via `java -cp tlc2.TLC ...`. + #[arg(long)] + tlc_bin: Option, + + /// Path to `tla2tools.jar` (required unless `--tlc-bin` is provided). + #[arg(long)] + tlc_jar: Option, + + /// Disable the DFS state queue optimization recommended for trace validation. + #[arg(long, default_value_t = false)] + tlc_no_dfs: bool, + #[command(subcommand)] command: Command, } @@ -70,6 +99,13 @@ fn main() { checker_dir: cli.checker_dir, leanguard_run: cli.leanguard_run, allow_nondeterministic: cli.allow_nondeterministic, + coverage: !cli.no_coverage, + tlc_check: cli.tlc_check, + require_tlc_accept: cli.require_tlc_accept, + tlc_spec_dir: cli.tlc_spec_dir, + tlc_bin: cli.tlc_bin, + tlc_jar: cli.tlc_jar, + tlc_no_dfs: cli.tlc_no_dfs, }; let result = match cli.command { diff --git a/src/utils/mod.rs b/src/utils/mod.rs index f5ab47d6..f2f11740 100644 --- a/src/utils/mod.rs +++ b/src/utils/mod.rs @@ -3,6 +3,7 @@ pub mod logger; pub mod testgen; pub mod time; +pub mod trace_export; pub mod trace_manifest; pub mod tracing; pub mod ui; diff --git a/src/utils/testgen.rs b/src/utils/testgen.rs index 29b0bf9c..3ed3ac99 100644 --- a/src/utils/testgen.rs +++ b/src/utils/testgen.rs @@ -21,6 +21,13 @@ pub struct TestGenOptions { pub checker_dir: PathBuf, pub leanguard_run: Option, pub allow_nondeterministic: bool, + pub coverage: bool, + pub tlc_check: bool, + pub require_tlc_accept: bool, + pub tlc_spec_dir: PathBuf, + pub tlc_bin: Option, + pub tlc_jar: Option, + pub tlc_no_dfs: bool, } #[derive(Debug, Serialize)] @@ -449,6 +456,13 @@ pub fn fuzz( &opts.checker_dir, &config_path, opts.allow_nondeterministic, + opts.coverage, + opts.tlc_check, + opts.require_tlc_accept, + &opts.tlc_spec_dir, + opts.tlc_bin.as_deref(), + opts.tlc_jar.as_deref(), + opts.tlc_no_dfs, ); let (accept, run_summary, parsed) = match run { @@ -720,6 +734,13 @@ fn campaign_with_options( &opts.checker_dir, &config_path, opts.allow_nondeterministic, + opts.coverage, + opts.tlc_check, + opts.require_tlc_accept, + &opts.tlc_spec_dir, + opts.tlc_bin.as_deref(), + opts.tlc_jar.as_deref(), + opts.tlc_no_dfs, ); let (run_accept, run_json, run_parsed) = match run { @@ -785,20 +806,27 @@ fn campaign_with_options( dcqcn_summary.as_ref(), ); - if !accept - || goal_met - || iter >= max_iters - || campaign_opts.protocol != TargetProtocol::Dcqcn - { + let supports_calibration = matches!( + campaign_opts.protocol, + TargetProtocol::Dcqcn | TargetProtocol::Aqm + ); + if !accept || goal_met || iter >= max_iters || !supports_calibration { break; } - if let Some(change) = calibrate_dcqcn( - &mut config, - dcqcn_summary.as_ref(), - &campaign_opts.goal_coverpoints, - &mut rng, - ) { + let change = match campaign_opts.protocol { + TargetProtocol::Dcqcn => calibrate_dcqcn( + &mut config, + dcqcn_summary.as_ref(), + &campaign_opts.goal_coverpoints, + &mut rng, + ), + TargetProtocol::Aqm => { + calibrate_aqm(&mut config, &campaign_opts.goal_coverpoints, &mut rng, iter) + } + _ => None, + }; + if let Some(change) = change { let calibration_step = Mutation::CalibrationStep { iter, knob: change.reason.knob.to_string(), @@ -936,6 +964,13 @@ pub fn replay(opts: &TestGenOptions, case_dir: &Path) -> Result Vec { match protocol { TargetProtocol::Dcqcn => mutate_dcqcn_targeted(config, rng, goal), + TargetProtocol::Aqm => mutate_aqm_targeted(config, rng, goal), _ => Vec::new(), } } @@ -1633,6 +1683,37 @@ fn mutate_switch_capacity(config: &mut toml::Value, rng: &mut StdRng) -> Option< }) } +fn mutate_switch_port_rate_down(config: &mut toml::Value, rng: &mut StdRng) -> Option { + let table = config.as_table_mut()?; + let switch = table.get_mut("switch")?.as_table_mut()?; + let current = switch.get("port_rate").and_then(value_to_f64)?; + let factors = [0.5, 0.75]; + let factor = *factors.choose(rng)?; + let new_value = (current * factor).max(1.0); + switch.insert("port_rate".to_string(), toml::Value::Float(new_value)); + Some(Mutation::TweakSwitchPortRate { + from: current, + to: new_value, + }) +} + +fn mutate_switch_capacity_down(config: &mut toml::Value, rng: &mut StdRng) -> Option { + let table = config.as_table_mut()?; + let switch = table.get_mut("switch")?.as_table_mut()?; + let current = switch.get("capacity").and_then(value_to_i64)?; + let factors = [0.5, 0.75]; + let factor = *factors.choose(rng)?; + let mut new_value = ((current as f64) * factor).round() as i64; + if new_value < 1 { + new_value = 1; + } + switch.insert("capacity".to_string(), toml::Value::Integer(new_value)); + Some(Mutation::TweakSwitchCapacity { + from: current, + to: new_value, + }) +} + fn mutate_shuffle_edges(config: &mut toml::Value, rng: &mut StdRng) -> Option { let table = config.as_table_mut()?; let edges = table.get_mut("edges")?.as_array_mut()?; @@ -1718,6 +1799,39 @@ fn mutate_dcqcn_targeted( mutations } +fn mutate_aqm_targeted( + config: &mut toml::Value, + rng: &mut StdRng, + goal: &[String], +) -> Vec { + // AQM config surface (from configs/*.toml): + // - switch: drop, port_rate, capacity, ecn_threshold + let mut mutations = Vec::new(); + + let mut targeted: Vec Option> = Vec::new(); + if goal + .iter() + .any(|g| g.eq_ignore_ascii_case("ecn_threshold_drop_overflow")) + { + targeted.push(mutate_switch_capacity_down); + targeted.push(mutate_switch_port_rate_down); + targeted.push(mutate_switch_ecn_threshold_up); + } + + if targeted.is_empty() { + return mutations; + } + + targeted.shuffle(rng); + let picks = targeted.len(); + for mutator in targeted.into_iter().take(picks) { + if let Some(mutation) = mutator(config, rng) { + mutations.push(mutation); + } + } + mutations +} + #[derive(Clone, Copy)] enum TrafficContainer { Flow, @@ -1989,6 +2103,27 @@ fn mutate_switch_ecn_threshold(config: &mut toml::Value, rng: &mut StdRng) -> Op }) } +fn mutate_switch_ecn_threshold_up(config: &mut toml::Value, rng: &mut StdRng) -> Option { + let current = config + .get("switch") + .and_then(|v| v.get("ecn_threshold")) + .and_then(value_to_f64)?; + let factors = [1.25, 1.5, 2.0]; + let factor = *factors.choose(rng)?; + let mut new_value = (current * factor).clamp(0.01, 0.99); + if (new_value - current).abs() < f64::EPSILON { + new_value = (current + 0.05).clamp(0.01, 0.99); + } + if new_value <= current { + return None; + } + let from = update_switch_value(config, "ecn_threshold", new_value)?; + Some(Mutation::TweakSwitchEcnThreshold { + from, + to: new_value, + }) +} + fn calibrate_dcqcn( config: &mut toml::Value, summary: Option<&DcqcnTraceSummary>, @@ -2005,7 +2140,7 @@ fn calibrate_dcqcn( }; if summary.cnp_sent == 0 || summary.cnp_recv == 0 { - if let Some(change) = adjust_switch_ecn_threshold(config, 0.5) { + if let Some(change) = adjust_switch_ecn_threshold(config, 0.5, "increase ECN marking") { return Some(change); } return adjust_dcqcn_rate(config, rng, 1.5, "increase CNP activity"); @@ -2045,7 +2180,7 @@ fn calibrate_dcqcn( } if missing("timer_without_cnp_seen") { - if let Some(change) = adjust_switch_ecn_threshold(config, 1.5) { + if let Some(change) = adjust_switch_ecn_threshold(config, 1.5, "reduce ECN marking") { return Some(change); } return adjust_dcqcn_rate(config, rng, 0.5, "reduce CNP frequency"); @@ -2054,6 +2189,39 @@ fn calibrate_dcqcn( None } +fn calibrate_aqm( + config: &mut toml::Value, + goal: &[String], + rng: &mut StdRng, + iter: usize, +) -> Option { + let missing = + |name: &str| !goal.is_empty() && goal.iter().any(|g| g.eq_ignore_ascii_case(name)); + + if missing("ecn_threshold_drop_overflow") { + // Rotate across a small set of increasingly aggressive knobs to increase the + // chance of observing an overflow drop under ECN-threshold AQM. + for offset in 0..5 { + let choice = (iter + offset) % 5; + let change = match choice { + 0 => adjust_switch_capacity(config, 0.5, "increase overflow likelihood"), + 1 => adjust_switch_port_rate(config, 0.5, "increase queue buildup"), + 2 => { + adjust_switch_ecn_threshold(config, 1.5, "delay ECN marking to allow overflow") + } + 3 => adjust_cnp_interval(config, rng, 2.0), + 4 => adjust_dcqcn_rate(config, rng, 2.0, "increase offered load for overflow"), + _ => None, + }; + if change.is_some() { + return change; + } + } + } + + None +} + fn adjust_cnp_interval( config: &mut toml::Value, rng: &mut StdRng, @@ -2210,7 +2378,96 @@ fn set_dcqcn_max_rate( }) } -fn adjust_switch_ecn_threshold(config: &mut toml::Value, factor: f64) -> Option { +fn adjust_switch_port_rate( + config: &mut toml::Value, + factor: f64, + reason: &str, +) -> Option { + let current = config + .get("switch") + .and_then(|v| v.get("port_rate")) + .and_then(value_to_f64)?; + if current <= 1.0 && factor < 1.0 { + return None; + } + let mut new_value = (current * factor).max(1.0); + if (new_value - current).abs() < f64::EPSILON { + new_value = if factor < 1.0 { + (current - 1.0).max(1.0) + } else { + current + 1.0 + }; + } + if (new_value - current).abs() < f64::EPSILON { + return None; + } + + let from = update_switch_value(config, "port_rate", new_value)?; + Some(CalibrationChange { + mutations: vec![Mutation::TweakSwitchPortRate { + from, + to: new_value, + }], + reason: CalibrationReason { + knob: "switch.port_rate", + from: format!("{current}"), + to: format!("{new_value}"), + reason: reason.to_string(), + }, + }) +} + +fn adjust_switch_capacity( + config: &mut toml::Value, + factor: f64, + reason: &str, +) -> Option { + let current = config + .get("switch") + .and_then(|v| v.get("capacity")) + .and_then(value_to_i64)?; + if current <= 1 && factor < 1.0 { + return None; + } + let mut new_value = ((current as f64) * factor).round() as i64; + if new_value < 1 { + new_value = 1; + } + if new_value == current { + new_value = if factor < 1.0 { + current - 1 + } else { + current + 1 + }; + if new_value < 1 { + new_value = 1; + } + } + if new_value == current { + return None; + } + + let switch = config.as_table_mut()?.get_mut("switch")?.as_table_mut()?; + switch.insert("capacity".to_string(), toml::Value::Integer(new_value)); + Some(CalibrationChange { + mutations: vec![Mutation::TweakSwitchCapacity { + from: current, + to: new_value, + }], + reason: CalibrationReason { + knob: "switch.capacity", + from: format!("{current}"), + to: format!("{new_value}"), + reason: reason.to_string(), + }, + }) +} + +fn adjust_switch_ecn_threshold( + config: &mut toml::Value, + factor: f64, + reason: &str, +) -> Option { let current = config .get("switch") .and_then(|v| v.get("ecn_threshold")) @@ -2229,7 +2486,7 @@ fn adjust_switch_ecn_threshold(config: &mut toml::Value, factor: f64) -> Option< knob: "switch.ecn_threshold", from: format!("{current}"), to: format!("{new_value}"), - reason: "adjust ECN threshold".to_string(), + reason: reason.to_string(), }, }) } @@ -2574,15 +2831,41 @@ fn run_leanguard( checker_dir: &Path, config_path: &Path, allow_nondeterministic: bool, + coverage: bool, + tlc_check: bool, + require_tlc_accept: bool, + tlc_spec_dir: &Path, + tlc_bin: Option<&Path>, + tlc_jar: Option<&Path>, + tlc_no_dfs: bool, ) -> Result { let mut cmd = Command::new(leanguard_run); cmd.arg("--config") .arg(config_path) .arg("--checker-dir") .arg(checker_dir); + if coverage { + cmd.arg("--coverage"); + } if allow_nondeterministic { cmd.arg("--allow-nondeterministic"); } + if tlc_check { + cmd.arg("--tlc-check"); + if require_tlc_accept { + cmd.arg("--require-tlc-accept"); + } + cmd.arg("--tlc-spec-dir").arg(tlc_spec_dir); + if let Some(bin) = tlc_bin { + cmd.arg("--tlc-bin").arg(bin); + } + if let Some(jar) = tlc_jar { + cmd.arg("--tlc-jar").arg(jar); + } + if tlc_no_dfs { + cmd.arg("--tlc-no-dfs"); + } + } let output = cmd .output() .map_err(|e| format!("Failed to run leanguard-run: {e}"))?; diff --git a/src/utils/trace_export.rs b/src/utils/trace_export.rs new file mode 100644 index 00000000..278091ec --- /dev/null +++ b/src/utils/trace_export.rs @@ -0,0 +1,455 @@ +use serde_json::{Map, Number, Value}; +use std::fs::File; +use std::io::{BufWriter, Write}; +use std::path::{Path, PathBuf}; + +#[derive(Debug, Clone)] +struct NdjsonRow { + time_ns: u64, + event_id: u64, + obj: Map, +} + +/// Default output path for an NDJSON export: replace the input extension with `.ndjson`. +pub fn default_ndjson_output_path(input: &Path) -> PathBuf { + let mut out = input.to_path_buf(); + out.set_extension("ndjson"); + out +} + +/// Export a Days `*_events.csv` file to an NDJSON file (one JSON object per row). +/// +/// If `sort` is true, rows are canonicalized by sorting on `(time_ns, event_id)` and duplicates +/// are rejected. +pub fn export_csv_to_ndjson(input: &Path, output: &Path, sort: bool) -> Result<(), String> { + let mut rdr = csv::ReaderBuilder::new() + .has_headers(true) + .from_path(input) + .map_err(|e| format!("Failed to open CSV {}: {e}", input.display()))?; + + let headers = rdr + .headers() + .map_err(|e| format!("Failed to read CSV header {}: {e}", input.display()))? + .clone(); + + let time_idx = headers + .iter() + .position(|h| h == "time_ns") + .ok_or_else(|| "CSV header is missing required column: time_ns".to_string())?; + let event_idx = headers + .iter() + .position(|h| h == "event_id") + .ok_or_else(|| "CSV header is missing required column: event_id".to_string())?; + + let mut rows = Vec::new(); + for (row_idx, result) in rdr.records().enumerate() { + let line_no = row_idx + 2; + let record = result.map_err(|e| { + format!( + "{}:{}: Failed to read CSV record: {e}", + input.display(), + line_no + ) + })?; + + let time_ns_str = record + .get(time_idx) + .ok_or_else(|| format!("{}:{}: missing time_ns field", input.display(), line_no))? + .trim(); + let event_id_str = record + .get(event_idx) + .ok_or_else(|| format!("{}:{}: missing event_id field", input.display(), line_no))? + .trim(); + + let time_ns = time_ns_str.parse::().map_err(|e| { + format!( + "{}:{}: invalid time_ns value {:?}: {e}", + input.display(), + line_no, + time_ns_str + ) + })?; + let event_id = event_id_str.parse::().map_err(|e| { + format!( + "{}:{}: invalid event_id value {:?}: {e}", + input.display(), + line_no, + event_id_str + ) + })?; + + let mut obj = Map::new(); + for (i, key) in headers.iter().enumerate() { + let raw = record.get(i).unwrap_or("").trim(); + if raw.is_empty() { + continue; + } + obj.insert(key.to_string(), parse_scalar_value(raw)); + } + + rows.push(NdjsonRow { + time_ns, + event_id, + obj, + }); + } + + if sort { + rows.sort_by_key(|r| (r.time_ns, r.event_id)); + + for pair in rows.windows(2) { + let a = &pair[0]; + let b = &pair[1]; + if a.time_ns == b.time_ns && a.event_id == b.event_id { + return Err(format!( + "Duplicate key (time_ns={}, event_id={}) in {}", + a.time_ns, + a.event_id, + input.display() + )); + } + } + } + + let file = File::create(output) + .map_err(|e| format!("Failed to create NDJSON {}: {e}", output.display()))?; + let mut writer = BufWriter::new(file); + + for row in rows { + serde_json::to_writer(&mut writer, &Value::Object(row.obj)) + .map_err(|e| format!("Failed to serialize NDJSON row: {e}"))?; + writer + .write_all(b"\n") + .map_err(|e| format!("Failed to write NDJSON row: {e}"))?; + } + + writer + .flush() + .map_err(|e| format!("Failed to flush NDJSON output: {e}"))?; + Ok(()) +} + +/// Export a Days `*_events.csv` file to a `.tla` module that defines `Trace` as a sequence of records. +/// +/// This is intended for TLC versions that do not support directly deserializing NDJSON. +/// +/// If `sort` is true, rows are canonicalized by sorting on `(time_ns, event_id)` and duplicates +/// are rejected. +pub fn export_csv_to_tla_trace_module( + input: &Path, + output: &Path, + sort: bool, + module_name: &str, +) -> Result<(), String> { + let mut rdr = csv::ReaderBuilder::new() + .has_headers(true) + .from_path(input) + .map_err(|e| format!("Failed to open CSV {}: {e}", input.display()))?; + + let headers = rdr + .headers() + .map_err(|e| format!("Failed to read CSV header {}: {e}", input.display()))? + .clone(); + + let time_idx = headers + .iter() + .position(|h| h == "time_ns") + .ok_or_else(|| "CSV header is missing required column: time_ns".to_string())?; + let event_idx = headers + .iter() + .position(|h| h == "event_id") + .ok_or_else(|| "CSV header is missing required column: event_id".to_string())?; + + let mut rows = Vec::new(); + for (row_idx, result) in rdr.records().enumerate() { + let line_no = row_idx + 2; + let record = result.map_err(|e| { + format!( + "{}:{}: Failed to read CSV record: {e}", + input.display(), + line_no + ) + })?; + + let time_ns_str = record + .get(time_idx) + .ok_or_else(|| format!("{}:{}: missing time_ns field", input.display(), line_no))? + .trim(); + let event_id_str = record + .get(event_idx) + .ok_or_else(|| format!("{}:{}: missing event_id field", input.display(), line_no))? + .trim(); + + let time_ns = time_ns_str.parse::().map_err(|e| { + format!( + "{}:{}: invalid time_ns value {:?}: {e}", + input.display(), + line_no, + time_ns_str + ) + })?; + let event_id = event_id_str.parse::().map_err(|e| { + format!( + "{}:{}: invalid event_id value {:?}: {e}", + input.display(), + line_no, + event_id_str + ) + })?; + + let mut obj = Map::new(); + for (i, key) in headers.iter().enumerate() { + let raw = record.get(i).unwrap_or("").trim(); + if raw.is_empty() { + continue; + } + obj.insert(key.to_string(), parse_scalar_value(raw)); + } + + rows.push(NdjsonRow { + time_ns, + event_id, + obj, + }); + } + + if sort { + rows.sort_by_key(|r| (r.time_ns, r.event_id)); + + for pair in rows.windows(2) { + let a = &pair[0]; + let b = &pair[1]; + if a.time_ns == b.time_ns && a.event_id == b.event_id { + return Err(format!( + "Duplicate key (time_ns={}, event_id={}) in {}", + a.time_ns, + a.event_id, + input.display() + )); + } + } + } + + let file = File::create(output) + .map_err(|e| format!("Failed to create TLA module {}: {e}", output.display()))?; + let mut writer = BufWriter::new(file); + + writeln!( + writer, + "---------------------------- MODULE {module_name} ----------------------------" + ) + .map_err(|e| format!("Failed to write TLA header: {e}"))?; + writeln!(writer, "\\* AUTOGENERATED from {}", input.display()) + .map_err(|e| format!("Failed to write TLA header: {e}"))?; + writeln!( + writer, + "\\* NOTE: This trace is rescaled to fit TLC's 32-bit integers:" + ) + .map_err(|e| format!("Failed to write TLA header: {e}"))?; + writeln!( + writer, + "\\* - `*_ns` are stored in microseconds (rounded)" + ) + .map_err(|e| format!("Failed to write TLA header: {e}"))?; + writeln!( + writer, + "\\* - `*_bps` are stored in units of 10 Mbps (rounded)" + ) + .map_err(|e| format!("Failed to write TLA header: {e}"))?; + writeln!( + writer, + "\\* - `*_ppb` are stored in permille (1/1000) units (rounded)" + ) + .map_err(|e| format!("Failed to write TLA header: {e}"))?; + writeln!(writer, "").map_err(|e| format!("Failed to write TLA header: {e}"))?; + + writeln!(writer, "Trace == <<").map_err(|e| format!("Failed to write TLA Trace: {e}"))?; + for (idx, row) in rows.iter().enumerate() { + write!(writer, " [").map_err(|e| format!("Failed to write TLA Trace row: {e}"))?; + + let mut first = true; + for key in headers.iter() { + let Some(value) = row.obj.get(key) else { + continue; + }; + let value = scale_for_tlc_trace(key, value.clone()).map_err(|e| { + format!( + "Failed to rescale field {key} for TLC trace export (input {}): {e}", + input.display() + ) + })?; + if !first { + write!(writer, ", ").map_err(|e| format!("Failed to write TLA Trace row: {e}"))?; + } + first = false; + + write!(writer, "{key} |-> {}", to_tla_value(&value)) + .map_err(|e| format!("Failed to write TLA Trace row: {e}"))?; + } + + if idx + 1 == rows.len() { + writeln!(writer, "]").map_err(|e| format!("Failed to write TLA Trace row: {e}"))?; + } else { + writeln!(writer, "],").map_err(|e| format!("Failed to write TLA Trace row: {e}"))?; + } + } + writeln!(writer, ">>").map_err(|e| format!("Failed to write TLA Trace: {e}"))?; + + writeln!( + writer, + "\n=============================================================================" + ) + .map_err(|e| format!("Failed to write TLA footer: {e}"))?; + + writer + .flush() + .map_err(|e| format!("Failed to flush TLA output: {e}"))?; + Ok(()) +} + +fn parse_scalar_value(s: &str) -> Value { + match s { + "true" => return Value::Bool(true), + "false" => return Value::Bool(false), + _ => {} + } + + if let Some(num) = parse_json_number(s) { + return Value::Number(num); + } + + Value::String(s.to_string()) +} + +fn parse_json_number(s: &str) -> Option { + if s.is_empty() { + return None; + } + + let (neg, rest) = s.strip_prefix('-').map_or((false, s), |r| (true, r)); + if rest.is_empty() || !rest.chars().all(|c| c.is_ascii_digit()) { + return None; + } + + if neg { + let n = s.parse::().ok()?; + Some(Number::from(n)) + } else { + let n = s.parse::().ok()?; + Some(Number::from(n)) + } +} + +fn to_tla_value(v: &Value) -> String { + match v { + Value::Bool(true) => "TRUE".to_string(), + Value::Bool(false) => "FALSE".to_string(), + Value::Number(n) => n.to_string(), + Value::String(s) => format!("\"{}\"", escape_tla_string(s)), + _ => "FALSE".to_string(), + } +} + +fn escape_tla_string(s: &str) -> String { + let mut out = String::with_capacity(s.len()); + for ch in s.chars() { + match ch { + '\\' => out.push_str("\\\\"), + '"' => out.push_str("\\\""), + '\n' => out.push_str("\\n"), + '\r' => out.push_str("\\r"), + '\t' => out.push_str("\\t"), + c => out.push(c), + } + } + out +} + +fn scale_for_tlc_trace(field: &str, value: Value) -> Result { + let Value::Number(n) = value else { + return Ok(value); + }; + + let raw = if let Some(v) = n.as_u64() { + v + } else if let Some(v) = n.as_i64() { + if v < 0 { + return Err("negative integers are not supported in TLC trace export".to_string()); + } + v as u64 + } else { + return Ok(Value::Number(n)); + }; + + let div = if field.ends_with("_ns") { + 1_000u64 + } else if field.ends_with("_bps") { + 10_000_000u64 + } else if field.ends_with("_ppb") { + 1_000_000u64 + } else { + return Ok(Value::Number(n)); + }; + + let scaled = (raw + (div / 2)) / div; + if scaled > i32::MAX as u64 { + return Err(format!( + "scaled value {scaled} exceeds TLC's 32-bit integer range" + )); + } + Ok(Value::Number(Number::from(scaled))) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn ndjson_is_lossless_but_tla_trace_is_scaled_for_tlc() { + let dir = tempfile::tempdir().expect("tempdir"); + let csv_path = dir.path().join("dcqcn_events.csv"); + let ndjson_path = dir.path().join("dcqcn_events.ndjson"); + let tla_path = dir.path().join("TraceData.tla"); + + { + let mut f = File::create(&csv_path).expect("create csv"); + writeln!(f, "time_ns,event_id,kind,rate_bps,g_ppb,cnp_interval_ns").unwrap(); + writeln!(f, "100000,7,cnp_recv,10000000000,500000000,10000").unwrap(); + } + + export_csv_to_ndjson(&csv_path, &ndjson_path, true).expect("ndjson export"); + let ndjson = std::fs::read_to_string(&ndjson_path).expect("read ndjson"); + assert!( + ndjson.contains("\"rate_bps\":10000000000"), + "expected lossless bps in ndjson, got: {ndjson}" + ); + assert!( + ndjson.contains("\"g_ppb\":500000000"), + "expected lossless ppb in ndjson, got: {ndjson}" + ); + assert!( + ndjson.contains("\"time_ns\":100000"), + "expected lossless ns in ndjson, got: {ndjson}" + ); + + export_csv_to_tla_trace_module(&csv_path, &tla_path, true, "TraceData") + .expect("tla trace export"); + let tla = std::fs::read_to_string(&tla_path).expect("read tla"); + assert!( + tla.contains("rate_bps |-> 1000"), + "expected scaled bps in tla module, got:\n{tla}" + ); + assert!( + tla.contains("g_ppb |-> 500"), + "expected scaled ppb in tla module, got:\n{tla}" + ); + assert!( + tla.contains("cnp_interval_ns |-> 10"), + "expected scaled ns in tla module, got:\n{tla}" + ); + assert!( + tla.contains("time_ns |-> 100"), + "expected scaled time in tla module, got:\n{tla}" + ); + } +} diff --git a/tests/leanguard_run.rs b/tests/leanguard_run.rs index e0624d0e..ce8e07c1 100644 --- a/tests/leanguard_run.rs +++ b/tests/leanguard_run.rs @@ -29,7 +29,9 @@ fn leanguard_run_check_only_uses_manifest_and_runs_checkers() { r#"{"version":1,"traces":["aqm_events.csv","dcqcn_events.csv"]}"#, ) .expect("write manifest"); - fs::write(log_path.join("aqm_events.csv"), "x").expect("write aqm_events.csv"); + // aqm_events.csv must be a valid CSV for NDJSON/TLA export when TLC baseline is enabled. + fs::write(log_path.join("aqm_events.csv"), "time_ns,event_id\n1,0\n") + .expect("write aqm_events.csv"); fs::write(log_path.join("dcqcn_events.csv"), "y").expect("write dcqcn_events.csv"); // Create stub checker executables. @@ -67,3 +69,636 @@ fn leanguard_run_check_only_uses_manifest_and_runs_checkers() { .stdout(predicate::str::contains("dcqcn_check")) .stdout(predicate::str::contains("aqm_dcqcn_check")); } + +#[test] +fn leanguard_run_parses_lean_coverage_report_json() { + let tmp = tempfile::tempdir().expect("tempdir"); + let log_path = tmp.path().join("logs"); + fs::create_dir_all(&log_path).expect("create log dir"); + + let checker_dir = tmp.path().join("checkers"); + fs::create_dir_all(&checker_dir).expect("create checker dir"); + + // Minimal config surface for leanguard-run: log_path + threading. + let config_path = tmp.path().join("case.toml"); + fs::write( + &config_path, + format!( + "log_path = \"{}\"\nthreading = \"single\"\n", + log_path.display() + ), + ) + .expect("write config"); + + // Create manifest + dummy trace file (non-empty). + fs::write( + log_path.join("traces.json"), + r#"{"version":1,"traces":["dcqcn_events.csv"]}"#, + ) + .expect("write manifest"); + fs::write(log_path.join("dcqcn_events.csv"), "x").expect("write dcqcn_events.csv"); + + // Create a stub checker that writes Lean-style CoverageReport JSON to --coverage-out. + let checker_path = checker_dir.join("dcqcn_check"); + let mut f = fs::File::create(&checker_path).expect("create stub checker"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "out=\"\"").unwrap(); + writeln!(f, "while [ \"$#\" -gt 0 ]; do").unwrap(); + writeln!(f, " if [ \"$1\" = \"--coverage-out\" ]; then").unwrap(); + writeln!(f, " shift").unwrap(); + writeln!(f, " out=\"$1\"").unwrap(); + writeln!(f, " fi").unwrap(); + writeln!(f, " shift").unwrap(); + writeln!(f, "done").unwrap(); + writeln!(f, "if [ -n \"$out\" ]; then").unwrap(); + writeln!( + f, + "{}", + r#" echo '{"checker":"dcqcn_check","accept":true,"cover":["cp_b","cp_a"],"stats":{"rows":1,"processed_rows":1}}' > "$out""#, + ) + .unwrap(); + writeln!(f, "fi").unwrap(); + writeln!(f, "echo ACCEPT").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&checker_path).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&checker_path, perms).unwrap(); + } + + let mut cmd = cargo_bin_cmd!("leanguard-run"); + cmd.args([ + "--config", + config_path.to_str().unwrap(), + "--mode", + "check-only", + "--checker-dir", + checker_dir.to_str().unwrap(), + "--coverage", + ]); + + let output = cmd.output().expect("run leanguard-run"); + assert!(output.status.success(), "leanguard-run exit code"); + + let v: serde_json::Value = + serde_json::from_slice(&output.stdout).expect("parse leanguard-run JSON"); + assert_eq!(v["accept"].as_bool(), Some(true)); + + let cov = v.get("coverage").expect("missing coverage"); + let union = cov + .get("union") + .and_then(|v| v.as_array()) + .expect("coverage union array"); + let union_strs: Vec<&str> = union.iter().filter_map(|v| v.as_str()).collect(); + assert!(union_strs.contains(&"cp_a")); + assert!(union_strs.contains(&"cp_b")); + + let per = cov + .get("per_checker") + .and_then(|v| v.as_object()) + .expect("coverage per_checker object"); + let dcqcn_cov = per + .get("dcqcn_check") + .and_then(|v| v.as_array()) + .expect("per_checker[dcqcn_check] array"); + let dcqcn_cov: Vec<&str> = dcqcn_cov.iter().filter_map(|v| v.as_str()).collect(); + assert!(dcqcn_cov.contains(&"cp_a")); + assert!(dcqcn_cov.contains(&"cp_b")); + + let checker_results = v["checker_results"].as_array().expect("checker_results"); + assert_eq!(checker_results.len(), 1); + let checker_cov = checker_results[0] + .get("coverage") + .and_then(|v| v.as_array()) + .expect("checker_results[0].coverage"); + let checker_cov: Vec<&str> = checker_cov.iter().filter_map(|v| v.as_str()).collect(); + assert!(checker_cov.contains(&"cp_a")); + assert!(checker_cov.contains(&"cp_b")); +} + +#[test] +fn leanguard_run_check_only_can_run_tlc_via_stub_runner() { + let tmp = tempfile::tempdir().expect("tempdir"); + let log_path = tmp.path().join("logs"); + fs::create_dir_all(&log_path).expect("create log dir"); + + let checker_dir = tmp.path().join("checkers"); + fs::create_dir_all(&checker_dir).expect("create checker dir"); + + // Minimal config surface for leanguard-run: log_path + threading. + let config_path = tmp.path().join("case.toml"); + fs::write( + &config_path, + format!( + "log_path = \"{}\"\nthreading = \"single\"\n", + log_path.display() + ), + ) + .expect("write config"); + + // Create manifest + dummy trace files (non-empty). + fs::write( + log_path.join("traces.json"), + r#"{"version":1,"traces":["aqm_events.csv","dcqcn_events.csv"]}"#, + ) + .expect("write manifest"); + // aqm_events.csv must be a valid CSV for NDJSON/TLA export when TLC baseline is enabled. + fs::write(log_path.join("aqm_events.csv"), "time_ns,event_id\n1,0\n") + .expect("write aqm_events.csv"); + + // dcqcn_events.csv must be a valid CSV for NDJSON export (time_ns/event_id required). + fs::write( + log_path.join("dcqcn_events.csv"), + "time_ns,event_id,kind,endpoint_id,flow_id\n1,0,timer_tick,0,0\n", + ) + .expect("write dcqcn_events.csv"); + + // Create stub checker executables. + for exe in ["aqm_check", "dcqcn_check", "aqm_dcqcn_check"] { + let path = checker_dir.join(exe); + let mut f = fs::File::create(&path).expect("create stub checker"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo ACCEPT").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&path).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&path, perms).unwrap(); + } + } + + // Create a stub TLC runner that reports a full-trace depth (Len(trace)+1). + let tlc_stub = tmp.path().join("tlc_stub.sh"); + let mut f = fs::File::create(&tlc_stub).expect("create tlc stub"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo The depth of the complete state graph search is 2.").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&tlc_stub).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&tlc_stub, perms).unwrap(); + } + + let tla_dir = format!("{}/tla", env!("CARGO_MANIFEST_DIR")); + + let mut cmd = cargo_bin_cmd!("leanguard-run"); + cmd.args([ + "--config", + config_path.to_str().unwrap(), + "--mode", + "check-only", + "--checker-dir", + checker_dir.to_str().unwrap(), + "--tlc-check", + "--tlc-bin", + tlc_stub.to_str().unwrap(), + "--tlc-spec-dir", + &tla_dir, + ]); + + let output = cmd.output().expect("run leanguard-run"); + assert!(output.status.success(), "leanguard-run exit code"); + + let v: serde_json::Value = + serde_json::from_slice(&output.stdout).expect("parse leanguard-run JSON"); + + assert_eq!(v["accept"].as_bool(), Some(true)); + assert_eq!(v["tlc_accept"].as_bool(), Some(true)); + assert!(v["tlc_results"].is_array(), "expected tlc_results array"); + assert!( + v["tlc_results"][0]["status"].as_str() == Some("accept"), + "expected tlc_results[0].status=accept" + ); +} + +#[test] +fn leanguard_run_tlc_reject_reports_first_failure_by_diameter_prefix() { + let tmp = tempfile::tempdir().expect("tempdir"); + let log_path = tmp.path().join("logs"); + fs::create_dir_all(&log_path).expect("create log dir"); + + let checker_dir = tmp.path().join("checkers"); + fs::create_dir_all(&checker_dir).expect("create checker dir"); + + // Minimal config surface for leanguard-run: log_path + threading. + let config_path = tmp.path().join("case.toml"); + fs::write( + &config_path, + format!( + "log_path = \"{}\"\nthreading = \"single\"\n", + log_path.display() + ), + ) + .expect("write config"); + + // Create manifest + dummy trace files (non-empty). + fs::write( + log_path.join("traces.json"), + r#"{"version":1,"traces":["aqm_events.csv","dcqcn_events.csv"]}"#, + ) + .expect("write manifest"); + fs::write(log_path.join("aqm_events.csv"), "x").expect("write aqm_events.csv"); + + // dcqcn_events.csv must be a valid CSV for NDJSON export (time_ns/event_id required). + fs::write( + log_path.join("dcqcn_events.csv"), + "time_ns,event_id,kind,endpoint_id,flow_id\n1,0,timer_tick,0,0\n", + ) + .expect("write dcqcn_events.csv"); + + // Create stub checker executables. + for exe in ["aqm_check", "dcqcn_check", "aqm_dcqcn_check"] { + let path = checker_dir.join(exe); + let mut f = fs::File::create(&path).expect("create stub checker"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo ACCEPT").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&path).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&path, perms).unwrap(); + } + } + + // Create a stub TLC runner that reports an empty matched prefix (Diameter 1 => prefix 0). + let tlc_stub = tmp.path().join("tlc_stub_fail.sh"); + let mut f = fs::File::create(&tlc_stub).expect("create tlc stub"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo Diameter: 1").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&tlc_stub).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&tlc_stub, perms).unwrap(); + } + + let tla_dir = format!("{}/tla", env!("CARGO_MANIFEST_DIR")); + + let mut cmd = cargo_bin_cmd!("leanguard-run"); + cmd.args([ + "--config", + config_path.to_str().unwrap(), + "--mode", + "check-only", + "--checker-dir", + checker_dir.to_str().unwrap(), + "--tlc-check", + "--tlc-bin", + tlc_stub.to_str().unwrap(), + "--tlc-spec-dir", + &tla_dir, + ]); + + let output = cmd.output().expect("run leanguard-run"); + assert!(output.status.success(), "leanguard-run exit code"); + + let v: serde_json::Value = + serde_json::from_slice(&output.stdout).expect("parse leanguard-run JSON"); + + assert_eq!(v["accept"].as_bool(), Some(true)); + assert_eq!(v["tlc_accept"].as_bool(), Some(false)); + + // Pick the DCQCN TLC result (avoid depending on the ordering of `tlc_results`). + let tlc_results = v["tlc_results"] + .as_array() + .expect("expected tlc_results array"); + let dcqcn = tlc_results + .iter() + .find(|r| { + r["module"] + .as_str() + .is_some_and(|m| m.ends_with("DcqcnTrace.tla")) + }) + .expect("missing DcqcnTrace TLC result"); + + let failure = &dcqcn["first_failure"]; + assert_eq!(failure["index"].as_u64(), Some(1)); + assert_eq!(failure["time_ns"].as_u64(), Some(1)); + assert_eq!(failure["event_id"].as_u64(), Some(0)); + assert_eq!(failure["kind"].as_str(), Some("timer_tick")); +} + +#[test] +fn leanguard_run_tlc_rejects_on_invariant_violation_exit_code() { + let tmp = tempfile::tempdir().expect("tempdir"); + let log_path = tmp.path().join("logs"); + fs::create_dir_all(&log_path).expect("create log dir"); + + let checker_dir = tmp.path().join("checkers"); + fs::create_dir_all(&checker_dir).expect("create checker dir"); + + // Minimal config surface for leanguard-run: log_path + threading. + let config_path = tmp.path().join("case.toml"); + fs::write( + &config_path, + format!( + "log_path = \"{}\"\nthreading = \"single\"\n", + log_path.display() + ), + ) + .expect("write config"); + + // Create manifest + dummy trace files (non-empty). + fs::write( + log_path.join("traces.json"), + r#"{"version":1,"traces":["dcqcn_events.csv"]}"#, + ) + .expect("write manifest"); + + // dcqcn_events.csv must be a valid CSV for NDJSON export (time_ns/event_id required). + fs::write( + log_path.join("dcqcn_events.csv"), + "time_ns,event_id,kind,endpoint_id,flow_id\n1,0,timer_tick,0,0\n", + ) + .expect("write dcqcn_events.csv"); + + // Create stub checker executables. + for exe in ["dcqcn_check"] { + let path = checker_dir.join(exe); + let mut f = fs::File::create(&path).expect("create stub checker"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo ACCEPT").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&path).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&path, perms).unwrap(); + } + } + + // Create a stub TLC runner that signals an invariant violation via non-zero exit. + let tlc_stub = tmp.path().join("tlc_stub_invariant_fail.sh"); + let mut f = fs::File::create(&tlc_stub).expect("create tlc stub"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo Error: Invariant ProgressOk is violated.").unwrap(); + writeln!(f, "echo The depth of the complete state graph search is 1.").unwrap(); + writeln!(f, "exit 1").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&tlc_stub).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&tlc_stub, perms).unwrap(); + } + + let tla_dir = format!("{}/tla", env!("CARGO_MANIFEST_DIR")); + + let mut cmd = cargo_bin_cmd!("leanguard-run"); + cmd.args([ + "--config", + config_path.to_str().unwrap(), + "--mode", + "check-only", + "--checker-dir", + checker_dir.to_str().unwrap(), + "--tlc-check", + "--tlc-bin", + tlc_stub.to_str().unwrap(), + "--tlc-spec-dir", + &tla_dir, + ]); + + let output = cmd.output().expect("run leanguard-run"); + assert!(output.status.success(), "leanguard-run exit code"); + + let v: serde_json::Value = + serde_json::from_slice(&output.stdout).expect("parse leanguard-run JSON"); + + assert_eq!(v["accept"].as_bool(), Some(true)); + assert_eq!(v["tlc_accept"].as_bool(), Some(false)); + + let tlc_results = v["tlc_results"] + .as_array() + .expect("expected tlc_results array"); + let dcqcn = tlc_results + .iter() + .find(|r| { + r["module"] + .as_str() + .is_some_and(|m| m.ends_with("DcqcnTrace.tla")) + }) + .expect("missing DcqcnTrace TLC result"); + + assert_eq!(dcqcn["status"].as_str(), Some("reject")); + let failure = &dcqcn["first_failure"]; + assert_eq!(failure["index"].as_u64(), Some(1)); + assert_eq!(failure["time_ns"].as_u64(), Some(1)); + assert_eq!(failure["event_id"].as_u64(), Some(0)); + assert_eq!(failure["kind"].as_str(), Some("timer_tick")); +} + +#[test] +fn leanguard_run_tlc_accept_parses_tool_wrapped_depth() { + let tmp = tempfile::tempdir().expect("tempdir"); + let log_path = tmp.path().join("logs"); + fs::create_dir_all(&log_path).expect("create log dir"); + + let checker_dir = tmp.path().join("checkers"); + fs::create_dir_all(&checker_dir).expect("create checker dir"); + + // Minimal config surface for leanguard-run: log_path + threading. + let config_path = tmp.path().join("case.toml"); + fs::write( + &config_path, + format!( + "log_path = \"{}\"\nthreading = \"single\"\n", + log_path.display() + ), + ) + .expect("write config"); + + fs::write( + log_path.join("traces.json"), + r#"{"version":1,"traces":["dcqcn_events.csv"]}"#, + ) + .expect("write manifest"); + + fs::write( + log_path.join("dcqcn_events.csv"), + "time_ns,event_id,kind,endpoint_id,flow_id\n1,0,timer_tick,0,0\n", + ) + .expect("write dcqcn_events.csv"); + + // Create stub checker executable. + let checker_path = checker_dir.join("dcqcn_check"); + let mut f = fs::File::create(&checker_path).expect("create stub checker"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo ACCEPT").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&checker_path).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&checker_path, perms).unwrap(); + } + + // Simulate TLC -tool output wrapping the depth line. + let tlc_stub = tmp.path().join("tlc_stub_tool_mode.sh"); + let mut f = fs::File::create(&tlc_stub).expect("create tlc stub"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo @\\!@\\!@\\!STARTMSG 9999:0 @\\!@\\!@\\!The depth of the complete state graph search is 2.@\\!@\\!@\\!ENDMSG 9999").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&tlc_stub).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&tlc_stub, perms).unwrap(); + } + + let tla_dir = format!("{}/tla", env!("CARGO_MANIFEST_DIR")); + + let mut cmd = cargo_bin_cmd!("leanguard-run"); + cmd.args([ + "--config", + config_path.to_str().unwrap(), + "--mode", + "check-only", + "--checker-dir", + checker_dir.to_str().unwrap(), + "--tlc-check", + "--tlc-bin", + tlc_stub.to_str().unwrap(), + "--tlc-spec-dir", + &tla_dir, + ]); + + cmd.assert() + .success() + .stdout(predicate::str::contains("\"tlc_accept\": true")); +} + +#[test] +fn leanguard_run_tlc_rejects_with_l_fallback_when_no_diameter() { + let tmp = tempfile::tempdir().expect("tempdir"); + let log_path = tmp.path().join("logs"); + fs::create_dir_all(&log_path).expect("create log dir"); + + let checker_dir = tmp.path().join("checkers"); + fs::create_dir_all(&checker_dir).expect("create checker dir"); + + // Minimal config surface for leanguard-run: log_path + threading. + let config_path = tmp.path().join("case.toml"); + fs::write( + &config_path, + format!( + "log_path = \"{}\"\nthreading = \"single\"\n", + log_path.display() + ), + ) + .expect("write config"); + + fs::write( + log_path.join("traces.json"), + r#"{"version":1,"traces":["dcqcn_events.csv"]}"#, + ) + .expect("write manifest"); + + fs::write( + log_path.join("dcqcn_events.csv"), + "time_ns,event_id,kind,endpoint_id,flow_id\n1,0,timer_tick,0,0\n", + ) + .expect("write dcqcn_events.csv"); + + // Create stub checker executable. + let checker_path = checker_dir.join("dcqcn_check"); + let mut f = fs::File::create(&checker_path).expect("create stub checker"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!(f, "echo ACCEPT").unwrap(); + writeln!(f, "exit 0").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&checker_path).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&checker_path, perms).unwrap(); + } + + // Invariant violation by the initial state: no depth/diameter line, but `l = 1`. + let tlc_stub = tmp.path().join("tlc_stub_initial_invariant_fail.sh"); + let mut f = fs::File::create(&tlc_stub).expect("create tlc stub"); + writeln!(f, "#!/bin/sh").unwrap(); + writeln!( + f, + "echo Error: Invariant ProgressOk is violated by the initial state:" + ) + .unwrap(); + writeln!(f, "echo l = 1").unwrap(); + writeln!(f, "exit 1").unwrap(); + drop(f); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mut perms = fs::metadata(&tlc_stub).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&tlc_stub, perms).unwrap(); + } + + let tla_dir = format!("{}/tla", env!("CARGO_MANIFEST_DIR")); + + let mut cmd = cargo_bin_cmd!("leanguard-run"); + cmd.args([ + "--config", + config_path.to_str().unwrap(), + "--mode", + "check-only", + "--checker-dir", + checker_dir.to_str().unwrap(), + "--tlc-check", + "--tlc-bin", + tlc_stub.to_str().unwrap(), + "--tlc-spec-dir", + &tla_dir, + ]); + + let output = cmd.output().expect("run leanguard-run"); + assert!(output.status.success(), "leanguard-run exit code"); + + let v: serde_json::Value = + serde_json::from_slice(&output.stdout).expect("parse leanguard-run JSON"); + + assert_eq!(v["accept"].as_bool(), Some(true)); + assert_eq!(v["tlc_accept"].as_bool(), Some(false)); + + let tlc_results = v["tlc_results"] + .as_array() + .expect("expected tlc_results array"); + let dcqcn = tlc_results + .iter() + .find(|r| { + r["module"] + .as_str() + .is_some_and(|m| m.ends_with("DcqcnTrace.tla")) + }) + .expect("missing DcqcnTrace TLC result"); + + assert_eq!(dcqcn["status"].as_str(), Some("reject")); + let failure = &dcqcn["first_failure"]; + assert_eq!(failure["index"].as_u64(), Some(1)); + assert_eq!(failure["time_ns"].as_u64(), Some(1)); + assert_eq!(failure["event_id"].as_u64(), Some(0)); + assert_eq!(failure["kind"].as_str(), Some("timer_tick")); +} diff --git a/tests/testgen_campaign_dcqcn.rs b/tests/testgen_campaign_dcqcn.rs index d32566d2..2673614c 100644 --- a/tests/testgen_campaign_dcqcn.rs +++ b/tests/testgen_campaign_dcqcn.rs @@ -21,6 +21,13 @@ fn test_campaign_dcqcn_targeted_mutations_in_dry_run() { checker_dir: PathBuf::from("lean/.lake/build/bin"), leanguard_run: None, allow_nondeterministic: false, + coverage: true, + tlc_check: false, + require_tlc_accept: false, + tlc_spec_dir: PathBuf::from("tla"), + tlc_bin: None, + tlc_jar: None, + tlc_no_dfs: false, }; seed_index(&opts, &seeds_src).expect("seed-index"); diff --git a/tests/testgen_seed_index.rs b/tests/testgen_seed_index.rs index 51b5587a..8224d65b 100644 --- a/tests/testgen_seed_index.rs +++ b/tests/testgen_seed_index.rs @@ -21,6 +21,13 @@ fn test_seed_index_creates_corpus() { checker_dir: PathBuf::from("lean/.lake/build/bin"), leanguard_run: None, allow_nondeterministic: false, + coverage: true, + tlc_check: false, + require_tlc_accept: false, + tlc_spec_dir: PathBuf::from("tla"), + tlc_bin: None, + tlc_jar: None, + tlc_no_dfs: false, }; let summary = seed_index(&opts, &seeds_src).expect("seed-index"); diff --git a/tla/AqmTrace.cfg b/tla/AqmTrace.cfg new file mode 100644 index 00000000..bd8aee5a --- /dev/null +++ b/tla/AqmTrace.cfg @@ -0,0 +1,4 @@ +SPECIFICATION TraceSpec +INVARIANT ProgressOk +\* Trace validation does not benefit from deadlock checking. +CHECK_DEADLOCK FALSE diff --git a/tla/AqmTrace.tla b/tla/AqmTrace.tla new file mode 100644 index 00000000..1eb5b4ef --- /dev/null +++ b/tla/AqmTrace.tla @@ -0,0 +1,151 @@ +------------------------------ MODULE AqmTrace ------------------------------ +\* Trace validation baseline for Days AQM decisions. +\* +\* Intended to mirror the checks in: +\* - `lean/LeanGuard/Aqm/Semantics.lean` +\* - `lean/LeanGuard/AqmEventLog.lean` +\* +\* This module expects a companion module named `TraceData` that defines: +\* Trace == << [ time_ns |-> ..., event_id |-> ..., ... ], ... >> +\* +\* IMPORTANT: `TraceData` is rescaled to fit TLC's 32-bit integers: +\* - `*_ns` fields are stored in microseconds +\* - `*_ppb` fields are stored in permille (PPB == 1000) +\* - `*_bps` fields are stored in units of 10 Mbps (unused here) + +EXTENDS Naturals, Integers, Sequences, TLC, TraceData + +PPB == 1000 + +LenTrace == Len(Trace) + +Key(rec) == <> +KeyLt(k1, k2) == + (k1[1] < k2[1]) \/ (k1[1] = k2[1] /\ k1[2] < k2[2]) + +TraceOk == + IF LenTrace <= 1 THEN + TRUE + ELSE + \A i \in 1..(LenTrace - 1) : KeyLt(Key(Trace[i]), Key(Trace[i + 1])) + +Has(ll, field) == field \in DOMAIN ll + +ApproxLeq(a, b, eps) == a <= b + eps + +EcnMarkAllowed(before, after) == + ~((before = "not_ect") /\ (after = "ce")) + +ThresholdCap(ppb, cap) == (ppb * cap) \div PPB + +QueueOverflow(ll) == + IF ll.capacity = 0 THEN + FALSE + ELSE + IF ll.capacity_unit = "bytes" THEN + ll.byte_length + ll.size_bytes > ll.capacity + ELSE + ll.queue_length + 1 > ll.capacity + +ExceedsThreshold(ll, ppb) == + IF ll.capacity = 0 THEN + FALSE + ELSE + IF ll.capacity_unit = "bytes" THEN + ll.byte_length + ll.size_bytes > ThresholdCap(ppb, ll.capacity) + ELSE + ll.queue_length + 1 > ThresholdCap(ppb, ll.capacity) + +RedProbPpb(ll, minPpb, maxPpb, maxProbPpb, avg) == + IF maxPpb <= minPpb THEN + 0 + ELSE + LET minCap == ThresholdCap(minPpb, ll.capacity) + diff == IF avg > minCap THEN avg - minCap ELSE 0 + IN (diff * ll.capacity * maxProbPpb) \div (maxPpb - minPpb) + +RedDecisionOk(ll) == + /\ Has(ll, "red_min_threshold_ppb") + /\ Has(ll, "red_max_threshold_ppb") + /\ Has(ll, "red_max_probability_ppb") + /\ Has(ll, "red_avg_queue_length") + /\ LET minPpb == ll.red_min_threshold_ppb + maxPpb == ll.red_max_threshold_ppb + maxProbPpb == ll.red_max_probability_ppb + avg == ll.red_avg_queue_length + overMax == ExceedsThreshold(ll, maxPpb) + overMin == ExceedsThreshold(ll, minPpb) + overflow == QueueOverflow(ll) + maxRandOk == IF overMax THEN Has(ll, "red_rand_max_ppb") ELSE TRUE + minRandOk == IF overMin THEN Has(ll, "red_rand_min_ppb") ELSE TRUE + maxHit == + IF Has(ll, "red_rand_max_ppb") THEN + ApproxLeq(ll.red_rand_max_ppb, maxProbPpb, 1) + ELSE + FALSE + minProbPpb == RedProbPpb(ll, minPpb, maxPpb, maxProbPpb, avg) + minHit == + IF Has(ll, "red_rand_min_ppb") THEN + ApproxLeq(ll.red_rand_min_ppb, minProbPpb, 1) + ELSE + FALSE + shouldMark == (overMax /\ maxHit) \/ (overMin /\ minHit) + IN + /\ maxRandOk + /\ minRandOk + /\ IF overflow THEN + ll.action = "drop" + ELSE + CASE ll.drop_strategy = "red" -> + IF shouldMark THEN ll.action = "drop" ELSE ll.action = "enqueue" + [] ll.drop_strategy = "red_ecn" -> + IF shouldMark THEN + (ll.action = "mark_ecn" \/ (ll.action = "drop" /\ ll.ecn_before = "not_ect")) + ELSE + ll.action = "enqueue" + [] OTHER -> FALSE + +TailDropOk(ll) == + LET overflow == QueueOverflow(ll) + IN IF overflow THEN ll.action = "drop" ELSE ll.action = "enqueue" + +EcnThresholdOk(ll) == + /\ Has(ll, "ecn_threshold_ppb") + /\ LET overflow == QueueOverflow(ll) + thresh == ExceedsThreshold(ll, ll.ecn_threshold_ppb) + IN + IF overflow THEN + ll.action = "drop" + ELSE IF thresh THEN + (ll.action = "mark_ecn" \/ (ll.action = "drop" /\ ll.ecn_before = "not_ect")) + ELSE + ll.action = "enqueue" + +DecisionOk(ll) == + /\ ll.kind = "decision" + /\ EcnMarkAllowed(ll.ecn_before, ll.ecn_after) + /\ CASE ll.drop_strategy = "tail_drop" -> TailDropOk(ll) + [] ll.drop_strategy = "ecn_threshold" -> EcnThresholdOk(ll) + [] ll.drop_strategy = "red" -> RedDecisionOk(ll) + [] ll.drop_strategy = "red_ecn" -> RedDecisionOk(ll) + [] OTHER -> FALSE + +VARIABLES l + +Vars == <> + +Init == + /\ l = 1 + /\ TraceOk + +Next == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] IN + /\ DecisionOk(ll) + /\ l' = l + 1 + +TraceSpec == Init /\ [][Next]_Vars + +ProgressOk == IF l <= LenTrace THEN ENABLED Next ELSE TRUE + +============================================================================= diff --git a/tla/CubicTrace.cfg b/tla/CubicTrace.cfg new file mode 100644 index 00000000..dab6cf84 --- /dev/null +++ b/tla/CubicTrace.cfg @@ -0,0 +1,3 @@ +SPECIFICATION TraceSpec +INVARIANT ProgressOk +CHECK_DEADLOCK FALSE diff --git a/tla/CubicTrace.tla b/tla/CubicTrace.tla new file mode 100644 index 00000000..cab3677b --- /dev/null +++ b/tla/CubicTrace.tla @@ -0,0 +1,342 @@ +------------------------------ MODULE CubicTrace ------------------------------ +\* Trace validation baseline for Days TCP CUBIC traces. +\* +\* Intended to mirror: +\* - `lean/LeanGuard/Cubic/Semantics.lean` +\* - `lean/LeanGuard/CubicEventLog.lean` +\* - the implementation in `src/flows/cubic.rs` and CUBIC event logging in `src/flows/tcp_source.rs`. +\* +\* This module expects a companion module named `TraceData` defining `Trace`. +\* +\* IMPORTANT: `TraceData` is rescaled to fit TLC's 32-bit integers: +\* - `*_ns` fields are stored in microseconds +\* - `*_ppb` fields are stored in permille (PPB == 1000) +\* +\* NOTE: This baseline implements: +\* - slow-start ACK growth, +\* - congestion-avoidance ACK growth via a fixed-point approximation of RFC 8312's +\* CUBIC window-growth function (scaled time + scaled segments), +\* - and the byte-level congestion/timeout reductions. +\* +\* Due to TraceData rescaling and the fixed-point approximation, this spec uses a +\* small tolerance when comparing the computed `cwnd_bytes` against the logged value. + +EXTENDS Naturals, Integers, Sequences, TLC, FiniteSets, TraceData + +PPB == 1000 +TIME_SCALE == 100 +\* Segment fixed-point scale: 1 segment == SEG_SCALE units. +SEG_SCALE == 1000 +\* Allowed absolute error (bytes) in cwnd snapshot equality. +CWND_BYTES_TOL == 64 + +LenTrace == Len(Trace) + +Key(rec) == <> +KeyLt(k1, k2) == + (k1[1] < k2[1]) \/ (k1[1] = k2[1] /\ k1[2] < k2[2]) + +TraceOk == + IF LenTrace <= 1 THEN + TRUE + ELSE + \A i \in 1..(LenTrace - 1) : KeyLt(Key(Trace[i]), Key(Trace[i + 1])) + +Has(ll, field) == field \in DOMAIN ll + +OkParams(ll) == + /\ ll.mss_bytes > 0 + /\ ll.beta_ppb > 0 /\ ll.beta_ppb < PPB + /\ ll.c_ppb > 0 + /\ ll.init_cwnd_bytes > 0 + /\ ll.init_ssthresh_bytes > 0 + +AbsDiff(a, b) == IF a >= b THEN a - b ELSE b - a + +ApproxEq(a, b, eps) == AbsDiff(a, b) <= eps + +DefaultFlow == + [ present |-> FALSE, + flow_id |-> 0, + mss_bytes |-> 0, + beta_ppb |-> 0, + c_ppb |-> 0, + tcp_friendly |-> FALSE, + fast_convergence |-> FALSE, + init_cwnd_bytes |-> 0, + init_ssthresh_bytes |-> 0, + cwnd_bytes |-> 0, + ssthresh_bytes |-> 0, + w_max_bytes |-> 0, + w_last_max_bytes |-> 0, + epoch_has |-> FALSE, + epoch_start_ns |-> 0, + srtt_scaled |-> 0, + k_zero |-> TRUE, + last_time_has |-> FALSE, + last_time_ns |-> 0 ] + +EndpointIds == { Trace[i].endpoint_id : i \in 1..LenTrace } + +RoundDiv(n, d) == (n + (d \div 2)) \div d + +Max2(a, b) == IF a >= b THEN a ELSE b + +MulDiv(n, mul, div) == + LET q == n \div div + r == n - (q * div) + IN q * mul + (r * mul) \div div + +ScaledTime(us) == RoundDiv(us * TIME_SCALE, 1000000) + +BytesToMseg(bytes, mssBytes) == + LET q == bytes \div mssBytes + r == bytes - (q * mssBytes) + IN (q * SEG_SCALE) + (r * SEG_SCALE) \div mssBytes + +MsegToBytes(mseg, mssBytes) == + LET q == mseg \div SEG_SCALE + r == mseg - (q * SEG_SCALE) + IN (q * mssBytes) + (r * mssBytes) \div SEG_SCALE + +Cube(n) == n * n * n + +CubicTermMseg(cPpb, tScaled) == + \* term_mseg = floor(c * t^3 * SEG_SCALE) where: + \* - c = cPpb / PPB + \* - t = tScaled / TIME_SCALE seconds + \* With SEG_SCALE == PPB, this simplifies to: + \* floor(cPpb * tScaled^3 / TIME_SCALE^3) + LET t3 == Cube(tScaled) + denom == TIME_SCALE * TIME_SCALE * TIME_SCALE + q == t3 \div denom + r == t3 - (q * denom) + IN (cPpb * q) + (cPpb * r) \div denom + +UpdateSrttScaled(prevSrtt, rttUs) == + LET rttScaled == ScaledTime(rttUs) + IN IF prevSrtt = 0 THEN + rttScaled + ELSE + \* Standard TCP smoothing: (7/8)*srtt + (1/8)*rtt. + (7 * prevSrtt + rttScaled + 4) \div 8 + +ReducedBytes(cwndBytes, betaPpb, mssBytes) == + LET reduced == MulDiv(cwndBytes, betaPpb, PPB) + IN IF reduced < mssBytes THEN mssBytes ELSE reduced + +SsthreshBytes(reducedBytes, mssBytes) == + LET twoMss == 2 * mssBytes + IN IF reducedBytes < twoMss THEN twoMss ELSE reducedBytes + +LastTimeOk(st, t) == ~st.last_time_has \/ st.last_time_ns <= t + +UpdateLastTimeState(st, t) == + [st EXCEPT !.last_time_has = TRUE, !.last_time_ns = t] + +EnsureParamsOk(st, ll) == + IF ~st.present THEN + TRUE + ELSE + /\ st.flow_id = ll.flow_id + /\ st.mss_bytes = ll.mss_bytes + /\ st.beta_ppb = ll.beta_ppb + /\ st.c_ppb = ll.c_ppb + /\ st.tcp_friendly = ll.tcp_friendly + /\ st.fast_convergence = ll.fast_convergence + /\ st.init_cwnd_bytes = ll.init_cwnd_bytes + /\ st.init_ssthresh_bytes = ll.init_ssthresh_bytes + +EnsureParamsState(st, ll) == + IF ~st.present THEN + [ st EXCEPT + !.present = TRUE, + !.flow_id = ll.flow_id, + !.mss_bytes = ll.mss_bytes, + !.beta_ppb = ll.beta_ppb, + !.c_ppb = ll.c_ppb, + !.tcp_friendly = ll.tcp_friendly, + !.fast_convergence = ll.fast_convergence, + !.init_cwnd_bytes = ll.init_cwnd_bytes, + !.init_ssthresh_bytes = ll.init_ssthresh_bytes, + !.cwnd_bytes = ll.init_cwnd_bytes, + !.ssthresh_bytes = ll.init_ssthresh_bytes, + !.w_max_bytes = 0, + !.w_last_max_bytes = 0, + !.epoch_has = FALSE, + !.epoch_start_ns = 0, + !.srtt_scaled = 0, + !.k_zero = TRUE ] + ELSE + st + +VARIABLES l, flow + +Vars == <> + +Init == + /\ l = 1 + /\ TraceOk + /\ flow = [eid \in EndpointIds |-> DefaultFlow] + +Ack == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + eid == ll.endpoint_id + st0 == flow[eid] + stT == UpdateLastTimeState(st0, ll.time_ns) + st1 == EnsureParamsState(stT, ll) + acked == ll.acked_segs + rttUs == ll.rtt_ns + srtt1 == UpdateSrttScaled(st1.srtt_scaled, rttUs) + ssPre == st1.cwnd_bytes < st1.ssthresh_bytes + cwndSsNext == st1.cwnd_bytes + (acked * st1.mss_bytes) + enterCa == ssPre /\ cwndSsNext >= st1.ssthresh_bytes + epochHasSs == IF enterCa THEN TRUE ELSE st1.epoch_has + epochStartSs == IF enterCa THEN ll.time_ns ELSE st1.epoch_start_ns + wMaxSs == IF enterCa /\ st1.w_max_bytes = 0 THEN cwndSsNext ELSE st1.w_max_bytes + kZeroSs == IF enterCa /\ st1.w_max_bytes = 0 THEN TRUE ELSE st1.k_zero + \* Congestion-avoidance update (fixed-point, approximate). + epochHasCa == TRUE + epochStartCa == IF st1.epoch_has THEN st1.epoch_start_ns ELSE ll.time_ns + wMaxCa == IF st1.w_max_bytes = 0 THEN st1.cwnd_bytes ELSE st1.w_max_bytes + kZeroCa == IF st1.w_max_bytes = 0 THEN TRUE ELSE st1.k_zero + tScaled == ScaledTime(ll.time_ns - epochStartCa) + wMaxMseg == BytesToMseg(wMaxCa, st1.mss_bytes) + cwndMseg == BytesToMseg(st1.cwnd_bytes, st1.mss_bytes) + wCubicTMseg == wMaxMseg + CubicTermMseg(st1.c_ppb, tScaled) + wMaxBetaMseg == MulDiv(wMaxMseg, st1.beta_ppb, PPB) + aNum == 3 * (PPB - st1.beta_ppb) + aDen == (PPB + st1.beta_ppb) * Max2(srtt1, 1) + bNum == aNum * tScaled + bQ == bNum \div aDen + bR == bNum - (bQ * aDen) + secondMseg == (bQ * SEG_SCALE) + (bR * SEG_SCALE) \div aDen + wEstMseg == wMaxBetaMseg + secondMseg + caTargetScaled == tScaled + srtt1 + wTargetMseg == wMaxMseg + CubicTermMseg(st1.c_ppb, caTargetScaled) + denomMseg == Max2(cwndMseg, SEG_SCALE) + diffMseg == wTargetMseg - cwndMseg + deltaMseg == (diffMseg * SEG_SCALE) \div denomMseg + cwndCaNextMseg == + IF st1.tcp_friendly /\ wCubicTMseg < wEstMseg THEN wEstMseg ELSE cwndMseg + deltaMseg + cwndCaNextBytes == MsegToBytes(cwndCaNextMseg, st1.mss_bytes) + st2 == + IF ssPre THEN + [st1 EXCEPT + !.cwnd_bytes = cwndSsNext, + !.epoch_has = epochHasSs, + !.epoch_start_ns = epochStartSs, + !.w_max_bytes = wMaxSs, + !.srtt_scaled = srtt1, + !.k_zero = kZeroSs] + ELSE + [st1 EXCEPT + !.cwnd_bytes = cwndCaNextBytes, + !.epoch_has = epochHasCa, + !.epoch_start_ns = epochStartCa, + !.w_max_bytes = wMaxCa, + !.srtt_scaled = srtt1, + !.k_zero = kZeroCa] + IN + /\ ll.kind = "ack" + /\ OkParams(ll) + /\ LastTimeOk(st0, ll.time_ns) + /\ EnsureParamsOk(stT, ll) + /\ Has(ll, "acked_segs") /\ acked > 0 + /\ Has(ll, "rtt_ns") /\ rttUs > 0 + /\ (~st1.epoch_has \/ st1.epoch_start_ns <= ll.time_ns) + /\ ApproxEq(ll.cwnd_bytes, st2.cwnd_bytes, CWND_BYTES_TOL) + /\ ll.ssthresh_bytes = st2.ssthresh_bytes + /\ ll.w_max_bytes = st2.w_max_bytes + /\ ll.w_last_max_bytes = st2.w_last_max_bytes + /\ (IF st2.epoch_has THEN Has(ll, "epoch_start_ns") /\ ll.epoch_start_ns = st2.epoch_start_ns + ELSE ~Has(ll, "epoch_start_ns")) + /\ l' = l + 1 + /\ flow' = [flow EXCEPT ![eid] = st2] + +Congestion == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + eid == ll.endpoint_id + st0 == flow[eid] + stT == UpdateLastTimeState(st0, ll.time_ns) + st1 == EnsureParamsState(stT, ll) + cwnd0 == st1.cwnd_bytes + reduced == ReducedBytes(cwnd0, st1.beta_ppb, st1.mss_bytes) + ssthresh1 == SsthreshBytes(reduced, st1.mss_bytes) + wMaxCur == cwnd0 + fast == st1.fast_convergence + wLast0 == st1.w_last_max_bytes + fcCond == fast /\ wLast0 > 0 /\ wMaxCur < wLast0 + wLast1 == wMaxCur + wMax1 == + IF fcCond THEN + MulDiv(wMaxCur, (PPB + st1.beta_ppb), 2 * PPB) + ELSE + wMaxCur + st2 == + [st1 EXCEPT + !.cwnd_bytes = reduced, + !.ssthresh_bytes = ssthresh1, + !.w_max_bytes = wMax1, + !.w_last_max_bytes = wLast1, + !.epoch_has = TRUE, + !.epoch_start_ns = ll.time_ns, + !.k_zero = FALSE] + IN + /\ ll.kind = "congestion" + /\ OkParams(ll) + /\ LastTimeOk(st0, ll.time_ns) + /\ EnsureParamsOk(stT, ll) + /\ ~Has(ll, "acked_segs") + /\ ~Has(ll, "rtt_ns") + /\ ll.cwnd_bytes = st2.cwnd_bytes + /\ ll.ssthresh_bytes = st2.ssthresh_bytes + /\ ll.w_max_bytes = st2.w_max_bytes + /\ ll.w_last_max_bytes = st2.w_last_max_bytes + /\ Has(ll, "epoch_start_ns") /\ ll.epoch_start_ns = st2.epoch_start_ns + /\ l' = l + 1 + /\ flow' = [flow EXCEPT ![eid] = st2] + +Timeout == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + eid == ll.endpoint_id + st0 == flow[eid] + stT == UpdateLastTimeState(st0, ll.time_ns) + st1 == EnsureParamsState(stT, ll) + cwnd0 == st1.cwnd_bytes + reduced == ReducedBytes(cwnd0, st1.beta_ppb, st1.mss_bytes) + ssthresh1 == SsthreshBytes(reduced, st1.mss_bytes) + st2 == + [st1 EXCEPT + !.cwnd_bytes = st1.mss_bytes, + !.ssthresh_bytes = ssthresh1, + !.w_max_bytes = 0, + !.w_last_max_bytes = 0, + !.epoch_has = FALSE, + !.epoch_start_ns = 0, + !.k_zero = TRUE] + IN + /\ ll.kind = "timeout" + /\ OkParams(ll) + /\ LastTimeOk(st0, ll.time_ns) + /\ EnsureParamsOk(stT, ll) + /\ ~Has(ll, "acked_segs") + /\ ~Has(ll, "rtt_ns") + /\ ll.cwnd_bytes = st2.cwnd_bytes + /\ ll.ssthresh_bytes = st2.ssthresh_bytes + /\ ll.w_max_bytes = st2.w_max_bytes + /\ ll.w_last_max_bytes = st2.w_last_max_bytes + /\ ~Has(ll, "epoch_start_ns") + /\ l' = l + 1 + /\ flow' = [flow EXCEPT ![eid] = st2] + +Next == Ack \/ Congestion \/ Timeout + +TraceSpec == Init /\ [][Next]_Vars + +ProgressOk == IF l <= LenTrace THEN ENABLED Next ELSE TRUE + +============================================================================= diff --git a/tla/DcqcnTrace.cfg b/tla/DcqcnTrace.cfg new file mode 100644 index 00000000..dab6cf84 --- /dev/null +++ b/tla/DcqcnTrace.cfg @@ -0,0 +1,3 @@ +SPECIFICATION TraceSpec +INVARIANT ProgressOk +CHECK_DEADLOCK FALSE diff --git a/tla/DcqcnTrace.tla b/tla/DcqcnTrace.tla new file mode 100644 index 00000000..656e335d --- /dev/null +++ b/tla/DcqcnTrace.tla @@ -0,0 +1,311 @@ +------------------------------ MODULE DcqcnTrace ------------------------------ +\* Trace validation baseline for Days. +\* +\* This module is intended to mirror the checks in `lean/LeanGuard/DcqcnEventLog.lean`: +\* - canonical total order by (time_ns, event_id) +\* - CNP packet field constraints +\* - sink CNP interval gating + pending pairing +\* - source parameter constancy + time monotonicity +\* - replay-like alpha/rate updates (in the integer domain) with snapshot equality +\* +\* Trace loading (TLC): this module expects a companion module named `TraceData` that +\* defines `Trace` as a sequence of records (one per CSV row). The intended workflow is: +\* +\* - export `dcqcn_events.csv` in canonical order (sort by `(time_ns,event_id)`) +\* - generate `TraceData.tla` next to this module +\* - run TLC on this module. +\* +\* IMPORTANT: `TraceData.tla` is rescaled to fit TLC's 32-bit integers: +\* - `*_ns` fields are stored in microseconds +\* - `*_bps` fields are stored in units of 10 Mbps +\* - `*_ppb` fields are stored in permille (PPB == 1000) + +EXTENDS Naturals, Integers, Sequences, TLC, FiniteSets, TraceData + +PPB == 1000 +PPB2 == PPB * PPB + +LenTrace == Len(Trace) + +Key(rec) == <> +KeyLt(k1, k2) == + (k1[1] < k2[1]) \/ (k1[1] = k2[1] /\ k1[2] < k2[2]) + +TraceOk == + IF LenTrace <= 1 THEN + TRUE + ELSE + \A i \in 1..(LenTrace - 1) : KeyLt(Key(Trace[i]), Key(Trace[i + 1])) + +EndpointIds == { Trace[i].endpoint_id : i \in 1..LenTrace } + +CnpIndices == { i \in 1..LenTrace : Trace[i].kind \in {"cnp_sent", "cnp_recv"} } + +PendingKeys == + { <> : i \in CnpIndices } + +Has(ll, field) == field \in DOMAIN ll + +RoundDiv(n, d) == (n + d \div 2) \div d + +ClampMin(x, lo) == IF x < lo THEN lo ELSE x +ClampMax(x, hi) == IF x < hi THEN x ELSE hi + +AbsDiff(a, b) == IF a >= b THEN a - b ELSE b - a +ApproxEq(a, b, eps) == AbsDiff(a, b) <= eps + +MatchOptNat(ll, field, hasVal, val) == + IF hasVal THEN + /\ Has(ll, field) + /\ ll[field] = val + ELSE + ~Has(ll, field) + +OkSrcParams(p) == + /\ p.g_ppb <= PPB + /\ p.mi_ppb <= PPB + /\ p.min_rate_bps <= p.init_rate_bps + /\ p.init_rate_bps <= p.max_rate_bps + +DefaultSrc == + [ present |-> FALSE, + flow_id |-> 0, + cnp_interval_ns |-> 0, + g_ppb |-> 0, + mi_ppb |-> 0, + init_rate_bps |-> 0, + min_rate_bps |-> 0, + max_rate_bps |-> 0, + ai_rate_bps |-> 0, + hai_rate_bps |-> 0, + alpha_ppb |-> 0, + rate_bps |-> 0, + cnp_seen |-> FALSE, + has_last_cnp |-> FALSE, + last_cnp_ns |-> 0, + has_last_time |-> FALSE, + last_time_ns |-> 0 ] + +DefaultSink == + [ present |-> FALSE, + flow_id |-> 0, + cnp_interval_ns |-> 0, + cnp_priority |-> 0, + has_last_cnp |-> FALSE, + last_cnp_ns |-> 0, + has_last_time |-> FALSE, + last_time_ns |-> 0 ] + +DefaultPending == + [ present |-> FALSE, + sent_time_ns |-> 0, + sent_event_id |-> 0 ] + +VARIABLES l, src, sink, pending + +Vars == <> + +Init == + /\ l = 1 + /\ TraceOk + /\ src = [e \in EndpointIds |-> DefaultSrc] + /\ sink = [e \in EndpointIds |-> DefaultSink] + /\ pending = [k \in PendingKeys |-> DefaultPending] + +InitSrcFrom(ll) == + [ present |-> TRUE, + flow_id |-> ll.flow_id, + cnp_interval_ns |-> ll.cnp_interval_ns, + g_ppb |-> ll.g_ppb, + mi_ppb |-> ll.mi_ppb, + init_rate_bps |-> ll.init_rate_bps, + min_rate_bps |-> ll.min_rate_bps, + max_rate_bps |-> ll.max_rate_bps, + ai_rate_bps |-> ll.ai_rate_bps, + hai_rate_bps |-> ll.hai_rate_bps, + alpha_ppb |-> 0, + rate_bps |-> ll.init_rate_bps, + cnp_seen |-> FALSE, + has_last_cnp |-> FALSE, + last_cnp_ns |-> 0, + has_last_time |-> FALSE, + last_time_ns |-> 0 ] + +InitSinkFrom(ll) == + [ present |-> TRUE, + flow_id |-> ll.flow_id, + cnp_interval_ns |-> ll.cnp_interval_ns, + cnp_priority |-> ll.cnp_priority, + has_last_cnp |-> FALSE, + last_cnp_ns |-> 0, + has_last_time |-> FALSE, + last_time_ns |-> 0 ] + +CnpPacketOk(ll) == + /\ Has(ll, "pkt_id") + /\ Has(ll, "pkt_flow_id") + /\ ll.pkt_flow_id = ll.flow_id + /\ Has(ll, "cnp_size_b") /\ ll.cnp_size_b = 64 + /\ Has(ll, "cnp_ecn") /\ ll.cnp_ecn = "NotEct" + /\ Has(ll, "cnp_cwr") /\ ll.cnp_cwr = FALSE + /\ Has(ll, "cnp_last_packet") /\ ll.cnp_last_packet = FALSE + +CnpSent == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + eid == ll.endpoint_id + fid == ll.flow_id + pktId == ll.pkt_id + pkey == <> + sk0 == sink[eid] + sk1 == IF sk0.present THEN sk0 ELSE InitSinkFrom(ll) + pk0 == pending[pkey] + IN + /\ ll.kind = "cnp_sent" + /\ CnpPacketOk(ll) + /\ Has(ll, "trigger_ecn") /\ ll.trigger_ecn = "Ce" + /\ Has(ll, "cnp_priority") + /\ Has(ll, "cnp_interval_ns") + /\ Has(ll, "last_cnp_ns") /\ ll.last_cnp_ns = ll.time_ns + /\ IF sk0.present THEN + /\ sk0.flow_id = fid + /\ sk0.cnp_interval_ns = ll.cnp_interval_ns + /\ sk0.cnp_priority = ll.cnp_priority + ELSE TRUE + /\ ~sk1.has_last_time \/ sk1.last_time_ns <= ll.time_ns + /\ ~sk1.has_last_cnp \/ sk1.last_cnp_ns + sk1.cnp_interval_ns <= ll.time_ns + /\ ~pk0.present + /\ l' = l + 1 + /\ src' = src + /\ sink' = + [sink EXCEPT ![eid] = + [sk1 EXCEPT + !.present = TRUE, + !.has_last_time = TRUE, + !.last_time_ns = ll.time_ns, + !.has_last_cnp = TRUE, + !.last_cnp_ns = ll.time_ns]] + /\ pending' = + [pending EXCEPT ![pkey] = + [pk0 EXCEPT + !.present = TRUE, + !.sent_time_ns = ll.time_ns, + !.sent_event_id = ll.event_id]] + +CnpRecv == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + eid == ll.endpoint_id + fid == ll.flow_id + pktId == ll.pkt_id + pkey == <> + pk0 == pending[pkey] + sentKey == <> + recvKey == Key(ll) + sPre0 == src[eid] + s0 == IF sPre0.present THEN sPre0 ELSE InitSrcFrom(ll) + applied == ~s0.has_last_cnp \/ (s0.last_cnp_ns + s0.cnp_interval_ns <= ll.time_ns) + alpha1 == + IF applied THEN + RoundDiv((PPB - s0.g_ppb) * s0.alpha_ppb + s0.g_ppb * PPB, PPB) + ELSE + s0.alpha_ppb + decNumer == PPB2 - (s0.mi_ppb * alpha1) + rateDecr == + IF applied THEN + RoundDiv(s0.rate_bps * decNumer, PPB2) + ELSE + s0.rate_bps + rate1 == ClampMin(rateDecr, s0.min_rate_bps) + seen1 == IF applied THEN TRUE ELSE s0.cnp_seen + hasLastCnp1 == IF applied THEN TRUE ELSE s0.has_last_cnp + lastCnp1 == IF applied THEN ll.time_ns ELSE s0.last_cnp_ns + s1 == + [s0 EXCEPT + !.present = TRUE, + !.alpha_ppb = alpha1, + !.rate_bps = rate1, + !.cnp_seen = seen1, + !.has_last_cnp = hasLastCnp1, + !.last_cnp_ns = lastCnp1, + !.has_last_time = TRUE, + !.last_time_ns = ll.time_ns] + IN + /\ ll.kind = "cnp_recv" + /\ CnpPacketOk(ll) + /\ pk0.present + /\ KeyLt(sentKey, recvKey) + /\ IF sPre0.present THEN + /\ sPre0.flow_id = ll.flow_id + /\ sPre0.cnp_interval_ns = ll.cnp_interval_ns + /\ sPre0.g_ppb = ll.g_ppb + /\ sPre0.mi_ppb = ll.mi_ppb + /\ sPre0.init_rate_bps = ll.init_rate_bps + /\ sPre0.min_rate_bps = ll.min_rate_bps + /\ sPre0.max_rate_bps = ll.max_rate_bps + /\ sPre0.ai_rate_bps = ll.ai_rate_bps + /\ sPre0.hai_rate_bps = ll.hai_rate_bps + ELSE TRUE + /\ OkSrcParams(ll) + /\ ~s0.has_last_time \/ s0.last_time_ns <= ll.time_ns + /\ Has(ll, "alpha_ppb") /\ ApproxEq(ll.alpha_ppb, alpha1, 1) + /\ Has(ll, "rate_bps") /\ ApproxEq(ll.rate_bps, rate1, 1) + /\ Has(ll, "cnp_seen") /\ ll.cnp_seen = seen1 + /\ MatchOptNat(ll, "last_cnp_ns", hasLastCnp1, lastCnp1) + /\ l' = l + 1 + /\ sink' = sink + /\ src' = [src EXCEPT ![eid] = s1] + /\ pending' = [pending EXCEPT ![pkey] = [pk0 EXCEPT !.present = FALSE]] + +TimerTick == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + eid == ll.endpoint_id + sPre0 == src[eid] + s0 == IF sPre0.present THEN sPre0 ELSE InitSrcFrom(ll) + decNumer == (PPB - s0.g_ppb) * s0.alpha_ppb + alphaDecPpb == RoundDiv(decNumer, PPB) + alphaDecIsSmall == (decNumer * 10) < PPB2 + inc == IF alphaDecIsSmall THEN s0.hai_rate_bps ELSE s0.ai_rate_bps + rateInc == ClampMax(s0.rate_bps + inc, s0.max_rate_bps) + alpha1 == IF s0.cnp_seen THEN s0.alpha_ppb ELSE alphaDecPpb + rate1 == IF s0.cnp_seen THEN s0.rate_bps ELSE rateInc + s1 == + [s0 EXCEPT + !.present = TRUE, + !.alpha_ppb = alpha1, + !.rate_bps = rate1, + !.cnp_seen = FALSE, + !.has_last_time = TRUE, + !.last_time_ns = ll.time_ns] + IN + /\ ll.kind = "timer_tick" + /\ IF sPre0.present THEN + /\ sPre0.flow_id = ll.flow_id + /\ sPre0.cnp_interval_ns = ll.cnp_interval_ns + /\ sPre0.g_ppb = ll.g_ppb + /\ sPre0.mi_ppb = ll.mi_ppb + /\ sPre0.init_rate_bps = ll.init_rate_bps + /\ sPre0.min_rate_bps = ll.min_rate_bps + /\ sPre0.max_rate_bps = ll.max_rate_bps + /\ sPre0.ai_rate_bps = ll.ai_rate_bps + /\ sPre0.hai_rate_bps = ll.hai_rate_bps + ELSE TRUE + /\ OkSrcParams(ll) + /\ ~s0.has_last_time \/ s0.last_time_ns <= ll.time_ns + /\ Has(ll, "alpha_ppb") /\ ApproxEq(ll.alpha_ppb, alpha1, 1) + /\ Has(ll, "rate_bps") /\ ApproxEq(ll.rate_bps, rate1, 1) + /\ Has(ll, "cnp_seen") /\ ll.cnp_seen = FALSE + /\ MatchOptNat(ll, "last_cnp_ns", s0.has_last_cnp, s0.last_cnp_ns) + /\ l' = l + 1 + /\ sink' = sink + /\ pending' = pending + /\ src' = [src EXCEPT ![eid] = s1] + +Next == CnpSent \/ CnpRecv \/ TimerTick + +TraceSpec == Init /\ [][Next]_Vars + +ProgressOk == IF l <= LenTrace THEN ENABLED Next ELSE TRUE + +=============================================================================== diff --git a/tla/DrrTrace.cfg b/tla/DrrTrace.cfg new file mode 100644 index 00000000..dab6cf84 --- /dev/null +++ b/tla/DrrTrace.cfg @@ -0,0 +1,3 @@ +SPECIFICATION TraceSpec +INVARIANT ProgressOk +CHECK_DEADLOCK FALSE diff --git a/tla/DrrTrace.tla b/tla/DrrTrace.tla new file mode 100644 index 00000000..2ef73ddf --- /dev/null +++ b/tla/DrrTrace.tla @@ -0,0 +1,269 @@ +------------------------------ MODULE DrrTrace ------------------------------ +\* Trace validation baseline for Days DRR (Deficit Round Robin) scheduling. +\* +\* Intended to mirror: +\* - `lean/LeanGuard/Drr/Semantics.lean` +\* - `lean/LeanGuard/DrrEventLog.lean` +\* +\* This module expects a companion module named `TraceData` defining `Trace`. +\* +\* IMPORTANT: `TraceData` is rescaled to fit TLC's 32-bit integers: +\* - `*_ns` fields are stored in microseconds +\* - `*_ppb` fields are stored in permille (unused here) +\* - `*_bps` fields are stored in units of 10 Mbps (only checked for constancy) + +EXTENDS Naturals, Integers, Sequences, TLC, FiniteSets, TraceData + +LenTrace == Len(Trace) + +Key(rec) == <> +KeyLt(k1, k2) == + (k1[1] < k2[1]) \/ (k1[1] = k2[1] /\ k1[2] < k2[2]) + +TraceOk == + IF LenTrace <= 1 THEN + TRUE + ELSE + \A i \in 1..(LenTrace - 1) : KeyLt(Key(Trace[i]), Key(Trace[i + 1])) + +Has(ll, field) == field \in DOMAIN ll + +SchedulerIds == { Trace[i].scheduler_id : i \in 1..LenTrace } + +MaxOfSet(S) == CHOOSE m \in S : \A x \in S : x <= m + +MaxClassCount == + IF LenTrace = 0 THEN 0 ELSE MaxOfSet({ Trace[i].class_count : i \in 1..LenTrace }) + +AllClassIds == + IF MaxClassCount = 0 THEN {0} ELSE 0..(MaxClassCount - 1) + +DefaultPacket == [ packet_id |-> 0, flow_id |-> 0, size_bytes |-> 0 ] + +DefaultSched == + [ class_count |-> 0, + rate_bps |-> 0, + quantum |-> [cid \in AllClassIds |-> 0], + deficit |-> [cid \in AllClassIds |-> 0], + queues |-> [cid \in AllClassIds |-> <<>>], + current_queue |-> 0, + packets_waiting |-> 0, + batch_has |-> FALSE, + batch_id |-> 0, + batch_class_has |-> FALSE, + batch_class |-> 0, + batch_next_has |-> FALSE, + batch_next_start_ns |-> 0, + last_time_has |-> FALSE, + last_time_ns |-> 0 ] + +QueueEmpty(st, cid) == Len(st.queues[cid]) = 0 + +WrapOk(st) == + \A cid \in 0..(st.class_count - 1) : + QueueEmpty(st, cid) \/ st.quantum[cid] > 0 + +UpdateDeficits(st) == + [cid \in AllClassIds |-> + IF cid < st.class_count THEN + IF QueueEmpty(st, cid) THEN + 0 + ELSE + st.deficit[cid] + st.quantum[cid] + ELSE + st.deficit[cid]] + +NextQueueState(st) == + IF st.current_queue + 1 < st.class_count THEN + [st EXCEPT !.current_queue = st.current_queue + 1] + ELSE + [st EXCEPT !.current_queue = 0, !.deficit = UpdateDeficits(st)] + +RECURSIVE AdvanceQueueOk(_, _), AdvanceQueueState(_, _) + +AdvanceQueueOk(st, steps) == + IF steps = 0 THEN + TRUE + ELSE + IF st.current_queue + 1 < st.class_count THEN + AdvanceQueueOk([st EXCEPT !.current_queue = st.current_queue + 1], steps - 1) + ELSE + /\ WrapOk(st) + /\ AdvanceQueueOk([st EXCEPT !.current_queue = 0, !.deficit = UpdateDeficits(st)], steps - 1) + +AdvanceQueueState(st, steps) == + IF steps = 0 THEN + st + ELSE + IF st.current_queue + 1 < st.class_count THEN + AdvanceQueueState([st EXCEPT !.current_queue = st.current_queue + 1], steps - 1) + ELSE + AdvanceQueueState([st EXCEPT !.current_queue = 0, !.deficit = UpdateDeficits(st)], steps - 1) + +LastTimeOk(st, t) == ~st.last_time_has \/ st.last_time_ns <= t + +UpdateLastTimeState(st, t) == + [st EXCEPT !.last_time_has = TRUE, !.last_time_ns = t] + +EnsureClassCountOk(st, n) == n > 0 /\ (st.class_count = 0 \/ st.class_count = n) + +EnsureClassCountState(st, n) == + IF st.class_count = 0 THEN + [st EXCEPT !.class_count = n] + ELSE + st + +EnsureRateOk(st, r) == r > 0 /\ (st.rate_bps = 0 \/ st.rate_bps = r) + +EnsureRateState(st, r) == + IF st.rate_bps = 0 THEN + [st EXCEPT !.rate_bps = r] + ELSE + st + +EnsureQuantumOk(st, cid, q) == q > 0 /\ (st.quantum[cid] = 0 \/ st.quantum[cid] = q) + +EnsureQuantumState(st, cid, q) == + IF st.quantum[cid] = 0 THEN + [st EXCEPT !.quantum[cid] = q] + ELSE + st + +ApplyBatchOk(st, batchId, timeNs) == + /\ ~st.batch_has \/ batchId >= st.batch_id + /\ LET st0 == + IF ~st.batch_has \/ batchId # st.batch_id THEN + [st EXCEPT + !.batch_has = TRUE, + !.batch_id = batchId, + !.batch_class_has = FALSE, + !.batch_next_has = FALSE] + ELSE + [st EXCEPT !.batch_has = TRUE, !.batch_id = batchId] + IN + IF ~st0.batch_next_has THEN + TRUE + ELSE + st0.batch_next_start_ns = timeNs + +ApplyBatchState(st, batchId, timeNs) == + LET st0 == + IF ~st.batch_has \/ batchId # st.batch_id THEN + [st EXCEPT + !.batch_has = TRUE, + !.batch_id = batchId, + !.batch_class_has = FALSE, + !.batch_next_has = FALSE] + ELSE + [st EXCEPT !.batch_has = TRUE, !.batch_id = batchId] + IN + IF ~st0.batch_next_has THEN + [st0 EXCEPT !.batch_next_has = TRUE, !.batch_next_start_ns = timeNs] + ELSE + st0 + +VARIABLES l, sched + +Vars == <> + +Init == + /\ l = 1 + /\ TraceOk + /\ sched = [sid \in SchedulerIds |-> DefaultSched] + +Enqueue == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + sid == ll.scheduler_id + st0 == sched[sid] + stT == UpdateLastTimeState(st0, ll.time_ns) + st1 == EnsureClassCountState(stT, ll.class_count) + st2 == EnsureRateState(st1, ll.rate_bps) + st3 == EnsureQuantumState(st2, ll.class_id, ll.quantum_bytes) + pkt == [packet_id |-> ll.packet_id, flow_id |-> ll.flow_id, size_bytes |-> ll.size_bytes] + q0 == st3.queues[ll.class_id] + q1 == Append(q0, pkt) + st4 == [st3 EXCEPT + !.queues[ll.class_id] = q1, + !.packets_waiting = st3.packets_waiting + 1] + IN + /\ ll.kind = "enqueue" + /\ LastTimeOk(st0, ll.time_ns) + /\ EnsureClassCountOk(stT, ll.class_count) + /\ EnsureRateOk(st1, ll.rate_bps) + /\ EnsureQuantumOk(st2, ll.class_id, ll.quantum_bytes) + /\ ~Has(ll, "batch_id") + /\ ~Has(ll, "departure_time_ns") + /\ ll.scan_steps = 0 + /\ ll.size_bytes > 0 + /\ ll.class_id < st3.class_count + /\ ll.current_queue < st3.class_count + /\ ll.current_queue = st3.current_queue + /\ ll.deficit_bytes = st4.deficit[ll.class_id] + /\ l' = l + 1 + /\ sched' = [sched EXCEPT ![sid] = st4] + +Schedule == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + sid == ll.scheduler_id + st0 == sched[sid] + stT == UpdateLastTimeState(st0, ll.time_ns) + st1 == EnsureClassCountState(stT, ll.class_count) + st2 == EnsureRateState(st1, ll.rate_bps) + st3 == EnsureQuantumState(st2, ll.class_id, ll.quantum_bytes) + batchId == ll.batch_id + dep == ll.departure_time_ns + stA == ApplyBatchState(st3, batchId, ll.time_ns) + stB == AdvanceQueueState(stA, ll.scan_steps) + q == stB.queues[ll.class_id] + headPkt == Head(q) + deficit0 == stB.deficit[ll.class_id] + qTail == Tail(q) + stC0 == + IF stB.batch_class_has THEN + stB + ELSE + [stB EXCEPT !.batch_class_has = TRUE, !.batch_class = ll.class_id] + stC == + [stC0 EXCEPT + !.queues[ll.class_id] = qTail, + !.packets_waiting = stC0.packets_waiting - 1, + !.deficit[ll.class_id] = deficit0 - ll.size_bytes, + !.batch_next_has = TRUE, + !.batch_next_start_ns = dep] + IN + /\ ll.kind = "schedule" + /\ LastTimeOk(st0, ll.time_ns) + /\ EnsureClassCountOk(stT, ll.class_count) + /\ EnsureRateOk(st1, ll.rate_bps) + /\ EnsureQuantumOk(st2, ll.class_id, ll.quantum_bytes) + /\ Has(ll, "batch_id") + /\ Has(ll, "departure_time_ns") + /\ dep >= ll.time_ns + /\ ll.size_bytes > 0 + /\ ll.class_id < st3.class_count + /\ ll.current_queue < st3.class_count + /\ st3.packets_waiting > 0 + /\ ApplyBatchOk(st3, batchId, ll.time_ns) + /\ AdvanceQueueOk(stA, ll.scan_steps) + /\ stB.current_queue = ll.class_id + /\ ~stB.batch_class_has \/ stB.batch_class = ll.class_id + /\ Len(q) > 0 + /\ headPkt.packet_id = ll.packet_id + /\ headPkt.flow_id = ll.flow_id + /\ headPkt.size_bytes = ll.size_bytes + /\ deficit0 > 0 + /\ ll.size_bytes <= deficit0 + /\ ll.current_queue = stC.current_queue + /\ ll.deficit_bytes = stC.deficit[ll.class_id] + /\ l' = l + 1 + /\ sched' = [sched EXCEPT ![sid] = stC] + +Next == Enqueue \/ Schedule + +TraceSpec == Init /\ [][Next]_Vars + +ProgressOk == IF l <= LenTrace THEN ENABLED Next ELSE TRUE + +============================================================================= diff --git a/tla/PfcTrace.cfg b/tla/PfcTrace.cfg new file mode 100644 index 00000000..dab6cf84 --- /dev/null +++ b/tla/PfcTrace.cfg @@ -0,0 +1,3 @@ +SPECIFICATION TraceSpec +INVARIANT ProgressOk +CHECK_DEADLOCK FALSE diff --git a/tla/PfcTrace.tla b/tla/PfcTrace.tla new file mode 100644 index 00000000..81da261e --- /dev/null +++ b/tla/PfcTrace.tla @@ -0,0 +1,129 @@ +------------------------------ MODULE PfcTrace ------------------------------ +\* Trace validation baseline for Days PFC (Priority Flow Control). +\* +\* Intended to mirror: +\* - `lean/LeanGuard/Pfc/Semantics.lean` +\* - `lean/LeanGuard/PfcEventLog.lean` +\* +\* This module expects a companion module named `TraceData` defining `Trace`. +\* +\* IMPORTANT: `TraceData` is rescaled to fit TLC's 32-bit integers: +\* - `*_ns` fields are stored in microseconds +\* - `*_ppb` fields are stored in permille (unused here) +\* - `*_bps` fields are stored in units of 10 Mbps (unused here) + +EXTENDS Naturals, Integers, Sequences, TLC, FiniteSets, TraceData + +LenTrace == Len(Trace) + +Key(rec) == <> +KeyLt(k1, k2) == + (k1[1] < k2[1]) \/ (k1[1] = k2[1] /\ k1[2] < k2[2]) + +TraceOk == + IF LenTrace <= 1 THEN + TRUE + ELSE + \A i \in 1..(LenTrace - 1) : KeyLt(Key(Trace[i]), Key(Trace[i + 1])) + +Has(ll, field) == field \in DOMAIN ll + +OneHot(prio) == 2^prio + +PendingKeys == { <> : i \in 1..LenTrace } +PauseKeys == { <> : i \in 1..LenTrace } + +DefaultPending == + [ present |-> FALSE, + sent_time_ns |-> 0, + sent_event_id |-> 0, + sender_id |-> 0, + receiver_id |-> 0, + class_enable |-> 0, + pause_quanta |-> 0 ] + +VARIABLES l, pending, paused + +Vars == <> + +Init == + /\ l = 1 + /\ TraceOk + /\ pending = [k \in PendingKeys |-> DefaultPending] + /\ paused = [k \in PauseKeys |-> FALSE] + +CheckCommon(ll) == + /\ ll.priority < 8 + /\ ll.pause_quanta <= 65535 + /\ ll.class_enable = OneHot(ll.priority) + +PfcSent == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + pkey == <> + wasPaused == paused[<>] + pk0 == pending[pkey] + occ == ll.queue_occupancy_bytes + xoff == ll.xoff_threshold_bytes + xon == ll.xon_threshold_bytes + cap == ll.buffer_capacity_bytes + IN + /\ ll.kind = "pfc_sent" + /\ CheckCommon(ll) + /\ Has(ll, "queue_occupancy_bytes") + /\ Has(ll, "xoff_threshold_bytes") + /\ Has(ll, "xon_threshold_bytes") + /\ Has(ll, "buffer_capacity_bytes") + /\ xon <= xoff + /\ cap = 0 \/ occ <= cap + /\ ~pk0.present + /\ IF ll.pause_quanta = 0 THEN + /\ wasPaused + /\ occ <= xon + ELSE + IF wasPaused THEN + occ > xon + ELSE + occ >= xoff + /\ l' = l + 1 + /\ paused' = + IF ll.pause_quanta = 0 THEN + [paused EXCEPT ![<>] = FALSE] + ELSE + [paused EXCEPT ![<>] = TRUE] + /\ pending' = + [pending EXCEPT ![pkey] = + [pk0 EXCEPT + !.present = TRUE, + !.sent_time_ns = ll.time_ns, + !.sent_event_id = ll.event_id, + !.sender_id = ll.sender_id, + !.receiver_id = ll.receiver_id, + !.class_enable = ll.class_enable, + !.pause_quanta = ll.pause_quanta]] + +PfcRecv == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + pkey == <> + pk0 == pending[pkey] + IN + /\ ll.kind = "pfc_recv" + /\ CheckCommon(ll) + /\ pk0.present + /\ KeyLt(<>, <>) + /\ ll.sender_id = pk0.sender_id + /\ ll.receiver_id = pk0.receiver_id + /\ ll.class_enable = pk0.class_enable + /\ ll.pause_quanta = pk0.pause_quanta + /\ l' = l + 1 + /\ paused' = paused + /\ pending' = [pending EXCEPT ![pkey] = [pk0 EXCEPT !.present = FALSE]] + +Next == PfcSent \/ PfcRecv + +TraceSpec == Init /\ [][Next]_Vars + +ProgressOk == IF l <= LenTrace THEN ENABLED Next ELSE TRUE + +============================================================================= diff --git a/tla/README.md b/tla/README.md new file mode 100644 index 00000000..a27055b7 --- /dev/null +++ b/tla/README.md @@ -0,0 +1,97 @@ +# TLC baseline (trace validation) + +This directory holds a **TLA+/TLC trace-validation baseline** for Days, intended to be comparable to LeanGuard as described in `ideas/comparison.md`. + +## Key idea + +- Days emits `*_events.csv`. +- We export: + - `*_events.csv` → `*.ndjson` (lossless; used for diagnostics and “first failing row” reporting) + - `*_events.csv` → a generated `TraceData.tla` module that defines `Trace == << ... >>` for TLC +- TLC runs a protocol-specific trace harness against `TraceData.tla`. + +Currently implemented trace validators: + +- `tla/DcqcnTrace.tla` (DCQCN) +- `tla/AqmTrace.tla` (AQM drop/mark decision witnesses) +- `tla/PfcTrace.tla` (PFC pause/resume pairing + hysteresis) +- `tla/WfqTrace.tla` (WFQ schedule/depart replay in scaled integer time) +- `tla/DrrTrace.tla` (DRR schedule replay) +- `tla/CubicTrace.tla` (TCP CUBIC, slow-start + congestion-avoidance ACK growth via a fixed-point approximation) + +### Why `TraceData.tla` (and why rescaling)? + +In practice, the released `tla2tools.jar` (TLC) has two constraints that matter for Days traces: + +- TLC integers are **32-bit** (`[-2^31, 2^31]`), so raw `rate_bps = 10_000_000_000` (10Gbps) does not fit. +- The JSON/NDJSON trace-ingestion modules used in trace-validation research (`Json` / `IOUtils` / `ndJsonDeserialize`) are **not reliably available in released jars**, so we avoid depending on them for the baseline. + +To keep the baseline reproducible, `leanguard-run` generates `TraceData.tla` and **rescales** large numeric fields to fit TLC. + +## Tooling + +Run the baseline via the normal runner (recommended): + +```bash +cargo run --bin leanguard-run -- \ + --config configs/dcqcn_simple.toml \ + --mode check-only \ + --checker-dir lean/.lake/build/bin \ + --tlc-check --tlc-jar /path/to/tla2tools.jar +``` + +This: + +- runs Days (or reuses an existing `log_path` depending on `--mode`) +- exports `*.ndjson` next to each `*_events.csv` (lossless) +- creates a TLC workspace under `/tlc//spec/` containing: + - the TLA module (e.g. `DcqcnTrace.tla`) + - the `.cfg` + - `TraceData.tla` (generated from the CSV, rescaled) + +You can also export a standalone `TraceData.tla` for a single CSV: + +```bash +cargo run --bin days-trace-export -- --format tla --input /dcqcn_events.csv +``` + +### Rescaling rules (for `TraceData.tla` only) + +`TraceData.tla` stores: + +- `*_ns` fields in **microseconds** (`round(ns / 1_000)`) +- `*_bps` fields in **10 Mbps units** (`round(bps / 10_000_000)`) +- `*_ppb` fields in **permille units** (`round(ppb / 1_000_000)`) + +The corresponding TLA specs use the same scaled units (e.g. `PPB == 1000` in `DcqcnTrace.tla`). + +Because rescaling loses precision, `DcqcnTrace.tla` uses a small tolerance for snapshot equality on scaled `alpha_ppb` and `rate_bps` (currently `±1` in the scaled units). + +`WfqTrace.tla` also uses a small tolerance (`±1` microsecond) when comparing the logged `vtime_ns` / `finish_time_ns` fields against the replay computation, because both the trace export and the scheduler logging round floating-point values. + +### Note: `CubicTrace.tla` uses a fixed-point approximation + +`CubicTrace.tla` currently validates: + +- parameter stability + time monotonicity, +- slow-start ACK updates (`cwnd_bytes` increments), +- congestion-avoidance ACK updates via a scaled integer approximation of the RFC 8312 update, +- byte-level congestion/timeout reductions, + +Because the trace export rescales times and the reference implementation uses floating-point arithmetic, `CubicTrace.tla` compares the computed `cwnd_bytes` to the logged value with a small tolerance (see `CWND_BYTES_TOL` in `tla/CubicTrace.tla`). + +## Running TLC manually (optional) + +If you want to run TLC directly, run it inside the generated TLC workspace so `TraceData.tla` is visible. +For example: + +```bash +cd /tlc/DcqcnTrace/spec +java -cp /path/to/tla2tools.jar tlc2.TLC -config DcqcnTrace.cfg DcqcnTrace.tla +``` + +## Notes + +- For trace validation, DFS can help performance: + - `java -Dtlc2.tool.queue.IStateQueue=StateDeque -cp ... tlc2.TLC ...` +- We disable deadlock checking (`CHECK_DEADLOCK FALSE`) and use TLC’s reported diameter/depth as the signal for how many trace steps were matched (see `leanguard-run`’s `matched_prefix` / `first_failure` fields). diff --git a/tla/WfqTrace.cfg b/tla/WfqTrace.cfg new file mode 100644 index 00000000..dab6cf84 --- /dev/null +++ b/tla/WfqTrace.cfg @@ -0,0 +1,3 @@ +SPECIFICATION TraceSpec +INVARIANT ProgressOk +CHECK_DEADLOCK FALSE diff --git a/tla/WfqTrace.tla b/tla/WfqTrace.tla new file mode 100644 index 00000000..1888524f --- /dev/null +++ b/tla/WfqTrace.tla @@ -0,0 +1,279 @@ +------------------------------ MODULE WfqTrace ------------------------------ +\* Trace validation baseline for Days WFQ (Weighted Fair Queueing). +\* +\* Intended to mirror: +\* - `lean/LeanGuard/Wfq/Semantics.lean` +\* - `lean/LeanGuard/WfqEventLog.lean` +\* - the corresponding implementation in `src/schedulers/wfq.rs` (under `--features lean`). +\* +\* This module expects a companion module named `TraceData` defining `Trace`. +\* +\* IMPORTANT: `TraceData` is rescaled to fit TLC's 32-bit integers: +\* - `*_ns` fields are stored in microseconds (rounded) +\* - `*_bps` fields are stored in units of 10 Mbps (rounded) +\* +\* This spec mirrors the Float-based implementation using **integer microseconds**: +\* - virtual time `vtime_ns` is interpreted as microseconds of virtual time +\* - finish/departure times are interpreted as microseconds +\* - service time is computed in microseconds using the scaled rate: +\* 10 Mbps == 10 bits/us, so service_us ~= bits / (rate_bps_scaled * 10 * weight) +\* +\* Because scaling introduces rounding, we accept a small tolerance on reported `vtime_ns` +\* and `finish_time_ns` (currently ±1 microsecond). + +EXTENDS Naturals, Integers, Sequences, TLC, FiniteSets, TraceData + +LenTrace == Len(Trace) + +Key(rec) == <> +KeyLt(k1, k2) == + (k1[1] < k2[1]) \/ (k1[1] = k2[1] /\ k1[2] < k2[2]) + +TraceOk == + IF LenTrace <= 1 THEN + TRUE + ELSE + \A i \in 1..(LenTrace - 1) : KeyLt(Key(Trace[i]), Key(Trace[i + 1])) + +Has(ll, field) == field \in DOMAIN ll + +RoundDiv(n, d) == (n + d \div 2) \div d + +AbsDiff(a, b) == IF a >= b THEN a - b ELSE b - a +ApproxEq(a, b, eps) == AbsDiff(a, b) <= eps + +SchedulerIds == { Trace[i].scheduler_id : i \in 1..LenTrace } +ClassIds == { Trace[i].class_id : i \in 1..LenTrace } + +PktKeys == { <> : i \in 1..LenTrace } + +DefaultPkt == + [ present |-> FALSE, + class_id |-> 0, + size_bytes |-> 0, + finish_time_ns |-> 0 ] + +DefaultPending == + [ present |-> FALSE, + key |-> <<0, 0, 0>>, + class_id |-> 0, + size_bytes |-> 0, + finish_time_ns |-> 0, + departure_time_ns |-> 0, + schedule_idx |-> 0 ] + +DefaultSched == + [ rate_bps |-> 0, + vtime_ns |-> 0, + last_updated_ns |-> 0, + active_weight_sum |-> 0, + last_time_has |-> FALSE, + last_time_ns |-> 0, + weights |-> [c \in ClassIds |-> 0], + flow_counts |-> [c \in ClassIds |-> 0], + finish_times |-> [c \in ClassIds |-> 0] ] + +QueuedKeysForSid(queue, sid) == + { k \in PktKeys : k[1] = sid /\ queue[k].present } + +MinOfSet(S) == + IF S = {} THEN + 0 + ELSE + CHOOSE m \in S : \A x \in S : m <= x + +MinFinish(queue, sid) == + LET S == { queue[k].finish_time_ns : k \in QueuedKeysForSid(queue, sid) } + IN MinOfSet(S) + +ServiceTimeUs(sizeBytes, rateBpsScaled, weight) == + RoundDiv(sizeBytes * 8, rateBpsScaled * 10 * weight) + +LastTimeOk(st, t) == ~st.last_time_has \/ st.last_time_ns <= t + +UpdateLastTime(st, t) == + [st EXCEPT !.last_time_has = TRUE, !.last_time_ns = t] + +EnsureRateOk(st, r) == r > 0 /\ (st.rate_bps = 0 \/ st.rate_bps = r) + +EnsureRateState(st, r) == + IF st.rate_bps = 0 THEN + [st EXCEPT !.rate_bps = r] + ELSE + st + +EnsureWeightOk(st, cid, w) == w > 0 /\ (st.weights[cid] = 0 \/ st.weights[cid] = w) + +EnsureWeightState(st, cid, w) == + IF st.weights[cid] = 0 THEN + [st EXCEPT !.weights[cid] = w] + ELSE + st + +VARIABLES l, sched, queue, pending + +Vars == <> + +Init == + /\ l = 1 + /\ TraceOk + /\ sched = [sid \in SchedulerIds |-> DefaultSched] + /\ queue = [k \in PktKeys |-> DefaultPkt] + /\ pending = [sid \in SchedulerIds |-> DefaultPending] + +Enqueue == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + sid == ll.scheduler_id + key == <> + st0 == sched[sid] + stT == UpdateLastTime(st0, ll.time_ns) + st1 == EnsureRateState(stT, ll.rate_bps) + st2 == EnsureWeightState(st1, ll.class_id, ll.weight) + pk0 == pending[sid] + q0 == queue[key] + wsum == st2.active_weight_sum + ftBase == IF wsum = 0 THEN [c \in ClassIds |-> 0] ELSE st2.finish_times + vBase == + IF wsum = 0 THEN + 0 + ELSE + st2.vtime_ns + RoundDiv(ll.time_ns - st2.last_updated_ns, wsum) + prevFinish == ftBase[ll.class_id] + vStart == IF vBase > prevFinish THEN vBase ELSE prevFinish + serviceUs == ServiceTimeUs(ll.size_bytes, st2.rate_bps, ll.weight) + finishUs == vStart + serviceUs + count0 == st2.flow_counts[ll.class_id] + count1 == count0 + 1 + wsum1 == IF count0 = 0 THEN wsum + ll.weight ELSE wsum + st3 == + [st2 EXCEPT + !.vtime_ns = vBase, + !.last_updated_ns = ll.time_ns, + !.active_weight_sum = wsum1, + !.flow_counts[ll.class_id] = count1, + !.finish_times = [ftBase EXCEPT ![ll.class_id] = finishUs]] + IN + /\ ll.kind = "enqueue" + /\ LastTimeOk(st0, ll.time_ns) + /\ EnsureRateOk(stT, ll.rate_bps) + /\ EnsureWeightOk(st1, ll.class_id, ll.weight) + /\ ll.size_bytes > 0 + /\ ~Has(ll, "departure_time_ns") + /\ ~q0.present + /\ ~pk0.present \/ pk0.key # key + /\ ApproxEq(ll.vtime_ns, vBase, 1) + /\ ApproxEq(ll.finish_time_ns, finishUs, 1) + /\ l' = l + 1 + /\ sched' = [sched EXCEPT ![sid] = st3] + /\ pending' = pending + /\ queue' = + [queue EXCEPT ![key] = + [q0 EXCEPT + !.present = TRUE, + !.class_id = ll.class_id, + !.size_bytes = ll.size_bytes, + !.finish_time_ns = ll.finish_time_ns]] + +Schedule == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + sid == ll.scheduler_id + dep == ll.departure_time_ns + key == <> + st0 == sched[sid] + stT == UpdateLastTime(st0, ll.time_ns) + st1 == EnsureRateState(stT, ll.rate_bps) + st2 == EnsureWeightState(st1, ll.class_id, ll.weight) + pk0 == pending[sid] + q0 == queue[key] + minFinish == MinFinish(queue, sid) + IN + /\ ll.kind = "schedule" + /\ LastTimeOk(st0, ll.time_ns) + /\ EnsureRateOk(stT, ll.rate_bps) + /\ EnsureWeightOk(st1, ll.class_id, ll.weight) + /\ Has(ll, "departure_time_ns") + /\ dep >= ll.time_ns + /\ ~pk0.present + /\ ApproxEq(ll.vtime_ns, st2.vtime_ns, 1) + /\ q0.present + /\ q0.class_id = ll.class_id + /\ q0.size_bytes = ll.size_bytes + /\ q0.finish_time_ns = ll.finish_time_ns + /\ minFinish = ll.finish_time_ns + /\ l' = l + 1 + /\ sched' = [sched EXCEPT ![sid] = st2] + /\ queue' = [queue EXCEPT ![key] = [q0 EXCEPT !.present = FALSE]] + /\ pending' = + [pending EXCEPT ![sid] = + [pk0 EXCEPT + !.present = TRUE, + !.key = key, + !.class_id = ll.class_id, + !.size_bytes = ll.size_bytes, + !.finish_time_ns = ll.finish_time_ns, + !.departure_time_ns = dep, + !.schedule_idx = l]] + +Depart == + /\ l \in 1..LenTrace + /\ LET ll == Trace[l] + sid == ll.scheduler_id + dep == ll.departure_time_ns + key == <> + st0 == sched[sid] + stT == UpdateLastTime(st0, ll.time_ns) + st1 == EnsureRateState(stT, ll.rate_bps) + st2 == EnsureWeightState(st1, ll.class_id, ll.weight) + pk0 == pending[sid] + wsum == st2.active_weight_sum + vNext == + IF wsum = 0 THEN + st2.vtime_ns + ELSE + st2.vtime_ns + RoundDiv(dep - st2.last_updated_ns, wsum) + count0 == st2.flow_counts[ll.class_id] + count1 == count0 - 1 + wsum1 == IF count1 = 0 THEN wsum - st2.weights[ll.class_id] ELSE wsum + vFinal == IF wsum1 = 0 THEN 0 ELSE vNext + ftFinal == + IF wsum1 = 0 THEN + [st2.finish_times EXCEPT ![ll.class_id] = 0] + ELSE + st2.finish_times + st3 == + [st2 EXCEPT + !.vtime_ns = vFinal, + !.last_updated_ns = dep, + !.active_weight_sum = wsum1, + !.flow_counts[ll.class_id] = count1, + !.finish_times = ftFinal] + IN + /\ ll.kind = "depart" + /\ LastTimeOk(st0, ll.time_ns) + /\ EnsureRateOk(stT, ll.rate_bps) + /\ EnsureWeightOk(st1, ll.class_id, ll.weight) + /\ Has(ll, "departure_time_ns") + /\ dep = ll.time_ns + /\ pk0.present + /\ pk0.key = key + /\ pk0.class_id = ll.class_id + /\ pk0.size_bytes = ll.size_bytes + /\ pk0.finish_time_ns = ll.finish_time_ns + /\ pk0.departure_time_ns = dep + /\ wsum > 0 + /\ count0 > 0 + /\ ApproxEq(ll.vtime_ns, vFinal, 1) + /\ l' = l + 1 + /\ sched' = [sched EXCEPT ![sid] = st3] + /\ queue' = queue + /\ pending' = [pending EXCEPT ![sid] = [pk0 EXCEPT !.present = FALSE]] + +Next == Enqueue \/ Schedule \/ Depart + +TraceSpec == Init /\ [][Next]_Vars + +ProgressOk == IF l <= LenTrace THEN ENABLED Next ELSE TRUE + +============================================================================= diff --git a/utils/bench_leanguard_vs_tlc.py b/utils/bench_leanguard_vs_tlc.py new file mode 100644 index 00000000..e447d1d0 --- /dev/null +++ b/utils/bench_leanguard_vs_tlc.py @@ -0,0 +1,344 @@ +#!/usr/bin/env python3 +import argparse +import json +import statistics +import subprocess +from dataclasses import dataclass +from datetime import datetime +from pathlib import Path +from typing import Any, Optional + +try: + import tomllib # py311+ +except ModuleNotFoundError: + import tomli as tomllib # py310 + + + +@dataclass(frozen=True) +class ProtocolSpec: + protocol: str + trace_csv: str + checker: str + tlc_module: str + + +PROTOCOLS: list[ProtocolSpec] = [ + ProtocolSpec( + protocol="aqm", trace_csv="aqm_events.csv", checker="aqm_check", tlc_module="AqmTrace.tla" + ), + ProtocolSpec( + protocol="pfc", trace_csv="pfc_events.csv", checker="pfc_check", tlc_module="PfcTrace.tla" + ), + ProtocolSpec( + protocol="dcqcn", + trace_csv="dcqcn_events.csv", + checker="dcqcn_check", + tlc_module="DcqcnTrace.tla", + ), + ProtocolSpec( + protocol="wfq", trace_csv="wfq_events.csv", checker="wfq_check", tlc_module="WfqTrace.tla" + ), + ProtocolSpec( + protocol="drr", trace_csv="drr_events.csv", checker="drr_check", tlc_module="DrrTrace.tla" + ), + ProtocolSpec( + protocol="cubic", + trace_csv="cubic_events.csv", + checker="cubic_check", + tlc_module="CubicTrace.tla", + ), +] + + +@dataclass(frozen=True) +class OneRun: + config: str + log_path: str + protocol: str + trace_csv: str + events: int + checker: str + checker_ms: int + tlc_module: str + tlc_cmd_ms: Optional[int] + tlc_total_ms: Optional[int] + tlc_status: Optional[str] + + +def parse_args() -> argparse.Namespace: + p = argparse.ArgumentParser( + description="Benchmark LeanGuard checkers vs TLC baseline across protocols." + ) + p.add_argument( + "--configs", + nargs="+", + default=[ + "configs/dcqcn_simple.toml", + "configs/dcqcn_multi.toml", + "configs/dcqcn_1s.toml", + "configs/dcqcn_2s.toml", + "configs/dcqcn_10s.toml", + "configs/pfc.toml", + "configs/wfq_simple.toml", + "configs/drr_simple.toml", + "configs/cubic_simple.toml", + ], + help="Config TOML paths to benchmark (requires logs already exist).", + ) + p.add_argument( + "--protocols", + nargs="+", + default=[p.protocol for p in PROTOCOLS], + choices=[p.protocol for p in PROTOCOLS], + help="Protocols to include in the benchmark.", + ) + p.add_argument("--reps", type=int, default=5, help="Repetitions per config.") + p.add_argument( + "--leanguard-run", + default="target/debug/leanguard-run", + help="Path to the leanguard-run binary.", + ) + p.add_argument( + "--checker-dir", + default="lean/.lake/build/bin", + help="Directory containing LeanGuard checker executables.", + ) + p.add_argument( + "--tlc-jar", + default="/tmp/leanguard_refs/tla2tools_v1.7.4.jar", + help="Path to tla2tools.jar for TLC.", + ) + p.add_argument( + "--out", + default="", + help="Output JSON path (default: logs/bench_leanguard_vs_tlc_.json).", + ) + return p.parse_args() + + +def mean(xs: list[float]) -> float: + return statistics.mean(xs) + + +def stdev(xs: list[float]) -> float: + return statistics.stdev(xs) if len(xs) >= 2 else 0.0 + + +def count_events(csv_path: Path) -> int: + # Events = lines - 1 header. + with csv_path.open("rb") as f: + lines = sum(1 for _ in f) + return max(0, lines - 1) + + +def run_one( + leanguard_run: Path, cfg_path: Path, checker_dir: Path, tlc_jar: Path +) -> dict[str, Any]: + cmd = [ + str(leanguard_run), + "--config", + str(cfg_path), + "--mode", + "check-only", + "--checker-dir", + str(checker_dir), + "--tlc-check", + "--tlc-jar", + str(tlc_jar), + ] + out = subprocess.check_output(cmd) + return json.loads(out) + + +def find_checker_runtime_ms(summary: dict[str, Any], checker: str) -> Optional[int]: + for r in summary.get("checker_results", []): + if r.get("checker") == checker: + rt = r.get("runtime_ms") + return int(rt) if rt is not None else None + return None + + +def find_tlc_result(summary: dict[str, Any], tlc_module: str) -> Optional[dict[str, Any]]: + tlc_results = summary.get("tlc_results") or [] + for r in tlc_results: + module_path = r.get("module", "") + if module_path.endswith("/" + tlc_module) or module_path.endswith("\\" + tlc_module) or ( + module_path.endswith(tlc_module) + ): + return r + return None + + +def main() -> None: + args = parse_args() + + leanguard_run = Path(args.leanguard_run) + checker_dir = Path(args.checker_dir) + tlc_jar = Path(args.tlc_jar) + + if not leanguard_run.is_file(): + raise SystemExit(f"Missing leanguard-run binary: {leanguard_run}") + if not checker_dir.is_dir(): + raise SystemExit(f"Missing checker dir: {checker_dir}") + if not tlc_jar.is_file(): + raise SystemExit(f"Missing TLC jar: {tlc_jar}") + + configs = [Path(c) for c in args.configs] + for c in configs: + if not c.is_file(): + raise SystemExit(f"Missing config: {c}") + + selected_protocols = set(args.protocols) + specs = [p for p in PROTOCOLS if p.protocol in selected_protocols] + + runs: list[OneRun] = [] + for cfg_path in configs: + cfg_data = tomllib.loads(cfg_path.read_text()) + log_path = Path(cfg_data.get("log_path", "")) + if not log_path.is_dir(): + raise SystemExit( + f"Missing log_path for {cfg_path}: {log_path}. " + "Run the simulation first to generate logs." + ) + + available_traces = {p.name for p in log_path.glob("*_events.csv") if p.is_file()} + + for _ in range(args.reps): + v = run_one(leanguard_run, cfg_path, checker_dir, tlc_jar) + + for spec in specs: + if spec.trace_csv not in available_traces: + continue + + trace_path = log_path / spec.trace_csv + if not trace_path.is_file(): + continue + event_count = count_events(trace_path) + if event_count <= 0: + continue + + rt = find_checker_runtime_ms(v, spec.checker) + if rt is None: + raise SystemExit( + f"Missing {spec.checker} runtime_ms in output for {cfg_path}" + ) + + tlc = find_tlc_result(v, spec.tlc_module) + if tlc is None: + raise SystemExit( + f"Missing TLC result for {spec.tlc_module} in output for {cfg_path}" + ) + + runs.append( + OneRun( + config=str(cfg_path), + log_path=str(log_path), + protocol=spec.protocol, + trace_csv=spec.trace_csv, + events=event_count, + checker=spec.checker, + checker_ms=int(rt), + tlc_module=spec.tlc_module, + tlc_cmd_ms=tlc.get("runtime_ms"), + tlc_total_ms=tlc.get("total_runtime_ms"), + tlc_status=tlc.get("status"), + ) + ) + + by_key: dict[tuple[str, str], list[OneRun]] = {} + for r in runs: + by_key.setdefault((r.protocol, r.config), []).append(r) + + timestamp = datetime.now().isoformat(timespec="seconds") + print(f"Benchmark timestamp: {timestamp}") + print(f"Repetitions per config: {args.reps}") + print() + + header = [ + "protocol", + "config", + "events", + "checker_ms_mean", + "checker_ms_stdev", + "tlc_total_ms_mean", + "tlc_total_ms_stdev", + "tlc_cmd_ms_mean", + "tlc_cmd_ms_stdev", + "tlc_total/lean_ratio_mean", + "tlc_statuses", + ] + print("\t".join(header)) + + summary: list[dict[str, Any]] = [] + for (protocol, cfg), rs in sorted(by_key.items()): + dc = [r.checker_ms for r in rs] + tlc_total = [r.tlc_total_ms for r in rs if r.tlc_total_ms is not None] + tlc_cmd = [r.tlc_cmd_ms for r in rs if r.tlc_cmd_ms is not None] + statuses = sorted({r.tlc_status for r in rs}) + + ratio = [t / d for (t, d) in zip(tlc_total, dc) if d] + + row = { + "protocol": protocol, + "config": cfg, + "trace_csv": rs[0].trace_csv, + "events": rs[0].events, + "checker": rs[0].checker, + "checker_ms_mean": mean(dc), + "checker_ms_stdev": stdev(dc), + "tlc_module": rs[0].tlc_module, + "tlc_total_ms_mean": mean(tlc_total) if tlc_total else None, + "tlc_total_ms_stdev": stdev(tlc_total) if tlc_total else None, + "tlc_cmd_ms_mean": mean(tlc_cmd) if tlc_cmd else None, + "tlc_cmd_ms_stdev": stdev(tlc_cmd) if tlc_cmd else None, + "tlc_total_over_lean_ratio_mean": mean(ratio) if ratio else None, + "tlc_statuses": statuses, + } + summary.append(row) + + print( + "\t".join( + [ + protocol, + cfg, + str(row["events"]), + f"{row['checker_ms_mean']:.1f}", + f"{row['checker_ms_stdev']:.1f}", + f"{row['tlc_total_ms_mean']:.1f}" if row["tlc_total_ms_mean"] else "n/a", + f"{row['tlc_total_ms_stdev']:.1f}" if row["tlc_total_ms_stdev"] else "n/a", + f"{row['tlc_cmd_ms_mean']:.1f}" if row["tlc_cmd_ms_mean"] else "n/a", + f"{row['tlc_cmd_ms_stdev']:.1f}" if row["tlc_cmd_ms_stdev"] else "n/a", + f"{row['tlc_total_over_lean_ratio_mean']:.1f}" + if row["tlc_total_over_lean_ratio_mean"] + else "n/a", + ",".join(str(s) for s in statuses), + ] + ) + ) + + out_path = Path(args.out) if args.out else None + if out_path is None: + Path("logs").mkdir(exist_ok=True) + out_path = Path("logs") / f"bench_leanguard_vs_tlc_{datetime.now().date().isoformat()}.json" + out_path.write_text( + json.dumps( + { + "timestamp": timestamp, + "reps": args.reps, + "protocols": sorted(selected_protocols), + "leanguard_run": str(leanguard_run), + "checker_dir": str(checker_dir), + "tlc_jar": str(tlc_jar), + "runs": [r.__dict__ for r in runs], + "summary": summary, + }, + indent=2, + ) + ) + print() + print(f"Wrote: {out_path}") + + +if __name__ == "__main__": + main() diff --git a/utils/ci_testgen_timings.py b/utils/ci_testgen_timings.py new file mode 100644 index 00000000..dd61172e --- /dev/null +++ b/utils/ci_testgen_timings.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +from __future__ import annotations + +import argparse +import csv +import json +import os +import shutil +import subprocess +import sys +import tempfile +import time +from dataclasses import dataclass +from datetime import datetime, timezone +from pathlib import Path + + +PROTOCOL_SEED_CONFIGS: dict[str, str] = { + "aqm": "configs/simple.toml", + "dcqcn": "configs/dcqcn_simple.toml", + "pfc": "configs/pfc.toml", + "wfq": "configs/wfq_simple.toml", + "drr": "configs/drr_simple.toml", + "cubic": "configs/cubic_simple.toml", +} + + +@dataclass(frozen=True) +class TimedRun: + seconds: float + stdout: str + + +def utc_now_iso() -> str: + return datetime.now(timezone.utc).replace(microsecond=0).isoformat() + + +def run_checked(argv: list[str], *, cwd: Path) -> TimedRun: + start = time.perf_counter() + completed = subprocess.run( + argv, + cwd=str(cwd), + check=False, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + text=True, + ) + elapsed = time.perf_counter() - start + if completed.returncode != 0: + tail = "\n".join(completed.stderr.splitlines()[-40:]) + raise RuntimeError( + f"Command failed ({completed.returncode}): {' '.join(argv)}\n" + f"--- stderr (tail) ---\n{tail}\n" + ) + return TimedRun(seconds=elapsed, stdout=completed.stdout) + + +def parse_json_stdout(stdout: str) -> dict: + try: + return json.loads(stdout) + except json.JSONDecodeError as e: + raise RuntimeError(f"Invalid JSON output: {e}\n--- stdout ---\n{stdout}\n") from e + + +def ensure_parent(path: Path) -> None: + path.parent.mkdir(parents=True, exist_ok=True) + + +def append_csv_row(path: Path, row: dict[str, object]) -> None: + ensure_parent(path) + write_header = not path.exists() + with path.open("a", newline="") as f: + writer = csv.DictWriter(f, fieldnames=list(row.keys())) + if write_header: + writer.writeheader() + writer.writerow(row) + + +def main(argv: list[str]) -> int: + p = argparse.ArgumentParser( + description="Run leanguard-testgen end-to-end for one protocol and emit a CSV timing row." + ) + p.add_argument( + "--protocol", + required=True, + choices=sorted(PROTOCOL_SEED_CONFIGS.keys()), + help="Target protocol to run.", + ) + p.add_argument( + "--budget", + type=int, + default=1, + help="Campaign budget (number of generated cases). Default: 1.", + ) + p.add_argument( + "--rng-seed", + type=int, + default=1, + help="RNG seed for campaign selection/mutation. Default: 1.", + ) + p.add_argument( + "--max-calibration-iters", + type=int, + default=0, + help="Max calibration iterations per case. Default: 0.", + ) + p.add_argument( + "--out", + type=Path, + required=True, + help="CSV output path (will be created/appended).", + ) + p.add_argument( + "--repo-root", + type=Path, + default=Path(__file__).resolve().parents[1], + help="Repo root (default: inferred from script location).", + ) + p.add_argument( + "--testgen-bin", + type=Path, + default=Path("target/release/leanguard-testgen"), + help="Path to leanguard-testgen binary (default: target/release/leanguard-testgen).", + ) + p.add_argument( + "--leanguard-run", + type=Path, + default=Path("target/release/leanguard-run"), + help="Path to leanguard-run binary (default: target/release/leanguard-run).", + ) + p.add_argument( + "--checker-dir", + type=Path, + default=Path("lean/.lake/build/bin"), + help="Path to LeanGuard checker binaries (default: lean/.lake/build/bin).", + ) + args = p.parse_args(argv) + + repo_root = args.repo_root.resolve() + testgen_bin = (repo_root / args.testgen_bin).resolve() + leanguard_run = (repo_root / args.leanguard_run).resolve() + checker_dir = (repo_root / args.checker_dir).resolve() + + seed_rel = PROTOCOL_SEED_CONFIGS[args.protocol] + seed_src = (repo_root / seed_rel).resolve() + if not seed_src.exists(): + raise RuntimeError(f"Seed config missing: {seed_src}") + + if not testgen_bin.exists(): + raise RuntimeError( + f"Missing {testgen_bin}. Build first, e.g.:\n" + f" cargo build --release --features lean,dcqcn,l2_pfc " + f"--bin leanguard-run --bin leanguard-testgen\n" + ) + if not leanguard_run.exists(): + raise RuntimeError(f"Missing {leanguard_run}. (Did you build --bin leanguard-run?)") + if not checker_dir.exists(): + raise RuntimeError( + f"Missing checker dir: {checker_dir}. Build Lean checkers first, e.g.:\n" + f" (cd lean && lake build)\n" + ) + + git_sha = os.environ.get("GITHUB_SHA") or os.environ.get("GIT_SHA") or "" + run_id = os.environ.get("GITHUB_RUN_ID") or "" + runner_os = os.environ.get("RUNNER_OS") or "" + lean_build_s = os.environ.get("CI_LEAN_BUILD_S") or "" + rust_build_s = os.environ.get("CI_RUST_BUILD_S") or "" + + with tempfile.TemporaryDirectory(prefix=f"testgen_ci_{args.protocol}_") as tmp: + tmp_path = Path(tmp) + corpus_root = tmp_path / "corpus" + seeds_src_dir = tmp_path / "seeds_src" + seeds_src_dir.mkdir(parents=True, exist_ok=True) + shutil.copy2(seed_src, seeds_src_dir / seed_src.name) + + common_prefix = [ + str(testgen_bin), + "--corpus-root", + str(corpus_root), + "--checker-dir", + str(checker_dir), + "--leanguard-run", + str(leanguard_run), + ] + + seed_index = run_checked(common_prefix + ["seed-index", str(seeds_src_dir)], cwd=repo_root) + _seed_index_json = parse_json_stdout(seed_index.stdout) + + campaign = run_checked( + common_prefix + + [ + "campaign", + "--protocol", + args.protocol, + "--budget", + str(args.budget), + "--rng-seed", + str(args.rng_seed), + "--max-calibration-iters", + str(args.max_calibration_iters), + ], + cwd=repo_root, + ) + campaign_json = parse_json_stdout(campaign.stdout) + + row: dict[str, object] = { + "timestamp_utc": utc_now_iso(), + "git_sha": git_sha, + "run_id": run_id, + "runner_os": runner_os, + "lean_build_s": lean_build_s, + "rust_build_s": rust_build_s, + "protocol": args.protocol, + "seed_config": seed_rel, + "budget": args.budget, + "rng_seed": args.rng_seed, + "max_calibration_iters": args.max_calibration_iters, + "seed_index_s": round(seed_index.seconds, 6), + "campaign_s": round(campaign.seconds, 6), + "total_s": round(seed_index.seconds + campaign.seconds, 6), + "attempted": campaign_json.get("attempted"), + "accepted": campaign_json.get("accepted"), + "rejected": campaign_json.get("rejected"), + "errors": campaign_json.get("errors"), + "dry_run": campaign_json.get("dry_run"), + } + append_csv_row(args.out, row) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv[1:])) diff --git a/utils/export_experiment_results.py b/utils/export_experiment_results.py new file mode 100644 index 00000000..dfea91fb --- /dev/null +++ b/utils/export_experiment_results.py @@ -0,0 +1,265 @@ +#!/usr/bin/env python3 +import argparse +import csv +import json +from dataclasses import dataclass +from pathlib import Path +from typing import Any + + +@dataclass(frozen=True) +class ExportPaths: + bench_json: Path + fault_json: Path + out_md: Path + out_bench_runs_csv: Path + out_bench_summary_csv: Path + out_fault_runs_csv: Path + + +def parse_args() -> argparse.Namespace: + p = argparse.ArgumentParser( + description="Export experiment artifacts (bench + fault-injection) to Markdown and CSV." + ) + p.add_argument( + "--bench-json", + default="", + help="Path to bench_leanguard_vs_tlc_*.json (default: pick latest under logs/).", + ) + p.add_argument( + "--fault-json", + default="", + help="Path to fault_injection_agreement_*.json (default: pick latest under logs/).", + ) + p.add_argument( + "--out-md", + default="ideas/results.md", + help="Markdown output path (default: ideas/results.md).", + ) + p.add_argument( + "--out-dir", + default="logs", + help="Directory for CSV exports (default: logs).", + ) + return p.parse_args() + + +def find_latest(glob_pattern: str) -> Path: + candidates = list(Path(".").glob(glob_pattern)) + candidates = [p for p in candidates if p.is_file()] + if not candidates: + raise SystemExit(f"No files match: {glob_pattern}") + candidates.sort(key=lambda p: p.stat().st_mtime, reverse=True) + return candidates[0] + + +def load_json(path: Path) -> dict[str, Any]: + try: + return json.loads(path.read_text()) + except Exception as e: + raise SystemExit(f"Failed to parse JSON {path}: {e}") from e + + +def fmt_mean_stdev(mean: float | None, stdev: float | None) -> str: + if mean is None: + return "" + if stdev is None: + return f"{mean:.1f}" + return f"{mean:.1f} ± {stdev:.1f}" + + +def write_csv(path: Path, rows: list[dict[str, Any]]) -> None: + path.parent.mkdir(parents=True, exist_ok=True) + if not rows: + path.write_text("") + return + fieldnames = list(rows[0].keys()) + with path.open("w", newline="") as f: + w = csv.DictWriter(f, fieldnames=fieldnames) + w.writeheader() + for r in rows: + w.writerow(r) + + +def export_bench(bench: dict[str, Any], out_dir: Path) -> tuple[Path, Path]: + runs = bench.get("runs") or [] + summary = bench.get("summary") or [] + + date = str(bench.get("timestamp", "")).split("T")[0] or "unknown_date" + runs_csv = out_dir / f"bench_leanguard_vs_tlc_{date}_runs.csv" + summary_csv = out_dir / f"bench_leanguard_vs_tlc_{date}_summary.csv" + + runs_out: list[dict[str, Any]] = [] + for r in runs: + runs_out.append(dict(r)) + + summary_out: list[dict[str, Any]] = [] + for r in summary: + row = dict(r) + statuses = row.get("tlc_statuses") + if isinstance(statuses, list): + row["tlc_statuses"] = ",".join(str(s) for s in statuses) + summary_out.append(row) + + write_csv(runs_csv, runs_out) + write_csv(summary_csv, summary_out) + return runs_csv, summary_csv + + +def export_fault(fault: dict[str, Any], out_dir: Path) -> Path: + runs = fault.get("runs") or [] + date = str(fault.get("timestamp", "")).split("T")[0] or "unknown_date" + runs_csv = out_dir / f"fault_injection_agreement_{date}.csv" + + flat_runs: list[dict[str, Any]] = [] + for r in runs: + row = dict(r) + lean_failure = row.pop("lean_failure", None) or {} + if isinstance(lean_failure, dict): + row["lean_failure_line"] = lean_failure.get("csv_line") + row["lean_failure_time_ns"] = lean_failure.get("time_ns") + row["lean_failure_event_id"] = lean_failure.get("event_id") + row["lean_failure_kind"] = lean_failure.get("kind") + else: + row["lean_failure_line"] = None + row["lean_failure_time_ns"] = None + row["lean_failure_event_id"] = None + row["lean_failure_kind"] = None + flat_runs.append(row) + + write_csv(runs_csv, flat_runs) + return runs_csv + + +def md_escape(s: str) -> str: + return s.replace("|", "\\|") + + +def render_markdown(bench: dict[str, Any], fault: dict[str, Any], paths: ExportPaths) -> str: + bench_rows = list(bench.get("summary") or []) + fault_rows = list(fault.get("runs") or []) + + bench_ts = str(bench.get("timestamp", "")) + fault_ts = str(fault.get("timestamp", "")) + + lines: list[str] = [] + lines.append("# Experiment results\n") + + lines.append("## Benchmarks (LeanGuard vs TLC)\n") + lines.append(f"- Timestamp: `{bench_ts}`") + lines.append(f"- Raw data: `{paths.bench_json}`") + lines.append(f"- CSV (runs): `{paths.out_bench_runs_csv}`") + lines.append(f"- CSV (summary): `{paths.out_bench_summary_csv}`\n") + + lines.append( + "| Protocol | Config | Events | checker_ms | tlc_total_ms | tlc_cmd_ms | tlc_total/checker | TLC statuses |" + ) + lines.append("|---|---|---:|---:|---:|---:|---:|---|") + for r in bench_rows: + lines.append( + "| " + + " | ".join( + [ + md_escape(str(r.get("protocol", ""))), + md_escape(str(r.get("config", ""))), + str(r.get("events", "")), + fmt_mean_stdev( + r.get("checker_ms_mean"), r.get("checker_ms_stdev") + ), + fmt_mean_stdev( + r.get("tlc_total_ms_mean"), r.get("tlc_total_ms_stdev") + ), + fmt_mean_stdev(r.get("tlc_cmd_ms_mean"), r.get("tlc_cmd_ms_stdev")), + f"{(r.get('tlc_total_over_lean_ratio_mean') or 0):.1f}", + md_escape(",".join(r.get("tlc_statuses") or [])), + ] + ) + + " |" + ) + + lines.append("\n## Fault-injection agreement (LeanGuard vs TLC)\n") + lines.append(f"- Timestamp: `{fault_ts}`") + lines.append(f"- Raw data: `{paths.fault_json}`") + lines.append(f"- CSV: `{paths.out_fault_runs_csv}`\n") + + lines.append("| Protocol | Case | Lean | TLC | Lean first failure | TLC first failure |") + lines.append("|---|---|---|---|---|---|") + for r in fault_rows: + lean_failure = r.get("lean_failure") or {} + lean_key = "" + if lean_failure: + t = lean_failure.get("time_ns") + e = lean_failure.get("event_id") + k = lean_failure.get("kind") + lean_key = f"line {lean_failure.get('csv_line')} ({t},{e},{k})" + + tlc_key = "" + if r.get("tlc_failure_time_ns") is not None or r.get("tlc_failure_event_id") is not None: + tlc_key = ( + f"idx {r.get('tlc_failure_index')} " + f"({r.get('tlc_failure_time_ns')},{r.get('tlc_failure_event_id')},{r.get('tlc_failure_kind')})" + ) + + lines.append( + "| " + + " | ".join( + [ + md_escape(str(r.get("protocol", ""))), + md_escape(str(r.get("case", ""))), + md_escape(str(r.get("lean_status", ""))), + md_escape(str(r.get("tlc_status", ""))), + md_escape(lean_key), + md_escape(tlc_key), + ] + ) + + " |" + ) + + lines.append( + "\n## Notes / caveats\n\n" + "- The TLC baseline for `CubicTrace.tla` is validated against `configs/cubic_simple.toml`.\n" + "- `configs/benchmarks/leanguard/tcp_cubic_micro.toml` currently produces a TLC **reject** for `CubicTrace.tla` (the fixed-point approximation drifts on longer traces), so it should not be used as an “accept” benchmark without adjusting either the config or the spec.\n" + ) + + return "\n".join(lines).rstrip() + "\n" + + +def resolve_paths(args: argparse.Namespace) -> ExportPaths: + bench_json = Path(args.bench_json) if args.bench_json else find_latest("logs/bench_leanguard_vs_tlc_*.json") + fault_json = Path(args.fault_json) if args.fault_json else find_latest("logs/fault_injection_agreement_*.json") + + bench = load_json(bench_json) + fault = load_json(fault_json) + out_dir = Path(args.out_dir) + + runs_csv, summary_csv = export_bench(bench, out_dir) + fault_csv = export_fault(fault, out_dir) + + return ExportPaths( + bench_json=bench_json, + fault_json=fault_json, + out_md=Path(args.out_md), + out_bench_runs_csv=runs_csv, + out_bench_summary_csv=summary_csv, + out_fault_runs_csv=fault_csv, + ) + + +def main() -> None: + args = parse_args() + paths = resolve_paths(args) + + bench = load_json(paths.bench_json) + fault = load_json(paths.fault_json) + + md = render_markdown(bench, fault, paths) + paths.out_md.parent.mkdir(parents=True, exist_ok=True) + paths.out_md.write_text(md) + print(f"Wrote: {paths.out_md}") + print(f"Wrote: {paths.out_bench_runs_csv}") + print(f"Wrote: {paths.out_bench_summary_csv}") + print(f"Wrote: {paths.out_fault_runs_csv}") + + +if __name__ == "__main__": + main() diff --git a/utils/fault_injection_agreement.py b/utils/fault_injection_agreement.py new file mode 100644 index 00000000..fb699d2f --- /dev/null +++ b/utils/fault_injection_agreement.py @@ -0,0 +1,484 @@ +#!/usr/bin/env python3 +import argparse +import json +import re +import subprocess +import tempfile +from dataclasses import dataclass +from datetime import datetime +from pathlib import Path +from typing import Any, Optional + + +@dataclass(frozen=True) +class ProtocolSpec: + protocol: str + trace_csv: str + checker: str + tlc_module: str + + +PROTOCOLS: list[ProtocolSpec] = [ + ProtocolSpec( + protocol="aqm", trace_csv="aqm_events.csv", checker="aqm_check", tlc_module="AqmTrace.tla" + ), + ProtocolSpec( + protocol="pfc", trace_csv="pfc_events.csv", checker="pfc_check", tlc_module="PfcTrace.tla" + ), + ProtocolSpec( + protocol="dcqcn", + trace_csv="dcqcn_events.csv", + checker="dcqcn_check", + tlc_module="DcqcnTrace.tla", + ), + ProtocolSpec( + protocol="wfq", trace_csv="wfq_events.csv", checker="wfq_check", tlc_module="WfqTrace.tla" + ), + ProtocolSpec( + protocol="drr", trace_csv="drr_events.csv", checker="drr_check", tlc_module="DrrTrace.tla" + ), + ProtocolSpec( + protocol="cubic", + trace_csv="cubic_events.csv", + checker="cubic_check", + tlc_module="CubicTrace.tla", + ), +] + + +@dataclass(frozen=True) +class FailureInfo: + csv_line: int + time_ns: Optional[int] + event_id: Optional[int] + kind: Optional[str] + + +@dataclass(frozen=True) +class OneCase: + protocol: str + case: str + base_trace: str + mutated_trace: str + lean_status: str + lean_runtime_ms: Optional[int] + lean_peak_rss_kb: Optional[int] + lean_failure: Optional[FailureInfo] + tlc_status: str + tlc_cmd_runtime_ms: Optional[int] + tlc_total_runtime_ms: Optional[int] + tlc_peak_rss_kb: Optional[int] + tlc_failure_index: Optional[int] + tlc_failure_time_ns: Optional[int] + tlc_failure_event_id: Optional[int] + tlc_failure_kind: Optional[str] + + +def parse_args() -> argparse.Namespace: + p = argparse.ArgumentParser( + description="Run fault-injection agreement checks between LeanGuard and the TLC baseline." + ) + p.add_argument( + "--logs-root", + default="logs", + help="Root directory to search for existing *_events.csv traces.", + ) + p.add_argument( + "--protocols", + nargs="+", + default=[p.protocol for p in PROTOCOLS], + choices=[p.protocol for p in PROTOCOLS], + help="Protocols to include in the suite.", + ) + p.add_argument( + "--leanguard-run", + default="target/debug/leanguard-run", + help="Path to the leanguard-run binary.", + ) + p.add_argument( + "--checker-dir", + default="lean/.lake/build/bin", + help="Directory containing LeanGuard checker executables.", + ) + p.add_argument( + "--tlc-jar", + default="/tmp/leanguard_refs/tla2tools_v1.7.4.jar", + help="Path to tla2tools.jar for TLC.", + ) + p.add_argument( + "--measure-rss", + action="store_true", + help="Ask leanguard-run to sample peak RSS (adds overhead).", + ) + p.add_argument( + "--out", + default="", + help="Output JSON path (default: logs/fault_injection_agreement_.json).", + ) + return p.parse_args() + + +def count_lines(path: Path) -> int: + with path.open("rb") as f: + return sum(1 for _ in f) + + +def find_smallest_trace(logs_root: Path, trace_csv: str) -> Path: + candidates: list[tuple[int, Path]] = [] + for p in logs_root.glob(f"*/{trace_csv}"): + if not p.is_file(): + continue + lines = count_lines(p) + if lines <= 1: + continue + candidates.append((lines, p)) + if not candidates: + raise SystemExit(f"No usable trace found under {logs_root}: {trace_csv}") + candidates.sort(key=lambda t: t[0]) + return candidates[0][1] + + +def load_csv_lines(path: Path) -> list[str]: + lines = path.read_text().splitlines() + if not lines: + raise ValueError(f"empty CSV: {path}") + return lines + + +def parse_header_indices(header: str) -> dict[str, int]: + cols = header.split(",") + return {c: i for (i, c) in enumerate(cols)} + + +def get_field(lines: list[str], idx: dict[str, int], csv_line: int, col: str) -> str: + row = lines[csv_line - 1].split(",") + return row[idx[col]] + + +def set_field(lines: list[str], idx: dict[str, int], csv_line: int, col: str, value: str) -> None: + parts = lines[csv_line - 1].split(",") + parts[idx[col]] = value + lines[csv_line - 1] = ",".join(parts) + + +def find_first_data_line_with_kind(lines: list[str], idx: dict[str, int], kind: str) -> int: + if "kind" not in idx: + raise ValueError("CSV has no 'kind' column") + for csv_line in range(2, len(lines) + 1): + parts = lines[csv_line - 1].split(",") + if parts[idx["kind"]] == kind: + return csv_line + raise ValueError(f"no row with kind={kind}") + + +def parse_lean_first_failure(stderr: str) -> Optional[int]: + # Typical: "REJECT: line 12: ..." + m = re.search(r"REJECT:\s*line\s+(\d+)\s*:", stderr) + if m: + return int(m.group(1)) + + # Parse failures can also be "line 12: ..." without the REJECT prefix (older tooling). + m = re.search(r"\bline\s+(\d+)\s*:", stderr) + if m: + return int(m.group(1)) + + return None + + +def failure_info_from_csv(path: Path, csv_line: int) -> FailureInfo: + lines = load_csv_lines(path) + idx = parse_header_indices(lines[0]) + + def as_int(col: str) -> Optional[int]: + if col not in idx: + return None + raw = get_field(lines, idx, csv_line, col).strip() + return int(raw) if raw else None + + def as_str(col: str) -> Optional[str]: + if col not in idx: + return None + raw = get_field(lines, idx, csv_line, col).strip() + return raw if raw else None + + return FailureInfo( + csv_line=csv_line, + time_ns=as_int("time_ns"), + event_id=as_int("event_id"), + kind=as_str("kind"), + ) + + +def run_leanguard_run( + leanguard_run: Path, + config_path: Path, + checker_dir: Path, + tlc_jar: Path, + measure_rss: bool, +) -> dict[str, Any]: + cmd = [ + str(leanguard_run), + "--config", + str(config_path), + "--mode", + "check-only", + "--checker-dir", + str(checker_dir), + "--tlc-check", + "--tlc-jar", + str(tlc_jar), + ] + if measure_rss: + cmd.append("--measure-rss") + proc = subprocess.run(cmd, stdout=subprocess.PIPE, check=False) + if not proc.stdout: + raise SystemExit(f"leanguard-run produced no stdout (exit={proc.returncode}): {cmd}") + return json.loads(proc.stdout) + + +def find_checker(summary: dict[str, Any], checker: str) -> Optional[dict[str, Any]]: + for r in summary.get("checker_results", []): + if r.get("checker") == checker: + return r + return None + + +def find_tlc(summary: dict[str, Any], tlc_module: str) -> Optional[dict[str, Any]]: + for r in summary.get("tlc_results", []) or []: + module = r.get("module", "") + if module.endswith("/" + tlc_module) or module.endswith("\\" + tlc_module) or module.endswith( + tlc_module + ): + return r + return None + + +def mutate_case(protocol: str, base: Path, out: Path, case: str) -> None: + lines = load_csv_lines(base) + idx = parse_header_indices(lines[0]) + + if case == "accept_smoke": + out.write_text("\n".join(lines) + "\n") + return + + if protocol == "dcqcn" and case == "alpha_mismatch_first_row": + # `TraceData.tla` rescales ppb → permille (divide by 1_000_000) and the TLC spec + # uses a ±1 tolerance in the rescaled units. Change by 2e6 so TLC must reject too. + set_field(lines, idx, 2, "alpha_ppb", "2000000") + elif protocol == "dcqcn" and case == "cnp_size_mismatch": + line = find_first_data_line_with_kind(lines, idx, "cnp_sent") + set_field(lines, idx, line, "cnp_size_b", "65") + elif protocol == "aqm" and case == "invalid_ecn_mark": + set_field(lines, idx, 2, "ecn_before", "not_ect") + set_field(lines, idx, 2, "ecn_after", "ce") + elif protocol == "pfc" and case == "pfc_recv_sender_mismatch": + line = find_first_data_line_with_kind(lines, idx, "pfc_recv") + cur = get_field(lines, idx, line, "sender_id").strip() + set_field(lines, idx, line, "sender_id", str(int(cur) + 1 if cur else 1)) + elif protocol == "wfq" and case == "finish_time_mismatch": + line = find_first_data_line_with_kind(lines, idx, "schedule") + cur = get_field(lines, idx, line, "finish_time_ns").strip() + # `TraceData.tla` rescales ns → µs (rounded). A +1ns change can vanish after rescaling + # and WFQ uses a ±1µs tolerance, so perturb by 5µs to force a TLC reject. + set_field(lines, idx, line, "finish_time_ns", str(int(cur) + 5000 if cur else 5000)) + elif protocol == "drr" and case == "deficit_mismatch": + line = find_first_data_line_with_kind(lines, idx, "schedule") + cur = get_field(lines, idx, line, "deficit_bytes").strip() + set_field(lines, idx, line, "deficit_bytes", str(int(cur) + 1 if cur else 1)) + elif protocol == "cubic" and case == "cwnd_mismatch": + set_field(lines, idx, 2, "cwnd_bytes", "999999") + else: + raise ValueError(f"unknown mutation: {protocol}:{case}") + + out.write_text("\n".join(lines) + "\n") + + +def cases_for_protocol(protocol: str) -> list[str]: + if protocol == "dcqcn": + return ["accept_smoke", "alpha_mismatch_first_row", "cnp_size_mismatch"] + if protocol == "aqm": + return ["accept_smoke", "invalid_ecn_mark"] + if protocol == "pfc": + return ["accept_smoke", "pfc_recv_sender_mismatch"] + if protocol == "wfq": + return ["accept_smoke", "finish_time_mismatch"] + if protocol == "drr": + return ["accept_smoke", "deficit_mismatch"] + if protocol == "cubic": + return ["accept_smoke", "cwnd_mismatch"] + raise ValueError(f"unknown protocol: {protocol}") + + +def main() -> None: + args = parse_args() + + leanguard_run = Path(args.leanguard_run) + checker_dir = Path(args.checker_dir) + tlc_jar = Path(args.tlc_jar) + logs_root = Path(args.logs_root) + + if not leanguard_run.is_file(): + raise SystemExit(f"Missing leanguard-run binary: {leanguard_run}") + if not checker_dir.is_dir(): + raise SystemExit(f"Missing checker dir: {checker_dir}") + if not tlc_jar.is_file(): + raise SystemExit(f"Missing TLC jar: {tlc_jar}") + if not logs_root.is_dir(): + raise SystemExit(f"Missing logs root: {logs_root}") + + selected_protocols = set(args.protocols) + specs = [p for p in PROTOCOLS if p.protocol in selected_protocols] + + timestamp = datetime.now().isoformat(timespec="seconds") + runs: list[OneCase] = [] + + for spec in specs: + base = find_smallest_trace(logs_root, spec.trace_csv) + for case in cases_for_protocol(spec.protocol): + with tempfile.TemporaryDirectory(prefix=f"fault_{spec.protocol}_") as tmp: + tmp_path = Path(tmp) + log_path = tmp_path / "logs" + log_path.mkdir(parents=True, exist_ok=True) + + mutated = log_path / spec.trace_csv + mutate_case(spec.protocol, base, mutated, case) + + # traces.json drives checker/spec selection. + (log_path / "traces.json").write_text( + json.dumps({"version": 1, "traces": [spec.trace_csv]}) + ) + config_path = tmp_path / "case.toml" + config_path.write_text( + f'log_path = "{log_path.as_posix()}"\nthreading = "single"\n' + ) + + summary = run_leanguard_run( + leanguard_run, config_path, checker_dir, tlc_jar, args.measure_rss + ) + + checker = find_checker(summary, spec.checker) + if checker is None: + raise SystemExit(f"Missing checker result: {spec.checker} ({spec.protocol})") + + tlc = find_tlc(summary, spec.tlc_module) + if tlc is None: + raise SystemExit(f"Missing TLC result: {spec.tlc_module} ({spec.protocol})") + + lean_status = str(checker.get("status")) + lean_rt = checker.get("runtime_ms") + lean_rss = checker.get("peak_rss_kb") + lean_failure: Optional[FailureInfo] = None + if lean_status == "reject": + csv_line = parse_lean_first_failure(str(checker.get("stderr", ""))) + if csv_line is not None: + lean_failure = failure_info_from_csv(mutated, csv_line) + + tlc_status = str(tlc.get("status")) + tlc_cmd_rt = tlc.get("runtime_ms") + tlc_total_rt = tlc.get("total_runtime_ms") + tlc_rss = tlc.get("peak_rss_kb") + tlc_failure = tlc.get("first_failure") or {} + + runs.append( + OneCase( + protocol=spec.protocol, + case=case, + base_trace=str(base), + mutated_trace=str(mutated), + lean_status=lean_status, + lean_runtime_ms=int(lean_rt) if lean_rt is not None else None, + lean_peak_rss_kb=int(lean_rss) if lean_rss is not None else None, + lean_failure=lean_failure, + tlc_status=tlc_status, + tlc_cmd_runtime_ms=int(tlc_cmd_rt) if tlc_cmd_rt is not None else None, + tlc_total_runtime_ms=int(tlc_total_rt) if tlc_total_rt is not None else None, + tlc_peak_rss_kb=int(tlc_rss) if tlc_rss is not None else None, + tlc_failure_index=( + int(tlc_failure.get("index")) + if tlc_failure.get("index") is not None + else None + ), + tlc_failure_time_ns=( + int(tlc_failure.get("time_ns")) + if tlc_failure.get("time_ns") is not None + else None + ), + tlc_failure_event_id=( + int(tlc_failure.get("event_id")) + if tlc_failure.get("event_id") is not None + else None + ), + tlc_failure_kind=( + str(tlc_failure.get("kind")) + if tlc_failure.get("kind") is not None + else None + ), + ) + ) + + out_path = Path(args.out) if args.out else None + if out_path is None: + Path("logs").mkdir(exist_ok=True) + out_path = Path("logs") / f"fault_injection_agreement_{datetime.now().date().isoformat()}.json" + + out = { + "timestamp": timestamp, + "protocols": [s.protocol for s in specs], + "leanguard_run": str(leanguard_run), + "checker_dir": str(checker_dir), + "tlc_jar": str(tlc_jar), + "measure_rss": bool(args.measure_rss), + "runs": [ + { + **r.__dict__, + "lean_failure": r.lean_failure.__dict__ if r.lean_failure is not None else None, + } + for r in runs + ], + } + out_path.write_text(json.dumps(out, indent=2)) + + # Print a small summary table. + print(f"Timestamp: {timestamp}") + print(f"Wrote: {out_path}") + print() + print( + "\t".join( + [ + "protocol", + "case", + "lean", + "tlc", + "lean_line", + "lean_key", + "tlc_key", + ] + ) + ) + for r in runs: + lean_line = str(r.lean_failure.csv_line) if r.lean_failure else "" + lean_key = ( + f"{r.lean_failure.time_ns},{r.lean_failure.event_id}" if r.lean_failure else "" + ) + tlc_key = ( + f"{r.tlc_failure_time_ns},{r.tlc_failure_event_id}" + if r.tlc_failure_time_ns is not None and r.tlc_failure_event_id is not None + else "" + ) + print( + "\t".join( + [ + r.protocol, + r.case, + r.lean_status, + r.tlc_status, + lean_line, + lean_key, + tlc_key, + ] + ) + ) + + +if __name__ == "__main__": + main()