diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml
index 91ae5187a8..4f9ab1c39a 100644
--- a/.github/workflows/coq-alpine.yml
+++ b/.github/workflows/coq-alpine.yml
@@ -55,23 +55,23 @@ jobs:
 #      shell: alpine.sh {0}
 #      run: make install-standalone-js-of-ocaml
     - name: upload standalone files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: standalone-${{ matrix.alpine }}
         path: dist/fiat_crypto
 #    - name: upload standalone js files
-#      uses: actions/upload-artifact@v3
+#      uses: actions/upload-artifact@v4
 #      with:
 #        name: standalone-html-${{ matrix.alpine }}
 #        path: fiat-html
     - name: upload OCaml files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionOCaml-${{ matrix.alpine }}
         path: src/ExtractionOCaml
       if: always ()
 #    - name: upload js_of_ocaml files
-#      uses: actions/upload-artifact@v3
+#      uses: actions/upload-artifact@v4
 #      with:
 #        name: ExtractionJsOfOCaml-${{ matrix.alpine }}
 #        path: src/ExtractionJsOfOCaml
@@ -82,7 +82,7 @@ jobs:
     - run: tar -czvf generated-files.tgz fiat-*/
       if: ${{ failure() }}
     - name: upload generated files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: generated-files-${{ matrix.alpine }}
         path: generated-files.tgz
@@ -91,7 +91,7 @@ jobs:
       shell: alpine.sh {0}
       run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
     - name: upload Haskell files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionHaskell-${{ matrix.alpine }}
         path: src/ExtractionHaskell
@@ -126,7 +126,7 @@ jobs:
     steps:
     - uses: actions/checkout@v4
     - name: Download standalone ${{ matrix.alpine }}
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-${{ matrix.alpine }}
         path: dist/
@@ -161,7 +161,7 @@ jobs:
         fetch-depth: 0 # Fetch all history for all tags and branches
         tags: true     # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
     - name: Download standalone edge
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-edge
         path: dist/
diff --git a/.github/workflows/coq-archlinux.yml b/.github/workflows/coq-archlinux.yml
index 71beb5334d..0a3f3abc32 100644
--- a/.github/workflows/coq-archlinux.yml
+++ b/.github/workflows/coq-archlinux.yml
@@ -47,7 +47,7 @@ jobs:
     - run: tar -czvf generated-files.tgz fiat-*/
       if: ${{ failure() }}
     - name: upload generated files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: generated-files-archlinux
         path: generated-files.tgz
@@ -59,23 +59,23 @@ jobs:
     #- name: install-standalone-js-of-ocaml
     #  run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
     - name: upload standalone files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: standalone-archlinux
         path: dist/fiat_crypto
     #- name: upload standalone js files
-    #  uses: actions/upload-artifact@v3
+    #  uses: actions/upload-artifact@v4
     #  with:
     #    name: standalone-html-archlinux
     #    path: fiat-html
     - name: upload OCaml files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionOCaml-archlinux
         path: src/ExtractionOCaml
       if: always ()
     #- name: upload js_of_ocaml files
-    #  uses: actions/upload-artifact@v3
+    #  uses: actions/upload-artifact@v4
     #  with:
     #    name: ExtractionJsOfOCaml-archlinux
     #    path: src/ExtractionJsOfOCaml
@@ -83,7 +83,7 @@ jobs:
     - name: standalone-haskell
       run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
     - name: upload Haskell files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionHaskell-archlinux
         path: src/ExtractionHaskell
@@ -111,7 +111,7 @@ jobs:
         pacman --noconfirm -Syu git --needed
     - uses: actions/checkout@v4
     - name: Download standalone archlinux
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-archlinux
         path: dist/
@@ -139,7 +139,7 @@ jobs:
         fetch-depth: 0 # Fetch all history for all tags and branches
         tags: true     # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
     - name: Download standalone archlinux
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-archlinux
         path: dist/
diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
index 93cd29d80d..cf066bf94d 100644
--- a/.github/workflows/coq-debian.yml
+++ b/.github/workflows/coq-debian.yml
@@ -48,7 +48,7 @@ jobs:
     - run: tar -czvf generated-files.tgz fiat-*/
       if: ${{ failure() }}
     - name: upload generated files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: generated-files-${{ matrix.debian }}
         path: generated-files.tgz
@@ -60,23 +60,23 @@ jobs:
     - name: install-standalone-js-of-ocaml
       run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
     - name: upload standalone files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: standalone-${{ matrix.debian }}
         path: dist/fiat_crypto
     - name: upload standalone js files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: standalone-html-${{ matrix.debian }}
         path: fiat-html
     - name: upload OCaml files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionOCaml-${{ matrix.debian }}
         path: src/ExtractionOCaml
       if: always ()
     - name: upload js_of_ocaml files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionJsOfOCaml-${{ matrix.debian }}
         path: src/ExtractionJsOfOCaml
@@ -84,7 +84,7 @@ jobs:
     - name: standalone-haskell
       run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
     - name: upload Haskell files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionHaskell-${{ matrix.debian }}
         path: src/ExtractionHaskell
@@ -114,7 +114,7 @@ jobs:
     steps:
     - uses: actions/checkout@v4
     - name: Download standalone ${{ matrix.debian }}
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-${{ matrix.debian }}
         path: dist/
@@ -159,7 +159,7 @@ jobs:
         fetch-depth: 0 # Fetch all history for all tags and branches
         tags: true     # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
     - name: Download standalone sid
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-sid
         path: dist/
diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml
index 20587cda88..13980fee9d 100644
--- a/.github/workflows/coq-docker.yml
+++ b/.github/workflows/coq-docker.yml
@@ -68,19 +68,19 @@ jobs:
         export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY
         custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 pre-standalone-extracted
     - name: upload OCaml files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }}
         path: src/ExtractionOCaml
       if: always ()
     - name: upload js_of_ocaml source files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionJsOfOCaml-source-${{ matrix.env.COQ_VERSION }}
         path: src/ExtractionJsOfOCaml
       if: always ()
     - name: upload Haskell source files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionHaskell-source-${{ matrix.env.COQ_VERSION }}
         path: src/ExtractionHaskell
@@ -88,13 +88,13 @@ jobs:
     - 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
+      uses: actions/upload-artifact@v4
       with:
         name: standalone-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}
         path: dist/fiat_crypto
     - run: git config --file .gitmodules --get-regexp path | awk '{ print $2 }' | xargs tar -czvf fiat-crypto-build.tar.gz src
     - name: Upload built files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: build-outputs-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }}
         path: fiat-crypto-build.tar.gz
@@ -195,7 +195,7 @@ jobs:
     - name: Load Docker image
       run: docker load -i image.tar
     - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: build-outputs-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }}
         path: .
@@ -237,7 +237,7 @@ jobs:
     - name: echo build params
       run: etc/ci/describe-system-config.sh
     - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: ExtractionJsOfOCaml-source-${{ matrix.coq-version }}
         path: src/ExtractionJsOfOCaml
@@ -248,13 +248,13 @@ jobs:
     - name: install-standalone-js-of-ocaml
       run: make -f Makefile.standalone install-standalone-js-of-ocaml
     - name: upload js_of_ocaml build files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionJsOfOCaml-${{ matrix.coq-version }}-ocaml-${{ matrix.ocaml-compiler }}
         path: src/ExtractionJsOfOCaml
       if: always ()
     - name: Upload js_of_ocaml outputs
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: fiat-html-js-of-ocaml
         path: fiat-html
@@ -298,7 +298,7 @@ jobs:
     - name: echo build params
       run: etc/ci/describe-system-config.sh
     - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: ExtractionJsOfOCaml-source-${{ matrix.coq-version }}
         path: src/ExtractionJsOfOCaml
@@ -309,13 +309,13 @@ jobs:
     - 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
+      uses: actions/upload-artifact@v4
       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
