WhyMP

WhyMP is an arbitrary-precision integer library for C that is inspired by GMP, implemented in WhyML, and formally verified using Why3.

The algorithms are heavily inspired from the mpn layer of the GMP library. The implemented algorithms are addition, subtraction, multiplication (schoolbook and Toom-2), division, square root, and modular exponentiation.

The library is compatible with GMP, and its performance is comparable to its standalone version, mini-gmp. For numbers under about 1000 bits (100,000 for multiplication), it is about 10% slower than the generic, pure-C version of GMP, and about twice as slow as GMP with hand-coded assembly.

Generating the sources

To regenerate the C sources of the library using Why3, go into the why3 submodule, and then use the following commands:

./autogen.sh
./configure --enable-local && make
cd examples/multiprecision
make LOCAL=yes dist

This produces a .tar.gz file containing a standalone C library.

Project overview

We have specified and reimplemented GMP's algorithms in WhyML. To do so, we have developed a simple memory model of the C language in WhyML. This memory model allows us to write WhyML programs in a fragment of the language that is practically a shallow embedding of C.

We have added to Why3 an extraction mechanism from Why3 to C. It only supports WhyML programs that are in the C-like fragment of the language, but the compilation is transparent and does not add inefficiencies that the compiler cannot optimize away. Thus, the resulting C program is easily predictable to the WhyML programmer.

As an example, the WhyML implementation and extracted C version of the comparison function can be found below.

let wmpn_cmp (x y: ptr uint64) (sz: int32): int32 =
  let ref i = sz in
  while i >= 1 do
    i <- i - 1;
    let lx = x[i] in
    let ly = y[i] in
    if lx <> ly then
    if lx > ly
    then return 1
    else return -1
  done;
  0

int32_t wmpn_cmp(uint64_t * x, uint64_t * y, int32_t sz) {
  int32_t i;
  uint64_t lx, ly;
  i = sz;
  while (i >= 1) {
    i = i - 1;
    lx = x[i];
    ly = y[i];
    if (!(lx == ly)) {
      if (lx > ly) { return 1; }
      else { return -1; }
    }
  }
  return 0;
}

The WhyML proofs are about 20,000 lines long in total (for about 5000 lines of extracted C). The split is about 1/3 program code to 2/3 specifications and assertions.