fix(hy-check): track scope depth in pre_moved and LX14 loop jumps on back-edge (fixes #739)

[c-viper-work]

Closes #739

Summary

Fixes three soundness bypasses in Checker::check_loop_backedge (compiler/crates/hy-check/src/freeze.rs, compiler/crates/hy-check/src/lib.rs, and compiler/crates/hy-check/src/closures.rs) where loop-carried ownership moves (O5.1 / O5.2 / O13 / SPEC LX14) passed hyb check with 0 diagnostics and triggered real go run -race data races (exit code 66) at runtime:

1. Scope-depth identity for pre_moved and reported_backedge (lib.rs, closures.rs, freeze.rs):

   • Changes pre_moved and reported_backedge from HashSet<String> to HashSet<(usize, String)> using the FnState::lookup_depth convention (0 for st.env, i + 1 for st.scopes[i]).
   • Prevents a pre-loop move of an outer binding m (e.g. at depth 0) from masking a loop-carried move of a fresh shadowing binding m (at depth d + 1 <= outer_depth) inside an enclosing block (if, { ... }, outer loop, or closure), and prevents a back-edge diagnostic on one binding from suppressing diagnostics on a distinct shadowed binding of the same name.

2. SPEC LX14 continue loop reachability across nested finite for loops (freeze.rs):

   • Separates unlabeled_continue_reach and labeled_continue_reach in LoopFlow and updates stmt_has_continue_for_loop, stmt_can_reach_backedge, and stmt_move_can_reach_backedge.
   • Recognizes that continue loop (Stmt::Continue { label: Some(_) }) skips enclosing finite for loops (ForKind::Range, ForKind::Iterate, ForKind::While) and jumps to the nearest enclosing loop (ForKind::Infinite), while leaving a finite for when that finite for itself is the loop under check.

3. SPEC LX14 break loop reachability across nested finite for loops and select (freeze.rs):

   • Separates unlabeled_break_reach and labeled_break_reach in LoopFlow so break loop (Stmt::Break { label: Some(_) }) inside a nested finite for or select binds to the nearest enclosing loop (ForKind::Infinite), accurately modeling exits from an inner loop to a path that reaches the outer loop back-edge.
   • Filters per-binding moves by move_span_can_reach_backedge when trailing_exit holds so a move on an exiting path before a trailing break/return does not falsely appear loop-carried alongside an earlier move that reached continue.

---

Verification

• Added comprehensive positive (Verdict::Reject with HYB-E3003) and negative (Verdict::Accept) unit tests in compiler/crates/hy-check/src/freeze.rs covering both top-level function and closure-boundary paths.
• Empirically verified all 3 minimal reproducers from hy-check: check_loop_backedge misses loop-carried moves on shadowed pre_moved bindings and LX14 continue loop / break loop inside nested finite for loops (go run -race) #739 with ./compiler/target/debug/hyb check (HYB-E3003 emitted).
• Full test suite passing:
  • cargo test --manifest-path compiler/Cargo.toml -p hy-check (1,146 passed, 0 failed)
  • cargo test --manifest-path compiler/Cargo.toml --workspace (1,544 passed, 0 failed)

---

Payout Wallet

• USDC / ETH (Base / Ethereum): 0x3018577736ebcdd3ddca916Bef44e7dC6E27e33E