diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml
index e38f1d3540f..d4842335813 100644
--- a/.github/workflows/coq-alpine.yml
+++ b/.github/workflows/coq-alpine.yml
@@ -65,14 +65,14 @@ jobs:
         name: generated-files-${{ matrix.alpine }}
         path: generated-files.tgz
       if: ${{ failure() }}
-    - name: package-standalone-ocaml
+    - name: install-standalone-unified-ocaml
       shell: alpine.sh {0}
-      run: make package-standalone-ocaml
+      run: make install-standalone-unified-ocaml BINDIR=dist
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:
         name: standalone-${{ matrix.alpine }}
-        path: standalone.tar.gz
+        path: dist/fiat_crypto
     - name: upload OCaml files
       uses: actions/upload-artifact@v3
       with:
@@ -112,32 +112,25 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-${{ matrix.alpine }}
-        path: dist-${{ matrix.alpine }}/
+        path: dist/
     - name: List files
-      run: find dist-edge
-    - name: Rename files
-      run: |
-        mkdir dist
-        mv dist-${{ matrix.alpine }}/standalone.tar.gz dist/fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
-        find dist
-        tar -tvf dist/fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
-    - name: Unpack files
-      run: |
-        cd dist
-        tar -xzvf fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
-        ls -la .
+      run: find dist
+    - run: chmod +x dist/fiat_crypto
     - 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 +141,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
 
@@ -168,21 +164,19 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-edge
-        path: dist-edge/
+        path: dist/
     - name: List files
-      run: find dist-edge
+      run: find dist
     - name: Unpack files
       run: |
-        mkdir dist
         echo "::group::find arch"
-        ( cd dist-edge && tar -xzvf standalone.tar.gz )
-        arch="$(etc/ci/find-arch.sh dist-edge/word_by_word_montgomery "unknown")"
+        arch="$(etc/ci/find-arch.sh dist/fiat_crypto "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/fiat_crypto "dist/$fname"
         find dist
-        tar -tvf "dist/$fname"
+        file "dist/$fname"
     - name: Upload artifacts to GitHub Release
       env:
         GITHUB_TOKEN: ${{ github.token }}
diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
index 7fb9976e99f..59e8f442a37 100644
--- a/.github/workflows/coq-debian.yml
+++ b/.github/workflows/coq-debian.yml
@@ -57,14 +57,14 @@ jobs:
         name: generated-files-${{ matrix.env.DEBIAN }}
         path: generated-files.tgz
       if: ${{ failure() }}
-    - name: package-standalone-ocaml
+    - name: install-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 install-standalone-unified-ocaml BINDIR=dist
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:
         name: standalone-${{ matrix.env.DEBIAN }}
-        path: standalone.tar.gz
+        path: dist/fiat_crypto
     - name: upload OCaml files
       uses: actions/upload-artifact@v3
       with:
@@ -103,32 +103,24 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-${{ matrix.debian }}
-        path: dist-${{ matrix.debian }}/
+        path: dist/
     - name: List files
-      run: find dist-${{ matrix.debian }}
-    - name: Rename files
-      run: |
-        mkdir dist
-        mv dist-${{ matrix.debian }}/standalone.tar.gz dist/fiat-crypto-${{ matrix.debian }}.tar.gz
-        find dist
-        tar -tvf dist/fiat-crypto-${{ matrix.debian }}.tar.gz
-    - name: Unpack Files
-      run: |
-        cd dist
-        tar -xzvf fiat-crypto-${{ matrix.debian }}.tar.gz
-        ls -la .
+      run: find dist
     - 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
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::ldd fiat_crypto"
+        ldd fiat_crypto
+        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
     - name: setup Debian chroot
@@ -137,15 +129,18 @@ jobs:
       shell: in-debian-chroot.sh {0}
       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
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::ldd fiat_crypto"
+        ldd fiat_crypto
+        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
 
@@ -163,21 +158,20 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-sid
-        path: dist-sid/
+        path: dist/
     - name: List files
-      run: find dist-sid
+      run: find dist
+    - run: chmod +x dist/fiat_crypto
     - name: Unpack files
       run: |
         mkdir dist
         echo "::group::find arch"
