tla: export safety.rs with Verus's TLA+ exporter and compare it with Raft.tla

[kiranandcode]

Step 4 of plans/tla_export.md: run Verus's TLA+ exporter (-V tla-export) on src/raft/safety.rs and check the generated module with TLC against the hand-written oracle tla/Raft.tla, at the same bounds. The comparison is written up in tla/EXPORT.md. The exporter fixes it needed are in BasisResearch/verus#53.

What is here

• tla/export/GState_tla.{tla,cfg,tla.json}: the exporter's output, unedited. export.sh regenerates it byte for byte.
• tla/export/RaftExportMC.tla and .cfgs: fill only what the export's report asks for. That is the three hole constants (a command payload, the ghost ack map q, and t_bump_term's new term), hosts (which init fixes only through n), and Raft.tla's state constraint. There is one .cfg per oracle configuration (Raft.cfg, deep_lc, deep_reads, and both witnesses).
• tla/export/RaftExportCti.tla, .cfg, cti.sh: Raft_cti.tla's seed family in the export's representation, with the per-conjunct probe loop.
• tla/export/oracle.sh, Raft_noA3.cfg, Raft_deep_lc_noA3.cfg: the oracle columns. oracle.sh a3 runs the same probe loop on Raft_cti.tla. oracle.sh noa3 deletes the four (A3) guard lines in a temporary copy of Raft.tla, then runs Raft.cfg and Raft_deep_lc.cfg without TypeOK (which the guard-free past-bound successors violate), followed by the probe loop.
• tla/Raft_cti.tla: inv_ack_persist_dom, the oracle's side of the restricted inv_ack_persist probe.
• tla/EXPORT.md: the comparison. README.md now points to it, and gives the reads witness as 14 states (the shortest, as a one-worker run finds for both models).

Results

	Raft.tla	export
Raft.cfg: distinct / diameter / conjuncts violated	597,764 / 18 / none	597,764 / 18 / none
Raft_deep_lc.cfg	390,622 / 20 / none	390,622 / 20 / none
Raft_deep_reads.cfg	10,849,481 / 24 / none	10,849,481 / 24 / none (24 with one worker; 16 workers report 25, an upper bound)
witnesses NoLC / NoR2	13 / 14 states	13 / 14 states
CTI probe: conjuncts with CTIs	msgs, lterms, ack_persist, vote_persist, leader_completeness, host_commits	the same six, from the same transitions

Every difference is accounted for in EXPORT.md:

• Exporter bugs, all fixed in verus#53. Set::range was refused; message-field quantifiers and step fields were holes; the guarding disjunction in t_recv_append stopped TLC.
• Raft.tla's (A3) action guards. They explain the generated-state counts (8,796,586 vs 7,324,630) and the extra inv_msgs / inv_lterms CTIs. Deleting the guards from a copy of the oracle reproduces every one of those numbers exactly.
• Raft.tla's (A5) total-map reads. The export's inv_ack_persist probe stops at an off-domain leader_log[t], where the oracle reads << >>. Restricted to in-domain acks, both models give 384 CTIs. In reachable states no map read is ever off its domain.

Deviations from the plan

• The deep-reads diameter needed one-worker runs of both models: TLC's multi-worker depth is only an upper bound, and the export's 16-worker run reported 25.
• Two holes are not ghost payloads. The plan's acceptance criterion is "the holes list is empty or names only ghost-payload quantifiers". Of the three holes, only t_leader_commit's ack map q is a ghost payload. The other two are real step parameters that no guard bounds, and no exporter could bound them. t_bump_term's t: nat has only the lower bound t > h.term, so the hole is filled with 1..MaxTerm: under the guard that is Raft.tla's (h.term+1)..MaxTerm, and the constraint excludes any larger term. t_propose's cmd: Option<Seq<u8>> ranges over all byte strings, filled with an NCommands-element alphabet, which is Raft.tla's (A2).
• The comparison also runs the oracle with its (A3) guards removed. The plan asks only for a comparison with the oracle, but this variant is what shows that the count differences come from the guards.

Test plan

• tla/export/export.sh with the verus#53 build regenerates GState_tla.* byte for byte.
• TLC: RaftExportMC.cfg, _deep_lc.cfg, _deep_reads.cfg, and both witness configurations, with the numbers above. Deep reads and the reads witness were also run with one worker for both models.
• tla/export/cti.sh: the export column of the CTI table. tla/export/oracle.sh a3 and oracle.sh noa3: the two oracle columns and the "without (A3)" state counts (8,796,586 and 5,075,165 generated), all as tabulated, including 384 for inv_ack_persist_dom on both sides.
• The "Running it" commands in EXPORT.md and README.md reproduce the tables. The witnesses run with one worker; with four, the reads witness came out at 15 states. With one worker, the export's Raft.cfg and deep_lc diameters are still 18 and 20.
• No Rust source changes, so cargo build, test, clippy and fmt are unaffected.

🤖 Generated with Claude Code