Add wasm_of_ocaml build (#1747)

gzip .wat file because it's too big to deploy otherwise

.github/workflows/coq-docker.yml

@@ -214,11 +214,72 @@ jobs:
         name: fiat-html-js-of-ocaml
         path: fiat-html
 
-  deploy-js-of-ocaml:
-    needs: build-js-of-ocaml
+  build-wasm-of-ocaml:
+    needs: build
     runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        coq-version: [ 'master' ]
+        ocaml-compiler: [ '4.14.1' ]
     concurrency:
-      group: ${{ github.workflow }}-deploy-js-of-ocaml-${{ github.head_ref || github.run_id }}
+      group: ${{ github.workflow }}-build-wasm-of-ocaml-${{ matrix.coq-version }}-${{ matrix.ocaml-compiler }}-${{ github.head_ref || github.run_id }}
+      cancel-in-progress: true
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        submodules: recursive
+    - name: Set up OCaml
+      uses: ocaml/setup-ocaml@v2
+      with:
+        ocaml-compiler: ${{ matrix.ocaml-compiler }}
+    - name: echo build params
+      run: etc/ci/describe-system-config.sh
+    - name: Set up binaryen >= 116
+      uses: acifani/setup-tinygo@v2
+      with:
+        tinygo-version: '0.30.0'
+        binaryen-version: '116'
+    - name: set up custom dune and wasm_of_ocaml
+      run: |
+        eval $(opam env)
+        opam update -y
+        opam pin add -y 'https://github.com/ocaml-wasm/dune.git#wasm'
+        opam pin add -y --no-action --cli=2.1 --with-version 5.3.0 https://github.com/ocaml-wasm/wasm_of_ocaml.git
+    - name: install wasm_of_ocaml
+      run: |
+        eval $(opam env)
+        opam install -y wasm_of_ocaml-compiler ocamlfind
+    - name: echo build params
+      run: etc/ci/describe-system-config.sh
+    - name: Download a Build Artifact
+      uses: actions/download-artifact@v3
+      with:
+        name: ExtractionJsOfOCaml-source-${{ matrix.coq-version }}
+        path: src/ExtractionJsOfOCaml
+    - name: standalone-wasm-of-ocaml
+      run: |
+        eval $(opam env)
+        etc/ci/github-actions-make.sh --warnings -f Makefile.standalone -j2 standalone-wasm-of-ocaml
+    - name: install-standalone-wasm-of-ocaml
+      run: make -f Makefile.standalone install-standalone-wasm-of-ocaml
+    - name: upload wasm_of_ocaml build files
+      uses: actions/upload-artifact@v3
+      with:
+        name: ExtractionJsOfOCaml-${{ matrix.coq-version }}-ocaml-${{ matrix.ocaml-compiler }}+wasm
+        path: src/ExtractionJsOfOCaml
+      if: always ()
+    - name: Upload wasm_of_ocaml outputs
+      uses: actions/upload-artifact@v3
+      with:
+        name: fiat-html-wasm-of-ocaml
+        path: fiat-html
+
+  deploy-js-wasm-of-ocaml:
+    needs: [build-js-of-ocaml, build-wasm-of-ocaml]
+    runs-on: ubuntu-latest
+    concurrency:
+      group: ${{ github.workflow }}-deploy-js-wasm-of-ocaml-${{ github.head_ref || github.run_id }}
       cancel-in-progress: true
     steps:
     - uses: actions/checkout@v4
@@ -231,12 +292,21 @@ jobs:
       with:
         name: fiat-html-js-of-ocaml
         path: fiat-html
+    - run: find fiat-html
+    - run: ls -la fiat-html
+    - name: Download a Build Artifact
+      uses: actions/download-artifact@v3
+      with:
+        name: fiat-html-wasm-of-ocaml
+        path: fiat-html
+    - run: find fiat-html
+    - run: ls -la fiat-html
     - run: make -f Makefile.js-html fiat-html/version.js
     - run: find fiat-html
     - run: ls -la fiat-html
     - name: backup .gitignore
       run: mv .gitignore{,.bak}
-    - name: Deploy js_of_ocaml 🚀 ${{ ( github.ref != 'refs/heads/master' && '(dry run)' ) || '' }}
+    - name: Deploy js_of_ocaml and wasm_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.
@@ -424,7 +494,7 @@ jobs:
 
   docker-check-all:
     runs-on: ubuntu-latest
-    needs: [build, validate, build-js-of-ocaml, deploy-js-of-ocaml, generated-files, standalone-haskell, test-amd64, test-standalone, publish-standalone-dry-run]
+    needs: [build, validate, build-js-of-ocaml, build-wasm-of-ocaml, deploy-js-wasm-of-ocaml, generated-files, standalone-haskell, test-amd64, test-standalone, publish-standalone-dry-run]
     if: always()
     steps:
     - run: echo 'build passed'
@@ -433,8 +503,10 @@ jobs:
       if: ${{ needs.validate.result == 'success' }}
     - run: echo 'build-js-of-ocaml passed'
       if: ${{ needs.build-js-of-ocaml.result == 'success' }}
-    - run: echo 'deploy-js-of-ocaml passed'
-      if: ${{ needs.deploy-js-of-ocaml.result == 'success' }}
+    - run: echo 'build-wasm-of-ocaml passed'
+      if: ${{ needs.build-wasm-of-ocaml.result == 'success' }}
+    - run: echo 'deploy-js-wasm-of-ocaml passed'
+      if: ${{ needs.deploy-js-wasm-of-ocaml.result == 'success' }}
     - run: echo 'generated-files passed'
       if: ${{ needs.generated-files.result == 'success' }}
     - run: echo 'standalone-haskell passed'
@@ -451,8 +523,10 @@ jobs:
       if: ${{ needs.validate.result != 'success' }}
     - run: echo 'build-js-of-ocaml failed' && false
       if: ${{ needs.build-js-of-ocaml.result != 'success' }}
-    - run: echo 'deploy-js-of-ocaml failed' && false
-      if: ${{ needs.deploy-js-of-ocaml.result != 'success' }}
+    - run: echo 'build-wasm-of-ocaml failed' && false
+      if: ${{ needs.build-wasm-of-ocaml.result != 'success' }}
+    - run: echo 'deploy-js-wasm-of-ocaml failed' && false
+      if: ${{ needs.deploy-js-wasm-of-ocaml.result != 'success' }}
     - run: echo 'generated-files failed' && false
       if: ${{ needs.generated-files.result != 'success' }}
     - run: echo 'standalone-haskell failed' && false

.gitignore

@@ -208,6 +208,9 @@ src/ExtractionJsOfOCaml/*.ml
 src/ExtractionJsOfOCaml/*.mli
 src/ExtractionJsOfOCaml/*.js
 src/ExtractionJsOfOCaml/*.map
+src/ExtractionJsOfOCaml/*.wasm
+src/ExtractionJsOfOCaml/*.wat
+src/ExtractionJsOfOCaml/*.wat.gz
 src/Rewriter/PerfTesting/Specific/generated/*.v
 src/Rewriter/PerfTesting/Specific/generated/*.log
 src/Rewriter/PerfTesting/Specific/generated/*.sh
@@ -222,6 +225,10 @@ 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/version.js
 /Makefile.test-amd64-files.mk
 

Makefile.config

@@ -71,6 +71,8 @@ STANDALONE_HASKELL := $(UNIFIED_STANDALONE_HASKELL) $(SEPARATE_STANDALONE_HASKEL
 
 STANDALONE_JS_OF_OCAML := $(UNIFIED_STANDALONE)
 BEDROCK2_STANDALONE_JS_OF_OCAML := $(BEDROCK2_UNIFIED_STANDALONE)
+STANDALONE_WASM_OF_OCAML := $(UNIFIED_STANDALONE)
+BEDROCK2_STANDALONE_WASM_OF_OCAML := $(BEDROCK2_UNIFIED_STANDALONE)
 
 UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/%)
 SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/%)
@@ -79,6 +81,9 @@ 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)
+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)
 
 WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%)
 WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%)
@@ -87,3 +92,6 @@ WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/Extrac
 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)
+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)

Makefile.standalone

@@ -23,15 +23,20 @@ CAMLOPT_PERF_SHOW:=OCAMLOPTP
 endif
 CAMLEXTRAFLAGS ?=
 JS_OF_OCAML ?= js_of_ocaml
+WASM_OF_OCAML ?= wasm_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 --enable=effects $(JS_OF_OCAML_EXTRAFLAGS)
+WASM_OF_OCAML_EXTRAFLAGS ?=
+WASM_OF_OCAML_FLAGS ?= --source-map --no-inline $(WASM_OF_OCAML_EXTRAFLAGS)
 
 PACKAGE ?= standalone.tar.gz
 PACKAGE_CMD ?= tar -czvf
 PACKAGE_CMD_FUNC ?= $(PACKAGE_CMD) $(1) $(2)
 MKTEMP_D ?= etc/ci/mktemp_d.sh
+GZIP ?= gzip
+GZIP_KEEP_FLAGS ?= -k
 
 ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true
 
@@ -47,6 +52,7 @@ ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true
 	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 \
+	standalone-wasm-of-ocaml install-standalone-wasm-of-ocaml uninstall-standalone-wasm-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 \
@@ -79,6 +85,15 @@ $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.js) : %.js : %.byte
 	$(HIDE)$(ENSURE_STACK_LIMIT); \
 	 $(TIMER) $(JS_OF_OCAML) $(JS_OF_OCAML_FLAGS) $<
 
+$(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.wasm) : %.wasm : %.byte
+	$(SHOW)'WASM_OF_OCAML $<'
+	$(HIDE)$(ENSURE_STACK_LIMIT); \
+	 $(TIMER) $(WASM_OF_OCAML) $(WASM_OF_OCAML_FLAGS) $<
+
+$(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.wat.gz) : %.wat.gz : %.wasm
+	$(SHOW)'GZIP $*'
+	$(HIDE)$(TIMER) $(GZIP) $(GZIP_KEEP_FLAGS) $*.wat
+
 $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%) : % : %.hs
 	$(SHOW)'GHC $< -o $@'
 	$(HIDE)$(TIMER) $(GHC) $(GHCFLAGS) -o $@ $<
@@ -95,6 +110,7 @@ standalone-haskell: standalone-unified-haskell standalone-separate-haskell
 standalone-unified-haskell: $(UNIFIED_STANDALONE_HASKELL:%=src/ExtractionHaskell/%)
 standalone-separate-haskell: $(SEPARATE_STANDALONE_HASKELL:%=src/ExtractionHaskell/%)
 standalone-js-of-ocaml: $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.js)
+standalone-wasm-of-ocaml: $(STANDALONE_WASM_OF_OCAML:%=src/ExtractionJsOfOCaml/%.wasm) $(STANDALONE_WASM_OF_OCAML:%=src/ExtractionJsOfOCaml/%.wat.gz)
 
 uninstall-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
 uninstall-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
@@ -103,11 +119,13 @@ 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)
+uninstall-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: PERMS=0755
-install-standalone-js-of-ocaml: PERMS=0644
+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)
 
 
 
@@ -119,8 +137,9 @@ 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-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-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
@@ -137,6 +156,8 @@ 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-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\
@@ -164,9 +185,31 @@ install-standalone-js-of-ocaml:
 	   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";\
+	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-js-of-ocaml:
+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 \
 	 instf="$(INSTALLDIR)/`basename $$f`" &&\
 	 rm -f "$$instf" &&\

etc/ci/describe-system-config.sh

@@ -41,6 +41,7 @@ group opam switch
 group opam list
 group ocamlc -config
 group js_of_ocaml --version
+group wasm_of_ocaml --version
 group coqc --config
 group coqc --version
 group "true | coqtop"

fiat-html/wasm_fiat_crypto_worker.js

@@ -0,0 +1,9 @@
+self.importScripts("wasm_fiat_crypto.js");
+self.onmessage = function(e) {
+    try {
+        const result = synthesize(e.data);
+        postMessage({result: result});
+    } catch (err) {
+        postMessage({error: err});
+    }
+};