diff options
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | README.md | 15 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/CLI.v | 45 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 13 |
4 files changed, 67 insertions, 9 deletions
@@ -545,8 +545,9 @@ $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%.hs) : %.hs : %.v $(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp $(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp | sed -f src/Experiments/NewPipeline/haskell.sed > $@ && rm -f $@.tmp +# pass -w -20 to disable the unused argument warning $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) : % : %.ml - $(TIMER_FULL) ocamlopt -o $@ $< + $(TIMER_FULL) ocamlopt -w -20 -o $@ $< $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) : % : %.hs $(TIMER_FULL) $(GHC) $(GHCFLAGS) -o $@ $< @@ -31,13 +31,15 @@ The binaries generating these C files can be made with make standalone +or `make standalone-haskell` or `make standalone-ocaml` for binaries generated with just one compiler. + The binaries are located in src/Experiments/NewPipeline/ExtractionOCaml/ or - src/Experiments/NewPipeline/ExtractionOCaml/ + src/Experiments/NewPipeline/ExtractionHaskell/ The binaries are: @@ -45,8 +47,17 @@ The binaries are: - `unsaturated_solinas` - `word_by_word_montgomery` -See the Makefile for examples of how to invoke these binaries. +Passing no arguments, or passing `-h` or `--help` (or any other invalid arguments) will result in a usage message being printed. These binaries output C code on stdout. + +Here are some examples of ways to invoke the binaries (from the directories that they live in): + + # Generate code for 2^255-19 + ./unsaturated_solinas '25519' '5' '2^255' '1,19' '64' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c + ./unsaturated_solinas '25519' '10' '2^255' '1,19' '32' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c + # Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1) + ./word_by_word_montgomery 'p256' '2^256' '2^224,1;2^192,-1;2^96,-1;1,1' '32' > p256_32.c + ./word_by_word_montgomery 'p256' '2^256' '2^224,1;2^192,-1;2^96,-1;1,1' '64' > p256_64.c Old Pipeline ---- 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). |