Formally verifying a floating-point division routine with Gappa – part 1

Summary

We have recently released a set of optimized assembly-language routines for basic floating-point arithmetic, in Arm Optimized Routines, under an open-source license. These functions perform the same operations as hardware floating point instructions, for example addition, multiplication, and division. However, they are implemented using only integer 32-bit Arm instructions, for Arm CPUs without hardware floating point. Existing open-source libraries such as libgcc and compiler-rt offer similar functions. Our optimized versions were previously part of the Arm Compiler for Embedded toolchain, which has reached end of life. We are now making them available as open source. Preparing these functions for publication mainly involved polishing the code and rewriting the comments to improve clarity. However, one of them was much more interesting: polishing up the double-precision division function, “ddiv”, as we call it. The task turned into an adventure in formal verification, and ended up finding a bug in the original version. In this two-part blog, I’ll tell the story, and share my learning experiences using Gappa and the Rocq prover. What is “ddiv” and how does it work? The “ddiv” function is implements double-precision floating-point division in accordance with the IEEE 754 standard. It accepts two (64-bit) floating-point numbers as input and gives their quotient as output. Since it only uses integer arithmetic, it treats the inputs and outputs as 64-bit integers. Each integer is divided into three fields: sign, exponent, and mantissa. Floating-point functions require handling many special cases such as NaNs, infinities, denormalized numbers, overflow, underflow, and signed zeroes. Division also requires handling dividing by zero. However, this discussion focuses on ordinary cases, where nothing strange happens. In these ordinary cases, the signs and exponents of the input number are easy to deal with. The primary challenge is the mantissas. Each input mantissa is effec...