updated verification status

cryspen · Dec 11, 2024 · ce63901 · ce63901
1 parent 2f140ae
commit ce63901
Showing 1 changed file with 10 additions and 3 deletions.
diff --git a/libcrux-ml-kem/proofs/verification_status.md b/libcrux-ml-kem/proofs/verification_status.md
@@ -11,9 +11,9 @@ This file keeps track of the current verification status of the modules in the M
 * ind_cca/instaniations/avx2: Verified
 * ind_cca/multiplexing: Verified
 
-* invert_ntt: Panic Free, Not linked to spec
-* ntt: Panic Free, Not linked to spec
-* mlkem*: Panic Free, Not linked to spec
+* invert_ntt: Panic Free
+* ntt: Panic Free
+* mlkem*: Panic Free
 
 * matrix: Needs proofs
 * sampling: Needs proofs
@@ -33,3 +33,10 @@ This file keeps track of the current verification status of the modules in the M
 * compress: Panic Free
 * ntt: Needs proofs
 * sampling: Needs proofs
+
+## Neon modules
+* arithmetic: Not verified
+* serialize: Not verified
+* compress: Not verified
+* ntt: Needs Not verified
+* sampling: Not verified