Review and revise all x86_64 backend contract

willieyz · willieyz · commit 275c2b1159c5 · 2025-12-31T15:37:45.000+08:00
- This commit re-check all x86_64 contract follow the corrseponding
  HOL-Light proof

- After checking, the follwoing contract need to be remove:
  - contract and proof for `mlk_poly_mulcache_compute_avx2`

- This commit also add the symmetric note for every .ml proof:
  (* NOTE: This must be kept in sync with the CBMC specification
   * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)

Signed-off-by: willieyz &lt;willie.zhao@chelpis.com&gt;
diff --git a/dev/x86_64/src/arith_native_x86_64.h b/dev/x86_64/src/arith_native_x86_64.h
@@ -81,16 +81,7 @@ __contract__(
 
 #define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2)
 void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
-                                    const int16_t *qdata)
-/* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/x86/proofs/mlkem_mulcache_compute.ml */
-__contract__(
-  requires(memory_no_alias(out, sizeof(int16_t) * (MLKEM_N / 2)))
-  requires(memory_no_alias(in, sizeof(int16_t) * MLKEM_N))
-  requires(qdata == mlk_qdata)
-  assigns(memory_slice(out, sizeof(int16_t) * (MLKEM_N / 2)))
-  ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))
-);
+                                    const int16_t *qdata);
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
   MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)
diff --git a/mlkem/src/native/x86_64/src/arith_native_x86_64.h b/mlkem/src/native/x86_64/src/arith_native_x86_64.h
@@ -81,16 +81,7 @@ __contract__(
 
 #define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2)
 void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
-                                    const int16_t *qdata)
-/* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/x86/proofs/mlkem_mulcache_compute.ml */
-__contract__(
-  requires(memory_no_alias(out, sizeof(int16_t) * (MLKEM_N / 2)))
-  requires(memory_no_alias(in, sizeof(int16_t) * MLKEM_N))
-  requires(qdata == mlk_qdata)
-  assigns(memory_slice(out, sizeof(int16_t) * (MLKEM_N / 2)))
-  ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))
-);
+                                    const int16_t *qdata);
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
   MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)
diff --git a/proofs/cbmc/poly_mulcache_compute_native_x86_64/Makefile b/proofs/cbmc/poly_mulcache_compute_native_x86_64/Makefile
diff --git a/proofs/cbmc/poly_mulcache_compute_native_x86_64/poly_mulcache_compute_native_x86_64_harness.c b/proofs/cbmc/poly_mulcache_compute_native_x86_64/poly_mulcache_compute_native_x86_64_harness.c
diff --git a/proofs/hol_light/x86/proofs/mlkem_frombytes.ml b/proofs/hol_light/x86/proofs/mlkem_frombytes.ml
@@ -444,6 +444,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_intt.ml b/proofs/hol_light/x86/proofs/mlkem_intt.ml
@@ -1194,6 +1194,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_ntt.ml b/proofs/hol_light/x86/proofs/mlkem_ntt.ml
@@ -1210,6 +1210,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml b/proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml
@@ -1080,6 +1080,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml b/proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml
@@ -1550,6 +1550,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml b/proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml
@@ -2026,6 +2026,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_reduce.ml b/proofs/hol_light/x86/proofs/mlkem_reduce.ml
@@ -419,6 +419,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_rej_uniform.ml b/proofs/hol_light/x86/proofs/mlkem_rej_uniform.ml
@@ -779,6 +779,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_tobytes.ml b/proofs/hol_light/x86/proofs/mlkem_tobytes.ml
@@ -402,6 +402,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 /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_tomont.ml b/proofs/hol_light/x86/proofs/mlkem_tomont.ml
@@ -309,6 +309,9 @@ let MLKEM_TOMONT_NOIBT_SUBROUTINE_CORRECT = prove(
               MAYCHANGE [memory :> bytes(a,512)])`, 
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_tomont_tmc MLKEM_TOMONT_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_TOMONT_SUBROUTINE_CORRECT = prove(
   `!a x pc stackpointer returnaddress.
         aligned 32 a /\
diff --git a/proofs/hol_light/x86/proofs/mlkem_unpack.ml b/proofs/hol_light/x86/proofs/mlkem_unpack.ml
@@ -382,6 +382,9 @@ let MLKEM_UNPACK_NOIBT_SUBROUTINE_CORRECT = prove(
               MAYCHANGE [memory :> bytes(a, 512)])`, 
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_unpack_tmc MLKEM_UNPACK_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_UNPACK_SUBROUTINE_CORRECT = prove(
     `!a (l:int16 list) pc.
         aligned 32 a /\
