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/CLI.v | 51 +++++----- src/PushButtonSynthesis.v | 35 ++++--- src/Util/Strings/ParseArithmetic.v | 194 +++++++++++++++++++++++++++++++++++++ 3 files changed, 236 insertions(+), 44 deletions(-) create mode 100644 src/Util/Strings/ParseArithmetic.v (limited to 'src') 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 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. -- cgit v1.2.3