-        ( cd dist-sid && tar -xzvf standalone.tar.gz )
-        arch="$(etc/ci/find-arch.sh dist-sid/word_by_word_montgomery "unknown")"
+        arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")"
         tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}.tar.gz"
+        fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}"
         echo "$fname"
-        mv dist-sid/standalone.tar.gz "dist/$fname"
+        mv dist/fiat_crypto "dist/$fname"
         find dist
-        tar -tvf "dist/$fname"
 #    - name: Upload artifacts to GitHub Release
 #      env:
 #        GITHUB_TOKEN: ${{ github.token }}
diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml
index 735e23f8986..1471c96f26b 100644
--- a/.github/workflows/coq-docker.yml
+++ b/.github/workflows/coq-docker.yml
@@ -68,13 +68,13 @@ 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: install-standalone-unified-ocaml
+      run: make -f Makefile.standalone install-standalone-unified-ocaml BINDIR=dist
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:
         name: standalone-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}
-        path: standalone.tar.gz
+        path: dist/fiat_crypto
     - name: upload OCaml files
       uses: actions/upload-artifact@v3
       with:
@@ -151,32 +151,25 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-docker-coq-${{ matrix.docker-coq-version }}
-        path: dist-docker-coq-${{ matrix.docker-coq-version }}/
+        path: dist/
     - name: List files
-      run: find dist-docker-coq-${{ matrix.docker-coq-version }}
-    - name: Rename files
-      run: |
-        mkdir dist
-        mv dist-docker-coq-${{ matrix.docker-coq-version }}/standalone.tar.gz dist/fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
-        find dist
-        tar -tvf dist/fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
-    - name: Unpack Files
-      run: |
-        cd dist
-        tar -xzvf fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
-        ls -la .
+      run: find dist
+    - run: chmod +x dist/fiat_crypto
     - 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
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::ldd fiat_crypto"
+        ldd fiat_crypto
+        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
     - name: Test files (container)
@@ -190,15 +183,18 @@ jobs:
           sudo apt-get install -y file
           echo "::endgroup::"
           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
-            echo "::endgroup::"
+          echo "::group::file fiat_crypto"
+          file fiat_crypto
+          echo "::endgroup::"
+          echo "::group::ldd fiat_crypto"
+          ldd fiat_crypto
+          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
 
@@ -216,21 +212,18 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-docker-coq-dev
-        path: dist-docker-coq-dev/
+        path: dist/
     - name: List files
-      run: find dist-docker-coq-dev
+      run: find dist
     - name: Unpack files
       run: |
-        mkdir dist
         echo "::group::find arch"
-        ( cd dist-docker-coq-dev && tar -xzvf standalone.tar.gz )
-        arch="$(etc/ci/find-arch.sh dist-docker-coq-dev/word_by_word_montgomery "unknown")"
+        arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")"
         tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}.tar.gz"
+        fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}"
         echo "$fname"
-        mv dist-docker-coq-dev/standalone.tar.gz "dist/$fname"
+        mv dist/fiat_crypto "dist/$fname"
         find dist
-        tar -tvf "dist/$fname"
 #    - name: Upload artifacts to GitHub Release
 #      env:
 #        GITHUB_TOKEN: ${{ github.token }}
diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml
index 51ea39d7f30..eede0748906 100644
--- a/.github/workflows/coq-macos.yml
+++ b/.github/workflows/coq-macos.yml
@@ -65,10 +65,10 @@ jobs:
         eval $(opam env)
         etc/ci/github-actions-make.sh -j2 all
 
-    - name: package standalone files
+    - name: install-standalone-unified-ocaml
       run: |
         eval $(opam env)
-        etc/ci/github-actions-make.sh package-standalone-ocaml
+        etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist
 
     - name: only-test-amd64-files-lite
       run: |
@@ -84,7 +84,7 @@ jobs:
       uses: actions/upload-artifact@v3
       with:
         name: standalone-macos
-        path: standalone.tar.gz
+        path: dist/fiat_crypto
     - name: display timing info
       run: cat time-of-build-pretty.log
     - name: display per-line timing info
@@ -110,35 +110,28 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-macos
-        path: dist-macos/
+        path: dist/
     - name: List files
