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, 194 insertions, 0 deletions

diff --git a/src/Util/Strings/ParseArithmetic.v b/src/Util/Strings/ParseArithmetic.v
new file mode 100644
index 000000000..2ae6ea347
--- /dev/null
+++ b/src/Util/Strings/ParseArithmetic.v
@@ -0,0 +1,194 @@
+Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List.
+Require Import Coq.Numbers.BinNums.
+Require Import Coq.ZArith.BinInt.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Strings.Equality.
+Require Import Crypto.Util.Strings.Decimal.
+Require Import Crypto.Util.Notations.
+Import ListNotations.
+Import BinPosDef.
+Local Open Scope option_scope.
+Local Open Scope list_scope.
+Local Open Scope char_scope.
+Local Open Scope string_scope.
+
+Definition is_num (ch : ascii) : bool
+  := (ascii_beq ch "0"
+      || ascii_beq ch "1"
+      || ascii_beq ch "2"
+      || ascii_beq ch "3"
+      || ascii_beq ch "4"
+      || ascii_beq ch "5"
+      || ascii_beq ch "6"
+      || ascii_beq ch "7"
+      || ascii_beq ch "8"
+      || ascii_beq ch "9")%bool.
+
+Fixpoint split_before_first (f : ascii -> bool) (s : string) : string * string
+  := match s with
+     | EmptyString => (EmptyString, EmptyString)
+     | String ch rest
+       => if f ch
+          then (EmptyString, s)
+          else let '(s1, s2) := split_before_first f rest in
+               (String ch s1, s2)
+     end.
+
+Definition parse_N (s : string) : option (N * string)
+  := let '(n, rest) := split_before_first (fun ch => negb (is_num ch)) s in
+     match Z_of_decimal_string n, Nat.eqb (String.length n) 0 with
+     | Zneg _, _ | _, true => None
+     | Z0, _ => Some (N0, rest)
+     | Zpos p, _ => Some (Npos p, rest)
+     end.
+
+Definition parse_ch {T} (ls : list (ascii * T)) (s : string) : option (T * string)
+  := match s with
+     | EmptyString => None
+     | String ch s
+       => List.fold_right
+            (fun '(ch', t) default
+             => if ascii_beq ch ch' then Some (t, s) else default)
+            None
+            ls
+     end.
+
+Inductive plus_or_minus := PLUS | MINUS.
+Inductive mul_or_div := MUL | DIV.
+
+Definition parse_plus_or_minus := parse_ch [("+", PLUS); ("-", MINUS)]%char.
+Definition parse_mul_or_div := parse_ch [("*", MUL); ("/", DIV)]%char.
+Definition parse_open := parse_ch [("(", tt)]%char.
+Definition parse_close := parse_ch [(")", tt)]%char.
+Definition parse_pow := parse_ch [("^", tt)]%char.
+
+Delimit Scope parse_scope with parse.
+
+Definition maybe_parse {A} (parse : string -> option (A * string))
+           (s : string)
+  : option (option A * string)
+  := Some match parse s with
+          | Some (a, rest) => (Some a, rest)
+          | None => (None, s)
+          end.
+Global Arguments maybe_parse {A%type} parse%parse s%string.
+
+Definition bind_parse {A B} (parse_A : string -> option (A * string))
+           (parse_B : A -> string -> option (B * string))
+           (s : string)
+  : option (B * string)
+  := (a <- parse_A s;
+        let '(a, s) := a in
+        parse_B a s).
+Global Arguments bind_parse {A B}%type (parse_A parse_B)%parse s%string.
+
+Definition ret {A} (a : A) (s : string) : option (A * string)
+  := Some (a, s).
+
+Definition orelse {A}
+           (parse parse' : string -> option (A * string))
+           (s : string)
+  : option (A * string)
+  := match parse s with
+     | Some v => Some v
+     | None => parse' s
+     end.
+Global Arguments orelse {A%type} (parse parse')%parse s%string.
+
+Local Open Scope parse_scope.
+Notation "a <- parse_A ; parse_B" := (bind_parse parse_A%parse (fun a => parse_B%parse)) : parse_scope.
+Notation "?" := maybe_parse : parse_scope.
+Infix "||" := orelse : parse_scope.
+
+Fixpoint parse_Z (s : string) : option (Z * string)
+  := match s with
+     | String ch rest
+       => if ascii_beq ch "+"
+          then parse_Z rest
+          else if ascii_beq ch "-"
+               then match parse_Z rest with
+                    | Some (z, s) => Some (-z, s)%Z
+                    | None => None
+                    end
+               else match parse_N s with
+                    | Some (v, s) => Some (Z.of_N v, s)
+                    | None => None
+                    end
+     | EmptyString => None
+     end.
+
+Fixpoint parseZ_op_fueled
+         (ops : list (ascii * (Z -> Z -> Z)))
+         (prev_parse : string -> option (Z * string))
+         (fuel : nat) (acc : Z) : string -> option (Z * string)
+  := match fuel with
+     | O => ret acc
+     | S fuel'
+       => (op <- parse_ch ops;
+             z <- prev_parse;
+             let acc := op acc z in
+             parseZ_op_fueled ops prev_parse fuel' acc)
+          || ret acc
+     end.
+
+Definition parseZ_op_from_acc
+         (ops : list (ascii * (Z -> Z -> Z)))
+         (prev_parse : string -> option (Z * string))
+         (acc : Z) (s : string) : option (Z * string)
+  := parseZ_op_fueled ops prev_parse (String.length s) acc s.
+
+Definition parseZ_op
+         (ops : list (ascii * (Z -> Z -> Z)))
+         (prev_parse : string -> option (Z * string))
+  : string -> option (Z * string)
+  := acc <- prev_parse;
+       parseZ_op_from_acc ops prev_parse acc.
+
+Fixpoint parseZ_parens_fueled
+         (prev_parse : string -> option (Z * string))
+         (fuel : nat) : string -> option (Z * string)
+  := match fuel with
+     | O => fun _ => None
+     | S fuel'
+       => ((_ <- parse_open;
+              z <- prev_parse;
+              _ <- parse_close;
+              ret z)
+           || parse_Z)
+     end.
+
+Section step.
+  Context (parseZ : string -> option (Z * string)).
+
+  Definition parseZ_parens (s : string) : option (Z * string)
+    := parseZ_parens_fueled parseZ (String.length s) s.
+  Definition parseZ_exp : string -> option (Z * string)
+    := parseZ_op [("^", Z.pow)]%char parseZ_parens.
+  Definition parseZ_mul_div : string -> option (Z * string)
+    := parseZ_op [("*", Z.mul); ("/", Z.div)]%char parseZ_exp.
+  Definition parseZ_add_sub : string -> option (Z * string)
+    := parseZ_op [("+", Z.add); ("-", Z.sub)]%char parseZ_mul_div.
+End step.
+
+Fixpoint parseZ_arith_fueled (fuel : nat) : string -> option (Z * string)
+  := match fuel with
+     | O => parseZ_add_sub parse_Z
+     | S fuel' => parseZ_add_sub (parseZ_arith_fueled fuel')
+     end.
+
+Definition parseZ_arith_prefix (s : string) : option (Z * string)
+  := parseZ_arith_fueled (String.length s) s.
+
+Fixpoint remove_spaces (s : string) : string
+  := match s with
+     | EmptyString => EmptyString
+     | String ch s
+       => let s' := remove_spaces s in
+          if ascii_beq ch " " then s' else String ch s'
+     end.
+
+Definition parseZ_arith (s : string) : option Z
+  := match parseZ_arith_prefix (remove_spaces s) with
+     | Some (z, EmptyString) => Some z
+     | _ => None
+     end.