You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs-site/content/edsl-api-reference.mdx
+15-3Lines changed: 15 additions & 3 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -14,7 +14,7 @@ open Verity.EVM.Uint256
14
14
open Verity.Stdlib.Math
15
15
```
16
16
17
-
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.
17
+
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.
`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.
51
+
`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.
52
52
53
53
```verity
54
54
require (amount > 0) "amount must be nonzero"
@@ -104,13 +104,25 @@ def safeMul (a b : Uint256) : Option Uint256
let sum <- requireSomeUint (safeAdd a b) "overflow"
109
110
let product <- requireSomeUint (safeMul a b) "overflow"
110
111
let quot <- requireSomeUint (safeDiv a b) "division by zero"
111
112
```
112
113
113
-
`verity_contract` lowers `requireSomeUint` over `safeAdd`/`Sub`/`Mul`/`Div` to explicit compiled `require` guards. Bare `add`/`sub`/`mul`/`div` stay wrapping.
114
+
`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.
115
+
116
+
```verity
117
+
errors
118
+
error AddOverflow()
119
+
error MulOverflow(Uint256, Uint256)
120
+
121
+
let sum <- requireSomeUintError (safeAdd a b) AddOverflow()
122
+
let product <- requireSomeUintError (safeMul sum b) MulOverflow(sum, b)
Copy file name to clipboardExpand all lines: docs/ARITHMETIC_PROFILE.md
+15-2Lines changed: 15 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -85,7 +85,20 @@ For contracts that require overflow protection, the EDSL provides checked operat
85
85
|`mulDiv512Down? a b c`|`Option Uint256`|`none` if `c = 0` or `floor(a * b / c) > 2^256 - 1`; product is unbounded |
86
86
|`mulDiv512Up? a b c`|`Option Uint256`|`none` if `c = 0` or `ceil(a * b / c) > 2^256 - 1`; product is unbounded |
87
87
88
-
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.
88
+
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.
89
+
90
+
Example checked arithmetic with a typed custom error:
91
+
92
+
```lean
93
+
errors
94
+
error AddOverflow ()
95
+
error MulOverflow (Uint256, Uint256)
96
+
97
+
function checked (a : Uint256, b : Uint256) : Uint256 := do
98
+
let sum ← requireSomeUintError (safeAdd a b) AddOverflow()
99
+
let product ← requireSomeUintError (safeMul sum b) MulOverflow(sum, b)
100
+
return product
101
+
```
89
102
90
103
For Solidity-0.8-style source models, prefer the panic wrappers
91
104
`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
175
188
176
189
1. Confirm that the contract's arithmetic assumptions match wrapping semantics.
177
190
2. If overflow or division-by-zero protection is required, verify the contract uses `safeAdd`/`safeSub`/`safeMul`/`safeDiv`.
178
-
3. Check that `requireSomeUint` is used to revert on overflow/underflow or zero divisors.
191
+
3. Check that `requireSomeUint`or `requireSomeUintError`is used to revert on overflow/underflow or zero divisors.
179
192
4. Review `Compiler/Proofs/ArithmeticProfile.lean` for the formal wrapping proofs.
180
193
5. Confirm the backend profile does not affect arithmetic behavior (it doesn't).
0 commit comments