add symmetric note to all .ML HOL-LIGHT proofs

Signed-off-by: willieyz <willie.zhao@chelpis.com>

Author: willieyz

proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml

@@ -446,6 +446,9 @@ let MLKEM_FROMBYTES_NOIBT_SUBROUTINE_CORRECT = prove(
               MAYCHANGE [RSP] ,, MAYCHANGE [memory :> bytes(r, 512)])`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_frombytes_tmc MLKEM_FROMBYTES_CORRECT);;
 
+(* 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_FROMBYTES_SUBROUTINE_CORRECT = prove(
     `!r a (l:(12 word) list) pc.
         aligned 32 a /\

proofs/hol_light/x86_64/proofs/mlkem_intt.ml

@@ -1213,6 +1213,9 @@ let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT  = prove
   CONV_TAC TWEAK_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_intt_tmc (CONV_RULE TWEAK_CONV MLKEM_INTT_CORRECT));;
 
+(* 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
   (`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 a /\

proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml

@@ -267,6 +267,9 @@ let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT  = prove(
   CONV_TAC TWEAK_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_mulcache_compute_tmc (CONV_RULE TWEAK_CONV MLKEM_MULCACHE_COMPUTE_CORRECT));;
 
+(* 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_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove(
  `!r a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 r /\

proofs/hol_light/x86_64/proofs/mlkem_ntt.ml

@@ -1222,6 +1222,9 @@ let MLKEM_NTT_NOIBT_SUBROUTINE_CORRECT  = prove
   CONV_TAC TWEAK_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_ntt_tmc (CONV_RULE TWEAK_CONV MLKEM_NTT_CORRECT));;
 
+(* 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
   (`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 a /\

proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml

@@ -1081,6 +1081,9 @@ let MLKEM_BASEMUL_K2_NOIBT_SUBROUTINE_CORRECT = prove(
                MAYCHANGE [memory :> bytes(dst, 512)])`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k2_tmc MLKEM_BASEMUL_K2_CORRECT);;
 
+(* 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_BASEMUL_K2_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 pc stackpointer returnaddress.
         aligned 32 src1 /\

proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml

@@ -1551,6 +1551,9 @@ let MLKEM_BASEMUL_K3_NOIBT_SUBROUTINE_CORRECT = prove(
                MAYCHANGE [memory :> bytes(dst, 512)])`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k3_tmc MLKEM_BASEMUL_K3_CORRECT);;
 
+(* 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_BASEMUL_K3_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 pc stackpointer returnaddress.
         aligned 32 src1 /\

proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml

@@ -2028,6 +2028,9 @@ let MLKEM_BASEMUL_K4_NOIBT_SUBROUTINE_CORRECT = prove(
                MAYCHANGE [memory :> bytes(dst, 512)])`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k4_tmc MLKEM_BASEMUL_K4_CORRECT);;
 
+(* 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_BASEMUL_K4_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 a3 b3 c3 d3 dz3 pc stackpointer returnaddress.
         aligned 32 src1 /\

proofs/hol_light/x86_64/proofs/mlkem_reduce.ml

@@ -421,6 +421,9 @@ let MLKEM_REDUCE_NOIBT_SUBROUTINE_CORRECT = prove
                MAYCHANGE [memory :> bytes(a, 512)])`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_reduce_tmc MLKEM_REDUCE_CORRECT);;
 
+(* 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_REDUCE_SUBROUTINE_CORRECT = prove
  (`!a x pc stackpointer returnaddress.
         aligned 32 a /\

proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml

@@ -781,6 +781,9 @@ let MLKEM_REJ_UNIFORM_NOIBT_SUBROUTINE_CORRECT = prove
   X86_PROMOTE_RETURN_STACK_TAC mlkem_rej_uniform_tmc
     (CONV_RULE TWEAK_CONV MLKEM_REJ_UNIFORM_CORRECT) `[]` 528);;
 
+(* 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_REJ_UNIFORM_SUBROUTINE_CORRECT = prove
  (`!res buf buflen table (inlist:(12 word)list) pc stackpointer returnaddress.
       12 divides val buflen /\

proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml

@@ -404,6 +404,9 @@ let MLKEM_TOBYTES_NOIBT_SUBROUTINE_CORRECT = prove
                MAYCHANGE [memory :> bytes(r, 384)])`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_tobytes_tmc MLKEM_TOBYTES_CORRECT);;
 
+(* 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_TOBYTES_SUBROUTINE_CORRECT = prove
 (`!r a (l:int16 list) pc.
         aligned 32 a /\