fix(tla): surface a reached Assert(FALSE) in an action as a safety violation

[zoratu]

Problem

A next-state action conjunct that errors during evaluation is treated as a disabled branch (no successor). That's correct for a benign guard-eval failure (e.g. a record access on a ModelValue when a sibling guard is false), but it also silently swallowed a reached Assert(FALSE) — so a spec whose Next action can reach a failing assertion was reported as passing instead of violated. TLC halts on such an assertion.

Why it's tricky

Model::next_states returns () — it has no error/violation channel — and the only violation channel (check_invariants) is state-level, not action-level. So the failure is surfaced via a per-thread side channel rather than a trait-signature change.

Change

• Detect narrowly: the Assert handlers (compiled + interpreted) record the failure only when the argument evaluated to Bool(false) and a committed next-state generation is in progress. A non-boolean argument (benign/ambiguous eval error) is not recorded.
• Committed-mode guard: next_states / next_states_labeled mark committed generation for the duration of the eval via an RAII CommittedNextStateGuard, so speculative evaluations (ENABLED, invariant/state-constraint checks, action probing) that hit an assertion do not record a spurious violation.
• Report cleanly: the worker clears the slot before generating successors and, right after, drains any recorded assertion and reports it exactly like an invariant violation (same trace reconstruction, channel, stop handling). next_states returns cleanly (no panic) when an assertion is pending, regardless of allow_deadlock.

Soundness rests on conjunction short-circuit (And stops at the first false conjunct; a false guard clause prunes the branch before later clauses evaluate), so a reached assertion means all preceding guards passed — exactly where TLC would evaluate and halt on it.

Approach chosen

Presented three options (side-channel / trait-signature change / defer); the side-channel was selected as best risk/reward — it reuses the existing violation machinery without a trait ripple across the runtime, POR, swarm, labeled variants, and every model.

Gate

• cargo test --release 1488 passed, 0 failed — adds tests/reached_assertion_violation.rs: a reached Assert(FALSE) is reported as a Safety violation; an Assert behind a never-satisfiable guard is not.
• scripts/diff_tlc.sh 23/23 with unchanged verdicts — adds assert_disabled (Assert behind an unsatisfiable guard: no violation, distinct count == TLC). No existing spec flips to a false violation.
• Verified via run-tla: AssertReached → violation=true ("assertion failed"); AssertDisabled → violation=false, 4 states.