tla-export: bound message and step fields from their guards; Set::range; guarded disjunctions (tla_export step 4)

[kiranandcode]

Step 4 of plans/tla_export.md: export toyDB's Raft model (src/raft/safety.rs) and model-check it against the hand-written oracle tla/Raft.tla. The comparison itself is in BasisResearch/toydb (tla/EXPORT.md, branch kg/raft-export). This PR holds the exporter fixes it needed. Each fix is general; nothing keys on toyDB.

What the first export of safety.rs got wrong, and the fix

found	effect on safety.rs	fix
Set::<int>::range(0, n) refused (an uninterpreted FiniteRange::range_set)	node_ids, so inv_hosts, inv_lterms and inv_commits were left out of the .cfg	Set::range / range_inclusive / range_set over integers print as lo..hi-1 / lo..hi; other element types are refused
forall|c, t, clog| net.contains(Msg::Campaign { c, term: t, clog }) ==> .. gave one Dom_<type> hole per binder	44 holes across the invariants, and products like 3·3·43·3·43 per state	a binder that is a field of a constructor (also nested) in an S.contains(..) / M.contains_key(..) guard ranges over {m.f : m \in {m \in S : m.tag = "Ctor"}}
b == 0 || (b <= h.log.len() && h.log[b - 1].term == bt) printed as \/	TLC branches on \/ in an action, evaluates h.log[0] and stops (the oracle hand-wrote an IF for exactly this)	a disjunction of two state predicates (neither reads the post state, also through a let or match binding), outside what Init reaches, prints as IF a THEN TRUE ELSE b
exists|step: TStep| next_step(pre, post, step) bounded as the union of every variant's values	41 step-field holes, and TLC building about 8,000 records per state (roughly 10x slower)	an exists over a datatype that the body (or the function it passes the binder to) matches on is one \E per variant. Each field is bounded from the guard of the transition its arm calls (0 <= i < pre.n, net.contains(Msg::X { .. }), b <= e <= h.log.len()), including the callee's lets that read only bound fields. A field that only its type bounds keeps the 2^10 cap and the split-into-holes rule of bound_variants

After these fixes, safety.rs exports with 0 refusals and 3 holes: the payload of a proposed command, the ghost ack map q, and t_bump_term's new term. None of the three is bounded anywhere in the model. With them filled from tla/Raft.cfg's bounds, TLC finds 597,764 distinct states, diameter 18, no conjunct violated, the same as the oracle. The only difference is states generated (8,796,586 vs 7,324,630), which equals the oracle's own count once its hand-added action guards (its (A3)) are removed.

Deviations from the plan

• The plan's bound analysis lists S.contains(x), map domains and ranges. Constructor-field membership and per-variant step expansion are additions. Without them TLC could not check the Raft export at the oracle's bounds (the unbounded holes multiply per state).
• The disjunction rewrite is not in the plan. It is TLC evaluation semantics (the plan's "shift once" style of invariant), found by the oracle comparison.
• The IF rewrite is applied only outside the operators Init reaches, because in Init a \/ may be what assigns the state. An operator Init and Next share keeps its \/, as before this PR.

Test plan

• New tla_export_bounds_message_fields_and_step_fields_from_their_guards: a small model with a node range, message-field quantifiers, the guarded index disjunction and a step enum dispatched to transitions. It asserts no holes and no refusals, checks the printed shapes, and runs SANY plus TLC (144 distinct states, which an independent breadth-first search of the same system also gives).
• tla_export_caps_a_domain_read_off_a_type updated to the per-variant \E shape. Its holes, and its TLC count of 22, are unchanged.
• Review fixes (744f1b6): a step field is bounded only from the first arm that could match its variant, when that arm is unguarded, the variant's constructor and binds each field plainly or with _ (else its type or a hole); Set::range_inclusive(lo, hi) prints as (lo..hi \cup {hi}), as vstd holds hi even below lo. New tests: tla_export_bounds_a_step_field_only_from_an_arm_taking_every_value (refutable, guarded and wildcard arms: 9 states, 4 before the fix), tla_export_keeps_a_disjunction_init_reaches (2 initial states, plus range_inclusive), tla_export_bounds_a_nested_tuple_and_map_key_constructor_field.
• Review fixes (da11dc1): a call giving a helper a post-state argument (pick(post.x)) goes to its _postarg operator, whose disjunctions keep \/ so TLC can assign through them; parameters of reduced applications likewise; the record variant of a recursive function stays one operator and keeps \/, as on main. A step field's domain never reads the step binder, the callee's scrutinee or a destructured let local. New tests: tla_export_keeps_a_disjunction_over_the_post_state (helper, let and match: 9 states), tla_export_bounds_a_step_field_whose_guard_reads_the_step (callee and inline match: 7 states).
• Review fix (90253e3): a local kept symbolically as a closure, or a record of closures, that captures post reads the post state, so a disjunction of its applications keeps \/. Before this fix it became an IF and TLC stopped on an undefined x'. New test tla_export_keeps_a_disjunction_over_a_closure_reading_the_post_state (7 states; it fails without the fix).
• Whole tla_export suite with TLA2TOOLS_JAR set: 69 passed. toyDB's export regenerates byte for byte.
• cargo fmt -- --check; cargo clippy -p vir -p rust_verify_test --all-targets -- -D warnings.
• End to end: toydb tla/export/export.sh regenerates the committed export byte for byte; TLC runs of the main, deep_lc and witness configurations, plus the per-conjunct CTI probes (see toydb tla/EXPORT.md).

PRs #50 (model tools) and #51 (liveness) also edit vir/src/tla.rs; expect textual conflicts in quant / Exporter fields when they merge.

🤖 Generated with Claude Code