Formal Verification of Fundamental Operations
Taking inspiration from efforts to verify selected integer operations in GMP (See: 7 and 8), we seek to formally verify the behavior of our library so that the term "safe" has more meaning. As noted in the design decisions, type coercion is a compiler error. This restricts all operations to endomorphisms on a fixed residue class, rather than the more general which comes with complications as is implicit widening, and is implicit narrowing. With this restriction we can more readily perform verification of the library. We use the Why3 platform to conduct our program verification.
Unsigned Integers
Addition and Subtraction
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.
Multiplication
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
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.