Autocompute s and c in WBW Montgomery

This allows us to support primes which are not a power of 2.

We also add p484 as an example.

To support this, I added a small parser combinator library which can
parse arithmetic expressions involving `()^*/+-` and decimal digits.

Closes #486
Closes #342

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
22m14.42s | Total                                        | 12m14.76s || +9m59.65s | +81.61%
--------------------------------------------------------------------------------------------
9m41.91s  | p484_32.c                                    |    N/A    || +9m41.90s | ∞
0m11.51s  | p484_64.c                                    |    N/A    || +0m11.50s | ∞
3m16.22s  | p384_32.c                                    | 3m12.02s  || +0m04.19s | +2.18%
4m12.18s  | PushButtonSynthesis.vo                       | 4m10.16s  || +0m02.02s | +0.80%
0m45.08s  | ExtractionHaskell/word_by_word_montgomery    | 0m45.24s  || -0m00.16s | -0.35%
0m38.14s  | p521_32.c                                    | 0m38.12s  || +0m00.02s | +0.05%
0m31.80s  | p521_64.c                                    | 0m31.78s  || +0m00.01s | +0.06%
0m31.09s  | ExtractionHaskell/unsaturated_solinas        | 0m30.77s  || +0m00.32s | +1.03%
0m24.18s  | ExtractionHaskell/saturated_solinas          | 0m24.21s  || -0m00.03s | -0.12%
0m17.38s  | ExtractionOCaml/word_by_word_montgomery      | 0m17.35s  || +0m00.02s | +0.17%
0m13.39s  | secp256k1_32.c                               | 0m13.59s  || -0m00.19s | -1.47%
0m13.14s  | p256_32.c                                    | 0m13.04s  || +0m00.10s | +0.76%
0m10.58s  | ExtractionOCaml/unsaturated_solinas          | 0m10.73s  || -0m00.15s | -1.39%
0m10.23s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m10.34s  || -0m00.10s | -1.06%
0m07.88s  | ExtractionOCaml/saturated_solinas            | 0m07.94s  || -0m00.06s | -0.75%
0m06.78s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m06.86s  || -0m00.08s | -1.16%
0m06.28s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s  || -0m00.13s | -2.18%
0m06.00s  | p224_32.c                                    | 0m05.97s  || +0m00.03s | +0.50%
0m05.50s  | p384_64.c                                    | 0m05.35s  || +0m00.15s | +2.80%
0m05.28s  | ExtractionOCaml/saturated_solinas.ml         | 0m05.08s  || +0m00.20s | +3.93%
0m05.10s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m04.98s  || +0m00.11s | +2.40%
0m04.12s  | ExtractionHaskell/saturated_solinas.hs       | 0m04.15s  || -0m00.03s | -0.72%
0m02.14s  | curve25519_32.c                              | 0m02.28s  || -0m00.13s | -6.14%
0m01.44s  | CLI.vo                                       | 0m01.42s  || +0m00.02s | +1.40%
0m01.44s  | curve25519_64.c                              | 0m01.57s  || -0m00.13s | -8.28%
0m01.14s  | StandaloneOCamlMain.vo                       | 0m01.11s  || +0m00.02s | +2.70%
0m01.12s  | p256_64.c                                    | 0m00.98s  || +0m00.14s | +14.28%
0m01.11s  | StandaloneHaskellMain.vo                     | 0m01.17s  || -0m00.05s | -5.12%
0m01.03s  | secp256k1_64.c                               | 0m01.15s  || -0m00.11s | -10.43%
0m01.02s  | p224_64.c                                    | 0m00.99s  || +0m00.03s | +3.03%
0m00.21s  | Util/Strings/ParseArithmetic.vo              |    N/A    || +0m00.21s | ∞

1 files changed, 2 insertions, 3 deletions

diff --git a/p256_32.c b/p256_32.c
index 24b3fe8ca..f75ede5b4 100644
--- a/p256_32.c
+++ b/p256_32.c
@@ -1,13 +1,12 @@
 /* Autogenerated */
 /* curve description: p256 */
 /* requested operations: (all) */
-/* s = 0x10000000000000000000000000000000000000000000000000000000000000000 (from "2^256") */
-/* c = [(26959946667150639794667015087019630673637144422540572481103610249216, 1), (6277101735386680763835789423207666416102355444464034512896, -1), (79228162514264337593543950336, -1), (1, 1)] (from "2^224,1;2^192,-1;2^96,-1;1,1") */
+/* m = 0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff (from "2^256 - 2^224 + 2^192 + 2^96 - 1") */
 /* machine_wordsize = 32 (from "32") */
 /*                                                                    */
 /* NOTE: In addition to the bounds specified above each function, all */
 /*   functions synthesized for this Montgomery arithmetic require the */
-/*   input to be strictly less than the prime modulus (s-c), and also */
+/*   input to be strictly less than the prime modulus (m), and also   */
 /*   require the input to be in the unique saturated representation.  */
 /*   All functions also ensure that these two properties are true of  */
 /*   return values.                                                   */