Proof follow-up: dynamic/composite internal-helper argument lowering

[Th0rgal]

Summary

Verity currently supports dynamic calldata at external entrypoints, but intentionally rejects dynamic parameters on internal helpers. This blocks clean translation of Solidity helpers whose signatures include bytes calldata or other ABI-dynamic values, such as Unlink's _transferWithBalanceCheck(PermitTransferFrom, address, bytes, uint256, bytes32) shape.

The current fail-fast guard is correct as a stopgap, but the feature we need is a first-class internal helper ABI/lowering convention for dynamic and composite parameters.

Current behavior

CompilationModel rejects any internal function whose parameter type is dynamic:

• Compiler/CompilationModel/ValidationCalls.lean: firstInternalDynamicParam
• Compiler/CompilationModel/Dispatch.lean: validateCompileInputsBeforeFieldWriteConflict throws Issue #753 (internal dynamic params unsupported)

The reason is that compileInternalFunction currently emits a Yul helper using only the source parameter names:

let paramNames := spec.params.map (·.name)
...
pure (YulStmt.funcDef (internalFunctionYulName spec.name) paramNames retNames bodyStmts)

External entrypoint ABI decoding is richer. For bytes / string / dynamic arrays it binds companion names such as:

• <name>_offset
• <name>_length
• <name>_data_offset

Static tuples/fixed arrays are also flattened into leaf bindings such as <name>_0, <name>_1, etc. That logic lives in Compiler/CompilationModel/ParamLoading.lean via genParamLoadsFrom, genDynamicParamLoads, and genStaticTypeLoads.

If the guard were simply removed, helper bodies that read signature_length, signature_data_offset, tuple leaves, etc. would reference bindings that were never passed into the Yul helper. This is the invalid-Yul failure that #753 originally reported.

Concrete Unlink impact

The Solidity helper _transferWithBalanceCheck wants to be translated as an internal Verity helper because it is semantically a reusable internal routine. Its natural shape includes:

• PermitTransferFrom (static composite / tuple-like value)
• address depositor
• bytes calldata signature
• uint256 amount
• bytes32 noteCommitment

Today the bytes calldata signature parameter trips the internal dynamic-param rejection. PermitTransferFrom also needs an explicit composite convention rather than pretending one Yul word contains the whole struct.

The practical result for Unlink translation is that this helper must remain inlined in each caller. That works around the compiler limitation, but it loses the source structure we want from Solidity-to-Verity translation:

• less faithful translation of internal Solidity helper boundaries;
• duplicated lowered statements at call sites;
• harder source review because the translated Verity no longer mirrors the Solidity helper decomposition;
• less reusable proof structure, since the helper cannot get a single summary/postcondition consumed by multiple callers;
• avoidable churn in the translator whenever a helper has a bytes calldata or tuple-like parameter.

A clean implementation would let the translator preserve _transferWithBalanceCheck as an internal FunctionSpec.isInternal := true helper and lower calls like _transferWithBalanceCheck(_permit, _depositor, _signature, _amount, _noteCommitment) by expanding the ABI-shaped arguments at the call boundary.

Proposed lowering model

Add an explicit internal-call ABI lowering layer shared by internal helper definitions and call sites.

1. Define lowered internal parameter slots

Introduce a helper such as:

def internalParamBindings : Param -> List String

with rules matching the existing external-entrypoint binding vocabulary:

• scalar static types (uint256, int256, uint8, address, bool, bytes32) lower to [name];
• bytes / string lower to [name_offset, name_length, name_data_offset] or, if the offset word is not useful after forwarding, a documented smaller convention such as [name_length, name_data_offset];
• dynamic arrays lower to their offset/length/data-offset bindings consistently with Expr.arrayLength, Expr.arrayElement, returnArray, event/custom-error ABI encoding, etc.;
• static tuples and fixed arrays lower recursively to leaf names (permit_0, permit_1, ...), matching genStaticTypeLoads naming;
• dynamic composites should initially be rejected unless/until their full recursive head/tail convention is implemented.

The important invariant is: any name that expression/statement lowering can emit for a source parameter must either be locally bound in an external entrypoint or appear in the internal helper's expanded Yul parameter list.

2. Use expanded params in compileInternalFunction

Change compileInternalFunction from spec.params.map (·.name) to the expanded internal parameter bindings.

inScopeNames should also include those expanded names so generated temporaries avoid collisions. Source-level parameter names may still be tracked for validation, but the generated Yul function signature must carry the names actually used by the compiled helper body.

3. Expand internal call arguments using the callee signature

