Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic

TL;DR

This paper presents a formally verified method for performing 32- and 64-bit integer division using floating-point arithmetic, addressing hardware limitations and enabling more efficient, predictable compiler implementations.

Contribution

It introduces a novel, formally verified algorithm that combines floating-point and integer computations for division, integrated into the CompCert compiler.

Findings

Algorithm is fully proven correct using Coq.

Successfully integrated into the CompCert compiler.

Addresses non-constant time division issues on certain processors.

Abstract

Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead using the processor's floating-point unit, and propose code that the compiler can easily interleave with other computations. We fully proved the correctness of our algorithm, which mixes floating-point and fixed-bitwidth integer computations, using the Coq proof assistant and successfully integrated it into the CompCert formally verified compiler.