Allow runtime scalar custom error args (#1974)

Compiler/MacroCustomErrorFeatureTest.lean

@@ -69,6 +69,44 @@ example : rejectLargeExecutableUsesRuntimeFallback = true := by native_decide
 
 end MacroCustomErrorUsageSmoke
 
+namespace MacroCustomErrorRuntimeArgSmoke
+
+verity_contract MacroCustomErrorRuntimeArgs where
+  storage
+    sentinel : Uint256 := slot 0
+
+  errors
+    error ExecutionResult(Uint256, Uint256, Address, Bool)
+
+  function failRuntime (preOpGas : Uint256, paid : Uint256, target : Address, success : Bool) : Unit := do
+    let total := add preOpGas paid
+    revertError ExecutionResult(total, add paid 1, target, success)
+
+def failRuntimeModelUsesRuntimeCustomErrorArgs : Bool :=
+  match MacroCustomErrorRuntimeArgs.failRuntime_modelBody with
+  | [Stmt.letVar "total" (Expr.add (Expr.param "preOpGas") (Expr.param "paid")),
+      Stmt.revertError "ExecutionResult"
+        [Expr.localVar "total",
+          Expr.add (Expr.param "paid") (Expr.literal 1),
+          Expr.param "target",
+          Expr.param "success"],
+      Stmt.stop] =>
+      true
+  | _ => false
+
+example : failRuntimeModelUsesRuntimeCustomErrorArgs = true := by decide
+
+def failRuntimeExecutableUsesRuntimeFallback : Bool :=
+  match MacroCustomErrorRuntimeArgs.failRuntime 3 4 9 true Verity.defaultState with
+  | .revert msg state =>
+      msg == "ExecutionResult(7, 5, 9, true)" &&
+        state.sender == Verity.defaultState.sender
+  | .success _ _ => false
+
+example : failRuntimeExecutableUsesRuntimeFallback = true := by decide
+
+end MacroCustomErrorRuntimeArgSmoke
+
 namespace RequireSomeUintErrorSmoke
 
 verity_contract RequireSomeUintErrorUsage where
@@ -196,6 +234,18 @@ verity_contract RequireSomeUintErrorWrongArityRejected where
     let result ← requireSomeUintError (safeMul a b) MulOverflow(a)
     return result
 
+/--
+error: custom error 'NeedsAmount' arg 1 in function 'bad' expects Verity.Macro.ValueType.uint256, got Verity.Macro.ValueType.bool
+-/
+#guard_msgs in
+verity_contract CustomErrorWrongArgTypeRejected where
+  storage
+  errors
+    error NeedsAmount (Uint256)
+
+  function bad (ok : Bool) : Unit := do
+    revertError NeedsAmount(ok)
+
 /--
 error: unsupported requireSomeUintError source; expected safeAdd, safeSub, safeMul, or safeDiv
 -/

Verity/Macro/Translate.lean

@@ -187,10 +187,10 @@ private partial def validateDoElemExprTypes
                   -- generic bind-source typer.
                   match stripParens rhs with
                   | `(term| requireSomeUintError $_optExpr:term $errorName:ident($args,*)) =>
-                      for arg in args.getElems do
-                        let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals arg
+                      let argTypes ← args.getElems.mapM
+                        (inferPureExprType fields constDecls immutableDecls externalDecls params locals)
                       validateCustomErrorCall ownerName (toString errorName.getId)
-                        params errorDecls args.getElems
+                        params errorDecls args.getElems argTypes
                   | _ => pure ()
                   match ← resolveTypedInterfaceCall? fields constDecls immutableDecls externalDecls params locals rhs with
                   | some (_, _, _, some retTy, _) =>
@@ -231,22 +231,22 @@ private partial def validateDoElemExprTypes
           | _ => throwErrorAt body "forEach body must be a do block"
       | `(doElem| requireError $cond:term $errorName:ident($args,*)) =>
           requireBoolType cond "requireError condition" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals cond)
-          for arg in args.getElems do
-            let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals arg
+          let argTypes ← args.getElems.mapM
+            (inferPureExprType fields constDecls immutableDecls externalDecls params locals)
           validateCustomErrorCall ownerName (toString errorName.getId)
-            params errorDecls args.getElems
+            params errorDecls args.getElems argTypes
           pure locals
       | `(doElem| revert $errorName:ident($args,*)) =>
-          for arg in args.getElems do
-            let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals arg
+          let argTypes ← args.getElems.mapM
+            (inferPureExprType fields constDecls immutableDecls externalDecls params locals)
           validateCustomErrorCall ownerName (toString errorName.getId)
-            params errorDecls args.getElems
+            params errorDecls args.getElems argTypes
           pure locals
       | `(doElem| revertError $errorName:ident($args,*)) =>
-          for arg in args.getElems do
-            let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals arg
+          let argTypes ← args.getElems.mapM
+            (inferPureExprType fields constDecls immutableDecls externalDecls params locals)
           validateCustomErrorCall ownerName (toString errorName.getId)
