Floating point verification in HOL Light: the exponential function

Technical Report 428, University of Cambridge Computer Laboratory.

Abstract:

In that they often embody compact but mathematically sophisticated algorithms, operations for computing the common transcendental functions in floating point arithmetic seem good targets for formal verification using a mechanical theorem prover. We discuss some of the general issues that arise in verifications of this class, and then present a machine-checked verification of an algorithm for computing the exponential function in IEEE-754 standard binary floating point arithmetic. We confirm (indeed strengthen) the main result of a previously published error analysis, though we uncover a minor error in the hand proof and are forced to confront several subtle issues that might easily be overlooked informally.

Our main theorem connects the floating point exponential to its abstract mathematical counterpart. The specification we prove is that the function has the correct overflow behaviour and, in the absence of overflow, the error in the result is less than 0.54 units in the last place (0.77 if the answer is denormalized) compared against the exact mathematical exponential function. The algorithm is expressed in a simple formalized programming language, intended to be a subset of real programming and hardware description languages. It uses underlying floating point operations (addition, multiplication etc.) that are assumed to conform to the IEEE-754 standard for binary floating point arithmetic.

The development described here includes, apart from the proof itself, a formalization of IEEE arithmetic, a mathematical semantics for the programming language in which the algorithm is expressed, and the body of pure mathematics needed. All this is developed logically from first principles using the HOL Light prover, which guarantees strict adherence to simple rules of inference while allowing the user to perform proofs using higher-level derived rules. We first present the main ideas and conclusions, and then collect some technical details about the prover and the underlying mathematical theories in appendices.

DVI or PostScript or PDF

Short version without appendices: DVI or PostScript

Shorter version still, to appear in AMAST: DVI or PostScript

Bibtex entry:

@TECHREPORT{harrison-style,
        author          = "John Harrison",
        title           = "Floating point verification in {HOL} {L}ight:
                           the exponential function",
        institution     = "University of Cambridge Computer Laboratory",
        address         = "New Museums Site, Pembroke Street,
                           Cambridge, CB2 3QG, UK",
        year            = 1997,
        type            = "Technical Report",
        number          = 428,
        note            = "Available on the Web as
 {\verb+http://www.cl.cam.ac.uk/~jrh13/papers/tang.html+}"}