Skip to content

ARITHMETIC_PROFILE.md

Latest commit

 

History

History
202 lines (162 loc) · 13 KB

ARITHMETIC_PROFILE.md

File metadata and controls

202 lines (162 loc) · 13 KB

Arithmetic Profile

Verity uses wrapping modular arithmetic at 2^256 across all compilation layers, matching the EVM Yellow Paper specification.

This document is the authoritative reference for arithmetic semantics. For formal proofs, see Compiler/Proofs/ArithmeticProfile.lean.

Wrapping Semantics

All arithmetic in the compilation path (EDSL -> CompilationModel -> IR -> Yul) wraps modulo 2^256. There are no implicit overflow checks; values silently wrap.

Operation Semantics Div/Mod-by-zero
add(a, b) (a + b) % 2^256 —
sub(a, b) (2^256 + a - b) % 2^256 —
mul(a, b) (a * b) % 2^256 —
div(a, b) a / b (truncating) returns 0
mod(a, b) a % b returns 0
and(a, b) bitwise AND —
or(a, b) bitwise OR —
xor(a, b) bitwise XOR —
not(a) (2^256 - 1) - a —
shl(s, v) (v * 2^s) % 2^256 —
shr(s, v) v / 2^s —
lt(a, b) 1 if a < b, else 0 —
gt(a, b) 1 if a > b, else 0 —
eq(a, b) 1 if a = b, else 0 —
iszero(a) 1 if a = 0, else 0 —

Proof Coverage

Wrapping semantics are proven (not assumed) across all three verification layers:

Layer Proof location What is proved
Layer 1 (EDSL) Verity/Core/Uint256.lean Uint256.add, sub, mul, pow, div, mod are wrapping modular
Layer 1 (EDSL) Verity/Proofs/Stdlib/Math.lean safeAdd, safeSub, safeMul correctness
Compiler Compiler/Proofs/ArithmeticProfile.lean add_wraps, sub_wraps, mul_wraps, div_by_zero, mod_by_zero
EVMYulLean native builtins Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBuiltinSemantics.lean Native builtin dispatch for EVMYulLean proofs
EVMYulLean routing facts Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean Native routing lemmas for all bridged builtins
EVMYulLean bridge tests Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean Smoke vectors for the native builtin routing surface

The EVMYulLean native builtin layer uses EVMYulLean's Fin-based UInt256 operations directly. Current coverage:

  • universal bridge lemmas for 25 pure builtins: add, sub, mul, div, mod, addmod, mulmod, exp, sdiv, smod, lt, gt, slt, sgt, eq, iszero, and, or, xor, not, shl, shr, sar, signextend, and byte
  • context-lifted native routing through evalBuiltinCallWithEvmYulLeanContext for all 36 covered builtin cases
  • concrete bridge smoke tests are no longer needed for any pure builtin

The EDSL exposes pow(a, b) and a ^ b for EVM modular exponentiation. Macro lowering emits a reserved compiler builtin that compiles directly to Yul/EVM exp(a, b).

Higher-Level Expression Operators

Beyond the 15 low-level builtins, the ExprCompileCore proven fragment includes compilation-correctness proofs for 8 higher-level expression operators:

Operator Arity Semantics
min(a, b) binary minimum of two values
max(a, b) binary maximum of two values
ceilDiv(a, b) binary ceiling division (a + b - 1) / b
ite(c, t, e) ternary conditional expression
wMulDown(a, b) binary (a * b) / WAD (WAD = 10^18)
wDivUp(a, b) binary (a * WAD + b - 1) / b
mulDivDown(a, b, c) ternary (a * b) / c
mulDivUp(a, b, c) ternary (a * b + c - 1) / c

These proofs are in Compiler/Proofs/IRGeneration/FunctionBody/Base.lean and Compiler/Proofs/IRGeneration/FunctionBody/Stmt.lean, and cover both IR compilation correctness and end-to-end evaluation semantics.

The compiled mulDivDown / mulDivUp operators still use 256-bit EVM multiplication before division. They are suitable for fixed-point code whose product is known to fit in uint256, but they are not full-precision OpenZeppelin/Solmate Math.mulDiv replacements.

Checked (Safe) Arithmetic

For contracts that require overflow protection, the EDSL provides checked operations:

Operation Type Behavior
safeAdd a b Option Uint256 none if a + b > 2^256 - 1
safeSub a b Option Uint256 none if b > a
safeMul a b Option Uint256 none if a * b > 2^256 - 1
safeDiv a b Option Uint256 none if b = 0
addPanic a b Contract Uint256 reverts with Panic(0x11) if a + b > 2^256 - 1
subPanic a b Contract Uint256 reverts with Panic(0x11) if b > a
mulPanic a b Contract Uint256 reverts with Panic(0x11) if a * b > 2^256 - 1
divPanic a b Contract Uint256 reverts with Panic(0x12) if b = 0
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. 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:

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 around the safe operations with canonical panic messages, and the verity_contract macro lowers binds such as let total ← addPanic total amount to the same checked guard/result shape as the explicit requireSomeUint spelling. The generated-Yul feature tests assert the guard lowering for all four safe arithmetic operations.

Correctness proofs: Verity/Proofs/Stdlib/Math.lean proves that checked operations return the correct result within bounds and none otherwise (e.g., safeAdd_some, safeAdd_none).

Stdlib.Math also exposes fixed-point helpers mulDivDown, mulDivUp, wMulDown, and wDivUp (the w variants fix the divisor/multiplier to WAD = 10^18). All lemmas are in Verity/Proofs/Stdlib/Math.lean and are intentionally preconditioned: they assume the widened numerator stays within MAX_UINT256.

