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 | ∞

3 files changed, 236 insertions, 44 deletions

diff --git a/src/CLI.v b/src/CLI.v
index 329937fc4..dc352d9b2 100644
--- a/src/CLI.v
+++ b/src/CLI.v
@@ -6,6 +6,7 @@ Require Import Coq.Strings.String.
 Require Crypto.Util.Strings.String.
 Require Import Crypto.Util.Strings.Decimal.
 Require Import Crypto.Util.Strings.HexString.
+Require Import Crypto.Util.Strings.ParseArithmetic.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Strings.Show.
 Require Import Crypto.PushButtonSynthesis.
@@ -82,6 +83,8 @@ Module ForExtraction.
 
   Definition parse_machine_wordsize (s : string) : Z
     := parse_Z s.
+  Definition parse_m (s : string) : option Z
+    := parseZ_arith s.
 
   Local Open Scope string_scope.
   Local Notation NewLine := (String "010" "") (only parsing).
@@ -127,6 +130,8 @@ Module ForExtraction.
     := "  s                       The largest component of the prime (e.g., '2^255' in '2^255-19')".
   Definition c_help
     := "  c                       The semi-colon separated list of taps, each of which is specified as weight,value (no parentheses) (e.g., '2^96,1;1,-1' in '2^224 - 2^96 + 1')".
+  Definition m_help
+    := "  m                       The prime (e.g., '2^434 - (2^216*3^137 - 1)')".
   Definition machine_wordsize_help
     := "  machine_wordsize        The machine bitwidth (e.g., 32 or 64)".
   Definition function_to_synthesize_help (valid_names : string)
@@ -247,38 +252,31 @@ Module ForExtraction.
   Module WordByWordMontgomery.
     Definition PipelineLines
                (curve_description : string)
-               (s : string)
-               (c : string)
+               (m : string)
                (machine_wordsize : string)
                (requests : list string)
     : list (string * Pipeline.ErrorT (list string)) + list string
       := let prefix := ("fiat_" ++ curve_description ++ "_")%string in
          let str_machine_wordsize := machine_wordsize in
-         let str_c := c in
-         let str_s := s in
+         let str_m := m in
          let machine_wordsize := parse_machine_wordsize machine_wordsize in
          let show_requests := match requests with nil => "(all)" | _ => String.concat ", " requests end in
-         match parse_s s, parse_c c with
-         | None, None
-           => inr ["Could not parse s (" ++ s ++ ") nor c (" ++ c ++ ")"]
-         | None, _
-           => inr ["Could not parse s (" ++ s ++ ")"]
-         | _, None
-           => inr ["Could not parse c (" ++ c ++ ")"]
-         | Some s, Some c
+         match parse_m m with
+         | None
+           => inr ["Could not parse m (" ++ m ++ ")"]
+         | Some m
            => let '(res, types_used)
