From 22cb19c626c320ed1be375e0a31f0ab1c27e4349 Mon Sep 17 00:00:00 2001 From: Andreas Hatziiliou Date: Wed, 1 Apr 2026 11:41:39 -0400 Subject: [PATCH 1/3] testing: HOL-Light: add support for cross-proofing This commit introduces two new flags to the hol_light command of the tests script. The first allows user specification of which architecture to run/list the proofs for and the second allows for entering the nix cross-compilation devshell for that architecture. If either are not passed, the behavior is unchanged. Signed-off-by: Andreas Hatziiliou --- scripts/tests | 36 ++++++++++++++++++++++++++++++------ 1 file changed, 30 insertions(+), 6 deletions(-) diff --git a/scripts/tests b/scripts/tests index 56b2c86c3..761335c65 100755 --- a/scripts/tests +++ b/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", From 1f2840ebf46347f65a7c02fd2e6429ab8f402f9d Mon Sep 17 00:00:00 2001 From: Andreas Hatziiliou Date: Wed, 1 Apr 2026 11:42:28 -0400 Subject: [PATCH 2/3] scripts: verify that all expected theorems are present We add a script called check-theorems that ensures that all HOL-Light proofs provide the expected set of theorems depending on the architecture. Signed-off-by: Andreas Hatziiliou --- scripts/check-theorems | 45 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100755 scripts/check-theorems diff --git a/scripts/check-theorems b/scripts/check-theorems new file mode 100755 index 000000000..10c2365fb --- /dev/null +++ b/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 " >&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 From 02bc1dc4540c85085cde916d211dd04ef1fed904 Mon Sep 17 00:00:00 2001 From: Andreas Hatziiliou Date: Wed, 1 Apr 2026 11:44:08 -0400 Subject: [PATCH 3/3] CI: HOL-Light: ensure necessary theorems are proven Add the check-theorems script to the HOL-Light CI action. Fail the CI if any of the required proofs are not present. Signed-off-by: Andreas Hatziiliou --- .github/workflows/hol_light.yml | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/.github/workflows/hol_light.yml b/.github/workflows/hol_light.yml index 5d9356dc8..ca013e08a 100644 --- a/.github/workflows/hol_light.yml +++ b/.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