+      uses: actions/upload-artifact@v4
       with:
         name: fiat-html-wasm-of-ocaml
         path: fiat-html
@@ -333,14 +333,14 @@ jobs:
         fetch-depth: 0 # Fetch all history for all tags and branches, for fiat-html/version.js
         tags: true     # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
     - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       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
+      uses: actions/download-artifact@v4
       with:
         name: fiat-html-wasm-of-ocaml
         path: fiat-html
@@ -379,7 +379,7 @@ jobs:
       with:
         submodules: recursive
     - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: ExtractionOCaml-${{ matrix.coq-version }}
         path: src/ExtractionOCaml
@@ -391,7 +391,7 @@ jobs:
     - run: tar -czvf generated-files.tgz fiat-*/
       if: ${{ failure() }}
     - name: upload generated files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: generated-files-${{ matrix.coq-version }}
         path: generated-files.tgz
@@ -412,14 +412,14 @@ jobs:
       with:
         submodules: recursive
     - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: ExtractionHaskell-source-${{ matrix.coq-version }}
         path: src/ExtractionHaskell
     - name: standalone-haskell
       run: etc/ci/github-actions-make.sh -f Makefile.standalone -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
     - name: upload Haskell files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionHaskell-${{ matrix.coq-version }}
         path: src/ExtractionHaskell
@@ -441,7 +441,7 @@ jobs:
       with:
         submodules: recursive
     - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: ExtractionOCaml-master
         path: src/ExtractionOCaml
@@ -466,7 +466,7 @@ jobs:
     steps:
     - uses: actions/checkout@v4
     - name: Download standalone Docker
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-docker-coq-${{ matrix.docker-coq-version }}
         path: dist/
@@ -511,7 +511,7 @@ jobs:
         fetch-depth: 0 # Fetch all history for all tags and branches
         tags: true     # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
     - name: Download standalone Docker
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-docker-coq-dev
         path: dist/
diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml
index da776310cd..2ba8c8003d 100644
--- a/.github/workflows/coq-windows.yml
+++ b/.github/workflows/coq-windows.yml
@@ -83,22 +83,22 @@ jobs:
     - name: only-test-amd64-files-lite
       run: opam exec -- etc/ci/github-actions-make.sh -j${{ env.NJOBS }} only-test-amd64-files-lite SLOWEST_FIRST=1
     - name: upload OCaml files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionOCaml
         path: src/ExtractionOCaml
     - name: upload js_of_ocaml files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ExtractionJsOfOCaml
         path: src/ExtractionJsOfOCaml
     - name: upload standalone files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: standalone-windows
         path: dist/fiat_crypto.exe
     - name: upload standalone js files
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: standalone-html-windows
         path: fiat-html
@@ -115,7 +115,7 @@ jobs:
       run: etc/ci/github-actions-display-per-line-timing.sh
       shell: bash
 #    - name: upload timing and .vo info
-#      uses: actions/upload-artifact@v3
+#      uses: actions/upload-artifact@v4
 #      with:
 #        name: build-outputs
 #        path: .
@@ -132,7 +132,7 @@ jobs:
     steps:
     - uses: actions/checkout@v4
     - name: Download standalone Windows
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-windows
         path: dist/
@@ -167,7 +167,7 @@ jobs:
         fetch-depth: 0 # Fetch all history for all tags and branches
         tags: true     # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version
     - name: Download standalone Windows
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: standalone-windows
         path: dist/
diff --git a/.github/workflows/java.yml b/.github/workflows/java.yml
index b38aa73010..c5e4c68a20 100644
--- a/.github/workflows/java.yml
+++ b/.github/workflows/java.yml
@@ -29,7 +29,7 @@ jobs:
       run: make only-test-java-files EXTERNAL_DEPENDENCIES=1
     - name: make documentation
       run: make only-javadoc EXTERNAL_DEPENDENCIES=1
-    - uses: actions/upload-artifact@v3
+    - uses: actions/upload-artifact@v4
       with:
         name: fiat-javadoc
         path: fiat-java/doc