Support dynamic array element aliases

[Th0rgal]

Summary

• Track immutable local aliases for dynamic arrayElement <param> <index> bindings in the macro local context
• Lower alias field reads, abiHeadWord, dynamic-member arrayLength / arrayElement, and helper/external array arguments back to the original calldata array element
• Add FixedArrayStructSmoke coverage for alias head-word and dynamic member length lowering

Testing

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

---

Note

Medium Risk
Touches core macro translation/type-inference for expression lowering, so regressions could affect many contracts that project into dynamic calldata arrays or pass dynamic members to helpers/external calls.

Overview
Adds first-class tracking for immutable locals that alias arrayElement <param> <index> (new TypedLocal + LocalSource) so the macro can recognize when a local name is really a dynamic calldata array element.

Extends type inference and lowering to resolve struct field reads, abiHeadWord, dynamic-member arrayLength/arrayElement, tuple-destructuring guards, and helper/external-call dynamic arguments through these aliases, emitting the same Expr.arrayElementDynamicWord/Expr.arrayElementDynamicMember* forms as direct arrayElement usage.

Updates smoke/invariant tests (FixedArrayStructSmoke, selector/signature snapshots) to cover alias-based head-word reads and dynamic member length reads.

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

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

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

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

[cursor]

New function duplicates existing arrayElementDynamicTupleArg? exactly

Low Severity

arrayElementAliasSource? is character-for-character identical to the existing arrayElementDynamicTupleArg? — same signature, same logic, same return type. One of the two can be removed and the other reused at all three call sites.

Additional Locations (1)

• Verity/Macro/Translate.lean#L1880-L1898

 

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

[cursor]

Type checker accepts alias projections that translator cannot lower

Medium Severity

inferPureExprType now accepts localArrayElementDynamicMemberProjection? arguments for inline externalCall and tryExternalCall expressions, but the corresponding externalCall translation path in translatePureExprWithTypes has no matching handling — it falls through to the generic recursive call, which cannot translate a dynamic member projection as a standalone expression and will throw an "unsupported expression" error at translation time.

Additional Locations (1)

• Verity/Macro/Translate.lean#L2982-L2989

 

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