From 7ed909f8033142d720fcbfe309243b9fa52d181d Mon Sep 17 00:00:00 2001 From: mamonet Date: Mon, 4 Nov 2024 07:02:48 +0000 Subject: [PATCH] Remove Ind_cca.Unpacked module from ADMIT_MODULES --- .../proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst | 8 +++++++- libcrux-ml-kem/proofs/fstar/extraction/Makefile | 3 +-- libcrux-ml-kem/src/ind_cpa.rs | 4 +++- 3 files changed, 11 insertions(+), 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 index aa3f657ef..29146d11c 100644 --- 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 index b7a4485d1..b054ead79 100644 --- 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 index 2db713036..4891caff8 100644 --- 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 /// . #[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 ==>