add changes

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

Author: willieyz

dev/x86_64/src/arith_native_x86_64.h

@@ -131,6 +131,9 @@ __contract__(
 
 #define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2)
 void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a)
+/* This must be kept in sync with the HOL-Light specification in
+ * proofs/hol_light/x86/proofs/mlkem_tobytes.ml.
+ */
 __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
@@ -140,6 +143,9 @@ __contract__(
 
 #define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2)
 void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a)
+/* This must be kept in sync with the HOL-Light specification in
+ * proofs/hol_light/x86/proofs/mlkem_frombytes.ml.
+ */
 __contract__(
   requires(memory_no_alias(a, MLKEM_POLYBYTES))
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -149,6 +155,9 @@ __contract__(
 
 #define mlk_tomont_avx2 MLK_NAMESPACE(tomont_avx2)
 void mlk_tomont_avx2(int16_t *r, const int16_t *qdata)
+/* This must be kept in sync with the HOL-Light specification in
+ * proofs/hol_light/x86/proofs/mlkem_tomont.ml.
+ */
 __contract__(
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
   requires(qdata == mlk_qdata)

mlkem/src/native/x86_64/src/arith_native_x86_64.h

@@ -131,6 +131,9 @@ __contract__(
 
 #define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2)
 void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a)
+/* This must be kept in sync with the HOL-Light specification in
+ * proofs/hol_light/x86/proofs/mlkem_tobytes.ml.
+ */
 __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
@@ -140,6 +143,9 @@ __contract__(
 
 #define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2)
 void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a)
+/* This must be kept in sync with the HOL-Light specification in
+ * proofs/hol_light/x86/proofs/mlkem_frombytes.ml.
+ */
 __contract__(
   requires(memory_no_alias(a, MLKEM_POLYBYTES))
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -149,6 +155,9 @@ __contract__(
 
 #define mlk_tomont_avx2 MLK_NAMESPACE(tomont_avx2)
 void mlk_tomont_avx2(int16_t *r, const int16_t *qdata)
+/* This must be kept in sync with the HOL-Light specification in
+ * proofs/hol_light/x86/proofs/mlkem_tomont.ml.
+ */
 __contract__(
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
   requires(qdata == mlk_qdata)