`verity_contract` rejects function-pointer parameters

[fricoben]

What I was trying to do

Model TermMaxOrderV2._swapAndUpdateReserves, which takes a function pointer:

// contracts/v2/TermMaxOrderV2.sol:859-867
function _swapAndUpdateReserves(
    uint256 tokenAmtInOrOut,
    uint256 limitTokenAmt,
    OrderConfig memory orderConfig_,
    function(
      uint256,
      uint256,
      OrderConfig memory) internal view returns (uint256, uint256, uint256, uint256, bool) func
) private returns (uint256, uint256, int256, int256) {
    (uint256 netAmt, uint256 feeAmt, uint256 deltaFt, uint256 deltaXt, bool isNegetiveXt) =
        func(tokenAmtInOrOut, limitTokenAmt, orderConfig_);
    ...
}

https://github.com/term-structure/termmax-contract-v2/blob/64bd47b98e064c7fb91ab4a59b70520e0ec285d5/contracts/v2/TermMaxOrderV2.sol#L859-L884

What I tried

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

verity_contract FnPtrRepro where
  storage dummy : Uint256 := slot 0

  function addOne (x : Uint256) : Uint256 := do
    return (add x 1)

  function apply (f : Uint256 -> Uint256, x : Uint256) : Uint256 := do
    return (f x)

Why it failed

Verity/Macro/Translate.lean:242 rejects function-typed parameters:

unsupported type 'Uint256 -> Uint256'; expected Uint256, Int256, Uint8,
  Address, Bytes32, Bool, String, Bytes, Array <type>, Tuple [...], Unit,
  or a user-defined type from the `types` or `inductive` section

Even if the parameter type were accepted, the bind-source checker at
Verity/Macro/Translate.lean:1889 rejects let x ← f ... whose source is
not getStorage or a direct internal helper call:

unsupported bind source; expected getStorage/getStorageAddr/...
  or a direct internal helper call

Reproduces on Verity 74d8fe20ffa2f5dbb94959f3dd40a62df6aa8224 (release
v1.0.0).

[Th0rgal]

Why this stays low-priority

Per the issue: "not used by Unlink, but flagged in the roadmap". The TermMaxOrderV2 use case is the only concrete blocker today, and the upstream Solidity pattern is itself a workaround for the lack of generics: the function-pointer parameter is the dispatch mechanism inside a hand-written virtual call. There is no value-flow that requires the dispatched function to be runtime-selected — every call site passes a static internal-function literal.

That suggests two implementation paths, ranked by tractability:

Path A — inline expansion at macro time (preferred)

Treat function (Uint256, ...) returns (...) parameters as static dispatch sites: at every call site, the user passes a literal Verity helper name, and the macro inlines that name's body into the calling function at elaboration time. This avoids any runtime indirection.

• Pro: no new IR. The Yul output is identical to a hand-inlined version. No proof obligation; no axiom; no trust surface.
• Pro: matches the upstream Solidity pattern where the function pointer is always a internal reference resolved at link time.
• Con: cannot model true dynamic dispatch (e.g., constructor-injected function pointer). None of TermMaxOrderV2's uses need that.
• Surface: extend Verity/Macro/Syntax.lean:34 to accept function (T,...) returns (R,...) parameter syntax. Extend Verity/Macro/Translate.lean paramTypeFromSyntax? to recognise the new shape. Inline at the macro level by replacing the function call with the body of the named helper, with arg substitution. No ParamType.function constructor needed; the parameter is erased at lowering.

Path B — true function-pointer values (deferred)

Add ParamType.function (args : List ParamType) (ret : List ParamType) and Expr.callFnPointer fp args. Lowering uses a jump-table indexed by an internal function-id (compile-time mapped 1:1 with internal Verity helpers). This is substantially more work and brings a new axiom-shaped trust assumption ("the jump table is total over the set of statically reachable function ids"). Defer until a value-flow use case shows up.

Suggested execution order if/when picked up

1. Path A pilot: add function (Uint256) returns (Uint256) syntax to verityParam and extend the param-type parser.
2. At the call site, recognise f x where f is a function-typed parameter; require the call site to pass a literal helper name (statically resolvable); inline the helper body with the literal argument.
3. Smoke contract mirroring the TermMax pattern (e.g. apply (f : Uint256 → Uint256, x : Uint256) : Uint256 := f x, invoked with apply incrementHelper 5).
4. Update Verity/Macro/Translate.lean:242 rejection list to remove the function-type entry once the new path is wired.

Severity tag should drop to nice-to-have once Path A lands — the Solidity pattern this models is already a static workaround for missing generics, and the value to a verifier is mainly ergonomic (less boilerplate in the Lean model). The deferred Path B remains a true language extension if/when a benchmark needs runtime dispatch.