Stmt.internalCall, Stmt.internalCallAssign, and Expr.internalCall currently call compileExprList positionally and emit one Yul argument per source argument. They need access to the callee FunctionSpec so a single source argument can expand into multiple Yul arguments according to the callee parameter type.

For the first implementation, keep this conservative:

• allow expanded arguments only for direct forwarding from existing bindings, e.g. Expr.param "signature" or Expr.localVar "signature" when the corresponding expanded companion names are known in scope;
• reject computed expressions for dynamic/composite parameters with a clear diagnostic, because materializing arbitrary dynamic ABI values into memory/calldata-shaped fat pointers is a separate feature;
• require argument type compatibility, not just arity. Today validation checks only source argument count vs callee parameter count.

For example, forwarding Expr.param "signature" to a callee bytes parameter should emit:

signature_offset, signature_length, signature_data_offset

Forwarding a static PermitTransferFrom tuple should emit the flattened leaf bindings expected by the helper, e.g. permitted token, permitted amount, nonce, deadline. Exact names should follow the existing tuple/fixedArray binding convention in ParamLoading.lean.

4. Share naming/layout code with external ABI loading

Avoid inventing a second naming scheme. Either expose and reuse the existing static/dynamic binding-name logic from ParamLoading.lean, or factor it into a small ABI binding-layout module that both entrypoint decoding and internal helper lowering consume.

This keeps source translation, Yul codegen, event/custom-error encoding, and future proof statements aligned around one convention.

Translator impact for Unlink

Once this exists, the Unlink translator can preserve Solidity helper boundaries instead of selectively inlining helpers that contain bytes calldata or static structs.

Translator-side requirements should be small:

• lower Solidity structs used as internal arguments to ParamType.tuple or an equivalent Verity composite representation with stable field ordering;
• emit direct parameter/local forwarding for calldata bytes values rather than attempting to copy bytes into memory;
• reject or inline only the cases that still require materializing a new dynamic value;
• add a regression fixture covering _transferWithBalanceCheck(PermitTransferFrom, address, bytes, uint256, bytes32) so this helper remains non-inline after translation.

This should also reduce duplicated Unlink proof obligations: one helper summary/postcondition can be attached to _transferWithBalanceCheck and reused at every direct call site.

Proof-side work

This is not just a codegen change. The proof stack currently has multiple places that assume or characterize the old one-source-param-to-one-Yul-param shape.

Expected proof updates:

• Generalize compileInternalFunction_output_shape in Compiler/Proofs/IRGeneration/IRInterpreter.lean. It currently states that successful helper compilation emits params spec.params.map (·.name). It should instead state params equal the expanded internal binding list.
• Update findInternalFunction?_exact_of_compileInternalFunction_mem_unique and related helper-table lemmas to carry the expanded parameter list.
• Generalize compileStmt_internalCall_shape and compileStmt_internalCallAssign_shape. They currently characterize call lowering as one compiled Yul arg per source arg via compileExprList. They need a callee-aware expanded-argument compiler and a corresponding shape theorem.
• Update the helper-aware IR execution lemmas (execIRStmtsWithInternals_of_internalCall_compile, execIRStmtsWithInternals_of_internalCallAssign_compile) so argVals correspond to the expanded ABI binding values, not source-argument count.
• Extend source-side helper-summary interfaces so a helper summary is parameterized over source params while the compiled-side helper receives expanded Yul params. The bridge needs a relation saying the expanded Yul argument vector represents the source argument values/fat pointers used by the source helper semantics.
• Preserve the existing helper-free conservative-extension theorems. The new work should affect only contracts with internal helper calls that use expanded params; the current helper-free/legacy-compatible path should remain a specialization.
• Add a SupportedSpec/body-surface widening step once the exact helper-call proof interface supports expanded dynamic/composite arguments. Until then, the compiler may support the feature operationally while the generic proof-complete fragment still gates it explicitly.

A useful proof decomposition would be:

1. prove deterministic binding-layout lemmas for internalParamBindings;
2. prove external entrypoint decoding and internal forwarding produce the same binding environment for directly forwarded values;
3. prove helper execution under expanded params simulates source helper execution under source params;
4. consume that simulation in the existing direct-helper-call / direct-helper-assign proof seams documented in the Layer 2 roadmap.

Acceptance criteria

