Skip to content

Commit

Permalink
Don't sed wasm files, instead use subfolders to ensure the binary nam…
Browse files Browse the repository at this point in the history
…es are correct from the start (#1961)
  • Loading branch information
JasonGross authored Sep 21, 2024
1 parent 9757358 commit 30b7261
Show file tree
Hide file tree
Showing 27 changed files with 81 additions and 122 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/coq-docker.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down Expand Up @@ -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:
Expand Down
47 changes: 28 additions & 19 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -194,23 +194,32 @@ 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
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
Expand All @@ -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

Expand Down
6 changes: 3 additions & 3 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down
26 changes: 12 additions & 14 deletions Makefile.config
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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))
Expand All @@ -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)
66 changes: 9 additions & 57 deletions Makefile.standalone
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand All @@ -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 $<'
Expand Down Expand Up @@ -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)



Expand All @@ -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)
Expand All @@ -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 \
Expand Down
2 changes: 1 addition & 1 deletion fiat-html/wasm_fiat_crypto_worker.js
Original file line number Diff line number Diff line change
@@ -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 () {
Expand Down
Original file line number Diff line number Diff line change
@@ -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.
4 changes: 4 additions & 0 deletions src/ExtractionOCaml/WithBedrock/base_conversion.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
Import Bedrock2Later.

Extraction "src/ExtractionOCaml/WithBedrock/base_conversion.tmp" BaseConversion.main.
4 changes: 4 additions & 0 deletions src/ExtractionOCaml/WithBedrock/dettman_multiplication.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
Import Bedrock2Later.

Extraction "src/ExtractionOCaml/WithBedrock/dettman_multiplication.tmp" DettmanMultiplication.main.
Original file line number Diff line number Diff line change
@@ -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.
4 changes: 4 additions & 0 deletions src/ExtractionOCaml/WithBedrock/saturated_solinas.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
Import Bedrock2Later.

Extraction "src/ExtractionOCaml/WithBedrock/saturated_solinas.tmp" SaturatedSolinas.main.
4 changes: 4 additions & 0 deletions src/ExtractionOCaml/WithBedrock/solinas_reduction.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
Import Bedrock2Later.

Extraction "src/ExtractionOCaml/WithBedrock/solinas_reduction.tmp" SaturatedSolinas.main.
4 changes: 4 additions & 0 deletions src/ExtractionOCaml/WithBedrock/unsaturated_solinas.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
Import Bedrock2Later.

Extraction "src/ExtractionOCaml/WithBedrock/unsaturated_solinas.tmp" UnsaturatedSolinas.main.
4 changes: 4 additions & 0 deletions src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
Import Bedrock2Later.

Extraction "src/ExtractionOCaml/WithBedrock/word_by_word_montgomery.tmp" WordByWordMontgomery.main.
4 changes: 0 additions & 4 deletions src/ExtractionOCaml/with_bedrock2_base_conversion.v

This file was deleted.

4 changes: 0 additions & 4 deletions src/ExtractionOCaml/with_bedrock2_dettman_multiplication.v

This file was deleted.

4 changes: 0 additions & 4 deletions src/ExtractionOCaml/with_bedrock2_saturated_solinas.v

This file was deleted.

4 changes: 0 additions & 4 deletions src/ExtractionOCaml/with_bedrock2_solinas_reduction.v

This file was deleted.

4 changes: 0 additions & 4 deletions src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v

This file was deleted.

4 changes: 0 additions & 4 deletions src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v

This file was deleted.

0 comments on commit 30b7261

Please sign in to comment.