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 <andreas.hatziiliou@savoirfairelinux.com>

Author: L-series

proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml

@@ -1755,7 +1755,7 @@ let STRIP_EXISTS_ASSUM_TAC =
 (* The main memory safety theorem.                                           *)
 (* ========================================================================= *)
 
-let MLKEM_REJ_UNIFORM_MEMSAFE = prove
+let MLKEM_REJ_UNIFORM_SAFE = prove
  (`!res buf buflen table (inlist:(12 word)list) pc e stackpointer.
       24 divides val buflen /\
       8 * val buflen = 12 * LENGTH inlist /\
@@ -3086,7 +3086,7 @@ let MLKEM_REJ_UNIFORM_MEMSAFE = prove
 (* Memory safety of the subroutine version.                                  *)
 (* ------------------------------------------------------------------------- *)
 
-let MLKEM_REJ_UNIFORM_SUBROUTINE_MEMSAFE = time prove
+let MLKEM_REJ_UNIFORM_SUBROUTINE_SAFE = time prove
  (`!res buf buflen table (inlist:(12 word)list) pc e stackpointer returnaddress.
       24 divides val buflen /\
       8 * val buflen = 12 * LENGTH inlist /\

scripts/check-theorems

@@ -0,0 +1,48 @@
+#!/usr/bin/env bash
+# Copyright (c) The mlkem-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")
+
+  # mlkem_rej_uniform on x86_64 only has a functional correctness proof
+  [[ $ARCH == "x86_64" && $routine == "mlkem_rej_uniform" ]] && suffixes=("CORRECT")
+
+  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