For full-precision modeling, mulDiv512Down?_some and mulDiv512Up?_some state the exact natural-number quotient returned when the divisor is nonzero and the final quotient fits; the matching _none_of_zero_divisor, _none_of_overflow, _eq_some_iff, _isSome_iff, and _isNone_iff lemmas expose the failure boundary. Successful full-precision results also have direct sandwich lemmas: mulDiv512Down?_mul_le, mulDiv512Down?_lt_succ_mul, mulDiv512Up?_mul_ge, and mulDiv512Up?_mul_le_add_pred, plus one-divisor error-bound lemmas mulDiv512Down?_mul_lt_add and mulDiv512Up?_mul_lt_add. They also mirror the existing mulDiv convenience surface with numerator commutativity, successful-result numerator monotonicity, divisor antitonicity, positivity, zero-numerator, and exact same-denominator cancellation lemmas. Compatibility bridge lemmas mulDiv512Down?_eq_mulDivDown_of_no_overflow and mulDiv512Up?_eq_mulDivUp_of_no_overflow connect the full-precision helpers to the existing 256-bit helpers under the older no-overflow preconditions. Full-precision ceil/floor exactness is covered by mulDiv512Up?_eq_down_of_dvd and mulDiv512Up?_some_succ_of_not_dvd, matching the older 256-bit mulDiv divisibility proof shape. The success/rejection bridge lemmas mulDiv512Down?_isSome_of_up_isSome and mulDiv512Up?_isNone_of_down_isNone connect the two rounding modes. Successful ceil/floor result pairs also expose the same one-step rounding boundary through mulDiv512Down?_le_up, mulDiv512Up?_le_down_add_one, and mulDiv512Up?_eq_down_or_succ.

Verity.Proofs.Stdlib.Automation mirrors the full-precision fit/rejection iff lemmas under automation-friendly names (mulDiv512Down?_some_iff, mulDiv512Down?_none_iff, mulDiv512Up?_some_iff, mulDiv512Up?_none_iff), so downstream proofs can rewrite common quotient-fit side conditions without importing the full arithmetic proof module directly.

Lemma family Generic helpers Wad-specialized helpers
Monotonicity (numerator) mulDivDown_monotone_left/right, mulDivUp_monotone_left/right wMulDown_monotone_left/right, wDivUp_monotone_left
Commutativity mulDivDown_comm, mulDivUp_comm wMulDown_comm
Positivity mulDivDown_pos, mulDivUp_pos wMulDown_pos, wDivUp_pos
Zero collapse mulDivDown_zero_left/right, mulDivUp_zero_left/right wMulDown_zero_left/right, wDivUp_zero
Cancellation / identity mulDivDown_cancel_right/left, mulDivUp_cancel_right/left wMulDown_one_left/right, wDivUp_by_wad
Antitonicity (divisor) mulDivDown_antitone_divisor, mulDivUp_antitone_divisor wDivUp_antitone_right
Rounding gap (ceil vs floor) mulDivUp_le_mulDivDown_add_one, mulDivUp_eq_mulDivDown_or_succ —
Divisibility exactness mulDivUp_eq_mulDivDown_of_dvd, mulDivUp_eq_mulDivDown_add_one_of_not_dvd —
Floor sandwich bounds mulDivDown_mul_le, mulDivDown_mul_lt_add wMulDown_mul_le, wMulDown_mul_lt_add
Ceil sandwich bounds mulDivUp_mul_ge, mulDivUp_mul_lt_add wDivUp_mul_ge, wDivUp_mul_lt_add

The sandwich bounds are especially useful for AMM reserve/share proofs. For BN254/Groth16 public-input proofs, modField_nat_eq, modField_lt, modField_zero, modField_SNARK_SCALAR_FIELD, modField_eq_zero_iff, modField_eq_of_nat_mod_eq, modField_eq_iff_nat_mod_eq, modField_eq_self_of_lt, modField_nat_mod_eq, and modField_idempotent expose the exact SNARK_SCALAR_FIELD reduction semantics used by Stdlib.Math.modField.

Example: See Contracts/SafeCounter/SafeCounter.lean and Contracts/SafeCounter/Proofs/Basic.lean for a contract using checked arithmetic with proven overflow/underflow behavior.

Backend Profiles and Arithmetic

All backend profiles (--backend-profile semantic, solidity-parity-ordering, solidity-parity) use identical wrapping arithmetic semantics. Profiles differ only in Yul output-shape normalization:

  • semantic (default): canonical output order
  • solidity-parity-ordering: dispatch case blocks sorted by selector
  • solidity-parity: selector sorting + deterministic patch pass

The arithmetic model is invariant across profiles. See docs/SOLIDITY_PARITY_PROFILE.md for profile details.

What Is NOT Proved

  • Gas semantics: proofs establish result correctness, not gas cost or bounded liveness.
  • Compiler-layer overflow detection: the compiler does not insert overflow or division-by-zero checks. Use EDSL safeAdd/safeSub/safeMul/safeDiv for checked behavior.
  • Cryptographic primitives: keccak256 is axiomatized (see AXIOMS.md).
  • Universal bridge equivalence: 25/25 pure EVMYulLean-backed builtins have universal bridge lemmas. All 25 also have context-lifted native bridge theorems. All 8 higher-level expression operators also have proven compilation correctness.

Auditor Checklist

  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 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).

Related Documents