Document and test requireSomeUintError

Compiler/MacroCustomErrorFeatureTest.lean

@@ -170,4 +170,43 @@ example : checkAddExecutableRevertsOnOverflow = true := by native_decide
 
 end RequireSomeUintErrorSmoke
 
+/--
+error: unknown custom error 'MissingOverflow'
+-/
+#guard_msgs in
+verity_contract RequireSomeUintErrorUnknownErrorRejected where
+  storage
+  errors
+    error AddOverflow ()
+
+  function bad (a : Uint256, b : Uint256) : Uint256 := do
+    let result ← requireSomeUintError (safeAdd a b) MissingOverflow()
+    return result
+
+/--
+error: custom error 'MulOverflow' expects 2 args, got 1
+-/
+#guard_msgs in
+verity_contract RequireSomeUintErrorWrongArityRejected where
+  storage
+  errors
+    error MulOverflow (Uint256, Uint256)
+
+  function bad (a : Uint256, b : Uint256) : Uint256 := do
+    let result ← requireSomeUintError (safeMul a b) MulOverflow(a)
+    return result
+
+/--
+error: unsupported requireSomeUintError source; expected safeAdd, safeSub, safeMul, or safeDiv
+-/
+#guard_msgs in
+verity_contract RequireSomeUintErrorInvalidSourceRejected where
+  storage
+  errors
+    error AddOverflow ()
+
+  function bad (a : Uint256) : Uint256 := do
+    let result ← requireSomeUintError a AddOverflow()
+    return result
+
 end Compiler.MacroCustomErrorFeatureTest

Verity/Macro/Translate.lean

@@ -5622,111 +5622,63 @@ private def translateSafeRequireBind
     (locals : Array TypedLocal)
     (varName : String)
     (rhs : Term) : CommandElabM (Option (Array Term)) := do
+  let translateSafeUintGuardAndValue (optExpr : Term) (label : String) :
+      CommandElabM (Term × Term) := do
+    match stripParens optExpr with
+    | `(term| safeAdd $a:term $b:term) =>
+        let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
+        let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
+        let valueExpr : Term ← `(Compiler.CompilationModel.Expr.add $aExpr $bExpr)
+        let guardExpr : Term ← `(Compiler.CompilationModel.Expr.ge $valueExpr $aExpr)
+        pure (guardExpr, valueExpr)
+    | `(term| safeSub $a:term $b:term) =>
+        let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
+        let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
+        let valueExpr : Term ← `(Compiler.CompilationModel.Expr.sub $aExpr $bExpr)
+        let guardExpr : Term ← `(Compiler.CompilationModel.Expr.ge $aExpr $bExpr)
+        pure (guardExpr, valueExpr)
+    | `(term| safeMul $a:term $b:term) =>
+        let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
+        let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
+        let valueExpr : Term ← `(Compiler.CompilationModel.Expr.mul $aExpr $bExpr)
+        let zeroExpr : Term ← `(Compiler.CompilationModel.Expr.literal 0)
+        let divisorZeroExpr : Term ← `(Compiler.CompilationModel.Expr.eq $bExpr $zeroExpr)
+        let quotientExpr : Term ← `(Compiler.CompilationModel.Expr.div $valueExpr $bExpr)
+        let noOverflowExpr : Term ← `(Compiler.CompilationModel.Expr.eq $quotientExpr $aExpr)
+        let guardExpr : Term ← `(Compiler.CompilationModel.Expr.logicalOr $divisorZeroExpr $noOverflowExpr)
+        pure (guardExpr, valueExpr)
+    | `(term| safeDiv $a:term $b:term) =>
+        let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
+        let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
+        let valueExpr : Term ← `(Compiler.CompilationModel.Expr.div $aExpr $bExpr)
+        let zeroExpr : Term ← `(Compiler.CompilationModel.Expr.literal 0)
+        let guardExpr : Term ←
+          `(Compiler.CompilationModel.Expr.logicalNot
+              (Compiler.CompilationModel.Expr.eq $bExpr $zeroExpr))
+        pure (guardExpr, valueExpr)
+    | _ =>
+        throwErrorAt rhs s!"unsupported {label} source; expected safeAdd, safeSub, safeMul, or safeDiv"
   let rhs := stripParens rhs
   match rhs with
   | `(term| requireSomeUint $optExpr:term $msg:term) =>
       let msgLit ← strTerm <$> expectStringLiteral msg
