Add js_of_ocaml build and deployment

.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'

.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'

.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/[email protected]
+      with:
+        branch: gh-pages # The branch the action should deploy to.
+        folder: fiat-html # The folder the action should deploy.
+        git-config-email: [email protected]
+        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'

.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,11 +94,21 @@ 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)

.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,11 +107,21 @@ 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'

.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

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 \
@@ -53,6 +53,7 @@ endif
 # coq .vo files that are not compiled using coq_makefile
 SPECIAL_VOFILES := \
 	src/ExtractionOCaml/%.vo \
+	src/ExtractionJsOfOCaml/%.vo \
 	src/ExtractionHaskell/%.vo \
 	src/Rewriter/PerfTesting/Specific/generated/%.vo
 GREP_EXCLUDE_SPECIAL := grep -v '^\(src/Extraction\(OCaml\|Haskell\)/\|src/Rewriter/PerfTesting/Specific/generated/\)'
@@ -69,8 +70,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 +151,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)
@@ -336,17 +341,25 @@ $(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)
+pre-standalone-extracted: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml) $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs)
 
 $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.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
+$(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) $< > [email protected]
 	$(HIDE)cat [email protected] | tr -d '\r' | sed -f src/haskell.sed > $@ && rm [email protected]

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,16 +69,21 @@ 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_%)
 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_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)