Skip to content

Commit f08face

Browse files
Th0rgalTh0rgal
authored
feat: self-delegate multicall helper (#1997) (#2029)
* feat: add self-delegate multicall helper * fix(verity): multicall offset-wrap bound check + documented trusted ECM (#2029)
1 parent 3b28770 commit f08face

9 files changed

Lines changed: 318 additions & 7 deletions

File tree

‎AXIOMS.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -245,6 +245,7 @@ call-buffer-disjoint-from-heap theorem live at `Verity.EVM.Layout`.
245245
| `Calls.withReturn` | `external_call_abi_interface` | Target contract function matches declared selector and ABI |
246246
| `Calls.callWithValue` / `Calls.callWithValueBytes` | `generic_call_with_value_interface` | Target accepts caller-provided calldata and ETH value; failures bubble returndata |
247247
| `Calls.bubblingValueCall` / `Calls.bubblingValueCallNoOutput` | `generic_low_level_value_call_interface` | Generic low-level `call` mechanics are emitted; calldata and successful returndata meaning remain package assumptions |
248+
| `Calls.selfDelegateMulticallBytes` | `self_delegate_multicall_bytes_revert_bubbling` | Trusted ECM boundary for Solidity-style `multicall(bytes[])`: generated Yul is audited to reject malformed/wrapping offsets, self-`delegatecall` each calldata payload, and bubble revert returndata exactly; full non-empty multicall semantics remain assumed |
248249
| `Hashing.abiEncodeStaticWords` | `keccak256_memory_slice_matches_evm`, `abi_standard_static_word_layout` | Static ABI words are laid out contiguously before Keccak |
249250
| `Hashing.abiEncodePackedWords` / `Hashing.abiEncodePacked` | `keccak256_memory_slice_matches_evm`, `abi_packed_static_word_layout` | Static packed words are laid out contiguously before Keccak |
250251
| `Hashing.abiEncodeStaticArray` | `keccak256_memory_slice_matches_evm`, `abi_standard_dynamic_array_static_element_layout` | Single dynamic-array ABI encoding with static-width elements is laid out before Keccak |

‎Compiler/CompilationModel/TrustSurface.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -788,7 +788,7 @@ private def boundaryClassFromModule (mod : ECM.ExternalCallModule) : String :=
788788
| "maxDeposit" | "maxMint" | "maxWithdraw" | "maxRedeem" | "deposit" =>
789789
"tokenModel"
790790
| "externalCallWithReturn" | "externalCallNoReturn" | "callWithValue" | "callWithValueBytes"
791-
| "bubblingValueCall" | "bubblingValueCallNoOutput" =>
791+
| "bubblingValueCall" | "bubblingValueCallNoOutput" | "selfDelegateMulticallBytes" =>
792792
"abiBoundary"
793793
| "create2Deploy" | "sstore2ReadCode" =>
794794
"storageLayoutAssumption"

‎Compiler/Modules/Calls.lean‎

Lines changed: 118 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,18 @@
1010
copying the payload to memory before the call
1111
- `bubblingValueCall`: arbitrary low-level call with caller-provided ETH value,
1212
caller-provided input/output memory slices, and exact revert-data bubbling
13+
- `selfDelegateMulticallBytes`: Solidity-style `multicall(bytes[])` over a
14+
calldata bytes-array parameter, using `delegatecall(address(), data)` for
15+
each element and bubbling exact revert data
1316
1417
Trust assumption: the target contract's function matches the declared
1518
selector and ABI encoding. For `callWithValue`, the caller is responsible for
1619
preparing calldata at the supplied memory slice. `callWithValueBytes` copies a
1720
bytes parameter into memory before calling. For arbitrary low-level calls, the
1821
target contract behavior and calldata ABI are deliberately outside Verity core
19-
and are surfaced as an explicit ECM assumption.
22+
and are surfaced as an explicit ECM assumption. The multicall helper is
23+
intentionally scoped to self-delegatecall: storage context is the current
24+
contract's storage, and no caller-selected implementation address is exposed.
2025
-/
2126

2227
import Compiler.ECM
@@ -51,6 +56,90 @@ private def bubblingValueCallYul
5156
]
5257
]]
5358

