diff options
author | Jason Gross <jgross@mit.edu> | 2019-01-13 04:42:03 -0500 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2019-01-14 11:25:10 -0800 |
commit | 08222f8c6228eaf3a6be44c4dbdca066813efd8c (patch) | |
tree | 437fe03546bdfff932bad932904264cadc93effb /src/CLI.v | |
parent | fa3ae820b785c2d98248bf805c76acfd7cc47e17 (diff) |
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 | ∞
Diffstat (limited to 'src/CLI.v')
-rw-r--r-- | src/CLI.v | 51 |
1 files changed, 23 insertions, 28 deletions
@@ -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; ""] |