Correctly Rounded mathematical library

CRlibm, an efficient and proven correctly-rounded mathematical library

CRlibm is a free mathematical library (libm) which provides:

  • implementations of the double-precision C99 standard elementary functions,

  • correctly rounded in the four IEEE-754 rounding modes,

  • with a comprehensive proof of both the algorithms used and their implementation,

  • sufficiently efficient in average time, worst-case time, and memory consumption to replace existing libms transparently,

CRlibm is distributed under the GNU Lesser General Public License (LGPL).

Included in the distribution is an extensive documentation with the proof of each function (currently more than 100 pages), as well as all the Maple scripts used to develop the functions. This makes this library an excellent tutorial on software elementary function development.

The CRlibm library also includes a lightweight library for multiple precision, scslib (Software Carry Save Library). This library has been developed specifically to answer the needs of the CRlibm project: precision up to a few hundred bits, portability, compatibility with IEEE floating-point, performance comparable to or better than GMP, small footprint. It uses a data-structure which allows to avoid carry propagations during multiple-precision multiplications. Supported operations are essentially addition/subtraction and multiplication, and conversions. This library is independent from CRlibm.