fix(tla): compiled LET action clause stages helper-hidden primes - #192
Merged
Conversation
…piledLetWithPrimes)
`compile_action_clause_text` routed a `LET ... IN <body>` action clause
through `compile_let_with_primes` (which compiles the body conjuncts as
action clauses, so each can stage a prime) only when the LET text
contained a literal `'`. That missed a prime hidden behind a helper call:
LET M == ... IN SendMessage(m) \* no literal ' in the LET text
SendMessage(m) == messages' = ... \* prime is in the helper
Without a visible `'` the clause fell through to a boolean `Guard`, which
evaluates the helper in value context and discards its primed assignment,
so the action produced 0 successors. This is exactly Paxos /
SimplifiedFastPaxos `PaxosAccept`, previously worked around in #175 via an
interpreted fallback on the empty compiled result.
Drop the `&& trimmed.contains('\'')` condition so every `LET` action
clause routes through `compile_let_with_primes`. Shapes it can't compile
(e.g. a `CASE`-of-actions body) still return None and fall to the
interpreted `LetWithPrimes` path, and a pure value LET compiles its body
to boolean `Guard` clauses as before — so the change only ADDS correct
prime staging, never removes a working path.
The #175 interpreted fallback (empty-compiled-result -> interpreted) is
retained as harmless defense-in-depth; it is now dead for the LET case
(the compiled path is correct on its own, verified in isolation).
Gate: diff_tlc 21/21 (adds `let_hidden_prime` regression spec: a
helper-hidden-prime LET == TLC=4); Paxos/SimplifiedFastPaxos still 1,207
distinct == TLC; cargo test 0-fail (modulo the known load-timing-flaky
`prop_pause_visibility` checkpoint proptest, which passes 5/5 in
isolation and is unrelated to TLA+ eval).
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.
Problem
compile_action_clause_textrouted aLET ... IN <body>action clause throughcompile_let_with_primes(which compiles the body conjuncts as action clauses so each can stage a prime) only when the LET text contained a literal'. That missed a prime hidden behind a helper call:Without a visible
'the clause fell through to a booleanGuard, which evaluates the helper in value context and discards its primed assignment → the action produced 0 successors. This is exactly Paxos / SimplifiedFastPaxosPaxosAccept, previously worked around in #175 via an interpreted fallback on the empty compiled result.Fix
Drop the
&& trimmed.contains('\'')condition so everyLETaction clause routes throughcompile_let_with_primes. Shapes it can't compile (e.g. aCASE-of-actions body) still returnNoneand fall to the interpretedLetWithPrimespath; a pure value LET compiles its body to booleanGuardclauses as before. The change only adds correct prime staging — it never removes a working path.The #175 interpreted fallback is retained as harmless defense-in-depth but is now dead for the LET case (the compiled path is correct on its own, verified with the fallback neutered).
Gate
scripts/diff_tlc.sh21/21 — addslet_hidden_primeregression spec (helper-hidden-prime LET == TLC=4)cargo test --release0-fail, modulo the known load-timing-flakyprop_pause_visibilitycheckpoint proptest (passes 5/5 in isolation; unrelated to TLA+ eval)