Support dynamic/composite internal helper args (#1889)#2016
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
…lper-args # Conflicts: # PrintAxioms.lean
…nd ADT storage writes (#1889)
There was a problem hiding this comment.
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 70d116e. Configure here.
| if isDynamicParamType ty then [s!"{name}_data_offset"] else staticParamBindingNames name ty | ||
| | ty@(ParamType.tuple _) => | ||
| if isDynamicParamType ty then [s!"{name}_data_offset"] else staticParamBindingNames name ty | ||
| | ParamType.newtypeOf _ baseTy => internalCallYulArgNamesForBase name baseTy |
There was a problem hiding this comment.
Arg name mismatch for newtypeOf wrapping dynamic types
High Severity
internalCallYulArgNamesForBase handles newtypeOf _ baseTy by recursing into baseTy, but internalFunctionYulParamNames checks isDynamicParamType param.ty at the newtypeOf level and returns only ["{name}_data_offset"] for dynamic base types. For newtypeOf _ bytes (or string/array), the callee definition gets 1 Yul parameter via internalFunctionYulParamNames, but the caller generates 2 Yul arguments via internalCallYulArgNamesForBase (which recurses to bytes → [data_offset, length]). This arity mismatch would cause a Yul compilation error for any internal call forwarding a newtypeOf-wrapped dynamic type.
Additional Locations (1)
Reviewed by Cursor Bugbot for commit 70d116e. Configure here.
|
|
||
| def directForwardedInternalCallArgName? : Expr → Option String | ||
| | Expr.param name => some name | ||
| | _ => none |
There was a problem hiding this comment.
Duplicated helper function across two files
Low Severity
directForwardedInternalCallArgName? in ExpressionCompile.lean and directForwardedInternalArgName? in ValidationCalls.lean are identical functions both newly added in this PR. Both match Expr.param name to some name and everything else to none. One shared definition (e.g., in InternalArgs.lean) would avoid the duplication risk of future divergence.
Additional Locations (1)
Reviewed by Cursor Bugbot for commit 70d116e. Configure here.
| \n### CI Failure Hints\n\nFailed jobs: `compiler-regressions`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
1 participant
Summary
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.PrintAxioms.leanregenerated (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] PASSmake check→ "All checks passed."scripts/check_proof_length.pypassedNote
Medium Risk
Changes sit on the core statement/expression lowering path and alter generated Yul for internal calls with dynamic ABI shapes; mistakes would miscompile contracts rather than fail at compile time, though validation and regression tests narrow the surface.
Overview
Internal helper argument lowering is reworked so calls with arrays, bytes, static tuples, and ADTs match the callee’s expanded Yul signature instead of passing a single scalar per source argument.
A new
InternalArgsmodule centralizes Yul parameter naming (internalFunctionYulParamNames, forwarding slot names) and moves related helpers out ofDispatch/ScopeValidation. Compilation now threads aninternalFunctionstable throughcompileStmtList,compileExprWithInternals, constructor/fallback/receive paths, ADT storage writes, and event emission socompileInternalCallArgscan resolve the callee and expand args (directExpr.paramforwarding for expanded types, plus a legacy expanded-arg list path with checked dynamic-member projections).Validation replaces raw Yul arg-count checks with
validateInternalCallSourceArgs: logical arity, exact type/layout match for forwarded params, and constructor bodies now validate internal calls with caller params. Feature tests and Yul smoke specs cover fallback, ADT ctor payloads, and compositepermit+bytesshapes.Proof modules are updated for the new compile signatures and empty internal-fn tables on supported fragments.
Reviewed by Cursor Bugbot for commit 70d116e. Bugbot is set up for automated code reviews on this repo. Configure here.