From c31f3a99518df3dfc764a0b76aef243b69e57902 Mon Sep 17 00:00:00 2001 From: mamonet Date: Mon, 20 Jan 2025 18:32:58 +0000 Subject: [PATCH] Fix verifying ind-cpa --- .../proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst | 4 ++-- libcrux-ml-kem/src/ind_cpa.rs | 4 ++-- 2 files changed, 4 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 a0e42d84a..d8e4b83fe 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 @@ -766,7 +766,7 @@ let decrypt secret_key_unpacked ciphertext -#push-options "--z3rlimit 800 --ext context_pruning --z3refresh" +#push-options "--z3rlimit 1500 --ext context_pruning --z3refresh" let compress_then_serialize_u (v_K v_OUT_LEN v_COMPRESSION_FACTOR v_BLOCK_LEN: usize) @@ -866,7 +866,7 @@ let compress_then_serialize_u #pop-options -#push-options "--z3rlimit 200" +#push-options "--z3rlimit 800 --ext context_pruning --z3refresh" let encrypt_unpacked (v_K v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_LEN v_C2_LEN v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR v_BLOCK_LEN v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE: diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs index bb893aed7..5c41ca234 100644 --- a/libcrux-ml-kem/src/ind_cpa.rs +++ b/libcrux-ml-kem/src/ind_cpa.rs @@ -621,7 +621,7 @@ pub(crate) fn serialize_unpacked_secret_key< } /// Call [`compress_then_serialize_ring_element_u`] on each ring element. -#[hax_lib::fstar::options("--z3rlimit 800 --ext context_pruning --z3refresh")] +#[hax_lib::fstar::options("--z3rlimit 1500 --ext context_pruning --z3refresh")] #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ $OUT_LEN == Spec.MLKEM.v_C1_SIZE $K /\ $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\ @@ -725,7 +725,7 @@ fn compress_then_serialize_u< /// The NIST FIPS 203 standard can be found at /// . #[allow(non_snake_case)] -#[hax_lib::fstar::options("--z3rlimit 200")] +#[hax_lib::fstar::options("--z3rlimit 800 --ext context_pruning --z3refresh")] #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ $ETA1 == Spec.MLKEM.v_ETA1 $K /\ $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\