WIP towards #1724

Makefile.config

@@ -50,16 +50,30 @@ 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)
 
-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)

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)
 

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,11 +1368,54 @@ Module ForExtraction.
         }.
 
     Definition PipelineMain
+               {prog_name_count : Arg.prog_name_countT}
                {supported_languages : supported_languagesT}
                {A}
                {io_driver : IODriverAPI A}
                (argv : list string)
       : 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.

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 *)

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 *)

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 *)

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.

src/ExtractionOCaml/fiat_crypto.v

@@ -0,0 +1,3 @@
+Require Import Crypto.StandaloneOCamlMain.
+
+Extraction "src/ExtractionOCaml/fiat_crypto.tmp" FiatCrypto.main.

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.

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.

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.

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 <? prog_name_count)%nat
+     then Error missing_prog_name
+     else let '(prog_names, argv) := (List.firstn prog_name_count argv, List.skipn prog_name_count argv) in
+          let prog_name := String.concat " " prog_names in
+          (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);
           let '(upd, anon_data, anon_opt_data, anon_opt_repeated_data) := res in
-          Success (upd default_named_results, anon_data, anon_opt_data, anon_opt_repeated_data))
-     end%error.
+          Success (upd default_named_results, anon_data, anon_opt_data, anon_opt_repeated_data))%error.
 
 Definition is_real_error (e : parse_error) : bool := match e with help _ => false | _ => true end.