[pa-khan]

Fixes #4006

Summary

Fixes two P0 soundness holes in Expr::Move projection handling across walk.rs, freeze.rs, and sendability.rs (GUARANTEES.md Rows 1, 2, 6, and 7 — HYB-E3003, HYB-E3004, HYB-E3102, HYB-E3104):

1. Walk index and slice-bound subexpressions along rooted move projection chains (compiler/crates/hy-check/src/walk.rs):

   • Adds expr_move_chain_subexpr_uses and calls it from the Expr::Field | Expr::Index | Expr::Slice arm of Expr::Move in expr_uses when operand.root_ident() is Some(root).
   • Preserves the single via_move: true use on root while recording all identifier uses inside index, lo, and hi subexpressions along the projection chain so use-after-move (HYB-E3003), same-statement move/consume (HYB-E3003, A7/O13), A3 map-slot loan last_use windows (HYB-E3102), and T24 address-of-loan checks (HYB-E3104) cannot be bypassed.

2. Require a rooted binding (root_ident().is_some()) for the O5.4 own-handle field move allowance and freeze underlying reference roots (compiler/crates/hy-check/src/freeze.rs, compiler/crates/hy-check/src/sendability.rs):

   • Gates the Expr::Field + TypeShape::OwnHandle(_) exemption in mark_move_in_value, check_o54_non_ident_move, and check_send_or_spawn on op.root_ident().is_some().
   • When an invalid non-ident move has op.root_ident() == None (e.g. move (holder{doc: h.doc}).doc, move passthrough(&h).doc, move ([]holder{h}[0]).doc), emits HYB-E3004 and freezes underlying non-sendable reference roots collected via collect_ref_roots so subsequent uses also trigger HYB-E3003.

Verification

• Added hermetic integration tests in compiler/crates/hy-check/tests/move_projection_index_uses_and_unrooted_handle_field_soundness.rs covering:
  • HYB-E3003 for use-after-move inside move projection index and slice bounds at local define, task spawn, and ch <- send sites.
  • HYB-E3003 for same-statement move + read and same-statement consume (flate2.writer.finish) + use inside move projection index.
  • HYB-E3102 when a map is mutated before a final read of an A3 map-slot loan (slot := &m["a"]) inside move s.holders[slot.idx].doc, and HYB-E3104 when taking &slot inside a move projection index.
  • HYB-E3004 + HYB-E3003 when moving .doc out of unrooted struct literals, pointer-passthrough call results, and slice literals across task, chan, and local define sites.
  • Positive control verifying valid rooted own-handle field moves continue to pass with zero diagnostics.
• Ran full cargo test -p hy-check suite: all test binaries pass with 0 regressions.

Settlement Coordinates

• GitHub: @pa-khan
• USDC Wallet (Base / EVM): 0x45Ecf534fD00bb3179D34E6a3FDdE084cBfBc9Fb
• Solana Wallet (USDC / SOL): Eek8wHTmTCjQoVtKw4ZATQLiTqwURR2LBdfTmxmuD4D8