Add -V tla-export: export a Verus transition-system model to TLA+

[kiranandcode]

Summary

vir::tla exports any module's (State, init, next, invariants) triple to TLA+ so the tlc_* MCP tools can model-check it, with nothing keyed on one project. Plan: verus-research/plans/tla_export.md.

• Three shapes recognised. Hand-rolled init(s) / next(pre, post) with a step enum and (State) -> bool invariants; VerusSync's state_machine! output (init_by, next_by, Step); verus-tla's init()/next() closures with Action { precondition, transition } records, reduced symbolically through variables, record fields and calls returning closures.
• Variables are the state struct's fields. A state-typed parameter in the pre or post role is dropped from its operator and read as the unprimed or primed variables; post == e on a whole state becomes one primed assignment per field, the shape TLC needs to enumerate.
• Types and definitions. Records for datatypes (a tag for enums), 1-based sequences for Seq (every index shifted once; seq![a, b] is <<a, b>>), sets, functions for Map (DOMAIN, :>/@@), operators for spec fns in dependency order, IF chains for match (a literal pattern an equality with the scrutinee, a range pattern its comparisons), LET for let.
• Quantifier bounds. From the guard (set membership, a map's domain, integer ranges from inequalities and chained comparisons, through binders bound later: 0 <= a < b < n bounds a by n - 2), intersected with the binder's integer type range (the type also closes a side the guard leaves open); from a finite type of at most 2^10 values (booleans, u8/i8, datatypes whose fields are bounded; a variant whose fields together take more has a Dom_<Type>_<variant>_<field> hole per field, so Step::Upd(u16, u16) is never enumerated), else a CONSTANT Dom_<Type> the cfg supplies, named after the type (Dom_u32, Dom_int), reported as a hole. Everything outside the fragment (choose, old, closures outside a known call, floats) is a refusal with its location, printed as Assert(FALSE, "...") so TLC stops wherever it is evaluated; an invariant that reaches one is left out of the .cfg. Hole constants are left unassigned (commented) in the .cfg, so TLC stops until they are given.
• Invariants. By default: the #[invariant]s for VerusSync (the conjuncts of the generated State::invariant, so <transition>_enabled predicates are not checked), every () -> spec_fn(State) -> bool for verus-tla, and every (State) -> bool spec fn for a hand-rolled model (one named invariant included) except one init/next read, unprimed or primed (a guard), and one another selected invariant calls (a helper: big in inv(s) = big(s) ==> !marked(s) is checked inside inv, not alone). When none is checked, the .cfg says so and lists the candidates with their reasons. -V tla-export=<module>:inv1,inv2 checks exactly the named ones. The report's candidates lists every candidate, included or not, with the reason.
• Arithmetic and names. / and % by anything but a positive literal go through EuclidDiv/EuclidMod (Verus's Euclidean semantics; TLC's \div rounds down and its % rejects a negative divisor). Option's spec helpers (spec_unwrap, arrow_0, is_some, ...) are recognised by the receiver's type, so a crate function of the same name is left alone. A state field named like a generated name (vars, Init, ...) or a TLA+ reserved word is held in a renamed variable.
• Integer types. TypeOK keeps every bounded integer the state holds (nat, uN, iN, through records, enum payloads, tuples and Seq/Set/Map elements) in its type's range, conjoined to Init and primed to Next, so a step that would leave the type is disabled as in Verus; bounds beyond TLC's 32-bit integers are left out. The report's typed_variables lists them.
• Casts. A widening cast (the operand's type lies in the target's, u8 as u16, as nat) is the identity. A narrowing one ((pre.x - 1) as nat, as u8, ...) is a value check, LET c == e IN IF <c in range> THEN c ELSE Assert(FALSE, "... value out of range of <type> in a cast at <location>"): Verus gives an out-of-range value some unspecified value of the type, so TLC stops only in a reached state whose value leaves the type (never behind a guard like pre.x > 0). It is not a refusal and taints nothing. A literal is decided at export: kept in range, refused out of it.
• Transitions. The report's transitions lists each transition Next reaches (an operator called in a disjunct, IF/match arm or exists, with the operators it conjoins) and the variables it never assigns (only a conjunct-level v' = e or =~= (VerusSync's tmp_assert => ... lowering of assert keeps its consequent at conjunct level), a conjunct-level call to an operator that assigns it, or an IF/match/disjunction all of whose branches assign it, counts, two conjunct-level implications of complementary guards (g/!g, x < y/x >= y, x == y/x != y) assigning what both consequents do, in Next and Init, a branch that is the literal false (VerusSync's dummy_to_use_type_params => false arm) counting as assigning everything, together with what the transition's callers assign around it, so a frame condition factored out of a disjunction counts for every branch; pre.y == post.y is printed y' = y, since TLC assigns only a primed variable on the left, and of two primed fields the one not yet assigned goes on the left); the .cfg names any that leaves one unassigned and says what the check can miss (conjunct order, v' \in S), since TLC stops there with "successor state not completely specified". Init is checked the same way: the report's init_unassigned and a .cfg line name any variable Init never assigns (TLC: "current state is not a legal state"), and 0 == s.x is printed x = 0; s.x == s.y assigns whichever an earlier conjunct left unassigned (printed on the left); a bare or negated bool field (s.done, !post.done) is printed done = TRUE / done' = FALSE and assigns it, in Init and Next.
• Flag. -V tla-export=<module>[:inv1,inv2] runs before ast_simplify, under --no-verify too, and writes <State>_tla.tla (named after the module it declares, so TLC loads it directly), a .cfg skeleton and a .tla.json report under the log directory.
• Trait impls. A trait method call Verus resolved to an impl exports the impl's function.
• Names. An enum value's record carries its variant in tag, so a field named tag (or tag plus underscores) takes one more underscore (tag_). Every local name is fresh within its operator and distinct from operators, variables and constants (TLA+ forbids redefining a name in its scope); a recursive function (decreases) is printed only as its record variant f_rec, the state passed as a record (a recursive root is a wrapper cnt == cnt_rec([n |-> n, m |-> m])), and only operators in a call cycle are declared RECURSIVE with their arity; a callee given post is a primed variant of its operator rather than a primed application.

examples/tla/ has one fixture per shape (plus toggle_sync.rs, VerusSync with parameterless transitions, and assert_sync.rs, VerusSync with an assert) and the hand-written Counter.tla. The counter export model-checks under TLC with exactly the hand-written spec's numbers (28 generated, 18 distinct, the same six violations); the VerusSync export is clean apart from the step's int parameter, which is a hole; the verus-tla export has no hole or refusal and checks under TLC (10 distinct states, both invariants hold).

Test plan

• vargo build --release clean.
• rust_verify_test --test tla_export: exports the four fixtures and probes for each shape the export once got wrong (including a crate fn named unwrap, negative div/mod, a field named vars, a guard predicate, an explicit invariant list, an unknown invariant name, state fields a/b beside Euclidean division, a u8 cast, Option<bool> beside Option<int>, a transition leaving a field unassigned, bounded-integer fields kept in range by TypeOK (TLC-checked), a trait impl call, guard-only and branching assignments, escaped char literals, pre.y == post.y and =~= with the post state on the right (TLC-checked), equalities of two primed fields, a hand-rolled invariant (TLC-checked), the .cfg comment when no invariant is checked, whole-state =~= (TLC-checked), a frame condition factored out of a disjunction (TLC-checked, plus real gaps in a called and an inline branch), widening casts and a narrowing value check that holds (TLC-checked), a narrowing cast TLC stops at when the reached value leaves u8, a guarded as nat/as u8 decrement (TLC-checked), a false branch counted as assigning everything (TLC-checked), what Init leaves unassigned (plus a fixed Init, TLC-checked), a field named tag (TLC-checked), u8/i8 binders bounded by their type and a u32 hole named Dom_u32 (TLC-checked), a chained guard bounding a binder through a later one (TLC-checked), a guard read on the post state left out of the invariants (TLC-checked), updates under a VerusSync assert counted as assigning (TLC-checked), a recursive invariant next reads on post plus a mutual recursion, by default and named (TLC-checked), complementary implications in Next and Init (TLC-checked) and a non-complementary one reported, seq! literals (TLC-checked), the VerusSync fixtures' transitions/init_unassigned, an export under --no-verify of a crate with an unprovable proof (TLC-checked), a step with Put(u16, u16), Pair(u8, u8) and Mixed(Option<int>, u8, u8) left as per-field holes beside a whole Nudge(u8) (TLC-checked), helpers an invariant calls left out by default and checked when named (TLC-checked), an Init equality of two fields assigning the unassigned one (TLC-checked), literal and range match patterns (TLC-checked), bare/negated bool fields assigning in Init and Next (TLC-checked), and swapped states (moved(post, pre)) and one state given twice (frame(post, post), same(pre, pre)) called in the record variant (TLC-checked), an Init helper same(s) = s.x == s.y read as it is printed (x = y, so y is reported unassigned after s.x == 0; TLC-checked), a helper checked on its own when the invariant calling it reaches a refusal (TLC-checked), and a one-variant fieldless enum enumerated as {[tag |-> "unit"]} rather than a hole (TLC-checked), Seq/Map/Set binders and step payloads as holes named after the type (Dom_Seq_u8, Dom_Step_Store_v0) and a Set<bool> as SUBSET BOOLEAN, never records of their representation (TLC-checked), and an or-pattern binding nothing as a disjunction (Step::A | Step::B, Step::C(1) | Step::C(2); TLC-checked)); with TLA2TOOLS_JAR set, SANY parses every export (checked by exit status and its semantic-processing line) and TLC checks counter (against Counter.tla), adder, mutex and probes. Passes with and without the jar.
• rust_verify_test --test examples -- examples_tla: the fixtures verify.
• cargo fmt -- --check; vargo clippy -p vir|rust_verify|rust_verify_test -- -D warnings and cargo clippy -p rust_verify_test --test tla_export -- -D warnings.
• cargo clippy -p rust_verify_test --test tla_export -- -D warnings.

Lands together with verus-tools-mcp#55

This PR writes the export as <State>_tla.tla. verus-tools-mcp's tla_export used to expect crate-<State>.tla and rename it; https://github.com/BasisResearch/verus-tools-mcp/pull/55 (branch kg/tlc-tools) takes <State>_tla.tla as written. Merge the two together: this one alone would leave the tool writing State_tla_tla.tla.

🤖 Generated with Claude Code