HOL-Light: Move notes on specification matching CBMC to actual spec

Signed-off-by: Matthias J. Kannwischer <[email protected]>

Author: mkannwischer

proofs/hol_light/arm/proofs/mlkem_intt.ml

@@ -482,8 +482,6 @@ let intt_constants = define
 (* Correctness proof.                                                        *)
 (* ------------------------------------------------------------------------- *)
 
-(* NOTE: This must be kept in sync with the CBMC specification
- * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
 
 let MLKEM_INTT_CORRECT = prove
  (`!a z_12345 z_67 x pc.
@@ -578,6 +576,9 @@ let MLKEM_INTT_CORRECT = prove
 
 (*** Subroutine form, somewhat messy elaboration of the usual wrapper ***)
 
+(* NOTE: This must be kept in sync with the CBMC specification
+ * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
+
 let MLKEM_INTT_SUBROUTINE_CORRECT = prove
  (`!a z_12345 z_67 x pc stackpointer returnaddress.
       aligned 16 stackpointer /\

proofs/hol_light/arm/proofs/mlkem_ntt.ml

@@ -357,9 +357,6 @@ let ntt_constants = define
 (* Correctness proof.                                                        *)
 (* ------------------------------------------------------------------------- *)
 
-(* NOTE: This must be kept in sync with the CBMC specification
- * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
-
 let MLKEM_NTT_CORRECT = prove
  (`!a z_12345 z_67 x pc.
       ALL (nonoverlapping (a,512))
@@ -459,6 +456,9 @@ let MLKEM_NTT_CORRECT = prove
 
 (*** Subroutine form, somewhat messy elaboration of the usual wrapper ***)
 
+(* NOTE: This must be kept in sync with the CBMC specification
+ * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
+
 let MLKEM_NTT_SUBROUTINE_CORRECT = prove
  (`!a z_12345 z_67 x pc stackpointer returnaddress.
       aligned 16 stackpointer /\

proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml

@@ -118,9 +118,6 @@ let overall_lemma = prove
   REWRITE_TAC[MATCH_MP lemma_rem (CONGBOUND_RULE `barred x`)] THEN
   BITBLAST_TAC);;
 
-(* NOTE: This must be kept in sync with the CBMC specification
- * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
-
 let MLKEM_POLY_REDUCE_CORRECT = prove
  (`!a x pc.
         nonoverlapping (word pc,0x124) (a,512)
@@ -183,6 +180,9 @@ let MLKEM_POLY_REDUCE_CORRECT = prove
   ASM_REWRITE_TAC[WORD_ADD_0] THEN DISCARD_STATE_TAC "s276" THEN
   REWRITE_TAC[GSYM barred; overall_lemma]);;
 
+(* NOTE: This must be kept in sync with the CBMC specification
+ * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
+
 let MLKEM_POLY_REDUCE_SUBROUTINE_CORRECT = prove
  (`!a x pc returnaddress.
         nonoverlapping (word pc,0x124) (a,512)

proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml

@@ -168,9 +168,6 @@ let lemma =
   CONV_RULE(EXPAND_CASES_CONV THENC
             DEPTH_CONV (NUM_RED_CONV ORELSEC EL_CONV)) th';;
 
-(* NOTE: This must be kept in sync with the CBMC specification
- * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
-
 let MLKEM_POLY_TOBYTES_CORRECT = prove
  (`!r a (l:int16 list) pc.
         ALL (nonoverlapping (r,384)) [(word pc,0x158); (a,512)]
@@ -247,6 +244,9 @@ let MLKEM_POLY_TOBYTES_CORRECT = prove
   REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN
   ABBREV_TAC `twae = &2:real` THEN REAL_ARITH_TAC);;
 
+(* NOTE: This must be kept in sync with the CBMC specification
+ * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
+
 let MLKEM_POLY_TOBYTES_SUBROUTINE_CORRECT = prove
  (`!r a (l:int16 list) pc returnaddress.
         ALL (nonoverlapping (r,384)) [(word pc,0x158); (a,512)]

proofs/hol_light/arm/proofs/mlkem_rej_uniform.ml

@@ -455,9 +455,6 @@ let DIMINDEX_384 = DIMINDEX_CONV `dimindex(:384)`;;
 (* Now the actual proof.                                                     *)
 (* ------------------------------------------------------------------------- *)
 
-(* NOTE: This must be kept in sync with the CBMC specification
- * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
-
 let MLKEM_REJ_UNIFORM_CORRECT = prove
  (`!res buf buflen table (inlist:(12 word)list) pc stackpointer.
         24 divides val buflen /\
@@ -1604,6 +1601,9 @@ let MLKEM_REJ_UNIFORM_CORRECT = prove
   SUBST1_TAC(SYM(ASSUME `curlen + len0:num = curlen1`)) THEN
   CONV_TAC WORD_RULE);;
 
+(* NOTE: This must be kept in sync with the CBMC specification
+ * in mlkem/native/aarch64/src/arith_native_aarch64.h *)
+
 let MLKEM_REJ_UNIFORM_SUBROUTINE_CORRECT = prove
  (`!res buf buflen table (inlist:(12 word)list) pc stackpointer returnaddress.
         24 divides val buflen /\