From 69a27e493369bbddc489b454aa3149a018376539 Mon Sep 17 00:00:00 2001 From: mamonet Date: Wed, 13 Nov 2024 15:04:51 +0000 Subject: [PATCH] Reomve Libcrux_ml_kem.Vector.Portable from ADMIT_MODULES --- .../Libcrux_ml_kem.Ind_cca.Unpacked.fst | 6 +++++- .../extraction/Libcrux_ml_kem.Serialize.fst | 8 ++++++++ .../extraction/Libcrux_ml_kem.Vector.Avx2.fsti | 8 ++++++-- ...Libcrux_ml_kem.Vector.Portable.Arithmetic.fst | 4 ++++ .../Libcrux_ml_kem.Vector.Portable.fsti | 16 ++++++++++------ .../extraction/Libcrux_ml_kem.Vector.Traits.fsti | 10 +++++++--- libcrux-ml-kem/proofs/fstar/extraction/Makefile | 2 -- libcrux-ml-kem/src/ind_cca.rs | 3 ++- libcrux-ml-kem/src/serialize.rs | 2 ++ libcrux-ml-kem/src/vector/avx2.rs | 8 ++++++-- libcrux-ml-kem/src/vector/portable.rs | 12 ++++++++---- libcrux-ml-kem/src/vector/portable/arithmetic.rs | 1 + libcrux-ml-kem/src/vector/traits.rs | 12 ++++++++---- 13 files changed, 67 insertions(+), 25 deletions(-) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst index 69e3ecca8..8cef7b507 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst @@ -45,6 +45,8 @@ let impl_4__serialized_private_key <: Rust_primitives.Hax.t_Never) +#push-options "--z3rlimit 200" + let transpose_a (v_K: usize) (#v_Vector: Type0) @@ -138,6 +140,8 @@ let transpose_a in v_A +#pop-options + let impl_4__new (v_K: usize) (#v_Vector: Type0) @@ -421,7 +425,7 @@ let impl_4__serialized_public_key v_PUBLIC_KEY_SIZE self.f_public_key -#push-options "--z3rlimit 200 --ext context_pruning" +#push-options "--z3rlimit 800 --ext context_pruning" let generate_keypair (v_K v_CPA_PRIVATE_KEY_SIZE v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_BYTES_PER_RING_ELEMENT v_ETA1 v_ETA1_RANDOMNESS_SIZE: diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst index be626ddec..d76da59ca 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst @@ -21,6 +21,8 @@ let to_unsigned_field_modulus let _:Prims.unit = admit () (* Panic freedom *) in result +#push-options "--admit_smt_queries true" + let deserialize_then_decompress_11_ (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -72,6 +74,8 @@ let deserialize_then_decompress_11_ in re +#pop-options + let deserialize_then_decompress_4_ (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -123,6 +127,8 @@ let deserialize_then_decompress_4_ in re +#push-options "--admit_smt_queries true" + let deserialize_then_decompress_5_ (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -186,6 +192,8 @@ let deserialize_then_decompress_5_ in re +#pop-options + let deserialize_then_decompress_message (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti index b2bed5eb4..72fb64e9e 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti @@ -256,8 +256,12 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector = f_decompress_ciphertext_coefficient_pre = (fun (v_COEFFICIENT_BITS: i32) (vector: t_SIMD256Vector) -> - v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l || - v_COEFFICIENT_BITS =. 11l); + (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/ + v v_COEFFICIENT_BITS == 11) /\ + (forall (i: nat). + i < 16 ==> + v (Seq.index (impl.f_repr vector) i) >= 0 /\ + v (Seq.index (impl.f_repr vector) i) < pow2 (v v_COEFFICIENT_BITS))); f_decompress_ciphertext_coefficient_post = (fun (v_COEFFICIENT_BITS: i32) (vector: t_SIMD256Vector) (out: t_SIMD256Vector) -> true); diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst index bdf22c030..84d549d13 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst @@ -310,6 +310,8 @@ let bitwise_and_with_constant in vec +#push-options "--z3rlimit 300" + let cond_subtract_3329_ (vec: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = let v__vec0:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = vec in let vec:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = @@ -356,6 +358,8 @@ let cond_subtract_3329_ (vec: Libcrux_ml_kem.Vector.Portable.Vector_type.t_Porta in vec +#pop-options + #push-options "--z3rlimit 150" let montgomery_multiply_by_constant diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti index 12bab0bbd..8ab792733 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti @@ -355,15 +355,19 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = = (fun (v_COEFFICIENT_BITS: i32) - (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) + (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> - v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l || - v_COEFFICIENT_BITS =. 11l); + (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/ + v v_COEFFICIENT_BITS == 11) /\ + (forall (i: nat). + i < 16 ==> + v (Seq.index (impl.f_repr a) i) >= 0 /\ + v (Seq.index (impl.f_repr a) i) < pow2 (v v_COEFFICIENT_BITS))); f_decompress_ciphertext_coefficient_post = (fun (v_COEFFICIENT_BITS: i32) - (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) + (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true); @@ -371,10 +375,10 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = = (fun (v_COEFFICIENT_BITS: i32) - (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) + (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> Libcrux_ml_kem.Vector.Portable.Compress.decompress_ciphertext_coefficient v_COEFFICIENT_BITS - v); + a); f_ntt_layer_1_step_pre = (fun diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti index 51ddaa539..7a2a775ab 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti @@ -167,11 +167,15 @@ class t_Operations (v_Self: Type0) = { -> Prims.Pure v_Self (f_compress_pre v_COEFFICIENT_BITS x0) (fun result -> f_compress_post v_COEFFICIENT_BITS x0 result); - f_decompress_ciphertext_coefficient_pre:v_COEFFICIENT_BITS: i32 -> v: v_Self + f_decompress_ciphertext_coefficient_pre:v_COEFFICIENT_BITS: i32 -> a: v_Self -> pred: Type0 - { v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l || - v_COEFFICIENT_BITS =. 11l ==> + { (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/ + v v_COEFFICIENT_BITS == 11) /\ + (forall (i: nat). + i < 16 ==> + v (Seq.index (f_repr a) i) >= 0 /\ + v (Seq.index (f_repr a) i) < pow2 (v v_COEFFICIENT_BITS)) ==> pred }; f_decompress_ciphertext_coefficient_post:v_COEFFICIENT_BITS: i32 -> v_Self -> v_Self -> Type0; f_decompress_ciphertext_coefficient:v_COEFFICIENT_BITS: i32 -> x0: v_Self diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Makefile b/libcrux-ml-kem/proofs/fstar/extraction/Makefile index fd1365e91..490eac317 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.Vector.Avx2.fsti \ - Libcrux_ml_kem.Vector.Portable.fsti \ Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.fst \ Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.fst \ Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.fst \ @@ -15,7 +14,6 @@ ADMIT_MODULES = Libcrux_ml_kem.Vector.Avx2.fsti \ Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fst \ Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fst \ Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fst \ - Libcrux_ml_kem.Vector.Portable.fst \ Libcrux_ml_kem.Vector.Avx2.Serialize.fst \ Libcrux_ml_kem.Vector.Avx2.fst \ Libcrux_ml_kem.Vector.Avx2.Ntt.fst \ diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs index 7f8128ddd..7032b7cc5 100644 --- a/libcrux-ml-kem/src/ind_cca.rs +++ b/libcrux-ml-kem/src/ind_cca.rs @@ -625,6 +625,7 @@ pub(crate) mod unpacked { } } + #[hax_lib::fstar::options("--z3rlimit 200")] #[hax_lib::ensures(|result| fstar!("forall (i: nat). i < v $K ==> (forall (j: nat). j < v $K ==> @@ -667,7 +668,7 @@ pub(crate) mod unpacked { /// Generate Unpacked Keys #[inline(always)] - #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")] + #[hax_lib::fstar::options("--z3rlimit 800 --ext context_pruning")] #[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 /\\ diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs index 80e2252be..f6b196aa7 100644 --- a/libcrux-ml-kem/src/serialize.rs +++ b/libcrux-ml-kem/src/serialize.rs @@ -375,6 +375,7 @@ fn deserialize_then_decompress_10( } #[inline(always)] +#[hax_lib::fstar::verification_status(lax)] #[hax_lib::requires( serialized.len() == 352 )] @@ -440,6 +441,7 @@ fn deserialize_then_decompress_4( } #[inline(always)] +#[hax_lib::fstar::verification_status(lax)] #[hax_lib::requires( serialized.len() == 160 )] diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs index 2d6d18798..9f3035fde 100644 --- a/libcrux-ml-kem/src/vector/avx2.rs +++ b/libcrux-ml-kem/src/vector/avx2.rs @@ -181,8 +181,12 @@ impl Operations for SIMD256Vector { } } - #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 || - COEFFICIENT_BITS == 10 || COEFFICIENT_BITS == 11)] + #[requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/ + v $COEFFICIENT_BITS == 5 \\/ + v $COEFFICIENT_BITS == 10 \\/ + v $COEFFICIENT_BITS == 11) /\\ + (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $vector) i) >= 0 /\\ + v (Seq.index (impl.f_repr $vector) i) < pow2 (v $COEFFICIENT_BITS))"))] #[inline(always)] fn decompress_ciphertext_coefficient(vector: Self) -> Self { Self { diff --git a/libcrux-ml-kem/src/vector/portable.rs b/libcrux-ml-kem/src/vector/portable.rs index b8e46b460..5effe4b67 100644 --- a/libcrux-ml-kem/src/vector/portable.rs +++ b/libcrux-ml-kem/src/vector/portable.rs @@ -198,10 +198,14 @@ impl Operations for PortableVector { compress::(a) } - #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 || - COEFFICIENT_BITS == 10 || COEFFICIENT_BITS == 11)] - fn decompress_ciphertext_coefficient(v: Self) -> Self { - decompress_ciphertext_coefficient::(v) + #[requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/ + v $COEFFICIENT_BITS == 5 \\/ + v $COEFFICIENT_BITS == 10 \\/ + v $COEFFICIENT_BITS == 11) /\\ + (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\\ + v (Seq.index (impl.f_repr $a) i) < pow2 (v $COEFFICIENT_BITS))"))] + fn decompress_ciphertext_coefficient(a: Self) -> Self { + decompress_ciphertext_coefficient::(a) } #[requires(fstar!("Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ diff --git a/libcrux-ml-kem/src/vector/portable/arithmetic.rs b/libcrux-ml-kem/src/vector/portable/arithmetic.rs index 54a7b150f..320e51a09 100644 --- a/libcrux-ml-kem/src/vector/portable/arithmetic.rs +++ b/libcrux-ml-kem/src/vector/portable/arithmetic.rs @@ -135,6 +135,7 @@ pub fn shift_right(mut vec: PortableVector) -> PortableVect /// Note: This function is not secret independent /// Only use with public values. #[inline(always)] +#[hax_lib::fstar::options("--z3rlimit 300")] #[hax_lib::requires(fstar!("Spec.Utils.is_i16b_array (pow2 12 - 1) ${vec}.f_elements"))] #[hax_lib::ensures(|result| fstar!("${result}.f_elements == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (${vec}.f_elements)"))] diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs index 208e58b51..50062b0f0 100644 --- a/libcrux-ml-kem/src/vector/traits.rs +++ b/libcrux-ml-kem/src/vector/traits.rs @@ -88,9 +88,13 @@ pub trait Operations: Copy + Clone + Repr { v $COEFFICIENT_BITS == 11) ==> (forall (i:nat). i < 16 ==> bounded (Seq.index (f_repr $result) i) (v $COEFFICIENT_BITS))"))] fn compress(a: Self) -> Self; - #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 || - COEFFICIENT_BITS == 10 || COEFFICIENT_BITS == 11)] - fn decompress_ciphertext_coefficient(v: Self) -> Self; + #[requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/ + v $COEFFICIENT_BITS == 5 \\/ + v $COEFFICIENT_BITS == 10 \\/ + v $COEFFICIENT_BITS == 11) /\\ + (forall (i:nat). i < 16 ==> v (Seq.index (f_repr $a) i) >= 0 /\\ + v (Seq.index (f_repr $a) i) < pow2 (v $COEFFICIENT_BITS))"))] + fn decompress_ciphertext_coefficient(a: Self) -> Self; // NTT #[requires(fstar!("Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ @@ -189,7 +193,7 @@ pub trait Operations: Copy + Clone { fn montgomery_multiply_by_constant(v: Self, c: i16) -> Self; fn compress_1(v: Self) -> Self; fn compress(v: Self) -> Self; - fn decompress_ciphertext_coefficient(v: Self) -> Self; + fn decompress_ciphertext_coefficient(a: Self) -> Self; fn ntt_layer_1_step(a: Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> Self; fn ntt_layer_2_step(a: Self, zeta0: i16, zeta1: i16) -> Self; fn ntt_layer_3_step(a: Self, zeta: i16) -> Self;