Add HOL Light proof for aarch64 poly_caddq

Add the first HOL Light functional correctness proof for an aarch64
ML-DSA function: poly_caddq, which performs conditional addition of q
to reduce polynomial coefficients from (-q, q) to [0, q).

This commit includes:
- HOL Light proof infrastructure for aarch64 (Makefile, utilities)
- Functional correctness proof showing the assembly computes
  `ival(x i) rem &8380417` for each coefficient
- autogen support for generating aarch64 HOL Light assembly
- Updates of both HOL-Light and s2n-bignum
- HOL-Light CI is extended and closely aligned with mlkem-native

- Resolves #493

Signed-off-by: Matthias J. Kannwischer <[email protected]>

Author: mkannwischer

.github/workflows/hol_light.yml

@@ -9,18 +9,28 @@ on:
     branches: ["main"]
     paths:
      - '.github/workflows/hol_light.yml'
+     - 'proofs/hol_light/aarch64/Makefile'
+     - 'proofs/hol_light/aarch64/**/*.S'
+     - 'proofs/hol_light/aarch64/**/*.ml'
      - 'proofs/hol_light/x86_64/Makefile'
      - 'proofs/hol_light/x86_64/**/*.S'
      - 'proofs/hol_light/x86_64/**/*.ml'
+     - 'flake.nix'
+     - 'flake.lock'
      - 'nix/hol_light/*'
      - 'nix/s2n_bignum/*'
   pull_request:
     branches: ["main"]
     paths:
       - '.github/workflows/hol_light.yml'
+      - 'proofs/hol_light/aarch64/Makefile'
+      - 'proofs/hol_light/aarch64/**/*.S'
+      - 'proofs/hol_light/aarch64/**/*.ml'
       - 'proofs/hol_light/x86_64/Makefile'
       - 'proofs/hol_light/x86_64/**/*.S'
       - 'proofs/hol_light/x86_64/**/*.ml'
+      - 'flake.nix'
+      - 'flake.lock'
       - 'nix/hol_light/*'
       - 'nix/s2n_bignum/*'
 
@@ -33,8 +43,8 @@ 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
-    runs-on: pqcp-x64
+    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:
       - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
@@ -47,8 +57,8 @@ jobs:
           script: |
             autogen --update-hol-light-bytecode --dry-run
   hol_light_interactive:
-    name: HOL-Light interactive shell test
-    runs-on: pqcp-x64
+    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
     steps:
@@ -60,21 +70,100 @@ jobs:
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           nix-shell: 'hol_light'
           script: |
-            # Load base infrastructure and specs to validate HOL-Light environment
-            # When we have smaller/faster proofs, we can run them here instead:
-            # make -C proofs/hol_light/x86_64 mldsa/mldsa_ntt.o
-            # echo 'needs "proofs/mldsa_ntt.ml";;' | hol.sh
-            echo 'needs "x86/proofs/base.ml";; needs "proofs/mldsa_specs.ml";; #quit;;' | hol.sh
+            make -C proofs/hol_light/aarch64 mldsa/mldsa_poly_caddq.o
+            echo 'needs "aarch64/proofs/mldsa_poly_caddq.ml";;' | hol.sh
   hol_light_proofs:
     needs: [ hol_light_bytecode ]
+    strategy:
+      fail-fast: false
+      matrix:
+        proof:
+          # Dependencies on {name}.{S,ml} are implicit
+          - name: mldsa_poly_caddq
+            needs: ["aarch64_utils.ml"]
+    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:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        with:
+          fetch-depth: 0
+      - name: Get changed files
+        id: changed-files
+        uses: tj-actions/changed-files@e0021407031f5be11a464abee9a0776171c79891 # v47.0.1
+      - 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/aarch64/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
+
+  # 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: |
+            # TODO: Enable when we have a cheaper proof
+            # make -C proofs/hol_light/x86_64 mldsa/mldsa_ntt.o
+            # echo 'needs "x86_64/proofs/mldsa_ntt.ml";;' | hol.sh
+            echo 'needs "x86/proofs/base.ml";; needs "x86_64/proofs/mldsa_specs.ml";; #quit;;' | 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: mldsa_ntt
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
-    name: HOL Light proof for ${{ matrix.proof.name }}.S
+    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:

README.md

@@ -59,12 +59,12 @@ We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to
 
 **Note:** The `MLD_CONFIG_REDUCE_RAM` configuration option is not currently covered by CBMC proofs.
 
-HOL-Light functional correctness proofs can be found in [proofs/hol_light/x86_64](proofs/hol_light/x86_64). So far, the following functions have been proven correct:
+HOL-Light functional correctness proofs can be found in [proofs/hol_light](proofs/hol_light). So far, the following functions have been proven correct:
 
+- AArch64 poly_caddq [poly_caddq_asm.S](mldsa/src/native/aarch64/src/poly_caddq_asm.S)
 - x86_64 NTT [ntt.S](mldsa/src/native/x86_64/src/ntt.S)
 