-      run: find dist-macos
-    - name: Rename files
-      run: |
-        mkdir dist
-        mv dist-macos/standalone.tar.gz dist/fiat-crypto-macos.tar.gz
-        find dist
-        tar -tvf dist/fiat-crypto-macos.tar.gz
-    - name: Unpack Files
-      run: |
-        cd dist
-        tar -xzvf fiat-crypto-macos.tar.gz
-        ls -la .
+      run: find dist
+    - run: chmod +x dist/fiat_crypto
     - name: Test files
       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::otool -L $prog"
-          otool -L $prog
-          echo "::endgroup::"
-          echo "::group::lipo -info $prog"
-          lipo -info $prog
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::otool -L fiat_crypto"
+        otool -L fiat_crypto
+        echo "::endgroup::"
+        echo "::group::lipo -info fiat_crypto"
+        lipo -info fiat_crypto
+        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
 
@@ -156,20 +149,18 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-macos
-        path: dist-macos/
+        path: dist/
     - name: List files
       run: find dist-macos
     - name: Unpack files
       run: |
         mkdir dist
-        ( cd dist-macos && tar -xzvf standalone.tar.gz )
-        arch="$(etc/ci/find-arch.sh dist-macos/word_by_word_montgomery)"
+        arch="$(etc/ci/find-arch.sh dist/fiat_crypto)"
         tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_macOS_${arch}.tar.gz"
+        fname="Fiat-Cryptography_${tag}_macOS_${arch}"
         echo "$fname"
-        mv dist-macos/standalone.tar.gz "dist/$fname"
+        mv dist/fiat_crypto "dist/$fname"
         find dist
-        tar -tvf "dist/$fname"
     - name: Upload artifacts to GitHub Release
       env:
         GITHUB_TOKEN: ${{ github.token }}
diff --git a/.github/workflows/coq-opam-package.yml b/.github/workflows/coq-opam-package.yml
index 3e756250311..0f9df7e6b66 100644
--- a/.github/workflows/coq-opam-package.yml
+++ b/.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
diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml
index de811eabae4..6f3bc4a18fd 100644
--- a/.github/workflows/coq-windows.yml
+++ b/.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: install-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 install-standalone-unified-ocaml BINDIR=dist'
       shell: cmd
     - name: coq
       run: |
@@ -101,7 +101,7 @@ jobs:
       uses: actions/upload-artifact@v3
       with:
         name: standalone-windows
-        path: standalone.zip
+        path: dist/fiat_crypto.exe
     - name: display timing info
       run: type time-of-build-pretty.log
       shell: cmd
@@ -130,43 +130,26 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-windows
-        path: dist-windows/
+        path: dist/
     - name: List files
-      run: Get-ChildItem dist-windows -Name
-    - name: Rename files
-      run: |
-        New-Item -ItemType Directory -Path dist
-        Move-Item dist-windows/standalone.zip dist/fiat-crypto-windows.zip
-        Get-ChildItem dist -Name
-    - name: Unpack files
-      run: |
-        Expand-Archive -Path dist/fiat-crypto-windows.zip -DestinationPath dist
-        Get-ChildItem dist
-    - run: .\dist\word_by_word_montgomery.exe -h
-    - run: .\dist\unsaturated_solinas.exe -h
-    - run: .\dist\saturated_solinas.exe -h
-    - run: .\dist\base_conversion.exe -h
+      run: Get-ChildItem dist -Name
+    - run: .\dist\fiat_crypto.exe  -h
+    - run: .\dist\fiat_crypto.exe word-by-word-montgomery -h
+    - run: .\dist\fiat_crypto.exe unsaturated-solinas -h
+    - run: .\dist\fiat_crypto.exe saturated-solinas -h
+    - run: .\dist\fiat_crypto.exe base-conversion -h
     - name: Set up MSVC Environment for dumpbin
       uses: ilammy/msvc-dev-cmd@v1
     - name: Check Executable Dependencies
       run: |
