Update README.md

README.md

 # WhyMP
 
-WhyMP  is an arbitrary-precision integer library for C that is inspired by GMP, implemented in WhyML, and formally verified using Why3.
\ No newline at end of file
+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](https://gmplib.org/manual/Low_002dlevel-Functions.html). 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
+
+You may regenerate the C sources of the library using the most recent version of Why3.
+To do so, clone [the master branch of Why3](https://gitlab.inria.fr/why3/why3), and then use the following commands:
+
+    ./autogen.sh
+    ./configure --enable-local && make
+    cd examples/multiprecision
+    PATH=../../bin:$PATH make dist
+
+![Overview of the project as a graph](img/over-1.png "Overview of the project as a graph")
+
+## 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
+
+```c
+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.
\ No newline at end of file