pending

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

Hide file tree

Showing 2 changed files with 1,524 additions and 0 deletions.
diff --git a/proof/correctness/avx2/MLKEM_Poly_avx2_proof_mr.ec b/proof/correctness/avx2/MLKEM_Poly_avx2_proof_mr.ec
@@ -25,7 +25,12 @@ 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        *)
@@ -216,6 +221,7 @@ qed.
 (*************************)
 (*************************)
 
+
 (*************************)
 (*************************)
 (* begin csubq proof     *)