feat: self-delegate multicall helper (#1997)

[Th0rgal]

Summary

Implements issue #1997 — multicall(bytes[]).

• Adds Compiler.Modules.Calls.selfDelegateMulticallBytesModule / selfDelegateMulticallBytes: a scoped multicall(bytes[]) ECM that walks checked bytes-array calldata offsets, copies each payload, self-delegatecalls address(), and bubbles exact revert returndata.
• Trust reports classify it as abiBoundary, not generic proxy upgradeability.

Proofs

• Adds selfDelegateMulticallBytesBody_empty_param; proof-length check passed.

Stacking

Based on task/1993a-checked-arith (#1993 emission), which carries the Tier-1 dynamic-ABI + checked-arith machinery this helper relies on.

Test plan

• lake build Verity Contracts Compiler PrintAxioms → "Build completed successfully."
• make check → "All checks passed."
• zero sorry, zero axioms

---

Note

Medium Risk
Introduces state-writing delegatecall loops and a trusted ECM boundary whose full multicall semantics are documented but not machine-proven; mis-generated Yul or malformed calldata handling could affect contract behavior.

Overview
Adds Compiler.Modules.Calls.selfDelegateMulticallBytes for Solidity-style multicall(bytes[]) on a named calldata parameter. Generated Yul walks the dynamic bytes[] offset table with bounds checks, copies each element, runs delegatecall(gas(), address(), …) (same contract only—no caller-chosen implementation address), and bubbles revert returndata on failure.

Trust reporting registers assumption self_delegate_multicall_bytes_revert_bubbling under abiBoundary, so usage does not appear in notModeledProxyUpgradeability. Docs (AXIOMS, TRUST_ASSUMPTIONS, EDSL/API, ECM guide) and CallsTest compile/Yul/trust-report smoke tests cover the new surface; a small selfDelegateMulticallBytesBody_empty_param proof guards empty parameter names.

^{Reviewed by Cursor Bugbot for commit 14684cd. 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 14, 2026 7:56pm

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

[cursor]

Wrong bytes element head base

High Severity

Each bytes[] offset in calldata is relative to the array length word, but __mc_head_offset adds the loaded offset to {arrayParam}_data_offset, which genDynamicParamLoads places 32 bytes after that length word. Standard Solidity-encoded multicall calldata can resolve the wrong element head, so calldatacopy and delegatecall may use incorrect payload bytes.

 

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

[Th0rgal]

Re: "Wrong bytes element head base" (High) — this is a false positive.

Per the Solidity ABI spec, bytes[] encodes as enc(k) enc((X[0],…,X[k-1])). The element head offsets live inside the inner tuple enc((X[0],…)), and tuple offsets are measured from the start of that tuple encoding — i.e. from the first head word, which is the byte immediately after the length word — not from the length word itself.

{arrayParam}_data_offset is exactly that position (the first head word, 32 bytes past the length word, as the finding itself notes). So __mc_head_offset = data_offset + __mc_rel_offset resolves the correct element head.

Worked example (bytes[] of two 2-byte elements, length word at byte P):

• length word P; heads at P+0x20, P+0x40; X[0] len at P+0x60, X[1] len at P+0xA0.
• data_offset = P+0x20. Encoded head[0] = 0x40 (relative to tuple start), so data_offset + 0x40 = P+0x60 = X[0] ✓.
• Using the length word P as base (as the finding suggests) would give P+0x40 = head[1] — i.e. that base is the incorrect one.

This is corroborated by the in-code guard if __mc_rel_offset < arrayLength*32 then revert: the minimum valid relative offset equals the size of the heads table only when offsets are measured from the heads-block start (= data_offset). The emission additionally guards against pre-add wraparound (__mc_rel_offset > not(0) - data_offset), out-of-range head (> calldatasize-32), and out-of-range payload (> calldatasize - data_offset). No fix needed.

[Th0rgal]

Bugbot HIGH "Wrong bytes element head base" — assessed as a FALSE POSITIVE (no code change).

The finding reads data_offset + rel_offset as pointing one word past the intended element head, on the assumption that the per-element head offset is encoded relative to the array length word. That assumption is incorrect for this layout: the per-element head offsets are encoded relative to the start of the heads block (data_offset), not relative to the length slot. So data_offset + rel_offset resolves to the correct element head.

This is corroborated by the existing offsetTableBytes lower-bound check, which is computed against the heads block beginning at data_offset — if the base were the length word, that bound would be off by one word and the check would already be failing on conformance fixtures, which it is not.

Adjudicated via concrete ABI offset analysis of Compiler/Modules/Calls.lean. Leaving the code unchanged.