Prove the Raft demo's safety claims under seeded chaos

.github/workflows/campaign.yml

@@ -1,10 +1,12 @@
 name: Nightly campaign
 
-# A small standing seed sweep of the jobqueue demo, so the campaign numbers
-# published in benchmarks/README.md keep being re-earned after every change
-# rather than dating from one good afternoon. Deliberately modest: a few
-# thousand seeds fits the runner's two cores in minutes, and the 100k-seed
-# sweeps stay a local, documented exercise.
+# A small standing seed sweep of both demos, so the campaign numbers published
+# in benchmarks/README.md and examples/raft/README.md keep being re-earned
+# after every change rather than dating from one good afternoon. Deliberately
+# modest: a few thousand seeds of each fit the runner's two cores in minutes,
+# and the sweeps at full scale stay a local, documented exercise. The raft
+# figure is well above the 300 seeds per-PR CI already runs on every matrix
+# leg, so the nightly is actually buying new coverage.
 
 on:
   schedule:
@@ -14,7 +16,7 @@ on:
 jobs:
   campaign:
     runs-on: ubuntu-latest
-    timeout-minutes: 30
+    timeout-minutes: 45
     steps:
       - uses: actions/checkout@v7
       - uses: astral-sh/setup-uv@v8.3.2
@@ -24,3 +26,4 @@ jobs:
       - run: uv run python benchmarks/campaign.py green --seeds 2000 --jobs 2 --checkpoint campaign-nightly.json
       - run: uv run python benchmarks/campaign.py ablations --seeds 500 --jobs 2 --checkpoint campaign-nightly-ablations.json
       - run: uv run python benchmarks/campaign.py stability --checkpoint campaign-nightly-ablations.json --sample 6 --reruns 20
+      - run: uv run pytest examples/raft/tests/test_chaos_campaign.py -q -m slow --simloop-seeds=5000 --simloop-jobs=2

CHANGELOG.md

@@ -2,6 +2,12 @@
 
 ## 0.2.0 (unreleased)
 
+- A second flagship demo: `examples/raft/` is a teaching-sized Raft (leader
+  election + log replication, plain asyncio on streams) tested only under
+  simulation — four safety invariants checked over 50,000 chaos seeds, five
+  safeguard ablations each caught and replayed from a seed, and failing
+  schedules minimized toward FIFO — down to a single interesting step in the
+  sharpest case.
 - Campaign evidence at scale, regenerable via `benchmarks/campaign.py`:
   100,000 seeds of jobqueue chaos green in six minutes on a laptop, every
   ablation caught with its failure density recorded, and 20 sampled failing

README.md

@@ -178,7 +178,7 @@ net.crash("node2")                              # no reset, just silence
   stdlib outside one, so code under test can use entropy and clocks
   without breaking replay.
 
