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, 6 insertions, 1 deletions

diff --git a/Makefile b/Makefile
index 9a433d056..3b5f88fef 100644
--- a/Makefile
+++ b/Makefile
@@ -83,7 +83,7 @@ ifneq ($(filter pre-standalone,$(MAKECMDGOALS)),)
 PRE_STANDALONE_VOFILES := $(call vo_closure,$(PRE_STANDALONE_PRE_VOFILES))
 endif
 
-UNSATURATED_SOLINAS_C_FILES := curve25519_64.c curve25519_32.c p521_64.c p521_32.c # p224_solinas_64.c
+UNSATURATED_SOLINAS_C_FILES := curve25519_64.c curve25519_32.c p521_64.c p521_32.c p448_solinas_64.c # p224_solinas_64.c
 WORD_BY_WORD_MONTGOMERY_C_FILES := p256_64.c p256_32.c p384_64.c p384_32.c secp256k1_64.c secp256k1_32.c p224_64.c p224_32.c p484_64.c # p484_32.c
 ALL_C_FILES := $(UNSATURATED_SOLINAS_C_FILES) $(WORD_BY_WORD_MONTGOMERY_C_FILES)
 FUNCTIONS_FOR_25519 := carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes
@@ -219,6 +219,11 @@ p521_32.c:
 #	$(SHOW)'SYNTHESIZE > $@'
 #	$(HIDE)$(TIMER_FULL) $(UNSATURATED_SOLINAS) 'p224' '4' '2^224' '2^96,1;1,-1' '64' > $@
 
+# 2^448 - 2^224 - 1
+p448_solinas_64.c:
+	$(SHOW)'SYNTHESIZE > $@'
+	$(HIDE)$(TIMER_FULL) $(UNSATURATED_SOLINAS) 'p448' '8' '2^448' '2^224,1;1,1' '64' > $@
+
 # 2^256 - 2^224 + 2^192 + 2^96 - 1
 p256_64.c p256_32.c : p256_%.c :
 	$(SHOW)'SYNTHESIZE > $@'