-        $executables = @(
-          ".\dist\word_by_word_montgomery.exe",
-          ".\dist\unsaturated_solinas.exe",
-          ".\dist\saturated_solinas.exe",
-          ".\dist\base_conversion.exe"
-        )
-
-        foreach ($prog in $executables) {
-          Write-Host "::group::File Info - $prog"
-          Get-Item $prog | Format-List
-          dumpbin.exe /headers $prog
-          Write-Host "::endgroup::"
+        Write-Host "::group::File Info - fiat_crypto"
+        Get-Item .\dist\fiat_crypto.exe | Format-List
+        dumpbin.exe /headers .\dist\fiat_crypto.exe
+        Write-Host "::endgroup::"
 
-          Write-Host "::group::DLL Dependencies - $prog"
-          dumpbin.exe /dependents $prog
-          Write-Host "::endgroup::"
-        }
+        Write-Host "::group::DLL Dependencies - fiat_crypto"
+        dumpbin.exe /dependents .\dist\fiat_crypto.exe
+        Write-Host "::endgroup::"
 
   publish-standalone:
     runs-on: ubuntu-latest
@@ -182,20 +165,17 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-windows
-        path: dist-windows/
+        path: dist/
     - name: List files
-      run: find dist-windows
+      run: find dist
     - name: Unpack files
       run: |
-        mkdir dist
-        ( cd dist-windows && unzip standalone.zip )
-        arch="$(etc/ci/find-arch.sh dist-windows/word_by_word_montgomery "x86_64")"
+        arch="$(etc/ci/find-arch.sh dist/fiat_crypto.exe "x86_64")"
         tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Windows_${arch}.zip"
+        fname="Fiat-Cryptography_${tag}_Windows_${arch}.exe"
         echo "$fname"
-        mv dist-windows/standalone.zip "dist/$fname"
+        mv dist/fiat_crypto.exe "dist/$fname"
         find dist
-        unzip -l "dist/$fname"
     - name: Upload artifacts to GitHub Release
       env:
         GITHUB_TOKEN: ${{ github.token }}
