HOL Light proofs infrastructure for x86 and basemul proof

Signed-off-by: Dusan Kostic <dkostic@protonmail.com>

Author: dkostic

.github/workflows/hol_light.yml

@@ -12,6 +12,9 @@ on:
      - 'proofs/hol_light/arm/Makefile'
      - 'proofs/hol_light/arm/**/*.S'
      - 'proofs/hol_light/arm/**/*.ml'
+     - 'proofs/hol_light/x86/Makefile'
+     - 'proofs/hol_light/x86/**/*.S'
+     - 'proofs/hol_light/x86/**/*.ml'
      - 'flake.nix'
      - 'flake.lock'
      - 'nix/hol_light/*'
@@ -23,6 +26,9 @@ on:
       - 'proofs/hol_light/arm/Makefile'
       - 'proofs/hol_light/arm/**/*.S'
       - 'proofs/hol_light/arm/**/*.ml'
+      - 'proofs/hol_light/x86/Makefile'
+      - 'proofs/hol_light/x86/**/*.S'
+      - 'proofs/hol_light/x86/**/*.ml'
       - 'flake.nix'
       - 'flake.lock'
       - 'nix/hol_light/*'
@@ -37,7 +43,7 @@ jobs:
   # but we use this as a fast path to not even start the proofs
   # if the byte code needs updating.
   hol_light_bytecode:
-    name: HOL-Light bytecode check
+    name: AArch64 HOL-Light bytecode check
     runs-on: pqcp-arm64
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
     steps:
@@ -51,7 +57,7 @@ jobs:
           script: |
             autogen --update-hol-light-bytecode --dry-run
   hol_light_interactive:
-    name: HOL-Light interactive shell test
+    name: AArch64 HOL-Light interactive shell test
     runs-on: pqcp-arm64
     needs: [ hol_light_bytecode ]
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
@@ -65,7 +71,7 @@ jobs:
           nix-shell: 'hol_light'
           script: |
             make -C proofs/hol_light/arm mlkem/mlkem_poly_tobytes.o
-            echo 'needs "proofs/mlkem_poly_tobytes.ml";;' | hol.sh
+            echo 'needs "arm/proofs/mlkem_poly_tobytes.ml";;' | hol.sh
   hol_light_proofs:
     needs: [ hol_light_bytecode ]
     strategy:
@@ -103,7 +109,7 @@ jobs:
             needs: ["keccak_specs.ml"]
           - name: keccak_f1600_x4_v8a_scalar
             needs: ["keccak_specs.ml"]
-    name: HOL Light proof for ${{ matrix.proof.name }}.S
+    name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
     runs-on: pqcp-arm64
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
     steps:
@@ -142,3 +148,87 @@ jobs:
           nix-shell: 'hol_light'
           script: |
             tests hol_light -p ${{ matrix.proof.name }} --verbose
