raft: trace validation of the shell against Raft.tla (tla-trace)

[kiranandcode]

Implements the toyDB half of plans/tlc_conform.md: trace validation of the Raft shell. With --features tla-trace, the shell logs every safety-model transition it performs. TLC then checks each log against the model, here the hand-written tla/Raft.tla oracle (the exported Raft module is being produced separately).

Based on yl/raft-safety-refine (#16), which carries tla/Raft.tla (#25).

What was built

• tla-trace/ is a small, dependency-free crate. It writes the per-thread log: a header, then one JSON line per step, in the Verus exporter's value encoding (Value, start/finish). trace_step! logs a step and evaluates nothing when no log is open.
• Emission is behind the tla-trace feature, with no effect without it.
  • After each call of a verified step function, the shell (node.rs) logs the t_* transitions that call performed, with the model's parameters (ranks, terms, indices), through a local trace_step!.
  • Each line carries the stepping node's observed host: term, vote, role, log, commit, plus votes while a candidate and read_seq while a leader. It is read by a feature-gated view of Abs in refine.rs, placed after the verus! block; verified code is untouched.
  • A step function that performs several transitions logs each one. A follower heartbeat logs ack, read confirmation, then commit, the earlier lines without the commit that follows them.
  • A leader commit also logs the ack map q it rests on, which the leader knows from its match indexes. Otherwise TLC would branch over every ghost q.
  • Node::new on a used log is t_restart.
• The node goldenscripts each write target/tla-traces/node/<script>.ndjson when built with the feature. The header holds the model's initial hosts.
• tla/Raft_trace.tla is the oracle's trace spec. It has the same interface as the exporter's generated one (TraceLog, one VARIABLE, TraceInit, TraceNext, TraceEnabled, TraceDiagnosis), so verus-tools-mcp's tlc_conform runs either. tla/Raft_trace.cfg configures it, and tla/conform.sh runs every script's log through TLC.

Result: all 58 node goldenscripts conform

Each script conforms with exactly one explaining behaviour (distinct states = steps + 1). The scripts range from 0 to 248 steps, on 1 to 7 nodes.

The first run found one divergence, in the test harness, not the shell. cluster ... leader=N promoted its leader by calling collect_vote for every peer directly, with no Vote message behind the votes. 41 of the 58 scripts are built that way. The first run checked 47 scripts before my survey script crashed; 35 of those were built that way, and all 35 left the model at step 2, t_become_leader: Raft.tla's t_collect_vote needs the Vote in the network, so the leader's vote set was {0}. The harness now elects through the message path (campaign, then stabilize). Every goldenscript's output is unchanged.

A second issue was in my own harness code: a one-node cluster elects itself inside Node::new, so its log must open before the nodes exist.

Deviations from the plan

• trace_step! is called at the step-function call sites in the shell, not inside the verified step functions.
  • Several step functions hold only &Log, and reading the log's entries needs &mut.
  • An external_body taking &mut Log would havoc the log in the proofs.
  • The shell sees each step function's result, so it knows which transitions ran.
• Raft_trace.tla does not conjoin Next again, unlike the generated trace spec. Each TraceStep arm is t_x(i) for a node i, which is a disjunct of Next. Re-evaluating all of Next made TLC enumerate t_leader_commit's ack maps [Q -> 0..MaxLog] at every step, past a million functions at N = 5. For the same reason, t_leader_commit is taken at its logged witness (Q, q) (LeaderCommitAt, its body with the existentials instantiated).
• The log's commands are only noop-or-not; Raft.tla abstracts commands to Command (A2), and the trace runs with Command = {c1}.
• Plan step 3 is checked against the hand-written oracle, as instructed, not the export. Once the Raft export is faithful, TOYDB_TLA_TRACE_MODULE renames the header's module and the same logs apply. One caveat: the generated trace spec needs every step parameter logged or finitely bounded, and the shell cannot log ghost payloads such as clog/vlog/rec.

Test plan

• cargo test (without the feature): every raft goldenscript passes, output unchanged by the harness election change.
• cargo test --features tla-trace --lib raft::node::tests writes 58 logs.
• TLA2TOOLS_JAR=<fork jar> tla/conform.sh: all 58 conform, exit 0.
• Through the MCP server (BasisResearch/verus-tools-mcp#59), tlc_open tla/Raft.tla then tlc_conform on election.ndjson with constants: ["N = 3", "MaxTerm = 20", "MaxLog = 50", "MaxRead = 50", "Command = {c1}"]: conforms (20 steps, 21 states). A copy logging ci = 2 for a one-entry leader diverges at step 15: the step is not enabled, and the model state and enabled steps are reported.
• cargo fmt --check; cargo clippy --tests --no-deps -- -D warnings, with and without --features tla-trace; cargo doc --no-deps; tla-trace crate tests and clippy.
• t_recv_append is pinned to the logged Append (term, base, base term) and to the ack built from the logged match_index (RecvAppendAt). All 58 scripts still conform.
• CI: the Test job runs clippy and the tests with --features tla-trace, plus fmt, clippy and the tests of the tla-trace crate. A new Trace validation job downloads the pinned basis-11305b4a05 jar (sha256-checked) and runs tla/conform.sh over every node goldenscript's log (all 58 must conform), then tla/conform.sh tla/traces/*.ndjson over the two known-bad fixtures. election-bad-quorum must diverge at step 15 (a commit on a non-quorum ack map). election-bad-ack must diverge at step 10 (a follower acking past the Append it applied); the unpinned spec accepted this one.
• Verus gate: left to CI (no released cargo-verus on this machine). The verus! block is unchanged; the new refine.rs code is a feature-gated module after it.

Companion PRs: BasisResearch/verus#54 (the exporter's trace spec) and BasisResearch/verus-tools-mcp#59 (tlc_conform).

🤖 Generated with Claude Code