everything except ind-cpa verified

cryspen · Jan 18, 2025 · 9d8d421 · 9d8d421
1 parent 29b3134
commit 9d8d421
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
@@ -440,7 +440,7 @@ let sample_vector_cbd_then_ntt_helper_2
       (Spec.MLKEM.sample_vector_cbd_then_ntt #v_K
         (Seq.slice prf_input 0 32) (sz (v domain_separator)))
 
-#push-options "--max_fuel 25 --z3rlimit 2500 --ext context_pruning --z3refresh --split_queries always"
+#push-options "--max_fuel 25 --z3rlimit 2800 --ext context_pruning --z3refresh --split_queries always"
 
 let sample_vector_cbd_then_ntt
       (v_K v_ETA v_ETA_RANDOMNESS_SIZE: usize)

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Makefile b/libcrux-ml-kem/proofs/fstar/extraction/Makefile
@@ -1,7 +1,8 @@
 SLOW_MODULES += Libcrux_ml_kem.Vector.Portable.Serialize.fst \
                 Libcrux_ml_kem.Vector.Rej_sample_table.fsti
 
-ADMIT_MODULES = Libcrux_ml_kem.Vector.Neon.Arithmetic.fst \
+ADMIT_MODULES = Libcrux_ml_kem.Ind_cpa.fst \
+              Libcrux_ml_kem.Vector.Neon.Arithmetic.fst \
               Libcrux_ml_kem.Vector.Neon.Compress.fst \
               Libcrux_ml_kem.Vector.Neon.fsti \
               Libcrux_ml_kem.Vector.Neon.fst \