equivalence magic

formosa-crypto · Oct 7, 2024 · a01c26d · a01c26d
1 parent 95b45a8
commit a01c26d
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/proof/correctness/avx2/MLKEM_avx2_equivs_mr.ec b/proof/correctness/avx2/MLKEM_avx2_equivs_mr.ec
@@ -425,6 +425,8 @@ qed.
 
 (******* BEGIN POLYVEC_COMPRESS *****)
 
+op pre16_compress(x : W16.t) : bool =  W16.zero \sle x && x \slt W16.of_int (3329). 
+
 equiv compressequiv_1 mem  : 
  Jkem_avx2.M(Jkem_avx2.Syscall)._poly_compress_1 ~  Jkem.M(Jkem.Syscall)._i_poly_compress :
 (*
@@ -905,8 +907,8 @@ proc rewrite {2} 1891 truncate32_8E.
 proc rewrite {2} 1906 truncate32_8E.
 proc rewrite {2} 1921 truncate32_8E.
 sp 2 1. wp 98 1920 => />.
-
-bdepeq 16 4 [ "a0" ] [ "a0" ] [ "rp0" ] [ "rp0" ]. smt().
+by bdepeq 16 4 [ "a0" ] [ "a0" ] [ "rp0" ] [ "rp0" ] pre16_compress;smt().
+qed.
 
 
 (****** BEGIN POLYVEC_COMPRESS ******)