This appendix contains the ACL2 library of floating point arithmetic referred to in the paper A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7^TM processor.

The files contained are:

• README
• add.lisp
• away.lisp
• basic.lisp
• cert.lisp
• divsqrt.lisp
• float.lisp
• floor.lisp
• fp.lisp
• logdefs.lisp
• loglemmas.lisp
• logxor-def.lisp
• logxor-lemmas.lisp
• near.lisp
• odd.lisp
• proofs.lisp
• reps.lisp
• rnd.lisp
• sticky.lisp
• trunc.lisp
• x-2xx.lisp
• lib/basic.lisp
• lib/bits.lisp
• lib/float.lisp
• lib/reps.lisp
• lib/round.lisp
• lib/top.lisp