Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ML-KEM/IND-CPA ] Fix verification #760

Merged
merged 1 commit into from
Jan 22, 2025
Merged

[ML-KEM/IND-CPA ] Fix verification #760

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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:
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/src/ind_cpa.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 /\
Expand Down Expand Up @@ -725,7 +725,7 @@ fn compress_then_serialize_u<
/// 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 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 /\
Expand Down
Loading