59+
def selfDelegateMulticallBytesBody
60+
(arrayParam ptrName indexName successName rdsName : String) : Except String (List YulStmt) := do
61+
if arrayParam.isEmpty then
62+
throw "selfDelegateMulticallBytes: arrayParam must be non-empty"
63+
let ptrExpr := YulExpr.ident ptrName
64+
let indexExpr := YulExpr.ident indexName
65+
let arrayDataOffset := YulExpr.ident s!"{arrayParam}_data_offset"
66+
let arrayLength := YulExpr.ident s!"{arrayParam}_length"
67+
let offsetTableBytes := YulExpr.call "mul" [arrayLength, YulExpr.lit 32]
68+
let elementOffsetSlot := YulExpr.call "add" [
69+
arrayDataOffset,
70+
YulExpr.call "mul" [indexExpr, YulExpr.lit 32]
71+
]
72+
let paddedSizeExpr := YulExpr.call "and" [
73+
YulExpr.call "add" [YulExpr.ident "__mc_data_size", YulExpr.lit 31],
74+
YulExpr.call "not" [YulExpr.lit 31]
75+
]
76+
pure [
77+
YulStmt.let_ ptrName (YulExpr.call "mload" [YulExpr.lit freeMemoryPointer]),
78+
YulStmt.for_
79+
[YulStmt.let_ indexName (YulExpr.lit 0)]
80+
(YulExpr.call "lt" [indexExpr, arrayLength])
81+
[YulStmt.assign indexName (YulExpr.call "add" [indexExpr, YulExpr.lit 1])]
82+
[
83+
YulStmt.let_ "__mc_rel_offset" (YulExpr.call "calldataload" [elementOffsetSlot]),
84+
YulStmt.if_ (YulExpr.call "lt" [YulExpr.ident "__mc_rel_offset", offsetTableBytes]) [
85+
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
86+
],
87+
YulStmt.if_ (YulExpr.call "gt" [
88+
YulExpr.ident "__mc_rel_offset",
89+
YulExpr.call "sub" [
90+
YulExpr.call "not" [YulExpr.lit 0],
91+
arrayDataOffset
92+
]
93+
]) [
94+
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
95+
],
96+
YulStmt.let_ "__mc_head_offset" (YulExpr.call "add" [arrayDataOffset, YulExpr.ident "__mc_rel_offset"]),
97+
YulStmt.if_ (YulExpr.call "gt" [
98+
YulExpr.ident "__mc_head_offset",
99+
YulExpr.call "sub" [YulExpr.call "calldatasize" [], YulExpr.lit 32]
100+
]) [
101+
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
102+
],
103+
YulStmt.let_ "__mc_data_size" (YulExpr.call "calldataload" [YulExpr.ident "__mc_head_offset"]),
104+
YulStmt.let_ "__mc_data_offset" (YulExpr.call "add" [YulExpr.ident "__mc_head_offset", YulExpr.lit 32]),
105+
YulStmt.if_ (YulExpr.call "gt" [
106+
YulExpr.ident "__mc_data_size",
107+
YulExpr.call "sub" [YulExpr.call "calldatasize" [], YulExpr.ident "__mc_data_offset"]
108+
]) [
109+
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
110+
],
111+
YulStmt.expr (YulExpr.call "calldatacopy" [
112+
ptrExpr,
113+
YulExpr.ident "__mc_data_offset",
114+
YulExpr.ident "__mc_data_size"
115+
]),
116+
YulStmt.expr (YulExpr.call "mstore" [
117+
YulExpr.lit freeMemoryPointer,
118+
YulExpr.call "add" [ptrExpr, paddedSizeExpr]
119+
]),
120+
YulStmt.let_ successName (YulExpr.call "delegatecall" [
121+
YulExpr.call "gas" [],
122+
YulExpr.call "address" [],
123+
ptrExpr,
124+
YulExpr.ident "__mc_data_size",
125+
YulExpr.lit 0,
126+
YulExpr.lit 0
127+
]),
128+
YulStmt.if_ (YulExpr.call "iszero" [YulExpr.ident successName]) [
129+
YulStmt.let_ rdsName (YulExpr.call "returndatasize" []),
130+
YulStmt.expr (YulExpr.call "returndatacopy" [
131+
YulExpr.lit 0, YulExpr.lit 0, YulExpr.ident rdsName
132+
]),
133+
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.ident rdsName])
134+
]
135+
]
136+
]
137+
138+
theorem selfDelegateMulticallBytesBody_empty_param :
139+
selfDelegateMulticallBytesBody "" "__mc_ptr" "__mc_i" "__mc_success" "__mc_rds" =
140+
Except.error "selfDelegateMulticallBytes: arrayParam must be non-empty" := by
141+
rfl
142+
54143
/-- Generic external call with single uint256 return.
55144
ABI-encodes `selector(args...)`, calls/staticcalls target, reverts on failure,
56145
validates returndatasize >= 32, and binds the result.
@@ -374,4 +463,32 @@ def callWithValueBytesModule (bytesParam : String) : ExternalCallModule where
374463
def callWithValueBytes (target value : Expr) (bytesParam : String) : Stmt :=
375464
.ecm (callWithValueBytesModule bytesParam) [target, value]
376465

