From 30b726101104be2123a3ba1640a7adb7f1b7030e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 20 Sep 2024 19:11:33 -0700 Subject: [PATCH] Don't sed wasm files, instead use subfolders to ensure the binary names are correct from the start (#1961) --- .github/workflows/coq-docker.yml | 4 +- .gitignore | 47 +++++++------ Makefile | 6 +- Makefile.config | 26 ++++---- Makefile.standalone | 66 +++---------------- fiat-html/wasm_fiat_crypto_worker.js | 2 +- .../base_conversion.v} | 0 .../dettman_multiplication.v} | 0 .../fiat_crypto.v} | 0 .../saturated_solinas.v} | 0 .../solinas_reduction.v} | 0 .../unsaturated_solinas.v} | 0 .../word_by_word_montgomery.v} | 0 .../fiat_crypto.v} | 2 +- .../WithBedrock/base_conversion.v | 4 ++ .../WithBedrock/dettman_multiplication.v | 4 ++ .../fiat_crypto.v} | 2 +- .../WithBedrock/saturated_solinas.v | 4 ++ .../WithBedrock/solinas_reduction.v | 4 ++ .../WithBedrock/unsaturated_solinas.v | 4 ++ .../WithBedrock/word_by_word_montgomery.v | 4 ++ .../with_bedrock2_base_conversion.v | 4 -- .../with_bedrock2_dettman_multiplication.v | 4 -- .../with_bedrock2_saturated_solinas.v | 4 -- .../with_bedrock2_solinas_reduction.v | 4 -- .../with_bedrock2_unsaturated_solinas.v | 4 -- .../with_bedrock2_word_by_word_montgomery.v | 4 -- 27 files changed, 81 insertions(+), 122 deletions(-) rename src/ExtractionHaskell/{with_bedrock2_base_conversion.v => WithBedrock/base_conversion.v} (100%) rename src/ExtractionHaskell/{with_bedrock2_dettman_multiplication.v => WithBedrock/dettman_multiplication.v} (100%) rename src/ExtractionHaskell/{with_bedrock2_fiat_crypto.v => WithBedrock/fiat_crypto.v} (100%) rename src/ExtractionHaskell/{with_bedrock2_saturated_solinas.v => WithBedrock/saturated_solinas.v} (100%) rename src/ExtractionHaskell/{with_bedrock2_solinas_reduction.v => WithBedrock/solinas_reduction.v} (100%) rename src/ExtractionHaskell/{with_bedrock2_unsaturated_solinas.v => WithBedrock/unsaturated_solinas.v} (100%) rename src/ExtractionHaskell/{with_bedrock2_word_by_word_montgomery.v => WithBedrock/word_by_word_montgomery.v} (100%) rename src/ExtractionJsOfOCaml/{with_bedrock2_fiat_crypto.v => WithBedrock/fiat_crypto.v} (51%) create mode 100644 src/ExtractionOCaml/WithBedrock/base_conversion.v create mode 100644 src/ExtractionOCaml/WithBedrock/dettman_multiplication.v rename src/ExtractionOCaml/{with_bedrock2_fiat_crypto.v => WithBedrock/fiat_crypto.v} (51%) create mode 100644 src/ExtractionOCaml/WithBedrock/saturated_solinas.v create mode 100644 src/ExtractionOCaml/WithBedrock/solinas_reduction.v create mode 100644 src/ExtractionOCaml/WithBedrock/unsaturated_solinas.v create mode 100644 src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.v delete mode 100644 src/ExtractionOCaml/with_bedrock2_base_conversion.v delete mode 100644 src/ExtractionOCaml/with_bedrock2_dettman_multiplication.v delete mode 100644 src/ExtractionOCaml/with_bedrock2_saturated_solinas.v delete mode 100644 src/ExtractionOCaml/with_bedrock2_solinas_reduction.v delete mode 100644 src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v delete mode 100644 src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index bc397c76b9..e805f7fa1c 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -366,7 +366,7 @@ jobs: name: ExtractionOCaml-${{ matrix.coq-version }} path: src/ExtractionOCaml - name: make binaries executable - run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x + run: git check-ignore src/ExtractionOCaml/* src/ExtractionOCaml/*/* | grep -v '\.' | xargs chmod +x - name: generated-files run: etc/ci/github-actions-make.sh --warnings -f Makefile.examples -j2 generated-files if: github.event_name == 'pull_request' @@ -428,7 +428,7 @@ jobs: name: ExtractionOCaml-master path: src/ExtractionOCaml - name: make binaries executable - run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x + run: git check-ignore src/ExtractionOCaml/* src/ExtractionOCaml/*/* | grep -v '\.' | xargs chmod +x - name: only-test-amd64-files run: etc/ci/github-actions-make.sh -f Makefile.examples -j2 only-test-amd64-files SLOWEST_FIRST=1 env: diff --git a/.gitignore b/.gitignore index 4e8c265d5a..0447e9d30b 100644 --- a/.gitignore +++ b/.gitignore @@ -171,17 +171,17 @@ src/ExtractionHaskell/bedrock2_solinas_reduction src/ExtractionHaskell/bedrock2_unsaturated_solinas src/ExtractionHaskell/bedrock2_word_by_word_montgomery src/ExtractionHaskell/fiat_crypto -src/ExtractionHaskell/with_bedrock2_base_conversion -src/ExtractionHaskell/with_bedrock2_dettman_multiplication -src/ExtractionHaskell/with_bedrock2_fiat_crypto -src/ExtractionHaskell/with_bedrock2_saturated_solinas -src/ExtractionHaskell/with_bedrock2_solinas_reduction -src/ExtractionHaskell/with_bedrock2_unsaturated_solinas -src/ExtractionHaskell/with_bedrock2_word_by_word_montgomery +src/ExtractionHaskell/WithBedrock/base_conversion +src/ExtractionHaskell/WithBedrock/dettman_multiplication +src/ExtractionHaskell/WithBedrock/fiat_crypto +src/ExtractionHaskell/WithBedrock/saturated_solinas +src/ExtractionHaskell/WithBedrock/solinas_reduction +src/ExtractionHaskell/WithBedrock/unsaturated_solinas +src/ExtractionHaskell/WithBedrock/word_by_word_montgomery src/ExtractionHaskell/*.hs src/ExtractionOCaml/bedrock2_fiat_crypto src/ExtractionOCaml/fiat_crypto -src/ExtractionOCaml/with_bedrock2_fiat_crypto +src/ExtractionOCaml/WithBedrock/fiat_crypto src/ExtractionOCaml/saturated_solinas src/ExtractionOCaml/dettman_multiplication src/ExtractionOCaml/unsaturated_solinas @@ -194,16 +194,18 @@ src/ExtractionOCaml/bedrock2_unsaturated_solinas src/ExtractionOCaml/bedrock2_solinas_reduction src/ExtractionOCaml/bedrock2_word_by_word_montgomery src/ExtractionOCaml/bedrock2_base_conversion -src/ExtractionOCaml/with_bedrock2_saturated_solinas -src/ExtractionOCaml/with_bedrock2_dettman_multiplication -src/ExtractionOCaml/with_bedrock2_unsaturated_solinas -src/ExtractionOCaml/with_bedrock2_solinas_reduction -src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery -src/ExtractionOCaml/with_bedrock2_base_conversion +src/ExtractionOCaml/WithBedrock/saturated_solinas +src/ExtractionOCaml/WithBedrock/dettman_multiplication +src/ExtractionOCaml/WithBedrock/unsaturated_solinas +src/ExtractionOCaml/WithBedrock/solinas_reduction +src/ExtractionOCaml/WithBedrock/word_by_word_montgomery +src/ExtractionOCaml/WithBedrock/base_conversion src/ExtractionOCaml/perf_unsaturated_solinas src/ExtractionOCaml/perf_word_by_word_montgomery src/ExtractionOCaml/*.ml src/ExtractionOCaml/*.mli +src/ExtractionOCaml/WithBedrock/*.ml +src/ExtractionOCaml/WithBedrock/*.mli src/ExtractionJsOfOCaml/*.ml src/ExtractionJsOfOCaml/*.mli src/ExtractionJsOfOCaml/*.js @@ -211,6 +213,13 @@ src/ExtractionJsOfOCaml/*.map src/ExtractionJsOfOCaml/*.wasm src/ExtractionJsOfOCaml/*.wat src/ExtractionJsOfOCaml/*.wat.gz +src/ExtractionJsOfOCaml/WithBedrock/*.ml +src/ExtractionJsOfOCaml/WithBedrock/*.mli +src/ExtractionJsOfOCaml/WithBedrock/*.js +src/ExtractionJsOfOCaml/WithBedrock/*.map +src/ExtractionJsOfOCaml/WithBedrock/*.wasm +src/ExtractionJsOfOCaml/WithBedrock/*.wat +src/ExtractionJsOfOCaml/WithBedrock/*.wat.gz src/Rewriter/PerfTesting/Specific/generated/*.v src/Rewriter/PerfTesting/Specific/generated/*.log src/Rewriter/PerfTesting/Specific/generated/*.sh @@ -225,11 +234,11 @@ fiat-amd64/*.description fiat-amd64/*.invocation fiat-html/fiat_crypto.js fiat-html/fiat_crypto.map -fiat-html/wasm_fiat_crypto.js -fiat-html/wasm_fiat_crypto.wat -fiat-html/wasm_fiat_crypto.wat.gz -fiat-html/wasm_fiat_crypto.wasm -fiat-html/wasm_fiat_crypto.wasm.map +fiat-html/wasm/fiat_crypto.js +fiat-html/wasm/fiat_crypto.wat +fiat-html/wasm/fiat_crypto.wat.gz +fiat-html/wasm/fiat_crypto.wasm +fiat-html/wasm/fiat_crypto.wasm.map fiat-html/version.js /Makefile.test-amd64-files.mk diff --git a/Makefile b/Makefile index 3e65f9f3c7..8163b0367f 100644 --- a/Makefile +++ b/Makefile @@ -73,9 +73,9 @@ BEDROCK2_FILES_PATTERN := \ src/ExtractionJsOfOCaml/bedrock2_% \ src/ExtractionOCaml/bedrock2_% \ src/ExtractionHaskell/bedrock2_% \ - src/ExtractionJsOfOCaml/with_bedrock2_% \ - src/ExtractionOCaml/with_bedrock2_% \ - src/ExtractionHaskell/with_bedrock2_% \ + src/ExtractionJsOfOCaml/WithBedrock/% \ + src/ExtractionOCaml/WithBedrock/% \ + src/ExtractionHaskell/WithBedrock/% \ 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 := diff --git a/Makefile.config b/Makefile.config index c3602b461c..bed7f453ea 100644 --- a/Makefile.config +++ b/Makefile.config @@ -7,7 +7,9 @@ SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) BINDIR?=/usr/local/bin -JSDIR?=fiat-html +JSWASM_BASEDIR?=fiat-html +JSDIR?=$(JSWASM_BASEDIR) +WASMDIR?=$(JSWASM_BASEDIR)/wasm # or $(shell opam config var bin) ? MOD_NAME := Crypto @@ -56,8 +58,8 @@ endif 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_UNIFIED_STANDALONE := $(addprefix bedrock2_,$(UNIFIED_BASE_STANDALONE)) $(addprefix WithBedrock/,$(UNIFIED_BASE_STANDALONE)) +BEDROCK2_SEPARATE_STANDALONE := $(addprefix bedrock2_,$(SEPARATE_BASE_STANDALONE)) $(addprefix WithBedrock/,$(SEPARATE_BASE_STANDALONE)) BEDROCK2_STANDALONE := $(BEDROCK2_UNIFIED_STANDALONE) $(BEDROCK2_SEPARATE_STANDALONE) UNIFIED_STANDALONE := $(UNIFIED_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_UNIFIED_STANDALONE)) SEPARATE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_SEPARATE_STANDALONE)) @@ -83,17 +85,13 @@ UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/%) SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/%) HASKELL_BINARIES := $(UNIFIED_HASKELL_BINARIES) $(SEPARATE_HASKELL_BINARIES) JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.map) -WASM_OF_OCAML_TEXT_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm.map) -WASM_OF_OCAML_BINARY_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wat.gz) -WASM_OF_OCAML_FILES := $(WASM_OF_OCAML_TEXT_FILES) $(WASM_OF_OCAML_BINARY_FILES) +WASM_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm.map) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wat.gz) -WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) -WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) +WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%) +WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%) WITH_BEDROCK2_OCAML_BINARIES := $(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES) $(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES) -WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%) -WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%) +WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/WithBedrock/%) +WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/WithBedrock/%) WITH_BEDROCK2_HASKELL_BINARIES := $(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES) $(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES) -WITH_BEDROCK2_JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.map) -WITH_BEDROCK2_WASM_OF_OCAML_TEXT_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.js) -WITH_BEDROCK2_WASM_OF_OCAML_BINARY_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/with_bedrock2_%.wat.gz) -WITH_BEDROCK2_WASM_OF_OCAML_FILES := $(WITH_BEDROCK2_WASM_OF_OCAML_TEXT_FILES) $(WITH_BEDROCK2_WASM_OF_OCAML_BINARY_FILES) +WITH_BEDROCK2_JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.map) +WITH_BEDROCK2_WASM_OF_OCAML := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wat.gz) diff --git a/Makefile.standalone b/Makefile.standalone index ae1ed6d5a0..cfb4602ef2 100644 --- a/Makefile.standalone +++ b/Makefile.standalone @@ -70,7 +70,7 @@ $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.cmi) : %.cmi : %.ml $(STANDALONE_OCAML:%=src/ExtractionOCaml/%) : % : %.ml %.cmi $(SHOW)'$(CAMLOPT_PERF_SHOW) $< -o $@' $(HIDE)$(ENSURE_STACK_LIMIT); \ - $(TIMER) $(CAMLOPT_PERF) $(STANDALONE_CAMLFLAGS) -linkpkg -I src/ExtractionOCaml/ -o $@ $< + $(TIMER) $(CAMLOPT_PERF) $(STANDALONE_CAMLFLAGS) -linkpkg -I $(dir $@) -o $@ $< $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.cmi) : %.cmi : %.ml $(SHOW)'OCAMLC $*.mli' @@ -80,7 +80,7 @@ $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.cmi) : %.cmi : %.ml $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.byte) : %.byte : %.ml %.cmi $(SHOW)'OCAMLC $< -o $@' $(HIDE)$(ENSURE_STACK_LIMIT); \ - $(TIMER) $(OCAMLC) $(STANDALONE_JS_CAMLFLAGS) -linkpkg -I src/ExtractionJsOfOCaml/ -o $@ $< + $(TIMER) $(OCAMLC) $(STANDALONE_JS_CAMLFLAGS) -linkpkg -I $(dir $@) -o $@ $< $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.js) : %.js : %.byte $(SHOW)'JS_OF_OCAML $<' @@ -127,7 +127,7 @@ install-standalone-ocaml install-standalone-unified-ocaml install-standalone-sep install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml: PERMS=0644 install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell: INSTALLDIR=$(BINDIR) install-standalone-js-of-ocaml: INSTALLDIR=$(JSDIR) -install-standalone-wasm-of-ocaml: INSTALLDIR=$(JSDIR) +install-standalone-wasm-of-ocaml: INSTALLDIR=$(WASMDIR) @@ -141,15 +141,6 @@ install-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES) install-standalone-js-of-ocaml: FILESTOINSTALL=$(JS_OF_OCAML_FILES) install-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WASM_OF_OCAML_FILES) -install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml: - $(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\ - install -d "$(INSTALLDIR)/" &&\ - install -m $(PERMS) "$$f" "$(INSTALLDIR)/" &&\ - echo INSTALL "$$f" "$(INSTALLDIR)/";\ - done else install-standalone-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES) install-standalone-unified-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES) @@ -158,58 +149,19 @@ install-standalone-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_HASKELL_BINARIES) install-standalone-unified-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES) install-standalone-separate-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES) install-standalone-js-of-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_JS_OF_OCAML_FILES) -install-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_TEXT_FILES) -install-standalone-wasm-of-ocaml: BINARYFILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_BINARY_FILES) +install-standalone-wasm-of-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_WASM_OF_OCAML_FILES) -install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-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 "$(INSTALLDIR)/" &&\ - install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\ - echo INSTALL "$$f" "$(INSTALLDIR)/$$df";\ - done -install-standalone-js-of-ocaml: +endif + +install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell install-standalone-js-of-ocaml install-standalone-wasm-of-ocaml: $(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 "$(INSTALLDIR)/" &&\ - install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\ - sed -i.bak -e 's,\(sourceMappingURL=.*\)with_bedrock2_,\1,g; s,\("file":[^"]*"[^"]*\)with_bedrock2_,\1,g' "$(INSTALLDIR)/$$df" &&\ - rm -f "$(INSTALLDIR)/$$df.bak" &&\ - echo 'INSTALL+SED' "$$f" "$(INSTALLDIR)/$$df";\ - done -install-standalone-wasm-of-ocaml: - $(HIDE)code=0; for f in $(FILESTOINSTALL) $(BINARYFILESTOINSTALL); 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="wasm_$${fname#with_bedrock2_}" &&\ - install -d "$(INSTALLDIR)/" &&\ - install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\ - sed -i.bak -e 's,with_bedrock2_,wasm_,g' "$(INSTALLDIR)/$$df" &&\ - rm -f "$(INSTALLDIR)/$$df.bak" &&\ - echo 'INSTALL+SED' "$$f" "$(INSTALLDIR)/$$df";\ - done - $(HIDE)for f in $(BINARYFILESTOINSTALL); do\ - fdir="$$(dirname "$$f")" &&\ - fname="$$(basename "$$f")" &&\ - df="wasm_$${fname#with_bedrock2_}" &&\ install -d "$(INSTALLDIR)/" &&\ - install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\ - echo 'INSTALL' "$$f" "$(INSTALLDIR)/$$df";\ + install -m $(PERMS) "$$f" "$(INSTALLDIR)/" &&\ + echo INSTALL "$$f" "$(INSTALLDIR)/";\ done -endif uninstall-standalone-ocaml uninstall-standalone-unified-ocaml uninstall-standalone-separate-ocaml uninstall-standalone-haskell uninstall-standalone-unified-haskell uninstall-standalone-separate-haskell uninstall-standalone-wasm-of-ocaml uninstall-standalone-js-of-ocaml: $(HIDE)for f in $(FILESTOINSTALL); do \ diff --git a/fiat-html/wasm_fiat_crypto_worker.js b/fiat-html/wasm_fiat_crypto_worker.js index 1e0f747f2a..9163c3d2f7 100644 --- a/fiat-html/wasm_fiat_crypto_worker.js +++ b/fiat-html/wasm_fiat_crypto_worker.js @@ -1,4 +1,4 @@ -self.importScripts("wasm_fiat_crypto.js"); +self.importScripts("wasm/fiat_crypto.js"); let pending = []; self.onmessage = function (e) { pending.push(e); }; setTimeout(function () { diff --git a/src/ExtractionHaskell/with_bedrock2_base_conversion.v b/src/ExtractionHaskell/WithBedrock/base_conversion.v similarity index 100% rename from src/ExtractionHaskell/with_bedrock2_base_conversion.v rename to src/ExtractionHaskell/WithBedrock/base_conversion.v diff --git a/src/ExtractionHaskell/with_bedrock2_dettman_multiplication.v b/src/ExtractionHaskell/WithBedrock/dettman_multiplication.v similarity index 100% rename from src/ExtractionHaskell/with_bedrock2_dettman_multiplication.v rename to src/ExtractionHaskell/WithBedrock/dettman_multiplication.v diff --git a/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v b/src/ExtractionHaskell/WithBedrock/fiat_crypto.v similarity index 100% rename from src/ExtractionHaskell/with_bedrock2_fiat_crypto.v rename to src/ExtractionHaskell/WithBedrock/fiat_crypto.v diff --git a/src/ExtractionHaskell/with_bedrock2_saturated_solinas.v b/src/ExtractionHaskell/WithBedrock/saturated_solinas.v similarity index 100% rename from src/ExtractionHaskell/with_bedrock2_saturated_solinas.v rename to src/ExtractionHaskell/WithBedrock/saturated_solinas.v diff --git a/src/ExtractionHaskell/with_bedrock2_solinas_reduction.v b/src/ExtractionHaskell/WithBedrock/solinas_reduction.v similarity index 100% rename from src/ExtractionHaskell/with_bedrock2_solinas_reduction.v rename to src/ExtractionHaskell/WithBedrock/solinas_reduction.v diff --git a/src/ExtractionHaskell/with_bedrock2_unsaturated_solinas.v b/src/ExtractionHaskell/WithBedrock/unsaturated_solinas.v similarity index 100% rename from src/ExtractionHaskell/with_bedrock2_unsaturated_solinas.v rename to src/ExtractionHaskell/WithBedrock/unsaturated_solinas.v diff --git a/src/ExtractionHaskell/with_bedrock2_word_by_word_montgomery.v b/src/ExtractionHaskell/WithBedrock/word_by_word_montgomery.v similarity index 100% rename from src/ExtractionHaskell/with_bedrock2_word_by_word_montgomery.v rename to src/ExtractionHaskell/WithBedrock/word_by_word_montgomery.v diff --git a/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v b/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v similarity index 51% rename from src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v rename to src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v index 4fbc0c90d2..ecebc266c1 100644 --- a/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v +++ b/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneJsOfOCamlMain. Import Bedrock2Later. -Extraction "src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.tmp" FiatCrypto.main. +Extraction "src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/ExtractionOCaml/WithBedrock/base_conversion.v b/src/ExtractionOCaml/WithBedrock/base_conversion.v new file mode 100644 index 0000000000..e1f4406d37 --- /dev/null +++ b/src/ExtractionOCaml/WithBedrock/base_conversion.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionOCaml/WithBedrock/base_conversion.tmp" BaseConversion.main. diff --git a/src/ExtractionOCaml/WithBedrock/dettman_multiplication.v b/src/ExtractionOCaml/WithBedrock/dettman_multiplication.v new file mode 100644 index 0000000000..54fe7194e1 --- /dev/null +++ b/src/ExtractionOCaml/WithBedrock/dettman_multiplication.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionOCaml/WithBedrock/dettman_multiplication.tmp" DettmanMultiplication.main. diff --git a/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v b/src/ExtractionOCaml/WithBedrock/fiat_crypto.v similarity index 51% rename from src/ExtractionOCaml/with_bedrock2_fiat_crypto.v rename to src/ExtractionOCaml/WithBedrock/fiat_crypto.v index 70b1716025..476ca47e1a 100644 --- a/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v +++ b/src/ExtractionOCaml/WithBedrock/fiat_crypto.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2Later. -Extraction "src/ExtractionOCaml/with_bedrock2_fiat_crypto.tmp" FiatCrypto.main. +Extraction "src/ExtractionOCaml/WithBedrock/fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/ExtractionOCaml/WithBedrock/saturated_solinas.v b/src/ExtractionOCaml/WithBedrock/saturated_solinas.v new file mode 100644 index 0000000000..7cf8547c34 --- /dev/null +++ b/src/ExtractionOCaml/WithBedrock/saturated_solinas.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionOCaml/WithBedrock/saturated_solinas.tmp" SaturatedSolinas.main. diff --git a/src/ExtractionOCaml/WithBedrock/solinas_reduction.v b/src/ExtractionOCaml/WithBedrock/solinas_reduction.v new file mode 100644 index 0000000000..0e759e1c8c --- /dev/null +++ b/src/ExtractionOCaml/WithBedrock/solinas_reduction.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionOCaml/WithBedrock/solinas_reduction.tmp" SaturatedSolinas.main. diff --git a/src/ExtractionOCaml/WithBedrock/unsaturated_solinas.v b/src/ExtractionOCaml/WithBedrock/unsaturated_solinas.v new file mode 100644 index 0000000000..09ee7a24e6 --- /dev/null +++ b/src/ExtractionOCaml/WithBedrock/unsaturated_solinas.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionOCaml/WithBedrock/unsaturated_solinas.tmp" UnsaturatedSolinas.main. diff --git a/src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.v b/src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.v new file mode 100644 index 0000000000..04320529b9 --- /dev/null +++ b/src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.tmp" WordByWordMontgomery.main. diff --git a/src/ExtractionOCaml/with_bedrock2_base_conversion.v b/src/ExtractionOCaml/with_bedrock2_base_conversion.v deleted file mode 100644 index 622e5c3862..0000000000 --- a/src/ExtractionOCaml/with_bedrock2_base_conversion.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. -Import Bedrock2Later. - -Extraction "src/ExtractionOCaml/with_bedrock2_base_conversion.tmp" BaseConversion.main. diff --git a/src/ExtractionOCaml/with_bedrock2_dettman_multiplication.v b/src/ExtractionOCaml/with_bedrock2_dettman_multiplication.v deleted file mode 100644 index 22b559d04f..0000000000 --- a/src/ExtractionOCaml/with_bedrock2_dettman_multiplication.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. -Import Bedrock2Later. - -Extraction "src/ExtractionOCaml/with_bedrock2_dettman_multiplication.tmp" DettmanMultiplication.main. diff --git a/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v b/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v deleted file mode 100644 index 9b2547df48..0000000000 --- a/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. -Import Bedrock2Later. - -Extraction "src/ExtractionOCaml/with_bedrock2_saturated_solinas.tmp" SaturatedSolinas.main. diff --git a/src/ExtractionOCaml/with_bedrock2_solinas_reduction.v b/src/ExtractionOCaml/with_bedrock2_solinas_reduction.v deleted file mode 100644 index 44c660ff92..0000000000 --- a/src/ExtractionOCaml/with_bedrock2_solinas_reduction.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. -Import Bedrock2Later. - -Extraction "src/ExtractionOCaml/with_bedrock2_solinas_reduction.tmp" SaturatedSolinas.main. diff --git a/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v b/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v deleted file mode 100644 index 74d3b13e81..0000000000 --- a/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. -Import Bedrock2Later. - -Extraction "src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.tmp" UnsaturatedSolinas.main. diff --git a/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v b/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v deleted file mode 100644 index b31bef8c15..0000000000 --- a/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. -Import Bedrock2Later. - -Extraction "src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.tmp" WordByWordMontgomery.main.