diff --git a/AXIOMS.md b/AXIOMS.md index f70aac61c..0718453c2 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -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 | diff --git a/Compiler/CompilationModel/TrustSurface.lean b/Compiler/CompilationModel/TrustSurface.lean index 4e59c7316..cec5f31db 100644 --- a/Compiler/CompilationModel/TrustSurface.lean +++ b/Compiler/CompilationModel/TrustSurface.lean @@ -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" diff --git a/Compiler/Modules/Calls.lean b/Compiler/Modules/Calls.lean index 0c29c58de..16f73f68c 100644 --- a/Compiler/Modules/Calls.lean +++ b/Compiler/Modules/Calls.lean @@ -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 @@ -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"]), + 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. @@ -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 diff --git a/Compiler/Modules/CallsTest.lean b/Compiler/Modules/CallsTest.lean new file mode 100644 index 000000000..e869b3732 --- /dev/null +++ b/Compiler/Modules/CallsTest.lean @@ -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 diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md index 0864de04e..008e24c6e 100644 --- a/TRUST_ASSUMPTIONS.md +++ b/TRUST_ASSUMPTIONS.md @@ -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 `, 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. diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx index 17ed80b64..691bf3dcc 100644 --- a/docs-site/content/edsl-api-reference.mdx +++ b/docs-site/content/edsl-api-reference.mdx @@ -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 diff --git a/docs/EXTERNAL_CALL_MODULES.md b/docs/EXTERNAL_CALL_MODULES.md index cf79c0798..04aaf3422 100644 --- a/docs/EXTERNAL_CALL_MODULES.md +++ b/docs/EXTERNAL_CALL_MODULES.md @@ -143,6 +143,7 @@ Standard modules ship in `Compiler/Modules/`: | `Calls.callWithValue` | Parameterized | Generic `call{value:v}` over an already prepared calldata slice, with revert bubbling | `generic_call_with_value_interface` | | `Calls.callWithValueBytes` | Parameterized | Generic `call{value:v}` over a `bytes` parameter, with revert bubbling | `generic_call_with_value_interface` | | `Calls.bubblingValueCall` / `Calls.bubblingValueCallNoOutput` | `call{value: v}(data)` shape | Generic low-level value call over caller-provided memory slices; bubbles exact revert returndata on failure | `generic_low_level_value_call_interface` | +| `Calls.selfDelegateMulticallBytes` | Parameterized | Self-delegatecall `multicall(bytes[])`; checks each bytes-array element offset, copies payload calldata, delegatecalls `address()`, and bubbles exact revert returndata | `self_delegate_multicall_bytes_revert_bubbling` | | `Create2SSTORE2.create2Deploy` | Parameterized | `create2(value, offset, size, salt)` over caller-prepared initcode | `create2_initcode_layout`, `create2_address_derivation` | | `Create2SSTORE2.sstore2ReadCode` | Parameterized | `extcodecopy(pointer, dest, codeOffset, size)` for code-as-data reads | `sstore2_pointer_code_layout` | @@ -196,6 +197,21 @@ inputSize`. It is backed by the four-argument `bubblingValueCallNoOutput` module name with the same `generic_low_level_value_call_interface` assumption. +### Self-Delegate Multicall + +`Compiler.Modules.Calls.selfDelegateMulticallBytes "calls"` is the standard +source-level helper for Solidity-style `multicall(bytes[] calldata calls)` when +each payload is executed against the current contract with the current storage +context. It expects a named `bytes[]` ABI parameter, walks the checked dynamic +array offset table, copies each element payload to the free-memory region, and +emits `delegatecall(gas(), address(), ptr, size, 0, 0)`. + +On failure, the helper copies `returndatasize()` bytes from returndata offset +zero to memory offset zero and reverts with that exact payload. The helper does +not expose an implementation address, so trust reports surface it as the +`selfDelegateMulticallBytes` ECM assumption rather than as a general +proxy/upgradeability `delegatecall` mechanic. + ### ERC-20 Optional Return Policies `Compiler.Modules.ERC20.safeTransfer`, `safeTransferFrom`, and `safeApprove` diff --git a/docs/INTERPRETER_FEATURE_MATRIX.md b/docs/INTERPRETER_FEATURE_MATRIX.md index cda31176d..b7cc91e59 100644 --- a/docs/INTERPRETER_FEATURE_MATRIX.md +++ b/docs/INTERPRETER_FEATURE_MATRIX.md @@ -127,9 +127,12 @@ including `Compiler.Modules.Calls.bubblingValueCall`, which lowers Solidity-style `call{value: v}(data)` wrappers to Yul `call` and forwards exact revert returndata on failure. `bubblingValueCallNoOutputModule` exposes the same no-output adapter/router shape directly to `verity_contract` `ecmDo` call -sites. These mechanics remain explicit trust-report surfaces: Verity models the -generic call choreography, while package-specific callee behavior and protocol -assumptions belong in dependent packages. +sites. `Compiler.Modules.Calls.selfDelegateMulticallBytes` adds the scoped +`multicall(bytes[])` shape for same-contract `delegatecall(address(), data)` +iteration with exact revert bubbling. These mechanics remain explicit +trust-report surfaces: Verity models the generic call choreography, while +package-specific callee behavior and protocol assumptions belong in dependent +packages. The standard ECM library also includes static-word packed hashing helpers: `Compiler.Modules.Hashing.abiEncodePackedWords` and diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 844ba993d..c71962960 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -118,6 +118,7 @@ Recent progress for low-level calls + returndata handling (`#622`): - `CompilationModel.Expr.returndataSize`, `Stmt.returndataCopy`, and `Stmt.revertReturndata` now provide first-class returndata access and revert-data forwarding without raw Yul builtin injection. - `CompilationModel.Expr.returndataOptionalBoolAt(outOffset)` now provides a first-class ERC20 compatibility helper for optional return-data bool decoding (`returndatasize()==0 || (returndatasize()==32 && mload(outOffset)==1)`), so low-level token call acceptance paths can be expressed without raw Yul builtins. - `Compiler.Modules.Calls.callWithValue` now provides a standard assumed-status ECM for generic `call{value:v}` over an already prepared calldata slice, with revert-data bubbling. `Calls.callWithValueBytes` adds the higher-level `(target, value, data)` wrapper for `Bytes` payloads by copying the payload to memory before calling. This covers adapter/router patterns that need arbitrary calldata and ETH value transfer while keeping the trust surface visible in reports, with distinct `callWithValue` / `callWithValueBytes` module names in audit manifests. +- `Compiler.Modules.Calls.selfDelegateMulticallBytes` now provides the scoped `multicall(bytes[])` surface for same-contract delegatecall loops: it checks the dynamic bytes-array offset table, copies each element payload, executes `delegatecall(gas(), address(), ptr, size, 0, 0)`, and bubbles exact revert data. Trust reports record the named ECM assumption instead of the generic proxy/upgradeability delegatecall boundary. - `verity-compiler --trust-report ` now emits a machine-readable per-contract trust surface covering low-level mechanics usage, raw `rawLog` event emission, linked external assumptions, ECM axioms, explicit `proved` / `assumed` / `unchecked` proof-status buckets for foreign surfaces, constructor/function-level `usageSites`, site-localized `localObligations` for unsafe/refinement escape hatches, and dedicated `notModeledEventEmission` / `notModeledProxyUpgradeability` / `partiallyModeledLinearMemoryMechanics` / `partiallyModeledRuntimeIntrospection` slices for the current event, proxy/upgradeability, memory/ABI, and runtime-context proof gaps; `--verbose` now includes matching human-readable summaries, `--deny-unchecked-dependencies` upgrades unchecked foreign usage from a warning to a fail-closed verification gate with site-localized diagnostics, `--deny-assumed-dependencies` provides a proof-strict gate for any remaining assumed or unchecked foreign dependency, `--deny-axiomatized-primitives` fails closed on contracts that still rely on axiomatized primitives such as `keccak256`, `--deny-local-obligations` fails closed on any undischarged local unsafe/refinement obligation, `--deny-linear-memory-mechanics` fails closed on contracts that still rely on partially modeled linear-memory mechanics, `--deny-event-emission` fails closed on raw `rawLog` event emission, `--deny-low-level-mechanics` fails closed on first-class low-level call / returndata usage, `--deny-proxy-upgradeability` fails closed on `delegatecall`-based proxy / upgradeability mechanics tracked under issue `#1420`, and `--deny-runtime-introspection` does the same for partially modeled runtime-introspection primitives. - Raw `Expr.externalCall` interop names for low-level/builtin opcodes remain fail-fast rejected, preserving explicit migration diagnostics while the first-class surface continues to expand.