diff --git a/Makefile.config b/Makefile.config
index c559c61740e..afed0c3954a 100644
--- a/Makefile.config
+++ b/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)
diff --git a/Makefile.standalone b/Makefile.standalone
index 2175966a598..a5f2fcd754a 100644
--- a/Makefile.standalone
+++ b/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,7 +120,7 @@ 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" &&\
@@ -102,11 +128,17 @@ uninstall-standalone-ocaml uninstall-standalone-haskell:
 	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))"; \
diff --git a/README.md b/README.md
index 2b49c30652b..3fc5b28980a 100644
--- a/README.md
+++ b/README.md
@@ -52,9 +52,9 @@ Then run:
 
 You can check out [our CI](https://github.com/mit-plv/fiat-crypto/actions?query=branch%3Amaster+workflow%3A%22CI+%28Coq%29%22) to see how long the build should take; as of the last update to this line in the README, it takes about 1h10m to run `make -j2` on Coq 8.11.1.
 
-If you want to build only the command-line binaries used for generating code, you can save a bit of time by making only the `standalone-ocaml` target with
+If you want to build only the command-line binaries used for generating code, you can save a bit of time by making only the `standalone-unified-ocaml` target with
 
-    make standalone-ocaml
+    make standalone-unified-ocaml
 
 Usage (Generating C Files)
 --------------------------
@@ -76,29 +76,36 @@ Just the compilers generating these C files can be made with
 or `make standalone-haskell` for compiler binaries generated with Haskell, or `make standalone` for both the Haskell and OCaml compiler binaries.
 The binaries are located in `src/ExtractionOcaml/` and `src/ExtractionHaskell/` respectively.
 
-There is a separate compiler binary for each implementation strategy:
+There is one compiler binary for all implementation strategies:
+
+ - `fiat_crypto`
+
+This binary takes arguments for the strategy:
 
- - `saturated_solinas`
- - `unsaturated_solinas`
- - `word_by_word_montgomery`
+ - `saturated-solinas`
+ - `unsaturated-solinas`
+ - `word-by-word-montgomery`
+ - `dettman-multiplication`
+ - `solinas-reduction`
+ - `base-conversion`
 
 Passing no arguments, or passing `-h` or `--help` (or any other invalid arguments) will result in a usage message being printed.  These binaries output C code on stdout.
 
 Here are some examples of ways to invoke the binaries (from the directories that they live in):
 
     # Generate code for 2^255-19
-    ./unsaturated_solinas '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c
-    ./unsaturated_solinas '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c
+    ./fiat_crypto unsaturated-solinas '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c
+    ./fiat_crypto unsaturated-solinas '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c
 
     # Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1)
-    ./word_by_word_montgomery 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c
-    ./word_by_word_montgomery 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c
+    ./fiat_crypto word-by-word-montgomery 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c
+    ./fiat_crypto word-by-word-montgomery 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c
 
 You can find more examples in the [`Makefile`](./Makefile).
 
 Note that for large primes, you may need to increase the stack size to avoid stack overflows.  For example:
 
-    ulimit -S -s 1048576; ./word_by_word_montgomery --static gost_512_paramSetB 32 '2^511 + 111'
+    ulimit -S -s 1048576; ./fiat_crypto word-by-word-montgomery --static gost_512_paramSetB 32 '2^511 + 111'
 
 This sets the stack size to 1 GB (= 1024 MB = 1024 * 1024 KB = 1048576 KB) before running the command.
 As of the last edit of this line, this command takes about an hour to run, but does in fact complete successfully.
@@ -124,27 +131,34 @@ Just the compilers generating these bedrock2/C files can be made with
 or `make standalone-haskell` for binaries generated with Haskell, or `make standalone` for both the Haskell and OCaml binaries.
 The binaries are located in `src/ExtractionOcaml/` and `src/ExtractionHaskell/` respectively.
 
-There is a separate compiler binary for each implementation strategy:
+There is one compiler binary for all implementation strategies:
+
+ - `bedrock2_fiat_crypto`
+
+This binary takes arguments for the strategy:
 
- - `bedrock2_saturated_solinas`
- - `bedrock2_unsaturated_solinas`
- - `bedrock2_word_by_word_montgomery`
+ - `saturated-solinas`
+ - `unsaturated-solinas`
+ - `word-by-word-montgomery`
+ - `dettman-multiplication`
+ - `solinas-reduction`
+ - `base-conversion`
 
 Passing no arguments, or passing `-h` or `--help` (or any other invalid arguments) will result in a usage message being printed.  These binaries output bedrock2/C code on stdout.
 
 Here are some examples of ways to invoke the binaries (from the directories that they live in):
 
     # Generate code for 2^255-19
-    ./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c
-    ./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c
+    ./bedrock2_fiat_crypto unsaturated-solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c
+    ./bedrock2_fiat_crypto unsaturated-solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c
 
     # Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1)
-    ./bedrock2_word_by_word_montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c
-    ./bedrock2_word_by_word_montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c
+    ./bedrock2_fiat_crypto word-by-word-montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c
+    ./bedrock2_fiat_crypto word-by-word-montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c
 
     # Generate code for 2^130 - 5
-    ./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '64' '3' '2^130 - 5' > poly1305_64.c
-    ./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '32' '5' '2^130 - 5' > poly1305_32.c
+    ./bedrock2_fiat_crypto unsaturated-solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '64' '3' '2^130 - 5' > poly1305_64.c
+    ./bedrock2_fiat_crypto unsaturated-solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '32' '5' '2^130 - 5' > poly1305_32.c
 
 You can find more examples in [`Makefile.examples`](./Makefile.examples).
 
diff --git a/src/CLI.v b/src/CLI.v
index 36cbd05930e..2e9d71f955e 100644
--- a/src/CLI.v
+++ b/src/CLI.v
@@ -17,6 +17,7 @@ Require Import Crypto.Util.Strings.NamingConventions.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.OptionList.
 Require Import Crypto.Util.Strings.Show.
+Require Import Crypto.Util.Strings.Show.Enum.
 Require Import Crypto.Util.Strings.Sorting.
 Require Import Crypto.Util.Strings.ParseFlagOptions.
 Require Import Crypto.Util.DebugMonad.
@@ -44,6 +45,32 @@ Import
   Stringification.C.Compilers.
 
 Module ForExtraction.
+  Variant SynthesisKind : Set :=
+    | word_by_word_montgomery
+    | unsaturated_solinas
+    | saturated_solinas
+    | dettman_multiplication
+    | solinas_reduction
+    | base_conversion
+  .
+
+  Derive SynthesisKind_Listable SuchThat (@FinitelyListable SynthesisKind SynthesisKind_Listable) As SynthesisKind_FinitelyListable.
+  Proof. prove_ListableDerive. Qed.
+  Global Existing Instances SynthesisKind_Listable SynthesisKind_FinitelyListable.
+
+  Global Instance show_SynthesisKind : Show SynthesisKind.
+  Proof. prove_Show_enum (). Defined.
+  Global Instance show_lvl_SynthesisKind : ShowLevel SynthesisKind := show_SynthesisKind.
+
+  Definition parse_SynthesisKind_list : list (string * SynthesisKind)
+    := Eval vm_compute in
+      List.map
+        (fun r => (String.replace "_" "-" (show r), r))
+        (list_all SynthesisKind).
+
+  Definition parse_SynthesisKind_act : ParserAction SynthesisKind
+    := parse_strs parse_SynthesisKind_list.
+
   Definition parse_string_and {T} (parse_T : string -> option T) (s : string) : option (string * T)
     := option_map (@pair _ _ s) (parse_T s).
   Definition parse_Z (s : string) : option Z := parseZ_arith_strict s.
@@ -62,6 +89,9 @@ Module ForExtraction.
           ls <-- List.map ParseArithmetic.Q_to_Z_strict ls;
           Some ls).
 
