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 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
If , then for all positive rationals and and positive integers and ,
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