+
+  # x86_64 proofs
+  hol_light_bytecode_x86_64:
+    name: x86_64 HOL-Light bytecode check
+    runs-on: pqcp-x64
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        with:
+          fetch-depth: 0
+      - uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            autogen --update-hol-light-bytecode --dry-run
+  hol_light_interactive_x86_64:
+    name: x86_64 HOL-Light interactive shell test
+    runs-on: pqcp-x64
+    needs: [ hol_light_bytecode_x86_64 ]
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        with:
+          fetch-depth: 0
+      - uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            make -C proofs/hol_light/x86 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
+            echo 'needs "x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
+  hol_light_proofs_x86_64:
+    needs: [ hol_light_bytecode_x86_64 ]
+    strategy:
+      fail-fast: false
+      matrix:
+        proof:
+          # Dependencies on {name}.{S,ml} are implicit
+          - name: mlkem_poly_basemul_acc_montgomery_cached_k2
+            needs: ["mlkem_specs.ml"]
+          - name: mlkem_poly_basemul_acc_montgomery_cached_k3
+            needs: ["mlkem_specs.ml"]
+          - name: mlkem_poly_basemul_acc_montgomery_cached_k4
+            needs: ["mlkem_specs.ml"]
+    name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
+    runs-on: pqcp-x64
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        with:
+          fetch-depth: 0
+      - name: Get changed files
+        id: changed-files
+        uses: tj-actions/changed-files@24d32ffd492484c1d75e0c0b894501ddb9d30d62 # v47.0.0
+      - name: Check if dependencies changed
+        id: check_run
+        shell: bash
+        run: |
+          run_needed=0
+          changed_files="${{ steps.changed-files.outputs.all_changed_files }}"
+          dependencies="${{ join(matrix.proof.needs, ' ') }} ${{ format('{0}.S {0}.ml', matrix.proof.name) }}"
+          for changed in $changed_files; do
+            for needs in $dependencies; do
+               if [[ "$changed" == *"$needs" ]]; then
+                 run_needed=1
+               fi
+            done
+          done
+
+          # Always re-run upon change to nix files for HOL-Light
+          if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86/Makefile"* ]]; then
+            run_needed=1
+          fi
+
+          echo "run_needed=${run_needed}" >> $GITHUB_OUTPUT
+      - uses: ./.github/actions/setup-shell
+        if: |
+          steps.check_run.outputs.run_needed == '1'
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            tests hol_light -p ${{ matrix.proof.name }} --verbose

BIBLIOGRAPHY.md

@@ -113,7 +113,7 @@ source code and documentation.
   - [mlkem/src/fips202/native/aarch64/auto.h](mlkem/src/fips202/native/aarch64/auto.h)
   - [mlkem/src/fips202/native/aarch64/src/keccak_f1600_x1_v84a_asm.S](mlkem/src/fips202/native/aarch64/src/keccak_f1600_x1_v84a_asm.S)
   - [mlkem/src/fips202/native/aarch64/src/keccak_f1600_x2_v84a_asm.S](mlkem/src/fips202/native/aarch64/src/keccak_f1600_x2_v84a_asm.S)
-  - [proofs/hol_light/arm/README.md](proofs/hol_light/arm/README.md)
+  - [proofs/hol_light/README.md](proofs/hol_light/README.md)
   - [proofs/hol_light/arm/mlkem/keccak_f1600_x1_v84a.S](proofs/hol_light/arm/mlkem/keccak_f1600_x1_v84a.S)
   - [proofs/hol_light/arm/mlkem/keccak_f1600_x2_v84a.S](proofs/hol_light/arm/mlkem/keccak_f1600_x2_v84a.S)
 
@@ -248,7 +248,7 @@ source code and documentation.
 * URL: https://github.com/slothy-optimizer/slothy/
 * Referenced from:
   - [dev/README.md](dev/README.md)
-  - [proofs/hol_light/arm/README.md](proofs/hol_light/arm/README.md)
+  - [proofs/hol_light/README.md](proofs/hol_light/README.md)
 
 ### `SLOTHY_Paper`
 

flake.nix

@@ -101,8 +101,8 @@
           }).overrideAttrs (old: {
             shellHook = ''
               export PATH=$PWD/scripts:$PATH
-              # Set PROOF_DIR_ARM based on where we entered the shell
-              export PROOF_DIR_ARM="$PWD/proofs/hol_light/arm"
+              # Set PROOF_DIR based on where we entered the shell
+              export PROOF_DIR="$PWD/proofs/hol_light"
             '';
           });
           devShells.ci = util.mkShell {

nix/hol_light/0005-Configure-hol-sh-for-mlkem-native.patch

@@ -21,10 +21,10 @@ index 1311255..8b2bc36 100755
 +SITELIB=$(dirname $(ocamlfind query findlib 2>/dev/null) 2>/dev/null)
 +
 +# Set HOLLIGHT_LOAD_PATH to include S2N_BIGNUM_DIR and mlkem-native proofs
-+export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR_ARM}:${HOLLIGHT_LOAD_PATH}"
++export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR}:${HOLLIGHT_LOAD_PATH}"
 +
 +# Change to mlkem-native proofs directory if set, so define_from_elf can find object files
