Skip to content

hy-check(addr_loan): run second-pass loop-carried slot-loan checks on top-level for loops and reject &pa[0]["k"] pointer-to-array map borrows (Fixes #4039) - #4040

Open
Burapa-J wants to merge 2 commits into
limitlessprojects:mainfrom
Burapa-J:fix/addr-loan-top-loop-body-and-ptr-map-borrow
Open

Burapa-J wants to merge 2 commits into
limitlessprojects:mainfrom
Burapa-J:fix/addr-loan-top-loop-body-and-ptr-map-borrow

Conversation

@Burapa-J

@Burapa-J Burapa-J commented Nov 7, 2026

Copy link
Copy Markdown
Contributor

Fixes #4039

Cause

  1. check_stmt_addr_of_loan_projections (compiler/crates/hy-check/src/addr_loan.rs:329-331) gated the second pass self.walk_for_loop_carried(&mut carry_st, kind, body, true) behind if include_direct_ident, which is false for all top-level for loops outside closures. Nested Stmt::For inside walk_for_loop_carried also ran only a single pass when emit == true.
  2. is_map_element_or_value_projection and place_is_map_element_or_value_projection (addr_loan.rs:692-742) did not unwrap TypeShape::Pointer(Map | Array) on Expr::Index / PlaceKind::Index bases (&pa[0]["a"]).

Fix

  • Unconditionally run the second pass self.walk_for_loop_carried(&mut carry_st, kind, body, true) on Stmt::For in check_stmt_addr_of_loan_projections and seed nested Stmt::For loops before emitting in walk_for_loop_carried.
  • Add expr_borrow_shape and handle TypeShape::Pointer(Map | Array) in is_map_element_or_value_projection and place_is_map_element_or_value_projection.
  • Add regression tests in compiler/crates/hy-check/tests/addr_loan_place_rebind_and_loop_carry.rs.

Verification

  • cargo test -p hy-check --lib --test addr_loan_place_rebind_and_loop_carry --test addr_of_loan (201 passed, 0 failed)

Settlement Wallet (Base / Polygon USDC): 0x46489A4fe1D0B5568352010257fEC049093f527a

@github-actions github-actions Bot added the bot:stale-base Shepherd: behind main beyond threshold label Nov 8, 2026
@github-actions github-actions Bot added the bot:land-candidate Shepherd: fresh, gate-clean, verifiable (set from classify()) label Nov 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bot:land-candidate Shepherd: fresh, gate-clean, verifiable (set from classify()) bot:stale-base Shepherd: behind main beyond threshold

Projects

None yet

1 participant