HOL-Light: improve tooling and CI

.github/workflows/hol_light.yml

@@ -41,12 +41,37 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
+  # Check that all proofs provide the expected theorems.
+  hol_light_check_structure:
+    strategy:
+      fail-fast: true
+      matrix:
+        arch: [aarch64, x86_64]
+        include:
+          - arch: aarch64
+            runs-on: pqcp-arm64
+          - arch: x86_64
+            runs-on: pqcp-x64
+    name: HOL-Light theorem structure check for ${{ matrix.arch }}
+    runs-on: ${{ matrix.runs-on }}
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          fetch-depth: 0
+      - uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            scripts/check-theorems ${{ matrix.arch }}
   # The proofs also check that the byte code is up to date,
   # but we use this as a fast path to not even start the proofs
   # if the byte code needs updating.
   hol_light_bytecode:
     name: AArch64 HOL-Light bytecode check
     runs-on: pqcp-arm64
+    needs: [ hol_light_check_structure ]
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
@@ -131,6 +156,7 @@ jobs:
   hol_light_bytecode_x86_64:
     name: x86_64 HOL-Light bytecode check
     runs-on: pqcp-x64
+    needs: [ hol_light_check_structure ]
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

scripts/check-theorems

@@ -0,0 +1,45 @@
+#!/usr/bin/env bash
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+# Verify that every proof contains the expected set of theorems.
+
+set -euo pipefail
+
+usage()
+{
+  echo "Usage: $0 <architecture>" >&2
+  echo "  architecture: aarch64 | x86_64" >&2
+  exit 1
+}
+
+[[ $# -eq 1 ]] || usage
+ARCH="$1"
+
+case "$ARCH" in
+  aarch64 | x86_64) ;;
+  *)
+    echo "ERROR: Unknown architecture '$ARCH'." >&2
+    usage
+    ;;
+esac
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+PROOFS_DIR="$SCRIPT_DIR/../proofs/hol_light/$ARCH/proofs"
+
+PROOFS="$(tests hol_light -l -a "$ARCH")"
+ERRORS=0
+
+for routine in $PROOFS; do
+  suffixes=("CORRECT" "SAFE" "SUBROUTINE_SAFE")
+  [[ $ARCH == "x86_64" ]] && suffixes+=("SUBROUTINE_CORRECT" "NOIBT_SUBROUTINE_CORRECT" "NOIBT_SUBROUTINE_SAFE")
+
+  for sfx in "${suffixes[@]}"; do
+    if ! grep -q "_${sfx}" "$PROOFS_DIR/${routine}.ml"; then
+      echo "FAIL: ${routine}_${sfx} not found in ${routine}.ml" >&2
+      ((ERRORS++)) || true
+    fi
+  done
+done
+
+[[ $ERRORS -eq 0 ]] && echo "OK" || exit 1

scripts/tests

@@ -1003,7 +1003,9 @@ class Tests:
 
     def hol_light(self):
 
-        if platform.machine().lower() in ["arm64", "aarch64"]:
+        if self.args.arch:
+            arch = self.args.arch
+        elif platform.machine().lower() in ["arm64", "aarch64"]:
             arch = "aarch64"
         elif platform.machine().lower() in ["x86_64"]:
             arch = "x86_64"
@@ -1036,12 +1038,19 @@ class Tests:
                     os.remove(os.path.join(proof_dir, proof_target))
                 except FileNotFoundError:
                     pass
+
+                make_cmd = [
+                    "make",
+                    f"mldsa/{func}.correct",
+                ] + self.make_j()
+
+                # If --use-nix is specified, enter nix shell
+                if self.args.use_nix:
+                    nix_profile = f"hol_light-cross-{arch}"
+                    make_cmd = ["nix", "develop", f".#{nix_profile}", "-c"] + make_cmd
+
                 p = subprocess.run(
-                    [
-                        "make",
-                        f"mldsa/{func}.correct",
-                    ]
-                    + self.make_j(),
+                    make_cmd,
                     cwd="proofs/hol_light/" + arch,
                     env=os.environ.copy(),
                     capture_output=(self.args.verbose is False),
@@ -1449,6 +1458,21 @@ def cli():
         default=False,
     )
 
+    hol_light_parser.add_argument(
+        "-a",
+        "--arch",
+        help="Architecture for which to list/run HOL_LIGHT proofs (aarch64 or x86_64).",
+        choices=["aarch64", "x86_64"],
+        default=None,
+    )
+
+    hol_light_parser.add_argument(
+        "--use-nix",
+        help="Use nix cross environment for the specified architecture.",
+        action="store_true",
+        default=False,
+    )
+
     # func arguments
     func_parser = cmd_subparsers.add_parser(
         "func",