466+
/-- Source-level `multicall(bytes[])` helper for self-delegatecall routers.
467+
468+
The named parameter must be a `bytes[]` ABI parameter. The generated Yul
469+
walks the ABI offset table, copies each element payload into memory, then
470+
executes `delegatecall(gas(), address(), ptr, size, 0, 0)`. On failure it
471+
forwards returndata exactly with `returndatacopy(0, 0, returndatasize())`
472+
followed by `revert(0, returndatasize())`.
473+
474+
Unlike the general `Expr.delegatecall` surface, this module has no dynamic
475+
implementation address and is intended for same-contract multicall only. -/
476+
def selfDelegateMulticallBytesModule (arrayParam : String) : ExternalCallModule where
477+
name := "selfDelegateMulticallBytes"
478+
numArgs := 0
479+
resultVars := []
480+
writesState := true
481+
readsState := true
482+
axioms := ["self_delegate_multicall_bytes_revert_bubbling"]
483+
compile := fun _ctx args => do
484+
match args with
485+
| [] =>
486+
selfDelegateMulticallBytesBody arrayParam "__mc_ptr" "__mc_i" "__mc_success" "__mc_rds"
487+
| _ =>
488+
throw "selfDelegateMulticallBytes expects 0 arguments"
489+
490+
/-- Convenience constructor for self-delegatecall `multicall(bytes[])`. -/
491+
def selfDelegateMulticallBytes (arrayParam : String) : Stmt :=
492+
.ecm (selfDelegateMulticallBytesModule arrayParam) []
493+
377494
end Compiler.Modules.Calls

‎Compiler/Modules/CallsTest.lean‎

