From 08222f8c6228eaf3a6be44c4dbdca066813efd8c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 13 Jan 2019 04:42:03 -0500 Subject: Autocompute s and c in WBW Montgomery MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | ∞ --- src/Util/Strings/ParseArithmetic.v | 194 +++++++++++++++++++++++++++++++++++++ 1 file changed, 194 insertions(+) create mode 100644 src/Util/Strings/ParseArithmetic.v (limited to 'src/Util') 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. -- cgit v1.2.3