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

Jump to bottom

Make generic ind_cpa module panic-free #578

Closed
wants to merge 1 commit into from
Closed

Make generic ind_cpa module panic-free #578

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
20 changes: 8 additions & 12 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 @@ -261,8 +261,6 @@ let compress_then_serialize_u
let hax_temp_output:Prims.unit = result in
out

#push-options "--admit_smt_queries true"

let deserialize_then_decompress_u
(v_K v_CIPHERTEXT_SIZE v_U_COMPRESSION_FACTOR: usize)
(#v_Vector: Type0)
Expand Down Expand Up @@ -321,9 +319,9 @@ let deserialize_then_decompress_u
in
u_as_ntt)
in
u_as_ntt

#pop-options
let result:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K = u_as_ntt in
let _:Prims.unit = admit () (* Panic freedom *) in
result

let deserialize_secret_key
(v_K: usize)
Expand Down Expand Up @@ -374,7 +372,7 @@ let deserialize_secret_key
let _:Prims.unit = admit () (* Panic freedom *) in
result

#push-options "--admit_smt_queries true"
#push-options "--z3rlimit 200"

let serialize_secret_key
(v_K v_OUT_LEN: usize)
Expand Down Expand Up @@ -431,7 +429,9 @@ let serialize_secret_key
<:
t_Array u8 v_OUT_LEN)
in
out
let result:t_Array u8 v_OUT_LEN = out in
let _:Prims.unit = admit () (* Panic freedom *) in
result

#pop-options

Expand Down Expand Up @@ -486,8 +486,6 @@ let serialize_public_key
let _:Prims.unit = admit () (* Panic freedom *) in
result

#push-options "--admit_smt_queries true"

let decrypt_unpacked
(v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
usize)
Expand Down Expand Up @@ -519,8 +517,6 @@ let decrypt_unpacked
in
Libcrux_ml_kem.Serialize.compress_then_serialize_message #v_Vector message

#pop-options

let decrypt
(v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
usize)
Expand Down Expand Up @@ -552,7 +548,7 @@ let decrypt
let _:Prims.unit = admit () (* Panic freedom *) in
result

#push-options "--admit_smt_queries true"
#push-options "--z3rlimit 200"

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
11 changes: 7 additions & 4 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,8 @@ val decrypt_unpacked
(requires
Spec.MLKEM.is_rank v_K /\ v_CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K /\
v_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\
v v_VECTOR_U_ENCODED_SIZE <= v v_CIPHERTEXT_SIZE)
v_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
v_VECTOR_U_ENCODED_SIZE == Spec.MLKEM.v_C1_SIZE v_K)
(fun _ -> Prims.l_True)

val decrypt
Expand Down Expand Up @@ -241,10 +242,12 @@ val encrypt_unpacked
v_ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE v_K /\
v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\
v_ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE v_K /\
v_C1_LEN == Spec.MLKEM.v_C1_SIZE v_K /\
v_C1_LEN == Spec.MLKEM.v_C1_SIZE v_K /\ v_C2_LEN == Spec.MLKEM.v_C2_SIZE v_K /\
v_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\
v_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\ v v_C1_LEN <= v v_CIPHERTEXT_SIZE /\
v (Core.Slice.impl__len #u8 randomness) <= 33)
v_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
v_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\
v_CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K /\
length randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE)
(fun _ -> Prims.l_True)

val encrypt
Expand Down
33 changes: 18 additions & 15 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 @@ -68,7 +68,8 @@ pub(crate) fn serialize_public_key<

/// Call [`serialize_uncompressed_ring_element`] for each ring element.
#[inline(always)]
#[hax_lib::fstar::verification_status(lax)]
#[hax_lib::fstar::options("--z3rlimit 200")]
#[hax_lib::fstar::verification_status(panic_free)]
#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
$OUT_LEN == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K"))]
#[hax_lib::ensures(|res|
Expand Down Expand Up @@ -365,17 +366,19 @@ 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::verification_status(lax)]
#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank v_K /\\
v_ETA1 == Spec.MLKEM.v_ETA1 v_K /\\
v_ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE v_K /\\
v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\\
v_ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE v_K /\\
v_C1_LEN == Spec.MLKEM.v_C1_SIZE v_K /\\
v_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\\
v_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\\
v v_C1_LEN <= v v_CIPHERTEXT_SIZE /\\
v (${randomness.len()}) <= 33"))]
#[hax_lib::fstar::options("--z3rlimit 200")]
#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
$ETA1 == Spec.MLKEM.v_ETA1 $K /\\
$ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\
$ETA2 == Spec.MLKEM.v_ETA2 $K /\\
$ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\\
$C1_LEN == Spec.MLKEM.v_C1_SIZE $K /\\
$C2_LEN == Spec.MLKEM.v_C2_SIZE $K /\\
$U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\
$V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\
$BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\
$CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
length $randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE"))]
pub(crate) fn encrypt_unpacked<
const K: usize,
const CIPHERTEXT_SIZE: usize,
Expand Down Expand Up @@ -529,7 +532,7 @@ pub(crate) fn encrypt<
/// Call [`deserialize_then_decompress_ring_element_u`] on each ring element
/// in the `ciphertext`.
#[inline(always)]
#[hax_lib::fstar::verification_status(lax)]
#[hax_lib::fstar::verification_status(panic_free)]
#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
$CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
$U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K"))]
Expand Down Expand Up @@ -603,11 +606,11 @@ fn deserialize_secret_key<const K: usize, Vector: Operations>(
/// The NIST FIPS 203 standard can be found at
/// <https://csrc.nist.gov/pubs/fips/203/ipd>.
#[allow(non_snake_case)]
#[hax_lib::fstar::verification_status(lax)]
#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
$CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
$U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\
v $VECTOR_U_ENCODED_SIZE <= v $CIPHERTEXT_SIZE"))]
$V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\
$VECTOR_U_ENCODED_SIZE == Spec.MLKEM.v_C1_SIZE $K"))]
pub(crate) fn decrypt_unpacked<
const K: usize,
const CIPHERTEXT_SIZE: usize,
Expand Down
Loading