tla-export: a trace spec for trace validation (tlc_conform)

[kiranandcode]

Implements the exporter half of plans/tlc_conform.md: -V tla-export now also writes a trace spec beside the export, which TLC uses to check that a logged run of the implementation is a behaviour of the exported model.

What was built

• Trace format (project-independent, documented in examples/tla/README.md and in the generated module's header). The log is newline-delimited JSON: a header line naming the module and the export ({"module": "State_tla", "export": "counter"}, optionally with "state", the observed initial state), then one line per step, {"step": "t_inc", "params": {...}, "state": {...}}.
  • step names a transition (a spec fn given the post state) that Next reaches through its branches (an IF, match, disjunction or exists): a step, a helper a step branches into, or a dispatcher on a Step enum (next_step, VerusSync's next_by). A transition Next conjoins is a step when it branches into steps itself or is the only transition Next conjoins (next = t_step). A guard on the pre state or on a value is never a step. It is given by its last segment or its full path. Next itself is a step only when it reaches none of these (the verus-tla shape). When two steps share a last segment, only the full path is accepted: the report marks them short_name_shared, and the short name stops TLC with an Assert naming the candidates.
  • params holds its parameters other than pre/post, by Rust name. A name the step does not declare stops TLC (TraceParamsDeclared), so a misspelling is not silently ignored.
  • The header's module must be the generated module and its export the module path given to -V tla-export; TraceInit asserts both. Exports whose state types share a name share a module name (State_tla), so the module name alone does not identify the export.
  • state holds the observed fields after the step.
  • Values use the exporter's encoding: records, tagged enums/Options, arrays for Seq and tuples, element arrays for Set, [k, v] pairs for Map.
  • Objects observed in the state are partial, so a field left out (ghost state) stays free. A key naming no field of its type stops TLC. A struct without fields is {} (the export's [tag |-> "unit"]). A Seq can be observed by index ({"1": {...}}), {} observes nothing of it, and [] is the empty Seq. A record inside a Set element, a Map key or a parameter is decoded whole and must name every field (documented in the README and the generated header).
• <State>_tla_trace.tla (vir/src/tla.rs, Exporter::trace_spec), plus a .cfg skeleton. It EXTENDS the export and reads the log with the Json module (ndJsonDeserialize).
  • TraceNext conjoins Next and then the logged step (a CASE over the transitions Next reaches), so it only ever narrows the model, and a helper step reads the successor Next assigned. TraceEnabled and TraceDiagnosis use the same order. It then compares the observed fields in the successor.
  • The observation and decoding operators are generated per type from the same type map the export uses (TraceDec_T, TraceObs_T, all RECURSIVE). A parameter left out of the log ranges over what Next's calls to the step pass it, the union over every call: the bound Next gives the quantifier binding the argument (exists|n: u64| n < 3 gives 0..2), or the field of a value matched against a constructor pattern, whatever the parameter's position (a VerusSync step's Dom_Step_<t>_v<i>, a hole of the field's own type). A hole is accepted only for a parameter of its type. Failing that, it ranges over its type's finite domain, never the export's Dom_<Type> hole, which holds only what a quantifier binds and not a value a call computes. A logged parameter is narrowed to its domain, so a value outside it is a step the model cannot take. The verus-tla shape has a single step, next.
  • An enum observed in the state without its tag leaves the tag free: the fields it names are compared under whichever variant the model has. Decoded whole (a parameter, a Set element or a Map key), an enum value without a tag stops TLC with an Assert saying so.
  • At a divergence, TraceEnabled gives the model's enabled steps with their parameters. TraceDiagnosis says whether the logged step is enabled at all, and which observed fields no successor matches.
• The report's new trace section lists the trace module, the index variable, the observable fields, and every loggable step with its parameters and domains, and whether TraceEnabled enumerates it (enumerated).

Deviations from the plan

• The trace module is named <Module>_trace (State_tla_trace.tla), not <State>Trace.tla. It follows the export's own <State>_tla naming, and tlc_conform finds it by that rule.

• The verdict is not an invariant or postcondition. TLC ends without error either way. The log conforms when the search depth is its step count plus one (TraceAccepted); otherwise the deepest index is the divergence. Depth 0 (TLC generates no initial state) means the header's observed state is not an initial state (documented in the trace spec, its .cfg and the README). This keeps nondeterminism in what the log leaves out from producing false divergences: a deadlock in one branch is not a verdict.

• Enabled steps come from a generated TraceEnabled evaluated in the diverging state, rather than from tlc_neighbours. Neighbours would list the trace spec's single TraceNext action, not the model's steps.

• TraceNext conjoins Next, so the .cfg's Dom_ constants must cover every value the log carries: a logged value outside a hole is a divergence (the README, the generated header and the .cfg comment say so).

• A step parameter with no domain (no call passes it a bounded variable, and its type has no finite domain) must be logged. If it is not, the step Asserts with that reason, and it is left out of TraceEnabled; the report marks the step "enumerated": false.

• A pass means the observed state sequence is a behaviour of the model; the logged step's name and parameters count only through their effect on the observed state. TraceNext requires a successor both Next and the logged step allow, not that Next took it by that step, so a step another of Next's steps explains is accepted (the README gives an example; the generated header says so too). The plan's "constrains Next to the logged step and parameters" is met for states, not for the step's identity. Restricting Next to the logged step's call sites is left as a follow-up.

Test plan

• tla_export_trace_spec_follows_a_counter_log: the counter's trace spec parses (SANY). counter_trace_ok.ndjson (5 steps) is followed to depth 6. counter_trace_bad.ndjson logs t_dbl where the counter took t_inc; TLC stops at step 4 with t_dbl enabled and x unmatched, and TraceEnabled = {t_dbl, t_inc}.
• tla_export_trace_spec_decodes_collections_and_parameters: Seq of records (whole and partial by index), Set, Map, Option, and a tagged enum with a payload, plus a u8 parameter logged and a bool one left out (it ranges over BOOLEAN). A parameter the guard forbids stops the log at step 1.
• tla_export_trace_spec_stops_at_a_malformed_log: a header for another module, an undeclared parameter, an unknown step and an unknown state field each stop TLC with their Assert.
• tla_export_trace_spec_names_a_shared_step_by_its_path: a::step and b::step are both reported short_name_shared. A log by full paths is followed, and the short name step stops TLC.
• tla_export_trace_spec_follows_a_verussync_log: adder_sync's add(v: int) reports domain Dom_Step_add_v0. A log leaving v out is followed. A step no v explains stops at depth 2, where TraceEnabled enumerates v over the hole.
• tla_export_trace_spec_decodes_a_record_in_a_set_whole: a partial record in the state and a whole one in a Set are followed, and a partial Set element stops TLC.
• tla_export_trace_spec_logs_a_step_that_branches_into_helpers: t_recv(b) is if b { bump } else { reset }, and bump is also a branch of t_other. The steps are bump, reset, t_other and t_recv. A log naming t_recv (with b logged, then left out), t_other and bump is followed to its end, and t_recv with b false where the state shows bump stops at step 1.
• The collections test also observes a Map with record values partially (keys whole), and an enum whose variants Lo(u8) and Hi(u8, bool) share the label v0. A wrong value field, a wrong key, the wrong tag or a wrong shared-label value each stops the log at that step.
• The malformed-log test also checks a header naming another export, and one naming no export.
• A key a step line or the header does not define ("stat", "param", a header's "State") stops TLC (TraceKeys), as does a step line without "step", so a misspelling never observes nothing. A Seq observed by a key that is no index ({"x1": ...}) stops TLC; an index past the end only diverges.
• tla_export_trace_spec_takes_next_before_the_logged_step: a helper chk reading y' = x', which its caller assigns, is followed when logged. next = t_step makes t_step loggable, and the conjoined frame is not a step.
• tla_export_trace_spec_logs_no_guard: guards in a branch (ready(pre), small(v)) are not steps. With next = ready(pre) && t_only(pre, post), the only step is t_only.
• tla_export_trace_spec_follows_a_verus_tla_log: mutex_tla.rs, whose only step is next, observed through Option holder. A wrong thread or count stops the log.
• The collections test also checks that "s": {} is followed and "s": [] stops on a non-empty Seq.
• tla_export_trace_spec_takes_a_parameter_domain_from_the_match: Step::t_set(f, n) passes its fields to t_set(n, f) swapped. n: int gets Dom_Step_t_set_v1 and f: bool the v0 field (the booleans). Before this, f got the int hole. A log leaving each out is followed, and an n outside the hole stops the log.
• tla_export_trace_spec_takes_a_parameter_domain_from_a_quantifier: exists|n: u64| n < 3 && t_go(n) gives n the domain 0..2, and TraceEnabled lists t_go's three. t_jump(pre.x + 5) has no domain, is "enumerated": false, and leaving to out stops TLC with the reason.
• tla_export_trace_spec_diverges_at_a_bad_header_state: a header state that is not an Init state ends at depth 0 with 0 states generated.
• tla_export_trace_spec_leaves_an_unobserved_tag_free: {"v0": 2} without a tag is followed. A field the model's variant lacks, or a wrong value, stops the log. A tagless enum parameter stops TLC with the tag Assert.
• tla_export_trace_spec_binds_no_name_of_the_export: a state with fields v, k, e, j, p, r (a Seq, a Map, an Option). Every name the trace module binds is fresh against the export's (TraceParam(e_2, k_2, Dec(_), D)), SANY accepts it, a log is followed and a wrong value diverges.
• tla_export_trace_spec_decodes_a_unit_struct: a struct without fields is observed from {} or {"tag": "unit"} and decoded whole as a parameter. A field named in it stops TLC.
• A key naming no field of its type stops TLC (Rec has no field aa, Mode has no field v2), as a misspelled state field does. A label another variant declares still only fails to match.
• tla_export_trace_spec_takes_no_hole_for_a_computed_argument: t_jump(pre, post, pre.x + 5) beside exists|n: int| t_set(pre, post, n) gives to no domain (not Dom_int) and "enumerated": false. to 5 logged, outside Dom_int = {0, 1}, is followed; left out, it stops TLC with the reason. A logged n 7 outside Dom_int stops at step 1. t_jump with to 0, which t_set(0) explains, is followed (the label limitation).
• Full tla_export suite with TLA2TOOLS_JAR set: 79 passed.
• cargo fmt -- --check, cargo clippy --all-targets -- -D warnings (in source/).

Companion PRs: verus-tools-mcp tlc_conform (runs this trace spec) and toyDB (trace_step! emission, and all 58 node goldenscripts conforming to the hand-written tla/Raft.tla).

🤖 Generated with Claude Code