diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml index 55f2341be29..7495a43b749 100644 --- a/.github/workflows/coq-alpine.yml +++ b/.github/workflows/coq-alpine.yml @@ -51,34 +51,48 @@ jobs: - name: make deps shell: alpine.sh {0} run: make TIMED=1 TIMING=1 -j2 deps - - name: all-except-generated + - name: all-except-generated-and-js-of-ocaml shell: alpine.sh {0} - run: make TIMED=1 TIMING=1 -j2 CAMLEXTRAFLAGS="-ccopt -static" all-except-generated - - name: generated-files - shell: alpine.sh {0} - run: make TIMED=1 TIMING=1 -j2 generated-files - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files - uses: actions/upload-artifact@v3 - with: - name: generated-files-${{ matrix.alpine }} - path: generated-files.tgz - if: ${{ failure() }} + run: make TIMED=1 TIMING=1 -j2 CAMLEXTRAFLAGS="-ccopt -static" all-except-generated-and-js-of-ocaml - name: install-standalone-unified-ocaml shell: alpine.sh {0} run: make install-standalone-unified-ocaml BINDIR=dist +# - name: install-standalone-js-of-ocaml +# shell: alpine.sh {0} +# run: make install-standalone-js-of-ocaml - name: upload standalone files uses: actions/upload-artifact@v3 with: name: standalone-${{ matrix.alpine }} path: dist/fiat_crypto +# - name: upload standalone js files +# uses: actions/upload-artifact@v3 +# with: +# name: standalone-html-${{ matrix.alpine }} +# path: fiat-html - name: upload OCaml files uses: actions/upload-artifact@v3 with: name: ExtractionOCaml-${{ matrix.alpine }} path: src/ExtractionOCaml if: always () +# - name: upload js_of_ocaml files +# uses: actions/upload-artifact@v3 +# with: +# name: ExtractionJsOfOCaml-${{ matrix.alpine }} +# path: src/ExtractionJsOfOCaml +# if: always () + - name: generated-files + shell: alpine.sh {0} + run: make TIMED=1 TIMING=1 -j2 generated-files + - run: tar -czvf generated-files.tgz fiat-*/ + if: ${{ failure() }} + - name: upload generated files + uses: actions/upload-artifact@v3 + with: + name: generated-files-${{ matrix.alpine }} + path: generated-files.tgz + if: ${{ failure() }} - name: standalone-haskell shell: alpine.sh {0} run: make TIMED=1 TIMING=1 -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' @@ -93,13 +107,13 @@ jobs: run: make TIMED=1 TIMING=1 -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - name: install shell: alpine.sh {0} - run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml + run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 SKIP_REGENERATING_EVERYTHING_V=1 install install-standalone-ocaml - name: install-without-bedrock2 shell: alpine.sh {0} - run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml + run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 SKIP_REGENERATING_EVERYTHING_V=1 install-without-bedrock2 install-standalone-ocaml - name: install-dev shell: alpine.sh {0} - run: sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml + run: sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 SKIP_REGENERATING_EVERYTHING_V=1 install install-standalone-ocaml - name: display timing info run: cat time-of-build-pretty.log || true - name: display per-line timing info diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml index f2cb4315cfd..cdc392341fc 100644 --- a/.github/workflows/coq-debian.yml +++ b/.github/workflows/coq-debian.yml @@ -43,9 +43,9 @@ jobs: - name: make deps shell: in-debian-chroot.sh {0} run: etc/ci/github-actions-make.sh -j2 deps - - name: all-except-generated + - name: all-except-generated-and-js-of-ocaml shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 all-except-generated + run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml - name: generated-files shell: in-debian-chroot.sh {0} run: etc/ci/github-actions-make.sh -j2 generated-files @@ -60,17 +60,34 @@ jobs: - name: install-standalone-unified-ocaml shell: in-debian-chroot.sh {0} run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist + - name: standalone-js-of-ocaml + shell: in-debian-chroot.sh {0} + run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml + - name: install-standalone-js-of-ocaml + shell: in-debian-chroot.sh {0} + run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml - name: upload standalone files uses: actions/upload-artifact@v3 with: name: standalone-${{ matrix.env.DEBIAN }} path: dist/fiat_crypto + - name: upload standalone js files + uses: actions/upload-artifact@v3 + with: + name: standalone-html-${{ matrix.env.DEBIAN }} + path: fiat-html - name: upload OCaml files uses: actions/upload-artifact@v3 with: name: ExtractionOCaml-${{ matrix.env.DEBIAN }} path: src/ExtractionOCaml if: always () + - name: upload js_of_ocaml files + uses: actions/upload-artifact@v3 + with: + name: ExtractionJsOfOCaml-${{ matrix.env.DEBIAN }} + path: src/ExtractionJsOfOCaml + if: always () - name: standalone-haskell shell: in-debian-chroot.sh {0} run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' @@ -85,13 +102,13 @@ jobs: run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - name: install shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml + run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 SKIP_REGENERATING_EVERYTHING_V=1 install install-standalone-ocaml - name: install-without-bedrock2 shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml + run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 SKIP_REGENERATING_EVERYTHING_V=1 install-without-bedrock2 install-standalone-ocaml - name: install-dev shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml + run: sudo etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 SKIP_REGENERATING_EVERYTHING_V=1 install install-standalone-ocaml - name: display timing info run: cat time-of-build-pretty.log - name: display per-line timing info diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 21427763eb9..bcce6431407 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -56,7 +56,43 @@ jobs: coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated + custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated-and-js-of-ocaml + - name: standalone-js-of-ocaml + uses: coq-community/docker-coq-action@v1 + with: + coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} + ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} + export: CI ALLOW_DIFF COQCHKEXTRAFLAGS + custom_script: | + eval $(opam env) + opam install -y js_of_ocaml + etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 standalone-js-of-ocaml + - name: install-standalone-js-of-ocaml + run: make -f Makefile.standalone install-standalone-js-of-ocaml + - name: backup .gitignore + run: mv .gitignore{,.bak} + - name: Deploy js_of_ocaml 🚀 ${{ ( github.ref != 'refs/heads/master' && '(dry run)' ) || '' }} + uses: JamesIves/github-pages-deploy-action@v4.4.3 + with: + branch: gh-pages # The branch the action should deploy to. + folder: fiat-html # The folder the action should deploy. + git-config-email: JasonGross@users.noreply.github.com + target-folder: . + single-commit: true # otherwise the repo will get too big + dry-run: ${{ github.ref != 'refs/heads/master' }} + - name: restore .gitignore + run: mv .gitignore{.bak,} + - name: upload standalone js files + uses: actions/upload-artifact@v3 + with: + name: standalone-html-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }} + path: fiat-html + - name: upload js_of_ocaml files + uses: actions/upload-artifact@v3 + with: + name: ExtractionJsOfOCaml-${{ matrix.env.COQ_VERSION }} + path: src/ExtractionJsOfOCaml + if: always () - name: generated-files run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -f Makefile.examples -j2 generated-files if: github.event_name == 'pull_request' || ${{ matrix.env.COQ_VERSION }} != 'master' diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml index cef2ba7b9fc..e9c376262f1 100644 --- a/.github/workflows/coq-macos.yml +++ b/.github/workflows/coq-macos.yml @@ -52,6 +52,15 @@ jobs: OPAMYES: "true" OPAMCONFIRMLEVEL: "unsafe-yes" + - name: Install js_of_ocaml + run: | + set -e + eval $(opam env) + opam install js_of_ocaml + env: + OPAMYES: "true" + OPAMCONFIRMLEVEL: "unsafe-yes" + - name: echo build params run: | eval $(opam env) @@ -70,6 +79,11 @@ jobs: eval $(opam env) etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist + - name: install-standalone-js-of-ocaml + run: | + eval $(opam env) + etc/ci/github-actions-make.sh install-standalone-js-of-ocaml + - name: only-test-amd64-files-lite run: | eval $(opam env) @@ -80,23 +94,33 @@ jobs: with: name: ExtractionOCaml path: src/ExtractionOCaml + - name: upload js_of_ocaml files + uses: actions/upload-artifact@v3 + with: + name: ExtractionJsOfOCaml + path: src/ExtractionJsOfOCaml - name: upload standalone files uses: actions/upload-artifact@v3 with: name: standalone-macos path: dist/fiat_crypto + - name: upload standalone js files + uses: actions/upload-artifact@v3 + with: + name: standalone-html-macos + path: fiat-html - name: install run: | eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml + etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 SKIP_REGENERATING_EVERYTHING_V=1 install install-standalone-ocaml - name: install-without-bedrock2 run: | eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml + etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 SKIP_REGENERATING_EVERYTHING_V=1 install-without-bedrock2 install-standalone-ocaml - name: install-dev run: | eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml + etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 SKIP_REGENERATING_EVERYTHING_V=1 install install-standalone-ocaml - name: display timing info run: cat time-of-build-pretty.log - name: display per-line timing info diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml index cc96accd6c2..6895e2156e5 100644 --- a/.github/workflows/coq-windows.yml +++ b/.github/workflows/coq-windows.yml @@ -49,6 +49,7 @@ jobs: default: https://github.com/ocaml/opam-repository.git - run: opam depext coq.${{ env.COQ_VERSION }} - run: opam pin add --kind=version coq ${{ env.COQ_VERSION }} + - run: opam install js_of_ocaml - name: Install System Dependencies run: | @@ -76,13 +77,22 @@ jobs: run: | %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist' shell: cmd + - name: coq run: | %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 coq' shell: cmd - - name: all-except-generated + - name: all-except-generated-and-js-of-ocaml + run: | + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 all-except-generated-and-js-of-ocaml' + shell: cmd + - name: standalone-js-of-ocaml + run: | + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 standalone-js-of-ocaml' + shell: cmd + - name: install-standalone-js-of-ocaml run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 all-except-generated' + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh install-standalone-js-of-ocaml' shell: cmd - name: c-files lite-generated-files run: | @@ -97,22 +107,32 @@ jobs: with: name: ExtractionOCaml path: src/ExtractionOCaml + - name: upload js_of_ocaml files + uses: actions/upload-artifact@v3 + with: + name: ExtractionJsOfOCaml + path: src/ExtractionJsOfOCaml - name: upload standalone files uses: actions/upload-artifact@v3 with: name: standalone-windows path: dist/fiat_crypto.exe + - name: upload standalone js files + uses: actions/upload-artifact@v3 + with: + name: standalone-html-windows + path: fiat-html - name: install run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml' + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 SKIP_REGENERATING_EVERYTHING_V=1 install install-standalone-ocaml' shell: cmd - name: install-without-bedrock2 run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml' + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 SKIP_REGENERATING_EVERYTHING_V=1 install-without-bedrock2 install-standalone-ocaml' shell: cmd - name: install-dev run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml' + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 SKIP_REGENERATING_EVERYTHING_V=1 install install-standalone-ocaml' shell: cmd - name: display timing info run: type time-of-build-pretty.log diff --git a/.gitignore b/.gitignore index a571427f68e..45de5854d02 100644 --- a/.gitignore +++ b/.gitignore @@ -204,6 +204,10 @@ src/ExtractionOCaml/perf_unsaturated_solinas src/ExtractionOCaml/perf_word_by_word_montgomery src/ExtractionOCaml/*.ml src/ExtractionOCaml/*.mli +src/ExtractionJsOfOCaml/*.ml +src/ExtractionJsOfOCaml/*.mli +src/ExtractionJsOfOCaml/*.js +src/ExtractionJsOfOCaml/*.map src/Rewriter/PerfTesting/Specific/generated/*.v src/Rewriter/PerfTesting/Specific/generated/*.log src/Rewriter/PerfTesting/Specific/generated/*.sh @@ -216,6 +220,8 @@ fiat-amd64/*.status fiat-amd64/*.only-status fiat-amd64/*.description fiat-amd64/*.invocation +fiat-html/fiat_crypto.js +fiat-html/fiat_crypto.map /Makefile.test-amd64-files.mk # Rust diff --git a/Makefile b/Makefile index 8f456d8c3d9..35f7fa72450 100644 --- a/Makefile +++ b/Makefile @@ -7,7 +7,7 @@ bedrock2 clean-bedrock2 install-bedrock2 coqutil clean-coqutil install-coqutil \ bedrock2-compiler clean-bedrock2-compiler install-bedrock2-compiler \ rupicola clean-rupicola install-rupicola \ - util all-except-generated all \ + util all-except-generated all all-except-generated-and-js-of-ocaml all-except-js-of-ocaml \ bedrock2-backend \ deps \ nobigmem print-nobigmem \ @@ -69,8 +69,10 @@ PERFTESTING_VO := \ src/Rewriter/PerfTesting/Core.vo \ src/Rewriter/PerfTesting/StandaloneOCamlMain.vo 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/Assembly/WithBedrock/% \ @@ -148,8 +150,10 @@ CHECK_OUTPUTS := $(addprefix check-,$(OUTPUT_PREOUTS)) ACCEPT_OUTPUTS := $(addprefix accept-,$(OUTPUT_PREOUTS) fiat-amd64.test) all-except-compiled: coq pre-standalone-extracted check-output -all-except-generated: standalone-ocaml perf-standalone all-except-compiled -all: all-except-generated generated-files copy-to-fiat-rust copy-to-fiat-go +all-except-generated-and-js-of-ocaml: standalone-ocaml perf-standalone all-except-compiled +all-except-generated: all-except-generated-and-js-of-ocaml standalone-js-of-ocaml +all-except-js-of-ocaml: all-except-generated-and-js-of-ocaml generated-files +all: all-except-generated-and-js-of-ocaml standalone-js-of-ocaml generated-files copy-to-fiat-rust copy-to-fiat-go @true coq: $(REGULAR_VOFILES) coq-without-bedrock2: $(REGULAR_EXCEPT_BEDROCK2_VOFILES) @@ -194,6 +198,7 @@ EXTERNAL_BEDROCK2?= EXTERNAL_COQUTIL?= EXTERNAL_REWRITER?= EXTERNAL_COQPRIME?= +SKIP_REGENERATING_EVERYTHING_V?= ifneq ($(EXTERNAL_DEPENDENCIES),1) @@ -336,6 +341,8 @@ $(BEDROCK2_STANDALONE:%=src/ExtractionOCaml/%.ml): src/Bedrock/Standalone/Standa $(PERF_STANDALONE:%=src/ExtractionOCaml/%.ml): src/Rewriter/PerfTesting/StandaloneOCamlMain.vo $(STANDALONE:%=src/ExtractionHaskell/%.hs): src/StandaloneHaskellMain.vo $(BEDROCK2_STANDALONE:%=src/ExtractionHaskell/%.hs): src/Bedrock/Standalone/StandaloneHaskellMain.vo +$(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml): src/StandaloneJsOfOCamlMain.vo +$(BEDROCK2_STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml): src/Bedrock/Standalone/StandaloneJsOfOCamlMain.vo # $(PERF_STANDALONE:%=src/ExtractionHaskell/%.hs): src/Rewriter/PerfTesting/StandaloneHaskellMain.vo pre-standalone-extracted: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) @@ -346,7 +353,13 @@ $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) : %.ml : %.v $(HIDE)cat $*.tmp.ml | tr -d '\r' > $@ && rm $*.tmp.ml $(HIDE)cat $*.tmp.mli | tr -d '\r' > $*.mli && rm $*.tmp.mli -$(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/haskell.sed +$(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml) : %.ml : %.v + $(SHOW)'COQC $<' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + $(HIDE)cat $*.tmp.ml | tr -d '\r' > $@ && rm $*.tmp.ml + $(HIDE)cat $*.tmp.mli | tr -d '\r' > $*.mli && rm $*.tmp.mli + +$(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/haskell.sed src/StandaloneHaskellMain.vo $(SHOW)'COQC $< > $@' $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp $(HIDE)cat $@.tmp | tr -d '\r' | sed -f src/haskell.sed > $@ && rm $@.tmp @@ -523,6 +536,7 @@ EXISTING_EVERYTHING_V_CONTENTS:=$(shell cat src/Everything.v 2>&1) EXISTING_BEDROCK_EVERYTHING_V_CONTENTS:=$(shell cat src/Bedrock/Everything.v 2>&1) NEW_EVERYTHING_V_CONTENTS:=$(shell $(make_Everything_v_cmd)) NEW_BEDROCK_EVERYTHING_V_CONTENTS:=$(shell $(make_Bedrock_Everything_v_cmd)) +ifneq ($(SKIP_REGENERATING_EVERYTHING_V),1) ifneq ($(EXISTING_EVERYTHING_V_CONTENTS),$(NEW_EVERYTHING_V_CONTENTS)) .PHONY: src/Everything.v src/Everything.v: @@ -536,3 +550,4 @@ src/Bedrock/Everything.v: $(SHOW)'ECHO > $@' $(HIDE)$(make_Bedrock_Everything_v_cmd) > $@ endif +endif diff --git a/Makefile.config b/Makefile.config index afed0c3954a..825b3b0ffb4 100644 --- a/Makefile.config +++ b/Makefile.config @@ -5,6 +5,7 @@ SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) BINDIR?=/usr/local/bin +JSDIR?=fiat-html # or $(shell opam config var bin) ? MOD_NAME := Crypto @@ -56,8 +57,8 @@ 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)) +UNIFIED_STANDALONE := $(UNIFIED_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_UNIFIED_STANDALONE)) +SEPARATE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_SEPARATE_STANDALONE)) STANDALONE := $(UNIFIED_STANDALONE) $(SEPARATE_STANDALONE) PERF_STANDALONE := perf_unsaturated_solinas perf_word_by_word_montgomery @@ -68,12 +69,16 @@ UNIFIED_STANDALONE_HASKELL := $(UNIFIED_STANDALONE) SEPARATE_STANDALONE_HASKELL := $(SEPARATE_STANDALONE) STANDALONE_HASKELL := $(UNIFIED_STANDALONE_HASKELL) $(SEPARATE_STANDALONE_HASKELL) +STANDALONE_JS_OF_OCAML := $(UNIFIED_STANDALONE) +BEDROCK2_STANDALONE_JS_OF_OCAML := $(BEDROCK2_UNIFIED_STANDALONE) + 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) +JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.map) WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) @@ -81,3 +86,4 @@ WITH_BEDROCK2_OCAML_BINARIES := $(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES) $(WITH_B 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_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) diff --git a/Makefile.standalone b/Makefile.standalone index 38722b5626d..fef87709b9b 100644 --- a/Makefile.standalone +++ b/Makefile.standalone @@ -12,6 +12,7 @@ GHCFLAGS?= # -XStrict # in case we didn't include Makefile.coq OCAMLFIND?=ocamlfind OCAMLOPT?="$(OCAMLFIND)" ocamlopt +OCAMLC?="$(OCAMLFIND)" ocamlc OCAMLOPTP?="$(OCAMLFIND)" ocamloptp ifneq ($(WITH_PERF),1) CAMLOPT_PERF ?= $(OCAMLOPT) @@ -21,7 +22,11 @@ CAMLOPT_PERF ?= $(OCAMLOPTP) CAMLOPT_PERF_SHOW:=OCAMLOPTP endif CAMLEXTRAFLAGS ?= +JS_OF_OCAML ?= js_of_ocaml STANDALONE_CAMLFLAGS ?= -package unix -w -20 -g $(CAMLEXTRAFLAGS) +STANDALONE_JS_CAMLFLAGS ?= -package js_of_ocaml $(STANDALONE_CAMLFLAGS) +JS_OF_OCAML_EXTRAFLAGS ?= +JS_OF_OCAML_FLAGS ?= --source-map --no-inline $(JS_OF_OCAML_EXTRAFLAGS) PACKAGE ?= standalone.tar.gz PACKAGE_CMD ?= tar -czvf @@ -41,6 +46,7 @@ ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true 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 \ + standalone-js-of-ocaml install-standalone-js-of-ocaml uninstall-standalone-js-of-ocaml \ package-standalone package-standalone-ocaml package-standalone-haskell \ package-standalone-unified package-standalone-unified-ocaml package-standalone-unified-haskell \ package-standalone-separate package-standalone-separate-ocaml package-standalone-separate-haskell \ @@ -58,12 +64,27 @@ $(STANDALONE_OCAML:%=src/ExtractionOCaml/%) : % : %.ml %.cmi $(HIDE)$(ENSURE_STACK_LIMIT); \ $(TIMER) $(CAMLOPT_PERF) $(STANDALONE_CAMLFLAGS) -linkpkg -I src/ExtractionOCaml/ -o $@ $< +$(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.cmi) : %.cmi : %.ml + $(SHOW)'OCAMLC $*.mli' + $(HIDE)$(ENSURE_STACK_LIMIT); \ + $(TIMER) $(OCAMLC) $(STANDALONE_JS_CAMLFLAGS) $*.mli + +$(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 $@ $< + +$(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.js) : %.js : %.byte + $(SHOW)'JS_OF_OCAML $<' + $(HIDE)$(ENSURE_STACK_LIMIT); \ + $(TIMER) $(JS_OF_OCAML) $(JS_OF_OCAML_FLAGS) $< + $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%) : % : %.hs $(SHOW)'GHC $< -o $@' $(HIDE)$(TIMER) $(GHC) $(GHCFLAGS) -o $@ $< -standalone: standalone-haskell standalone-ocaml -standalone-unified: standalone-unified-haskell standalone-unified-ocaml +standalone: standalone-haskell standalone-ocaml standalone-js-of-ocaml +standalone-unified: standalone-unified-haskell standalone-unified-ocaml standalone-js-of-ocaml standalone-separate: standalone-separate-haskell standalone-separate-ocaml perf-standalone: $(PERF_STANDALONE:%=src/ExtractionOCaml/%) @@ -73,13 +94,22 @@ 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 +standalone-js-of-ocaml: $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.js) + uninstall-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES) uninstall-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES) uninstall-standalone-separate-ocaml: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES) uninstall-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES) uninstall-standalone-unified-haskell: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES) uninstall-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES) +uninstall-standalone-js-of-ocaml: FILESTOINSTALL=$(JS_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: PERMS=0755 +install-standalone-js-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) + + ifeq ($(SKIP_BEDROCK2),1) install-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES) @@ -88,15 +118,16 @@ install-standalone-separate-ocaml: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES) install-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES) install-standalone-unified-haskell: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES) install-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES) +install-standalone-js-of-ocaml: FILESTOINSTALL=$(JS_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-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: $(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 "$(BINDIR)/" &&\ - install -m 0755 "$$f" "$(BINDIR)/" &&\ - echo INSTALL "$$f" "$(BINDIR)/";\ + install -d "$(INSTALLDIR)/" &&\ + install -m $(PERMS) "$$f" "$(INSTALLDIR)/" &&\ + echo INSTALL "$$f" "$(INSTALLDIR)/";\ done else install-standalone-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES) @@ -105,6 +136,7 @@ install-standalone-separate-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_OCAML 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-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\ @@ -114,15 +146,29 @@ install-standalone-ocaml install-standalone-unified-ocaml install-standalone-sep fdir="$$(dirname "$$f")" &&\ fname="$$(basename "$$f")" &&\ df="$${fname#with_bedrock2_}" &&\ - install -d "$(BINDIR)/" &&\ - install -m 0755 "$$f" "$(BINDIR)/$$df" &&\ - echo INSTALL "$$f" "$(BINDIR)/$$df";\ + install -d "$(INSTALLDIR)/" &&\ + install -m $(PERMS) "$$f" "$(INSTALLDIR)/$$df" &&\ + echo INSTALL "$$f" "$(INSTALLDIR)/$$df";\ + done +install-standalone-js-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 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-ocaml uninstall-standalone-unified-ocaml uninstall-standalone-separate-ocaml uninstall-standalone-haskell uninstall-standalone-unified-haskell uninstall-standalone-separate-haskell uninstall-standalone-js-of-ocaml: $(HIDE)for f in $(FILESTOINSTALL); do \ - instf="$(BINDIR)/`basename $$f`" &&\ + instf="$(INSTALLDIR)/`basename $$f`" &&\ rm -f "$$instf" &&\ echo RM "$$instf"; \ done diff --git a/etc/ci/setup-debian-chroot.sh b/etc/ci/setup-debian-chroot.sh index f031dc32ef9..de790cb5c25 100755 --- a/etc/ci/setup-debian-chroot.sh +++ b/etc/ci/setup-debian-chroot.sh @@ -11,7 +11,7 @@ sudo apt-get -q -y -o Acquire::Retries=30 install debootstrap sudo debootstrap --variant=minbase "$debian" /chroot http://debian-archive.trafficmanager.net/debian/ || ( cat /tmp/tmp.*/debootstrap/debootstrap.log ; exit 1 ) sudo mount proc /chroot/proc -t proc sudo mount sysfs /chroot/sys -t sysfs -sudo chroot /chroot apt-get -q -y -o Acquire::Retries=30 install sudo git make time jq python3 python-is-python3 ocaml coq libcoq-core-ocaml-dev libfindlib-ocaml-dev ocaml-findlib cabal-install +sudo chroot /chroot apt-get -q -y -o Acquire::Retries=30 install sudo git make time jq python3 python-is-python3 ocaml coq libcoq-core-ocaml-dev libfindlib-ocaml-dev ocaml-findlib cabal-install js-of-ocaml sudo chroot /chroot groupadd -g "$(id -g)" "$(id -g -n)" sudo chroot /chroot useradd -g "$(id -g)" -u "$(id -u)" "$(id -u -n)" printf "%s ALL=(ALL) NOPASSWD: ALL\n" "$(id -u -n)" | sudo tee /chroot/etc/sudoers.d/root diff --git a/fiat-html/copy-button.js b/fiat-html/copy-button.js new file mode 100644 index 00000000000..375d80edd0a --- /dev/null +++ b/fiat-html/copy-button.js @@ -0,0 +1,18 @@ +// JavaScript for copy functionality +document.addEventListener('click', function(e) { + if (e.target.matches('.copy-button')) { + const button = e.target; + const targetId = button.getAttribute('data-target'); + const codeText = document.getElementById(targetId).textContent; + + navigator.clipboard.writeText(codeText).then(() => { + button.textContent = "Copied!"; + button.disabled = true; + + setTimeout(() => { + button.textContent = "Copy"; + button.disabled = false; + }, 3000); // Revert after 3 seconds + }); + } +}); diff --git a/fiat-html/fiat-crypto.html b/fiat-html/fiat-crypto.html new file mode 100644 index 00000000000..819704077c4 --- /dev/null +++ b/fiat-html/fiat-crypto.html @@ -0,0 +1,71 @@ + + + + + Fiat Cryptography Web Interface + + + + + + + + + + + diff --git a/fiat-html/index.html b/fiat-html/index.html new file mode 120000 index 00000000000..d260c79135e --- /dev/null +++ b/fiat-html/index.html @@ -0,0 +1 @@ +fiat-crypto.html \ No newline at end of file diff --git a/fiat-html/main.js b/fiat-html/main.js new file mode 100644 index 00000000000..555f06fa9b8 --- /dev/null +++ b/fiat-html/main.js @@ -0,0 +1,271 @@ +// Written with help from https://chat.openai.com/share/74d5901c-9005-4560-8307-582ff54e403e +document.addEventListener('DOMContentLoaded', function() { + const errorDiv = document.getElementById('error'); + const outputDiv = document.getElementById('output'); + const stdoutDiv = document.getElementById('stdoutContainer'); + const stderrDiv = document.getElementById('stderrContainer'); + const stdoutBox = document.getElementById('stdout'); + const stderrBox = document.getElementById('stderr'); + const inputForm = document.getElementById('inputForm'); + const inputArgs = document.getElementById('inputArgs'); + const synthesizeButton = document.getElementById('synthesizeButton'); + const cancelButton = document.getElementById('cancelButton'); + const permalink = document.getElementById('permalink'); + const statusSpan = document.getElementById('status'); + const isSafari = /^((?!chrome|android).)*safari/i.test(navigator.userAgent); + const isMacOrIOS = /Macintosh|MacIntel|MacPPC|Mac68K|iPhone|iPad|iPod/.test(navigator.platform); + + function splitUnescapedSpaces(input) { + return input + .replace(/\\\\/g, '\u0000') // Temporarily replace \\ with a placeholder + .replace(/\\ /g, '\u0001') // Temporarily replace escaped spaces with a placeholder + .split(/ +/) // Split by spaces + .filter(s => s) + .map(s => s + .replace(/\u0000/g, '\\') // Restore backslashes + .replace(/\u0001/g, ' ') // Restore spaces + ); + } + + function joinWithEscaping(inputArray) { + return inputArray + .map(s => s + .replace(/\\/g, '\\\\') // Escape backslashes + .replace(/ /g, '\\ ') // Escape spaces + ) + .join(' '); + } + + function parseToStringArray(str) { + let args = JSON.parse(str); + if (!Array.isArray(args) || !args.every(arg => typeof arg === 'string')) { + throw new Error('Invalid: Not an array of strings'); + } + return args; + } + + function isValidJsonStringArray(str) { + try { + parseToStringArray(str); + return true; + } catch (e) { + return false; + } + } + + function validateInput() { + const isJson = document.querySelector('input[name="inputType"][value="json"]').checked; + const isValid = !isJson || isValidJsonStringArray(inputArgs.value); + synthesizeButton.disabled = !isValid; + document.querySelector('input[name="inputType"]:not([value="json"])').disabled = !isValid; + } + + function enableForm() { + inputArgs.disabled = false; + synthesizeButton.disabled = false; + cancelButton.disabled = true; + } + + function clearOutput() { + errorDiv.textContent = ''; + stdoutBox.textContent = ''; + stderrBox.textContent = ''; + errorDiv.classList.add('hidden'); + outputDiv.classList.add('hidden'); + stderrDiv.classList.add('hidden'); + stdoutDiv.classList.add('hidden'); + } + + function escapeHtml(html) { + var text = document.createTextNode(html); + var p = document.createElement('p'); + p.appendChild(text); + return p.innerHTML; + } + + + function displayError(message, isHtml = false) { + if (isHtml) { + errorDiv.innerHTML = message; + } else { + errorDiv.textContent = message; + } + if (message) { + errorDiv.classList.remove('hidden'); + const consoleMessage = message.replace(//gi, '\n'); + console.error(consoleMessage); + } else { + errorDiv.classList.add('hidden'); + } + enableForm(); + } + + function displayOutput(stdout, stderr) { + stdoutBox.textContent = stdout; + stderrBox.textContent = stderr; + outputDiv.classList.remove('hidden'); + if (stdout) { + stdoutDiv.classList.remove('hidden'); + } else { + stdoutDiv.classList.add('hidden'); + } + if (stderr) { + console.error(stderr); + stderrDiv.classList.remove('hidden'); + } else { + stderrDiv.classList.add('hidden'); + } + enableForm(); + } + + function updatePermalink(args) { + const queryString = `?argv=${encodeURIComponent(JSON.stringify(args.slice(1)))}&interactive`; + // Handle both file and http(s) URLs + let baseUrl = window.location.href.split('?')[0]; // Get base URL without query string + permalink.href = baseUrl + queryString; + permalink.classList.remove('hidden'); + } + + function updateStatus(message) { + statusSpan.textContent = message; + if (message) { + statusSpan.classList.remove('hidden'); + } else { + statusSpan.classList.add('hidden'); + } + } + + function handleSynthesisResult(result) { + const success = result[0]; + const exceptionText = result[1]; + const stdout = result[2]; + const stderr = result[3]; + const files = result[4]; + + if (!success) { + displayError(exceptionText.join('\n')); + } + displayOutput(stdout.join(''), stderr.join('')); + } + + function handleException(err) { + let errorMessage = `Synthesis failed: ${escapeHtml(err.toString())}`; + + if (/stack size exceeded|[Tt]oo much recursion/.test(err.message)) { + if (!isSafari) { + errorMessage += "
Unfortunately Chrome, Firefox, and the ECMAScript Standard don't support proper tail-call elimination for unfortunate historical reasons."; + + if (!isMacOrIOS) { + errorMessage += "
Consider opening this page in Safari on a Mac or iOS device instead."; + } else { + errorMessage += "
Consider opening this page in Safari instead."; + } + } + } + + clearOutput(); + displayError(errorMessage, true); + updateStatus(""); // Clear status + } + + + + var curSynthesisPromise; + function handleSynthesis(args) { + const startTime = performance.now(); + console.log({'synthesize args': args}); + updateStatus("Synthesizing..."); + updatePermalink(args); + const synthesisPromise = new Promise((resolve, reject) => { + try { + resolve(synthesize(args)) + } catch (error) { + reject(error); + } + }); + curSynthesisPromise = synthesisPromise; + synthesisPromise + .then((value) => { + if (curSynthesisPromise === synthesisPromise) { + const endTime = performance.now(); + clearOutput(); + updateStatus(`Synthesis completed in ${(endTime - startTime) / 1000} seconds`); + handleSynthesisResult(value); + } else { + console.log(`Synthesis of ${args} completed after being canceled: ${value}`); + } + }) + .catch((err) => { + if (curSynthesisPromise === synthesisPromise) { + handleException(err); + } else { + console.log(`Synthesis of ${args} errored after being canceled: ${err}`); + } + }); + } + + function parseAndRun(argv) { + try { + let args = parseToStringArray(decodeURIComponent(argv)); + args.unshift('fiat_crypto.js'); + handleSynthesis(args); + } catch (e) { + displayError(`Error: ${e.message}: ${argv}`); + } + } + + const queryParams = new URLSearchParams(window.location.search); + const argv = queryParams.get('argv'); + const interactive = queryParams.get('interactive'); + + if (argv) { + if (interactive !== null && interactive != 'false' && interactive != '0') { + inputArgs.value = decodeURIComponent(argv); + document.querySelector('input[value="json"]').checked = true; + inputForm.classList.remove('hidden'); + } + parseAndRun(argv); + } else { + inputForm.classList.remove('hidden'); + } + + inputArgs.addEventListener('input', validateInput); + + document.querySelectorAll('input[name="inputType"]').forEach(radio => { + radio.addEventListener('change', function() { + if (this.value === 'string') { + if (isValidJsonStringArray(inputArgs.value)) { + inputArgs.value = joinWithEscaping(JSON.parse(inputArgs.value)); + } + } else if (this.value === 'json') { + inputArgs.value = JSON.stringify(splitUnescapedSpaces(inputArgs.value)); + } + validateInput(); + }); + }); + + synthesizeButton.addEventListener('click', function() { + // Disable form elements + inputArgs.disabled = true; + synthesizeButton.disabled = true; + cancelButton.disabled = false; + // Parse arguments and handle synthesis + const argsType = document.querySelector('input[name="inputType"]:checked').value; + const args = argsType === 'json' ? JSON.parse(inputArgs.value) : splitUnescapedSpaces(inputArgs.value); + args.unshift('fiat_crypto.js'); + handleSynthesis(args); + }); + + inputForm.addEventListener('submit', function(event) { + event.preventDefault(); // Prevent the default form submission + synthesizeButton.click(); // Programmatically click the synthesize button + }); + + cancelButton.addEventListener('click', function() { + // Cancel synthesis if possible and re-enable form elements + inputArgs.disabled = false; + synthesizeButton.disabled = false; + cancelButton.disabled = true; + updateStatus(""); + }); +}); diff --git a/src/Bedrock/Standalone/StandaloneJsOfOCamlMain.v b/src/Bedrock/Standalone/StandaloneJsOfOCamlMain.v new file mode 100644 index 00000000000..4835ae225a7 --- /dev/null +++ b/src/Bedrock/Standalone/StandaloneJsOfOCamlMain.v @@ -0,0 +1,38 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. +Require Import Crypto.CLI. +Require Export Crypto.StandaloneJsOfOCamlMain. +Require Import Crypto.Bedrock.Field.Stringification.Stringification. +Import ListNotations. +Local Open Scope string_scope. +Local Open Scope list_scope. + +(** Needed to work around COQBUG(https://github.com/coq/coq/issues/4875) *) +Extraction Inline coqutil.Map.SortedListString.map. + +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 FiatCrypto. + Definition main : unit + := main_gen ForExtraction.FiatCrypto.PipelineMain. + End FiatCrypto. +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 FiatCrypto. + Definition main : unit + := main_gen ForExtraction.FiatCrypto.PipelineMain. + End FiatCrypto. +End Bedrock2Later. diff --git a/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v b/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..c8de96ef770 --- /dev/null +++ b/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneJsOfOCamlMain. +Import Bedrock2First. + +Extraction "src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/ExtractionJsOfOCaml/fiat_crypto.v b/src/ExtractionJsOfOCaml/fiat_crypto.v new file mode 100644 index 00000000000..58a12cc16bf --- /dev/null +++ b/src/ExtractionJsOfOCaml/fiat_crypto.v @@ -0,0 +1,3 @@ +Require Import Crypto.StandaloneJsOfOCamlMain. + +Extraction "src/ExtractionJsOfOCaml/fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v b/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..4fbc0c90d2b --- /dev/null +++ b/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneJsOfOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/StandaloneJsOfOCamlMain.v b/src/StandaloneJsOfOCamlMain.v new file mode 100644 index 00000000000..1cef5d59b78 --- /dev/null +++ b/src/StandaloneJsOfOCamlMain.v @@ -0,0 +1,187 @@ +Require Export Coq.extraction.Extraction. +Require Export Coq.extraction.ExtrOcamlBasic. +Require Export Coq.extraction.ExtrOcamlString. +Require Import Coq.Lists.List. +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. +Require Crypto.Util.Strings.String. +Require Import Crypto.CLI. +Require Import Crypto.StandaloneMonadicUtils. +Require Import Crypto.Util.Notations. +Import ListNotations. Local Open Scope string_scope. + +Global Set Warnings Append "-extraction-opaque-accessed". +Extraction Language OCaml. +Global Unset Extraction Optimize. + +(** Work around COQBUG(https://github.com/coq/coq/issues/4875) / COQBUG(https://github.com/coq/coq/issues/7954) / COQBUG(https://github.com/coq/coq/issues/7954) / https://discuss.ocaml.org/t/why-wont-ocaml-specialize-weak-type-variables-in-dead-code/7776 *) +Extraction Inline Show.ShowLevel_of_Show. + +Inductive int : Set := int_O | int_S (x : int). + +(** We pull a hack to get coqchk to not report these as axioms; for + this, all we care about is that there exists a model. *) +Module Type OCamlPrimitivesT. + Axiom OCaml_string : Set. + Notation string := OCaml_string. + Axiom string_length : string -> int. + Axiom string_get : string -> int -> Ascii.ascii. + Axiom string_init : int -> (int -> Ascii.ascii) -> string. + (*Axiom raise_Failure : string -> unit.*) + (*Axiom exn : Set. + Axiom Failure : string -> exn.*) + Axiom OCaml_array : Set -> Set. + Notation array := OCaml_array. + Axiom Array_to_list : forall {a : Set}, array a -> list a. + Axiom Array_of_list : forall {a : Set}, list a -> array a. +End OCamlPrimitivesT. + +Module Export OCamlPrimitives : OCamlPrimitivesT. + Definition OCaml_string : Set := unit. + Notation string := OCaml_string. + Definition string_length : string -> int := fun _ => int_O. + Definition string_get : string -> int -> Ascii.ascii := fun _ _ => "000"%char. + Definition string_init : int -> (int -> Ascii.ascii) -> string := fun _ _ => tt. + (*Definition raise_Failure : string -> unit := fun _ => tt.*) + (*Definition exn : Set := unit. + Definition Failure : string -> exn := fun _ => tt.*) + Definition OCaml_array (A : Set) := list A. + Notation array := OCaml_array. + Definition Array_to_list {a : Set} : array a -> list a := fun x => x. + Definition Array_of_list {a : Set} : list a -> array a := fun x => x. +End OCamlPrimitives. + +Module Type Js_of_ocamlPrimitivesT. + Axiom Js_t : Set -> Set. + Axiom js_string : Set. + Axiom js_array : Set -> Set. + Axiom js_to_array : forall {a}, Js_t (js_array a) -> array a. + Axiom js_to_string : Js_t js_string -> string. + Axiom js_of_array : forall {a}, array a -> Js_t (js_array a). + Axiom js_of_string : string -> Js_t js_string. + Axiom js_to_bool : Js_t bool -> bool. + Axiom js_of_bool : bool -> Js_t bool. + Axiom Js_Unsafe_any : Set. + Axiom Js_Unsafe_inject : forall {a : Set}, a -> Js_Unsafe_any. + Axiom Js_export : forall {a : Set}, string -> a -> unit. + Axiom js_callback : Set -> Set. + Axiom js_wrap_callback : forall {a b : Set}, (a -> b) -> js_callback (a -> b). +End Js_of_ocamlPrimitivesT. + +Module Import Js_of_ocamlPrimitives : Js_of_ocamlPrimitivesT. + Definition Js_t : Set -> Set := fun t => t. + Definition js_string : Set := string. + Definition js_array : Set -> Set := array. + Definition js_to_array : forall {a}, Js_t (js_array a) -> array a := fun _ x => x. + Definition js_to_string : Js_t js_string -> string := fun x => x. + Definition js_of_array : forall {a}, array a -> Js_t (js_array a) := fun _ x => x. + Definition js_of_string : string -> Js_t js_string := fun x => x. + Definition js_to_bool : Js_t bool -> bool := fun x => x. + Definition js_of_bool : bool -> Js_t bool := fun x => x. + Definition Js_Unsafe_any : Set := unit. + Definition Js_Unsafe_inject : forall {a : Set}, a -> Js_Unsafe_any := fun _ _ => tt. + Definition Js_export : forall {a : Set}, string -> a -> unit := fun _ _ _ => tt. + Definition js_callback : Set -> Set := fun a => a. + Definition js_wrap_callback : forall {a b : Set}, (a -> b) -> js_callback (a -> b) := fun _ _ f => f. +End Js_of_ocamlPrimitives. + +Extract Inductive int + => "Int.t" [ "0" "(fun n -> n+1)" ] + "(fun fO fS n -> if n=0 then fO () else fS (n-1))". +(* We cannot inline these constants due to COQBUG(https://github.com/coq/coq/issues/16169) *) +Extract (*Inlined*) Constant string => "string". +Extract (*Inlined*) Constant string_length => "String.length". +Extract (*Inlined*) Constant string_get => "String.get". +Extract (*Inlined*) Constant string_init => "String.init". +Extract (*Inlined*) Constant array "'a" => "'a array". +Extract (*Inlined*) Constant Array_to_list => "Array.to_list". +Extract (*Inlined*) Constant Array_of_list => "Array.of_list". + +Extract (*Inlined*) Constant Js_t "'a" => "'a Js_of_ocaml.Js.t". +Extract (*Inlined*) Constant js_string => "Js_of_ocaml.Js.js_string". +Extract (*Inlined*) Constant js_array "'a" => "'a Js_of_ocaml.Js.js_array". +Extract (*Inlined*) Constant js_to_array => "Js_of_ocaml.Js.to_array". +Extract (*Inlined*) Constant js_of_array => "Js_of_ocaml.Js.array". +Extract (*Inlined*) Constant js_to_string => "Js_of_ocaml.Js.to_string". +Extract (*Inlined*) Constant js_of_string => "Js_of_ocaml.Js.string". +Extract (*Inlined*) Constant js_to_bool => "Js_of_ocaml.Js.to_bool". +Extract (*Inlined*) Constant js_of_bool => "Js_of_ocaml.Js.bool". +Extract (*Inlined*) Constant Js_Unsafe_any => "Js_of_ocaml.Js.Unsafe.any". +Extract (*Inlined*) Constant Js_Unsafe_inject => "Js_of_ocaml.Js.Unsafe.inject". +Extract (*Inlined*) Constant Js_export => "Js_of_ocaml.Js.export". +Extract (*Inlined*) Constant js_callback "'a" => "'a Js_of_ocaml.Js.callback". +Extract (*Inlined*) Constant js_wrap_callback => "Js_of_ocaml.Js.wrap_callback". + +Fixpoint nat_of_int (x : int) : nat + := match x with + | int_O => O + | int_S x' => S (nat_of_int x') + end. +Fixpoint int_of_nat (x : nat) : int + := match x with + | O => int_O + | S x' => int_S (int_of_nat x') + end. +Global Set Warnings Append "-ambiguous-paths". +Coercion nat_of_int : int >-> nat. +Coercion int_of_nat : nat >-> int. + +Definition string_of_Coq_string (s : String.string) : string + := let s := String.list_ascii_of_string s in + string_init + (List.length s) + (fun n => List.nth n s "?"%char). + +Definition string_to_Coq_string (s : string) : String.string + := String.string_of_list_ascii + (List.map (fun n:nat => string_get s n) (List.seq 0 (string_length s))). + +Definition valid_synthesis_kinds_list : list string + := List.map string_of_Coq_string (List.map fst ForExtraction.parse_SynthesisKind_list). + +Global Existing Instance IODriverTrace. + +Definition main_gen + (PipelineMain : forall (A := _) + (argv : list String.string), + A) + : unit + := let stdin := [] in + let files := [] in + let js_of_Coq_string s := js_of_string (string_of_Coq_string s) in + let js_of_list_string ls := js_of_array (Array_of_list (List.map js_of_Coq_string ls)) in + let synthesize : js_callback (Js_t (js_array (Js_t js_string)) -> Js_t (js_array Js_Unsafe_any)) + := js_wrap_callback + (fun argv + => let argv := List.map string_to_Coq_string (List.map js_to_string (Array_to_list (js_to_array argv))) in + let '(result, (stdout, stderr), new_files) := eval_trace (PipelineMain argv) stdin files split_stdout_stderr in + js_of_array + (Array_of_list + [Js_Unsafe_inject (js_of_bool (Option.is_None result)) + ; Js_Unsafe_inject (js_of_list_string match result with Some msg => msg | None => [] end) + ; Js_Unsafe_inject (js_of_list_string stdout) + ; Js_Unsafe_inject (js_of_list_string stderr) + ; Js_Unsafe_inject + (js_of_array + (Array_of_list + (List.map + (fun '(name, contents) + => js_of_array + (Array_of_list + [Js_Unsafe_inject (js_of_Coq_string name) + ; Js_Unsafe_inject (js_of_list_string contents)])) + new_files))) + ])) + in + let valid_synthesis_kinds : Js_t (js_array (Js_t js_string)) + := js_of_list_string (List.map fst ForExtraction.parse_SynthesisKind_list) in + let 'tt := Js_export (string_of_Coq_string "synthesize") synthesize in + let 'tt := Js_export (string_of_Coq_string "valid_synthesis_kinds") valid_synthesis_kinds in + tt. + +Local Existing Instance ForExtraction.default_supported_languages. + +Module FiatCrypto. + Definition main : unit + := main_gen ForExtraction.FiatCrypto.PipelineMain. +End FiatCrypto. diff --git a/src/StandaloneMonadicUtils.v b/src/StandaloneMonadicUtils.v new file mode 100644 index 00000000000..7eb76884f5a --- /dev/null +++ b/src/StandaloneMonadicUtils.v @@ -0,0 +1,72 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. +Require Crypto.Util.Strings.String. +Require Import Crypto.CLI. +Require Import Crypto.Util.Notations. +Import ListNotations. Local Open Scope string_scope. + +Inductive trace : Set := +| finished +| err (msg : list string) +| read_stdin (k : list string -> trace) +| write_stdout (msg : list string) (k : trace) +| write_stderr (msg : list string) (k : trace) +| read_file (name : string) (k : list string -> trace) +| write_file (name : string) (contents : list string) (k : trace) +. + +Definition IODriverTrace : ForExtraction.IODriverAPI trace + := {| ForExtraction.error := err + ; ForExtraction.ret := fun 'tt => finished + ; ForExtraction.with_read_stdin := read_stdin + ; ForExtraction.write_stdout_then msg k := write_stdout msg (k tt) + ; ForExtraction.write_stderr_then msg k := write_stderr msg (k tt) + ; ForExtraction.with_read_file := read_file + ; ForExtraction.write_file_then name contents k := write_file name contents (k tt) + |}. + +Fixpoint fuse_stdout_stderr (ls : list (list string + list string)) : list string + := match ls with + | [] => [] + | inl msg :: ls | inr msg :: ls => msg ++ fuse_stdout_stderr ls + end%list. + +Fixpoint split_stdout_stderr (ls : list (list string + list string)) : list string * list string + := match ls with + | [] => ([], []) + | inl stdout :: ls + => let '(stdouts, stderrs) := split_stdout_stderr ls in + (stdout ++ stdouts, stderrs) + | inr stderr :: ls + => let '(stdouts, stderrs) := split_stdout_stderr ls in + (stdouts, stderr ++ stderrs) + end%list. + +Fixpoint eval' {A} (t : trace) (stdin : list (list string)) (files : list (string * list string)) (fuse_stdout_stderr : list (list string + list string) -> A) (stdout_stderr_r_acc : list (list string + list string)) (new_files : list (string * list string)) : option (list string) (* return *) * A (* stdout / stderr *) * list (string * list string) (* new files *) + := match t with + | finished + => (None, fuse_stdout_stderr (List.rev' stdout_stderr_r_acc), new_files) + | err msg + => (Some msg, fuse_stdout_stderr (List.rev' stdout_stderr_r_acc), new_files) + | read_stdin k + => let '(inp, stdin) := match stdin with + | inp :: stdin => (inp, stdin) + | [] => ([], []) + end in + eval' (k inp) stdin files fuse_stdout_stderr stdout_stderr_r_acc new_files + | write_stdout msg k + => eval' k stdin files fuse_stdout_stderr (inl msg :: stdout_stderr_r_acc) new_files + | write_stderr msg k + => eval' k stdin files fuse_stdout_stderr (inr msg :: stdout_stderr_r_acc) new_files + | read_file name k + => let contents := match List.find (fun '(fname, contents) => (fname =? name)%string) (new_files ++ files) with + | Some (_, contents) => contents + | None => [] + end in + eval' (k contents) stdin files fuse_stdout_stderr stdout_stderr_r_acc new_files + | write_file name contents k + => eval' k stdin files fuse_stdout_stderr stdout_stderr_r_acc ((name, contents) :: new_files) + end. +Definition eval_trace {A} (t : trace) (stdin : list (list string)) (files : list (string * list string)) (fuse_stdout_stderr : list (list string + list string) -> A) : option (list string) (* return *) * A (* stdout / stderr *) * list (string * list string) (* new files *) + := eval' t stdin files fuse_stdout_stderr [] [].