Support internal array return registers

[Th0rgal]

Summary

• expand logical internal array returns to offset/length Yul return registers
• compile internal returnArray as offset/length assignments plus leave
• add memory-backed dynamic array accessors for returned (data_offset, length) bindings
• add CompilationModel regressions for internal address[] helper returns and memory-backed reads

Verification

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

---

Note

Medium Risk
Changes internal function return lowering and validation to treat array returns as two Yul values (offset/length), which can affect codegen and call-shape checking across the compiler pipeline.

Overview
Internal Stmt.returnArray is now supported by lowering dynamic array returns to two internal return registers (offset + length) and leave, instead of ABI-encoding and return.

The internal dispatch/validation pipeline is updated to account for array returns expanding to two Yul values: freshInternalRetNames generates extra return registers, and ValidationCalls enforces Yul-level arity for Expr.internalCall/Stmt.internalCallAssign.

Adds Expr.memoryArrayLength/Expr.memoryArrayElement for reading memory-backed array bindings (e.g. from internal helper returns) and threads these constructors through scope validation, purity/usage analyses, trust-surface checks, and proof scaffolding. Includes new feature tests asserting internal address[] round-trips and callers read via the memory array helper.

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

[cursor]

Validation allows Stmt.return for array-returning internal functions

Medium Severity

After this PR, freshInternalRetNames generates two Yul return registers for array return types, but validateReturnShapesInStmt still accepts Stmt.return for internal functions with any single return type (matching [_]), including ParamType.array _. The compileStmt path for Stmt.return only assigns the first register via retName :: _, leaving the second (length) register at Yul's default of 0. This produces silently incorrect code where the array length is always zero.

Additional Locations (2)

• Compiler/CompilationModel/Compile.lean#L212-L218
• Compiler/CompilationModel/Dispatch.lean#L20-L25

 

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

[cursor]

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

There are 2 total unresolved issues (including 1 from previous review).

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

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

[cursor]

Validation/compilation mismatch for internal array returnValues

Low Severity

Stmt.returnValues validation checks values.length against the logical return count (expectedReturns.length), but the compilation path checks it against internalRetNames.length (the Yul-level count, which is 2 for array returns). For an internal function returning a single array type, validation passes with one value expression, but compilation throws an arity mismatch because internalRetNames has two entries after the array expansion introduced by freshInternalRetNames.

Additional Locations (1)

• Compiler/CompilationModel/Compile.lean#L293-L301

 

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