• The internal dynamic-param rejection is replaced with a narrower diagnostic: reject only unsupported dynamic/composite cases that cannot be represented by the new internal binding layout.
• Internal helpers with direct-forwarded bytes / string / dynamic-array calldata params compile to valid Yul.
• Internal helpers with static tuple/fixed-array params compile with flattened leaf Yul params.
• Internal call validation checks type/layout compatibility, not just source arity.
• Regression tests cover a helper with both static composite and bytes params, including a shape matching Unlink's _transferWithBalanceCheck.
• Proof shape lemmas are updated to mention expanded helper params and expanded call args.
• The current supported/proof-complete fragment either proves the new cases or continues to fail closed with an explicit, issue-linked boundary until those proofs land.

Related context

• [Bug] Internal dynamic params are accepted but lower to invalid Yul (undeclared arr/arr_length) #753 fixed the old invalid-Yul bug by adding a fail-fast guard.
• This issue tracks replacing that guard with a real internal helper ABI convention.
• This directly unblocks faithful Unlink helper translation without inlining _transferWithBalanceCheck solely because it contains bytes calldata.

[Th0rgal]

Triage update against current lfglabs/main:

This issue is still valid, but the remaining scope is narrower than the original description. Internal helpers with dynamic-array parameters have since landed (#1858), so this should focus on the cases that still need a uniform internal ABI argument-lowering layer:

• bytes / string helper parameters, lowered as explicit fat-pointer args such as <name>_offset, <name>_length, <name>_data_offset or the canonical equivalent used by the calldata loader;
• static composite helper parameters, lowered to ABI leaf words instead of a single synthetic Yul parameter;
• dynamic composite helper parameters, where static leaves and nested dynamic heads/tails need the same explicit binding discipline used at external-entry boundaries;
• call-site lowering for Stmt.internalCall / Expr.internalCall that looks up the callee signature and expands forwarded params/locals to the callee's lowered Yul arguments.

A conservative first implementation can support only direct forwarding from existing params/locals with known lowered bindings. That is enough for the Unlink _transferWithBalanceCheck(_permit, _depositor, _signature, ...) shape without requiring general ABI materialization of arbitrary expressions.

Proof-side impact remains the important part: helper-shape lemmas and source/helper summary bridges need to stop assuming one source argument equals one Yul helper argument. SupportedSpec can then be widened in stages: arrays are already done; bytes/string and composites should each get their own proof boundary and smoke coverage.

[Th0rgal]

Status update from the current Unlink translation work (local branches, not yet merged):

• Compiler.CompilationModel.Dispatch.internalFunctionYulParamNames now expands internal helper params for bytes / string, dynamic arrays, static tuples/fixed arrays, and static named structs.
• ValidationCalls.internalCallYulArgCountForParam now counts the expanded Yul arguments instead of assuming one source param = one Yul param.
• Verity.Macro.Translate now forwards direct bytes / string params as data-offset + length and forwards static composite params as flattened leaf bindings.
• Regression coverage in Contracts.Smoke includes:
  • helper with Bytes param and side effect,
  • helper with Bytes param and return binding,
  • helper with Bytes param and tuple return,
  • Unlink-shaped helper with PermitTransferFrom, Address, Bytes, Uint256, Bytes32,
  • Uint256/Bytes32 word-alias forwarding needed by the Unlink witness path.
• verity-benchmark UnlinkPool.deposit now calls a real transferWithBalanceCheck(PermitTransferFrom, Address, Bytes, Uint256, Bytes32) helper instead of inlining the Permit2 balance-delta logic.
• Benchmark.Cases.UnlinkXyz.Pool.Compile has a regression that checks the helper signature and that deposit contains an internal call to it.

Recommended narrowing after this lands: keep this issue open only for proof-side generalization and unsupported dynamic-composite/materialized-value cases. The concrete Unlink _transferWithBalanceCheck blocker described here is operationally addressed by the local implementation once merged.

[Th0rgal]

Post-merge status update:

The concrete Unlink translation blocker covered by this issue is fixed by verity#1900 and exercised by verity-benchmark#71:

• internal bytes/string helper parameters lower to data_offset/length form for declarations, validation calls, and direct helper calls;
• static composite helper parameters lower through static binding names;
• helper overload aliasing covers the Uint256/Bytes32 source-shape case used by Unlink;
• the benchmark deposit path now calls the source-shaped transferWithBalanceCheck helper instead of inlining the Permit2 balance-delta logic.

I am leaving this open as the narrower follow-up for any general dynamic/composite internal-helper work outside that translated surface, especially proof-side/materialized-value cases. It should no longer be treated as a blocker for the current Unlink pool benchmark translation.

[Th0rgal]

Converted this issue to the narrower remaining scope. The operational Unlink helper blocker is no longer the target here; this issue now tracks proof-side generalization and still-unsupported materialized dynamic/composite helper values after the direct-forwarding cases landed.