7 IEEE-Compliant Square Root

Most of the results listed in Chapters 1, 4, and 6 are propositions pertaining to real variables, which are formalized by ACL2 events in which these variables are restricted to the rational domain. Many of the lemmas of this chapter similarly apply to arbitrary real numbers, but in light of its focus, these results are formulated to correspond more closely with their formal versions. Apart from the informal discussion below, the lemmas themselves contain no references to the real numbers or the square root function.

Establishing IEEE compliance of a floating-point square root module entails proving that the final value computed for a given radicand , rounding mode , and precision satisfies

We would like to formulate a proposition of rational arithmetic that is transparently equivalent to (7.1). This requirement is satisfied by the following criterion:

Obviously, the monotonicity of rounding (Lemma 6.5.11) ensures that (7.1) implies (7.2). On the other hand, suppose that (7.2) holds. According to Lemma 6.5.16, either is -exact (and, in particular, rational) or for some , for all satisfying . In either case, there exist and such that and . Since ,

We would also like to prove formally that (7.2) is satisfied by the value computed by any module of interest. For this purpose, it will be useful to have a function that computes, for given and , a rational number that satisfies

We shall define a conceptually simple (albeit computationally horrendous) rational function

where , then (7.3) holds for . Of course, (7.4) will not be our formal definition of

*If
, then for all positive rationals and * and positive integers and ,

Thus, in order to prove that a computed value satisfies (7.2), it suffices to show that for some .

Among various other properties of *qsqrt* that are derived in this chapter is one that warrants some motivation.
In practice, a typical implementation of a subtractive square root algorithm produces a final truncated approximation
of and a remainder that provides a comparison between and . A final rounded result is derived from this approximation
in accordance with a given rounding mode and precision . In order to apply (7.5), we would like to show that
for some appropriate . This may be done by invoking Lemma 6.5.20
with and
substituted for and , respectively. But this requires showing that
and determining whether
. Thus, we require a means of converting inequalities relating and to inequalities
relating and
. This is achieved by the following result (Lemma 7.3.6):

*If and are positive rationals and is -exact,*
then