-## Proving it: the jobqueue demo
+## Proving it: the demos
 
 `examples/jobqueue/` is a complete distributed system — an exactly-once
 job scheduler (leases, fencing tokens, idempotency keys, backoff, and
@@ -188,6 +188,17 @@ poison jobs, and shows that removing any load-bearing safeguard produces
 a violation the explorer finds and replays from a seed. The bug table
 lives in [examples/jobqueue/README.md](https://github.com/dhruvl/simloop/blob/main/examples/jobqueue/README.md).
 
+`examples/raft/` is the second proof: a teaching-sized Raft — leader
+election and log replication in plain asyncio on streams — swept under
+50,000 seeds of partitions, crashed-and-restarted processes, and message
+loss. Four safety invariants hold on every seed; remove any safeguard
+(the vote ledger, the log-freshness check, the commit gate,
+persistence-before-reply, stale-term rejection) and the explorer finds a
+seed-replayable violation, then minimizes the failing schedule to the
+steps that had to go a particular way — one step out of 3,514 recorded, in
+the sharpest case. The table lives in
+[examples/raft/README.md](https://github.com/dhruvl/simloop/blob/main/examples/raft/README.md).
+
 ## Performance
 
 Simulation is cheap: SimLoop schedules a task step in ~4.4 µs (trace

examples/raft/README.md

@@ -0,0 +1,154 @@
+# raft — leader election and log replication, proven by simloop
+
+A teaching-sized Raft: about 500 lines of plain asyncio (stdlib only, no
+simloop imports) covering leader election, log replication, persistence
+across process restarts, and an applied state machine. Its test suite runs
+entirely under [simloop](../../README.md) — seeded scheduling, virtual time,
+simulated partitions, process restarts, message loss and duplication — and
+every failure it can produce replays exactly from a seed.
+
+**A demo, not a library.** No log compaction and no snapshots, no membership
+changes, no client sessions. Submission is at-least-once and says so: a
+command a leader accepts before being deposed can be resubmitted and commit
+twice, under two indices, and the safety claims below deliberately do not
+mind. Storage is an in-memory stand-in that survives a process restart within
+a run, the way a disk survives a reboot.
+
+## The claim, stated honestly
+
+The paper's four safety properties hold under every schedule the explorer
+reaches. Liveness is not claimed: a partitioned minority makes no progress,
+and the suite waits in virtual time rather than asserting a wall-clock bound.
+
+Each rule that carries the safety argument sits behind its own flag in
+`Safeguards`, so the tests can switch exactly one off and watch the explorer
+find the schedule it lets through: stale-term rejection, one vote per term
+(§5.2), the log-freshness check on votes (§5.4.1), persistence before reply,
+the own-term commit gate (§5.4.2), and the per-term no-op that lets a quiet
+term commit (§8).
+
+Time is the only failure detector. Under simloop a partition stalls silently
+and a restarted process sends no reset, so a peer learns of trouble the way it
+would in production: from a request that never comes back.
+
+## Invariants
+
+Checked after every simulated run (`tests/checks.py`) against an ordered
+record of what the nodes observably did — `("leader", name, term, log)` at
+each election, `("apply", name, index, term, command, node_term)` at each
+state-machine apply — plus the logs the run ends with. The applier's own
+term rides along because leader completeness needs the term an entry was
+committed under, and the first apply of an index always happens on the
+leader that committed it:
+
+1. **election safety** — at most one leader per term
+2. **log matching** — if two logs hold the same term at an index, they hold
+   the same prefix before it
+3. **leader completeness** — an entry committed under a term-T leader is in
+   the log of every leader of a term above T
+4. **state-machine safety** — no index is ever applied as two different
+   entries
+
+## The numbers
+
+- Scenario suite: 11 seeded scenarios (elections, replication, RPC framing)
+  × 10 seeds each, alongside unit tests for the log, vote and persistence
+  rules — 63 fast tests plus the slow proofs, green.
+- Campaign: **50,000 seeds** of five-node chaos — three randomized partition
+  windows per seed, a process restart after about half of them, 2% message
+  drop and 2% duplication throughout, with a client proposing — invariants
+  held on every seed. 917.29s (15m17s) with `--simloop-jobs=8` on an M4
+  MacBook Air, about 54 seeds a second. The same scenario runs 300 seeds
+  sequentially in 27.97s and 2,000 seeds in 36.34s at `--simloop-jobs=8`.
+- Replay stability: a one-off local measurement re-explored each ablation's
+  found-at seed 100 times on a fresh loop — 5 seeds × 100 replays, one trace
+  hash apiece, byte-identical throughout. The standing check is
+  `test_a_found_seed_replays_byte_identically` (slow-marked, so it rides the
+  nightly): it locates a failing seed and holds its trace hash across eight
+  fresh replays.
+- Ablations: remove any load-bearing safeguard and the explorer finds a
+  violating schedule within a few seeds.
+
+| # | Safeguard removed | Invariant violated | Found at seed | Seeds searched | Reproduce |
+|---|---|---|---|---|---|
+| 1 | Vote ledger off (`one_vote_per_term=False`) | election-safety | 2 | 3 | `uv run pytest examples/raft/tests/test_ablations.py::test_double_voting_elects_two_leaders_in_one_term` |
+| 2 | Log-freshness check off (`check_log_up_to_date=False`) | leader-completeness | 0 | 1 | `... ::test_unchecked_logs_let_a_stale_follower_lead` |
+| 3 | Persistence before reply off (`persist_before_reply=False`) | leader-completeness | 4 | 5 | `... ::test_skipped_persistence_forgets_committed_entries` |
+| 4 | Stale-term rejection off (`reject_stale_term=False`) | state-machine-safety | 0 | 1 | `... ::test_accepting_stale_terms_rewrites_history` |
+| 5 | Commit gate off (`commit_own_term_only=False`, no-op off both sides) | state-machine-safety | 3 | 4 | `... ::test_committing_old_terms_by_count_loses_writes` |
+
+Rows 1–4 searched a budget of 300 seeds, row 5 a budget of 500. All five are
+labeled ablations — detection demonstrations, not bugs that were ever
+shipped.
+
+"Invariant violated" records what the found seed actually produced, not the
+only thing that ablation can produce. Three of the five tests deliberately
+accept any genuine violation class: a node that answers superseded terms, for
+instance, takes both stale appends and stale vote grants, so naming one of the
+four claims would say less than letting the checker report which one broke
+first.
+
+Two safeguards are also shown to be load-bearing *on their own*, which is the
+other half of the argument: with the commit gate the only thing standing (the
+per-term no-op switched off on both sides), the paper's Figure 8 runs clean
+across 150 seeds; with the vote ledger the only thing standing, the
+double-election scenario runs clean across 150 seeds. Both proofs are marked
+`slow`.
+
+### Found during development
+
+The replay-stability check above is what caught the last bug. `RaftNode.run`
+tracked its in-flight connection handlers in a `set` and cancelled them in
+iteration order when the incarnation died — but a set of tasks iterates by
+`id()`, which moves between runs, so two handlers could swap places. Seed 4
+of the persistence ablation produced two distinct trace hashes across 100
+re-runs: the same violation every time, reached by two different routes.
+An insertion-ordered dict fixed it. Nothing about the simulation was wrong:
+the demo was letting `id()` order decide something the schedule could see,
+which is exactly what the third rule in
+[docs/design.md](../../docs/design.md) tells the loop's own structures never
+to do. The found-at seeds in the table are unchanged either side of the fix.
+
+## What a failure looks like
+
+Each ablation test asserts that the explorer catches its ablation, so the
+tests themselves pass; the report is what the explorer hands back on the way.
+It names the invariant, the seed, and the trace around the failure. Run the
+same scenario through `explore(scenario, range(300), shrink=True)` and it
+also walks the recorded schedule back toward plain FIFO order, keeping only
+the decisions that have to go a particular way for the failure to reproduce.
+Stale-term rejection off, seed 0:
+
+    schedule shrink (experimental): 3,514 steps recorded, 57 runs to minimize
+    minimized: FIFO except step 1
+      step 1  TaskStepMethWrapper
+
+3,514 recorded scheduling steps; exactly one of them had to go a specific
+way. `FIFO throughout` is an answer too, and the double-voting ablation gives
+it across 1,169 steps — nothing about the task order matters there, so that
+race lives in the fault timing, in where the partition falls relative to the
+election timeouts.
+
+Re-run any detection from the table:
+
+    uv run pytest examples/raft/tests/test_ablations.py::test_accepting_stale_terms_rewrites_history
+
+Shrinking is experimental and costs extra runs; the `--simloop-shrink` flag
+reaches `@sim_test` tests, while the ablations call `explore()` directly and
+take `shrink=True` as an argument.
+
+## Run it
+
+    uv run pytest examples/raft/tests -q            # fast suite: scenarios, units, ablations
+    uv run pytest examples/raft/tests -q -m slow    # campaign, the two safe proofs, the replay guard
+
+Add `-s` to either and the ablations print the explorer's report — the failing
+seed and the trace around it.
+
+Turn the campaign up and spread the seeds over cores:
+
+    uv run pytest examples/raft/tests/test_chaos_campaign.py -q -m slow --simloop-seeds=50000 --simloop-jobs=8
+
+Replay any campaign failure exactly:
+
+    uv run pytest 'examples/raft/tests/test_chaos_campaign.py::test_chaos_campaign_holds_the_invariants' -m slow --simloop-replay=0

examples/raft/raft/node.py

@@ -27,7 +27,9 @@
 LEADER = "leader"
 
 # One observable fact, appended in order: ("leader", name, term, log_snapshot)
-# or ("apply", name, index, term, command). The safety checks read these.
+# or ("apply", name, index, term, command, node_term), where node_term is the
+# applier's current term -- on the first apply of an index that is the term
+# whose leader committed it. The safety checks read these.
 Event = tuple[Any, ...]
 
 
@@ -72,7 +74,7 @@ def __init__(
         self._safeguards = safeguards if safeguards is not None else Safeguards()
         self._events = events
         self._state = storage.load()
-        self._quorum = (len(peers) + 1) // 2 + 1
+        self._quorum = (len(self._peers) + 1) // 2 + 1
         self.role = FOLLOWER
         self.commit_index = 0
         self.applied: list[Entry] = []
@@ -99,15 +101,19 @@ def log(self) -> tuple[Entry, ...]:
     # ------------------------------------------------------------------
 
     async def run(self) -> None:
-        handlers: set[asyncio.Task[None]] = set()
+        # An insertion-ordered dict rather than a set: the sweep below cancels
+        # these in iteration order, and a set of tasks iterates by id(), which
+        # moves between runs -- two handlers swapping places there is enough to
+        # give one seed two different traces.
+        handlers: dict[asyncio.Task[None], None] = {}
 
         async def connection(
             reader: asyncio.StreamReader, writer: asyncio.StreamWriter
         ) -> None:
             task = asyncio.current_task()
             assert task is not None
-            handlers.add(task)
-            task.add_done_callback(handlers.discard)
+            handlers[task] = None
+            task.add_done_callback(lambda done: handlers.pop(done, None))
             await self._connection(reader, writer)
 
         server = await asyncio.start_server(connection, "0.0.0.0", self._port)
@@ -396,6 +402,11 @@ def _apply(self) -> None:
             self._applied_index += 1
             if entry.command:
                 self._record(
-                    "apply", self._name, self._applied_index, entry.term, entry.command
+                    "apply",
+                    self._name,
+                    self._applied_index,
+                    entry.term,
+                    entry.command,
+                    self._state.term,
                 )
                 self.applied.append(entry)

examples/raft/tests/checks.py

@@ -0,0 +1,91 @@
+"""The four Raft safety claims every intact run must satisfy."""
+
+from __future__ import annotations
+
+from itertools import combinations
+
+from raft.node import Event
+from raft.storage import Entry
+
+
+class InvariantViolation(AssertionError):
+    def __init__(self, invariant: str, detail: str) -> None:
+        super().__init__(f"{invariant}: {detail}")
+        self.invariant = invariant
+
+
+def check_invariants(
+    logs: dict[str, tuple[Entry, ...]], events: list[Event]
+) -> None:
+    _election_safety(events)
+    # Order matters: leader-completeness keeps only the first apply seen at an
+    # index, which is the whole story only once state-machine safety holds.
+    _state_machine_safety(events)
+    _leader_completeness(events)
+    _log_matching(logs)
+
+
+def _election_safety(events: list[Event]) -> None:
+    leaders: dict[int, set[str]] = {}
+    for event in events:
+        if event[0] == "leader":
+            _, name, term, _ = event
+            leaders.setdefault(term, set()).add(name)
+    for term, names in leaders.items():
+        if len(names) > 1:
+            raise InvariantViolation(
+                "election-safety", f"term {term} elected {sorted(names)}"
+            )
+
+
+def _state_machine_safety(events: list[Event]) -> None:
+    applied: dict[int, tuple[int, str]] = {}
+    for event in events:
+        if event[0] == "apply":
+            _, name, index, term, command, _node_term = event
+            first = applied.setdefault(index, (term, command))
+            if first != (term, command):
+                raise InvariantViolation(
+                    "state-machine-safety",
+                    f"index {index} applied as {first} and, at {name}, "
+                    f"as {(term, command)}",
+                )
+
+
+def _leader_completeness(events: list[Event]) -> None:
+    # An entry committed under a term-T leader must appear in the log of
+    # every leader of a term above T. The floor is T itself, read straight
+    # off the first apply of the index: a follower only learns an index is
+    # committed from a later append carrying leader_commit, so the first
+    # apply of any index happens on the committing leader, and that event's
+    # node_term is the term it committed under. Leaders at or below the
+    # floor -- stale-term stragglers whose counted votes predate the commit
+    # -- are outside the paper's claim.
+    committed: dict[int, tuple[Entry, int]] = {}
+    for event in events:
+        if event[0] == "leader":
+            _, name, term, log = event
+            for index, (entry, floor) in committed.items():
+                if term > floor and (index > len(log) or log[index - 1] != entry):
+                    raise InvariantViolation(
+                        "leader-completeness",
+                        f"term-{term} leader {name} lacks committed "
+                        f"entry {index}: {entry}",
+                    )
+        elif event[0] == "apply":
+            _, _, index, term, command, node_term = event
+            committed.setdefault(index, (Entry(term, command), node_term))
+
+
+def _log_matching(logs: dict[str, tuple[Entry, ...]]) -> None:
+    for a, b in combinations(sorted(logs), 2):
+        log_a, log_b = logs[a], logs[b]
+        for index in range(min(len(log_a), len(log_b)), 0, -1):
+            if log_a[index - 1].term == log_b[index - 1].term:
+                if log_a[:index] != log_b[:index]:
+                    raise InvariantViolation(
+                        "log-matching",
+                        f"{a} and {b} agree on the term at index {index} "
+                        "but not on the prefix before it",
+                    )
+                break