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
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:
- "How to Get an Efficient yet Verified Arbitrary-Precision Integer Library" by Raphaël Rieu-Helft, Claude Marché and Guillaume Melquiond, published in VSTTE'2017 proceedings, Springer LNCS.
- "A Why3 framework for reflection proofs and its application to GMP's algorithms" by Guillaume Melquiond and Raphaël Rieu-Helft, published in IJCAR'2018 proceedings, Springer LNAI.
Instructions for extraction to C and runnings tests
make extract command to extract and build the C files in the
C compilation requires some GMP headers (the
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 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 export LD_LIBRARY_PATH=$GMP_LIB make plots