From 9e509e7329283f429237c4f68b4ae9b1ca705b07 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 22 May 2022 19:18:49 +0100 Subject: [PATCH] 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 | 8 ++ Makefile | 40 +++++++-- .../Standalone/StandaloneHaskellMain.v | 81 +++++++++++++------ src/Bedrock/Standalone/StandaloneOCamlMain.v | 81 +++++++++++++------ .../bedrock2_base_conversion.v | 1 + .../bedrock2_saturated_solinas.v | 1 + .../bedrock2_unsaturated_solinas.v | 1 + .../bedrock2_word_by_word_montgomery.v | 1 + .../with_bedrock2_base_conversion.v | 5 ++ .../with_bedrock2_saturated_solinas.v | 5 ++ .../with_bedrock2_unsaturated_solinas.v | 5 ++ .../with_bedrock2_word_by_word_montgomery.v | 5 ++ .../bedrock2_base_conversion.v | 1 + .../bedrock2_saturated_solinas.v | 1 + .../bedrock2_unsaturated_solinas.v | 1 + .../bedrock2_word_by_word_montgomery.v | 1 + .../with_bedrock2_base_conversion.v | 4 + .../with_bedrock2_saturated_solinas.v | 4 + .../with_bedrock2_unsaturated_solinas.v | 4 + .../with_bedrock2_word_by_word_montgomery.v | 4 + 20 files changed, 196 insertions(+), 58 deletions(-) create mode 100644 src/ExtractionHaskell/with_bedrock2_base_conversion.v create mode 100644 src/ExtractionHaskell/with_bedrock2_saturated_solinas.v create mode 100644 src/ExtractionHaskell/with_bedrock2_unsaturated_solinas.v create mode 100644 src/ExtractionHaskell/with_bedrock2_word_by_word_montgomery.v create mode 100644 src/ExtractionOCaml/with_bedrock2_base_conversion.v create mode 100644 src/ExtractionOCaml/with_bedrock2_saturated_solinas.v create mode 100644 src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v create mode 100644 src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v diff --git a/.gitignore b/.gitignore index 1746dab8c7..f35597ecb9 100644 --- a/.gitignore +++ b/.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 diff --git a/Makefile b/Makefile index 7917f0877c..69762a778f 100644 --- a/Makefile +++ b/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 \ diff --git a/src/Bedrock/Standalone/StandaloneHaskellMain.v b/src/Bedrock/Standalone/StandaloneHaskellMain.v index 99c0573676..c37260bf22 100644 --- a/src/Bedrock/Standalone/StandaloneHaskellMain.v +++ b/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. diff --git a/src/Bedrock/Standalone/StandaloneOCamlMain.v b/src/Bedrock/Standalone/StandaloneOCamlMain.v index ad9eb7ed34..346a0f1208 100644 --- a/src/Bedrock/Standalone/StandaloneOCamlMain.v +++ b/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. diff --git a/src/ExtractionHaskell/bedrock2_base_conversion.v b/src/ExtractionHaskell/bedrock2_base_conversion.v index b06aeacf12..5a29ff1b18 100644 --- a/src/ExtractionHaskell/bedrock2_base_conversion.v +++ b/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 *) diff --git a/src/ExtractionHaskell/bedrock2_saturated_solinas.v b/src/ExtractionHaskell/bedrock2_saturated_solinas.v index bb9d12c4a4..e863da28f3 100644 --- a/src/ExtractionHaskell/bedrock2_saturated_solinas.v +++ b/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 *) diff --git a/src/ExtractionHaskell/bedrock2_unsaturated_solinas.v b/src/ExtractionHaskell/bedrock2_unsaturated_solinas.v index 87628b00c0..6853e9f0b9 100644 --- a/src/ExtractionHaskell/bedrock2_unsaturated_solinas.v +++ b/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 *) diff --git a/src/ExtractionHaskell/bedrock2_word_by_word_montgomery.v b/src/ExtractionHaskell/bedrock2_word_by_word_montgomery.v index 1452e3a5a3..12e7e0d91d 100644 --- a/src/ExtractionHaskell/bedrock2_word_by_word_montgomery.v +++ b/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 *) diff --git a/src/ExtractionHaskell/with_bedrock2_base_conversion.v b/src/ExtractionHaskell/with_bedrock2_base_conversion.v new file mode 100644 index 0000000000..b3ceaab4a0 --- /dev/null +++ b/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 *) diff --git a/src/ExtractionHaskell/with_bedrock2_saturated_solinas.v b/src/ExtractionHaskell/with_bedrock2_saturated_solinas.v new file mode 100644 index 0000000000..04dc75284f --- /dev/null +++ b/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 *) diff --git a/src/ExtractionHaskell/with_bedrock2_unsaturated_solinas.v b/src/ExtractionHaskell/with_bedrock2_unsaturated_solinas.v new file mode 100644 index 0000000000..daf00dde02 --- /dev/null +++ b/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 *) diff --git a/src/ExtractionHaskell/with_bedrock2_word_by_word_montgomery.v b/src/ExtractionHaskell/with_bedrock2_word_by_word_montgomery.v new file mode 100644 index 0000000000..9c9fd78322 --- /dev/null +++ b/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 *) diff --git a/src/ExtractionOCaml/bedrock2_base_conversion.v b/src/ExtractionOCaml/bedrock2_base_conversion.v index ce11e84cb8..32686ff312 100644 --- a/src/ExtractionOCaml/bedrock2_base_conversion.v +++ b/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. diff --git a/src/ExtractionOCaml/bedrock2_saturated_solinas.v b/src/ExtractionOCaml/bedrock2_saturated_solinas.v index bcb014e4ef..02aa4fe94f 100644 --- a/src/ExtractionOCaml/bedrock2_saturated_solinas.v +++ b/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. diff --git a/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v b/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v index e1cecb4846..90ad60fed1 100644 --- a/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v +++ b/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. diff --git a/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v b/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v index 611161aa5e..a8af9714d2 100644 --- a/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v +++ b/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. diff --git a/src/ExtractionOCaml/with_bedrock2_base_conversion.v b/src/ExtractionOCaml/with_bedrock2_base_conversion.v new file mode 100644 index 0000000000..ba356b462f --- /dev/null +++ b/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. diff --git a/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v b/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v new file mode 100644 index 0000000000..077673791b --- /dev/null +++ b/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. diff --git a/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v b/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v new file mode 100644 index 0000000000..c5ccdc48ba --- /dev/null +++ b/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. diff --git a/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v b/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v new file mode 100644 index 0000000000..482fb85892 --- /dev/null +++ b/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.