-            params errorDecls args.getElems
+            params errorDecls args.getElems argTypes
           pure locals
       | `(doElem| tryCatch $attempt:term $handler:term) => do
           requireWordLikeType attempt "tryCatch attempt"

Verity/Macro/Translate/Expr.lean

@@ -1541,20 +1541,33 @@ def validateDirectParamCustomErrorArg
       throwErrorAt arg
         s!"custom error '{errorName}' arg {argIdx + 1} in function '{fnName}' currently requires direct parameter reference of type {renderValueType expectedTy} on the compilation-model path"
 
+def validateCustomErrorArg
+    (arg : Term)
+    (actualTy : ValueType)
+    (fnName errorName : String)
+    (params : Array ParamDecl)
+    (expectedTy : ValueType)
+    (argIdx : Nat) : CommandElabM Unit := do
+  requireDeclaredValueType arg
+    s!"custom error '{errorName}' arg {argIdx + 1} in function '{fnName}'"
+    expectedTy actualTy
+  if customErrorRequiresDirectParamRef expectedTy then
+    validateDirectParamCustomErrorArg arg fnName errorName params expectedTy argIdx
+
 def validateCustomErrorCall
     (fnName errorName : String)
     (params : Array ParamDecl)
     (errorDecls : Array ErrorDecl)
-    (args : Array Term) : CommandElabM Unit := do
+    (args : Array Term)
+    (argTypes : Array ValueType) : CommandElabM Unit := do
   let errorDecl ←
     match errorDecls.find? (·.name == errorName) with
     | some decl => pure decl
     | none => throwError s!"unknown custom error '{errorName}'"
-  unless errorDecl.params.size == args.size do
+  unless errorDecl.params.size == args.size && args.size == argTypes.size do
     throwError s!"custom error '{errorName}' expects {errorDecl.params.size} args, got {args.size}"
-  for ((expectedTy, arg), argIdx) in errorDecl.params.zip args |>.zipIdx do
-    if customErrorRequiresDirectParamRef expectedTy then
-      validateDirectParamCustomErrorArg arg fnName errorName params expectedTy argIdx
+  for (((expectedTy, arg), actualTy), argIdx) in errorDecl.params.zip args |>.zip argTypes |>.zipIdx do
+    validateCustomErrorArg arg actualTy fnName errorName params expectedTy argIdx
 
 def throwPureContextAccessorError (stx : Syntax) (name : String) : CommandElabM α :=
   throwErrorAt stx

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

@@ -369,7 +369,7 @@ function rejectLarge (amount : Uint256) : Unit := do
     revert AmountTooLarge(amount, 100)
 ```
 
-Populates `CompilationModel.errors`; guarded and unconditional custom-error exits lower to `Stmt.requireError` / `Stmt.revertError`.
+Populates `CompilationModel.errors`; guarded and unconditional custom-error exits lower to `Stmt.requireError` / `Stmt.revertError`. Scalar ABI arguments (`Uint256`, `Address`, `Bool`, fixed-width word aliases, and newtypes over them) may be runtime expressions of the declared parameter type. Dynamic and composite payloads remain direct-parameter ABI surfaces.
 
 ## External Calls (ECM)
 

docs/ROADMAP.md

@@ -142,7 +142,7 @@ Recent progress for arithmetic modeling:
 - Internal function-pointer parameters are now supported at the `verity_contract` boundary via a compile-time monomorphization pre-pass (#1747). A higher-order helper (one with a `f : T → U` parameter) is specialized into a first-order clone for each call site that passes a statically-known internal helper in the function-pointer position: the clone drops the function-pointer parameters and substitutes the concrete helper at every call, and the call site is rewritten to target the clone. The pass runs to a fixpoint over the parsed `FunctionDecl` array before any model/IR lowering, then topologically orders the resulting helpers so the executable emission keeps callee-before-caller. Nothing downstream — CompilationModel, IR, or Yul — ever sees a function pointer, so 100% of the existing first-order machinery (and its proofs) applies unchanged, with zero overhead when no helper is higher-order. The remaining genuine restriction is dynamic dispatch: a function-pointer argument that is a runtime value, an expression, or a non-helper name still fails fast with an issue-linked diagnostic, since there is no statically-known target to specialize.
 
 Recent progress for custom errors (`#586`):
-- `Stmt.requireError` / `Stmt.revertError` now support ABI encoding for tuple/fixed-array/array/bytes payloads (including nested dynamic composites) when arguments are direct `Expr.param` references.
+- `Stmt.requireError` / `Stmt.revertError` now support ABI encoding for runtime scalar arguments and tuple/fixed-array/array/bytes payloads (including nested dynamic composites) when dynamic/composite arguments are direct `Expr.param` references.
 - Static scalar payload args remain expression-friendly (`uint256`, `address`, `bool`, `bytes32`), while composite/dynamic payload args fail fast with issue-linked diagnostics when not provided as direct parameter references.
 
 Recent progress for ABI JSON artifact generation (`#688`):