Going for equivs

formosa-crypto · Sep 20, 2024 · a6f35b0 · a6f35b0
1 parent 1bd0921
commit a6f35b0
Show file tree

Hide file tree

Showing 2 changed files with 404 additions and 87 deletions.
diff --git a/proof/correctness/avx2/MLKEM_Poly_avx2_proof_mr.ec b/proof/correctness/avx2/MLKEM_Poly_avx2_proof_mr.ec
@@ -25,12 +25,6 @@ import BitEncoding.BitChunking.
 
 timeout 1.
 
-require import AllCore List.
-from Jasmin require import JModel.
-import BitEncoding.BitChunking.
-
-require import MLKEMFCLib.
-require import Array8 Array256 WArray512 Array16 WArray32 Array128 WArray128.
 (*************************)
 (*************************)
 (* BEGIN BINDINGS        *)