Wiki Agenda Contact Version française

An Efficient Arbitrary-Precision Integer Library

An arbitrary-precision integer library in the style of GMP, designed to be both efficient and formally proved correct.

Authors: Raphaël Rieu-Helft

Topics: Arithmetic / Pointer Programs / Proofs by reflection / Non-linear Arithmetic

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

download ZIP archive

This code implements arbitrary-precision integers in the style of GMP. Supported operations are addition, multiplication, division on non-negative integers, and also comparisons and shifts.

For detailed info, see the papers:

Instructions for extraction to C and runnings tests

Execute the make extract command to extract and build the C files in the build subdirectory.

C compilation requires some GMP headers (the longlong.h and config.h headers are used), so an installation of GMP with sources is required to compile it (see here).

To run the tests and benchmarks, you need the source repository rather than only this archive.

The following commands test the library on random inputs and compare the results to GMP for verification:

    export GMP_DIR=/path/to/your/gmp/install
    make tests

To execute the benchmarks, an installation of GMP with assembly disabled is required. First install GMP with assembly disabled in a fresh directory:

    cd /path/to/gmp/sources
    ./configure --disable-assembly --prefix=/where/to/install/gmp
    make install

You are now ready to benchmark the library (gnuplot required to view the plots). The process takes a few minutes.

    export GMP_DIR=/path/to/gmp/sources
    export GMP_LIB=/where/to/install/gmp/lib
    make plots