Checked vs Wrapping Arithmetic

In .cam source, +, -, and * are checked: overflow or underflow is a failure. +%, -%, and *% are wrapping: the result is reduced modulo the type’s range. There is no wrapping division.

The same operators apply in pure fn bodies, route actions, and member transforms. On EVM, checked ops match Solidity 0.8. On Lean, the source meaning is still checked, but the generated model of +/-/* depends on lean.numerics in project.yaml — the default Lean model wraps.

Checked operators

Widening as is a no-op (zero- or sign-extend). Wrap-around is only +% / -% / *%.

pure fn checked_u8_add(a: u8, b: u8) -> u8 {
    a + b   // reverts on EVM if a + b > 255
}

pure fn checked_div(a: U256, b: U256) -> U256 {
    a / b   // reverts if b == 0
}

Use checked ops for balances, supplies, counters, and any path where silent wrap-around would be a bug.

std::math::{divc,divr,divmod,muldiv} also fail on a zero divisor on every target (independent of lean.numerics).

Wrapping operators

pure fn wrapping_u8_add() -> u8 {
    (255 as u8) +% 1    // 0
}

pure fn wrapping_u8_sub() -> u8 {
    (0 as u8) -% 1      // 255
}

pure fn wrapping_u8_mul() -> u8 {
    (255 as u8) *% 2    // 254
}

Signed wrapping is two’s complement:

pure fn wrapping_i8_inc() -> i8 {
    (127 as i8) +% 1    // -128
}

There is no /% or %%.

EVM lowering

On --target evm, wrapping ops lower to per-entity internal pure helpers _wadd / _wsub / _wmul whose bodies are unchecked { … }. That preserves Solidity 0.8 wrap-around without turning off checked arithmetic elsewhere in the contract. Helpers are emitted only when the entity uses a wrapping op.

The helpers take uint256; a narrower result is truncated with an explicit Solidity cast (so u8 wrap-around is the low 8 bits).

Canonical use: the Uniswap V2 cumulative-price oracle (examples/uniswap-v2/UniswapV2Pair.cam) accumulates time_elapsed * uqdiv(…) with +% so UQ112x112 math can overflow the 112-bit boundary by design.

Lean: lean.numerics

Source +/-/* stay checked as above. How --target lean models those operators is selected in project.yaml. Wrapping ops +%/-%/*% are wrapping infix in every BitVec mode.

lean:
  numerics: overflow-panic   # or overflow-wrap (default) or nat

nat is a simplified proof model, not a reproduction of Solidity 0.8: unsigned - saturates (0 - 1 = 0), +/* overflow is ignored, and / 0 is Lean’s total Nat division (not Panic(0x12)). Use overflow-panic when the Lean model must match checked EVM arithmetic. Unknown values are rejected (F2).

See project.yaml and Lean-EVM.

Applicability

Interaction with widening

Overflow checking (or wrapping) applies to the result type after widening. Adding two u8 values into a u16 context widens first, so checked + cannot overflow for any pair of u8s. An explicit wider cast is an alternative to wrapping when you want the full mathematical result.

Mixing operators

Each operator decides independently:

pure fn mix_wrap_then_checked(a: u8, b: u8, c: u8) -> u8 {
    (a +% b) * c    // wrap the sum, then checked multiply
}

Choosing