HOL-Light: Run NTT and invNTT proof in CI

Signed-off-by: Hanno Becker <[email protected]>

.github/workflows/ci.yml

@@ -364,21 +364,6 @@ jobs:
           acvp: false
           nix-shell: ${{ matrix.compiler.shell }}
           cflags: "-std=c17"
-  # The purpose of this job is to test non-default yet valid configurations
-  hol_light_proofs:
-    name: hol-light proofs
-    runs-on: pqcp-arm64
-    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - uses: ./.github/actions/setup-shell
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          nix-shell: 'hol_light'
-          script: |
-            make -C proofs/hol_light/arm p256/bignum_montmul_p256.correct
-
   config_variations:
     name: Non-standard configurations
     needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]

.github/workflows/hol_light.yml

@@ -0,0 +1,37 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: HOL-Light
+permissions:
+  contents: read
+on:
+  push:
+    branches: ["main"]
+    # Only run upon changes to AArch64 NTT or invNTT
+    paths:
+     - 'proofs/hol_light/arm/**/*.S'
+  pull_request:
+    branches: ["main"]
+    paths:
+      # Only run upon changes to AArch64 NTT or invNTT
+      - 'proofs/hol_light/arm/**/*.S'
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  hol_light_proofs:
+    strategy:
+      matrix:
+        proof: [mlkem_ntt,mlkem_intt]
+    name: HOL Light proof for ${{ matrix.proof }}.S
+    runs-on: pqcp-arm64
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            make -C proofs/hol_light/arm mlkem/${{ matrix.proof }}.correct