From 392604e5d11a2a4ada815d169bf926a2198498d2 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Mon, 11 Nov 2024 11:36:54 +0100 Subject: [PATCH] fstar refresh --- .../Libcrux_intrinsics.Arm64_extract.fsti | 2 +- .../Libcrux_intrinsics.Avx2_extract.fsti | 2 +- .../extraction/Libcrux_ml_kem.Ind_cpa.fst | 6 ++++-- .../extraction/Libcrux_ml_kem.Serialize.fst | 4 ++-- .../extraction/Libcrux_ml_kem.Serialize.fsti | 21 ++++++++++--------- libcrux-ml-kem/src/ind_cpa.rs | 4 ++-- libcrux-ml-kem/src/serialize.rs | 17 ++++++++------- .../extraction/Libcrux_platform.Platform.fsti | 2 +- 8 files changed, 32 insertions(+), 26 deletions(-) diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti index d4014e6a8..a03c287ec 100644 --- a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti +++ b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti @@ -1,5 +1,5 @@ module Libcrux_intrinsics.Arm64_extract -#set-options "--fuel 0 --ifuel 1 --z3rlimit 80" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti index 16d93fb14..290b679a5 100644 --- a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti +++ b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti @@ -1,5 +1,5 @@ module Libcrux_intrinsics.Avx2_extract -#set-options "--fuel 0 --ifuel 1 --z3rlimit 80" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul 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 794773f44..53bae6ddb 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 @@ -738,7 +738,8 @@ let encrypt_unpacked let ciphertext:t_Array u8 v_CIPHERTEXT_SIZE = Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from ciphertext ({ Core.Ops.Range.f_start = v_C1_LEN } <: Core.Ops.Range.t_RangeFrom usize) - (Libcrux_ml_kem.Serialize.compress_then_serialize_ring_element_v v_V_COMPRESSION_FACTOR + (Libcrux_ml_kem.Serialize.compress_then_serialize_ring_element_v v_K + v_V_COMPRESSION_FACTOR v_C2_LEN #v_Vector v @@ -881,7 +882,8 @@ let deserialize_then_decompress_u let u_as_ntt:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize u_as_ntt i - (Libcrux_ml_kem.Serialize.deserialize_then_decompress_ring_element_u v_U_COMPRESSION_FACTOR + (Libcrux_ml_kem.Serialize.deserialize_then_decompress_ring_element_u v_K + v_U_COMPRESSION_FACTOR #v_Vector u_bytes <: 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 b6aeb2798..86f3ca4fc 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 @@ -777,7 +777,7 @@ let compress_then_serialize_ring_element_u result let compress_then_serialize_ring_element_v - (v_COMPRESSION_FACTOR v_OUT_LEN: usize) + (v_K v_COMPRESSION_FACTOR v_OUT_LEN: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: @@ -862,7 +862,7 @@ let deserialize_then_decompress_10_ re let deserialize_then_decompress_ring_element_u - (v_COMPRESSION_FACTOR: usize) + (v_K v_COMPRESSION_FACTOR: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti index 91cb4979d..95e9c748b 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti @@ -81,13 +81,14 @@ val deserialize_then_decompress_ring_element_v (serialized: t_Slice u8) : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) (requires - (v_COMPRESSION_FACTOR =. sz 4 || v_COMPRESSION_FACTOR =. sz 5) && - (Core.Slice.impl__len #u8 serialized <: usize) =. (sz 32 *! v_COMPRESSION_FACTOR <: usize)) + Spec.MLKEM.is_rank v_K /\ + v v_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\ + Seq.length serialized == 32 * v v_COMPRESSION_FACTOR) (ensures fun result -> let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = result in Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector result == - Spec.MLKEM.decode_then_decompress_v v_COMPRESSION_FACTOR serialized) + Spec.MLKEM.decode_then_decompress_v #v_K serialized) /// Only use with public values. /// This MUST NOT be used with secret inputs, like its caller `deserialize_ring_elements_reduced`. @@ -224,22 +225,22 @@ val compress_then_serialize_ring_element_u (Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector re)) val compress_then_serialize_ring_element_v - (v_COMPRESSION_FACTOR v_OUT_LEN: usize) + (v_K v_COMPRESSION_FACTOR v_OUT_LEN: usize) (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) (out: t_Slice u8) : Prims.Pure (t_Slice u8) (requires - (v v_COMPRESSION_FACTOR == 4 \/ v v_COMPRESSION_FACTOR == 5) /\ - v v_OUT_LEN == 32 * v v_COMPRESSION_FACTOR /\ Seq.length out == v v_OUT_LEN /\ - coefficients_field_modulus_range re) + Spec.MLKEM.is_rank v_K /\ + v v_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\ + Seq.length out == v v_OUT_LEN /\ coefficients_field_modulus_range re) (ensures fun out_future -> let out_future:t_Slice u8 = out_future in Core.Slice.impl__len #u8 out_future == Core.Slice.impl__len #u8 out /\ out_future == - Spec.MLKEM.compress_then_encode_v v_COMPRESSION_FACTOR + Spec.MLKEM.compress_then_encode_v #v_K (Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector re)) val deserialize_then_decompress_10_ @@ -251,7 +252,7 @@ val deserialize_then_decompress_10_ (fun _ -> Prims.l_True) val deserialize_then_decompress_ring_element_u - (v_COMPRESSION_FACTOR: usize) + (v_K v_COMPRESSION_FACTOR: usize) (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (serialized: t_Slice u8) @@ -263,7 +264,7 @@ val deserialize_then_decompress_ring_element_u fun result -> let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = result in Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector result == - Spec.MLKEM.byte_decode_then_decompress (v v_COMPRESSION_FACTOR) serialized) + Spec.MLKEM.byte_decode_then_decompress #v_K serialized) val serialize_uncompressed_ring_element (#v_Vector: Type0) diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs index 4891caff8..2657fd040 100644 --- a/libcrux-ml-kem/src/ind_cpa.rs +++ b/libcrux-ml-kem/src/ind_cpa.rs @@ -682,7 +682,7 @@ pub(crate) fn encrypt_unpacked< ); // c_2 := Encode_{dv}(Compress_q(v,d_v)) - compress_then_serialize_ring_element_v::( + compress_then_serialize_ring_element_v::( v, &mut ciphertext[C1_LEN..], ); @@ -808,7 +808,7 @@ fn deserialize_then_decompress_u< Spec.MLKEM.poly_ntt (Spec.MLKEM.byte_decode_then_decompress (v $U_COMPRESSION_FACTOR) (Seq.slice $ciphertext (j * v (Spec.MLKEM.v_C1_BLOCK_SIZE $K)) (j * v (Spec.MLKEM.v_C1_BLOCK_SIZE $K) + v (Spec.MLKEM.v_C1_BLOCK_SIZE $K))))") }); - u_as_ntt[i] = deserialize_then_decompress_ring_element_u::(u_bytes); + u_as_ntt[i] = deserialize_then_decompress_ring_element_u::(u_bytes); ntt_vector_u::(&mut u_as_ntt[i]); } } diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs index 18f8444b7..c8f55583e 100644 --- a/libcrux-ml-kem/src/serialize.rs +++ b/libcrux-ml-kem/src/serialize.rs @@ -325,14 +325,16 @@ fn compress_then_serialize_5( #[inline(always)] #[hax_lib::fstar::verification_status(panic_free)] -#[hax_lib::requires(fstar!("(v $COMPRESSION_FACTOR == 4 \\/ v $COMPRESSION_FACTOR == 5) /\\ v $OUT_LEN == 32 * v $COMPRESSION_FACTOR /\\ +#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank v_K /\\ + v $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\\ Seq.length $out == v $OUT_LEN /\\ coefficients_field_modulus_range $re"))] #[hax_lib::ensures(|_| fstar!("${out_future.len()} == ${out.len()} /\\ - ${out}_future == Spec.MLKEM.compress_then_encode_v $COMPRESSION_FACTOR + ${out}_future == Spec.MLKEM.compress_then_encode_v #v_K (Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector $re)") )] pub(super) fn compress_then_serialize_ring_element_v< + const K: usize, const COMPRESSION_FACTOR: usize, const OUT_LEN: usize, Vector: Operations, @@ -399,9 +401,10 @@ fn deserialize_then_decompress_11( )] #[hax_lib::ensures(|result| fstar!("Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector $result == - Spec.MLKEM.byte_decode_then_decompress (v $COMPRESSION_FACTOR) $serialized") + Spec.MLKEM.byte_decode_then_decompress #v_K $serialized") )] pub(super) fn deserialize_then_decompress_ring_element_u< + const K: usize, const COMPRESSION_FACTOR: usize, Vector: Operations, >( @@ -457,13 +460,13 @@ fn deserialize_then_decompress_5( #[inline(always)] #[hax_lib::fstar::verification_status(panic_free)] -#[hax_lib::requires( - (COMPRESSION_FACTOR == 4 || COMPRESSION_FACTOR == 5) && - serialized.len() == 32 * COMPRESSION_FACTOR +#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank v_K /\\ + v $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\\ + Seq.length serialized == 32 * v v_COMPRESSION_FACTOR") )] #[hax_lib::ensures(|result| fstar!("Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector $result == - Spec.MLKEM.decode_then_decompress_v $COMPRESSION_FACTOR $serialized") + Spec.MLKEM.decode_then_decompress_v #v_K $serialized") )] pub(super) fn deserialize_then_decompress_ring_element_v< const COMPRESSION_FACTOR: usize, diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti index 95dad6932..e8713dad5 100644 --- a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti +++ b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti @@ -1,5 +1,5 @@ module Libcrux_platform.Platform -#set-options "--fuel 0 --ifuel 1 --z3rlimit 80" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul