The library in subdirectory lib1/ was originally developed by David Russinoff
at Advanced Micro Devices from 1996 to 1998 in support of the mechanical
verification of a number of floating point operations of the AMD-K5 and AMD-K7
microprocessors.  He has updated it (coincidentally with the development of
ACL2 Version 2.5, and with the assistance of Matt Kaufmann) to library lib3/.

Most users should only use lib3/.  Subdirectory lib1/ is included for legacy
reasons; if you previously retrieved a library called "fp" from the Web (under
the ACL2 home page), you will probably be interested to know that its "lib/"
subdirectory corresponds closely to the "lib1/" directory included here.
Future ACL2 releases may have newer libs.  Contributions are welcome.

The files contain virtually no documentation, but most of the interesting
events are formal versions of definitions and lemmas that are stated and proved
in the earlier sections of the following two papers:

  D.M. Russinoff, A mechanically checked proof of correctness of the AMD-K5
  floating point square root microcode</A>, to appear in Formal Methods in
  System Design 14, 75-125 (1999).  See
  http://www.onr.com/user/russ/david/fsqrt.html.

  D.M. Russinoff, A Mechanically checked proof of IEEE compliance of the AMD-K7
  floating point multiplication, division, and square root instructions, to
  appear in the London Mathematical Society Journal of Computation and
  Mathematics, (1), pp. 148-200, December, 1998.  See
  http://www.onr.com/user/russ/david/k7-div-sqrt.html.

The original version of the library, lib1/, defines approximately 40 ACL2
functions for manipulating rational numbers as floating point numbers and
contains about 300 useful top-level theorems relating the defined concepts.
All events of interest are collected in the following five ACL2 books:

basic -- properties of basic arithmetic functions: floor, ceiling, exponential,
and remainder

bits -- bit vectors and logical operations

float -- floating point numbers

reps -- floating point formats and representations

round -- floating point rounding

In addition, a sixth book is provided:

brat -- support of binary notation

The book brat plays no role in the library.  It is included here because you
may find it convenient to use binary notation while experimenting with the
library.  You may wish to (include-book "rtl/lib1/brat") to obtain ACL2
:program mode functions for converting between binary rationals and
conventional binary notation, e.g., converting 209/16 to B1101.0001, or vice
versa.  See the comment at the top of /rtl/lib1/brat.lisp.

You can include all of these books using (include-book "rtl/lib1/top").

Library lib3/ extends lib1/ with an additional book:

fadd -- support for reasoning about floating-point addition

Moreover, changes have been made in books basic and bits from lib1/ to lib3/,
primarily to support more automatic application of the lemmas.

Numerous books are present in subdirectory support/.  Their primary purpose is
to support the books in lib1/ and lib3/.