diff --git a/Makefile.config b/Makefile.config index c559c61740e..cac0930e4ae 100644 --- a/Makefile.config +++ b/Makefile.config @@ -50,16 +50,34 @@ else if_SKIP_BEDROCK2 = $(1) endif -BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction -BEDROCK2_STANDALONE := $(addprefix bedrock2_,$(BASE_STANDALONE)) $(addprefix with_bedrock2_,$(BASE_STANDALONE)) -STANDALONE := $(BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_STANDALONE) $(WITH_BEDROCK2_STANDALONE)) +UNIFIED_BASE_STANDALONE := fiat_crypto +SEPARATE_BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction +BASE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(UNIFIED_STANDALONE) +BEDROCK2_UNIFIED_STANDALONE := $(addprefix bedrock2_,$(UNIFIED_BASE_STANDALONE)) $(addprefix with_bedrock2_,$(UNIFIED_BASE_STANDALONE)) +BEDROCK2_SEPARATE_STANDALONE := $(addprefix bedrock2_,$(SEPARATE_BASE_STANDALONE)) $(addprefix with_bedrock2_,$(SEPARATE_BASE_STANDALONE)) +BEDROCK2_STANDALONE := $(BEDROCK2_UNIFIED_STANDALONE) $(BEDROCK2_SEPARATE_STANDALONE) +UNIFIED_STANDALONE := $(UNIFIED_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_UNIFIED_STANDALONE) $(WITH_BEDROCK2_UNIFIED_STANDALONE)) +SEPARATE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_SEPARATE_STANDALONE) $(WITH_BEDROCK2_SEPARATE_STANDALONE)) +STANDALONE := $(UNIFIED_STANDALONE) $(SEPARATE_STANDALONE) PERF_STANDALONE := perf_unsaturated_solinas perf_word_by_word_montgomery -STANDALONE_OCAML := $(STANDALONE) $(PERF_STANDALONE) -STANDALONE_HASKELL := $(STANDALONE) +UNIFIED_STANDALONE_OCAML := $(UNIFIED_STANDALONE) +SEPARATE_STANDALONE_OCAML := $(SEPARATE_STANDALONE) $(PERF_STANDALONE) +STANDALONE_OCAML := $(UNIFIED_STANDALONE_OCAML) $(SEPARATE_STANDALONE_OCAML) +UNIFIED_STANDALONE_HASKELL := $(UNIFIED_STANDALONE) +SEPARATE_STANDALONE_HASKELL := $(SEPARATE_STANDALONE) +STANDALONE_HASKELL := $(UNIFIED_STANDALONE_HASKELL) $(SEPARATE_STANDALONE_HASKELL) -OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/%) -HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/%) +UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/%) +SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/%) +OCAML_BINARIES := $(UNIFIED_OCAML_BINARIES) $(SEPARATE_OCAML_BINARIES) +UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/%) +SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/%) +HASKELL_BINARIES := $(UNIFIED_HASKELL_BINARIES) $(SEPARATE_HASKELL_BINARIES) -WITH_BEDROCK2_OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) -WITH_BEDROCK2_HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%) +UNIFIED_WITH_BEDROCK2_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) +SEPARATE_WITH_BEDROCK2_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) +WITH_BEDROCK2_OCAML_BINARIES := $(UNIFIED_WITH_BEDROCK2_OCAML_BINARIES) $(SEPARATE_WITH_BEDROCK2_OCAML_BINARIES) +UNIFIED_WITH_BEDROCK2_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%) +SEPARATE_WITH_BEDROCK2_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%) +WITH_BEDROCK2_HASKELL_BINARIES := $(UNIFIED_WITH_BEDROCK2_HASKELL_BINARIES) $(SEPARATE_WITH_BEDROCK2_HASKELL_BINARIES) diff --git a/Makefile.standalone b/Makefile.standalone index 2175966a598..ea466028ac7 100644 --- a/Makefile.standalone +++ b/Makefile.standalone @@ -32,10 +32,17 @@ ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true .PHONY: \ perf-standalone \ + standalone-unified install-standalone-unified install-standalone-unified \ + standalone-separate install-standalone-separate uninstall-standalone-separate \ standalone install-standalone uninstall-standalone \ + standalone-unified-ocaml install-standalone-unified-ocaml uninstall-standalone-unified-ocaml \ + standalone-separate-ocaml install-standalone-separate-ocaml uninstall-standalone-separate-ocaml \ standalone-ocaml install-standalone-ocaml uninstall-standalone-ocaml \ + standalone-unified-haskell install-standalone-unified-haskell uninstall-standalone-unified-haskell \ + standalone-separate-haskell install-standalone-separate-haskell uninstall-standalone-separate-haskell \ standalone-haskell install-standalone-haskell uninstall-standalone-haskell \ package-standalone package-standalone-ocaml package-standalone-haskell \ + package-standalone-full package-standalone-full-ocaml package-standalone-full-haskell \ # # pass -w -20 to disable the unused argument warning @@ -55,11 +62,17 @@ $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%) : % : %.hs $(HIDE)$(TIMER) $(GHC) $(GHCFLAGS) -o $@ $< standalone: standalone-haskell standalone-ocaml +standalone-unified: standalone-unified-haskell standalone-unified-ocaml +standalone-separate: standalone-separate-haskell standalone-separate-ocaml perf-standalone: $(PERF_STANDALONE:%=src/ExtractionOCaml/%) -standalone-ocaml: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%) -standalone-haskell: $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%) - +standalone-ocaml: standalone-unified-ocaml standalone-separate-ocaml +standalone-unified-ocaml: $(UNIFIED_STANDALONE_OCAML:%=src/ExtractionOCaml/%) +standalone-separate-ocaml: $(SEPARATE_STANDALONE_OCAML:%=src/ExtractionOCaml/%) +standalone-haskell: standalone-unified-haskell standalone-separate-haskell +standalone-unified-haskell: $(UNIFIED_STANDALONE_HASKELL:%=src/ExtractionHaskell/%) +standalone-separate-haskell: $(SEPARATE_STANDALONE_HASKELL:%=src/ExtractionHaskell/%) +# FIXME HERE uninstall-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES) uninstall-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES) diff --git a/src/CLI.v b/src/CLI.v index 36cbd05930e..07fdcdd2d7a 100644 --- a/src/CLI.v +++ b/src/CLI.v @@ -17,6 +17,7 @@ Require Import Crypto.Util.Strings.NamingConventions. Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. Require Import Crypto.Util.Strings.Show. +Require Import Crypto.Util.Strings.Show.Enum. Require Import Crypto.Util.Strings.Sorting. Require Import Crypto.Util.Strings.ParseFlagOptions. Require Import Crypto.Util.DebugMonad. @@ -44,6 +45,32 @@ Import Stringification.C.Compilers. Module ForExtraction. + Variant SynthesisKind : Set := + | word_by_word_montgomery + | unsaturated_solinas + | saturated_solinas + | dettman_multiplication + | solinas_reduction + | base_conversion + . + + Derive SynthesisKind_Listable SuchThat (@FinitelyListable SynthesisKind SynthesisKind_Listable) As SynthesisKind_FinitelyListable. + Proof. prove_ListableDerive. Qed. + Global Existing Instances SynthesisKind_Listable SynthesisKind_FinitelyListable. + + Global Instance show_SynthesisKind : Show SynthesisKind. + Proof. prove_Show_enum (). Defined. + Global Instance show_lvl_SynthesisKind : ShowLevel SynthesisKind := show_SynthesisKind. + + Definition parse_SynthesisKind_list : list (string * SynthesisKind) + := Eval vm_compute in + List.map + (fun r => (String.replace "_" "-" (show r), r)) + (list_all SynthesisKind). + + Definition parse_SynthesisKind_act : ParserAction SynthesisKind + := parse_strs parse_SynthesisKind_list. + Definition parse_string_and {T} (parse_T : string -> option T) (s : string) : option (string * T) := option_map (@pair _ _ s) (parse_T s). Definition parse_Z (s : string) : option Z := parseZ_arith_strict s. @@ -62,6 +89,9 @@ Module ForExtraction. ls <-- List.map ParseArithmetic.Q_to_Z_strict ls; Some ls). + Definition parse_SynthesisKind (s : string) : option SynthesisKind + := finalize parse_SynthesisKind_act s. + Definition parse_list_REG (s : string) : option (list REG) := finalize (parse_comma_list parse_REG) s. @@ -77,9 +107,6 @@ Module ForExtraction. Definition parse_callee_saved_registers (s : string) : option assembly_callee_saved_registers_opt := finalize parse_assembly_callee_saved_registers_opt s. - (* Workaround for lack of notation in 8.8 *) - Local Notation "x =? y" := (if string_dec x y then true else false) : string_scope. - Definition parse_n (n : string) : option MaybeLimbCount := match parse_nat n with | Some n => Some (NumLimbs n) @@ -301,6 +328,10 @@ Module ForExtraction. end)%string special_options)). + Definition synthesis_kind_spec : anon_argT + := ("synthesis_kind", + Arg.CustomSymbol parse_SynthesisKind_list, + ["The algorithm for field arithmetic. Further options depend on the choice of algorithm, and can be viewed by passing -h after this argument."]). Definition curve_description_spec : anon_argT := ("curve_description", Arg.String, @@ -1003,6 +1034,7 @@ Module ForExtraction. end. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1105,6 +1137,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1147,6 +1180,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1182,6 +1216,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1228,6 +1263,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1263,6 +1299,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1331,6 +1368,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1338,4 +1376,46 @@ Module ForExtraction. : A := Parameterized.PipelineMain argv. End BaseConversion. + + (** The combined binary that delegates *) + Module FiatCrypto. + Definition PipelineMain + {supported_languages : supported_languagesT} + {A} + {io_driver : IODriverAPI A} + (argv : list string) + : A + := let spec + := {| Arg.named_args := [] + ; Arg.anon_args := [synthesis_kind_spec] + ; Arg.anon_opt_args := [] + ; Arg.anon_opt_repeated_arg := None |} in + match Arg.parse_argv (List.firstn 2 argv) spec with + | ErrorT.Success (tt as _named_data, anon_data, tt as _anon_opt_data, tt as _anon_opt_repeated_data) + => let synthesis_kind := anon_data in + let prog_name_count : Arg.prog_name_countT := 2%nat in + match synthesis_kind with + | word_by_word_montgomery + => WordByWordMontgomery.PipelineMain (prog_name_count:=prog_name_count) argv + | unsaturated_solinas + => UnsaturatedSolinas.PipelineMain (prog_name_count:=prog_name_count) argv + | saturated_solinas + => SaturatedSolinas.PipelineMain (prog_name_count:=prog_name_count) argv + | dettman_multiplication + => DettmanMultiplication.PipelineMain (prog_name_count:=prog_name_count) argv + | solinas_reduction + => SolinasReduction.PipelineMain (prog_name_count:=prog_name_count) argv + | base_conversion + => BaseConversion.PipelineMain (prog_name_count:=prog_name_count) argv + end + | ErrorT.Error err + => let display := Arg.show_list_parse_error spec err in + if Arg.is_real_error err + then error display + else (* just a requested help/usage message *) + write_stdout_then + (List.map (fun s => s ++ String.NewLine)%string display) + ret + end. + End FiatCrypto. End ForExtraction. diff --git a/src/ExtractionHaskell/bedrock2_fiat_crypto.v b/src/ExtractionHaskell/bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..509dd3ced04 --- /dev/null +++ b/src/ExtractionHaskell/bedrock2_fiat_crypto.v @@ -0,0 +1,5 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain. +Import Bedrock2First. + +(*Redirect "/tmp/bedrock2_fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main. +(* cat /tmp/bedrock2_fiat_crypto.hs.out | sed -f haskell.sed > ../../bedrock2_fiat_crypto.hs *) diff --git a/src/ExtractionHaskell/fiat_crypto.v b/src/ExtractionHaskell/fiat_crypto.v new file mode 100644 index 00000000000..89a96038958 --- /dev/null +++ b/src/ExtractionHaskell/fiat_crypto.v @@ -0,0 +1,4 @@ +Require Import Crypto.StandaloneHaskellMain. + +(*Redirect "/tmp/fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main. +(* cat /tmp/fiat_crypto.hs.out | sed -f haskell.sed > ../../fiat_crypto.hs *) diff --git a/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v b/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..2b175121a05 --- /dev/null +++ b/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v @@ -0,0 +1,5 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain. +Import Bedrock2Later. + +(*Redirect "/tmp/bedrock2_fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main. +(* cat /tmp/bedrock2_fiat_crypto.hs.out | sed -f haskell.sed > ../../bedrock2_fiat_crypto.hs *) diff --git a/src/ExtractionOCaml/bedrock2_fiat_crypto.v b/src/ExtractionOCaml/bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..a2b85f8dc8c --- /dev/null +++ b/src/ExtractionOCaml/bedrock2_fiat_crypto.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2First. + +Extraction "src/ExtractionOCaml/bedrock2_fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/ExtractionOCaml/fiat_crypto.v b/src/ExtractionOCaml/fiat_crypto.v new file mode 100644 index 00000000000..fcd64cad02f --- /dev/null +++ b/src/ExtractionOCaml/fiat_crypto.v @@ -0,0 +1,3 @@ +Require Import Crypto.StandaloneOCamlMain. + +Extraction "src/ExtractionOCaml/fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v b/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..70b1716025e --- /dev/null +++ b/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionOCaml/with_bedrock2_fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/StandaloneHaskellMain.v b/src/StandaloneHaskellMain.v index b6e2923a96f..ac897510e81 100644 --- a/src/StandaloneHaskellMain.v +++ b/src/StandaloneHaskellMain.v @@ -144,3 +144,8 @@ Module BaseConversion. Definition main : IO_unit := main_gen ForExtraction.BaseConversion.PipelineMain. End BaseConversion. + +Module FiatCrypto. + Definition main : IO_unit + := main_gen ForExtraction.FiatCrypto.PipelineMain. +End FiatCrypto. diff --git a/src/StandaloneOCamlMain.v b/src/StandaloneOCamlMain.v index 2a19c9baee6..9c7710a56ff 100644 --- a/src/StandaloneOCamlMain.v +++ b/src/StandaloneOCamlMain.v @@ -233,3 +233,8 @@ Module BaseConversion. Definition main : unit := main_gen ForExtraction.BaseConversion.PipelineMain. End BaseConversion. + +Module FiatCrypto. + Definition main : unit + := main_gen ForExtraction.FiatCrypto.PipelineMain. +End FiatCrypto. diff --git a/src/Util/Arg.v b/src/Util/Arg.v index f61be6b2807..3e9ea65ef82 100644 --- a/src/Util/Arg.v +++ b/src/Util/Arg.v @@ -548,15 +548,24 @@ Definition default_named_results {ls} | (_, s, _) :: ss => @default_named_results' _ ss default_named_result end. -Definition parse_argv (argv : list string) (arg_spec : arg_spec) +Class prog_name_countT := prog_name_count : nat. +Global Typeclasses Opaque prog_name_countT. +Ltac fill_default_prog_name_countT _ + := lazymatch goal with + | [ H : prog_name_countT |- prog_name_countT ] => exact H + | [ |- prog_name_countT ] => exact 1%nat + end. +Global Hint Extern 1 prog_name_countT => fill_default_prog_name_countT () : typeclass_instances. + +Definition parse_argv {prog_name_count : prog_name_countT} (argv : list string) (arg_spec : arg_spec) : parse_result (arg_spec_results arg_spec) - := match argv with - | nil => Error missing_prog_name - | prog_name :: argv - => (res <- consume_args (10 + (List.length argv)) argv arg_spec (missing prog_name) (wrong prog_name) (too_many_args prog_name) (internal_error prog_name) (no_keyed_arg prog_name) (help prog_name) (out_of_fuel prog_name); + := if (List.length argv false | _ => true end.