WIP towards #1724

.github/workflows/coq-alpine.yml

@@ -65,9 +65,9 @@ jobs:
         name: generated-files-${{ matrix.alpine }}
         path: generated-files.tgz
       if: ${{ failure() }}
-    - name: package-standalone-ocaml
+    - name: package-standalone-unified-ocaml
       shell: alpine.sh {0}
-      run: make package-standalone-ocaml
+      run: make package-standalone-unified-ocaml
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:
@@ -129,15 +129,18 @@ jobs:
     - name: Test files (host)
       run: |
         cd dist
-        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
-          echo "::group::file $prog"
-          file $prog
-          echo "::endgroup::"
-          echo "::group::ldd $prog"
-          ldd $prog || true
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::ldd fiat_crypto"
+        ldd fiat_crypto || true
+        echo "::endgroup::"
+        echo "::group::fiat_crypto"
+        ./fiat_crypto -h
+        echo "::endgroup::"
+        for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do
           echo "::group::$prog"
-          ./$prog -h
+          ./fiat_crypto $prog -h
           echo "::endgroup::"
         done
     - uses: jirutka/setup-alpine@v1
@@ -148,9 +151,12 @@ jobs:
       shell: alpine.sh {0}
       run: |
         cd dist
-        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+        echo "::group::fiat_crypto"
+        ./fiat_crypto -h
+        echo "::endgroup::"
+        for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do
           echo "::group::$prog"
-          ./$prog -h
+          ./fiat_crypto $prog -h
           echo "::endgroup::"
         done
 
@@ -178,11 +184,11 @@ jobs:
         ( cd dist-edge && tar -xzvf standalone.tar.gz )
         arch="$(etc/ci/find-arch.sh dist-edge/word_by_word_montgomery "unknown")"
         tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Linux_${arch}.tar.gz"
+        fname="Fiat-Cryptography_${tag}_Linux_${arch}"
         echo "$fname"
-        mv dist-edge/standalone.tar.gz "dist/$fname"
+        mv dist-edge/fiat_crypto "dist/$fname"
         find dist
-        tar -tvf "dist/$fname"
+        file "dist/$fname"
     - name: Upload artifacts to GitHub Release
       env:
         GITHUB_TOKEN: ${{ github.token }}

.github/workflows/coq-debian.yml

@@ -57,9 +57,9 @@ jobs:
         name: generated-files-${{ matrix.env.DEBIAN }}
         path: generated-files.tgz
       if: ${{ failure() }}
-    - name: package-standalone-ocaml
+    - name: package-standalone-unified-ocaml
       shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh package-standalone-ocaml
+      run: etc/ci/github-actions-make.sh package-standalone-unified-ocaml
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:

.github/workflows/coq-docker.yml

@@ -68,8 +68,8 @@ jobs:
         name: generated-files-${{ matrix.env.COQ_VERSION }}
         path: generated-files.tgz
       if: ${{ failure() }}
-    - name: package-standalone-ocaml
-      run: etc/ci/github-actions-make.sh -f Makefile.standalone package-standalone-ocaml
+    - name: package-standalone-unified-ocaml
+      run: etc/ci/github-actions-make.sh -f Makefile.standalone package-standalone-unified-ocaml
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:

.github/workflows/coq-macos.yml

@@ -68,7 +68,7 @@ jobs:
     - name: package standalone files
       run: |
         eval $(opam env)
-        etc/ci/github-actions-make.sh package-standalone-ocaml
+        etc/ci/github-actions-make.sh package-standalone-unified-ocaml
 
     - name: only-test-amd64-files-lite
       run: |

.github/workflows/coq-opam-package.yml

@@ -165,7 +165,8 @@ jobs:
       if: ${{ always() && runner.os == 'Windows' }}
 
     - run: opam list
-    - run: opam exec -- word_by_word_montgomery -h
-    - run: opam exec -- unsaturated_solinas -h
-    - run: opam exec -- saturated_solinas -h
-    - run: opam exec -- base_conversion -h
+    - run: opam exec -- fiat_crypto -h
+    - run: opam exec -- fiat_crypto word-by-word-montgomery -h
+    - run: opam exec -- fiat_crypto unsaturated-solinas -h
+    - run: opam exec -- fiat_crypto saturated-solinas -h
+    - run: opam exec -- fiat_crypto base-conversion -h

.github/workflows/coq-windows.yml

@@ -72,9 +72,9 @@ jobs:
       run: |
         %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} standalone-ocaml'
       shell: cmd
-    - name: package-standalone-ocaml
+    - name: package-standalone-unified-ocaml
       run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh package-standalone-ocaml PACKAGE=standalone.zip PACKAGE_CMD=zip'
+        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh package-standalone-unified-ocaml PACKAGE=standalone.zip PACKAGE_CMD=zip'
       shell: cmd
     - name: coq
       run: |

Makefile.config

@@ -50,16 +50,34 @@ else
 if_SKIP_BEDROCK2 = $(1)
 endif
 
-BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction
-BEDROCK2_STANDALONE := $(addprefix bedrock2_,$(BASE_STANDALONE)) $(addprefix with_bedrock2_,$(BASE_STANDALONE))
-STANDALONE := $(BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_STANDALONE) $(WITH_BEDROCK2_STANDALONE))
+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_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))
+STANDALONE := $(UNIFIED_STANDALONE) $(SEPARATE_STANDALONE)
 PERF_STANDALONE := perf_unsaturated_solinas perf_word_by_word_montgomery
 
-STANDALONE_OCAML := $(STANDALONE) $(PERF_STANDALONE)
-STANDALONE_HASKELL := $(STANDALONE)
+UNIFIED_STANDALONE_OCAML := $(UNIFIED_STANDALONE)
+SEPARATE_STANDALONE_OCAML := $(SEPARATE_STANDALONE) $(PERF_STANDALONE)
+STANDALONE_OCAML := $(UNIFIED_STANDALONE_OCAML) $(SEPARATE_STANDALONE_OCAML)
+UNIFIED_STANDALONE_HASKELL := $(UNIFIED_STANDALONE)
+SEPARATE_STANDALONE_HASKELL := $(SEPARATE_STANDALONE)
+STANDALONE_HASKELL := $(UNIFIED_STANDALONE_HASKELL) $(SEPARATE_STANDALONE_HASKELL)
 
-OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/%)
-HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/%)
+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)
 
-WITH_BEDROCK2_OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%)
-WITH_BEDROCK2_HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%)
+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)

Makefile.standalone

@@ -32,10 +32,18 @@ ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true
 
 .PHONY: \
 	perf-standalone \
+	standalone-unified install-standalone-unified install-standalone-unified \
+	standalone-separate install-standalone-separate uninstall-standalone-separate \
 	standalone install-standalone uninstall-standalone \
+	standalone-unified-ocaml install-standalone-unified-ocaml uninstall-standalone-unified-ocaml \
+	standalone-separate-ocaml install-standalone-separate-ocaml uninstall-standalone-separate-ocaml \
 	standalone-ocaml install-standalone-ocaml uninstall-standalone-ocaml \
+	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 \
 	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 \
 	#
 
 # pass -w -20 to disable the unused argument warning
@@ -55,19 +63,33 @@ $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%) : % : %.hs
 	$(HIDE)$(TIMER) $(GHC) $(GHCFLAGS) -o $@ $<
 
 standalone: standalone-haskell standalone-ocaml
+standalone-unified: standalone-unified-haskell standalone-unified-ocaml
+standalone-separate: standalone-separate-haskell standalone-separate-ocaml
 perf-standalone: $(PERF_STANDALONE:%=src/ExtractionOCaml/%)
 
-standalone-ocaml: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%)
-standalone-haskell: $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%)
-
+standalone-ocaml: standalone-unified-ocaml standalone-separate-ocaml
+standalone-unified-ocaml: $(UNIFIED_STANDALONE_OCAML:%=src/ExtractionOCaml/%)
+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
 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)
 
 ifeq ($(SKIP_BEDROCK2),1)
 install-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES)
+install-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES)
+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-ocaml install-standalone-haskell:
+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
@@ -78,9 +100,13 @@ install-standalone-ocaml install-standalone-haskell:
 	done
 else
 install-standalone-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES)
+install-standalone-unified-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES)
+install-standalone-separate-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES)
 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-ocaml install-standalone-haskell:
+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
@@ -94,19 +120,25 @@ install-standalone-ocaml install-standalone-haskell:
 	done
 endif
 
-uninstall-standalone-ocaml uninstall-standalone-haskell:
+uninstall-standalone-ocaml uninstall-standalone-unified-ocaml uninstall-standalone-separate-ocaml uninstall-standalone-haskell uninstall-standalone-unified-haskell uninstall-standalone-separate-haskell:
 	$(HIDE)for f in $(FILESTOINSTALL); do \
 	 instf="$(BINDIR)/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
 	 echo RM "$$instf"; \
 	done
 
 install-standalone: install-standalone-ocaml # install-standalone-haskell
+install-standalone-unified: install-standalone-unified-ocaml # install-standalone-unified-haskell
+install-standalone-separate: install-standalone-separate-ocaml # install-standalone-separate-haskell
 uninstall-standalone: uninstall-standalone-ocaml # uninstall-standalone-haskell
+uninstall-standalone-unified: uninstall-standalone-unified-ocaml # uninstall-standalone-unified-haskell
+uninstall-standalone-separate: uninstall-standalone-separate-ocaml # uninstall-standalone-separate-haskell
 
 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
 
-package-standalone-ocaml package-standalone-haskell : package-standalone-% :
+package-standalone-ocaml package-standalone-unified-ocaml package-standalone-separate-ocaml package-standalone-haskell package-standalone-unified-haskell package-standalone-separate-haskell : package-standalone-% :
 	$(SHOW)'PACKAGE STANDALONE $*'
 	$(HIDE)rm -f "$(PACKAGE)"
 	+$(HIDE)standalonedir="$$(TMPDIR="$$(pwd)" $(MKTEMP_D))"; \