Support dynamic/composite internal helper args (#1889)

[Th0rgal]

Summary

• Adds shared internal argument expansion helpers (Compiler/CompilationModel/InternalArgs.lean): internal helper definitions now receive expanded Yul slots for dynamic/composite params, and helper calls forward source-level dynamic/composite args by direct param/local reference with slot expansion.
• Updates IR-generation supported-fragment proofs for the new internal helper table threading and the Yul call-closure proof for internal calls; long proofs split to satisfy the 50-line limit.
• PrintAxioms.lean regenerated (zero new axioms, no sorry, no native_decide).

Closes #1889. Tier 1 dynamic ABI codec track (downstream: Morpho Midnight ECM removal). Stacked on #2006 (#1975 struct-array calldata).

Test plan

• lake build Verity Contracts Compiler PrintAxioms → "Build completed successfully."
• refresh_verification_artifacts.sh → [refresh] PASS
• make check → "All checks passed."
• scripts/check_proof_length.py passed
• CI green

---

Note

Medium Risk
Touches core compilation and validation for internal calls across the whole stmt/expr pipeline; mistakes could mis-lower ABI-shaped helper args or accept invalid forwards, but behavior is gated by stricter validation and extensive feature/proof updates.

Overview
Internal helper calls now treat dynamic and composite parameters (arrays, bytes, static tuples/fixed arrays, ADTs) like external ABI slots: callee Yul signatures expand to multiple slots, and callers must forward matching source-level args—direct Expr.param references for expanded types, or legacy flat expanded Yul arg lists with exact generated names / checked dynamic-member projections.

A new InternalArgs module centralizes internalFunctionYulParamNames, static binding names, and isExpandedInternalParamType; compileInternalCallArgs / compileExprWithInternals replace plain expression compilation wherever internal specs are in scope (statements, events, storage writes, dispatch). Validation drops raw Yul-arg-count checks in favor of validateInternalCallSourceArgs (type/layout match, forwarding rules, issue #1889 errors); constructor bodies pass caller params into internal-call shape validation.

compileValidatedCore threads the internal function list into external bodies, internal Yul defs, and constructors (each internal compiles with the full internal table). IR-generation proofs and feature tests are updated for the extra parameters and empty-internal supported fragment; compileExpr/compileExprList remain as wrappers with internalFunctions = [].

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

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jun 15, 2026 6:11am

[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 e11c39a. Configure here.}

[cursor]

ADT storage write skips internals

Medium Severity

compileAdtStorageWrite still lowers payload expressions with compileExprList, which uses an empty internal-function table. After this change, other setStorage paths use compileExprWithInternals with internalFunctions, so internal helper calls inside ADT constructor payloads can compile with incorrect argument expansion.

Additional Locations (1)

• Compiler/CompilationModel/Compile.lean#L151-L153

 

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