pure: harden simplify_let_branching against hoisting branch-local variables

[karthikbhargavan]

Summary

simplify_let_branching rewrites let (x, y, ...) = switch ... in next by hoisting outputs that are identical in every branch into let-bindings after the switch. The candidate outputs (the raw endpoint tuple args) were never filtered against bound_fvars, the set of variables bound inside the bound expression; the existing is_bound_before_fvar guard was only applied to switch scrutinees.

Degenerate single-ok-endpoint case: fail/break/continue endpoints contribute no candidates, so a switch with exactly one ok endpoint gets that endpoint's raw args verbatim (the branch-wise intersection degenerates to a single set). If such an arg mentions a branch-local binder (match binder or intermediate let), the hoist emits a let-binding outside the switch referencing an out-of-scope variable — an unbound fvar, i.e. a crash in a later pass or invalid extracted code.

The defect is latent today: SymbolicToPure only creates a join-let when >= 2 branches reach the join point, and with >= 2 ok endpoints the intersection cannot contain branch-local fvars (their ids differ per branch). But nothing enforced that invariant; any future producer of a single-ok-endpoint switch-in-let would silently activate the bug.

Fix: in push_to_outs, drop any candidate whose free variables intersect bound_fvars (FVarId.Set.disjoint (texpr_get_fvars e) bound_fvars). This only disables the optimization in the unsound case and mirrors how is_bound_before_fvar already guards scrutinees.

Fixes #23

Validation

• dune build and dune build @fmt pass (charon pinned at cb50ff16, v0.1.223).
• Regression battery: all 89 llbc test fixtures (regenerated from the same sources with the pinned charon v0.1.223, since the pre-existing fixture dumps were emitted by charon v0.1.196 and are unreadable by any dev-based binary) translated with -backend lean by both the patched build and an unpatched origin/dev build: identical exit statuses (88 ok; raw_pointers fails identically in both, pre-existing and unrelated) and byte-identical generated Lean across the whole battery.
• Hoisting-still-works check: probe_pass_fires.rs (two live if arms sharing the constant 5 for one output slot) still gets the hoist with the patched build — let y1 ← if c then y + 1#u32 else y + 2#u32; let x1 ← 5#u32 + 10#u32; ... — identical to the unpatched output. probe_fail_endpoint_in_switch_let.rs (switch-in-let with a fail panic endpoint) also translates identically.

🤖 Generated with Claude Code