Checked Arithmetic

Checked arithmetic operations detect integer overflow before it occurs, returning a Result<T> rather than silently wrapping. Nitpick provides checked variants for int64, int32, tbb32, and tbb64.

The Problem with Silent Overflow

Standard integer arithmetic in Nitpick (and most systems languages) wraps silently on overflow:

int64:x = 9223372036854775807i64;  // INT64_MAX
int64:y = x + 1i64;               // Wraps to -9223372036854775808 — no error!

For security-critical, financial, or real-time control code, this is unacceptable. Checked arithmetic makes overflow visible.

Checked Arithmetic Builtins (v0.55.3)

These are compiler intrinsics — no import needed.

int64

Function	Description	Returns
`checked_add(a, b)`	a + b, fail on overflow	`Result<int64>`
`checked_sub(a, b)`	a - b, fail on underflow	`Result<int64>`
`checked_mul(a, b)`	a * b, fail on overflow	`Result<int64>`
`checked_div(a, b)`	a / b, fail on div-by-zero or INT64_MIN/-1	`Result<int64>`
`checked_neg(a)`	-a, fail if a == INT64_MIN	`Result<int64>`

int64:a = 9223372036854775000i64;
int64:b = 1000i64;

// Pattern-match on overflow
(checked_add(a, b)) {
    | ok(int64:sum) -> drop println("sum = {sum}");
    | err(_)        -> drop println("overflow detected!");
};

int32

Function	Description
`checked_add_i32(a, b)`	int32 add with overflow detection
`checked_sub_i32(a, b)`	int32 subtract
`checked_mul_i32(a, b)`	int32 multiply

tbb32 / tbb64

TBB types carry an ERR sentinel (INT32_MIN / INT64_MIN). Checked operations for TBB types additionally ensure the result never silently becomes the ERR sentinel:

Function	Description
`checked_add_tbb32(a, b)`	tbb32 add — fails on overflow OR if result == ERR
`checked_sub_tbb32(a, b)`	tbb32 subtract
`checked_mul_tbb32(a, b)`	tbb32 multiply
`checked_add_tbb64(a, b)`	tbb64 add — fails on overflow OR if result == ERR
`checked_sub_tbb64(a, b)`	tbb64 subtract
`checked_mul_tbb64(a, b)`	tbb64 multiply

Safety Patterns

Accumulator with Overflow Guard

// Sum a large array safely
func:safe_sum = Result<int64>(int64[]:values) {
    int64:total = 0i64;
    for (int32:i = 0; i < len(values); i++) {
        (checked_add(total, values[i])) {
            | ok(int64:s) -> total = s;
            | err(_)      -> return err("sum overflowed");
        };
    }
    return ok(total);
};

Multiplication Guard (Financial)

// Compute price * quantity without silent overflow
func:calc_total = Result<int64>(int64:price_cents, int64:qty) {
    return checked_mul(price_cents, qty);
};

Checked Negation (Absolute Value)

// Safe abs that handles INT64_MIN
func:safe_abs = Result<int64>(int64:x) {
    if (x >= 0i64) { return ok(x); }
    return checked_neg(x);  // Fails if x == INT64_MIN
};

INT64_MIN Edge Cases

The value INT64_MIN = -9223372036854775808 requires special attention:

checked_neg(INT64_MIN) → err (no positive representation)
checked_div(INT64_MIN, -1) → err (result would be INT64_MAX+1)
checked_mul(INT64_MIN, -1) → err
abs(INT64_MIN) → undefined in two's complement (wraps back to INT64_MIN)

These edge cases are formally verified by Z3 in verification/z3/checked_arithmetic_properties.py.

Formal Verification

The Z3 proof file verification/z3/checked_arithmetic_properties.py proves:

checked_add(a, b) returns err iff a + b would overflow int64 range
checked_mul(a, b) returns err iff a * b would overflow int64 range
Commutativity: checked_add(a, b) succeeds iff checked_add(b, a) succeeds
TBB checked ops never produce the ERR sentinel as a success value
checked_neg(INT64_MIN) always returns err

Run the proofs:

python3 verification/z3/checked_arithmetic_properties.py

When to Use Checked Arithmetic

Use checked arithmetic when:

Computing financial values (prices, balances, quantities)
Accumulating large datasets where overflow is possible
Implementing security-sensitive protocols
Working in real-time control systems where silent corruption is catastrophic
Any code that will run on untrusted or user-supplied input

For performance-critical inner loops where overflow is provably impossible by construction, standard arithmetic is appropriate. Document the invariant as a comment.

standard_library/math.md — general math functions
types/int.md — integer type system
types/tbb.md — TBB type semantics and ERR sentinel