Skip to content

ARITHMETIC_PROFILE.md

Latest commit

 

History

History
175 lines (139 loc) · 11.7 KB

ARITHMETIC_PROFILE.md

File metadata and controls

175 lines (139 loc) · 11.7 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 reference oracle Compiler/Proofs/YulGeneration/ReferenceOracle/Builtins.lean evalBuiltinCall implements wrapping for all 15 pure builtins
Compiler Compiler/Proofs/ArithmeticProfile.lean add_wraps, sub_wraps, mul_wraps, div_by_zero, mod_by_zero
EVMYulLean bridge Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean Universal bridge lemmas for all 25 pure builtins (see list below)
EVMYulLean bridge tests Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean Regression vectors for the universal pure-builtin bridge lemmas

The EVMYulLean bridge validates that Verity's Nat-modular arithmetic agrees with EVMYulLean's Fin-based UInt256 operations. 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 bridge theorems for all 25 pure builtins at the evalBuiltinCallWithBackendContext level (the Phase 4 backend-retargeting surface)
  • 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.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
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.

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 backend bridge theorems for Phase 4 retargeting. 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 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