-      let optExpr := stripParens optExpr
-      match optExpr with
-      | `(term| safeAdd $a:term $b:term) =>
-          let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
-          let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
-          let valueExpr : Term ← `(Compiler.CompilationModel.Expr.add $aExpr $bExpr)
-          let guardExpr : Term ← `(Compiler.CompilationModel.Expr.ge $valueExpr $aExpr)
-          pure (some #[
-            (← `(Compiler.CompilationModel.Stmt.require $guardExpr $msgLit)),
-            (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
-          ])
-      | `(term| safeSub $a:term $b:term) =>
-          let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
-          let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
-          let valueExpr : Term ← `(Compiler.CompilationModel.Expr.sub $aExpr $bExpr)
-          let guardExpr : Term ← `(Compiler.CompilationModel.Expr.ge $aExpr $bExpr)
-          pure (some #[
-            (← `(Compiler.CompilationModel.Stmt.require $guardExpr $msgLit)),
-            (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
-          ])
-      | `(term| safeMul $a:term $b:term) =>
-          let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
-          let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
-          let valueExpr : Term ← `(Compiler.CompilationModel.Expr.mul $aExpr $bExpr)
-          let zeroExpr : Term ← `(Compiler.CompilationModel.Expr.literal 0)
-          let divisorZeroExpr : Term ← `(Compiler.CompilationModel.Expr.eq $bExpr $zeroExpr)
-          let quotientExpr : Term ← `(Compiler.CompilationModel.Expr.div $valueExpr $bExpr)
-          let noOverflowExpr : Term ← `(Compiler.CompilationModel.Expr.eq $quotientExpr $aExpr)
-          let guardExpr : Term ← `(Compiler.CompilationModel.Expr.logicalOr $divisorZeroExpr $noOverflowExpr)
-          pure (some #[
-            (← `(Compiler.CompilationModel.Stmt.require $guardExpr $msgLit)),
-            (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
-          ])
-      | `(term| safeDiv $a:term $b:term) =>
-          let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
-          let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
-          let valueExpr : Term ← `(Compiler.CompilationModel.Expr.div $aExpr $bExpr)
-          let zeroExpr : Term ← `(Compiler.CompilationModel.Expr.literal 0)
-          let guardExpr : Term ←
-            `(Compiler.CompilationModel.Expr.logicalNot
-                (Compiler.CompilationModel.Expr.eq $bExpr $zeroExpr))
-          pure (some #[
-            (← `(Compiler.CompilationModel.Stmt.require $guardExpr $msgLit)),
-            (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
-          ])
-      | _ =>
-          throwErrorAt rhs "unsupported requireSomeUint source; expected safeAdd, safeSub, safeMul, or safeDiv"
+      let (guardExpr, valueExpr) ← translateSafeUintGuardAndValue optExpr "requireSomeUint"
+      pure (some #[
+        (← `(Compiler.CompilationModel.Stmt.require $guardExpr $msgLit)),
+        (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
+      ])
   -- Typed-error counterpart to `requireSomeUint`. The lowering mirrors the
   -- string-message variant exactly, except the guard becomes a
   -- `Stmt.requireError` emitting a 4-byte selector revert with the supplied
   -- error name and argument list.
   | `(term| requireSomeUintError $optExpr:term $errorName:ident($args,*)) =>
       let errorNameLit := strTerm (toString errorName.getId)
       let argExprs ← args.getElems.mapM (translatePureExprWithTypes fields constDecls immutableDecls params locals)
-      let optExpr := stripParens optExpr
-      match optExpr with
-      | `(term| safeAdd $a:term $b:term) =>
-          let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
-          let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
-          let valueExpr : Term ← `(Compiler.CompilationModel.Expr.add $aExpr $bExpr)
-          let guardExpr : Term ← `(Compiler.CompilationModel.Expr.ge $valueExpr $aExpr)
-          pure (some #[
-            (← `(Compiler.CompilationModel.Stmt.requireError $guardExpr $errorNameLit [ $[$argExprs],* ])),
-            (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
-          ])
-      | `(term| safeSub $a:term $b:term) =>
-          let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
-          let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
-          let valueExpr : Term ← `(Compiler.CompilationModel.Expr.sub $aExpr $bExpr)
-          let guardExpr : Term ← `(Compiler.CompilationModel.Expr.ge $aExpr $bExpr)
-          pure (some #[
-            (← `(Compiler.CompilationModel.Stmt.requireError $guardExpr $errorNameLit [ $[$argExprs],* ])),
-            (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
-          ])
-      | `(term| safeMul $a:term $b:term) =>
-          let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
-          let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
-          let valueExpr : Term ← `(Compiler.CompilationModel.Expr.mul $aExpr $bExpr)
-          let zeroExpr : Term ← `(Compiler.CompilationModel.Expr.literal 0)
-          let divisorZeroExpr : Term ← `(Compiler.CompilationModel.Expr.eq $bExpr $zeroExpr)
-          let quotientExpr : Term ← `(Compiler.CompilationModel.Expr.div $valueExpr $bExpr)
-          let noOverflowExpr : Term ← `(Compiler.CompilationModel.Expr.eq $quotientExpr $aExpr)
-          let guardExpr : Term ← `(Compiler.CompilationModel.Expr.logicalOr $divisorZeroExpr $noOverflowExpr)
-          pure (some #[
-            (← `(Compiler.CompilationModel.Stmt.requireError $guardExpr $errorNameLit [ $[$argExprs],* ])),
-            (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
-          ])
-      | `(term| safeDiv $a:term $b:term) =>
-          let aExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals a
-          let bExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals b
-          let valueExpr : Term ← `(Compiler.CompilationModel.Expr.div $aExpr $bExpr)
-          let zeroExpr : Term ← `(Compiler.CompilationModel.Expr.literal 0)
-          let guardExpr : Term ←
-            `(Compiler.CompilationModel.Expr.logicalNot
-                (Compiler.CompilationModel.Expr.eq $bExpr $zeroExpr))
-          pure (some #[
-            (← `(Compiler.CompilationModel.Stmt.requireError $guardExpr $errorNameLit [ $[$argExprs],* ])),
-            (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
-          ])
-      | _ =>
-          throwErrorAt rhs "unsupported requireSomeUintError source; expected safeAdd, safeSub, safeMul, or safeDiv"
+      let (guardExpr, valueExpr) ← translateSafeUintGuardAndValue optExpr "requireSomeUintError"
+      pure (some #[
+        (← `(Compiler.CompilationModel.Stmt.requireError $guardExpr $errorNameLit [ $[$argExprs],* ])),
+        (← `(Compiler.CompilationModel.Stmt.letVar $(strTerm varName) $valueExpr))
+      ])
   -- Solidity-0.8 default-revert arithmetic (verity#1752): `let x ← addPanic a b`
   -- lowers to the same IR as
   -- `let x ← requireSomeUint (safeAdd a b) "Panic(0x11): arithmetic overflow"`,

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

@@ -14,7 +14,7 @@ open Verity.EVM.Uint256
 open Verity.Stdlib.Math
 ```
 
-Every primitive is a `Contract α = ContractState → ContractResult α`. Read-only primitives never revert; write primitives return `success ()`; only `require` and `requireSomeUint` (and `revertError`) may emit `ContractResult.revert`. Proof lemmas for every primitive live in `Verity/Core.lean` (one `_run` lemma per primitive) and `Verity/Proofs/Stdlib/Automation.lean` / `Verity/Proofs/Stdlib/MappingAutomation.lean` (`_runState` / `_runValue` mirrors). See [Core Architecture](/core) for the model.
+Every primitive is a `Contract α = ContractState → ContractResult α`. Read-only primitives never revert; write primitives return `success ()`; only `require`, `requireSomeUint`, `requireSomeUintError`, and explicit error reverts such as `revertError` may emit `ContractResult.revert`. Proof lemmas for every primitive live in `Verity/Core.lean` (one `_run` lemma per primitive) and `Verity/Proofs/Stdlib/Automation.lean` / `Verity/Proofs/Stdlib/MappingAutomation.lean` (`_runState` / `_runValue` mirrors). See [Core Architecture](/core) for the model.
 
 ## Storage
 
@@ -48,7 +48,7 @@ def require (condition : Bool) (message : String) : Contract Unit
 def bind {α β : Type} (ma : Contract α) (f : α → Contract β) : Contract β
 ```
 
-`require false msg` is the only revert primitive. Use it in place of an explicit `revert`. `bind` short-circuits on revert and powers do-notation.
+`require false msg` emits a string-message revert. Use `revertError` or helpers such as `requireSomeUintError` when a typed custom-error revert is required. `bind` short-circuits on revert and powers do-notation.
 
 ```verity
 require (amount > 0) "amount must be nonzero"
@@ -104,13 +104,25 @@ def safeMul (a b : Uint256) : Option Uint256
 def safeDiv (a b : Uint256) : Option Uint256
 
 def requireSomeUint (opt : Option Uint256) (message : String) : Contract Uint256
+def requireSomeUintError (opt : Option Uint256) ErrorName(args...) : Contract Uint256
 
 let sum     <- requireSomeUint (safeAdd a b) "overflow"
 let product <- requireSomeUint (safeMul a b) "overflow"
 let quot    <- requireSomeUint (safeDiv a b) "division by zero"
 ```
 
-`verity_contract` lowers `requireSomeUint` over `safeAdd`/`Sub`/`Mul`/`Div` to explicit compiled `require` guards. Bare `add`/`sub`/`mul`/`div` stay wrapping.
+`verity_contract` lowers `requireSomeUint` over `safeAdd`/`Sub`/`Mul`/`Div` to explicit compiled `require` guards. Use `requireSomeUintError` with errors declared in the contract's `errors` block when checked arithmetic should revert with a typed custom error instead of a string message.
+
+```verity
+errors
+  error AddOverflow()
+  error MulOverflow(Uint256, Uint256)
+
+let sum     <- requireSomeUintError (safeAdd a b) AddOverflow()
+let product <- requireSomeUintError (safeMul sum b) MulOverflow(sum, b)
+```
+
+Bare `add`/`sub`/`mul`/`div` stay wrapping.
 
 ### Fixed-point helpers
 

docs/ARITHMETIC_PROFILE.md

@@ -85,7 +85,20 @@ For contracts that require overflow protection, the EDSL provides checked operat
 | `mulDiv512Down? a b c` | `Option Uint256` | `none` if `c = 0` or `floor(a * b / c) > 2^256 - 1`; product is unbounded |
 | `mulDiv512Up? a b c` | `Option Uint256` | `none` if `c = 0` or `ceil(a * b / c) > 2^256 - 1`; product is unbounded |
 
-Checked operations are **explicit EDSL-level constructs**. The compiler does not insert overflow checks for bare `add`/`sub`/`mul`, and bare `div` keeps EVM division-by-zero semantics. Contracts that need checked behavior must explicitly use `safeAdd`/`safeSub`/`safeMul`/`safeDiv` and handle the `Option` result. In `verity_contract`, `requireSomeUint (safeAdd ...)`, `requireSomeUint (safeSub ...)`, `requireSomeUint (safeMul ...)`, and `requireSomeUint (safeDiv ...)` lower to concrete `require` guards followed by the corresponding arithmetic result binding. The `mulDiv512...?` helpers are proof/modeling helpers for full-precision Solidity `Math.mulDiv` semantics; compiled Yul lowering for a first-class 512-bit division primitive is still tracked by #1761.
+Checked operations are **explicit EDSL-level constructs**. The compiler does not insert overflow checks for bare `add`/`sub`/`mul`, and bare `div` keeps EVM division-by-zero semantics. Contracts that need checked behavior must explicitly use `safeAdd`/`safeSub`/`safeMul`/`safeDiv` and handle the `Option` result. In `verity_contract`, `requireSomeUint (safeAdd ...)`, `requireSomeUint (safeSub ...)`, `requireSomeUint (safeMul ...)`, and `requireSomeUint (safeDiv ...)` lower to concrete `require` guards followed by the corresponding arithmetic result binding. `requireSomeUintError (safeAdd ...) ErrorName(args)` and the corresponding `safeSub`/`safeMul`/`safeDiv` forms lower to the same guards but emit typed custom errors through `requireError`. The `mulDiv512...?` helpers are proof/modeling helpers for full-precision Solidity `Math.mulDiv` semantics; compiled Yul lowering for a first-class 512-bit division primitive is still tracked by #1761.
+
+Example checked arithmetic with a typed custom error:
+
+```lean
+errors
+  error AddOverflow ()
+  error MulOverflow (Uint256, Uint256)
+
+function checked (a : Uint256, b : Uint256) : Uint256 := do
+  let sum ← requireSomeUintError (safeAdd a b) AddOverflow()
+  let product ← requireSomeUintError (safeMul sum b) MulOverflow(sum, b)
+  return product
+```
 
 For Solidity-0.8-style source models, prefer the panic wrappers
 `addPanic`/`subPanic`/`mulPanic`/`divPanic`. They are thin `Contract` wrappers
@@ -175,7 +188,7 @@ The arithmetic model is invariant across profiles. See [`docs/SOLIDITY_PARITY_PR
 
 1. Confirm that the contract's arithmetic assumptions match wrapping semantics.
 2. If overflow or division-by-zero protection is required, verify the contract uses `safeAdd`/`safeSub`/`safeMul`/`safeDiv`.
-3. Check that `requireSomeUint` is used to revert on overflow/underflow or zero divisors.
+3. Check that `requireSomeUint` or `requireSomeUintError` is used to revert on overflow/underflow or zero divisors.
 4. Review `Compiler/Proofs/ArithmeticProfile.lean` for the formal wrapping proofs.
 5. Confirm the backend profile does not affect arithmetic behavior (it doesn't).