+  Definition parse_SynthesisKind (s : string) : option SynthesisKind
+    := finalize parse_SynthesisKind_act s.
+
   Definition parse_list_REG (s : string) : option (list REG)
     := finalize (parse_comma_list parse_REG) s.
 
@@ -77,9 +107,6 @@ Module ForExtraction.
   Definition parse_callee_saved_registers (s : string) : option assembly_callee_saved_registers_opt
     := finalize parse_assembly_callee_saved_registers_opt s.
 
-  (* Workaround for lack of notation in 8.8 *)
-  Local Notation "x =? y" := (if string_dec x y then true else false) : string_scope.
-
   Definition parse_n (n : string) : option MaybeLimbCount
     := match parse_nat n with
        | Some n => Some (NumLimbs n)
@@ -301,6 +328,10 @@ Module ForExtraction.
                     end)%string
                 special_options)).
 
+  Definition synthesis_kind_spec : anon_argT
+    := ("synthesis_kind",
+         Arg.CustomSymbol parse_SynthesisKind_list,
+         ["The algorithm for field arithmetic.  Further options depend on the choice of algorithm, and can be viewed by passing -h after this argument.  Note that no options other than -h are permitted before this argument."]).
   Definition curve_description_spec : anon_argT
     := ("curve_description",
         Arg.String,
@@ -1003,6 +1034,7 @@ Module ForExtraction.
            end.
 
       Definition PipelineMain
+                 {prog_name_count : Arg.prog_name_countT}
                  {supported_languages : supported_languagesT}
                  {A}
                  {io_driver : IODriverAPI A}
@@ -1105,6 +1137,7 @@ Module ForExtraction.
         }.
 
     Definition PipelineMain
+               {prog_name_count : Arg.prog_name_countT}
                {supported_languages : supported_languagesT}
                {A}
                {io_driver : IODriverAPI A}
@@ -1147,6 +1180,7 @@ Module ForExtraction.
         }.
 
     Definition PipelineMain
+               {prog_name_count : Arg.prog_name_countT}
                {supported_languages : supported_languagesT}
                {A}
                {io_driver : IODriverAPI A}
@@ -1182,6 +1216,7 @@ Module ForExtraction.
         }.
 
     Definition PipelineMain
+               {prog_name_count : Arg.prog_name_countT}
                {supported_languages : supported_languagesT}
                {A}
                {io_driver : IODriverAPI A}
@@ -1228,6 +1263,7 @@ Module ForExtraction.
         }.
 
     Definition PipelineMain
+               {prog_name_count : Arg.prog_name_countT}
                {supported_languages : supported_languagesT}
                {A}
                {io_driver : IODriverAPI A}
@@ -1263,6 +1299,7 @@ Module ForExtraction.
       }.
 
     Definition PipelineMain
+               {prog_name_count : Arg.prog_name_countT}
                {supported_languages : supported_languagesT}
                {A}
                {io_driver : IODriverAPI A}
@@ -1331,6 +1368,7 @@ Module ForExtraction.
         }.
 
     Definition PipelineMain
