A formally verified library of common unsigned and signed operations.

We have formally verified all non-trivial functions of this library using the Sui Prover. Verification was performed by Asymptotic in partnership with Bluefin.

This library is a fork the widely-used integer-mate library but with a focus on security and correctness, and backed by full formal verification.

The verification effort covers 126 functions across multiple integer types (u64, u128, u256, i32, i64, i128). The only public functions not verified are wrappers-unwrappers of signed integers, as they are both trivial and needed as part of the verification itself.

1. Cetus Protocol Vulnerability Discovery: After the Cetus protocol exploit we checked both the exitance of the bug and the correctness of the fix using formal verification. See our detailed analysis.

2. Integer Library Bug: During the initial formal verification of the library we discovered and reported a new bug in the signed ::sub function that could cause incorrect results under specific conditions. We coordinated with the Sui Foundation for an ecosystem-wide fix. See our report. The buggy version is preserved as sub_buggy in the codebase for educational purposes.

• Total Functions Verified: 126
• Integer Types Covered: u64, u128, u256, I32, I64, I128
• Operation Categories:
  • Arithmetic operations (add, sub, mul, div, mod)
  • Bitwise operations (shl, shr, and, or, not)
  • Overflow-safe variants (wrapping, checked, overflowing)
  • Comparison operations (eq, lt, gt, lte, gte)
  • Type conversions and utility functions

Through formal verification, we established comprehensive mathematical guarantees for every possible input:

Functional Correctness:

• Exact computation: Every function produces the mathematically correct result for all valid inputs
• Abort conditions: Precise specification of when functions abort (division by zero, overflow in non-wrapping functions, shift amounts out of bounds)
• No undefined behavior: Every input produces either a well-defined result or a well-defined abort

Overflow Behavior:

• Wrapping semantics: wrapping_* functions correctly implement modular arithmetic (mod 2^n)
• Overflow detection: overflowing_* functions correctly return both wrapped result and overflow flag
• Checked operations: Functions without wrapping_ abort on overflow, preventing silent errors
• Full precision: Operations like full_mul correctly compute results in higher precision (e.g., 256-bit product from two 128-bit inputs)

Integer Type Properties:

• Two's complement correctness: Signed integer operations correctly implement two's complement arithmetic
• Sign handling: Negation, absolute value, and sign detection work correctly for all values including boundary cases
• Type conversions: Conversions between integer types correctly preserve values when in range and abort when out of range
• Boundary correctness: Operations handle MIN/MAX values correctly (e.g., abs(MIN_I128) correctly aborts)

Bit Operations:

• Shift correctness: Left and right shifts produce correct results with proper bounds checking
• Arithmetic right shift: Signed right shifts correctly extend the sign bit
• Bitwise operations: AND, OR, NOT operations compute correct bit-level results

Division and Modulo:

• Division modes: Correct implementation of floor, ceiling, and truncating division
• Zero handling: All division operations correctly abort on division by zero
• Remainder correctness: div_mod returns quotient and remainder satisfying dividend = quotient * divisor + remainder

Several functions exhibit important behavioral patterns that users should be aware of:

• Functions with wrapping_ prefix perform modular arithmetic and never abort
• Functions with checked_ prefix return overflow indicators
• Some shift operations use modular arithmetic which can be unintuitive (see warnings in function descriptions)
• Certain operations require custom prover configurations due to complexity

✅ indicates that the specification is proved. All functions have been proved.

1. Install Sui Prover
2. Run sui-prover in the specs directory
3. Run sui-prover --no-bv-int-encoding in the specs-bv directory

✅ Computes num1 + num2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes arithmetic right shift v >> shift.
⏮️ The function aborts unless shift < 128.

✅ Computes num1 + num2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes arithmetic right shift v >> shift.
⏮️ The function aborts unless shift < 32.

✅ Computes num1 + num2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes arithmetic right shift v >> shift.
⏮️ The function aborts unless shift < 64.

