diff options
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; ""] |