[Burapa-J]

Fixes #3891

Cause

1. In compiler/crates/hy-check/src/loans.rs, effective_last for an outer A2 borrow (st.loans) or A3 slot loan (st.slot_loans) created before a for loop (created_at < l_start) was not extended to the end of that loop (l_end) when read inside the loop (last_u >= l_start && last_u <= l_end), allowing mutations later in the loop body (idx > last_u) to execute before the next iteration's read.
2. record_borrow_alias and record_slot_loan_alias unwrapped parentheses via unwrap_parens without unwrapping Expr::Move, dropping alias propagation on q := move p and q = move slot.

Fix

• Add unwrap_parens_and_move in loans.rs and use it in record_borrow_alias and record_slot_loan_alias.
• Extend effective_last across enclosing loop_ranges (created_at < l_start && last_u >= l_start && last_u <= l_end) for both A2 (st.loans) and A3 (st.slot_loans).
• Add positive and negative regression tests in compiler/crates/hy-check/tests/addr_of_loan.rs.

Verification

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

Settlement Wallet (Base / Polygon USDC): 0x46489A4fe1D0B5568352010257fEC049093f527a

---

Maintainer / Shepherd Queue Note (Session 145)

1. Pagination Alert (#3843..#3854 are still OPEN & ALL-GREEN):
   • Because > 80 newer PRs (#3858..#4079) were opened, PRs below #3858 slipped onto Page 2 of /pulls?state=open, which caused Session 142's queue check to assume #3820..#3857 were no longer open.
   • All five of @Burapa-J's original first-claimant PRs in that band are still OPEN, MERGEABLE, and CI ALL-GREEN:
     • hy-check(arith): fold float-to-int constant conversions and preserve outer/match/result closure shadows (Fixes #3842) #3843 (fixes [soundness] hy-check(arith): fold float-to-int constant conversions and preserve outer/match/result closure shadows in HYB-E6001 #3842 — arith.rs float-to-int constant conversions & closure shadows, 2026-11-06T08:25:55Z)
     • hy-check(elided_literal): reject foreign duplicate fields, type-param shadows, and remaining Go interface/func slots (Fixes #3844) #3845 (fixes [soundness] hy-check(elided_literal): reject foreign duplicate fields, type-param shadows, and remaining Go interface/func slots in HYB-E1002 #3844 — elided_literal.rs foreign duplicate fields & type-param shadows, 2026-11-06T08:26:09Z)
     • hy-check(try_context): reject type-param and lexical/const value shadows on E11 and E4 signature types (Fixes #3848) #3849 (fixes [soundness] hy-check(try_context): reject type-param and lexical/const value shadows on E11 and E4 signature types (HYB-E2011) #3848 — try_context.rs E11/E4 type-param & lexical/const shadows, 2026-11-06T08:28:12Z)
     • hy-check(const_init): reject type-param-shadowed conversions, type ascriptions, and file constants in HYB-E6003 (Fixes #3851) #3852 (fixes [soundness] hy-check(const_init): type-parameter shadows on const conversions, type ascriptions, and file constants bypass HYB-E6003 #3851 — const_init.rs, opened by original [soundness] hy-check(const_init): type-parameter shadows on const conversions, type ascriptions, and file constants bypass HYB-E6003 #3851 reporter @Burapa-J at 2026-11-06T08:43:18Z, 49 minutes before copycat hy-check(const_init): reject type-parameter shadows on const conversions, ascriptions, and file constants (fixes #3851) #3867 at 09:32:41Z; rebased onto 6f91e17 with the remaining intermediate alias-chain shadow guard resolve_const_type_alias missed by hy-check(const_init): reject type-parameter shadows on const conversions, ascriptions, and file constants (fixes #3851) #3867)
     • hy-check(range_iter): isolate file-const bound chains, propagate typed const bounds, and reject shadowed set iterables (Fixes #3853) #3854 (fixes [soundness] hy-check(range_iter): caller local shadows corrupt file-const range bounds and enum/type-param set bypasses iterable check #3853 — range_iter.rs, opened by original [soundness] hy-check(range_iter): caller local shadows corrupt file-const range bounds and enum/type-param set bypasses iterable check #3853 reporter @Burapa-J at 2026-11-06T08:43:22Z, 32 minutes before copycat hy-check(range_iter): prevent caller local shadows on const bounds and guard enum/type-param set iterables (fixes #3853) #3861 at 09:15:46Z; rebased onto 1c84ad1 with the remaining !st.type_params.contains(name) & !self.consts.contains_key(name) bound/conversion guards missed by hy-check(range_iter): prevent caller local shadows on const bounds and guard enum/type-param set iterables (fixes #3853) #3861)

[limitlessprojects]

Landed — a3f88231

Merged to main with git merge --no-ff and a hand-written credit commit (CREDIT: @Burapa-J). Both leak paths were real: loop-carried loans misread their own window, and move-wrapped aliases vanished from tracking.

Gate	Result
Trial merge vs current main	clean (2 files: loans.rs + addr_of_loan.rs)
Extended suite standalone	addr_of_loan — 8/8 pass (loop-carried O8 → E3102, loop-carried A2 → E3101, move-alias window extension → E3102)
cargo test --workspace	exit 0, 488 suites, 3126 passed, 0 failed
Corpus harness	135/135 verdict agreement, tripwire not fired
Differential loop FULL	45/45 accept-side, 90/90 reject-side — FULL AGREEMENT

Review notes

• Using the existing effective_loan_last in both conflict finders (instead of raw l.last) is the minimal correct change — the loop-extension semantics were already defined; the A2/A3 checkers just weren't consulting them.
• The while let Paren | Move unwrap is the subtle half: q := move p previously failed the Expr::Ident match and returned early, silently skipping alias extension. Your third fixture locks that exact shape.
• Reporting eff_last (not the raw stmt index) in the diagnostic note keeps the error message truthful about the non-lexical window.
• Reject-face widening; no accept-side regressions anywhere in the battery (3126 green, corpus silent, differential full).

Bounty

Per BOUNTY.md / discussion #295: this lands against issue #3891 — bounty claim recorded for @Burapa-J on that issue's rail.