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

entity Counter8 {
    routes {
        tick() => []
        untick() => []
        double() => []
    }

    m_ring: u8 {
        in tick() => m_ring +% 1      // 255 -> 0
        in untick() => m_ring -% 1    // 0 -> 255
        in double() => m_ring *% 2    // 255 -> 254
    }
}

Signed wrapping is two’s complement (127 +% 1 is -128 for i8).

There is no /% or %%.

EVM lowering

On --target evm, wrapping ops lower to pure helpers _wadd / _wsub / _wmul (and _wadds / _wsubs / _wmuls for signed operands) whose bodies are unchecked { … }. That preserves Solidity 0.8 wrap-around without turning off checked arithmetic elsewhere in the contract. The helpers are emitted inside the contract for entity code, and at file scope when a free pure fn uses a wrapping op.

The helpers take uint256 / int256; a narrower result is truncated with an explicit Solidity cast (so u8 wrap-around is the low 8 bits, and i8 wraps within -128…127).

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

Both kinds work in member transforms, route bodies, and pure fn bodies, on EVM and Lean. In the BitVec Lean modes, a wrapping result is truncated to the width of its type, as on EVM.

Interaction with widening

Overflow checking (or wrapping) applies to the result type after widening, which depends only on the operand types — not on where the result is stored. a + b with a, b: u8 is computed in u8 and reverts if the sum exceeds 255, even when assigned to a u16. Cast an operand first ((a as u16) + b) when you want the full mathematical result.

Mixing operators

Each operator decides independently:

entity Mixer {
    routes {
        mix(b: U256, c: U256) => []
    }

    m_acc: U256 {
        in mix(b, c) => (m_acc +% b) * c    // wrap the sum, then checked multiply
    }
}

Choosing