Add with_bedrock2 binaries (#1252)

This is in preparation for #1250.  We generate `with_bedrock2_*`
binaries which support bedrock2 output but default to C.  We also
install these by default when we are installing with bedrock2 enabled.
These will be the source files that we want to package up into source
releases of our generated code, as well as the source we use for
generating statically-linked redistributable binaries.

.gitignore

@@ -200,6 +200,10 @@ src/ExtractionOCaml/bedrock2_saturated_solinas
 src/ExtractionOCaml/bedrock2_unsaturated_solinas
 src/ExtractionOCaml/bedrock2_word_by_word_montgomery
 src/ExtractionOCaml/bedrock2_base_conversion
+src/ExtractionOCaml/with_bedrock2_saturated_solinas
+src/ExtractionOCaml/with_bedrock2_unsaturated_solinas
+src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery
+src/ExtractionOCaml/with_bedrock2_base_conversion
 src/ExtractionOCaml/perf_unsaturated_solinas
 src/ExtractionOCaml/perf_word_by_word_montgomery
 src/ExtractionOCaml/saturated_solinas.exe
@@ -210,6 +214,10 @@ src/ExtractionOCaml/bedrock2_saturated_solinas.exe
 src/ExtractionOCaml/bedrock2_unsaturated_solinas.exe
 src/ExtractionOCaml/bedrock2_word_by_word_montgomery.exe
 src/ExtractionOCaml/bedrock2_base_conversion.exe
+src/ExtractionOCaml/with_bedrock2_saturated_solinas.exe
+src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.exe
+src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.exe
+src/ExtractionOCaml/with_bedrock2_base_conversion.exe
 src/ExtractionOCaml/perf_unsaturated_solinas.exe
 src/ExtractionOCaml/perf_word_by_word_montgomery.exe
 src/ExtractionOCaml/*.cmi

Makefile

@@ -132,6 +132,8 @@ PERFTESTING_VO := \
 BEDROCK2_FILES_PATTERN := \
 	src/ExtractionOCaml/bedrock2_% \
 	src/ExtractionHaskell/bedrock2_% \
+	src/ExtractionOCaml/with_bedrock2_% \
+	src/ExtractionHaskell/with_bedrock2_% \
 	src/Assembly/WithBedrock/% \
 	src/Bedrock/% # it's important to catch not just the .vo files, but also the .glob files, etc, because this is used to filter FILESTOINSTALL
 EXCLUDE_PATTERN :=
@@ -570,18 +572,22 @@ Makefile.coq: Makefile _CoqProject
 	$(HIDE)$(COQBIN)coq_makefile -f _CoqProject INSTALLDEFAULTROOT = $(INSTALLDEFAULTROOT) -o Makefile-coq && cat Makefile-coq | sed 's/^printenv:/printenv::/g; s/^printenv:::/printenv::/g; s/^all:/all-old:/g; s/^validate:/validate-vo:/g; s/^.PHONY: validate/.PHONY: validate-vo/g' > $@ && rm -f Makefile-coq
 
 
-STANDALONE := unsaturated_solinas saturated_solinas word_by_word_montgomery base_conversion
-BEDROCK2_STANDALONE := $(addprefix bedrock2_,$(STANDALONE))
+BASE_STANDALONE := unsaturated_solinas saturated_solinas word_by_word_montgomery base_conversion
+BEDROCK2_STANDALONE := $(addprefix bedrock2_,$(BASE_STANDALONE)) $(addprefix with_bedrock2_,$(BASE_STANDALONE))
+STANDALONE := $(BASE_STANDALONE)
 ifneq ($(SKIP_BEDROCK2),1)
-STANDALONE += $(BEDROCK2_STANDALONE)
+STANDALONE += $(BEDROCK2_STANDALONE) $(WITH_BEDROCK2_STANDALONE)
 endif
 PERF_STANDALONE := perf_unsaturated_solinas perf_word_by_word_montgomery
 
 STANDALONE_OCAML := $(STANDALONE) $(PERF_STANDALONE)
 STANDALONE_HASKELL := $(STANDALONE)
 
-OCAML_BINARIES := $(STANDALONE:%=src/ExtractionOCaml/%)
-HASKELL_BINARIES := $(STANDALONE:%=src/ExtractionHaskell/%)
+OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/%)
+HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/%)
+
+WITH_BEDROCK2_OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%)
+WITH_BEDROCK2_HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%)
 
 
 $(STANDALONE:%=src/ExtractionOCaml/%.ml): src/StandaloneOCamlMain.vo
@@ -930,12 +936,13 @@ install-without-bedrock2:
 install-standalone-ocaml: standalone-ocaml
 install-standalone-haskell: standalone-haskell
 
-install-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
-install-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES)
-
 uninstall-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
 uninstall-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES)
 
+ifeq ($(SKIP_BEDROCK2),1)
+install-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
+install-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES)
+
 install-standalone-ocaml install-standalone-haskell:
 	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
 	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
@@ -945,6 +952,23 @@ install-standalone-ocaml install-standalone-haskell:
 	   install -m 0755 "$$f" "$(BINDIR)/" &&\
 	   echo INSTALL "$$f" "$(BINDIR)/";\
 	done
+else
+install-standalone-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES)
+install-standalone-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_HASKELL_BINARIES)
+
+install-standalone-ocaml install-standalone-haskell:
+	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
+	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
+	done; exit $$code
+	$(HIDE)for f in $(FILESTOINSTALL); do\
+	   fdir="$$(dirname "$$f")" &&\
+	   fname="$$(basename "$$f")" &&\
+	   df="$${fname#with_bedrock2_}" &&\
+	   install -d "$(BINDIR)/" &&\
+	   install -m 0755 "$$f" "$(BINDIR)/$$df" &&\
+	   echo INSTALL "$$f" "$(BINDIR)/$$df";\
+	done
+endif
 
 uninstall-standalone-ocaml uninstall-standalone-haskell:
 	$(HIDE)for f in $(FILESTOINSTALL); do \

src/Bedrock/Standalone/StandaloneHaskellMain.v

@@ -7,28 +7,59 @@ Import ListNotations.
 Local Open Scope string_scope.
 Local Open Scope list_scope.
 
-(** N.B. We put bedrock2 first so that the default for these binaries
-    is bedrock2 *)
-Local Instance bedrock2_supported_languages : ForExtraction.supported_languagesT
-  := [("bedrock2", OutputBedrock2API)]
-       ++ ForExtraction.default_supported_languages.
-
-Module UnsaturatedSolinas.
-  Definition main : IO_unit
-    := main_gen ForExtraction.UnsaturatedSolinas.PipelineMain.
-End UnsaturatedSolinas.
-
-Module WordByWordMontgomery.
-  Definition main : IO_unit
-    := main_gen ForExtraction.WordByWordMontgomery.PipelineMain.
-End WordByWordMontgomery.
-
-Module SaturatedSolinas.
-  Definition main : IO_unit
-    := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
-End SaturatedSolinas.
-
-Module BaseConversion.
-  Definition main : IO_unit
-    := main_gen ForExtraction.BaseConversion.PipelineMain.
-End BaseConversion.
+Module Bedrock2First.
+  (** N.B. We put bedrock2 first so that the default for these binaries
+      is bedrock2 *)
+  Local Instance bedrock2_supported_languages : ForExtraction.supported_languagesT
+    := [("bedrock2", OutputBedrock2API)]
+         ++ ForExtraction.default_supported_languages.
+
+  Module UnsaturatedSolinas.
+    Definition main : IO_unit
+      := main_gen ForExtraction.UnsaturatedSolinas.PipelineMain.
+  End UnsaturatedSolinas.
+
+  Module WordByWordMontgomery.
+    Definition main : IO_unit
+      := main_gen ForExtraction.WordByWordMontgomery.PipelineMain.
+  End WordByWordMontgomery.
+
+  Module SaturatedSolinas.
+    Definition main : IO_unit
+      := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
+  End SaturatedSolinas.
+
+  Module BaseConversion.
+    Definition main : IO_unit
+      := main_gen ForExtraction.BaseConversion.PipelineMain.
+  End BaseConversion.
+End Bedrock2First.
+
+Module Bedrock2Later.
+  Local Instance bedrock2_supported_languages : ForExtraction.supported_languagesT
+    := let bedrock2 := ("bedrock2", OutputBedrock2API) in
+       match ForExtraction.default_supported_languages with
+       | l :: ls => l :: bedrock2 :: ls
+       | ls => bedrock2 :: ls
+       end.
+
+  Module UnsaturatedSolinas.
+    Definition main : IO_unit
+      := main_gen ForExtraction.UnsaturatedSolinas.PipelineMain.
+  End UnsaturatedSolinas.
+
+  Module WordByWordMontgomery.
+    Definition main : IO_unit
+      := main_gen ForExtraction.WordByWordMontgomery.PipelineMain.
+  End WordByWordMontgomery.
+
+  Module SaturatedSolinas.
+    Definition main : IO_unit
+      := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
+  End SaturatedSolinas.
+
+  Module BaseConversion.
+    Definition main : IO_unit
+      := main_gen ForExtraction.BaseConversion.PipelineMain.
+  End BaseConversion.
+End Bedrock2Later.

src/Bedrock/Standalone/StandaloneOCamlMain.v

@@ -10,28 +10,59 @@ Local Open Scope list_scope.
 (** Needed to work around COQBUG(https://github.com/coq/coq/issues/4875) *)
 Extraction Inline coqutil.Map.SortedListString.map.
 
-(** N.B. We put bedrock2 first so that the default for these binaries
-    is bedrock2 *)
-Local Instance bedrock2_supported_languages : ForExtraction.supported_languagesT
-  := [("bedrock2", OutputBedrock2API)]
-       ++ ForExtraction.default_supported_languages.
-
-Module UnsaturatedSolinas.
-  Definition main : unit
-    := main_gen ForExtraction.UnsaturatedSolinas.PipelineMain.
-End UnsaturatedSolinas.
-
-Module WordByWordMontgomery.
-  Definition main : unit
-    := main_gen ForExtraction.WordByWordMontgomery.PipelineMain.
-End WordByWordMontgomery.
-
-Module SaturatedSolinas.
-  Definition main : unit
-    := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
-End SaturatedSolinas.
-
-Module BaseConversion.
-  Definition main : unit
-    := main_gen ForExtraction.BaseConversion.PipelineMain.
-End BaseConversion.
+Module Bedrock2First.
+  (** N.B. We put bedrock2 first so that the default for these binaries
+      is bedrock2 *)
+  Local Instance bedrock2_supported_languages : ForExtraction.supported_languagesT
+    := [("bedrock2", OutputBedrock2API)]
+         ++ ForExtraction.default_supported_languages.
+
+  Module UnsaturatedSolinas.
+    Definition main : unit
+      := main_gen ForExtraction.UnsaturatedSolinas.PipelineMain.
+  End UnsaturatedSolinas.
+
+  Module WordByWordMontgomery.
+    Definition main : unit
+      := main_gen ForExtraction.WordByWordMontgomery.PipelineMain.
+  End WordByWordMontgomery.
+
+  Module SaturatedSolinas.
+    Definition main : unit
+      := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
+  End SaturatedSolinas.
+
+  Module BaseConversion.
+    Definition main : unit
+      := main_gen ForExtraction.BaseConversion.PipelineMain.
+  End BaseConversion.
+End Bedrock2First.
+
+Module Bedrock2Later.
+  Local Instance bedrock2_supported_languages : ForExtraction.supported_languagesT
+    := let bedrock2 := ("bedrock2", OutputBedrock2API) in
+       match ForExtraction.default_supported_languages with
+       | l :: ls => l :: bedrock2 :: ls
+       | ls => bedrock2 :: ls
+       end.
+
+  Module UnsaturatedSolinas.
+    Definition main : unit
+      := main_gen ForExtraction.UnsaturatedSolinas.PipelineMain.
+  End UnsaturatedSolinas.
+
+  Module WordByWordMontgomery.
+    Definition main : unit
+      := main_gen ForExtraction.WordByWordMontgomery.PipelineMain.
+  End WordByWordMontgomery.
+
+  Module SaturatedSolinas.
+    Definition main : unit
+      := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
+  End SaturatedSolinas.
+
+  Module BaseConversion.
+    Definition main : unit
+      := main_gen ForExtraction.BaseConversion.PipelineMain.
+  End BaseConversion.
+End Bedrock2Later.

src/ExtractionHaskell/bedrock2_base_conversion.v

@@ -1,4 +1,5 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2First.
 
 (*Redirect "/tmp/bedrock2_base_conversion.hs"*) Recursive Extraction BaseConversion.main.
 (* cat /tmp/bedrock2_base_conversion.hs.out | sed -f haskell.sed  > ../../bedrock2_base_conversion.hs *)

src/ExtractionHaskell/bedrock2_saturated_solinas.v

@@ -1,4 +1,5 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2First.
 
 (*Redirect "/tmp/bedrock2_saturated_solinas.hs"*) Recursive Extraction SaturatedSolinas.main.
 (* cat /tmp/bedrock2_saturated_solinas.hs.out | sed -f haskell.sed  > ../../bedrock2_saturated_solinas.hs *)

src/ExtractionHaskell/bedrock2_unsaturated_solinas.v

@@ -1,4 +1,5 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2First.
 
 (*Redirect "/tmp/bedrock2_unsaturated_solinas.hs" *)Recursive Extraction UnsaturatedSolinas.main.
 (* cat /tmp/bedrock2_unsaturated_solinas.hs.out | sed -f haskell.sed  > ../../bedrock2_unsaturated_solinas.hs *)

src/ExtractionHaskell/bedrock2_word_by_word_montgomery.v

@@ -1,4 +1,5 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2First.
 
 (*Redirect "/tmp/bedrock2_word_by_word_montgomery.hs" *)Recursive Extraction WordByWordMontgomery.main.
 (* cat /tmp/bedrock2_word_by_word_montgomery.hs.out | sed -f haskell.sed  > ../../bedrock2_word_by_word_montgomery.hs *)

src/ExtractionHaskell/with_bedrock2_base_conversion.v

@@ -0,0 +1,5 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_base_conversion.hs"*) Recursive Extraction BaseConversion.main.
+(* cat /tmp/bedrock2_base_conversion.hs.out | sed -f haskell.sed  > ../../bedrock2_base_conversion.hs *)

src/ExtractionHaskell/with_bedrock2_saturated_solinas.v

@@ -0,0 +1,5 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_saturated_solinas.hs"*) Recursive Extraction SaturatedSolinas.main.
+(* cat /tmp/bedrock2_saturated_solinas.hs.out | sed -f haskell.sed  > ../../bedrock2_saturated_solinas.hs *)

src/ExtractionHaskell/with_bedrock2_unsaturated_solinas.v

@@ -0,0 +1,5 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_unsaturated_solinas.hs" *)Recursive Extraction UnsaturatedSolinas.main.
+(* cat /tmp/bedrock2_unsaturated_solinas.hs.out | sed -f haskell.sed  > ../../bedrock2_unsaturated_solinas.hs *)

src/ExtractionHaskell/with_bedrock2_word_by_word_montgomery.v

@@ -0,0 +1,5 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_word_by_word_montgomery.hs" *)Recursive Extraction WordByWordMontgomery.main.
+(* cat /tmp/bedrock2_word_by_word_montgomery.hs.out | sed -f haskell.sed  > ../../bedrock2_word_by_word_montgomery.hs *)

src/ExtractionOCaml/bedrock2_base_conversion.v

@@ -1,3 +1,4 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2First.
 
 (*Redirect "/tmp/bedrock2_base_conversion.ml"*) Recursive Extraction BaseConversion.main.

src/ExtractionOCaml/bedrock2_saturated_solinas.v

@@ -1,3 +1,4 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2First.
 
 (*Redirect "/tmp/bedrock2_saturated_solinas.ml"*) Recursive Extraction SaturatedSolinas.main.

src/ExtractionOCaml/bedrock2_unsaturated_solinas.v

@@ -1,3 +1,4 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2First.
 
 (*Redirect "/tmp/bedrock2_unsaturated_solinas.ml"*) Recursive Extraction UnsaturatedSolinas.main.

src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v

@@ -1,3 +1,4 @@
 Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2First.
 
 (*Redirect "/tmp/bedrock2_word_by_word_montgomery.ml"*) Recursive Extraction WordByWordMontgomery.main.

src/ExtractionOCaml/with_bedrock2_base_conversion.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_base_conversion.ml"*) Recursive Extraction BaseConversion.main.

src/ExtractionOCaml/with_bedrock2_saturated_solinas.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_saturated_solinas.ml"*) Recursive Extraction SaturatedSolinas.main.

src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_unsaturated_solinas.ml"*) Recursive Extraction UnsaturatedSolinas.main.

src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_word_by_word_montgomery.ml"*) Recursive Extraction WordByWordMontgomery.main.