Add better computation of carry chain

We port the computation of the carry chain from generate_parameters.py
to Coq, for unsaturated solinas.

Note that while we now bounds-check p448, we do not yet support
goldilocks nor karatsuba.

However, there is still an issue with the synthesized p448 code, which
is that on 64-bit, it tries to use 256-bit and 512-bit integers.  I'm
not sure what's up with that.

Partial progress towards #507

After    | File Name                                    | Before   || Change    | % Change
------------------------------------------------------------------------------------------
8m51.64s | Total                                        | 8m34.60s || +0m17.04s | +3.31%
------------------------------------------------------------------------------------------
0m15.16s | p448_solinas_64.c                            |   N/A    || +0m15.16s | ∞
3m09.12s | p384_32.c                                    | 3m09.36s || -0m00.24s | -0.12%
0m44.99s | ExtractionHaskell/word_by_word_montgomery    | 0m44.91s || +0m00.08s | +0.17%
0m39.58s | p521_32.c                                    | 0m39.22s || +0m00.35s | +0.91%
0m32.54s | p521_64.c                                    | 0m32.49s || +0m00.04s | +0.15%
0m30.87s | ExtractionHaskell/unsaturated_solinas        | 0m31.04s || -0m00.16s | -0.54%
0m24.31s | ExtractionHaskell/saturated_solinas          | 0m24.32s || -0m00.01s | -0.04%
0m18.62s | PushButtonSynthesis/UnsaturatedSolinas.vo    | 0m17.90s || +0m00.72s | +4.02%
0m17.53s | ExtractionOCaml/word_by_word_montgomery      | 0m17.44s || +0m00.08s | +0.51%
0m13.36s | secp256k1_32.c                               | 0m13.58s || -0m00.22s | -1.62%
0m13.21s | p256_32.c                                    | 0m13.15s || +0m00.06s | +0.45%
0m11.47s | p484_64.c                                    | 0m11.39s || +0m00.08s | +0.70%
0m11.27s | ExtractionOCaml/unsaturated_solinas          | 0m10.71s || +0m00.55s | +5.22%
0m10.48s | ExtractionOCaml/word_by_word_montgomery.ml   | 0m10.34s || +0m00.14s | +1.35%
0m07.97s | ExtractionOCaml/saturated_solinas            | 0m07.98s || -0m00.01s | -0.12%
0m07.05s | ExtractionOCaml/unsaturated_solinas.ml       | 0m06.98s || +0m00.06s | +1.00%
0m06.58s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.48s || +0m00.09s | +1.54%
0m06.09s | p224_32.c                                    | 0m06.04s || +0m00.04s | +0.82%
0m05.24s | p384_64.c                                    | 0m05.34s || -0m00.09s | -1.87%
0m05.13s | ExtractionOCaml/saturated_solinas.ml         | 0m05.19s || -0m00.06s | -1.15%
0m05.00s | ExtractionHaskell/unsaturated_solinas.hs     | 0m04.98s || +0m00.01s | +0.40%
0m04.14s | ExtractionHaskell/saturated_solinas.hs       | 0m04.04s || +0m00.09s | +2.47%
0m02.22s | curve25519_32.c                              | 0m02.22s || +0m00.00s | +0.00%
0m01.49s | curve25519_64.c                              | 0m01.53s || -0m00.04s | -2.61%
0m01.46s | CLI.vo                                       | 0m01.44s || +0m00.02s | +1.38%
0m01.29s | SlowPrimeSynthesisExamples.vo                | 0m01.24s || +0m00.05s | +4.03%
0m01.08s | p256_64.c                                    | 0m01.00s || +0m00.08s | +8.00%
0m01.06s | StandaloneOCamlMain.vo                       | 0m00.96s || +0m00.10s | +10.41%
0m01.06s | secp256k1_64.c                               | 0m01.17s || -0m00.10s | -9.40%
0m01.02s | p224_64.c                                    | 0m01.08s || -0m00.06s | -5.55%
0m00.99s | StandaloneHaskellMain.vo                     | 0m01.08s || -0m00.09s | -8.33%
0m00.27s | TAPSort.vo                                   |   N/A    || +0m00.27s | ∞

1 files changed, 1 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 23bccf874..202362476 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,6 +44,7 @@ src/RewriterWf2.v
 src/SlowPrimeSynthesisExamples.v
 src/StandaloneHaskellMain.v
 src/StandaloneOCamlMain.v
+src/TAPSort.v
 src/UnderLets.v
 src/UnderLetsProofs.v
 src/Algebra/Field.v