Remove Ind_cca.Unpacked module from ADMIT_MODULES

cryspen · Nov 4, 2024 · 7ed909f · 7ed909f
1 parent 1b88555
commit 7ed909f
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 4 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
@@ -382,6 +382,8 @@ let sample_vector_cbd_then_ntt_out
   <:
   (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8)
 
+#push-options "--z3rlimit 500 --ext context_pruning --z3refresh"
+
 let generate_keypair_unpacked
       (v_K v_ETA1 v_ETA1_RANDOMNESS_SIZE: usize)
       (#v_Vector #v_Hasher #v_Scheme: Type0)
@@ -496,12 +498,14 @@ let generate_keypair_unpacked
     Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector
   in
   let _:Prims.unit =
-    let ((t_as_ntt, seed_for_A), secret_as_ntt), valid =
+    let (((t_as_ntt, seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid =
       Spec.MLKEM.ind_cpa_generate_keypair_unpacked v_K key_generation_seed
     in
     assert (valid ==>
         ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key.f_t_as_ntt) ==
           t_as_ntt) /\ (public_key.f_seed_for_A == seed_for_A) /\
+        (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key.f_A == matrix_A_as_ntt
+        ) /\
         ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector private_key.f_secret_as_ntt) ==
           secret_as_ntt));
     assert ((forall (i: nat).
@@ -520,6 +524,8 @@ let generate_keypair_unpacked
   (Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPrivateKeyUnpacked v_K v_Vector &
     Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector)
 
+#pop-options
+
 #push-options "--z3rlimit 200 --ext context_pruning --z3refresh"
 
 let compress_then_serialize_u

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Makefile b/libcrux-ml-kem/proofs/fstar/extraction/Makefile
@@ -1,7 +1,6 @@
 SLOW_MODULES += Libcrux_ml_kem.Vector.Portable.Serialize.fst
 
-ADMIT_MODULES = Libcrux_ml_kem.Ind_cca.Unpacked.fst \
-              Libcrux_ml_kem.Vector.Avx2.fsti \
+ADMIT_MODULES = Libcrux_ml_kem.Vector.Avx2.fsti \
               Libcrux_ml_kem.Vector.Avx2.fst \
               Libcrux_ml_kem.Vector.Avx2.Ntt.fst \
               Libcrux_ml_kem.Vector.Avx2.Sampling.fst \

diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs
@@ -357,6 +357,7 @@ fn sample_vector_cbd_then_ntt_out<
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 #[allow(non_snake_case)]
+#[hax_lib::fstar::options("--z3rlimit 500 --ext context_pruning --z3refresh")]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\
     $ETA1 == Spec.MLKEM.v_ETA1 $K /\\
@@ -418,11 +419,12 @@ pub(crate) fn generate_keypair_unpacked<
 
     public_key.seed_for_A = seed_for_A.try_into().unwrap();
 
-    hax_lib::fstar!("let ((t_as_ntt, seed_for_A), secret_as_ntt), valid =
+    hax_lib::fstar!("let (((t_as_ntt,seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid =
         Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K $key_generation_seed in
         assert (valid ==>
             ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector public_key.f_t_as_ntt) ==
               t_as_ntt) /\\ (public_key.f_seed_for_A == seed_for_A) /\\
+            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector public_key.f_A == matrix_A_as_ntt) /\\
             ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector private_key.f_secret_as_ntt) ==
               secret_as_ntt));
         assert ((forall (i: nat). i < v $K ==>