-                 := WordByWordMontgomery.Synthesize s c machine_wordsize prefix requests in
+                  := WordByWordMontgomery.Synthesize m machine_wordsize prefix requests in
              let header :=
                  ((["/* Autogenerated */";
                        "/* curve description: " ++ curve_description ++ " */";
                        "/* requested operations: " ++ show_requests ++ " */";
-                       "/* s = " ++ Hex.show_Z false s ++ " (from """ ++ str_s ++ """) */";
-                       "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */";
+                       "/* m = " ++ Hex.show_Z false m ++ " (from """ ++ str_m ++ """) */";
                        "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */";
                        "/*                                                                    */";
                        "/* 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.                                                   */";
@@ -288,19 +286,18 @@ Module ForExtraction.
              inl
                ([("check_args" ++ NewLine ++ String.concat NewLine header,
                   WordByWordMontgomery.check_args
-                    s c machine_wordsize
+                    m machine_wordsize
                     (ErrorT.Success header))%string]
                   ++ res)%list
          end.
 
     Definition ProcessedLines
                (curve_description : string)
-               (s : string)
-               (c : string)
+               (m : string)
                (machine_wordsize : string)
                (requests : list string)
       : list string + list string
-      := match CollectErrors (PipelineLines curve_description s c machine_wordsize requests) with
+      := match CollectErrors (PipelineLines curve_description m machine_wordsize requests) with
          | inl ls
            => inl
                (List.map (fun s => String.concat NewLine s ++ NewLine ++ NewLine)
@@ -315,14 +312,13 @@ Module ForExtraction.
     Definition Pipeline
                {A}
                (curve_description : string)
-               (s : string)
-               (c : string)
+               (m : string)
                (machine_wordsize : string)
                (requests : list string)
                (success : list string -> A)
                (error : list string -> A)
       : A
-      := match ProcessedLines curve_description s c machine_wordsize requests with
+      := match ProcessedLines curve_description m machine_wordsize requests with
          | inl s => success s
          | inr s => error s
          end.
@@ -334,18 +330,17 @@ Module ForExtraction.
                (error : list string -> A)
       : A
       := match argv with
-         | _::curve_description::s::c::machine_wordsize::requests
+         | _::curve_description::m::machine_wordsize::requests
            => Pipeline
-               curve_description s c machine_wordsize requests
+               curve_description m machine_wordsize requests
                success
                error
          | nil => error ["empty argv"]
          | prog::args
-           => error ["Expected arguments curve_description, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog;
+           => error ["Expected arguments curve_description, m, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog;
                        "";
                        curve_description_help;
-                       s_help;
-                       c_help;
+                       m_help;
                        machine_wordsize_help;
                        function_to_synthesize_help WordByWordMontgomery.valid_names;
                        ""]
diff --git a/src/PushButtonSynthesis.v b/src/PushButtonSynthesis.v
index c8e1e97df..b16f62a7f 100644
--- a/src/PushButtonSynthesis.v
+++ b/src/PushButtonSynthesis.v
@@ -1488,12 +1488,12 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
   Local Opaque expr.Interp.
 
   Section __.
-    Context (s : Z)
-            (c : list (Z * Z))
+    Context (m : Z)
             (machine_wordsize : Z).
 
+    Let s := 2^Z.log2_up m.
+    Let c := [(1, s - m)].
     Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)).
-    Let m := s - Associational.eval c.
     Let r := 2^machine_wordsize.
     Let r' := match Z.modinv r m with
               | Some r' => r'
@@ -1510,7 +1510,7 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
       := Partition.partition (weight 8 1) n_bytes (s-1).
     Let upperbounds : list Z := prime_upperbound_list.
     Definition prime_bound : ZRange.type.option.interp (base.type.Z)
-      := Some r[0~>(s - Associational.eval c - 1)]%zrange.
+      := Some r[0~>m-1]%zrange.
     Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z))
       := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list).
     Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z))
@@ -1519,7 +1519,7 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
     Local Notation saturated_bounds := (saturated_bounds n machine_wordsize).
 
     Definition m_enc : list Z
-      := encode (UniformWeight.uweight machine_wordsize) n s c (s-Associational.eval c).
+      := encode (UniformWeight.uweight machine_wordsize) n s c m.
 
     Definition possible_values_of_machine_wordsize
       := [1; machine_wordsize; 2 * machine_wordsize]%Z.
@@ -1540,19 +1540,17 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
            (fun '(b, e) k => if b:bool then Error e else k)
            res
            [(negb (1 <? machine_wordsize)%Z, Pipeline.Value_not_ltZ "machine_wordsize <= 1" 1 machine_wordsize);
-              ((negb (0 <? Associational.eval c))%Z, Pipeline.Value_not_ltZ "Associational.eval c ≤ 0" 0 (Associational.eval c));
-              ((negb (Associational.eval c <? s))%Z, Pipeline.Value_not_ltZ "s ≤ Associational.eval c" (Associational.eval c) s);
-              ((s =? 0)%Z, Pipeline.Values_not_provably_distinctZ "s = 0" s 0);
+              ((negb (0 <? Associational.eval c))%Z, Pipeline.Value_not_ltZ "c ≤ 0" 0 (Associational.eval c));
+              ((negb (1 <? m))%Z, Pipeline.Value_not_ltZ "m ≤ 1" 1 m);
               ((n =? 0)%nat, Pipeline.Values_not_provably_distinctZ "n = 0" n 0%nat);
               ((r' =? 0)%Z, Pipeline.No_modular_inverse "r⁻¹ mod m" r m);
               (negb ((r * r') mod m =? 1)%Z, Pipeline.Values_not_provably_equalZ "(r * r') mod m ≠ 1" ((r * r') mod m) 1);
               (negb ((m * m') mod r =? (-1) mod r)%Z, Pipeline.Values_not_provably_equalZ "(m * m') mod r ≠ (-1) mod r" ((m * m') mod r) ((-1) mod r));
               (negb (s <=? r^n), Pipeline.Value_not_leZ "r^n ≤ s" s (r^n));
-              (negb (1 <? s - Associational.eval c), Pipeline.Value_not_ltZ "s - Associational.eval c ≤ 1" 1 (s - Associational.eval c));
-              (negb (s =? 2^Z.log2 s), Pipeline.Values_not_provably_equalZ "s ≠ 2^log2(s) (needed for from_bytes)" s (2^Z.log2 s));
               (negb (s <=? UniformWeight.uweight machine_wordsize n), Pipeline.Value_not_leZ "weight n < s (needed for from_bytes)" s (UniformWeight.uweight machine_wordsize n));
               (negb (UniformWeight.uweight machine_wordsize n =? UniformWeight.uweight 8 n_bytes), Pipeline.Values_not_provably_equalZ "weight n ≠ bytes_weight n_bytes (needed for from_bytes)" (UniformWeight.uweight machine_wordsize n) (UniformWeight.uweight 8 n_bytes))].
 
+    Local Arguments Z.mul !_ !_.
     Local Ltac use_curve_good_t :=
       repeat first [ assumption
                    | progress rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *
@@ -1565,14 +1563,17 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
                    | progress cbv [Qle] in *
                    | progress cbn -[reify_list] in *
                    | progress intros
-                   | solve [ auto ] ].
+                   | solve [ auto with zarith ]
+                   | rewrite Z.log2_pow2 by use_curve_good_t ].
 
     Context (curve_good : check_args (Success tt) = Success tt).
 
     Lemma use_curve_good
-      : Z.pos (Z.to_pos m) = s - Associational.eval c
+      : Z.pos (Z.to_pos m) = m
+        /\ m = s - Associational.eval c
         /\ Z.pos (Z.to_pos m) <> 0
         /\ s - Associational.eval c <> 0
+        /\ 0 < s
         /\ s <> 0
         /\ 0 < machine_wordsize
         /\ n <> 0%nat
@@ -1605,7 +1606,9 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
              | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ]
              end.
       repeat apply conj.
-      { destruct (s - Associational.eval c) eqn:?; cbn; lia. }
+      { destruct m eqn:?; cbn; lia. }
+      { use_curve_good_t. }
+      { use_curve_good_t. }
       { use_curve_good_t. }
       { use_curve_good_t. }
       { use_curve_good_t. }
@@ -1860,7 +1863,7 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
       intros [v1 v0]; cbn [fst snd].
       rename x into x'.
       generalize dependent (eval (n:=n') lgr x').
-      cbv [m].
+      replace m with (s - Associational.eval c) in * by easy.
       intro x; intros ??? H; subst x'.
       eapply In_nth_error in H; destruct H as [i H].
       rewrite nth_error_combine in H.
@@ -1942,11 +1945,11 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very
       cbv [bytes_valid] in H.
       destruct H as [_ H].
       pose proof use_curve_good.
-      cbv [m UniformWeight.uweight] in *; destruct_head'_and; lia.
+      cbv [UniformWeight.uweight] in *; destruct_head'_and; lia.
     Qed.
 
     Local Ltac solve_extra_bounds_side_conditions :=
-      solve [ cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; cbv [m] in *; lia
+      solve [ cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia
             | cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto
             | now apply weight_bounded_of_bytes_valid
             | eapply length_of_valid; eassumption ].
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.