fix(tla): keep CONSTANTS out of the fingerprinted state

[zoratu]

Problem

In TLA+/TLC a state is a valuation of the declared VARIABLES only; CONSTANTS belong to the fixed model context. We were seeding every config constant into each initial state (so Init predicates could read them), and since the active state schema is derived from the first init state's keys, those constants ended up in the schema — compiling every constant reference to a per-state StateVar { slot } and carrying the constant in every fingerprinted state.

This never changed distinct-state counts (constants are identical across all states) but bloated every fingerprint (bincode-serialized + hashed per state) and every stored state, and conflated the constant context with mutable state.

Two prior attempts to strip constants were reverted because they removed the data from the state but left the schema/compilation still pointing at constant slots. This fixes it at the root and in lockstep.

Change

• A (TlaModel::from_files): after the initial states are materialized and before set_active_schema, retain only module.variables in each state. One central filter covers the brute-force, joint-symbolic (T5.5) and streaming Init paths. The active schema is then variable-only, so constant references compile to name-based Var (resolved via injected definitions / the ModelValue fallback) instead of StateVar { slot }.
• C (inject_constants_into_module_tree): do not inject the self-referential def for a model-value constant whose name equals its value (NULL = NULL → NULL == NULL), which would recurse to MAX_DEPTH once the state binding is gone; the ModelValue(name) identifier fallback resolves it. An aliased model value (NoBlock = NoBlockVal, name ≠ value) still injects its non-self-referential def — otherwise NoBlock would wrongly fall back to ModelValue("NoBlock").

Successors inherit the change for free (they clone the current state and only overwrite staged variables). Symmetry is count-neutral: the held-fixed constant self-bindings were identical across all permutation candidates, so removing them cannot change which permutation wins — fixed_keys now simply never matches a state key (comments updated). Probe tests updated to probe the model's injected module (matching production analyze-tla) rather than relying on constants-in-state.

Design review

Design and plan were reviewed independently (codex, read-only) and cross-checked against the source before implementation — root cause, model-value self-ref loop, successor propagation, operator-ref constants, TransitionContext, and symmetry count-neutrality all confirmed; conclusion was A+C is minimal-complete (no separate constant-env context field required). The gate then caught a real bug in the first (too-broad) Impl C, which is why it's narrowed to the self-referential case only.

Gate

• scripts/diff_tlc.sh 22/22 with byte-identical distinct counts — adds const_state_omit regression (scalar-constant guard + model value in Init and an invariant, == TLC)
• Paxos / SimplifiedFastPaxos still 1,207 distinct == TLC (symmetry intact)
• cargo test --release 1486 passed, 0 failed
• Verified via --dump that constants no longer appear as state entries