Support macro binds for array-return helpers

[Th0rgal]

Summary

• track macro locals that are memory-backed arrays returned by internal helpers
• lower let xs ← helperReturningArray ... to Stmt.internalCallAssign [xs_data_offset, xs_length] ...
• lower arrayLength xs, arrayElement xs i, and forwarding xs into Array helper params through memory-array offset/length locals
• add macro regressions for length reads, element reads, and forwarding returned arrays into another helper

Verification

• lake build Compiler.CompilationModelFeatureTest
• git diff --check

---

Note

Medium Risk
Touches macro translation and typing/lowering for internal helper calls returning arrays, which can affect generated IR/Yul for dynamic array handling and call argument passing. Scope is constrained to Array returns and covered by new regression tests.

Overview
Macros can now let xs ← helperReturningArray ... and treat xs as a memory-backed array local represented by xs_data_offset/xs_length locals, lowered via Stmt.internalCallAssign.

arrayLength xs, arrayElement xs i, and passing xs into other helper Array parameters are updated to lower through new Expr.memoryArrayLength/Expr.memoryArrayElement paths when xs comes from an internal helper array return (restricted to Array<wordLike>).

Adds CompilationModelFeatureTest regressions that assert the new lowering for length reads, element reads, and forwarding a returned array through another helper call.

^{Reviewed by Cursor Bugbot for commit 497b62b. Bugbot is set up for automated code reviews on this repo. Configure here.}

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 497b62b. Configure here.}

[cursor]

Inconsistent check ordering between type inference and translation

Low Severity

In the arrayLength handling, inferPureExprType checks localMemoryArray? before paramDynamicMemberProjection?, but translatePureExprWithTypes checks paramDynamicMemberProjection? before localMemoryArray?. If a name ever matched both predicates, type inference and code generation would disagree on which branch to take, producing mismatched semantics. The arrayElement case has consistent ordering in both functions, making this arrayLength discrepancy likely unintentional.

Additional Locations (1)

• Verity/Macro/Translate.lean#L2733-L2737

 

^{Reviewed by Cursor Bugbot for commit 497b62b. Configure here.}