+               {prog_name_count : Arg.prog_name_countT}
                {supported_languages : supported_languagesT}
                {A}
                {io_driver : IODriverAPI A}
@@ -1338,4 +1376,46 @@ Module ForExtraction.
       : A
       := Parameterized.PipelineMain argv.
   End BaseConversion.
+
+  (** The combined binary that delegates *)
+  Module FiatCrypto.
+    Definition PipelineMain
+      {supported_languages : supported_languagesT}
+      {A}
+      {io_driver : IODriverAPI A}
+      (argv : list string)
+      : A
+      := let spec
+           := {| Arg.named_args := []
+              ; Arg.anon_args := [synthesis_kind_spec]
+              ; Arg.anon_opt_args := []
+              ; Arg.anon_opt_repeated_arg := None |} in
+         match Arg.parse_argv (List.firstn 2 argv) spec with
+         | ErrorT.Success (tt as _named_data, anon_data, tt as _anon_opt_data, tt as _anon_opt_repeated_data)
+           => let synthesis_kind := anon_data in
+              let prog_name_count : Arg.prog_name_countT := 2%nat in
+              match synthesis_kind with
+              | word_by_word_montgomery
+                => WordByWordMontgomery.PipelineMain (prog_name_count:=prog_name_count) argv
+              | unsaturated_solinas
+                => UnsaturatedSolinas.PipelineMain (prog_name_count:=prog_name_count) argv
+              | saturated_solinas
+                => SaturatedSolinas.PipelineMain (prog_name_count:=prog_name_count) argv
+              | dettman_multiplication
+                => DettmanMultiplication.PipelineMain (prog_name_count:=prog_name_count) argv
+              | solinas_reduction
+                => SolinasReduction.PipelineMain (prog_name_count:=prog_name_count) argv
+              | base_conversion
+                => BaseConversion.PipelineMain (prog_name_count:=prog_name_count) argv
+              end
+         | ErrorT.Error err
+           => let display := Arg.show_list_parse_error spec err in
+              if Arg.is_real_error err
+              then error display
+              else (* just a requested help/usage message *)
+                write_stdout_then
+                  (List.map (fun s => s ++ String.NewLine)%string display)
+                  ret
+         end.
+  End FiatCrypto.
 End ForExtraction.