-
-These proofs are utilizing the verification infrastructure in [s2n-bignum](https://github.com/awslabs/s2n-bignum).
+These proofs utilize the verification infrastructure in [s2n-bignum](https://github.com/awslabs/s2n-bignum).
 
 ## Security
 

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

@@ -1,18 +1,8 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 diff --git a/hol_4.14.sh b/hol_4.14.sh
-index 1311255..8b2bc36 100755
 --- a/hol_4.14.sh
 +++ b/hol_4.14.sh
-@@ -5,7 +5,7 @@ export HOLLIGHT_DIR=__DIR__
-
- if [ "$#" -eq 1 ]; then
-   if [ "$1" == "-pp" ]; then
--    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo"
-+    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I ${HOLLIGHT_DIR} pa_j.cmo"
-     exit 0
-   elif [ "$1" == "-dir" ]; then
-     echo "${HOLLIGHT_DIR}"
-@@ -32,4 +32,13 @@ if [ "${HOL_ML_PATH}" == "" ]; then
+@@ -57,4 +57,13 @@ if [ "${HOL_ML_PATH}" == "" ]; then
    HOL_ML_PATH="${HOLLIGHT_DIR}/hol.ml"
  fi
 
@@ -21,22 +11,21 @@ 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 mldsa-native proofs
-+export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR_X86_64}:${HOLLIGHT_LOAD_PATH}"
++export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR}:${HOLLIGHT_LOAD_PATH}"
 +
 +# Change to mldsa-native proofs directory if set, so define_from_elf can find object files
-+[ -n "${PROOF_DIR_X86_64}" ] && cd "${PROOF_DIR_X86_64}"
++[ -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
-index 0aaa5c7..5adaf4c 100755
 --- a/hol_4.sh
 +++ b/hol_4.sh
 @@ -5,7 +5,7 @@ export HOLLIGHT_DIR=__DIR__
 
  if [ "$#" -eq 1 ]; then
    if [ "$1" == "-pp" ]; then
 -    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo"
-+    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "${HOLLIGHT_DIR}" pa_j.cmo"
++    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I \"${HOLLIGHT_DIR}\" pa_j.cmo"
      exit 0
    elif [ "$1" == "-dir" ]; then
      echo "${HOLLIGHT_DIR}"

nix/hol_light/default.nix

@@ -9,21 +9,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-2026-01-17";
   src = fetchFromGitHub {
     owner = "jrh13";
     repo = "hol-light";
-    rev = "bed58fa74649fa74015176f8f90e77f7af5cf8e3";
-    hash = "sha256-QDubbUUChvv04239BdcKPSU+E2gdSzqAWfAETK2Xtg0=";
+    rev = "e960dd0f636c36d48f79664c7cf11a59ba6f66a3";
+    hash = "sha256-ZgOzAYokQsgO1Ua3m50shxvU9dVSzocuFHRLdIrINmU=";
   };
   patches = [
     ./0005-Configure-hol-sh-for-mldsa-native.patch
     ./0006-Add-findlib-to-ocaml-hol.patch
   ];
   propagatedBuildInputs = old.propagatedBuildInputs ++ old.nativeBuildInputs ++ [ ocamlPackages.pcre2 ledit ];
   buildPhase = ''
+    patchShebangs .
     HOLLIGHT_USE_MODULE=1 make hol.sh
-    patchShebangs hol.sh
     HOLLIGHT_USE_MODULE=1 make
   '';
   installPhase = ''

nix/hol_light/hol-server.sh

@@ -15,8 +15,8 @@ PORT=${1:-2012}
 HOL_LIGHT_DIR="@hol_light@/lib/hol_light"
 HOL_SERVER_SRC="@hol_server_src@"
 
-# cd to x86_64 proofs directory if in mldsa-native repo
-PROOF_DIR="$(git rev-parse --show-toplevel 2>/dev/null)/proofs/hol_light/x86_64"
+# cd to proofs directory if in mldsa-native repo
+PROOF_DIR="$(git rev-parse --show-toplevel 2>/dev/null)/proofs/hol_light"
 [ -d "$PROOF_DIR" ] && cd "$PROOF_DIR"
 
 echo "Starting HOL Light server on port $PORT..."

nix/s2n_bignum/default.nix

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

proofs/hol_light/README.md

@@ -2,11 +2,11 @@
 
 # HOL Light functional correctness proofs
 
-This directory contains functional correctness proofs for x86_64 assembly routines
+This directory contains functional correctness proofs for AArch64 and x86_64 assembly routines
 used in mldsa-native. The proofs 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 [x86_64/proofs/](x86_64/proofs). Each file
+Each function is proved in a separate `.ml` file in [aarch64/proofs/](aarch64/proofs) and [x86_64/proofs/](x86_64/proofs). Each file
 contains the byte code being verified, as well as the specification that is being proved.
 
 ## Reproducing the proofs
@@ -19,12 +19,19 @@ nix develop .#hol_light --experimental-features 'nix-command flakes'
 
 from mldsa-native's base directory. Then
 
+```bash
+make -C proofs/hol_light/aarch64
+```
+or
+
 ```bash
 make -C proofs/hol_light/x86_64
 ```
 
 will build and run the proofs. Note that this may take hours even on powerful machines.
 
+For convenience, you can also use `tests hol_light` which wraps the `make` invocation above; see `tests hol_light --help`.
+
 ## Interactive proof development
 
 For interactive proof development, start the HOL Light server:
@@ -44,4 +51,5 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
 
 ## What is covered?
 
+- AArch64 poly_caddq: [mldsa_poly_caddq.S](aarch64/mldsa/mldsa_poly_caddq.S)
 - x86_64 forward NTT: [mldsa_ntt.S](x86_64/mldsa/mldsa_ntt.S)