feat: checked-arithmetic helper emission (#1993 emission half) (#2028)

* Support dynamic internal helper args

* feat: allow runtime scalar custom error args

* feat: add source-shaped dynamic event proof surface

* Emit checked arithmetic helpers

* feat(Codegen): factor solidityPanicPayload for Panic(uint256) emission (#1999) (#2030)

Extract the Panic(uint256) revert payload (selector 0x4e487b71 + one ABI word
holding the panic code) into a reusable solidityPanicPayload builder so panic
emission is compiler-owned and reusable for checked-arithmetic paths; assert
the encoded code words (mstore(4, 17/18)) in the arithmetic-panic smoke test.

* feat: self-delegate multicall helper (#1997) (#2029)

* feat: add self-delegate multicall helper

* fix(verity): multicall offset-wrap bound check + documented trusted ECM (#2029)

* fix(merge): drop duplicate internal-call helpers from Compile.lean

The #1997 refactor moved findInternalFunctionForCall?, compileInternalCallArg,
compileInternalCallArgsWithParams, and compileInternalCallArgs into
ExpressionCompile.lean. The merge of origin/main kept the stale copies in
Compile.lean too, producing "already been declared" errors. Remove the stale
copies; ExpressionCompile.lean is the single source.

* fix(proofs): set noCheckedArithmetic on scalarEventSmoke supported spec

The merge brought in main's scalar-events supported-spec smoke test, which
the SupportedSpecSurfaceWithScalarEvents struct now requires to discharge the
noCheckedArithmetic obligation added in this PR. Prove it by simp over the
spec definitions.

* fix(merge): restore CompilationModelFeatureTest content dropped by botched origin/main merge

The eb9fadb merge of origin/main into task/1993a-checked-arith dropped ~3385
lines of origin/main test content and left the namespace structure broken
(InternalHelperDynamicArgs never closed), causing the compiler-regressions CI
job to fail with a parse error. Restore origin/main's full feature-test file and
re-graft task/1993a's unique checked-arithmetic helper assertions on top, so the
union of both sides' test cases is preserved.

Author: Th0rgal

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 |

Compiler/Codegen.lean

@@ -50,11 +50,13 @@ private def patchBackend : Compiler.CodegenCommon.PatchBackend :=
         patchReport := mergedPatchReport } }
 
 def emitYulWithOptions (contract : IRContract) (options : YulEmitOptions) : YulObject :=
-  Compiler.CodegenCommon.emitYulWithOptions patchBackend contract options
+  Compiler.CodegenCommon.optimizeCheckedArithmeticObjectIfAvailable contract
+    (Compiler.CodegenCommon.emitYulWithOptions patchBackend contract options)
 
 def emitYulWithOptionsReport (contract : IRContract) (options : YulEmitOptions) :
     YulObject × Yul.PatchPassReport :=
-  Compiler.CodegenCommon.emitYulWithOptionsReport patchBackend contract options
+  let report := Compiler.CodegenCommon.emitYulWithOptionsReport patchBackend contract options
+  (Compiler.CodegenCommon.optimizeCheckedArithmeticObjectIfAvailable contract report.1, report.2)
 
 /-- Regression guard:
     expression/statement/block patching remains runtime-scoped (deploy is unchanged),

Compiler/CodegenCommon.lean

@@ -1,4 +1,6 @@
 import Compiler.Constants
+import Compiler.CompilationModel.AbiHelpers
+import Compiler.CompilationModel.DynamicData
 import Compiler.IR
 import Compiler.Yul.PrettyPrint
 import Compiler.Yul.PatchFramework
@@ -7,6 +9,7 @@ import Verity.Core.Intrinsics
 namespace Compiler.CodegenCommon
 
 open Compiler.Constants (selectorShift)
+open Compiler.CompilationModel
 open Compiler.Yul
 
 inductive BackendProfile where
@@ -144,6 +147,133 @@ def buildSwitch
       [YulStmt.switch selectorExpr cases (some defaultCase)]
   ]
 
+private def yulExprSame (a b : YulExpr) : Bool :=
+  toString (repr a) == toString (repr b)
+
+private def yulStmtListSame (a b : List YulStmt) : Bool :=
+  toString (repr a) == toString (repr b)
+
+private def isRevertMessageBody (message : String) (body : List YulStmt) : Bool :=
+  yulStmtListSame body (revertWithMessage message)
+
+private def checkedAddFailCond (a b : YulExpr) : YulExpr :=
+  YulExpr.call "lt" [YulExpr.call "add" [a, b], a]
+
+private def checkedSubFailCond (a b : YulExpr) : YulExpr :=
+  YulExpr.call "lt" [a, b]
+
+private def checkedMulFailCond (a b : YulExpr) : YulExpr :=
+  YulExpr.call "iszero" [
+    YulExpr.call "or" [
+      YulExpr.call "iszero" [YulExpr.call "iszero" [
+        YulExpr.call "eq" [b, YulExpr.lit 0]
+      ]],
+      YulExpr.call "iszero" [YulExpr.call "iszero" [
+        YulExpr.call "eq" [
+          YulExpr.call "div" [YulExpr.call "mul" [a, b], b],
+          a
+        ]
+      ]]
+    ]
+  ]
+
+private def checkedDivFailCond (b : YulExpr) : YulExpr :=
+  YulExpr.call "iszero" [YulExpr.call "iszero" [
+    YulExpr.call "eq" [b, YulExpr.lit 0]
+  ]]
+
+private def checkedArithmeticReplacement? (prev cur : YulStmt) : Option YulStmt :=
+  match prev, cur with
+  | YulStmt.if_ cond body, YulStmt.let_ name (YulExpr.call "add" [a, b]) =>
+      if yulExprSame cond (checkedAddFailCond a b) &&
+          isRevertMessageBody "Panic(0x11): arithmetic overflow" body then
+        some (YulStmt.let_ name (YulExpr.call checkedAddUint256HelperName [a, b]))
+      else
+        none
+  | YulStmt.if_ cond body, YulStmt.let_ name (YulExpr.call "sub" [a, b]) =>
+      if yulExprSame cond (checkedSubFailCond a b) &&
+          isRevertMessageBody "Panic(0x11): arithmetic underflow" body then
+        some (YulStmt.let_ name (YulExpr.call checkedSubUint256HelperName [a, b]))
+      else
+        none
+  | YulStmt.if_ cond body, YulStmt.let_ name (YulExpr.call "mul" [a, b]) =>
+      if yulExprSame cond (checkedMulFailCond a b) &&
+          isRevertMessageBody "Panic(0x11): arithmetic overflow" body then
+        some (YulStmt.let_ name (YulExpr.call checkedMulUint256HelperName [a, b]))
+      else
+        none
+  | YulStmt.if_ cond body, YulStmt.let_ name (YulExpr.call "div" [a, b]) =>
+      if yulExprSame cond (checkedDivFailCond b) &&
+          isRevertMessageBody "Panic(0x12): division by zero" body then
+        some (YulStmt.let_ name (YulExpr.call checkedDivUint256HelperName [a, b]))
+      else
+        none
+  | _, _ => none
+
+mutual
+
+private def optimizeCheckedArithmeticStmtFuel : Nat → YulStmt → YulStmt
+  | 0, stmt => stmt
+  | fuel + 1, YulStmt.if_ cond body =>
+      YulStmt.if_ cond (optimizeCheckedArithmeticStmtsFuel fuel body)
+  | fuel + 1, YulStmt.for_ init cond post body =>
+      YulStmt.for_
+        (optimizeCheckedArithmeticStmtsFuel fuel init)
+        cond
+        (optimizeCheckedArithmeticStmtsFuel fuel post)
+        (optimizeCheckedArithmeticStmtsFuel fuel body)
+  | fuel + 1, YulStmt.switch expr cases default =>
+      YulStmt.switch expr
+        (cases.map fun (tag, body) => (tag, optimizeCheckedArithmeticStmtsFuel fuel body))
+        (default.map (optimizeCheckedArithmeticStmtsFuel fuel))
+  | fuel + 1, YulStmt.block stmts =>
+      YulStmt.block (optimizeCheckedArithmeticStmtsFuel fuel stmts)
+  | fuel + 1, YulStmt.funcDef name params rets body =>
+      YulStmt.funcDef name params rets (optimizeCheckedArithmeticStmtsFuel fuel body)
+  | _fuel + 1, stmt => stmt
+
+private def optimizeCheckedArithmeticStmtsFuel : Nat → List YulStmt → List YulStmt
+  | 0, stmts => stmts
+  | _fuel + 1, [] => []
+  | fuel + 1, [stmt] => [optimizeCheckedArithmeticStmtFuel fuel stmt]
+  | fuel + 1, prev :: cur :: rest =>
+      let prev' := optimizeCheckedArithmeticStmtFuel fuel prev
+      let cur' := optimizeCheckedArithmeticStmtFuel fuel cur
+      match checkedArithmeticReplacement? prev' cur' with
+      | some replacement => replacement :: optimizeCheckedArithmeticStmtsFuel fuel rest
+      | none => prev' :: optimizeCheckedArithmeticStmtsFuel fuel (cur :: rest)
+
+end
+
+private def yulStmtListFuel (stmts : List YulStmt) : Nat :=
+  (toString (repr stmts)).length + 1
+
+private def optimizeCheckedArithmeticStmts (stmts : List YulStmt) : List YulStmt :=
+  optimizeCheckedArithmeticStmtsFuel (yulStmtListFuel stmts) stmts
+
+private def internalHelperNamed (name : String) : YulStmt → Bool
+  | YulStmt.funcDef fnName _ _ _ => fnName == name
+  | _ => false
+
+private def hasCheckedArithmeticHelpers (contract : IRContract) : Bool :=
+  contract.internalFunctions.any (internalHelperNamed checkedAddUint256HelperName) &&
+    contract.internalFunctions.any (internalHelperNamed checkedSubUint256HelperName) &&
+    contract.internalFunctions.any (internalHelperNamed checkedMulUint256HelperName) &&
+    contract.internalFunctions.any (internalHelperNamed checkedDivUint256HelperName)
+
+private def optimizeCheckedArithmeticIfAvailable (contract : IRContract) (stmts : List YulStmt) :
+    List YulStmt :=
+  if hasCheckedArithmeticHelpers contract then
+    optimizeCheckedArithmeticStmts stmts
+  else
+    stmts
+
+def optimizeCheckedArithmeticObjectIfAvailable (contract : IRContract) (object : YulObject) :
+    YulObject :=
+  { object with
+    deployCode := optimizeCheckedArithmeticIfAvailable contract object.deployCode
+    runtimeCode := optimizeCheckedArithmeticIfAvailable contract object.runtimeCode }
+
 def runtimeCode (contract : IRContract) : List YulStmt :=
   let mapping := if contract.usesMapping then [mappingSlotFuncAt 0] else []
   let internals := contract.internalFunctions

Compiler/CompilationModel/Dispatch.lean

@@ -515,11 +515,13 @@ def validateCompileInputs (spec : CompilationModel) (selectors : List Nat)
   let mulDiv512HelpersRequired := contractUsesMulDiv512 spec
   let storageArrayHelpersRequired := contractUsesStorageArrayElement spec
   let dynamicBytesEqHelpersRequired := contractUsesDynamicBytesEq spec
+  let checkedArithmeticHelpersRequired := contractUsesCheckedArithmetic spec
   match firstReservedExternalCollision
       spec mappingHelpersRequired arrayHelpersRequired arrayElementWordHelpersRequired
         paramDynamicHeadWordHelpersRequired
         mulDiv512HelpersRequired
-        storageArrayHelpersRequired dynamicBytesEqHelpersRequired with
+        storageArrayHelpersRequired dynamicBytesEqHelpersRequired
+        checkedArithmeticHelpersRequired with
   | some name =>
       if name.startsWith internalFunctionPrefix then
         throw s!"Compilation error: external declaration '{name}' uses reserved prefix '{internalFunctionPrefix}' ({issue756Ref})."
@@ -562,6 +564,7 @@ def compileValidatedCore (spec : CompilationModel) (selectors : List Nat) : Exce
   let mulDiv512HelpersRequired := contractUsesMulDiv512 spec
   let storageArrayHelpersRequired := contractUsesStorageArrayElement spec
   let dynamicBytesEqHelpersRequired := contractUsesDynamicBytesEq spec
+  let checkedArithmeticHelpersRequired := contractUsesCheckedArithmetic spec
   let fallbackSpec ← pickUniqueFunctionByName "fallback" spec.functions
   let receiveSpec ← pickUniqueFunctionByName "receive" spec.functions
   let functions ← (externalFns.zip selectors).mapM fun entry =>
@@ -627,6 +630,17 @@ def compileValidatedCore (spec : CompilationModel) (selectors : List Nat) : Exce
       [dynamicBytesEqCalldataHelper, dynamicBytesEqMemoryHelper]
     else
       []
+  let checkedArithmeticHelpers :=
+    if checkedArithmeticHelpersRequired then
+      [ panicError0x11Helper
+      , panicError0x12Helper
+      , checkedAddUint256Helper
+      , checkedSubUint256Helper
+      , checkedMulUint256Helper
+      , checkedDivUint256Helper
+      ]
+    else
+      []
   let fallbackEntrypoint ← fallbackSpec.mapM (compileSpecialEntrypoint fields spec.events spec.errors spec.adtTypes internalFns)
   let receiveEntrypoint ← receiveSpec.mapM (compileSpecialEntrypoint fields spec.events spec.errors spec.adtTypes internalFns)
   return {
@@ -637,7 +651,7 @@ def compileValidatedCore (spec : CompilationModel) (selectors : List Nat) : Exce
     fallbackEntrypoint := fallbackEntrypoint
     receiveEntrypoint := receiveEntrypoint
     usesMapping := mappingHelpersRequired
-    internalFunctions := arrayElementHelpers ++ storageArrayElementHelpers ++ dynamicBytesEqHelpers ++ internalFuncDefs
+    internalFunctions := arrayElementHelpers ++ storageArrayElementHelpers ++ dynamicBytesEqHelpers ++ checkedArithmeticHelpers ++ internalFuncDefs
   }
 
 /-- Compile a `CompilationModel` to an `IRContract`.

Compiler/CompilationModel/DynamicData.lean

@@ -99,6 +99,87 @@ def dynamicBytesEqCalldataHelperName : String :=
 def dynamicBytesEqMemoryHelperName : String :=
   "__verity_dynamic_bytes_eq_memory"
 
+def checkedAddUint256HelperName : String :=
+  "checked_add_t_uint256"
+
+def checkedSubUint256HelperName : String :=
+  "checked_sub_t_uint256"
+
+def checkedMulUint256HelperName : String :=
+  "checked_mul_t_uint256"
+
+def checkedDivUint256HelperName : String :=
+  "checked_div_t_uint256"
+
+def panicError0x11HelperName : String :=
+  "panic_error_0x11"
+
+def panicError0x12HelperName : String :=
+  "panic_error_0x12"
+
+/-- ABI payload for Solidity's built-in `Panic(uint256)` error.
+
+    The payload is exactly 36 bytes:
+    4-byte selector `0x4e487b71` followed by one ABI word containing `code`. -/
+def solidityPanicPayload (code : Nat) : List YulStmt :=
+  [
+    YulStmt.expr (YulExpr.call "mstore" [
+      YulExpr.lit 0,
+      YulExpr.call "shl" [YulExpr.lit 224, YulExpr.hex 0x4e487b71]
+    ]),
+    YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 4, YulExpr.lit code]),
+    YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 36])
+  ]
+
+def panicErrorHelper (helperName : String) (code : Nat) : YulStmt :=
+  YulStmt.funcDef helperName [] [] (solidityPanicPayload code)
+
+def panicError0x11Helper : YulStmt :=
+  panicErrorHelper panicError0x11HelperName 0x11
+
+def panicError0x12Helper : YulStmt :=
+  panicErrorHelper panicError0x12HelperName 0x12
+
+def checkedAddUint256Helper : YulStmt :=
+  YulStmt.funcDef checkedAddUint256HelperName ["x", "y"] ["sum"] [
+    YulStmt.assign "sum" (YulExpr.call "add" [YulExpr.ident "x", YulExpr.ident "y"]),
+    YulStmt.if_ (YulExpr.call "gt" [YulExpr.ident "x", YulExpr.ident "sum"]) [
+      YulStmt.expr (YulExpr.call panicError0x11HelperName [])
+    ]
+  ]
+
+def checkedSubUint256Helper : YulStmt :=
+  YulStmt.funcDef checkedSubUint256HelperName ["x", "y"] ["diff"] [
+    YulStmt.if_ (YulExpr.call "gt" [YulExpr.ident "y", YulExpr.ident "x"]) [
+      YulStmt.expr (YulExpr.call panicError0x11HelperName [])
+    ],
+    YulStmt.assign "diff" (YulExpr.call "sub" [YulExpr.ident "x", YulExpr.ident "y"])
+  ]
+
+def checkedMulUint256Helper : YulStmt :=
+  YulStmt.funcDef checkedMulUint256HelperName ["x", "y"] ["product"] [
+    YulStmt.assign "product" (YulExpr.call "mul" [YulExpr.ident "x", YulExpr.ident "y"]),
+    YulStmt.if_ (YulExpr.call "iszero" [
+      YulExpr.call "or" [
+        YulExpr.call "iszero" [YulExpr.ident "x"],
+        YulExpr.call "eq" [
+          YulExpr.call "div" [YulExpr.ident "product", YulExpr.ident "x"],
+          YulExpr.ident "y"
+        ]
+      ]
+    ]) [
+      YulStmt.expr (YulExpr.call panicError0x11HelperName [])
+    ]
+  ]
+
+def checkedDivUint256Helper : YulStmt :=
+  YulStmt.funcDef checkedDivUint256HelperName ["x", "y"] ["quotient"] [
+    YulStmt.if_ (YulExpr.call "iszero" [YulExpr.ident "y"]) [
+      YulStmt.expr (YulExpr.call panicError0x12HelperName [])
+    ],
+    YulStmt.assign "quotient" (YulExpr.call "div" [YulExpr.ident "x", YulExpr.ident "y"])
+  ]
+
 private def checkedArrayElementHelper (helperName loadOp : String) : YulStmt :=
   YulStmt.funcDef helperName ["data_offset", "length", "index"] ["word"] [
     YulStmt.if_ (YulExpr.call "iszero" [

Compiler/CompilationModel/TrustSurface.lean

@@ -789,7 +789,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"

Compiler/CompilationModel/UsageAnalysis.lean

@@ -62,6 +62,51 @@ termination_by bs => sizeOf bs
 decreasing_by all_goals simp_wf; all_goals omega
 end
 
+private def isCheckedArithmeticPanicMessage (message : String) : Bool :=
+  message == "Panic(0x11): arithmetic overflow" ||
+    message == "Panic(0x11): arithmetic underflow" ||
+    message == "Panic(0x12): division by zero"
+
+mutual
+
+def stmtMayUseCheckedArithmetic : Stmt → Bool
+  | Stmt.require _ message =>
+      isCheckedArithmeticPanicMessage message
+  | Stmt.ite _ thenBranch elseBranch =>
+      stmtListMayUseCheckedArithmetic thenBranch ||
+        stmtListMayUseCheckedArithmetic elseBranch
+  | Stmt.forEach _ _ body =>
+      stmtListMayUseCheckedArithmetic body
+  | Stmt.unsafeBlock _ body =>
+      stmtListMayUseCheckedArithmetic body
+  | Stmt.matchAdt _ _ branches =>
+      matchBranchesMayUseCheckedArithmetic branches
+  | _ => false
+termination_by s => sizeOf s
+decreasing_by all_goals simp_wf; all_goals omega
+
+def stmtListMayUseCheckedArithmetic : List Stmt → Bool
+  | [] => false
+  | stmt :: rest =>
+      stmtMayUseCheckedArithmetic stmt ||
+        stmtListMayUseCheckedArithmetic rest
+termination_by stmts => sizeOf stmts
+decreasing_by all_goals simp_wf; all_goals omega
+
+def matchBranchesMayUseCheckedArithmetic : List (String × List String × List Stmt) → Bool
+  | [] => false
+  | (_, _, body) :: rest =>
+      stmtListMayUseCheckedArithmetic body ||
+        matchBranchesMayUseCheckedArithmetic rest
+termination_by branches => sizeOf branches
+decreasing_by all_goals simp_wf; all_goals omega
+
+end
+
+def contractUsesCheckedArithmetic (spec : CompilationModel) : Bool :=
+  (spec.constructor.map (fun ctor => stmtListMayUseCheckedArithmetic ctor.body) |>.getD false) ||
+    spec.functions.any (fun fn => stmtListMayUseCheckedArithmetic fn.body)
+
 mutual
 def exprUsesArrayElementKind (includePlain includeWord : Bool) : Expr → Bool
   | Expr.arrayElement _ index | Expr.memoryArrayElement _ index =>