✅ Computes num1 * num2 using 256-bit arithmetic for intermediate product computation.
⏮️ The function does not abort.

✅ Computes (num1 * num2) / denom with floor division using 256-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless denom > 0 and the result fits in u128.

✅ Computes (num1 * num2) / denom with rounding division using 256-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless denom > 0 and the result fits in u128.

✅ Computes (num1 * num2) / denom with ceiling division using 256-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless denom > 0 and the result fits in u128.

✅ Computes (num1 * num2) >> shift using 256-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless shift <= 255 and the result fits in u128.

✅ Computes (num1 * num2) << shift using 256-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless shift <= 255 and the result fits in u128.
⚠️ Note that due to << not aborting when losing significant bits, the actual result is ((num1 * num2) << shift) mod 2^256 (note the modulo), which can be unintuitive to users.

✅ Computes num1 * num2 using 128-bit arithmetic for intermediate product computation.
⏮️ The function does not abort.

✅ Computes (num1 * num2) / denom with floor division using 128-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless denom > 0 and the result fits in u64.

✅ Computes (num1 * num2) / denom with rounding division using 128-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless denom > 0 and the result fits in u64.

✅ Computes (num1 * num2) / denom with ceiling division using 128-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless denom > 0 and the result fits in u64.

✅ Computes (num1 * num2) >> shift using 128-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless shift <= 127 and the result fits in u64.

✅ Computes (num1 * num2) << shift using 128-bit arithmetic for intermediate product computation.
⏮️ The function aborts unless shift <= 127 and the result fits in u64.
⚠️ Note that due to << not aborting when losing significant bits, the actual result is ((num1 * num2) << shift) mod 2^128 (note the modulo), which can be unintuitive to users.

✅ Computes 0 as an I128.
⏮️ The function does not abort.

✅ Computes an I128 from a u128.
⏮️ The function aborts when the value exceeds I128::MAX.

✅ Computes an I128 from the negation of a u128.
⏮️ The function aborts when the result does not fit in I128.

✅ Computes the negation of an I128.
⏮️ The function aborts when the input is MIN_I128, that is -2^127.

✅ Computes num1 + num2 with wrapping overflow.
⏮️ The function does not abort.
⚠️ Proved in a separate package as it requires a custom prover configuration.

✅ Computes num1 + num2.
⏮️ The function aborts when the result does not fit in I128.

✅ Computes num1 + num2 and returns a flag indicating overflow.
⏮️ The function does not abort.

✅ Computes num1 - num2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes num1 - num2.
⏮️ The function aborts when the result does not fit in I128.

✅ Computes num1 - num2 and returns a flag indicating overflow.
⏮️ The function does not abort.

✅ Computes num1 * num2.
⏮️ The function aborts when the result does not fit in I128.

✅ Computes num1 / num2 with truncation.
⏮️ The function aborts when the result does not fit in I128, or the denominator is zero.

✅ Computes the absolute value of an I128.
⏮️ The function aborts when the input is MIN_I128, that is -2^127.

✅ Computes the absolute value of an I128 as a u128.
⏮️ The function does not abort.

✅ Computes v << shift.
⏮️ The function aborts unless shift < 128.

✅ Computes v >> shift.
⏮️ The function aborts unless shift < 128.
⚠️ Proved in a separate package as it requires a custom prover configuration.

✅ Converts an I128 to an I64.
⏮️ The function aborts when the value does not fit in I64.

✅ Converts an I128 to an I32.
⏮️ The function aborts when the value does not fit in I32.

✅ Returns 1 if the input is negative, 0 otherwise.
⏮️ The function does not abort.

✅ Returns true if the input is negative, false otherwise.
⏮️ The function does not abort.

✅ Compares two I128s.
⏮️ The function does not abort.

✅ Compares two I128s, returns true if they are equal, false otherwise.
⏮️ The function does not abort.

✅ Compares two I128s, returns true if the first is greater than the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I128s, returns true if the first is greater than or equal to the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I128s, returns true if the first is less than the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I128s, returns true if the first is less than or equal to the second, false otherwise.
⏮️ The function does not abort.

