Added a TLA+/TLC trace-validation baseline with trace export, runner integration, and experiment tooling.

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

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 }

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

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 }

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"

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 }

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 }

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