Support macro allocation of memory arrays

[Th0rgal]

Summary

• add macro support for allocArray memory-backed uint256[] locals
• add setMemoryArrayElement lowering for memory array writes
• allow returnArray to return compiler-tracked memory array locals
• cover allocation, writes, and return shape with native-decide regressions

Verification

• git diff --check
• lake build Compiler.CompilationModelFeatureTest
• python3 scripts/generate_print_axioms.py --check
• python3 scripts/check_axioms.py

---

Note

Medium Risk
Updates macro translation and compilation-model validation to recognize/emit memory-backed uint256[] locals, which can affect generated Yul memory layout and return behavior. While scoped to arrays and guarded by new checks/tests, mistakes could cause incorrect codegen or runtime memory corruption.

Overview
Enables macros to create and use memory-backed uint256[] locals via allocArray, including lowering to Yul-style memory allocation (updating free memory pointer) and introducing setMemoryArrayElement to write elements.

Extends identifier/return-shape validation so returnArray can return these memory-array locals (not just parameters), with stricter scope/type checks, and adds feature tests that assert the allocation, write, and Stmt.returnArray shapes in the generated compilation model.

^{Reviewed by Cursor Bugbot for commit 7871621. 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 7871621. Configure here.}

[cursor]

Semantic model for setMemoryArrayElement discards writes silently

Low Severity

The setMemoryArrayElement contract-level semantic model is a complete no-op that discards all arguments and returns pure (). Combined with allocArray producing Array.replicate len 0, any function using the allocArray/setMemoryArrayElement/returnArray pattern (like compactAmounts) will have a Lean-level specification that returns an all-zeros array instead of the intended result. While other low-level ops like calldatacopy follow a similar stub pattern, setMemoryArrayElement is a new user-facing abstraction where the specification mismatch could mislead proof attempts.

Additional Locations (1)

• Contracts/Common.lean#L219-L221

 

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