✅ Computes the bitwise OR of two I128s.
⏮️ The function does not abort.

✅ Computes the bitwise AND of two I128s.
⏮️ The function does not abort.

✅ Computes the bitwise NOT of a u128.
⏮️ The function does not abort.

✅ Computes the bitwise NOT of a u8.
⏮️ The function does not abort.

✅ Computes 0 as an I32.
⏮️ The function does not abort.

✅ Computes an I32 from a u32.
⏮️ The function does not abort.

✅ Computes an I32 from a u32.
⏮️ The function does not abort.

✅ Computes an I32 from a u32.
⏮️ The function aborts when the result does not fit in I32.

✅ Computes num1 + num2 with wrapping overflow.
⏮️ The function does not abort.
⚠️ Proved in a separate package as it requires a custom prover configuration.

✅ Computes num1 + num2.
⏮️ The function aborts when the result does not fit in I32.

✅ Computes num1 - num2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes num1 - num2.
⏮️ The function aborts when the result does not fit in I32.
⚠️ This function was initially incorrect but fixed after our reporting. Replace the target with sub_buggy to see the how the bug is caught.

✅ Computes num1 * num2.
⏮️ The function aborts when the result does not fit in I32.

✅ Computes num1 / num2 with truncation.
⏮️ The function aborts when the result does not fit in I32, or the denominator is zero.

✅ Computes the absolute value of an I32.
⏮️ The function aborts when the input is MIN_I32, that is -2^31.

✅ Computes the absolute value of an I32 as a u32.
⏮️ The function does not abort.

✅ Computes v << shift.
⏮️ The function aborts unless shift < 32.

✅ Computes v >> shift.
⏮️ The function aborts unless shift < 32.
⚠️ Proved in a separate package as it requires a custom prover configuration.

✅ Computes v % n.
⏮️ The function aborts when the denominator is zero.

✅ Returns 1 if the input is negative, 0 otherwise.
⏮️ The function does not abort.

✅ Returns true if the input is negative, false otherwise.
⏮️ The function does not abort.

✅ Compares two I32s.
⏮️ The function does not abort.

✅ Compares two I32s, returns true if they are equal, false otherwise.
⏮️ The function does not abort.

✅ Compares two I32s, returns true if the first is greater than the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I32s, returns true if the first is greater than or equal to the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I32s, returns true if the first is less than the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I32s, returns true if the first is less than or equal to the second, false otherwise.
⏮️ The function does not abort.

✅ Computes the bitwise OR of two I32s.
⏮️ The function does not abort.

✅ Computes the bitwise AND of two I32s.
⏮️ The function does not abort.

✅ Computes the bitwise NOT of a u32.
⏮️ The function does not abort.

✅ Computes the bitwise NOT of a u8.
⏮️ The function does not abort.

✅ Computes 0 as an I64.
⏮️ The function does not abort.

✅ Computes an I64 from a u64.
⏮️ The function does not abort.

✅ Computes an I64 from a u64.
⏮️ The function does not abort.

✅ Computes an I64 from a u64.
⏮️ The function aborts when the result does not fit in I64.

✅ Computes num1 + num2 with wrapping overflow.
⏮️ The function does not abort.
⚠️ Proved in a separate package as it requires a custom prover configuration.

✅ Computes num1 + num2.
⏮️ The function aborts when the result does not fit in I64.

✅ Computes num1 - num2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes num1 - num2.
⏮️ The function aborts when the result does not fit in I64.

✅ Computes num1 * num2.
⏮️ The function aborts when the result does not fit in I64.

✅ Computes num1 / num2 with truncation.
⏮️ The function aborts when the result does not fit in I64, or the denominator is zero.

✅ Computes the absolute value of an I64.
⏮️ The function aborts when the input is MIN_I64, that is -2^63.

✅ Computes the absolute value of an I64 as a u64.
⏮️ The function does not abort.

