Repository navigation
tla-export: the trace spec selects the logged step's arm - #62
Merged
Merged
Conversation
…-research/trace-arm-eval)
…eview policy Preserve conditional action path guards and fixed-argument call sites. Keep unsupported occurrences as reported Next-conjoined relations instead of dropping names or incompletely selecting the remaining occurrences. Nest dependent enum-field domains and preserve hole bookkeeping when probing trace parameter domains. Add TLC regressions for omitted dependent parameters, out-of-domain values, and TypeOK enforcement. Embed trace-policy metadata for the companion MCP preview change in BasisResearch/verus-tools-mcp#68, including unknown-name fallback reporting. Validation: release build, 182 exporter tests with TLA2TOOLS_JAR, vargo fmt, and cargo clippy --all-targets -- -D warnings. Six fixture model modules remain byte-identical to the PR baseline. MCP conformance rejects the conditional-action reproduction and qualifies unknown-name fallback; the 551-step LRU log conforms in 0.686 seconds.
- Require action wrappers to execute both precondition and transition; otherwise retain and report the general-relation check. - Lower standalone trace actions with fresh assignment analysis while reserving cached locals to prevent mixed-call-site name collisions. - Guard conditional action parameter domains as well as their bodies. - Check all enum transition occurrences, including nested and indirect calls, before selecting an arm; report incomplete coverage as general. - Isolate trace lowering and emit trace-only helpers in the trace module; byte-compare the complete base-model export against a pre-PR golden. - Share selected relations with TraceEnabled, using identity decoders for model-typed diagnostic parameters instead of decoding them as JSON. Add seven TLC regressions covering the six findings and set-valued parameters; compare diagnostic sets semantically rather than by print order.
- Include source-level calls through closure-returning helpers when proving complete enum-arm coverage; report incomplete selection as general. - Discover transitive action-builder occurrences in helper bodies and let their general relations override incomplete direct-call selections. - Snapshot trace lowering before named-expression exports, so those exports cannot suppress trace-only helper definitions or dependencies. - Keep post-dependent action inputs on the general-relation path, after Next assigns successor variables, instead of hoisting primed domains. Turn all four round-3 reproductions into regression tests, including positive/negative conformance, reported fallback, byte comparisons with named expressions, and enabled-step diagnostics for post-dependent inputs.
- Preserve guard-dependent input evaluation through reported general relations, avoiding premature singleton-domain and binder-equality evaluation. - Retain and union bounded action arguments across direct and transitive call sites when falling back; preserve guards on inherited quantified domains. - Turn both round-4 reproductions into regression tests, including omitted parameters, disjoint call-site domains, guarded bounds and negative logs.
- Fix computed inputs evaluated before action preconditions by selecting only literals, total pre-state projections, and original scoped binders. - Fix transitive domain evaluation outside caller guards with construction-time certification shared by selection, fallback unions and all trace consumers. - Keep unsafe bounds out of TraceEnabled and TraceDiagnosis; require explicit parameters without safe domains and fail closed for uncheckable helpers. - Add the round-5 reproductions and nine regression tests covering every row of the evaluation-order audit; document the conservative fallback policy.
kiranandcode
added a commit
that referenced
this pull request
Oct 8, 2026
Resolve tla.rs record-call conflict with FunctionUse::Call specialization and retain Action argument-domain collection under the resolved identity. Normalize types before bound_from_type_inner and safe_trace_domains insert. Keep the trace writer's mutable arm definitions, action types and general relation steps, resolving operator roots through FunctionUse::Root. Route main's remaining trace builder, wrapper, forward and dispatcher lookups through resolved handles; retain specialized forward identities. Clone the private resolver registry for isolated trace generation. Resolve all three tla_export.rs tail conflicts by retaining the merged shared prefix and both complete appended test blocks (234 tests). Retain main's module-order changes and trace-isolation fixtures. Validation: release build; full 234-test exporter suite with SANY/TLC; 35 byte-identical fixture artifacts including Raft against the #62/main exporter; vargo fmt (optional vstd formatting unavailable); cargo clippy --all-targets -- -D warnings.
This was referenced Oct 8, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Select the logged enum constructor or action-record branch before evaluating successors. Narrow logged parameters while retaining safe omitted-parameter domains, dispatcher guards, and TypeOK. Hand-written next_step, VerusSync next_by, and verus-tla action records are supported.
Selection and domain reuse now share one conservative eligibility boundary. Source operands must be literals or total pre-state projections; existing quantifier/constructor binders remain in their original scope. Type-generated domains and configured constants are also certified. Calls, indexing, casts, and arithmetic in inputs or bounds are not assumed safe because of a particular guard shape. Certification happens while lowering source expressions, not by inspecting emitted TLA text.
Every consumer uses that decision: fixed singleton domains and binder equalities, call-site unions, conditional paths, cached quantifiers, enum field templates and dispatcher selection, transitive fallback domains, parameter narrowing, TraceEnabled, and TraceDiagnosis. An ineligible occurrence makes the whole action name a reported general relation. Unsafe domains cannot reappear through general fallback or diagnostic enumeration, and incomplete unions are never silently retained.
General relations use certified call-site domains or safe finite type domains. Without either, parameters must be logged and the report marks the step non-enumerable. A helper with a computed bound that cannot be checked independently of caller guards is also reported as general and non-enumerable, excluded from TraceEnabled, and refused explicitly if logged; next remains available for state-only validation. These are deliberate conservative limits, replacing the previous evaluation-order special cases.
Coverage still includes transitive calls and closure-returning helpers. Trace-only definitions remain isolated from the base export and named-expression exports. Unknown names retain the advertised state-only fallback, with policy metadata consumed by the companion MCP preview change: https://github.com/BasisResearch/verus-tools-mcp/pull/68.
Validation:
Historical performance measurements (before the conservative eligibility restriction) recorded fresh-JVM timings of 5.508 s (raft-rs), 0.804 s (LRU), and 1.004 s (circular-buffer), versus 120 s baseline timeouts. The three logs contain 35,238 steps; raw data is under verus-research/trace-arm-eval/ on aws-dev. The original toyDB check passed 58 goldenscripts against its existing hand-written trace model; it was not rerun for these changes.