Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions AXIOMS.md
Original file line number Diff line number Diff line change
Expand Up @@ -245,6 +245,7 @@ call-buffer-disjoint-from-heap theorem live at `Verity.EVM.Layout`.
| `Calls.withReturn` | `external_call_abi_interface` | Target contract function matches declared selector and ABI |
| `Calls.callWithValue` / `Calls.callWithValueBytes` | `generic_call_with_value_interface` | Target accepts caller-provided calldata and ETH value; failures bubble returndata |
| `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 |
| `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 |
| `Hashing.abiEncodeStaticWords` | `keccak256_memory_slice_matches_evm`, `abi_standard_static_word_layout` | Static ABI words are laid out contiguously before Keccak |
| `Hashing.abiEncodePackedWords` / `Hashing.abiEncodePacked` | `keccak256_memory_slice_matches_evm`, `abi_packed_static_word_layout` | Static packed words are laid out contiguously before Keccak |
| `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 |
Expand Down
2 changes: 1 addition & 1 deletion Compiler/CompilationModel/TrustSurface.lean
Original file line number Diff line number Diff line change
Expand Up @@ -788,7 +788,7 @@ private def boundaryClassFromModule (mod : ECM.ExternalCallModule) : String :=
| "maxDeposit" | "maxMint" | "maxWithdraw" | "maxRedeem" | "deposit" =>
"tokenModel"
| "externalCallWithReturn" | "externalCallNoReturn" | "callWithValue" | "callWithValueBytes"
| "bubblingValueCall" | "bubblingValueCallNoOutput" =>
| "bubblingValueCall" | "bubblingValueCallNoOutput" | "selfDelegateMulticallBytes" =>
"abiBoundary"
| "create2Deploy" | "sstore2ReadCode" =>
"storageLayoutAssumption"
Expand Down
119 changes: 118 additions & 1 deletion Compiler/Modules/Calls.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,18 @@
copying the payload to memory before the call
- `bubblingValueCall`: arbitrary low-level call with caller-provided ETH value,
caller-provided input/output memory slices, and exact revert-data bubbling
- `selfDelegateMulticallBytes`: Solidity-style `multicall(bytes[])` over a
calldata bytes-array parameter, using `delegatecall(address(), data)` for
each element and bubbling exact revert data

Trust assumption: the target contract's function matches the declared
selector and ABI encoding. For `callWithValue`, the caller is responsible for
preparing calldata at the supplied memory slice. `callWithValueBytes` copies a
bytes parameter into memory before calling. For arbitrary low-level calls, the
target contract behavior and calldata ABI are deliberately outside Verity core
and are surfaced as an explicit ECM assumption.
and are surfaced as an explicit ECM assumption. The multicall helper is
intentionally scoped to self-delegatecall: storage context is the current
contract's storage, and no caller-selected implementation address is exposed.
-/

import Compiler.ECM
Expand Down Expand Up @@ -51,6 +56,90 @@ private def bubblingValueCallYul
]
]]

def selfDelegateMulticallBytesBody
(arrayParam ptrName indexName successName rdsName : String) : Except String (List YulStmt) := do
if arrayParam.isEmpty then
throw "selfDelegateMulticallBytes: arrayParam must be non-empty"
let ptrExpr := YulExpr.ident ptrName
let indexExpr := YulExpr.ident indexName
let arrayDataOffset := YulExpr.ident s!"{arrayParam}_data_offset"
let arrayLength := YulExpr.ident s!"{arrayParam}_length"
let offsetTableBytes := YulExpr.call "mul" [arrayLength, YulExpr.lit 32]
let elementOffsetSlot := YulExpr.call "add" [
arrayDataOffset,
YulExpr.call "mul" [indexExpr, YulExpr.lit 32]
]
let paddedSizeExpr := YulExpr.call "and" [
YulExpr.call "add" [YulExpr.ident "__mc_data_size", YulExpr.lit 31],
YulExpr.call "not" [YulExpr.lit 31]
]
pure [
YulStmt.let_ ptrName (YulExpr.call "mload" [YulExpr.lit freeMemoryPointer]),
YulStmt.for_
[YulStmt.let_ indexName (YulExpr.lit 0)]
(YulExpr.call "lt" [indexExpr, arrayLength])
[YulStmt.assign indexName (YulExpr.call "add" [indexExpr, YulExpr.lit 1])]
[
YulStmt.let_ "__mc_rel_offset" (YulExpr.call "calldataload" [elementOffsetSlot]),
YulStmt.if_ (YulExpr.call "lt" [YulExpr.ident "__mc_rel_offset", offsetTableBytes]) [
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
],
YulStmt.if_ (YulExpr.call "gt" [
YulExpr.ident "__mc_rel_offset",
YulExpr.call "sub" [
YulExpr.call "not" [YulExpr.lit 0],
arrayDataOffset
]
]) [
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
],
YulStmt.let_ "__mc_head_offset" (YulExpr.call "add" [arrayDataOffset, YulExpr.ident "__mc_rel_offset"]),

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Fix in Cursor Fix in Web

Reviewed by Cursor Bugbot for commit c199d98. Configure here.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

YulStmt.if_ (YulExpr.call "gt" [
YulExpr.ident "__mc_head_offset",
YulExpr.call "sub" [YulExpr.call "calldatasize" [], YulExpr.lit 32]
]) [
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
],
YulStmt.let_ "__mc_data_size" (YulExpr.call "calldataload" [YulExpr.ident "__mc_head_offset"]),
YulStmt.let_ "__mc_data_offset" (YulExpr.call "add" [YulExpr.ident "__mc_head_offset", YulExpr.lit 32]),
YulStmt.if_ (YulExpr.call "gt" [
YulExpr.ident "__mc_data_size",
YulExpr.call "sub" [YulExpr.call "calldatasize" [], YulExpr.ident "__mc_data_offset"]
]) [
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
],
YulStmt.expr (YulExpr.call "calldatacopy" [
ptrExpr,
YulExpr.ident "__mc_data_offset",
YulExpr.ident "__mc_data_size"
]),
YulStmt.expr (YulExpr.call "mstore" [
YulExpr.lit freeMemoryPointer,
YulExpr.call "add" [ptrExpr, paddedSizeExpr]
]),
YulStmt.let_ successName (YulExpr.call "delegatecall" [
YulExpr.call "gas" [],
YulExpr.call "address" [],
ptrExpr,
YulExpr.ident "__mc_data_size",
YulExpr.lit 0,
YulExpr.lit 0
]),
YulStmt.if_ (YulExpr.call "iszero" [YulExpr.ident successName]) [
YulStmt.let_ rdsName (YulExpr.call "returndatasize" []),
YulStmt.expr (YulExpr.call "returndatacopy" [
YulExpr.lit 0, YulExpr.lit 0, YulExpr.ident rdsName
]),
YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.ident rdsName])
]
]
]

theorem selfDelegateMulticallBytesBody_empty_param :
selfDelegateMulticallBytesBody "" "__mc_ptr" "__mc_i" "__mc_success" "__mc_rds" =
Except.error "selfDelegateMulticallBytes: arrayParam must be non-empty" := by
rfl

/-- Generic external call with single uint256 return.
ABI-encodes `selector(args...)`, calls/staticcalls target, reverts on failure,
validates returndatasize >= 32, and binds the result.
Expand Down Expand Up @@ -374,4 +463,32 @@ def callWithValueBytesModule (bytesParam : String) : ExternalCallModule where
def callWithValueBytes (target value : Expr) (bytesParam : String) : Stmt :=
.ecm (callWithValueBytesModule bytesParam) [target, value]

/-- Source-level `multicall(bytes[])` helper for self-delegatecall routers.

The named parameter must be a `bytes[]` ABI parameter. The generated Yul
walks the ABI offset table, copies each element payload into memory, then
executes `delegatecall(gas(), address(), ptr, size, 0, 0)`. On failure it
forwards returndata exactly with `returndatacopy(0, 0, returndatasize())`
followed by `revert(0, returndatasize())`.

Unlike the general `Expr.delegatecall` surface, this module has no dynamic
implementation address and is intended for same-contract multicall only. -/
def selfDelegateMulticallBytesModule (arrayParam : String) : ExternalCallModule where
name := "selfDelegateMulticallBytes"
numArgs := 0
resultVars := []
writesState := true
readsState := true
axioms := ["self_delegate_multicall_bytes_revert_bubbling"]
compile := fun _ctx args => do
match args with
| [] =>
selfDelegateMulticallBytesBody arrayParam "__mc_ptr" "__mc_i" "__mc_success" "__mc_rds"
| _ =>
throw "selfDelegateMulticallBytes expects 0 arguments"

/-- Convenience constructor for self-delegatecall `multicall(bytes[])`. -/
def selfDelegateMulticallBytes (arrayParam : String) : Stmt :=
.ecm (selfDelegateMulticallBytesModule arrayParam) []

end Compiler.Modules.Calls
166 changes: 166 additions & 0 deletions Compiler/Modules/CallsTest.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,166 @@
import Compiler.Codegen
import Compiler.CompilationModel
import Compiler.CompilationModel.TrustSurface
import Compiler.Modules.Calls
import Compiler.Yul.PrettyPrint

namespace Compiler.Modules.CallsTest

open Compiler
open Compiler.CompilationModel

private def contains (haystack needle : String) : Bool :=
let h := haystack.toList
let n := needle.toList
if n.isEmpty then true
else
let rec go : List Char → Bool
| [] => false
| c :: cs =>
if (c :: cs).take n.length == n then true
else go cs
go h

private def expectTrue (label : String) (ok : Bool) : IO Unit := do
if !ok then
throw (IO.userError s!"✗ {label}")
IO.println s!"✓ {label}"

private def selectorsFor (spec : CompilationModel) : List Nat :=
List.range (spec.functions.filter (fun fn =>
!fn.isInternal && fn.name != "fallback" && fn.name != "receive")).length

private def expectCompileErrorContains (label : String)
(spec : CompilationModel) (needle : String) : IO Unit := do
match Compiler.CompilationModel.compile spec (selectorsFor spec) with
| .ok _ => throw (IO.userError s!"✗ {label}: expected compile error containing '{needle}'")
| .error err =>
if !contains err needle then
throw (IO.userError s!"✗ {label}: expected error containing '{needle}', got '{err}'")
IO.println s!"✓ {label}"

private def expectCompileToYul (label : String) (spec : CompilationModel) : IO String := do
match Compiler.CompilationModel.compile spec (selectorsFor spec) with
| .ok ir =>
IO.println s!"✓ {label}"
pure (Compiler.Yul.render (Compiler.emitYul ir))
| .error err =>
throw (IO.userError s!"✗ {label}: compile failed: {err}")

private def selfDelegateMulticallBytesSmokeSpec : CompilationModel := {
name := "SelfDelegateMulticallBytesSmoke"
fields := []
«constructor» := none
functions := [
{ name := "multicall"
params := [
{ name := "calls", ty := ParamType.array ParamType.bytes }
]
returnType := none
body := [
Compiler.Modules.Calls.selfDelegateMulticallBytes "calls",
Stmt.stop
]
}
]
}

private def selfDelegateMulticallBytesBadAritySpec : CompilationModel := {
name := "SelfDelegateMulticallBytesBadArity"
fields := []
«constructor» := none
functions := [
{ name := "bad"
params := [
{ name := "calls", ty := ParamType.array ParamType.bytes }
]
returnType := none
body := [
Stmt.ecm (Compiler.Modules.Calls.selfDelegateMulticallBytesModule "calls")
[Expr.arrayLength "calls"],
Stmt.stop
]
}
]
}

private def selfDelegateMulticallBytesEmptyParamSpec : CompilationModel := {
name := "SelfDelegateMulticallBytesEmptyParam"
fields := []
«constructor» := none
functions := [
{ name := "bad"
params := [
{ name := "calls", ty := ParamType.array ParamType.bytes }
]
returnType := none
body := [
Compiler.Modules.Calls.selfDelegateMulticallBytes "",
Stmt.stop
]
}
]
}

private def selfDelegateMulticallBytesViewRejectedSpec : CompilationModel := {
name := "SelfDelegateMulticallBytesViewRejected"
fields := []
«constructor» := none
functions := [
{ name := "multicall"
params := [
{ name := "calls", ty := ParamType.array ParamType.bytes }
]
returnType := none
isView := true
body := [
Compiler.Modules.Calls.selfDelegateMulticallBytes "calls",
Stmt.stop
]
}
]
}

unsafe def runTests : IO Unit := do
let yul ←
expectCompileToYul "self-delegate multicall bytes smoke spec" selfDelegateMulticallBytesSmokeSpec
expectTrue "self-delegate multicall walks bytes[] calldata offsets"
(contains yul "for {" &&
contains yul "let __mc_i := 0" &&
contains yul "lt(__mc_i, calls_length)" &&
contains yul "let __mc_rel_offset := calldataload(add(calls_data_offset, mul(__mc_i, 32)))" &&
contains yul "if lt(__mc_rel_offset, mul(calls_length, 32)) {" &&
contains yul "if gt(__mc_rel_offset, sub(not(0), calls_data_offset)) {" &&
contains yul "let __mc_head_offset := add(calls_data_offset, __mc_rel_offset)" &&
contains yul "let __mc_data_size := calldataload(__mc_head_offset)" &&
contains yul "let __mc_data_offset := add(__mc_head_offset, 32)")
expectTrue "self-delegate multicall copies each bytes payload and delegatecalls address()"
(contains yul "calldatacopy(__mc_ptr, __mc_data_offset, __mc_data_size)" &&
contains yul "delegatecall(gas(), address(), __mc_ptr, __mc_data_size, 0, 0)")
expectTrue "self-delegate multicall forwards revert returndata exactly"
(contains yul "let __mc_rds := returndatasize()" &&
contains yul "returndatacopy(0, 0, __mc_rds)" &&
contains yul "revert(0, __mc_rds)")
expectCompileErrorContains
"self-delegate multicall ECM rejects invalid argument counts"
selfDelegateMulticallBytesBadAritySpec
"uses ECM 'selfDelegateMulticallBytes' with 1 arguments but it expects 0"
expectCompileErrorContains
"self-delegate multicall rejects empty parameter names"
selfDelegateMulticallBytesEmptyParamSpec
"selfDelegateMulticallBytes: arrayParam must be non-empty"
expectCompileErrorContains
"self-delegate multicall remains rejected from view functions"
selfDelegateMulticallBytesViewRejectedSpec
"function 'multicall' is marked view but writes state"
let report := emitTrustReportJson [selfDelegateMulticallBytesSmokeSpec]
expectTrue "self-delegate multicall trust report surfaces scoped multicall assumption without proxy boundary"
(contains report "\"module\":\"selfDelegateMulticallBytes\"" &&
contains report "\"assumption\":\"self_delegate_multicall_bytes_revert_bubbling\"" &&
contains report "\"boundaryClass\":\"abiBoundary\"" &&
contains report "\"notModeledProxyUpgradeability\":[]" &&
! (contains report "\"delegatecall\""))

#eval! runTests

end Compiler.Modules.CallsTest
4 changes: 2 additions & 2 deletions TRUST_ASSUMPTIONS.md
Original file line number Diff line number Diff line change
Expand Up @@ -75,8 +75,8 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V
- **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`).

### 7. External Call Modules (ECMs)
- **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).
- **Trust**: Each module's `compile` produces correct Yul. Bug in one module doesn't affect others.
- **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`).
- **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.
- **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).
- **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.

Expand Down
7 changes: 7 additions & 0 deletions docs-site/content/edsl-api-reference.mdx
Original file line number Diff line number Diff line change
Expand Up @@ -442,9 +442,16 @@ Compiler.Modules.Calls.withReturn

Compiler.Modules.Calls.bubblingValueCall
(target value inputOffset inputSize outputOffset outputSize : Expr) : Stmt

Compiler.Modules.Calls.selfDelegateMulticallBytes
(arrayParam : String) : Stmt
```

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

### `keccak256` primitive

Expand Down
Loading
Loading