diff --git a/src/ExtractionHaskell/bedrock2_fiat_crypto.v b/src/ExtractionHaskell/bedrock2_fiat_crypto.v
new file mode 100644
index 00000000000..509dd3ced04
--- /dev/null
+++ b/src/ExtractionHaskell/bedrock2_fiat_crypto.v
@@ -0,0 +1,5 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2First.
+
+(*Redirect "/tmp/bedrock2_fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main.
+(* cat /tmp/bedrock2_fiat_crypto.hs.out | sed -f haskell.sed  > ../../bedrock2_fiat_crypto.hs *)
diff --git a/src/ExtractionHaskell/fiat_crypto.v b/src/ExtractionHaskell/fiat_crypto.v
new file mode 100644
index 00000000000..89a96038958
--- /dev/null
+++ b/src/ExtractionHaskell/fiat_crypto.v
@@ -0,0 +1,4 @@
+Require Import Crypto.StandaloneHaskellMain.
+
+(*Redirect "/tmp/fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main.
+(* cat /tmp/fiat_crypto.hs.out | sed -f haskell.sed  > ../../fiat_crypto.hs *)
diff --git a/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v b/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v
new file mode 100644
index 00000000000..2b175121a05
--- /dev/null
+++ b/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v
@@ -0,0 +1,5 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main.
+(* cat /tmp/bedrock2_fiat_crypto.hs.out | sed -f haskell.sed  > ../../bedrock2_fiat_crypto.hs *)
diff --git a/src/ExtractionOCaml/bedrock2_fiat_crypto.v b/src/ExtractionOCaml/bedrock2_fiat_crypto.v
new file mode 100644
index 00000000000..a2b85f8dc8c
--- /dev/null
+++ b/src/ExtractionOCaml/bedrock2_fiat_crypto.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2First.
+
+Extraction "src/ExtractionOCaml/bedrock2_fiat_crypto.tmp" FiatCrypto.main.
diff --git a/src/ExtractionOCaml/fiat_crypto.v b/src/ExtractionOCaml/fiat_crypto.v
new file mode 100644
index 00000000000..fcd64cad02f
--- /dev/null
+++ b/src/ExtractionOCaml/fiat_crypto.v
@@ -0,0 +1,3 @@
+Require Import Crypto.StandaloneOCamlMain.
+
+Extraction "src/ExtractionOCaml/fiat_crypto.tmp" FiatCrypto.main.
diff --git a/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v b/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v
new file mode 100644
index 00000000000..70b1716025e
--- /dev/null
+++ b/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+Extraction "src/ExtractionOCaml/with_bedrock2_fiat_crypto.tmp" FiatCrypto.main.
diff --git a/src/StandaloneHaskellMain.v b/src/StandaloneHaskellMain.v
index b6e2923a96f..ac897510e81 100644
--- a/src/StandaloneHaskellMain.v
+++ b/src/StandaloneHaskellMain.v
@@ -144,3 +144,8 @@ Module BaseConversion.
   Definition main : IO_unit
     := main_gen ForExtraction.BaseConversion.PipelineMain.
 End BaseConversion.
+
+Module FiatCrypto.
+  Definition main : IO_unit
+    := main_gen ForExtraction.FiatCrypto.PipelineMain.
+End FiatCrypto.
diff --git a/src/StandaloneOCamlMain.v b/src/StandaloneOCamlMain.v
index 2a19c9baee6..9c7710a56ff 100644
--- a/src/StandaloneOCamlMain.v
+++ b/src/StandaloneOCamlMain.v
@@ -233,3 +233,8 @@ Module BaseConversion.
   Definition main : unit
     := main_gen ForExtraction.BaseConversion.PipelineMain.
 End BaseConversion.
+
+Module FiatCrypto.
+  Definition main : unit
+    := main_gen ForExtraction.FiatCrypto.PipelineMain.
+End FiatCrypto.
diff --git a/src/Util/Arg.v b/src/Util/Arg.v
index f61be6b2807..3e9ea65ef82 100644
--- a/src/Util/Arg.v
+++ b/src/Util/Arg.v
@@ -548,15 +548,24 @@ Definition default_named_results {ls}
      | (_, s, _) :: ss => @default_named_results' _ ss default_named_result
      end.
 
-Definition parse_argv (argv : list string) (arg_spec : arg_spec)
+Class prog_name_countT := prog_name_count : nat.
+Global Typeclasses Opaque prog_name_countT.
+Ltac fill_default_prog_name_countT _
+  := lazymatch goal with
+     | [ H : prog_name_countT |- prog_name_countT ] => exact H
+     | [ |- prog_name_countT ] => exact 1%nat
+     end.
+Global Hint Extern 1 prog_name_countT => fill_default_prog_name_countT () : typeclass_instances.
+
+Definition parse_argv {prog_name_count : prog_name_countT} (argv : list string) (arg_spec : arg_spec)
   : parse_result (arg_spec_results arg_spec)
-  := match argv with
-     | nil => Error missing_prog_name
-     | prog_name :: argv
-       => (res <- consume_args (10 + (List.length argv)) argv arg_spec (missing prog_name) (wrong prog_name) (too_many_args prog_name) (internal_error prog_name) (no_keyed_arg prog_name) (help prog_name) (out_of_fuel prog_name);
+  := if (List.length argv <? prog_name_count)%nat
+     then Error missing_prog_name
+     else let '(prog_names, argv) := (List.firstn prog_name_count argv, List.skipn prog_name_count argv) in
+          let prog_name := String.concat " " prog_names in
+          (res <- consume_args (10 + (List.length argv)) argv arg_spec (missing prog_name) (wrong prog_name) (too_many_args prog_name) (internal_error prog_name) (no_keyed_arg prog_name) (help prog_name) (out_of_fuel prog_name);
           let '(upd, anon_data, anon_opt_data, anon_opt_repeated_data) := res in
-          Success (upd default_named_results, anon_data, anon_opt_data, anon_opt_repeated_data))
-     end%error.
+          Success (upd default_named_results, anon_data, anon_opt_data, anon_opt_repeated_data))%error.
 
 Definition is_real_error (e : parse_error) : bool := match e with help _ => false | _ => true end.