✅ Computes v << shift.
⏮️ The function aborts unless shift < 64.

✅ Computes v >> shift.
⏮️ The function aborts unless shift < 64.
⚠️ Proved in a separate package as it requires a custom prover configuration.

✅ Computes v % n.
⏮️ The function aborts when the denominator is zero.

✅ Returns 1 if the input is negative, 0 otherwise.
⏮️ The function does not abort.

✅ Returns true if the input is negative, false otherwise.
⏮️ The function does not abort.

✅ Compares two I64s.
⏮️ The function does not abort.

✅ Compares two I64s, returns true if they are equal, false otherwise.
⏮️ The function does not abort.

✅ Compares two I64s, returns true if the first is greater than the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I64s, returns true if the first is greater than or equal to the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I64s, returns true if the first is less than the second, false otherwise.
⏮️ The function does not abort.

✅ Compares two I64s, returns true if the first is less than or equal to the second, false otherwise.
⏮️ The function does not abort.

✅ Computes the bitwise OR of two I64s.
⏮️ The function does not abort.

✅ Computes the bitwise AND of two I64s.
⏮️ The function does not abort.

✅ Computes the bitwise NOT of a u64.
⏮️ The function does not abort.

✅ Computes the bitwise NOT of a u8.
⏮️ The function does not abort.

✅ Computes n1 + n2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes n1 + n2 with wrapping overflow and a boolean indicating overflow.
⏮️ The function does not abort.

✅ Computes n1 - n2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes n1 - n2 with wrapping overflow and a boolean indicating overflow.
⏮️ The function does not abort.

✅ Computes n1 * n2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes n1 * n2 with wrapping overflow and a boolean indicating overflow.
⏮️ The function does not abort.

✅ Computes the full 256-bit product of n1 * n2 as two u128 values (lo, hi).
⏮️ The function does not abort.

✅ Extracts the high 64 bits of a u128 value.
⏮️ The function does not abort.

✅ Extracts the low 64 bits of a u128 value.
⏮️ The function does not abort.

✅ Extracts the high 64 bits of a u128 value as a u128.
⏮️ The function does not abort.

✅ Extracts the low 64 bits of a u128 value as a u128.
⏮️ The function does not abort.

✅ Constructs a u128 from low and high u64 components.
⏮️ The function does not abort.

✅ Computes num / denom with optional rounding up.
⏮️ The function aborts if denom == 0.

✅ Returns the maximum of two u128 values.
⏮️ The function does not abort.

✅ Returns the minimum of two u128 values.
⏮️ The function does not abort.

✅ Checks if num1 + num2 will overflow.
⏮️ The function does not abort.

✅ Computes num / denom and num % denom.
⏮️ The function aborts if denom == 0.

✅ Shifts n left by 64 bits (one word) with wrapping overflow.
⏮️ The function does not abort.

✅ Shifts n right by 64 bits (one word).
⏮️ The function does not abort.

✅ Shifts n left by 64 bits (one word) and returns a boolean indicating overflow.
⏮️ The function does not abort.
⚠️ Returns (0, true) when overflow occurs, not the wrapped value.

✅ Computes num / denom with optional rounding up.
⏮️ The function aborts if denom == 0.

✅ Checks if num1 + num2 will overflow.
⏮️ The function does not abort.

✅ Computes n1 + n2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes n1 + n2 with wrapping overflow and a boolean indicating overflow.
⏮️ The function does not abort.

✅ Computes n1 - n2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes n1 - n2 with wrapping overflow and a boolean indicating overflow.
⏮️ The function does not abort.

✅ Computes n1 * n2 with wrapping overflow.
⏮️ The function does not abort.

✅ Computes n1 * n2 with overflowing overflow and a boolean indicating overflow.
⏮️ The function does not abort.

✅ Computes n1 + n2 + carry returning the result and the new carry.
⏮️ The function aborts unless carry <= 1.

✅ Checks if n1 + n2 will overflow.
⏮️ The function does not abort.