lint: verify that all expected theorems are present

We add a check to the linting 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 /\
@@ -3119,6 +3119,6 @@ let MLKEM_REJ_UNIFORM_SUBROUTINE_MEMSAFE = time prove
     REWRITE_CONV[wordlist_from_memory] in
   CONV_TAC TWEAK_CONV THEN
   ARM_ADD_RETURN_STACK_TAC MLKEM_REJ_UNIFORM_EXEC
-   (CONV_RULE TWEAK_CONV MLKEM_REJ_UNIFORM_MEMSAFE)
+   (CONV_RULE TWEAK_CONV MLKEM_REJ_UNIFORM_SAFE)
     `[]:int64 list` 576 THEN
   DISCHARGE_MEMSAFE_TAC);;

proofs/hol_light/x86_64/proofs/mlkem_intt.ml

@@ -1206,7 +1206,7 @@ let MLKEM_INTT_CORRECT = prove
     CONV_TAC INT_REDUCE_CONV]))
 );;
 
-let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT  = prove
+let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT = prove
   (`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 a /\
     aligned 32 zetas /\
@@ -1241,7 +1241,7 @@ let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT  = prove
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_INTT_SUBROUTINE_CORRECT  = prove
+let MLKEM_INTT_SUBROUTINE_CORRECT = prove
   (`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 a /\
     aligned 32 zetas /\

proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml

@@ -259,7 +259,7 @@ let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(
     CONV_TAC INT_REDUCE_CONV])
 );;
 
-let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT  = prove(
+let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT = prove(
  `!r a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 r /\
     aligned 32 a /\

proofs/hol_light/x86_64/proofs/mlkem_ntt.ml

@@ -1214,7 +1214,7 @@ let MLKEM_NTT_CORRECT = prove
      CONV_TAC INT_REDUCE_CONV]))
 );;
 
-let MLKEM_NTT_NOIBT_SUBROUTINE_CORRECT  = prove
+let MLKEM_NTT_NOIBT_SUBROUTINE_CORRECT = prove
   (`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 a /\
     aligned 32 zetas /\
@@ -1250,7 +1250,7 @@ let MLKEM_NTT_NOIBT_SUBROUTINE_CORRECT  = prove
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_NTT_SUBROUTINE_CORRECT  = prove
+let MLKEM_NTT_SUBROUTINE_CORRECT = prove
   (`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 a /\
     aligned 32 zetas /\

scripts/lint

@@ -295,6 +295,51 @@ gh_group_start "Check contracts"
 check-contracts
 gh_group_end
 
+check-theorems()
+{
+  local success=true
+  for arch in aarch64 x86_64; do
+    local proofs_dir="$ROOT/proofs/hol_light/$arch/proofs"
+    local proofs
+    proofs=$("$ROOT/proofs/hol_light/$arch/list_proofs.sh")
+
+    for routine in $proofs; do
+      local suffixes=("CORRECT" "SAFE" "SUBROUTINE_SAFE")
+      if [[ $arch == "x86_64" && ${routine} == "mlkem_rej_uniform" ]]; then
+        suffixes=("CORRECT")
+      elif [[ $arch == "x86_64" ]]; then
+        suffixes+=("SUBROUTINE_CORRECT" "NOIBT_SUBROUTINE_CORRECT" "NOIBT_SUBROUTINE_SAFE")
+      fi
+
+      for sfx in "${suffixes[@]}"; do
+        if ! grep -qE "_${sfx} = (time )?prove" "$proofs_dir/${routine}.ml"; then
+          gh_error "${routine}" "" "Missing theorem" "${routine}_${sfx} not found in ${routine}.ml for arch ${arch}"
+          success=false
+        fi
+      done
+
+      # Check for CHEAT_TAC usage (bypasses actual proving)
+      if grep -q "CHEAT_TAC" "$proofs_dir/${routine}.ml"; then
+        gh_error "${routine}" "" "CHEAT_TAC detected" "${routine}.ml uses CHEAT_TAC"
+        success=false
+      fi
+    done
+  done
+
+  if $success; then
+    info "Check HOL-Light theorems"
+    gh_summary_success "Check HOL-Light theorems"
+  else
+    error "Check HOL-Light theorems"
+    SUCCESS=false
+    gh_summary_failure "Check HOL-Light theorems"
+  fi
+}
+
+gh_group_start "Check HOL-Light theorems"
+check-theorems
+gh_group_end
+
 if ! $SUCCESS; then
   if $IN_GITHUB_CONTEXT; then
     printf "%b%s%b\n" "${RED}" "The following checks failed, expand each for more details." "${NORMAL}"