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 +++++++++++++++++++++++---------------------------- 1 file changed, 23 insertions(+), 28 deletions(-) (limited to 'src/CLI.v') 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; ""] -- cgit v1.2.3