## 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:

- "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

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 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