From c50611790812ba94c052ec51364e13d773d5c64a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Aug 2018 20:56:50 -0400 Subject: Improve documentation of binaries --- src/Experiments/NewPipeline/CLI.v | 45 ++++++++++++++++++++++++++++++--- src/Experiments/NewPipeline/Toplevel1.v | 13 +++++++--- 2 files changed, 52 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/CLI.v b/src/Experiments/NewPipeline/CLI.v index f82d9e2a6..524def965 100644 --- a/src/Experiments/NewPipeline/CLI.v +++ b/src/Experiments/NewPipeline/CLI.v @@ -105,6 +105,21 @@ Module ForExtraction. => inr [res] end. + Definition curve_description_help + := " curve_description A string which will be prefixed to every function name generated". + Definition n_help + := " n The number of limbs". + Definition s_help + := " 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 machine_wordsize_help + := " machine_wordsize The machine bitwidth (e.g., 32 or 64)". + Definition function_to_synthesize_help (valid_names : string) + := " function_to_synthesize A list of functions that should be synthesized. If no functions are given, all functions are synthesized." + ++ String.NewLine ++ + " Valid options are " ++ valid_names. + Module UnsaturatedSolinas. Definition PipelineLines (curve_description : string) @@ -201,8 +216,18 @@ Module ForExtraction. error | nil => error ["empty argv"] | prog::args - => error ["Expected arguments curve_description, n, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog] + => error ["Expected arguments curve_description, n, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog; + ""; + curve_description_help; + n_help; + s_help; + c_help; + machine_wordsize_help; + function_to_synthesize_help UnsaturatedSolinas.valid_names; + ""] end. + + End UnsaturatedSolinas. Module WordByWordMontgomery. @@ -302,7 +327,14 @@ Module ForExtraction. 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, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog; + ""; + curve_description_help; + s_help; + c_help; + machine_wordsize_help; + function_to_synthesize_help WordByWordMontgomery.valid_names; + ""] end. End WordByWordMontgomery. @@ -396,7 +428,14 @@ Module ForExtraction. 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, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog; + ""; + curve_description_help; + s_help; + c_help; + machine_wordsize_help; + function_to_synthesize_help SaturatedSolinas.valid_names; + ""] end. End SaturatedSolinas. End ForExtraction. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 6eeee9f48..3f8da3a1a 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -1893,6 +1893,9 @@ Module Import UnsaturatedSolinas. ("to_bytes", srto_bytes); ("from_bytes", srfrom_bytes)]. + Definition valid_names : string + := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions) ++ ", or 'carry_scmul' followed by a decimal literal". + Definition synthesize_of_name (function_name_prefix : string) (name : string) : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos) := fold_right @@ -1904,7 +1907,7 @@ Module Import UnsaturatedSolinas. ((name, Error (Pipeline.Invalid_argument - ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ String.concat ", " (List.map (@fst _ _) known_functions) ++ ", or 'carry_scmul' followed by a decimal literal.")))) + ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ ".")))) ((map (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None) known_functions) @@ -2967,6 +2970,8 @@ Module WordByWordMontgomery. ("to_bytes", srto_bytes); ("from_bytes", srfrom_bytes)]. + Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions). + Definition synthesize_of_name (function_name_prefix : string) (name : string) : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos) := fold_right @@ -2978,7 +2983,7 @@ Module WordByWordMontgomery. ((name, Error (Pipeline.Invalid_argument - ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ String.concat ", " (List.map (@fst _ _) known_functions))))) + ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ ".")))) (map (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None) known_functions). @@ -3151,6 +3156,8 @@ Module SaturatedSolinas. Definition known_functions := [("mulmod", srmulmod)]. + Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions). + Definition synthesize_of_name (function_name_prefix : string) (name : string) : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos) := fold_right @@ -3162,7 +3169,7 @@ Module SaturatedSolinas. ((name, Error (Pipeline.Invalid_argument - ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ String.concat ", " (List.map (@fst _ _) known_functions) ++ ".")))) + ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ ".")))) (map (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None) known_functions). -- cgit v1.2.3