verity_contract cannot call internal helpers with Array parameters

[fricoben]

What I was trying to do

While modeling Polygon/AgglayerBridge claim verification, the Solidity source keeps Merkle-proof logic behind internal helpers:

• claimAsset(...) calls _verifyLeafAndSetNullifier(...)
• _verifyLeafAndSetNullifier(...) calls _verifyLeaf(...)
• _verifyLeaf(...) consumes two bytes32[32] calldata Merkle proofs

Source references:

• https://github.com/agglayer/agglayer-contracts/blob/110bda5a03e70ee7331bc06407a8e79226d3e520/contracts/AgglayerBridge.sol#L555-L569
• https://github.com/agglayer/agglayer-contracts/blob/110bda5a03e70ee7331bc06407a8e79226d3e520/contracts/AgglayerBridge.sol#L788-L820

In Verity, the natural model is to represent those proofs as Array Uint256 and preserve the helper boundary:

import Contracts.Common

open Verity hiding pure bind
open Verity.EVM.Uint256
open Contracts

verity_contract ArrayHelperRepro where
  storage
    ok : Uint256 := slot 0

  function first (xs : Array Uint256) : Uint256 := do
    let x := arrayElement xs 0
    return x

  function useFirst (xs : Array Uint256) : Unit := do
    let x ← first xs
    setStorage ok x

What fails

On current main (3157166c48534db72817b1ac5acb3a7f29c5b45d), lake env lean .tmp/ArrayHelperRepro.lean fails with:

error: helper call 'first' uses a parameter or return type that direct macro helper lowering does not support yet; only static non-fallback/non-receive helpers can be lowered to internal specs

The same limitation appears in the existing smoke tests around helper calls such as consumePayload, measurePayload, and fanoutPayload, but I did not find a focused open issue for Array-parameter helper calls.

Why this is a real modeling gap

This is not a proof-gap-only issue. Array Uint256 parameters and arrayElement are supported directly, and scalar helper calls are supported directly, but combining them forces a source-structure change: callers must inline the helper body. For AgglayerBridge, that means claimAsset and claimMessage cannot remain line-by-line close to Solidity around _verifyLeafAndSetNullifier / _verifyLeaf.

The workaround preserves semantics for this benchmark, but it harms reviewability and makes larger Merkle/proof-heavy bridge contracts much harder to model faithfully.

Desired behavior

A verity_contract function should be able to call a static internal helper whose parameter or return type includes supported ABI/static array types, at least Array Uint256, when those types already work as direct public/function parameters and in arrayElement expressions.

Open PR check

I checked open PRs for related terms (direct macro helper lowering, helper call, Array, internal specs) and did not find one that appears to fix this surface. #1822 appears focused on EVMYulLean correctness retargeting, not this macro helper-lowering gap.