progress

formosa-crypto · Feb 18, 2025 · e5a489b · e5a489b
1 parent 840aee3
commit e5a489b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec b/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec
@@ -677,7 +677,7 @@ phoare gen_matrix_buf_rejection_ph _pol _ctr _buf _buf_offset:
    let l = take (256-to_uint _ctr) (rejection16 (buf_subl _buf (to_uint _buf_offset) 504))
    in plist res.`1 (to_uint _ctr + size l)
       = plist _pol (to_uint _ctr) ++ l
-      /\ res.`2 = W64.of_int (to_uint _ctr + size l)
+      /\ to_uint _ctr + size l = min 256 (to_uint res.`2)
  ] = 1%r.
 proof.
 by conseq gen_matrix_buf_rejection_ll (gen_matrix_buf_rejection_h _pol _ctr _buf _buf_offset).