Lines changed: 166 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,166 @@
1+
import Compiler.Codegen
2+
import Compiler.CompilationModel
3+
import Compiler.CompilationModel.TrustSurface
4+
import Compiler.Modules.Calls
5+
import Compiler.Yul.PrettyPrint
6+
7+
namespace Compiler.Modules.CallsTest
8+
9+
open Compiler
10+
open Compiler.CompilationModel
11+
12+
private def contains (haystack needle : String) : Bool :=
13+
let h := haystack.toList
14+
let n := needle.toList
15+
if n.isEmpty then true
16+
else
17+
let rec go : List Char → Bool
18+
| [] => false
19+
| c :: cs =>
20+
if (c :: cs).take n.length == n then true
21+
else go cs
22+
go h
23+
24+
private def expectTrue (label : String) (ok : Bool) : IO Unit := do
25+
if !ok then
26+
throw (IO.userError s!"✗ {label}")
27+
IO.println s!"✓ {label}"
28+
29+
private def selectorsFor (spec : CompilationModel) : List Nat :=
30+
List.range (spec.functions.filter (fun fn =>
31+
!fn.isInternal && fn.name != "fallback" && fn.name != "receive")).length
32+
33+
private def expectCompileErrorContains (label : String)
34+
(spec : CompilationModel) (needle : String) : IO Unit := do
35+
match Compiler.CompilationModel.compile spec (selectorsFor spec) with
36+
| .ok _ => throw (IO.userError s!"✗ {label}: expected compile error containing '{needle}'")
37+
| .error err =>
38+
if !contains err needle then
39+
throw (IO.userError s!"✗ {label}: expected error containing '{needle}', got '{err}'")
40+
IO.println s!"✓ {label}"
41+
42+
private def expectCompileToYul (label : String) (spec : CompilationModel) : IO String := do
43+
match Compiler.CompilationModel.compile spec (selectorsFor spec) with
44+
| .ok ir =>
45+
IO.println s!"✓ {label}"
46+
pure (Compiler.Yul.render (Compiler.emitYul ir))
47+
| .error err =>
48+
throw (IO.userError s!"✗ {label}: compile failed: {err}")
49+
50+
private def selfDelegateMulticallBytesSmokeSpec : CompilationModel := {
51+
name := "SelfDelegateMulticallBytesSmoke"
52+
fields := []
53+
«constructor» := none
54+
functions := [
55+
{ name := "multicall"
56+
params := [
57+
{ name := "calls", ty := ParamType.array ParamType.bytes }
58+
]
59+
returnType := none
60+
body := [
61+
Compiler.Modules.Calls.selfDelegateMulticallBytes "calls",
62+
Stmt.stop
63+
]
64+
}
65+
]
66+
}
67+
68+
private def selfDelegateMulticallBytesBadAritySpec : CompilationModel := {
69+
name := "SelfDelegateMulticallBytesBadArity"
70+
fields := []
71+
«constructor» := none
72+
functions := [
73+
{ name := "bad"
74+
params := [
75+
{ name := "calls", ty := ParamType.array ParamType.bytes }
76+
]
77+
returnType := none
78+
body := [
79+
Stmt.ecm (Compiler.Modules.Calls.selfDelegateMulticallBytesModule "calls")
80+
[Expr.arrayLength "calls"],
81+
Stmt.stop
82+
]
83+
}
84+
]
85+
}
86+
87+
private def selfDelegateMulticallBytesEmptyParamSpec : CompilationModel := {
88+
name := "SelfDelegateMulticallBytesEmptyParam"
89+
fields := []
90+
«constructor» := none
91+
functions := [
92+
{ name := "bad"
93+
params := [
94+
{ name := "calls", ty := ParamType.array ParamType.bytes }
95+
]
96+
returnType := none
97+
body := [
98+
Compiler.Modules.Calls.selfDelegateMulticallBytes "",
99+
Stmt.stop
100+
]
101+
}
102+
]
103+
}
104+
105+
private def selfDelegateMulticallBytesViewRejectedSpec : CompilationModel := {
106+
name := "SelfDelegateMulticallBytesViewRejected"
107+
fields := []
108+
«constructor» := none
109+
functions := [
110+
{ name := "multicall"
111+
params := [
112+
{ name := "calls", ty := ParamType.array ParamType.bytes }
113+
]
114+
returnType := none
115+
isView := true
116+
body := [
117+
Compiler.Modules.Calls.selfDelegateMulticallBytes "calls",
118+
Stmt.stop
119+
]
120+
}
121+
]
122+
}
123+
124+
unsafe def runTests : IO Unit := do
125+
let yul ←
126+
expectCompileToYul "self-delegate multicall bytes smoke spec" selfDelegateMulticallBytesSmokeSpec
127+
expectTrue "self-delegate multicall walks bytes[] calldata offsets"
128+
(contains yul "for {" &&
129+
contains yul "let __mc_i := 0" &&
130+
contains yul "lt(__mc_i, calls_length)" &&
131+
contains yul "let __mc_rel_offset := calldataload(add(calls_data_offset, mul(__mc_i, 32)))" &&
132+
contains yul "if lt(__mc_rel_offset, mul(calls_length, 32)) {" &&
133+
contains yul "if gt(__mc_rel_offset, sub(not(0), calls_data_offset)) {" &&
134+
contains yul "let __mc_head_offset := add(calls_data_offset, __mc_rel_offset)" &&
135+
contains yul "let __mc_data_size := calldataload(__mc_head_offset)" &&
136+
contains yul "let __mc_data_offset := add(__mc_head_offset, 32)")
137+
expectTrue "self-delegate multicall copies each bytes payload and delegatecalls address()"
138+
(contains yul "calldatacopy(__mc_ptr, __mc_data_offset, __mc_data_size)" &&
139+
contains yul "delegatecall(gas(), address(), __mc_ptr, __mc_data_size, 0, 0)")
140+
expectTrue "self-delegate multicall forwards revert returndata exactly"
141+
(contains yul "let __mc_rds := returndatasize()" &&
142+
contains yul "returndatacopy(0, 0, __mc_rds)" &&
143+
contains yul "revert(0, __mc_rds)")
144+
expectCompileErrorContains
145+
"self-delegate multicall ECM rejects invalid argument counts"
146+
selfDelegateMulticallBytesBadAritySpec
147+
"uses ECM 'selfDelegateMulticallBytes' with 1 arguments but it expects 0"
148+
expectCompileErrorContains
149+
"self-delegate multicall rejects empty parameter names"
150+
selfDelegateMulticallBytesEmptyParamSpec
151+
"selfDelegateMulticallBytes: arrayParam must be non-empty"
152+
expectCompileErrorContains
153+
"self-delegate multicall remains rejected from view functions"
154+
selfDelegateMulticallBytesViewRejectedSpec
155+
"function 'multicall' is marked view but writes state"
156+
let report := emitTrustReportJson [selfDelegateMulticallBytesSmokeSpec]
157+
expectTrue "self-delegate multicall trust report surfaces scoped multicall assumption without proxy boundary"
158+
(contains report "\"module\":\"selfDelegateMulticallBytes\"" &&
159+
contains report "\"assumption\":\"self_delegate_multicall_bytes_revert_bubbling\"" &&
160+
contains report "\"boundaryClass\":\"abiBoundary\"" &&
161+
contains report "\"notModeledProxyUpgradeability\":[]" &&
162+
! (contains report "\"delegatecall\""))
163+
164+
#eval! runTests
165+
166+
end Compiler.Modules.CallsTest