-+[ -n "${PROOF_DIR_ARM}" ] && cd "${PROOF_DIR_ARM}"
++[ -n "${PROOF_DIR}" ] && cd "${PROOF_DIR}"
 +
 +${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOL_ML_PATH} -I ${HOLLIGHT_DIR} ${SITELIB:+-I "$SITELIB"}
 diff --git a/hol_4.sh b/hol_4.sh

nix/hol_light/default.nix

@@ -7,19 +7,21 @@ hol_light.overrideAttrs (old: {
     export HOLLIGHT_DIR="$1/lib/hol_light"
     export PATH="$1/lib/hol_light:$PATH"
   '';
-  version = "unstable-2025-09-22";
+  version = "unstable-2025-11-17";
   src = fetchFromGitHub {
     owner = "jrh13";
     repo = "hol-light";
-    rev = "bed58fa74649fa74015176f8f90e77f7af5cf8e3";
-    hash = "sha256-QDubbUUChvv04239BdcKPSU+E2gdSzqAWfAETK2Xtg0=";
+    rev = "08bcac75772d37c2447a90c90d1dff9ab415f217";
+    hash = "sha256-kYOzGW7uQGOM/b+JPWQfpqqtgMmMku/BkN58WZTtokU=";
   };
   patches = [
     ./0005-Configure-hol-sh-for-mlkem-native.patch
     ./0006-Add-findlib-to-ocaml-hol.patch
   ];
   propagatedBuildInputs = old.propagatedBuildInputs ++ old.nativeBuildInputs ++ [ ocamlPackages.pcre2 ledit ];
   buildPhase = ''
+    patchShebangs pa_j/chooser.sh
+    patchShebangs update_database/chooser.sh
     HOLLIGHT_USE_MODULE=1 make hol.sh
     patchShebangs hol.sh
     HOLLIGHT_USE_MODULE=1 make

nix/s2n_bignum/default.nix

@@ -2,12 +2,12 @@
 { stdenv, fetchFromGitHub, writeText, ... }:
 stdenv.mkDerivation rec {
   pname = "s2n_bignum";
-  version = "2ab2252b8505e58a7c3392f8ad823782032b61e7";
+  version = "84a604317b94cbca9f14c7b2b771afc2827ab99f";
   src = fetchFromGitHub {
     owner = "awslabs";
     repo = "s2n-bignum";
     rev = "${version}";
-    hash = "sha256-7lil3jAFo5NiyNOSBYZcRjduXkotV3x4PlxXSKt63M8=";
+    hash = "sha256-J2tVZ2x23ZHP+ZNkbiUqyaci5bu4zNfkXuRemnuB+N0=";
   };
   setupHook = writeText "setup-hook.sh" ''
     export S2N_BIGNUM_DIR="$1"

proofs/hol_light/arm/README.md proofs/hol_light/README.mdproofs/hol_light/arm/README.md renamed to proofs/hol_light/README.md

@@ -2,12 +2,12 @@
 
 # HOL Light functional correctness proofs
 
-This directory contains functional correctness proofs for all AArch64 assembly routines
-used in mlkem-native. The proofs were largely developed by John Harrison
+This directory contains functional correctness proofs for all AArch64 and some x86_64 assembly routines
+used in mlkem-native. The proofs were largely developed by John Harrison and Dusan Kostic
 and are written in the [HOL Light](https://hol-light.github.io/) theorem
 prover, utilizing the assembly verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum).
 
-Each function is proved in a separate `.ml` file in [proofs/](proofs). Each file
+Each function is proved in a separate `.ml` file in [arm/proofs/](arm/proofs) and [x86/proofs/](x86/proofs). Each file
 contains the byte code being verified, as well as the specification that is being
 proved.
 
@@ -16,7 +16,7 @@ proved.
 Proofs are 'post-hoc' in the sense that HOL-Light/s2n-bignum operate on the final object code. In particular, the means by which the code was generated (including the [SLOTHY](https://github.com/slothy-optimizer/slothy/) superoptimizer) need not be trusted.
 
 Specifications are essentially [Hoare triples](https://en.wikipedia.org/wiki/Hoare_logic), with the noteworthy difference that the program is implicit as the content of memory at the PC; which is asserted to
-be the code under verification as part of the precondition. For example, the following is the specification of the `poly_reduce` function:
+be the code under verification as part of the precondition. For example, the following is the specification of the aarch64 `poly_reduce` function:
 
 ```ocaml
  (* For all (abbreviated by `!` in HOL):
@@ -67,6 +67,11 @@ from mlkem-native's base directory. Then
 ```bash
 make -C proofs/hol_light/arm
 ```
+or
+
+```bash
+make -C proofs/hol_light/x86
+```
 
 will build and run the proofs. Note that this make take hours even on powerful machines.
 
@@ -77,23 +82,27 @@ For convenience, you can also use `tests hol_light` which wraps the `make` invoc
 All AArch64 assembly routines used in mlkem-native are covered. Those are:
 
 - ML-KEM Arithmetic:
-  * AArch64 forward NTT: [mlkem_ntt.S](mlkem/mlkem_ntt.S)
-  * AArch64 inverse NTT: [mlkem_intt.S](mlkem/mlkem_intt.S)
-  * AArch64 base multiplications: [mlkem_poly_basemul_acc_montgomery_cached_k2.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S) [mlkem_poly_basemul_acc_montgomery_cached_k3.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S) [mlkem_poly_basemul_acc_montgomery_cached_k4.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
-  * AArch64 conversion to Montgomery form: [mlkem_poly_tomont.S](mlkem/mlkem_poly_tomont.S)
-  * AArch64 modular reduction: [mlkem_poly_reduce.S](mlkem/mlkem_poly_reduce.S)
-  * AArch64 'multiplication cache' computation: [mlkem_poly_mulcache_compute.S](mlkem/mlkem_poly_mulcache_compute.S)
-  * AArch64 rejection sampling: [mlkem_rej_uniform.S](mlkem/mlkem_rej_uniform.S)
-  * AArch64 polynomial compresseion: [mlkem_poly_tobytes.S](mlkem/mlkem_poly_tobytes.S)
+  * AArch64 forward NTT: [mlkem_ntt.S](arm/mlkem/mlkem_ntt.S)
+  * AArch64 inverse NTT: [mlkem_intt.S](arm/mlkem/mlkem_intt.S)
+  * AArch64 base multiplications: [mlkem_poly_basemul_acc_montgomery_cached_k2.S](arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S) [mlkem_poly_basemul_acc_montgomery_cached_k3.S](arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S) [mlkem_poly_basemul_acc_montgomery_cached_k4.S](arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
+  * AArch64 conversion to Montgomery form: [mlkem_poly_tomont.S](arm/mlkem/mlkem_poly_tomont.S)
+  * AArch64 modular reduction: [mlkem_poly_reduce.S](arm/mlkem/mlkem_poly_reduce.S)
+  * AArch64 'multiplication cache' computation: [mlkem_poly_mulcache_compute.S](arm/mlkem/mlkem_poly_mulcache_compute.S)
+  * AArch64 rejection sampling: [mlkem_rej_uniform.S](arm/mlkem/mlkem_rej_uniform.S)
+  * AArch64 polynomial compresseion: [mlkem_poly_tobytes.S](arm/mlkem/mlkem_poly_tobytes.S)
 - FIPS202:
-  * Keccak-F1600 using lazy rotations[^HYBRID]: [keccak_f1600_x1_scalar.S](mlkem/keccak_f1600_x1_scalar.S)
-  * Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x1_v84a.S](mlkem/keccak_f1600_x1_v84a.S)
-  * 2-fold Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x2_v84a.S](mlkem/keccak_f1600_x2_v84a.S)
-  * 'Hybrid' 4-fold Keccak-F1600 using scalar and v8-A Neon instructions: [keccak_f1600_x4_v8a_scalar.S](mlkem/keccak_f1600_x4_v8a_scalar.S)
-  * 'Triple hybrid' 4-fold Keccak-F1600 using scalar, v8-A Neon and v8.4-A+SHA3 Neon instructions:[keccak_f1600_x4_v8a_v84a_scalar.S](mlkem/keccak_f1600_x4_v8a_v84a_scalar.S)
+  * Keccak-F1600 using lazy rotations[^HYBRID]: [keccak_f1600_x1_scalar.S](arm/mlkem/keccak_f1600_x1_scalar.S)
+  * Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x1_v84a.S](arm/mlkem/keccak_f1600_x1_v84a.S)
+  * 2-fold Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x2_v84a.S](arm/mlkem/keccak_f1600_x2_v84a.S)
+  * 'Hybrid' 4-fold Keccak-F1600 using scalar and v8-A Neon instructions: [keccak_f1600_x4_v8a_scalar.S](arm/mlkem/keccak_f1600_x4_v8a_scalar.S)
+  * 'Triple hybrid' 4-fold Keccak-F1600 using scalar, v8-A Neon and v8.4-A+SHA3 Neon instructions:[keccak_f1600_x4_v8a_v84a_scalar.S](arm/mlkem/keccak_f1600_x4_v8a_v84a_scalar.S)
 
 The NTT and invNTT functions are super-optimized using [SLOTHY](https://github.com/slothy-optimizer/slothy/).
 
+The following x86_64 assembly routines used in mlkem-native are covered:
+- ML-KEM Arithmetic:
+  * x86_64 base multiplications: [mlkem_poly_basemul_acc_montgomery_cached_k2.S](x86/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S) [mlkem_poly_basemul_acc_montgomery_cached_k3.S](x86/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S) [mlkem_poly_basemul_acc_montgomery_cached_k4.S](x86/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
+
 <!--- bibliography --->
 [^HYBRID]: Becker, Kannwischer: Hybrid scalar/vector implementations of Keccak and SPHINCS+ on AArch64, [https://eprint.iacr.org/2022/1243](https://eprint.iacr.org/2022/1243)
 [^SLOTHY]: Abdulrahman, Becker, Kannwischer, Klein: SLOTHY superoptimizer, [https://github.com/slothy-optimizer/slothy/](https://github.com/slothy-optimizer/slothy/)

proofs/hol_light/arm/Makefile

@@ -130,7 +130,7 @@ proofs/dump_bytecode.native: proofs/dump_bytecode.ml $(OBJ)
 
 # Run them and print the standard output+error at *.correct
 %.correct: %.native
-	$< 2>&1 | tee $@
+	cd .. ; ./arm/$< 2>&1 | tee ./arm/$@
 	@if (grep -i "error:\|exception:" "$@" >/dev/null); then  \
 		echo "$< had errors!";			          \
 		exit 1;					          \

proofs/hol_light/arm/proofs/build-proof.sh

@@ -16,7 +16,7 @@
 # - Removal of s2n-bignum specific code that is not relevant for
 #   the mlkem-native proofs.
 
-ROOT="$(realpath "$(dirname "$0")"/../)"
+ROOT="$(realpath "$(dirname "$0")"/../../)"
 
 if [ "$#" -ne 3 ]; then
   echo "${ROOT}/build-proof.sh <.ml file path> <hol.sh> <output .native path>"

proofs/hol_light/arm/proofs/keccak_f1600_x1_scalar.ml

@@ -8,13 +8,13 @@
 (* ========================================================================= *)
 
 needs "arm/proofs/base.ml";;
-needs "proofs/keccak_spec.ml";;
+needs "arm/proofs/keccak_spec.ml";;
 
 (**** print_literal_from_elf "mlkem/keccak_f1600_x1_scalar.o";;
  ****)
 
 let keccak_f1600_x1_scalar_mc = define_assert_from_elf
-  "keccak_f1600_x1_scalar_mc" "mlkem/keccak_f1600_x1_scalar.o"
+  "keccak_f1600_x1_scalar_mc" "arm/mlkem/keccak_f1600_x1_scalar.o"
 (*** BYTECODE START ***)
 [
   0xd10203ff;       (* arm_SUB SP SP (rvalue (word 128)) *)