Formal Verification of Fundamental Operations

As shown in 5, the integers form a commutative ring with the operations addition, unary negation, multiplication, and contain the constant 0. Subtraction is a derived operation as it is nothing but . This allows us to detect overflow in addition (and underflow in subtraction) easily by detecting instances where the result is less than (or greater than) the left operand. Examples are UINT32_MAX + 1 = 0 and 0U - 1 = UINT32_MAX.

We are also given from Definition 1[5] that an integer arithmetic A is more precise than an integer arithmetic B, denoted by , iff there exists a surjective homomorphism . This means that we can lift the computation into A and compare the results of the operation in both A and B. If they are equivalent then no overflow occurred; otherwise it did. In the u128 case we do not have an integer arithmetic A to lift the computation into. For this operation between a and b we check if . If it is, then overflow must occur; otherwise it does not.

Division and modulo do not belong to the ring operations [5]. What we do know is that and the result of . This means that we need only check for the case where b = 0, as this operation is undefined.

The inequality that serves unsigned addition does not carry over: adding two negatives can wrap to a positive result that is still less than either operand. Detection instead relies on a sign-bit identity. A signed sum overflows iff the operands share a sign and the result sign differs, which in two’s complement is the predicate where denotes the unsigned view of . Subtraction is the dual case: overflows iff the operands differ in sign and the result sign differs from , captured by . Examples are INT32_MAX + 1 (overflow) and INT32_MIN - 1 (underflow); a familiar asymmetric case is -INT32_MIN, which cannot be represented because .

For widths i8 through i64 the argument of [5] applies unchanged: the signed integers of width embed into the signed integers of width by a ring homomorphism, so we lift into the wider arithmetic and compare against the bounds of the narrower ring. In the i128 case there is no wider native arithmetic to lift into, and the unsigned division trick must account for sign. Working in absolute values, overflow occurs iff , where when the signs of and agree and when they differ — the latter accommodating products that land exactly on , which is representable only when the result is negative.

Division and modulo again fall outside the ring operations [5], but for signed arithmetic the safe region is narrowly smaller than in the unsigned case. For and , truncated division places in the closed interval except in the single pair , for which the mathematical quotient is unrepresentable. Two inputs must therefore be rejected: , which is undefined, and the INT_MIN / -1 pair, which overflows. The same pair is rejected for modulo even though mathematically, because the C++ language specifies the result of INT_MIN % -1 as undefined behavior on native types and the library preserves that contract at the type boundary.