Guard partial TLA reads and model total collections with finite carriers

[kiranandcode]

Partial reads can stop TLC before a later source guard rejects an action. This change moves an unguarded read behind its source guard and inserts a reported IF DefinedRead THEN predicate ELSE FALSE restriction when needed. Total/infinite collections use explicit typed finite carriers, with warnings and reported holes. Guarded and total reads preserve the parent export.

The analysis carries branch and linear bounds, checks preserved state-length facts, and analyzes lazy LET values at their use sites. Action-disabling rules apply to Init/Next and their helpers. Narrowing casts contribute range requirements before recursive definedness checks, fixing AbstractMap's cast assertion.

Definedness declarations now precede mutual-recursion traversal, and retained guards emit their operator dependencies. This fixes PagedBetree/PivotBetree's forward reference to Defined_substitute and nrkernel guard-only core_mem_rec variants. Unused analysis probes do not introduce table holes. Arguments are checked once, repeated helper applications are memoized within their guard context, and captured environments are shared. An explicit work/depth budget retains source-located refusals for analysis exhaustion.

Anvil's sub_vrs_reconcile also exposed a partial Option read inside a value-returning match helper. Guarding its negated condition by forcing it FALSE selected the unsafe branch, while caller analysis skipped the match arms. Value-helper conditions now retain their meaning; the enclosing predicate guards the selected arm, its guard, and short-circuit operands. Guard locals preserve lexical scope and cannot capture later LET declarations.

The unchanged round-2 VRS harness improves from 1,138 generated / 2 distinct states followed by None.v0 failure to a complete search of 7,960 generated / 7 distinct states, with zero refusals and no evaluation error. It reports the expected source error branch as a not_error invariant violation (Init -> AfterListPods -> Error); this is not a claimed controller defect. All three Anvil exports were replayed on lane 3. Network/controller retain their existing 2/9 closure-related refusals; their generated modules pass SANY, but their saved harnesses cannot run successfully on this lane alone. Anvil evidence and current regression replay.

The incoming-parent merge preserves all 264 tests from both branches, the trace-arm selection/bookkeeping and module-order fixes, and the mandatory Functions::resolve specialization boundary. Definedness and guard dependency lookups now use resolved handles; the private registry is shared across analysis snapshots so guard-only instances remain available for emission. Workspace Rust formatting, workspace clippy, and clippy for the exporter test target pass with warnings denied. Portable golden files were regenerated from the incoming parent to retain its trace-arm changes. Merge evidence.

Validation after merging kg/export-nrkernel at 519e9295 (merge commit ca16f117, plain-pushed):

• 264 exporter tests pass, with TLA2TOOLS_JAR set; vstd verifies 2,045 functions. New regressions check Option helper projections and branch selection (including both Some and None), nested match guards and lexical LET scopes, mutual substitution through a map constructor, guard-only dependencies, and a 40-layer shared helper graph with 2^40 paths (export under 30 seconds, zero refusals, bounded output, SANY; TLC at eight layers).
• 35/35 generated files (TLA, configuration, and JSON reports) are byte-identical to the incoming parent for toyDB Raft and every examples/tla fixture, including mutex_liveness. Complete golden regressions and an independent raw re-export check both pass.
• All 12 campaign models export and pass SANY; 11/12 have zero refusals. All 16 saved TLC configuration/bound files remain byte-identical in that campaign replay.

Regression	Before at 64f1c6e3	After
PagedBetree	SANY: undefined Defined_substitute	TLC completes: 25 distinct / 173 generated
PivotBetree	Same SANY failure	TLC completes: 25 distinct / 133 generated
mmu_rl1	189 expansion refusals, 25.7 s	0 refusals, 8.9 s
mmu_rl2	Export timeout at 90 s	0 refusals, 8.6 s
mmu_rl3	Export timeout at 90 s	0 refusals, 8.6 s
os	Export timeout at 90 s	7 refusals, 11.6 s

Both trees recover the original campaign's 25 distinct states. OS's remaining refusals are choose and integer type bounds; none is a definedness-expansion refusal. The nrkernel models have no saved campaign MC command, so those results cover export/SANY only.

The original six machines still produce 6/6 zero-refusal exports and 4/6 usable bounded TLC runs (original campaign: 5/6 and 0/6). AbstractJournal completes at 72 states; AbstractMap completes at 3; CrashTolerantJournal explores until the 30-second cap; LinkedJournal reaches an invariant violation at 4. NR and CrashTolerantMap retain missing constant assignments in the unchanged campaign configurations. No source finding is claimed from these finite-model counterexamples.

Design, construct mappings, and full before/after report · Measurements and binary hashes · Replay helper