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.

Addition and subtraction share the skeleton and differ only in their indeterminate form. For addition it is the sum of two infinities of opposite sign, inf + (-inf) (7.2.d). Subtraction is the dual under the same clause: inf - inf of like sign is the cancellation that produces a NaN. For each we prove that no_error holds exactly when the native result is finite, overflow exactly when it is , underflow exactly when it is , invalid_op exactly on a signaling operand or the infinity form above, and nan_op exactly on a quiet NaN operand with no signaling operand present.

These branch characterizations are then tied to the real numbers. When two finite operands have an exact real sum that leaves the representable range, the result is reported as overflow if that sum is positive and underflow if it is negative. When the exact sum is representable the operation is never flagged, and the value delivered equals that sum rounded to nearest, so the safe layer neither rejects a computation that fits nor perturbs the value a bare float or double would have produced.

Multiplication carries the same skeleton with its own indeterminate form, the product of a zero and an infinity in either order, 0 * inf or inf * 0 (7.2.c). The five branch characterizations hold as for addition. The soundness statements change in one respect: the sign of a product follows the signs of its operands rather than the sign of a sum, so a genuine overflow of finite operands is reported as overflow when the operands share a sign and as underflow when their signs differ. A product that is representable is delivered as the correctly rounded exact product.

Division introduces the sixth category. Its indeterminate forms are the two undefined quotients 0.0 / 0.0 and inf / inf, both invalid_op (7.2.b). Separate from these is the division of a finite nonzero dividend by zero, which the standard signals as divideByZero (7.3) and which the classifier reports as divide_by_zero; that case produces an infinity, and we prove that it does. The zero test here is a true-zero test rather than a comparison against 0.0, so a subnormal divisor flushed to zero under a denormals-are-zero (DAZ) mode is not mistaken for a genuine zero.

Because a finite nonzero dividend over zero produces an infinity yet is reported as divide_by_zero, the overflow and underflow results for division are stated as implications rather than equivalences: overflow still implies a result and underflow a result, but a positive infinity no longer implies overflow. Soundness returns against the reals once the divisor is constrained to be nonzero: a finite computation that overflows the range is overflow when the operands share a sign and underflow when their signs differ, and a quotient that is representable is delivered as the correctly rounded exact quotient.

The comparison operators are modeled on operator<⇒, whose result type is std::partial_ordering, so the model is a four-valued ordering: less, greater, equivalent, and unordered. Any NaN operand compares unordered, and only a NaN operand does, which is the whole reason the ordering is partial rather than total. With both operands non-NaN the comparison is less, greater, or equivalent according to the ordered IEEE comparison. Alongside the ordering we prove the properties of operator== as the IEEE equality: it is false whenever either operand is a NaN, it is reflexive on every non-NaN value, and it holds between and . On finite operands equality and the ordering agree, with x == y exactly when the two compare equivalent.

The branch characterizations above are settled entirely within the backend provers' built-in floating-point theory, since they speak only of the format’s own predicates. The soundness and correctness statements cross out of that theory into reasoning about the real-valued result and its rounding, which is discharged separately. Two modeling choices are deliberately left to the library’s test suite rather than the proof: a signaling NaN is modeled abstractly as a NaN refining the quiet case, so the fidelity of the bit-level signaling test is a testing obligation, and the denormals-are-zero behavior folded into the true-zero test is a bit-level concern outside the real-number model. Both formats, binary32 (f32) and binary64 (f64), are covered by the identical development.