‎TRUST_ASSUMPTIONS.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -75,8 +75,8 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V
7575
- **Proxy note**: `delegatecall`-based proxy / upgradeability flows still sit outside the current native verified runtime model. Archive `--trust-report` and use `--deny-proxy-upgradeability` when proxy semantics must remain outside the selected verified subset (issue `#1420`).
7676

7777
### 7. External Call Modules (ECMs)
78-
- **Role**: Reusable typed external call patterns (ERC-20 writes/reads including `totalSupply`, ERC-4626 preview/conversion helpers plus `totalAssets`, `asset`, `max*` limit reads, and `deposit`, oracle reads, precompiles 0x01 / 0x02 / 0x06 / 0x07 / 0x08 — `ecrecover`, `sha256`, BN254 `bn256Add`, `bn256ScalarMul`, `bn256Pairing` — callbacks).
79-
- **Trust**: Each module's `compile` produces correct Yul. Bug in one module doesn't affect others.
78+
- **Role**: Reusable typed external call patterns (ERC-20 writes/reads including `totalSupply`, ERC-4626 preview/conversion helpers plus `totalAssets`, `asset`, `max*` limit reads, and `deposit`, oracle reads, precompiles 0x01 / 0x02 / 0x06 / 0x07 / 0x08 — `ecrecover`, `sha256`, BN254 `bn256Add`, `bn256ScalarMul`, `bn256Pairing` — callbacks, and same-contract `selfDelegateMulticallBytes`).
79+
- **Trust**: Each module's `compile` produces correct Yul. Bug in one module doesn't affect others. `selfDelegateMulticallBytes` is an explicitly trusted ECM boundary under `self_delegate_multicall_bytes_revert_bubbling`: the compiler emits concrete bounds checks for ABI element offsets, including a pre-add overflow guard before forming the calldata head offset, but full non-empty multicall revert-bubbling semantics are not yet machine-proven.
8080
- **Mitigation**: Axiom aggregation at compile time (`--verbose`), machine-readable trust-surface emission via `--trust-report <path>`, and a fail-closed verification gate via `--deny-unchecked-dependencies` when unchecked foreign surfaces must be excluded. See [docs/EXTERNAL_CALL_MODULES.md](docs/EXTERNAL_CALL_MODULES.md).
8181
- **Caller-frame preservation**: The EVM frame condition (external `CALL` cannot mutate caller storage / transient storage / memory outside the declared output buffer) is now a *theorem* of `Verity.EVM.Frame` rather than an assumption. Downstream proofs consume `external_call_preserves_caller_storage` etc. directly. The abstract memory model used by these theorems is `Verity.EVM.MemoryModel`; the solc memory-layout schema and call-buffer-disjoint-from-heap result are in `Verity.EVM.Layout`. EvmYul ↔ abstract-model correspondence remains the open follow-up.
8282

‎docs-site/content/edsl-api-reference.mdx‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -442,9 +442,16 @@ Compiler.Modules.Calls.withReturn
442442
443443
Compiler.Modules.Calls.bubblingValueCall
444444
(target value inputOffset inputSize outputOffset outputSize : Expr) : Stmt
445+
446+
Compiler.Modules.Calls.selfDelegateMulticallBytes
447+
(arrayParam : String) : Stmt
445448
```
446449

447450
`Oracle.oracleReadUint256` is the standard read-only oracle case; trust-report assumption `oracle_read_uint256_interface`.
451+
`selfDelegateMulticallBytes "calls"` is the scoped `multicall(bytes[])`
452+
helper for same-contract delegatecall loops. It walks the named `bytes[]`
453+
calldata parameter, copies each payload, emits `delegatecall(gas(), address(),
454+
ptr, size, 0, 0)`, and bubbles exact revert data on failure.
448455

449456
### `keccak256` primitive
450457

0 commit comments

Comments
 (0)