diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fst index f6d345f9d..9cbda3450 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fst @@ -126,7 +126,6 @@ let decompose_vector (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))) in - let hax_temp_output:Prims.unit = () <: Prims.unit in low, high <: (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & @@ -242,7 +241,6 @@ let power2round_vector (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))) in - let hax_temp_output:Prims.unit = () <: Prims.unit in t, t1 <: (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & @@ -289,7 +287,6 @@ let shift_left_then_reduce <: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re let use_hint @@ -372,7 +369,6 @@ let use_hint in re_vector) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re_vector let vector_infinity_norm_exceeds diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Commitment.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Commitment.fst index ba042cfe4..a459d9535 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Commitment.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Commitment.fst @@ -57,7 +57,6 @@ let serialize <: t_Slice u8) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized let serialize_vector @@ -110,5 +109,4 @@ let serialize_vector let offset:usize = offset +! ring_element_size in offset, serialized <: (usize & t_Slice u8)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Error.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Error.fst index a89960040..b1c4bdc78 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Error.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Error.fst @@ -65,7 +65,6 @@ let deserialize <: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in result let deserialize_to_vector_then_ntt @@ -117,7 +116,6 @@ let deserialize_to_vector_then_ntt in ring_elements) in - let hax_temp_output:Prims.unit = () <: Prims.unit in ring_elements let serialize @@ -168,5 +166,4 @@ let serialize <: t_Slice u8) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Gamma1.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Gamma1.fst index 404fe91ba..fa942586c 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Gamma1.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Gamma1.fst @@ -61,7 +61,7 @@ let deserialize <: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in + let _:Prims.unit = () <: Prims.unit in result let serialize @@ -113,5 +113,5 @@ let serialize <: t_Slice u8) in - let hax_temp_output:Prims.unit = () <: Prims.unit in + let _:Prims.unit = () <: Prims.unit in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst index 07c14734b..5eb1c72d7 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst @@ -10,8 +10,7 @@ let _ = () let set_hint (out_hint: t_Slice (t_Array i32 (sz 256))) (i j: usize) = - let hax_temp_output, out_hint:(Prims.unit & t_Slice (t_Array i32 (sz 256))) = - (), + let out_hint:t_Slice (t_Array i32 (sz 256)) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out_hint i (Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (out_hint.[ i ] @@ -21,8 +20,6 @@ let set_hint (out_hint: t_Slice (t_Array i32 (sz 256))) (i j: usize) = 1l <: t_Array i32 (sz 256)) - <: - (Prims.unit & t_Slice (t_Array i32 (sz 256))) in out_hint @@ -467,5 +464,4 @@ let serialize in signature, true_hints_seen <: (t_Slice u8 & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in signature diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signing_key.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signing_key.fst index 563ad8f9c..d218cb62f 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signing_key.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signing_key.fst @@ -186,5 +186,4 @@ let generate_serialized let offset:usize = offset +! Libcrux_ml_dsa.Constants.v_RING_ELEMENT_OF_T0S_SIZE in offset, signing_key_serialized <: (usize & t_Slice u8)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in signing_key_serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T0.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T0.fst index a12bf71c5..4b0b93667 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T0.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T0.fst @@ -59,7 +59,6 @@ let deserialize <: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in result let deserialize_to_vector_then_ntt @@ -108,7 +107,6 @@ let deserialize_to_vector_then_ntt in ring_elements) in - let hax_temp_output:Prims.unit = () <: Prims.unit in ring_elements let serialize @@ -156,5 +154,4 @@ let serialize <: t_Slice u8) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fst index 02ad5957d..1b47121ee 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fst @@ -57,7 +57,6 @@ let deserialize <: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in result let serialize @@ -107,5 +106,4 @@ let serialize <: t_Slice u8) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Verification_key.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Verification_key.fst index 2066af081..dc840bd86 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Verification_key.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Verification_key.fst @@ -63,7 +63,6 @@ let deserialize <: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in t1 let generate_serialized @@ -140,5 +139,4 @@ let generate_serialized in verification_key_serialized) in - let hax_temp_output:Prims.unit = () <: Prims.unit in verification_key_serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Matrix.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Matrix.fst index 78b15caa6..78a4705b7 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Matrix.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Matrix.fst @@ -53,7 +53,6 @@ let vector_times_ring_element in vector) in - let hax_temp_output:Prims.unit = () <: Prims.unit in vector let add_vectors @@ -85,7 +84,6 @@ let add_vectors <: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in lhs let compute_as1_plus_s2 @@ -187,7 +185,6 @@ let compute_as1_plus_s2 in result) in - let hax_temp_output:Prims.unit = () <: Prims.unit in result let compute_matrix_x_mask @@ -264,7 +261,6 @@ let compute_matrix_x_mask in result) in - let hax_temp_output:Prims.unit = () <: Prims.unit in result let compute_w_approx @@ -366,7 +362,6 @@ let compute_w_approx in t1) in - let hax_temp_output:Prims.unit = () <: Prims.unit in t1 let subtract_vectors @@ -398,5 +393,4 @@ let subtract_vectors <: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in lhs diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fst index bf51216c4..d4addf2d9 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fst @@ -43,7 +43,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) (signing_key verification in let signing_key:t_Slice u8 = tmp0 in let verification_key:t_Slice u8 = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Slice u8 & t_Slice u8) let sign___inner diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_65_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_65_.fst index 76460ff5f..384431e2f 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_65_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_65_.fst @@ -43,7 +43,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) (signing_key verification in let signing_key:t_Slice u8 = tmp0 in let verification_key:t_Slice u8 = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Slice u8 & t_Slice u8) let sign___inner diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_87_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_87_.fst index 4b0b2f7b9..85209dee4 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_87_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_87_.fst @@ -43,7 +43,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) (signing_key verification in let signing_key:t_Slice u8 = tmp0 in let verification_key:t_Slice u8 = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Slice u8 & t_Slice u8) let sign___inner diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.fst index 4d4ef382b..da2a3cd8c 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.fst @@ -35,7 +35,7 @@ let generate_key_pair in let signing_key:t_Array u8 (sz 2560) = tmp0 in let verification_key:t_Array u8 (sz 1312) = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) let sign diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_65_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_65_.fst index ffad39510..692bdeb30 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_65_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_65_.fst @@ -35,7 +35,7 @@ let generate_key_pair in let signing_key:t_Array u8 (sz 4032) = tmp0 in let verification_key:t_Array u8 (sz 1952) = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) let sign diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_87_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_87_.fst index 2e13a6e28..736cfca36 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_87_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_87_.fst @@ -35,7 +35,7 @@ let generate_key_pair in let signing_key:t_Array u8 (sz 4896) = tmp0 in let verification_key:t_Array u8 (sz 2592) = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) let sign diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.fst index 10b695e9e..888e90ff3 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.fst @@ -34,7 +34,7 @@ let generate_key_pair in let signing_key:t_Array u8 (sz 2560) = tmp0 in let verification_key:t_Array u8 (sz 1312) = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) let sign diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.fst index 997301ee1..320ff0fd1 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.fst @@ -34,7 +34,7 @@ let generate_key_pair in let signing_key:t_Array u8 (sz 4032) = tmp0 in let verification_key:t_Array u8 (sz 1952) = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) let sign diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_87_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_87_.fst index c9ba5db20..6c59d201b 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_87_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_87_.fst @@ -34,7 +34,7 @@ let generate_key_pair in let signing_key:t_Array u8 (sz 4896) = tmp0 in let verification_key:t_Array u8 (sz 2592) = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) let sign diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.fst index 3d5bc9e4a..6b04e42e0 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.fst @@ -8,9 +8,7 @@ let generate_key_pair (signing_key: t_Array u8 (sz 2560)) (verification_key: t_Array u8 (sz 1312)) = - let (signing_key, verification_key), hax_temp_output:((t_Array u8 (sz 2560) & t_Array u8 (sz 1312) - ) & - Prims.unit) = + let signing_key, verification_key:(t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) = if Libcrux_platform.Platform.simd256_support () then let tmp0, tmp1:(t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) = @@ -21,9 +19,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 2560) = tmp0 in let verification_key:t_Array u8 (sz 1312) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))), () - <: - ((t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) else if Libcrux_platform.Platform.simd128_support () then @@ -35,9 +31,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 2560) = tmp0 in let verification_key:t_Array u8 (sz 1312) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))), () - <: - ((t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) else let tmp0, tmp1:(t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.generate_key_pair randomness @@ -47,9 +41,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 2560) = tmp0 in let verification_key:t_Array u8 (sz 1312) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))), () - <: - ((t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) in signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_65_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_65_.fst index 22dde3f4a..b6a00d573 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_65_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_65_.fst @@ -8,9 +8,7 @@ let generate_key_pair (signing_key: t_Array u8 (sz 4032)) (verification_key: t_Array u8 (sz 1952)) = - let (signing_key, verification_key), hax_temp_output:((t_Array u8 (sz 4032) & t_Array u8 (sz 1952) - ) & - Prims.unit) = + let signing_key, verification_key:(t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) = if Libcrux_platform.Platform.simd256_support () then let tmp0, tmp1:(t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) = @@ -21,9 +19,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 4032) = tmp0 in let verification_key:t_Array u8 (sz 1952) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))), () - <: - ((t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) else if Libcrux_platform.Platform.simd128_support () then @@ -35,9 +31,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 4032) = tmp0 in let verification_key:t_Array u8 (sz 1952) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))), () - <: - ((t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) else let tmp0, tmp1:(t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.generate_key_pair randomness @@ -47,9 +41,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 4032) = tmp0 in let verification_key:t_Array u8 (sz 1952) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))), () - <: - ((t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) in signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_87_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_87_.fst index 8427f42e6..5e27cee1a 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_87_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_87_.fst @@ -8,9 +8,7 @@ let generate_key_pair (signing_key: t_Array u8 (sz 4896)) (verification_key: t_Array u8 (sz 2592)) = - let (signing_key, verification_key), hax_temp_output:((t_Array u8 (sz 4896) & t_Array u8 (sz 2592) - ) & - Prims.unit) = + let signing_key, verification_key:(t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) = if Libcrux_platform.Platform.simd256_support () then let tmp0, tmp1:(t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) = @@ -21,9 +19,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 4896) = tmp0 in let verification_key:t_Array u8 (sz 2592) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592))), () - <: - ((t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) else if Libcrux_platform.Platform.simd128_support () then @@ -35,9 +31,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 4896) = tmp0 in let verification_key:t_Array u8 (sz 2592) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592))), () - <: - ((t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) else let tmp0, tmp1:(t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_87_.generate_key_pair randomness @@ -47,9 +41,7 @@ let generate_key_pair let signing_key:t_Array u8 (sz 4896) = tmp0 in let verification_key:t_Array u8 (sz 2592) = tmp1 in let _:Prims.unit = () in - (signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592))), () - <: - ((t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) & Prims.unit) + signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) in signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ntt.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ntt.fst index d85329e30..f79c280f8 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ntt.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ntt.fst @@ -91,5 +91,4 @@ let ntt_multiply_montgomery <: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in lhs diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fst index 1960a3305..cdb574003 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fst @@ -100,7 +100,6 @@ let impl__from_i32_array <: t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in result let impl__zero @@ -159,7 +158,6 @@ let impl__add <: t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in self let impl__infinity_norm_exceeds @@ -228,7 +226,6 @@ let impl__subtract <: t_PolynomialRingElement v_SIMDUnit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in self let impl__to_i32_array diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fst index 1a77972f4..b5b5bafcc 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fst @@ -682,7 +682,6 @@ let sample_four_error_ring_elements <: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re let sample_mask_ring_element @@ -697,8 +696,7 @@ let sample_mask_ring_element (result: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) (gamma1_exponent: usize) = - let result, hax_temp_output:(Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & - Prims.unit) = + let result:Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit = match cast (gamma1_exponent <: usize) <: u8 with | 17uy -> let out:t_Array u8 (sz 576) = Rust_primitives.Hax.repeat 0uy (sz 576) in @@ -715,7 +713,7 @@ let sample_mask_ring_element (out <: t_Slice u8) result in - result, () <: (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & Prims.unit) + result | 19uy -> let out:t_Array u8 (sz 640) = Rust_primitives.Hax.repeat 0uy (sz 640) in let out:t_Array u8 (sz 640) = @@ -731,15 +729,8 @@ let sample_mask_ring_element (out <: t_Slice u8) result in - result, () <: (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & Prims.unit) - | _ -> - result, - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" - - <: - Rust_primitives.Hax.t_Never) - <: - (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & Prims.unit) + result + | _ -> result in result @@ -936,7 +927,6 @@ let sample_mask_vector <: (u16 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))) in - let hax_temp_output:Prims.unit = () <: Prims.unit in domain_separator, mask <: (u16 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) @@ -1205,7 +1195,6 @@ let sample_up_to_four_ring_elements_flat <: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in matrix, rand_stack0, rand_stack1, rand_stack2, rand_stack3, tmp_stack <: (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & t_Array u8 (sz 840) & diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Avx2.fst index e37581122..acdc5dacc 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Avx2.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Avx2.fst @@ -20,16 +20,12 @@ let matrix_flat__inner (seed: t_Slice u8) (matrix: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) = - let hax_temp_output, matrix:(Prims.unit & - t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) = - (), + let matrix:t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) = Libcrux_ml_dsa.Samplex4.matrix_flat #v_SIMDUnit #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 columns seed matrix - <: - (Prims.unit & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in matrix diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Neon.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Neon.fst index d90d272f9..972628a50 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Neon.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Neon.fst @@ -50,16 +50,12 @@ let impl: Libcrux_ml_dsa.Samplex4.t_X4Sampler t_NeonSampler = (seed: t_Slice u8) (matrix: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) -> - let hax_temp_output, matrix:(Prims.unit & - t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) = - (), + let matrix:t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) = Libcrux_ml_dsa.Samplex4.matrix_flat #v_SIMDUnit #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 columns seed matrix - <: - (Prims.unit & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in matrix } diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Portable.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Portable.fst index ae973a8f9..efcf1f44f 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Portable.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.Portable.fst @@ -50,16 +50,12 @@ let impl: Libcrux_ml_dsa.Samplex4.t_X4Sampler t_PortableSampler = (seed: t_Slice u8) (matrix: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) -> - let hax_temp_output, matrix:(Prims.unit & - t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) = - (), + let matrix:t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) = Libcrux_ml_dsa.Samplex4.matrix_flat #v_SIMDUnit #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 columns seed matrix - <: - (Prims.unit & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in matrix } diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fst index 01461283e..55bb938a2 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fst @@ -126,7 +126,6 @@ let matrix_flat t_Array u8 (sz 840) & t_Array (t_Array i32 (sz 263)) (sz 4))) in - let hax_temp_output:Prims.unit = () <: Prims.unit in matrix let sample_s1_and_s2 @@ -169,8 +168,7 @@ let sample_s1_and_s2 t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in let remainder:usize = len %! sz 4 in - let s1_s2, hax_temp_output:(t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & - Prims.unit) = + let s1_s2:t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) = if remainder <>. sz 0 then let s1_s2:t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) = @@ -181,12 +179,7 @@ let sample_s1_and_s2 (cast (len -! remainder <: usize) <: u16) s1_s2 in - s1_s2, () - <: - (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & Prims.unit) - else - s1_s2, () - <: - (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & Prims.unit) + s1_s2 + else s1_s2 in s1_s2 diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fst index 4b5f42cbb..1385acbb6 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fst @@ -4,10 +4,8 @@ open Core open FStar.Mul let add (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256) = - let hax_temp_output, lhs:(Prims.unit & Libcrux_intrinsics.Avx2_extract.t_Vec256) = - (), Libcrux_intrinsics.Avx2_extract.mm256_add_epi32 lhs rhs - <: - (Prims.unit & Libcrux_intrinsics.Avx2_extract.t_Vec256) + let lhs:Libcrux_intrinsics.Avx2_extract.t_Vec256 = + Libcrux_intrinsics.Avx2_extract.mm256_add_epi32 lhs rhs in lhs @@ -70,10 +68,8 @@ let infinity_norm_exceeds (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) result <>. 1l let subtract (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256) = - let hax_temp_output, lhs:(Prims.unit & Libcrux_intrinsics.Avx2_extract.t_Vec256) = - (), Libcrux_intrinsics.Avx2_extract.mm256_sub_epi32 lhs rhs - <: - (Prims.unit & Libcrux_intrinsics.Avx2_extract.t_Vec256) + let lhs:Libcrux_intrinsics.Avx2_extract.t_Vec256 = + Libcrux_intrinsics.Avx2_extract.mm256_sub_epi32 lhs rhs in lhs @@ -378,9 +374,8 @@ let use_hint (gamma2: i32) (r hint: Libcrux_intrinsics.Avx2_extract.t_Vec256) = let r1_plus_hints:Libcrux_intrinsics.Avx2_extract.t_Vec256 = Libcrux_intrinsics.Avx2_extract.mm256_add_epi32 r1 hints in - let (hint, r1_plus_hints), hax_temp_output:((Libcrux_intrinsics.Avx2_extract.t_Vec256 & - Libcrux_intrinsics.Avx2_extract.t_Vec256) & - Prims.unit) = + let hint, r1_plus_hints:(Libcrux_intrinsics.Avx2_extract.t_Vec256 & + Libcrux_intrinsics.Avx2_extract.t_Vec256) = match gamma2 <: i32 with | 95232l -> let max:Libcrux_intrinsics.Avx2_extract.t_Vec256 = @@ -397,13 +392,9 @@ let use_hint (gamma2: i32) (r hint: Libcrux_intrinsics.Avx2_extract.t_Vec256) = all_zeros greater_than_or_equal_to_max in - (hint, r1_plus_hints - <: - (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256)), - () + hint, r1_plus_hints <: - ((Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256) & - Prims.unit) + (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256) | 261888l -> let hint:Libcrux_intrinsics.Avx2_extract.t_Vec256 = Libcrux_intrinsics.Avx2_extract.mm256_and_si256 r1_plus_hints @@ -411,23 +402,12 @@ let use_hint (gamma2: i32) (r hint: Libcrux_intrinsics.Avx2_extract.t_Vec256) = <: Libcrux_intrinsics.Avx2_extract.t_Vec256) in - (hint, r1_plus_hints - <: - (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256)), - () + hint, r1_plus_hints <: - ((Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256) & - Prims.unit) + (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256) | _ -> - (hint, r1_plus_hints - <: - (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256)), - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" - - <: - Rust_primitives.Hax.t_Never) + hint, r1_plus_hints <: - ((Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256) & - Prims.unit) + (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256) in hint diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fst index a9d609566..705c073d9 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fst @@ -5,7 +5,7 @@ open FStar.Mul let serialize (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (out: t_Slice u8) = let serialized:t_Array u8 (sz 19) = Rust_primitives.Hax.repeat 0uy (sz 19) in - let (out, serialized), hax_temp_output:((t_Slice u8 & t_Array u8 (sz 19)) & Prims.unit) = + let out, serialized:(t_Slice u8 & t_Array u8 (sz 19)) = match cast (Core.Slice.impl__len #u8 out <: usize) <: u8 with | 4uy -> let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 = @@ -59,9 +59,7 @@ let serialize (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (out: t_Slic <: t_Slice u8) in - (out, serialized <: (t_Slice u8 & t_Array u8 (sz 19))), () - <: - ((t_Slice u8 & t_Array u8 (sz 19)) & Prims.unit) + out, serialized <: (t_Slice u8 & t_Array u8 (sz 19)) | 6uy -> let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 = Libcrux_intrinsics.Avx2_extract.mm256_sllv_epi32 simd_unit @@ -142,16 +140,7 @@ let serialize (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (out: t_Slic <: t_Slice u8) in - (out, serialized <: (t_Slice u8 & t_Array u8 (sz 19))), () - <: - ((t_Slice u8 & t_Array u8 (sz 19)) & Prims.unit) - | _ -> - (out, serialized <: (t_Slice u8 & t_Array u8 (sz 19))), - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" - - <: - Rust_primitives.Hax.t_Never) - <: - ((t_Slice u8 & t_Array u8 (sz 19)) & Prims.unit) + out, serialized <: (t_Slice u8 & t_Array u8 (sz 19)) + | _ -> out, serialized <: (t_Slice u8 & t_Array u8 (sz 19)) in out diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst index 833930c84..e64d2efe3 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst @@ -224,8 +224,7 @@ let serialize_when_eta_is_4_ (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec25 <: t_Slice u8) in - let hax_temp_output, out:(Prims.unit & t_Slice u8) = - (), + let out:t_Slice u8 = Core.Slice.impl__copy_from_slice #u8 out (serialized.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 4 } @@ -233,8 +232,6 @@ let serialize_when_eta_is_4_ (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec25 Core.Ops.Range.t_Range usize ] <: t_Slice u8) - <: - (Prims.unit & t_Slice u8) in out @@ -243,11 +240,9 @@ let serialize (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (serialized: t_Slice u8) = - let serialized, hax_temp_output:(t_Slice u8 & Prims.unit) = + let serialized:t_Slice u8 = match eta <: Libcrux_ml_dsa.Constants.t_Eta with - | Libcrux_ml_dsa.Constants.Eta_Two -> - serialize_when_eta_is_2_ simd_unit serialized, () <: (t_Slice u8 & Prims.unit) - | Libcrux_ml_dsa.Constants.Eta_Four -> - serialize_when_eta_is_4_ simd_unit serialized, () <: (t_Slice u8 & Prims.unit) + | Libcrux_ml_dsa.Constants.Eta_Two -> serialize_when_eta_is_2_ simd_unit serialized + | Libcrux_ml_dsa.Constants.Eta_Four -> serialize_when_eta_is_4_ simd_unit serialized in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Gamma1.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Gamma1.fst index 0d58dcd4a..4e1d65188 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Gamma1.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Gamma1.fst @@ -122,15 +122,12 @@ let deserialize_when_gamma1_is_2_pow_19_ <: Libcrux_intrinsics.Avx2_extract.t_Vec256) in - let hax_temp_output, out:(Prims.unit & Libcrux_intrinsics.Avx2_extract.t_Vec256) = - (), + let out:Libcrux_intrinsics.Avx2_extract.t_Vec256 = Libcrux_intrinsics.Avx2_extract.mm256_sub_epi32 (Libcrux_intrinsics.Avx2_extract.mm256_set1_epi32 deserialize_when_gamma1_is_2_pow_19___GAMMA1 <: Libcrux_intrinsics.Avx2_extract.t_Vec256) coefficients - <: - (Prims.unit & Libcrux_intrinsics.Avx2_extract.t_Vec256) in out @@ -139,24 +136,11 @@ let deserialize (out: Libcrux_intrinsics.Avx2_extract.t_Vec256) (gamma1_exponent: usize) = - let out, hax_temp_output:(Libcrux_intrinsics.Avx2_extract.t_Vec256 & Prims.unit) = + let out:Libcrux_intrinsics.Avx2_extract.t_Vec256 = match cast (gamma1_exponent <: usize) <: u8 with - | 17uy -> - deserialize_when_gamma1_is_2_pow_17_ serialized out, () - <: - (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Prims.unit) - | 19uy -> - deserialize_when_gamma1_is_2_pow_19_ serialized out, () - <: - (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Prims.unit) - | _ -> - out, - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" - - <: - Rust_primitives.Hax.t_Never) - <: - (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Prims.unit) + | 17uy -> deserialize_when_gamma1_is_2_pow_17_ serialized out + | 19uy -> deserialize_when_gamma1_is_2_pow_19_ serialized out + | _ -> out in out @@ -316,8 +300,7 @@ let serialize_when_gamma1_is_2_pow_19_ <: t_Slice u8) in - let hax_temp_output, out:(Prims.unit & t_Slice u8) = - (), + let out:t_Slice u8 = Core.Slice.impl__copy_from_slice #u8 out (serialized.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 20 } @@ -325,8 +308,6 @@ let serialize_when_gamma1_is_2_pow_19_ Core.Ops.Range.t_Range usize ] <: t_Slice u8) - <: - (Prims.unit & t_Slice u8) in out @@ -335,19 +316,10 @@ let serialize (serialized: t_Slice u8) (gamma1_exponent: usize) = - let serialized, hax_temp_output:(t_Slice u8 & Prims.unit) = + let serialized:t_Slice u8 = match cast (gamma1_exponent <: usize) <: u8 with - | 17uy -> - serialize_when_gamma1_is_2_pow_17_ simd_unit serialized, () <: (t_Slice u8 & Prims.unit) - | 19uy -> - serialize_when_gamma1_is_2_pow_19_ simd_unit serialized, () <: (t_Slice u8 & Prims.unit) - | _ -> - serialized, - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" - - <: - Rust_primitives.Hax.t_Never) - <: - (t_Slice u8 & Prims.unit) + | 17uy -> serialize_when_gamma1_is_2_pow_17_ simd_unit serialized + | 19uy -> serialize_when_gamma1_is_2_pow_19_ simd_unit serialized + | _ -> serialized in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.T0.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.T0.fst index b95c1b986..2a5d26958 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.T0.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.T0.fst @@ -115,8 +115,7 @@ let serialize (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (out: t_Slic let serialized:t_Array u8 (sz 16) = Libcrux_intrinsics.Avx2_extract.mm_storeu_bytes_si128 serialized bits_sequential in - let hax_temp_output, out:(Prims.unit & t_Slice u8) = - (), + let out:t_Slice u8 = Core.Slice.impl__copy_from_slice #u8 out (serialized.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 13 } @@ -124,7 +123,5 @@ let serialize (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (out: t_Slic Core.Ops.Range.t_Range usize ] <: t_Slice u8) - <: - (Prims.unit & t_Slice u8) in out diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Invntt.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Invntt.fst index 9a4782dfd..b51dbfe26 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Invntt.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Invntt.fst @@ -465,7 +465,6 @@ let outer_3_plus in re) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re let invert_ntt_at_layer_3_ (re: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32)) = @@ -635,7 +634,6 @@ let invert_ntt_montgomery__inv_inner <: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re let invert_ntt_montgomery (re: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32)) = diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Ntt.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Ntt.fst index cdc59b38d..e57e38802 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Ntt.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Ntt.fst @@ -842,7 +842,6 @@ let ntt_at_layer_5_to_3___round in re) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re let ntt_at_layer_5_to_3_ (re: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32)) = @@ -933,7 +932,7 @@ let ntt_at_layer_5_to_3_ (re: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec ntt_at_layer_5_to_3___round (sz 8) (sz 1) re (sz 15) 280005l in let _:Prims.unit = () in - let hax_temp_output:Prims.unit = () <: Prims.unit in + let _:Prims.unit = () <: Prims.unit in re let ntt__avx2_ntt (re: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32)) = @@ -945,10 +944,5 @@ let ntt__avx2_ntt (re: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz re let ntt (re: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32)) = - let hax_temp_output, re:(Prims.unit & - t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32)) = - (), ntt__avx2_ntt re - <: - (Prims.unit & t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32)) - in + let re:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 (sz 32) = ntt__avx2_ntt re in re diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst index 223d7ca5e..cb7d7a4f1 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst @@ -4,13 +4,10 @@ open Core open FStar.Mul let from_coefficient_array (coefficient_array: t_Slice i32) (out: t_Vec256) = - let hax_temp_output, out:(Prims.unit & t_Vec256) = - (), - ({ out with f_value = Libcrux_intrinsics.Avx2_extract.mm256_loadu_si256_i32 coefficient_array } - <: - t_Vec256) + let out:t_Vec256 = + { out with f_value = Libcrux_intrinsics.Avx2_extract.mm256_loadu_si256_i32 coefficient_array } <: - (Prims.unit & t_Vec256) + t_Vec256 in out diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst index 7fd8a989d..d92dc0ac9 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst @@ -32,10 +32,8 @@ let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vecto f_from_coefficient_array = (fun (coefficient_array: t_Slice i32) (out: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) -> - let hax_temp_output, out:(Prims.unit & Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) = - (), Libcrux_ml_dsa.Simd.Avx2.Vector_type.from_coefficient_array coefficient_array out - <: - (Prims.unit & Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) + let out:Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 = + Libcrux_ml_dsa.Simd.Avx2.Vector_type.from_coefficient_array coefficient_array out in out); f_to_coefficient_array_pre @@ -52,11 +50,7 @@ let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vecto f_to_coefficient_array = (fun (value: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) (out: t_Slice i32) -> - let hax_temp_output, out:(Prims.unit & t_Slice i32) = - (), Libcrux_ml_dsa.Simd.Avx2.Vector_type.to_coefficient_array value out - <: - (Prims.unit & t_Slice i32) - in + let out:t_Slice i32 = Libcrux_ml_dsa.Simd.Avx2.Vector_type.to_coefficient_array value out in out); f_add_pre = @@ -79,20 +73,16 @@ let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vecto (lhs: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) (rhs: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) -> - let hax_temp_output, lhs:(Prims.unit & Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) = - (), - ({ - lhs with - Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value - = - Libcrux_ml_dsa.Simd.Avx2.Arithmetic.add lhs - .Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value - rhs.Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value - } - <: - Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) + let lhs:Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 = + { + lhs with + Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value + = + Libcrux_ml_dsa.Simd.Avx2.Arithmetic.add lhs.Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value + rhs.Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value + } <: - (Prims.unit & Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) + Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 in lhs); f_subtract_pre @@ -116,20 +106,17 @@ let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vecto (lhs: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) (rhs: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) -> - let hax_temp_output, lhs:(Prims.unit & Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) = - (), - ({ - lhs with - Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value - = - Libcrux_ml_dsa.Simd.Avx2.Arithmetic.subtract lhs - .Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value - rhs.Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value - } - <: - Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) + let lhs:Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 = + { + lhs with + Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value + = + Libcrux_ml_dsa.Simd.Avx2.Arithmetic.subtract lhs + .Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value + rhs.Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value + } <: - (Prims.unit & Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) + Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 in lhs); f_montgomery_multiply_pre @@ -180,20 +167,16 @@ let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vecto f_shift_left_then_reduce = (fun (v_SHIFT_BY: i32) (simd_unit: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) -> - let hax_temp_output, simd_unit:(Prims.unit & Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) - = - (), - ({ - simd_unit with - Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value - = - Libcrux_ml_dsa.Simd.Avx2.Arithmetic.shift_left_then_reduce v_SHIFT_BY - simd_unit.Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value - } - <: - Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) + let simd_unit:Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 = + { + simd_unit with + Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value + = + Libcrux_ml_dsa.Simd.Avx2.Arithmetic.shift_left_then_reduce v_SHIFT_BY + simd_unit.Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value + } <: - (Prims.unit & Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) + Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 in simd_unit); f_power2round_pre @@ -451,14 +434,11 @@ let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vecto (serialized: t_Slice u8) (gamma1_exponent: usize) -> - let hax_temp_output, serialized:(Prims.unit & t_Slice u8) = - (), + let serialized:t_Slice u8 = Libcrux_ml_dsa.Simd.Avx2.Encoding.Gamma1.serialize simd_unit .Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value serialized gamma1_exponent - <: - (Prims.unit & t_Slice u8) in serialized); f_gamma1_deserialize_pre @@ -513,13 +493,10 @@ let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vecto f_commitment_serialize = (fun (simd_unit: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) (serialized: t_Slice u8) -> - let hax_temp_output, serialized:(Prims.unit & t_Slice u8) = - (), + let serialized:t_Slice u8 = Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.serialize simd_unit .Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value serialized - <: - (Prims.unit & t_Slice u8) in serialized); f_error_serialize_pre @@ -546,13 +523,10 @@ let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vecto (simd_unit: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) (serialized: t_Slice u8) -> - let hax_temp_output, serialized:(Prims.unit & t_Slice u8) = - (), + let serialized:t_Slice u8 = Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.serialize eta simd_unit.Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_value serialized - <: - (Prims.unit & t_Slice u8) in serialized); f_error_deserialize_pre diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Arithmetic.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Arithmetic.fst index 58fdeb5e6..1564e438b 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Arithmetic.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Arithmetic.fst @@ -152,7 +152,6 @@ let add (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = <: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) in - let hax_temp_output:Prims.unit = () <: Prims.unit in lhs let compute_hint @@ -273,7 +272,6 @@ let decompose (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in low, high <: (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & @@ -359,7 +357,6 @@ let montgomery_multiply (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coe <: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) in - let hax_temp_output:Prims.unit = () <: Prims.unit in lhs let montgomery_multiply_by_constant @@ -404,7 +401,6 @@ let montgomery_multiply_by_constant <: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) in - let hax_temp_output:Prims.unit = () <: Prims.unit in simd_unit let power2round (t0 t1: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = @@ -466,7 +462,6 @@ let power2round (t0 t1: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in t0, t1 <: (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & @@ -511,7 +506,6 @@ let shift_left_then_reduce <: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) in - let hax_temp_output:Prims.unit = () <: Prims.unit in simd_unit let subtract (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = @@ -546,7 +540,6 @@ let subtract (lhs rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) <: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) in - let hax_temp_output:Prims.unit = () <: Prims.unit in lhs let use_hint (gamma2: i32) (simd_unit hint: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = @@ -582,5 +575,4 @@ let use_hint (gamma2: i32) (simd_unit hint: Libcrux_ml_dsa.Simd.Portable.Vector_ <: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) in - let hax_temp_output:Prims.unit = () <: Prims.unit in hint diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst index 5539eba4b..ad1e8b82e 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst @@ -7,7 +7,7 @@ let serialize (simd_unit: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (serialized: t_Slice u8) = - let serialized, hax_temp_output:(t_Slice u8 & Prims.unit) = + let serialized:t_Slice u8 = match cast (Core.Slice.impl__len #u8 serialized <: usize) <: u8 with | 4uy -> let serialized:t_Slice u8 = @@ -30,7 +30,7 @@ let serialize in serialized) in - serialized, (() <: Prims.unit) <: (t_Slice u8 & Prims.unit) + serialized | 6uy -> let serialized:t_Slice u8 = Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 4) @@ -64,14 +64,7 @@ let serialize in serialized) in - serialized, (() <: Prims.unit) <: (t_Slice u8 & Prims.unit) - | _ -> - serialized, - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" - - <: - Rust_primitives.Hax.t_Never) - <: - (t_Slice u8 & Prims.unit) + serialized + | _ -> serialized in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Error.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Error.fst index 1de900ea9..d950169bc 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Error.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Error.fst @@ -180,7 +180,6 @@ let deserialize_when_eta_is_4_ in simd_units) in - let hax_temp_output:Prims.unit = () <: Prims.unit in simd_units let deserialize @@ -188,16 +187,10 @@ let deserialize (serialized: t_Slice u8) (out: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = - let out, hax_temp_output:(Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Prims.unit) = + let out:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = match eta <: Libcrux_ml_dsa.Constants.t_Eta with - | Libcrux_ml_dsa.Constants.Eta_Two -> - deserialize_when_eta_is_2_ serialized out, () - <: - (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Prims.unit) - | Libcrux_ml_dsa.Constants.Eta_Four -> - deserialize_when_eta_is_4_ serialized out, () - <: - (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Prims.unit) + | Libcrux_ml_dsa.Constants.Eta_Two -> deserialize_when_eta_is_2_ serialized out + | Libcrux_ml_dsa.Constants.Eta_Four -> deserialize_when_eta_is_4_ serialized out in out @@ -331,7 +324,6 @@ let serialize_when_eta_is_4_ in serialized) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized let serialize @@ -339,11 +331,9 @@ let serialize (simd_unit: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (serialized: t_Slice u8) = - let serialized, hax_temp_output:(t_Slice u8 & Prims.unit) = + let serialized:t_Slice u8 = match eta <: Libcrux_ml_dsa.Constants.t_Eta with - | Libcrux_ml_dsa.Constants.Eta_Two -> - serialize_when_eta_is_2_ simd_unit serialized, () <: (t_Slice u8 & Prims.unit) - | Libcrux_ml_dsa.Constants.Eta_Four -> - serialize_when_eta_is_4_ simd_unit serialized, () <: (t_Slice u8 & Prims.unit) + | Libcrux_ml_dsa.Constants.Eta_Two -> serialize_when_eta_is_2_ simd_unit serialized + | Libcrux_ml_dsa.Constants.Eta_Four -> serialize_when_eta_is_4_ simd_unit serialized in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Gamma1.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Gamma1.fst index e95fd8d89..6a637b6b9 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Gamma1.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Gamma1.fst @@ -120,7 +120,6 @@ let deserialize_when_gamma1_is_2_pow_17_ in simd_unit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in simd_unit let deserialize_when_gamma1_is_2_pow_19_ @@ -191,7 +190,6 @@ let deserialize_when_gamma1_is_2_pow_19_ in simd_unit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in simd_unit let deserialize @@ -199,24 +197,11 @@ let deserialize (out: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (gamma1_exponent: usize) = - let out, hax_temp_output:(Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Prims.unit) = + let out:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = match cast (gamma1_exponent <: usize) <: u8 with - | 17uy -> - deserialize_when_gamma1_is_2_pow_17_ serialized out, () - <: - (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Prims.unit) - | 19uy -> - deserialize_when_gamma1_is_2_pow_19_ serialized out, () - <: - (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Prims.unit) - | _ -> - out, - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" - - <: - Rust_primitives.Hax.t_Never) - <: - (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & Prims.unit) + | 17uy -> deserialize_when_gamma1_is_2_pow_17_ serialized out + | 19uy -> deserialize_when_gamma1_is_2_pow_19_ serialized out + | _ -> out in out @@ -318,7 +303,6 @@ let serialize_when_gamma1_is_2_pow_17_ in serialized) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized let serialize_when_gamma1_is_2_pow_19_ @@ -377,7 +361,6 @@ let serialize_when_gamma1_is_2_pow_19_ in serialized) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized let serialize @@ -385,19 +368,10 @@ let serialize (serialized: t_Slice u8) (gamma1_exponent: usize) = - let serialized, hax_temp_output:(t_Slice u8 & Prims.unit) = + let serialized:t_Slice u8 = match cast (gamma1_exponent <: usize) <: u8 with - | 17uy -> - serialize_when_gamma1_is_2_pow_17_ simd_unit serialized, () <: (t_Slice u8 & Prims.unit) - | 19uy -> - serialize_when_gamma1_is_2_pow_19_ simd_unit serialized, () <: (t_Slice u8 & Prims.unit) - | _ -> - serialized, - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" - - <: - Rust_primitives.Hax.t_Never) - <: - (t_Slice u8 & Prims.unit) + | 17uy -> serialize_when_gamma1_is_2_pow_17_ simd_unit serialized + | 19uy -> serialize_when_gamma1_is_2_pow_19_ simd_unit serialized + | _ -> serialized in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.T1.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.T1.fst index ed7685a93..80f5daa84 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.T1.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.T1.fst @@ -86,7 +86,6 @@ let deserialize in simd_unit) in - let hax_temp_output:Prims.unit = () <: Prims.unit in simd_unit let serialize @@ -148,5 +147,4 @@ let serialize in serialized) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Invntt.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Invntt.fst index 16fb78743..e31da3316 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Invntt.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Invntt.fst @@ -863,7 +863,6 @@ let outer_3_plus in re) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re let invert_ntt_at_layer_3_ @@ -1036,5 +1035,4 @@ let invert_ntt_montgomery <: t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Ntt.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Ntt.fst index 8378cebc1..a3cb8b326 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Ntt.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Ntt.fst @@ -818,7 +818,6 @@ let outer_3_plus in re) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re let ntt_at_layer_3_ (re: t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32)) = diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fst index d33b18595..8ef8d81cb 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fst @@ -18,27 +18,24 @@ let impl_1 = impl_1' let zero (_: Prims.unit) = { f_values = Rust_primitives.Hax.repeat 0l (sz 8) } <: t_Coefficients let from_coefficient_array (array: t_Slice i32) (out: t_Coefficients) = - let hax_temp_output, out:(Prims.unit & t_Coefficients) = - (), - ({ - out with - f_values - = - Core.Slice.impl__copy_from_slice #i32 - out.f_values - (array.[ { - Core.Ops.Range.f_start = sz 0; - Core.Ops.Range.f_end = Libcrux_ml_dsa.Simd.Traits.v_COEFFICIENTS_IN_SIMD_UNIT - } - <: - Core.Ops.Range.t_Range usize ] + let out:t_Coefficients = + { + out with + f_values + = + Core.Slice.impl__copy_from_slice #i32 + out.f_values + (array.[ { + Core.Ops.Range.f_start = sz 0; + Core.Ops.Range.f_end = Libcrux_ml_dsa.Simd.Traits.v_COEFFICIENTS_IN_SIMD_UNIT + } <: - t_Slice i32) - } - <: - t_Coefficients) + Core.Ops.Range.t_Range usize ] + <: + t_Slice i32) + } <: - (Prims.unit & t_Coefficients) + t_Coefficients in out diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.fst index 1bdaefb89..fb0e68113 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.fst @@ -35,11 +35,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = f_from_coefficient_array = (fun (array: t_Slice i32) (out: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) -> - let hax_temp_output, out:(Prims.unit & - Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = - (), Libcrux_ml_dsa.Simd.Portable.Vector_type.from_coefficient_array array out - <: - (Prims.unit & Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) + let out:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = + Libcrux_ml_dsa.Simd.Portable.Vector_type.from_coefficient_array array out in out); f_to_coefficient_array_pre @@ -57,10 +54,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = f_to_coefficient_array = (fun (value: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (out: t_Slice i32) -> - let hax_temp_output, out:(Prims.unit & t_Slice i32) = - (), Libcrux_ml_dsa.Simd.Portable.Vector_type.to_coefficient_array value out - <: - (Prims.unit & t_Slice i32) + let out:t_Slice i32 = + Libcrux_ml_dsa.Simd.Portable.Vector_type.to_coefficient_array value out in out); f_add_pre @@ -84,11 +79,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = (lhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) -> - let hax_temp_output, lhs:(Prims.unit & - Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = - (), Libcrux_ml_dsa.Simd.Portable.Arithmetic.add lhs rhs - <: - (Prims.unit & Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) + let lhs:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = + Libcrux_ml_dsa.Simd.Portable.Arithmetic.add lhs rhs in lhs); f_subtract_pre @@ -112,11 +104,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = (lhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (rhs: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) -> - let hax_temp_output, lhs:(Prims.unit & - Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = - (), Libcrux_ml_dsa.Simd.Portable.Arithmetic.subtract lhs rhs - <: - (Prims.unit & Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) + let lhs:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = + Libcrux_ml_dsa.Simd.Portable.Arithmetic.subtract lhs rhs in lhs); f_montgomery_multiply_pre @@ -192,7 +181,7 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = in let t0:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = tmp0 in let t1:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in t0, t1 <: (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & @@ -247,7 +236,7 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = in let low:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = tmp0 in let high:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = tmp1 in - let hax_temp_output:Prims.unit = () in + let _:Prims.unit = () in low, high <: (Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients & @@ -309,11 +298,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = (simd_unit: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (hint: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) -> - let hax_temp_output, hint:(Prims.unit & - Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = - (), Libcrux_ml_dsa.Simd.Portable.Arithmetic.use_hint gamma2 simd_unit hint - <: - (Prims.unit & Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) + let hint:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = + Libcrux_ml_dsa.Simd.Portable.Arithmetic.use_hint gamma2 simd_unit hint in hint); f_rejection_sample_less_than_field_modulus_pre @@ -388,13 +374,10 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = (serialized: t_Slice u8) (gamma1_exponent: usize) -> - let hax_temp_output, serialized:(Prims.unit & t_Slice u8) = - (), + let serialized:t_Slice u8 = Libcrux_ml_dsa.Simd.Portable.Encoding.Gamma1.serialize simd_unit serialized gamma1_exponent - <: - (Prims.unit & t_Slice u8) in serialized); f_gamma1_deserialize_pre @@ -421,12 +404,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = (out: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (gamma1_exponent: usize) -> - let hax_temp_output, out:(Prims.unit & - Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = - (), + let out:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = Libcrux_ml_dsa.Simd.Portable.Encoding.Gamma1.deserialize serialized out gamma1_exponent - <: - (Prims.unit & Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) in out); f_commitment_serialize_pre @@ -450,10 +429,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = (simd_unit: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (serialized: t_Slice u8) -> - let hax_temp_output, serialized:(Prims.unit & t_Slice u8) = - (), Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.serialize simd_unit serialized - <: - (Prims.unit & t_Slice u8) + let serialized:t_Slice u8 = + Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.serialize simd_unit serialized in serialized); f_error_serialize_pre @@ -480,10 +457,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = (simd_unit: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (serialized: t_Slice u8) -> - let hax_temp_output, serialized:(Prims.unit & t_Slice u8) = - (), Libcrux_ml_dsa.Simd.Portable.Encoding.Error.serialize eta simd_unit serialized - <: - (Prims.unit & t_Slice u8) + let serialized:t_Slice u8 = + Libcrux_ml_dsa.Simd.Portable.Encoding.Error.serialize eta simd_unit serialized in serialized); f_error_deserialize_pre @@ -529,11 +504,7 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = f_t0_serialize = (fun (simd_unit: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) (out: t_Slice u8) -> - let hax_temp_output, out:(Prims.unit & t_Slice u8) = - (), Libcrux_ml_dsa.Simd.Portable.Encoding.T0.serialize simd_unit out - <: - (Prims.unit & t_Slice u8) - in + let out:t_Slice u8 = Libcrux_ml_dsa.Simd.Portable.Encoding.T0.serialize simd_unit out in out); f_t0_deserialize_pre = @@ -550,11 +521,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = f_t0_deserialize = (fun (serialized: t_Slice u8) (out: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) -> - let hax_temp_output, out:(Prims.unit & - Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) = - (), Libcrux_ml_dsa.Simd.Portable.Encoding.T0.deserialize serialized out - <: - (Prims.unit & Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) + let out:Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = + Libcrux_ml_dsa.Simd.Portable.Encoding.T0.deserialize serialized out in out); f_t1_serialize_pre @@ -607,11 +575,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = f_ntt = (fun (simd_units: t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32)) -> - let hax_temp_output, simd_units:(Prims.unit & - t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32)) = - (), Libcrux_ml_dsa.Simd.Portable.Ntt.ntt simd_units - <: - (Prims.unit & t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32)) + let simd_units:t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32) = + Libcrux_ml_dsa.Simd.Portable.Ntt.ntt simd_units in simd_units); f_invert_ntt_montgomery_pre @@ -628,11 +593,8 @@ Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients = f_invert_ntt_montgomery = fun (simd_units: t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32)) -> - let hax_temp_output, simd_units:(Prims.unit & - t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32)) = - (), Libcrux_ml_dsa.Simd.Portable.Invntt.invert_ntt_montgomery simd_units - <: - (Prims.unit & t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32)) + let simd_units:t_Array Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients (sz 32) = + Libcrux_ml_dsa.Simd.Portable.Invntt.invert_ntt_montgomery simd_units in simd_units } diff --git a/libcrux-ml-dsa/src/arithmetic.rs b/libcrux-ml-dsa/src/arithmetic.rs index a86aa7752..f40580c3c 100644 --- a/libcrux-ml-dsa/src/arithmetic.rs +++ b/libcrux-ml-dsa/src/arithmetic.rs @@ -27,8 +27,6 @@ pub(crate) fn shift_left_then_reduce( for i in 0..re.simd_units.len() { SIMDUnit::shift_left_then_reduce::(&mut re.simd_units[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -41,8 +39,6 @@ pub(crate) fn power2round_vector( SIMDUnit::power2round(&mut t[i].simd_units[j], &mut t1[i].simd_units[j]); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -63,8 +59,6 @@ pub(crate) fn decompose_vector( ); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -110,6 +104,4 @@ pub(crate) fn use_hint( } re_vector[i] = tmp; } - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/encoding/commitment.rs b/libcrux-ml-dsa/src/encoding/commitment.rs index f123ab670..81e9d3471 100644 --- a/libcrux-ml-dsa/src/encoding/commitment.rs +++ b/libcrux-ml-dsa/src/encoding/commitment.rs @@ -12,8 +12,6 @@ fn serialize(re: &PolynomialRingElement, seriali ); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -30,8 +28,6 @@ pub(crate) fn serialize_vector( offset += ring_element_size; } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/encoding/error.rs b/libcrux-ml-dsa/src/encoding/error.rs index ad3aecbde..68e4f5a7c 100644 --- a/libcrux-ml-dsa/src/encoding/error.rs +++ b/libcrux-ml-dsa/src/encoding/error.rs @@ -21,9 +21,6 @@ pub(crate) fn serialize( ); } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -49,9 +46,6 @@ fn deserialize( &mut result.simd_units[i], ); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -67,8 +61,6 @@ pub(crate) fn deserialize_to_vector_then_ntt( ntt(&mut ring_elements[i]); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/encoding/signature.rs b/libcrux-ml-dsa/src/encoding/signature.rs index 34c9351fd..82b023802 100644 --- a/libcrux-ml-dsa/src/encoding/signature.rs +++ b/libcrux-ml-dsa/src/encoding/signature.rs @@ -47,9 +47,6 @@ pub(crate) fn serialize( } signature[offset + max_ones_in_hint + i] = true_hints_seen as u8; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] diff --git a/libcrux-ml-dsa/src/encoding/signing_key.rs b/libcrux-ml-dsa/src/encoding/signing_key.rs index aaee2d442..f61bbf8ab 100644 --- a/libcrux-ml-dsa/src/encoding/signing_key.rs +++ b/libcrux-ml-dsa/src/encoding/signing_key.rs @@ -56,7 +56,4 @@ pub(crate) fn generate_serialized( SIMDUnit::t0_serialize(simd_unit, &mut serialized[i * OUTPUT_BYTES_PER_SIMD_UNIT..(i + 1) * OUTPUT_BYTES_PER_SIMD_UNIT]); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -34,8 +32,6 @@ fn deserialize( &mut result.simd_units[i], ); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -49,8 +45,6 @@ pub(crate) fn deserialize_to_vector_then_ntt( ntt(&mut ring_elements[i]); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/encoding/t1.rs b/libcrux-ml-dsa/src/encoding/t1.rs index 9de90bc62..815162b92 100644 --- a/libcrux-ml-dsa/src/encoding/t1.rs +++ b/libcrux-ml-dsa/src/encoding/t1.rs @@ -14,9 +14,6 @@ pub(crate) fn serialize( SIMDUnit::t1_serialize(simd_unit, &mut serialized[i * OUTPUT_BYTES_PER_SIMD_UNIT..(i + 1) * OUTPUT_BYTES_PER_SIMD_UNIT]); } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } pub(crate) fn deserialize( @@ -30,9 +27,6 @@ pub(crate) fn deserialize( &mut result.simd_units[i], ); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/encoding/verification_key.rs b/libcrux-ml-dsa/src/encoding/verification_key.rs index 1dd8043f9..95b706153 100644 --- a/libcrux-ml-dsa/src/encoding/verification_key.rs +++ b/libcrux-ml-dsa/src/encoding/verification_key.rs @@ -23,8 +23,6 @@ pub(crate) fn generate_serialized( ); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -42,6 +40,4 @@ pub(crate) fn deserialize( &mut t1[i], ); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/matrix.rs b/libcrux-ml-dsa/src/matrix.rs index 9e0cb199f..c32d7e257 100644 --- a/libcrux-ml-dsa/src/matrix.rs +++ b/libcrux-ml-dsa/src/matrix.rs @@ -27,8 +27,6 @@ pub(crate) fn compute_as1_plus_s2( invert_ntt_montgomery::(&mut result[i]); PolynomialRingElement::add(&mut result[i], &s1_s2[columns_in_a + i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } /// Compute InvertNTT(Â ◦ ŷ) @@ -48,8 +46,6 @@ pub(crate) fn compute_matrix_x_mask( } invert_ntt_montgomery(&mut result[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -61,8 +57,6 @@ pub(crate) fn vector_times_ring_element( ntt_multiply_montgomery(&mut vector[i], ring_element); invert_ntt_montgomery(&mut vector[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -74,8 +68,6 @@ pub(crate) fn add_vectors( for i in 0..dimension { PolynomialRingElement::::add(&mut lhs[i], &rhs[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -87,8 +79,6 @@ pub(crate) fn subtract_vectors( for i in 0..dimension { PolynomialRingElement::::subtract(&mut lhs[i], &rhs[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } /// Compute InvertNTT(Â ◦ ẑ - ĉ ◦ NTT(t₁2ᵈ)) @@ -116,6 +106,4 @@ pub(crate) fn compute_w_approx( t1[i] = inner_result; invert_ntt_montgomery(&mut t1[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/ntt.rs b/libcrux-ml-dsa/src/ntt.rs index 711dc2668..2e96a67f9 100644 --- a/libcrux-ml-dsa/src/ntt.rs +++ b/libcrux-ml-dsa/src/ntt.rs @@ -20,8 +20,6 @@ pub(crate) fn ntt_multiply_montgomery( for i in 0..lhs.simd_units.len() { SIMDUnit::montgomery_multiply(&mut lhs.simd_units[i], &rhs.simd_units[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/polynomial.rs b/libcrux-ml-dsa/src/polynomial.rs index 4cf104952..e212ca612 100644 --- a/libcrux-ml-dsa/src/polynomial.rs +++ b/libcrux-ml-dsa/src/polynomial.rs @@ -36,8 +36,6 @@ impl PolynomialRingElement { &mut result.simd_units[i], ); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] @@ -62,8 +60,6 @@ impl PolynomialRingElement { for i in 0..self.simd_units.len() { SIMDUnit::add(&mut self.simd_units[i], &rhs.simd_units[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -71,7 +67,5 @@ impl PolynomialRingElement { for i in 0..self.simd_units.len() { SIMDUnit::subtract(&mut self.simd_units[i], &rhs.simd_units[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } } diff --git a/libcrux-ml-dsa/src/sample.rs b/libcrux-ml-dsa/src/sample.rs index d8883de12..8363d6313 100644 --- a/libcrux-ml-dsa/src/sample.rs +++ b/libcrux-ml-dsa/src/sample.rs @@ -164,9 +164,6 @@ pub(crate) fn sample_up_to_four_ring_elements_flat< &mut matrix[start_index + k], ); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -350,9 +347,6 @@ pub(crate) fn sample_four_error_ring_elements::from_i32_array(&out[i % 4], &mut re[i]); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -436,9 +430,6 @@ pub(crate) fn sample_mask_vector< // TODO: For 87 we may want to do another 4 and discard 1. sample_mask_ring_element::(&seed, &mut mask[i], gamma1_exponent); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] diff --git a/libcrux-ml-dsa/src/samplex4.rs b/libcrux-ml-dsa/src/samplex4.rs index 827c8b993..504ff9bd1 100644 --- a/libcrux-ml-dsa/src/samplex4.rs +++ b/libcrux-ml-dsa/src/samplex4.rs @@ -50,9 +50,6 @@ pub(crate) fn matrix_flat( ); } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } /// Portable sampling diff --git a/libcrux-ml-dsa/src/simd/avx2/invntt.rs b/libcrux-ml-dsa/src/simd/avx2/invntt.rs index f266992ac..0a6e05025 100644 --- a/libcrux-ml-dsa/src/simd/avx2/invntt.rs +++ b/libcrux-ml-dsa/src/simd/avx2/invntt.rs @@ -29,9 +29,6 @@ pub(crate) fn invert_ntt_montgomery(re: &mut AVX2RingElement) { value: arithmetic::montgomery_multiply_by_constant(re[i].value, FACTOR), }; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } unsafe { inv_inner(re) }; @@ -300,9 +297,6 @@ fn outer_3_plus( value: arithmetic::montgomery_multiply_by_constant(a_minus_b, ZETA), }; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg_attr(not(hax), target_feature(enable = "avx2"))] diff --git a/libcrux-ml-dsa/src/simd/avx2/ntt.rs b/libcrux-ml-dsa/src/simd/avx2/ntt.rs index 0f0306642..544a267bc 100644 --- a/libcrux-ml-dsa/src/simd/avx2/ntt.rs +++ b/libcrux-ml-dsa/src/simd/avx2/ntt.rs @@ -326,9 +326,6 @@ unsafe fn ntt_at_layer_5_to_3(re: &mut AVX2RingElement) { }; re[j + STEP_BY] = AVX2SIMDUnit { value: tmp }; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } // Layer 5 diff --git a/libcrux-ml-dsa/src/simd/portable/arithmetic.rs b/libcrux-ml-dsa/src/simd/portable/arithmetic.rs index 9e4df9a44..5671d8331 100644 --- a/libcrux-ml-dsa/src/simd/portable/arithmetic.rs +++ b/libcrux-ml-dsa/src/simd/portable/arithmetic.rs @@ -13,9 +13,6 @@ pub fn add(lhs: &mut Coefficients, rhs: &Coefficients) { for i in 0..lhs.values.len() { lhs.values[i] += rhs.values[i]; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -23,9 +20,6 @@ pub fn subtract(lhs: &mut Coefficients, rhs: &Coefficients) { for i in 0..lhs.values.len() { lhs.values[i] -= rhs.values[i]; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -60,9 +54,6 @@ pub(crate) fn montgomery_multiply_by_constant(simd_unit: &mut Coefficients, c: i for i in 0..simd_unit.values.len() { simd_unit.values[i] = montgomery_reduce_element((simd_unit.values[i] as i64) * (c as i64)) } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -70,9 +61,6 @@ pub(crate) fn montgomery_multiply(lhs: &mut Coefficients, rhs: &Coefficients) { for i in 0..lhs.values.len() { lhs.values[i] = montgomery_reduce_element((lhs.values[i] as i64) * (rhs.values[i] as i64)) } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } // Splits t ∈ {0, ..., q-1} into t0 and t1 with a = t1*2ᴰ + t0 @@ -107,9 +95,6 @@ pub(super) fn power2round(t0: &mut Coefficients, t1: &mut Coefficients) { for i in 0..t0.values.len() { (t0.values[i], t1.values[i]) = power2round_element(t0.values[i]); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } // TODO: Revisit this function when doing the range analysis and testing @@ -153,9 +138,6 @@ pub(super) fn shift_left_then_reduce(simd_unit: &mut Coeffi for i in 0..simd_unit.values.len() { simd_unit.values[i] = reduce_element(simd_unit.values[i] << SHIFT_BY); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -287,9 +269,6 @@ pub fn decompose( for i in 0..low.values.len() { (low.values[i], high.values[i]) = decompose_element(gamma2, simd_unit.values[i]); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -297,9 +276,6 @@ pub fn use_hint(gamma2: Gamma2, simd_unit: &Coefficients, hint: &mut Coefficient for i in 0..hint.values.len() { hint.values[i] = use_one_hint(gamma2, simd_unit.values[i], hint.values[i]); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/simd/portable/encoding/error.rs b/libcrux-ml-dsa/src/simd/portable/encoding/error.rs index da747fbbd..34096bb79 100644 --- a/libcrux-ml-dsa/src/simd/portable/encoding/error.rs +++ b/libcrux-ml-dsa/src/simd/portable/encoding/error.rs @@ -33,9 +33,6 @@ fn serialize_when_eta_is_4(simd_unit: &Coefficients, serialized: &mut [u8]) { serialized[i] = (coefficient1 << 4) | coefficient0; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -79,9 +76,6 @@ fn deserialize_when_eta_is_4(serialized: &[u8], simd_units: &mut Coefficients) { simd_units.values[2 * i + 1] = ETA - ((byte >> 4) as i32); } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] pub(crate) fn deserialize(eta: Eta, serialized: &[u8], out: &mut Coefficients) { diff --git a/libcrux-ml-dsa/src/simd/portable/encoding/gamma1.rs b/libcrux-ml-dsa/src/simd/portable/encoding/gamma1.rs index 520c8adfa..05239491a 100644 --- a/libcrux-ml-dsa/src/simd/portable/encoding/gamma1.rs +++ b/libcrux-ml-dsa/src/simd/portable/encoding/gamma1.rs @@ -31,9 +31,6 @@ fn serialize_when_gamma1_is_2_pow_17(simd_unit: &Coefficients, serialized: &mut serialized[9 * i + 8] = (coefficient3 >> 10) as u8; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -55,9 +52,6 @@ fn serialize_when_gamma1_is_2_pow_19(simd_unit: &Coefficients, serialized: &mut serialized[5 * i + 4] = (coefficient1 >> 12) as u8; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -106,9 +100,6 @@ fn deserialize_when_gamma1_is_2_pow_17(serialized: &[u8], simd_unit: &mut Coeffi simd_unit.values[4 * i + 3] = GAMMA1 - coefficient3; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -135,9 +126,6 @@ fn deserialize_when_gamma1_is_2_pow_19(serialized: &[u8], simd_unit: &mut Coeffi simd_unit.values[2 * i + 1] = GAMMA1 - coefficient1; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] diff --git a/libcrux-ml-dsa/src/simd/portable/encoding/t1.rs b/libcrux-ml-dsa/src/simd/portable/encoding/t1.rs index f53788dd6..35e8c28cc 100644 --- a/libcrux-ml-dsa/src/simd/portable/encoding/t1.rs +++ b/libcrux-ml-dsa/src/simd/portable/encoding/t1.rs @@ -18,9 +18,6 @@ pub fn serialize(simd_unit: &Coefficients, serialized: &mut [u8]) { serialized[5 * i + 4] = ((coefficients[3] >> 2) & 0xFF) as u8; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -43,7 +40,4 @@ pub fn deserialize(serialized: &[u8], simd_unit: &mut Coefficients) { simd_unit.values[4 * i + 3] = ((byte3 >> 6) | (byte4 << 2)) & mask; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/simd/portable/invntt.rs b/libcrux-ml-dsa/src/simd/portable/invntt.rs index 4ec015e60..95e1ac58b 100644 --- a/libcrux-ml-dsa/src/simd/portable/invntt.rs +++ b/libcrux-ml-dsa/src/simd/portable/invntt.rs @@ -212,9 +212,6 @@ fn outer_3_plus( re[j + STEP_BY] = a_minus_b; arithmetic::montgomery_multiply_by_constant(&mut re[j + STEP_BY], ZETA); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -301,7 +298,4 @@ pub(crate) fn invert_ntt_montgomery(re: &mut [Coefficients; SIMD_UNITS_IN_RING_E // - Convert the elements form montgomery domain to the standard domain. arithmetic::montgomery_multiply_by_constant(&mut re[i], 41_978); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/simd/portable/ntt.rs b/libcrux-ml-dsa/src/simd/portable/ntt.rs index 6e017f5a8..0b071815a 100644 --- a/libcrux-ml-dsa/src/simd/portable/ntt.rs +++ b/libcrux-ml-dsa/src/simd/portable/ntt.rs @@ -212,7 +212,6 @@ fn outer_3_plus( arithmetic::subtract(&mut re[j + STEP_BY], &tmp); arithmetic::add(&mut re[j], &tmp); } - () // Needed because of https://github.com/hacspec/hax/issues/720 } #[inline(always)] diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti index 05c34b4bc..cef2d8613 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti @@ -3,6 +3,12 @@ module Libcrux_ml_kem.Hash_functions open Core open FStar.Mul +/// The SHA3 block size. +let v_BLOCK_SIZE: usize = sz 168 + +/// The size of 3 SHA3 blocks. +let v_THREE_BLOCKS: usize = v_BLOCK_SIZE *! sz 3 + /// Abstraction for the hashing, to pick the fastest version depending on the /// platform features available. /// There are 3 instantiations of this trait right now, using the libcrux-sha3 crate. @@ -61,9 +67,3 @@ class t_Hash (v_Self: Type0) (v_K: usize) = { (f_shake128_squeeze_next_block_pre x0) (fun result -> f_shake128_squeeze_next_block_post x0 result) } - -/// The SHA3 block size. -let v_BLOCK_SIZE: usize = sz 168 - -/// The size of 3 SHA3 blocks. -let v_THREE_BLOCKS: usize = v_BLOCK_SIZE *! sz 3 diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.fst index ec082d69c..ec28ee0ba 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.fst @@ -75,18 +75,12 @@ let generate_keypair_avx2 Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - let hax_temp_output, out:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - (), + let out:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K + Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector = Libcrux_ml_kem.Ind_cca.Unpacked.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 #Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector #Libcrux_ml_kem.Hash_functions.Avx2.t_Simd256Hash #Libcrux_ml_kem.Variant.t_MlKem randomness out - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) in out @@ -98,10 +92,8 @@ let generate_keypair Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - let hax_temp_output, out:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - (), + let out:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K + Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector = generate_keypair_avx2 v_K v_CPA_PRIVATE_KEY_SIZE v_PRIVATE_KEY_SIZE @@ -111,10 +103,6 @@ let generate_keypair v_ETA1_RANDOMNESS_SIZE randomness out - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) in out @@ -147,10 +135,8 @@ let unpack_public_key_avx2 Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K + Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector = Libcrux_ml_kem.Ind_cca.Unpacked.unpack_public_key v_K v_T_AS_NTT_ENCODED_SIZE v_RANKED_BYTES_PER_RING_ELEMENT @@ -159,10 +145,6 @@ let unpack_public_key_avx2 #Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) in unpacked_public_key @@ -173,19 +155,13 @@ let unpack_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K + Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector = unpack_public_key_avx2 v_K v_T_AS_NTT_ENCODED_SIZE v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.fst index 591097306..c6b885fed 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.fst @@ -50,19 +50,13 @@ let generate_keypair Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - let hax_temp_output, out:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - (), + let out:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K + Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector = Libcrux_ml_kem.Ind_cca.Unpacked.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 #Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector #Libcrux_ml_kem.Hash_functions.Neon.t_Simd128Hash #Libcrux_ml_kem.Variant.t_MlKem randomness out - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) in out @@ -95,10 +89,8 @@ let unpack_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K + Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector = Libcrux_ml_kem.Ind_cca.Unpacked.unpack_public_key v_K v_T_AS_NTT_ENCODED_SIZE v_RANKED_BYTES_PER_RING_ELEMENT @@ -107,9 +99,5 @@ let unpack_public_key #Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.fst index b9f62cbc3..c32203958 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.fst @@ -50,19 +50,13 @@ let generate_keypair Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - let hax_temp_output, out:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - (), + let out:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K + Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = Libcrux_ml_kem.Ind_cca.Unpacked.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 #Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector #(Libcrux_ml_kem.Hash_functions.Portable.t_PortableHash v_K) #Libcrux_ml_kem.Variant.t_MlKem randomness out - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) in out @@ -95,10 +89,8 @@ let unpack_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K + Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = Libcrux_ml_kem.Ind_cca.Unpacked.unpack_public_key v_K v_T_AS_NTT_ENCODED_SIZE v_RANKED_BYTES_PER_RING_ELEMENT @@ -107,9 +99,5 @@ let unpack_public_key #Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) in unpacked_public_key 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 ed2632129..74db3dabb 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 @@ -615,17 +615,13 @@ let impl_4__serialized_public_key_mut (self: t_MlKemKeyPairUnpacked v_K v_Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) = - let hax_temp_output, serialized:(Prims.unit & - Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) = - (), + let serialized:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = impl_3__serialized_mut v_K #v_Vector v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE self.f_public_key serialized - <: - (Prims.unit & Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) in serialized 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 ffe998283..a0e42d84a 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 @@ -862,7 +862,6 @@ let compress_then_serialize_u (Spec.MLKEM.compress_then_encode_u #v_K (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector input)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in out #pop-options diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst index b819cb727..c405a03d7 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst @@ -105,7 +105,6 @@ let invert_ntt_at_layer_1_ in re, zeta_i <: (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in zeta_i, re <: (usize & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) #pop-options @@ -183,7 +182,6 @@ let invert_ntt_at_layer_2_ in re, zeta_i <: (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in zeta_i, re <: (usize & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) #pop-options @@ -259,7 +257,6 @@ let invert_ntt_at_layer_3_ in re, zeta_i <: (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in zeta_i, re <: (usize & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) #pop-options @@ -346,7 +343,6 @@ let invert_ntt_at_layer_4_plus in re, zeta_i <: (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in zeta_i, re <: (usize & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) #pop-options @@ -402,10 +398,7 @@ let invert_ntt_montgomery let zeta_i:usize = tmp0 in let re:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = tmp1 in let _:Prims.unit = () in - let hax_temp_output, re:(Prims.unit & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) - = - (), Libcrux_ml_kem.Polynomial.impl_2__poly_barrett_reduce #v_Vector re - <: - (Prims.unit & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) + let re:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = + Libcrux_ml_kem.Polynomial.impl_2__poly_barrett_reduce #v_Vector re in re diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Matrix.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Matrix.fst index 92a2c589d..6c1d41758 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Matrix.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Matrix.fst @@ -134,7 +134,7 @@ let sample_matrix_A in let result:Prims.unit = () <: Prims.unit in let _:Prims.unit = admit () (* Panic freedom *) in - let hax_temp_output:Prims.unit = result in + let _:Prims.unit = result in v_A_transpose let compute_As_plus_e @@ -229,7 +229,7 @@ let compute_As_plus_e in let result:Prims.unit = () <: Prims.unit in let _:Prims.unit = admit () (* Panic freedom *) in - let hax_temp_output:Prims.unit = result in + let _:Prims.unit = result in tt_as_ntt #push-options "--admit_smt_queries true" diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fst index e37975ff3..be6ebd525 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fst @@ -111,10 +111,8 @@ let generate_key_pair_mut Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - let hax_temp_output, key_pair:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - (), + let key_pair:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) + Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector = Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.generate_keypair (sz 4) (sz 1536) (sz 3168) @@ -124,10 +122,6 @@ let generate_key_pair_mut (sz 128) randomness key_pair - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) in key_pair @@ -182,19 +176,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) + Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector = Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.unpack_public_key (sz 4) (sz 1536) (sz 1536) (sz 1568) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fst index 92cd21b33..865f73d20 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fst @@ -111,10 +111,8 @@ let generate_key_pair_mut Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - let hax_temp_output, key_pair:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - (), + let key_pair:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) + Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector = Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.generate_keypair (sz 4) (sz 1536) (sz 3168) @@ -124,10 +122,6 @@ let generate_key_pair_mut (sz 128) randomness key_pair - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) in key_pair @@ -182,19 +176,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) + Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector = Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.unpack_public_key (sz 4) (sz 1536) (sz 1536) (sz 1568) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fst index c0f9ff42d..864cd1438 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fst @@ -111,10 +111,8 @@ let generate_key_pair_mut Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - let hax_temp_output, key_pair:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - (), + let key_pair:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) + Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.generate_keypair (sz 4) (sz 1536) (sz 3168) @@ -124,10 +122,6 @@ let generate_key_pair_mut (sz 128) randomness key_pair - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked (sz 4) - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) in key_pair @@ -182,19 +176,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) + Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.unpack_public_key (sz 4) (sz 1536) (sz 1536) (sz 1568) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 4) - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fst index a63bcaf11..c02a6e7aa 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fst @@ -75,16 +75,13 @@ let serialized_public_key Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) = - let hax_temp_output, serialized:(Prims.unit & Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) = - (), + let serialized:Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800) = Libcrux_ml_kem.Ind_cca.Unpacked.impl_3__serialized_mut (sz 2) #Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector (sz 768) (sz 800) public_key serialized - <: - (Prims.unit & Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) in serialized @@ -178,19 +175,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) + Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector = Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.unpack_public_key (sz 2) (sz 768) (sz 768) (sz 800) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fst index 1142a8c11..dc2ec0335 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fst @@ -75,16 +75,13 @@ let serialized_public_key Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) = - let hax_temp_output, serialized:(Prims.unit & Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) = - (), + let serialized:Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800) = Libcrux_ml_kem.Ind_cca.Unpacked.impl_3__serialized_mut (sz 2) #Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector (sz 768) (sz 800) public_key serialized - <: - (Prims.unit & Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) in serialized @@ -178,19 +175,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) + Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector = Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.unpack_public_key (sz 2) (sz 768) (sz 768) (sz 800) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fst index ac9e84801..858d9359a 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fst @@ -75,16 +75,13 @@ let serialized_public_key Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) = - let hax_temp_output, serialized:(Prims.unit & Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) = - (), + let serialized:Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800) = Libcrux_ml_kem.Ind_cca.Unpacked.impl_3__serialized_mut (sz 2) #Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector (sz 768) (sz 800) public_key serialized - <: - (Prims.unit & Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) in serialized @@ -179,19 +176,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) + Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.unpack_public_key (sz 2) (sz 768) (sz 768) (sz 800) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 2) - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fst index 7788eac55..26a1de1e8 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fst @@ -198,19 +198,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) + Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector = Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.unpack_public_key (sz 3) (sz 1152) (sz 1152) (sz 1184) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) - Libcrux_ml_kem.Vector.Avx2.t_SIMD256Vector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fst index 541f0ab82..3a57c5f0b 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fst @@ -199,19 +199,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) + Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector = Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.unpack_public_key (sz 3) (sz 1152) (sz 1152) (sz 1184) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) - Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fst index 4588ae4aa..02504bb00 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fst @@ -199,19 +199,13 @@ let unpacked_public_key Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - let hax_temp_output, unpacked_public_key:(Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = - (), + let unpacked_public_key:Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) + Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.unpack_public_key (sz 3) (sz 1152) (sz 1152) (sz 1184) public_key unpacked_public_key - <: - (Prims.unit & - Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked (sz 3) - Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) in unpacked_public_key diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst index d9896a6e6..c9cb3fbc7 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst @@ -103,7 +103,6 @@ let ntt_at_layer_1_ in re, zeta_i <: (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in zeta_i, re <: (usize & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) #pop-options @@ -183,7 +182,6 @@ let ntt_at_layer_2_ in re, zeta_i <: (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in zeta_i, re <: (usize & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) #pop-options @@ -261,7 +259,6 @@ let ntt_at_layer_3_ in re, zeta_i <: (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in zeta_i, re <: (usize & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) #pop-options @@ -347,7 +344,6 @@ let ntt_at_layer_4_plus in re, zeta_i <: (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector & usize)) in - let hax_temp_output:Prims.unit = () <: Prims.unit in zeta_i, re <: (usize & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) #pop-options @@ -422,7 +418,6 @@ let ntt_at_layer_7_ in re) in - let hax_temp_output:Prims.unit = () <: Prims.unit in re #pop-options @@ -482,7 +477,7 @@ let ntt_binomially_sampled_ring_element (Prims.unit & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) in let _:Prims.unit = admit () (* Panic freedom *) in - let hax_temp_output:Prims.unit = result in + let _:Prims.unit = result in re #pop-options @@ -546,7 +541,7 @@ let ntt_vector_u (Prims.unit & Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) in let _:Prims.unit = admit () (* Panic freedom *) in - let hax_temp_output:Prims.unit = result in + let _:Prims.unit = result in re #pop-options diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst index 4cad63238..98121e9f7 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst @@ -95,7 +95,6 @@ let add_error_reduce in myself) in - let hax_temp_output:Prims.unit = () <: Prims.unit in myself #pop-options @@ -225,7 +224,6 @@ let add_standard_error_reduce in myself) in - let hax_temp_output:Prims.unit = () <: Prims.unit in myself #pop-options @@ -277,7 +275,6 @@ let poly_barrett_reduce <: t_PolynomialRingElement v_Vector) in - let hax_temp_output:Prims.unit = () <: Prims.unit in myself #pop-options @@ -540,7 +537,6 @@ let add_to_ring_element <: t_PolynomialRingElement v_Vector) in - let hax_temp_output:Prims.unit = () <: Prims.unit in myself #pop-options diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti index 7f60ace38..c64101d1e 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti @@ -37,6 +37,10 @@ val zeta (i: usize) let result:i16 = result in Spec.Utils.is_i16b 1664 result) +let v_VECTORS_IN_RING_ELEMENT: usize = + Libcrux_ml_kem.Constants.v_COEFFICIENTS_IN_RING_ELEMENT /! + Libcrux_ml_kem.Vector.Traits.v_FIELD_ELEMENTS_IN_VECTOR + type t_PolynomialRingElement (v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} = { f_coefficients:t_Array v_Vector (sz 16) } @@ -45,7 +49,7 @@ let to_spec_poly_t (#v_Vector: Type0) {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (p: t_PolynomialRingElement v_Vector) : Spec.MLKEM.polynomial = createi (sz 256) (fun i -> Spec.MLKEM.Math.to_spec_fe - (Seq.index (i2._super_8706949974463268012.f_repr + (Seq.index (i2._super_12682756204189288427.f_repr (Seq.index p.f_coefficients (v i / 16))) (v i % 16))) let to_spec_vector_t (#r:Spec.MLKEM.rank) (#v_Vector: Type0) @@ -58,10 +62,6 @@ let to_spec_matrix_t (#r:Spec.MLKEM.rank) (#v_Vector: Type0) (m:t_Array (t_Array (t_PolynomialRingElement v_Vector) r) r) : Spec.MLKEM.matrix r = createi r (fun i -> to_spec_vector_t #r #v_Vector (m.[i])) -let v_VECTORS_IN_RING_ELEMENT: usize = - Libcrux_ml_kem.Constants.v_COEFFICIENTS_IN_RING_ELEMENT /! - Libcrux_ml_kem.Vector.Traits.v_FIELD_ELEMENTS_IN_VECTOR - [@@ FStar.Tactics.Typeclasses.tcinstance] val impl (#v_Vector: Type0) 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 5de9a6d47..d24b6539c 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 @@ -435,7 +435,7 @@ let deserialize_ring_elements_reduced in let result:Prims.unit = () <: Prims.unit in let _:Prims.unit = admit () (* Panic freedom *) in - let hax_temp_output:Prims.unit = result in + let _:Prims.unit = result in deserialized_pk let deserialize_ring_elements_reduced_out @@ -647,7 +647,7 @@ let compress_then_serialize_4_ (serialized: t_Slice u8) = let _:Prims.unit = assert_norm (pow2 4 == 16) in - let serialized:t_Slice u8 = + let serialized, result:(t_Slice u8 & Prims.unit) = Rust_primitives.Hax.Folds.fold_range (sz 0) Libcrux_ml_kem.Polynomial.v_VECTORS_IN_RING_ELEMENT (fun serialized i -> @@ -699,11 +699,13 @@ let compress_then_serialize_4_ <: t_Slice u8) in - serialized) + serialized), + () + <: + (t_Slice u8 & Prims.unit) in - let result:Prims.unit = () <: Prims.unit in let _:Prims.unit = admit () (* Panic freedom *) in - let hax_temp_output:Prims.unit = result in + let _:Prims.unit = result in serialized #push-options "--admit_smt_queries true" @@ -764,7 +766,6 @@ let compress_then_serialize_5_ in serialized) in - let hax_temp_output:Prims.unit = () <: Prims.unit in serialized #pop-options @@ -888,7 +889,7 @@ let compress_then_serialize_ring_element_v (t_Slice u8 & Prims.unit) in let _:Prims.unit = admit () (* Panic freedom *) in - let hax_temp_output:Prims.unit = result in + let _:Prims.unit = result in out let serialize_uncompressed_ring_element diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst index d4dea7527..900372fd8 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst @@ -342,6 +342,8 @@ let impl_3 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemCiphertext v_SIZE) ( #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value + <: + Core.Result.t_Result (t_Array u8 v_SIZE) Core.Array.t_TryFromSliceError with | Core.Result.Result_Ok value -> Core.Result.Result_Ok ({ f_value = value } <: t_MlKemCiphertext v_SIZE) @@ -373,6 +375,8 @@ let impl_10 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemPrivateKey v_SIZE) #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value + <: + Core.Result.t_Result (t_Array u8 v_SIZE) Core.Array.t_TryFromSliceError with | Core.Result.Result_Ok value -> Core.Result.Result_Ok ({ f_value = value } <: t_MlKemPrivateKey v_SIZE) @@ -404,6 +408,8 @@ let impl_17 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemPublicKey v_SIZE) ( #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value + <: + Core.Result.t_Result (t_Array u8 v_SIZE) Core.Array.t_TryFromSliceError with | Core.Result.Result_Ok value -> Core.Result.Result_Ok ({ f_value = value } <: t_MlKemPublicKey v_SIZE) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst index b0b8981ad..f63bcef62 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst @@ -203,8 +203,8 @@ let vec_to_i16_array (v: t_SIMD256Vector) = [@@ FStar.Tactics.Typeclasses.tcinstance] let impl: Libcrux_ml_kem.Vector.Traits.t_Repr t_SIMD256Vector = { - _super_11581440318597584651 = FStar.Tactics.Typeclasses.solve; - _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; + _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve; + _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve; f_repr_pre = (fun (x: t_SIMD256Vector) -> true); f_repr_post = (fun (x: t_SIMD256Vector) (out: t_Array i16 (sz 16)) -> true); f_repr = fun (x: t_SIMD256Vector) -> vec_to_i16_array x @@ -227,9 +227,9 @@ let deserialize_12_ (bytes: t_Slice u8) = [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector = { - _super_11581440318597584651 = FStar.Tactics.Typeclasses.solve; - _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; - _super_8706949974463268012 = FStar.Tactics.Typeclasses.solve; + _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve; + _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve; + _super_12682756204189288427 = FStar.Tactics.Typeclasses.solve; f_ZERO_pre = (fun (_: Prims.unit) -> true); f_ZERO_post = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Compress.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Compress.fst index 29ffc7ec4..797444743 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Compress.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Compress.fst @@ -17,7 +17,7 @@ let compress_int32x4_t (v_COEFFICIENT_BITS: i32) (v: u8) = Libcrux_intrinsics.Arm64_extract.v__vshrq_n_u32 4l compressed let mask_n_least_significant_bits (coefficient_bits: i16) = - match coefficient_bits with + match coefficient_bits <: i16 with | 4s -> 15s | 5s -> 31s | 10s -> 1023s diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.fst index 7697d036c..0c4739a48 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.fst @@ -51,8 +51,8 @@ let rej_sample (a: t_Slice u8) (result: t_Slice i16) = [@@ FStar.Tactics.Typeclasses.tcinstance] let impl: Libcrux_ml_kem.Vector.Traits.t_Repr Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector = { - _super_11581440318597584651 = FStar.Tactics.Typeclasses.solve; - _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; + _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve; + _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve; f_repr_pre = (fun (x: Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector) -> true); f_repr_post = @@ -68,9 +68,9 @@ let impl: Libcrux_ml_kem.Vector.Traits.t_Repr Libcrux_ml_kem.Vector.Neon.Vector_ let impl_1: Libcrux_ml_kem.Vector.Traits.t_Operations Libcrux_ml_kem.Vector.Neon.Vector_type.t_SIMD128Vector = { - _super_11581440318597584651 = FStar.Tactics.Typeclasses.solve; - _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; - _super_8706949974463268012 = FStar.Tactics.Typeclasses.solve; + _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve; + _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve; + _super_12682756204189288427 = FStar.Tactics.Typeclasses.solve; f_ZERO_pre = (fun (_: Prims.unit) -> true); f_ZERO_post = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Ntt.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Ntt.fst index 72a8bfad1..cd2dd7446 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Ntt.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Ntt.fst @@ -317,7 +317,7 @@ let ntt_multiply_binomials assert (forall k. (k <> 2 * v i /\ k <> 2 * v i + 1) ==> Seq.index out.f_elements k == Seq.index v__out0 k) in - let hax_temp_output:Prims.unit = admit () (* Panic freedom *) in + let _:Prims.unit = admit () (* Panic freedom *) in out #pop-options diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst index 03cede344..9e7f111dc 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst @@ -365,7 +365,7 @@ let serialize_5_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 10); Rust_primitives.Hax.array_of_list 10 list -let deserialize_1_ (v: t_Slice u8) = +let rec deserialize_1_ (v: t_Slice u8) = let result0:i16 = cast ((v.[ sz 0 ] <: u8) &. 1uy <: u8) <: i16 in let result1:i16 = cast (((v.[ sz 0 ] <: u8) >>! 1l <: u8) &. 1uy <: u8) <: i16 in let result2:i16 = cast (((v.[ sz 0 ] <: u8) >>! 2l <: u8) &. 1uy <: u8) <: i16 in @@ -421,7 +421,7 @@ let deserialize_1_lemma inputs = let deserialize_1_bounded_lemma inputs = admit() -let deserialize_10_ (bytes: t_Slice u8) = +let rec deserialize_10_ (bytes: t_Slice u8) = let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) = deserialize_10_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 10 } <: @@ -475,7 +475,7 @@ let deserialize_10_lemma inputs = let deserialize_10_bounded_lemma inputs = admit() -let deserialize_12_ (bytes: t_Slice u8) = +let rec deserialize_12_ (bytes: t_Slice u8) = let v0_1_:(i16 & i16) = deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 3 } <: @@ -571,7 +571,7 @@ let deserialize_12_lemma inputs = let deserialize_12_bounded_lemma inputs = admit() -let deserialize_4_ (bytes: t_Slice u8) = +let rec deserialize_4_ (bytes: t_Slice u8) = let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) = deserialize_4_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 4 } <: @@ -625,7 +625,7 @@ let deserialize_4_lemma inputs = let deserialize_4_bounded_lemma inputs = admit() -let serialize_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = +let rec serialize_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = let result0:u8 = (((((((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 0 ] <: i16) <: u8) |. ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 1 ] <: i16) @@ -742,7 +742,7 @@ let serialize_1_lemma inputs = #pop-options -let serialize_10_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = +let rec serialize_10_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = let r0_4_:(u8 & u8 & u8 & u8 & u8) = serialize_10_int (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ { Core.Ops.Range.f_start = sz 0; @@ -815,7 +815,7 @@ let serialize_10_lemma inputs = #pop-options -let serialize_12_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = +let rec serialize_12_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = let r0_2_:(u8 & u8 & u8) = serialize_12_int (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ { Core.Ops.Range.f_start = sz 0; @@ -928,7 +928,7 @@ let serialize_12_lemma inputs = #pop-options -let serialize_4_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = +let rec serialize_4_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) = let result0_3_:(u8 & u8 & u8 & u8) = serialize_4_int (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ { Core.Ops.Range.f_start = sz 0; diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fsti index 3e010f599..6344562a5 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fsti @@ -5,62 +5,62 @@ open FStar.Mul val deserialize_10_int (bytes: t_Slice u8) : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) - (requires Core.Slice.impl__len #u8 bytes =. sz 10) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 10) (fun _ -> Prims.l_True) val deserialize_11_int (bytes: t_Slice u8) : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) - (requires Core.Slice.impl__len #u8 bytes =. sz 11) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 11) (fun _ -> Prims.l_True) val deserialize_12_int (bytes: t_Slice u8) : Prims.Pure (i16 & i16) - (requires Core.Slice.impl__len #u8 bytes =. sz 3) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 3) (fun _ -> Prims.l_True) val deserialize_4_int (bytes: t_Slice u8) : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) - (requires Core.Slice.impl__len #u8 bytes =. sz 4) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 4) (fun _ -> Prims.l_True) val deserialize_5_int (bytes: t_Slice u8) : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) - (requires Core.Slice.impl__len #u8 bytes =. sz 5) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 5) (fun _ -> Prims.l_True) val serialize_10_int (v: t_Slice i16) : Prims.Pure (u8 & u8 & u8 & u8 & u8) - (requires Core.Slice.impl__len #i16 v =. sz 4) + (requires (Core.Slice.impl__len #i16 v <: usize) =. sz 4) (fun _ -> Prims.l_True) val serialize_11_int (v: t_Slice i16) : Prims.Pure (u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8) - (requires Core.Slice.impl__len #i16 v =. sz 8) + (requires (Core.Slice.impl__len #i16 v <: usize) =. sz 8) (fun _ -> Prims.l_True) val serialize_12_int (v: t_Slice i16) : Prims.Pure (u8 & u8 & u8) - (requires Core.Slice.impl__len #i16 v =. sz 2) + (requires (Core.Slice.impl__len #i16 v <: usize) =. sz 2) (fun _ -> Prims.l_True) val serialize_4_int (v: t_Slice i16) : Prims.Pure (u8 & u8 & u8 & u8) - (requires Core.Slice.impl__len #i16 v =. sz 8) + (requires (Core.Slice.impl__len #i16 v <: usize) =. sz 8) (fun _ -> Prims.l_True) val serialize_5_int (v: t_Slice i16) : Prims.Pure (u8 & u8 & u8 & u8 & u8) - (requires Core.Slice.impl__len #i16 v =. sz 8) + (requires (Core.Slice.impl__len #i16 v <: usize) =. sz 8) (fun _ -> Prims.l_True) val deserialize_11_ (bytes: t_Slice u8) : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector - (requires Core.Slice.impl__len #u8 bytes =. sz 22) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 22) (fun _ -> Prims.l_True) val deserialize_5_ (bytes: t_Slice u8) : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector - (requires Core.Slice.impl__len #u8 bytes =. sz 10) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 10) (fun _ -> Prims.l_True) val serialize_11_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) @@ -71,7 +71,7 @@ val serialize_5_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector val deserialize_1_ (v: t_Slice u8) : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector - (requires Core.Slice.impl__len #u8 v =. sz 2) + (requires (Core.Slice.impl__len #u8 v <: usize) =. sz 2) (fun _ -> Prims.l_True) val deserialize_1_lemma (inputs: t_Array u8 (sz 2)) : Lemma @@ -82,7 +82,7 @@ val deserialize_1_bounded_lemma (inputs: t_Array u8 (sz 2)) : Lemma val deserialize_10_ (bytes: t_Slice u8) : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector - (requires Core.Slice.impl__len #u8 bytes =. sz 20) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 20) (fun _ -> Prims.l_True) val deserialize_10_lemma (inputs: t_Array u8 (sz 20)) : Lemma @@ -93,7 +93,7 @@ val deserialize_10_bounded_lemma (inputs: t_Array u8 (sz 20)) : Lemma val deserialize_12_ (bytes: t_Slice u8) : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector - (requires Core.Slice.impl__len #u8 bytes =. sz 24) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 24) (fun _ -> Prims.l_True) val deserialize_12_lemma (inputs: t_Array u8 (sz 24)) : Lemma @@ -104,7 +104,7 @@ val deserialize_12_bounded_lemma (inputs: t_Array u8 (sz 24)) : Lemma val deserialize_4_ (bytes: t_Slice u8) : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector - (requires Core.Slice.impl__len #u8 bytes =. sz 8) + (requires (Core.Slice.impl__len #u8 bytes <: usize) =. sz 8) (fun _ -> Prims.l_True) val deserialize_4_lemma (inputs: t_Array u8 (sz 8)) : Lemma diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst index 7c018d9cf..e59261ebb 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst @@ -24,8 +24,8 @@ let serialize_5_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector let impl: Libcrux_ml_kem.Vector.Traits.t_Repr Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = { - _super_11581440318597584651 = FStar.Tactics.Typeclasses.solve; - _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; + _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve; + _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve; f_repr_pre = (fun (x: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true); f_repr_post = @@ -84,9 +84,9 @@ let serialize_4_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector let impl_1: Libcrux_ml_kem.Vector.Traits.t_Operations Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = { - _super_11581440318597584651 = FStar.Tactics.Typeclasses.solve; - _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; - _super_8706949974463268012 = FStar.Tactics.Typeclasses.solve; + _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve; + _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve; + _super_12682756204189288427 = FStar.Tactics.Typeclasses.solve; f_ZERO_pre = (fun (_: Prims.unit) -> true); f_ZERO_post = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst index 69e93a949..534f1aae9 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst @@ -12,24 +12,24 @@ let decompress_1_ = let z:v_T = f_ZERO #v_T #FStar.Tactics.Typeclasses.solve () in let _:Prims.unit = - assert (forall i. Seq.index (i1._super_8706949974463268012.f_repr z) i == 0s) + assert (forall i. Seq.index (i1._super_12682756204189288427.f_repr z) i == 0s) in let _:Prims.unit = assert (forall i. - let x = Seq.index (i1._super_8706949974463268012.f_repr vec) i in + let x = Seq.index (i1._super_12682756204189288427.f_repr vec) i in ((0 - v x) == 0 \/ (0 - v x) == - 1)) in let _:Prims.unit = assert (forall i. i < 16 ==> Spec.Utils.is_intb (pow2 15 - 1) - (0 - v (Seq.index (i1._super_8706949974463268012.f_repr vec) i))) + (0 - v (Seq.index (i1._super_12682756204189288427.f_repr vec) i))) in let s:v_T = f_sub #v_T #FStar.Tactics.Typeclasses.solve z vec in let _:Prims.unit = assert (forall i. - Seq.index (i1._super_8706949974463268012.f_repr s) i == 0s \/ - Seq.index (i1._super_8706949974463268012.f_repr s) i == (-1s)) + Seq.index (i1._super_12682756204189288427.f_repr s) i == 0s \/ + Seq.index (i1._super_12682756204189288427.f_repr s) i == (-1s)) in let _:Prims.unit = assert (i1.f_bitwise_and_with_constant_pre s 1665s) in f_bitwise_and_with_constant #v_T #FStar.Tactics.Typeclasses.solve s 1665s 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 21e6d6a50..8b0564a28 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 @@ -3,9 +3,21 @@ module Libcrux_ml_kem.Vector.Traits open Core open FStar.Mul +let v_BARRETT_SHIFT: i32 = 26l + +let v_BARRETT_R: i32 = 1l < pred: Type0{true ==> pred}; f_repr_post:v_Self -> t_Array i16 (sz 16) -> Type0; f_repr:x0: v_Self @@ -13,9 +25,9 @@ class t_Repr (v_Self: Type0) = { } class t_Operations (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_11581440318597584651:Core.Marker.t_Copy v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_8706949974463268012:t_Repr v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_13011033735201511749:Core.Marker.t_Copy v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_9529721400157967266:Core.Clone.t_Clone v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_12682756204189288427:t_Repr v_Self; f_ZERO_pre:x: Prims.unit -> pred: Type0 @@ -402,23 +414,11 @@ class t_Operations (v_Self: Type0) = { (fun result -> f_rej_sample_post x0 x1 result) } -let v_BARRETT_SHIFT: i32 = 26l - -let v_BARRETT_R: i32 = 1l < Prims.l_True) @@ -430,11 +430,11 @@ val to_standard_domain (#v_T: Type0) {| i1: t_Operations v_T |} (v: v_T) val to_unsigned_representative (#v_T: Type0) {| i1: t_Operations v_T |} (a: v_T) : Prims.Pure v_T - (requires Spec.Utils.is_i16b_array 3328 (i1._super_8706949974463268012.f_repr a)) + (requires Spec.Utils.is_i16b_array 3328 (i1._super_12682756204189288427.f_repr a)) (ensures fun result -> let result:v_T = result in forall i. - (let x = Seq.index (i1._super_8706949974463268012.f_repr a) i in - let y = Seq.index (i1._super_8706949974463268012.f_repr result) i in + (let x = Seq.index (i1._super_12682756204189288427.f_repr a) i in + let y = Seq.index (i1._super_12682756204189288427.f_repr result) i in (v y >= 0 /\ v y <= 3328 /\ (v y % 3329 == v x % 3329)))) diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs index a552ba5dd..bb893aed7 100644 --- a/libcrux-ml-kem/src/ind_cpa.rs +++ b/libcrux-ml-kem/src/ind_cpa.rs @@ -649,8 +649,6 @@ fn compress_then_serialize_u< assert (v ($OUT_LEN /! $K) == v $OUT_LEN / v $K); assert (v $OUT_LEN / v $K == 32 * v $COMPRESSION_FACTOR)" ); - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 cloop! { for (i, re) in input.into_iter().enumerate() { hax_lib::loop_invariant!(|i: usize| { fstar!(r#"(v $i < v $K ==> Seq.length out == v $OUT_LEN /\ @@ -684,8 +682,7 @@ fn compress_then_serialize_u< "Lib.Sequence.eq_intro #u8 #(v $OUT_LEN) out (Spec.MLKEM.compress_then_encode_u #$K (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector $input))" - ); - () + ) } /// This function implements Algorithm 13 of the diff --git a/libcrux-ml-kem/src/invert_ntt.rs b/libcrux-ml-kem/src/invert_ntt.rs index 1d87eea97..ac197a13a 100644 --- a/libcrux-ml-kem/src/invert_ntt.rs +++ b/libcrux-ml-kem/src/invert_ntt.rs @@ -35,8 +35,6 @@ pub(crate) fn invert_ntt_at_layer_1( hax_lib::fstar!(r#"reveal_opaque (`%invert_ntt_re_range_1) (invert_ntt_re_range_1 #$:Vector)"#); hax_lib::fstar!(r#"reveal_opaque (`%invert_ntt_re_range_2) (invert_ntt_re_range_2 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -72,7 +70,6 @@ pub(crate) fn invert_ntt_at_layer_1( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -87,8 +84,6 @@ pub(crate) fn invert_ntt_at_layer_2( ) { hax_lib::fstar!(r#"reveal_opaque (`%invert_ntt_re_range_2) (invert_ntt_re_range_2 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -119,7 +114,6 @@ pub(crate) fn invert_ntt_at_layer_2( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -134,8 +128,6 @@ pub(crate) fn invert_ntt_at_layer_3( ) { hax_lib::fstar!(r#"reveal_opaque (`%invert_ntt_re_range_2) (invert_ntt_re_range_2 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -165,7 +157,6 @@ pub(crate) fn invert_ntt_at_layer_3( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -201,8 +192,6 @@ pub(crate) fn invert_ntt_at_layer_4_plus( ) { let step = 1 << layer; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..(128 >> layer) { *zeta_i -= 1; @@ -220,7 +209,6 @@ pub(crate) fn invert_ntt_at_layer_4_plus( re.coefficients[j + step_vec] = y; } } - () } #[inline(always)] diff --git a/libcrux-ml-kem/src/ntt.rs b/libcrux-ml-kem/src/ntt.rs index 5ea2923c3..2434eafea 100644 --- a/libcrux-ml-kem/src/ntt.rs +++ b/libcrux-ml-kem/src/ntt.rs @@ -36,8 +36,6 @@ pub(crate) fn ntt_at_layer_1( hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_2) (ntt_re_range_2 #$:Vector)"#); hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_1) (ntt_re_range_1 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -73,7 +71,6 @@ pub(crate) fn ntt_at_layer_1( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -99,8 +96,6 @@ pub(crate) fn ntt_at_layer_2( hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_3) (ntt_re_range_3 #$:Vector)"#); hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_2) (ntt_re_range_2 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -131,7 +126,6 @@ pub(crate) fn ntt_at_layer_2( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -157,8 +151,6 @@ pub(crate) fn ntt_at_layer_3( hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_4) (ntt_re_range_4 #$:Vector)"#); hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_3) (ntt_re_range_3 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -187,7 +179,6 @@ pub(crate) fn ntt_at_layer_3( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -233,8 +224,6 @@ pub(crate) fn ntt_at_layer_4_plus( let step = 1 << layer; let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..(128 >> layer) { *zeta_i += 1; @@ -252,7 +241,6 @@ pub(crate) fn ntt_at_layer_4_plus( re.coefficients[j + step_vec] = y; } } - () } #[inline(always)] @@ -282,8 +270,6 @@ pub(crate) fn ntt_at_layer_4_plus( pub(crate) fn ntt_at_layer_7(re: &mut PolynomialRingElement) { let step = VECTORS_IN_RING_ELEMENT / 2; hax_lib::fstar!(r#"assert (v $step == 8)"#); - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for j in 0..step { hax_lib::loop_invariant!(|j: usize| { fstar!( @@ -297,7 +283,6 @@ pub(crate) fn ntt_at_layer_7(re: &mut PolynomialRingElement< re.coefficients[j + step] = Vector::sub(re.coefficients[j], &t); re.coefficients[j] = Vector::add(re.coefficients[j], &t); } - () } #[inline(always)] diff --git a/libcrux-ml-kem/src/polynomial.rs b/libcrux-ml-kem/src/polynomial.rs index 5b161c355..0b97d24ac 100644 --- a/libcrux-ml-kem/src/polynomial.rs +++ b/libcrux-ml-kem/src/polynomial.rs @@ -92,24 +92,18 @@ fn add_to_ring_element( myself: &mut PolynomialRingElement, rhs: &PolynomialRingElement, ) { - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..myself.coefficients.len() { myself.coefficients[i] = Vector::add(myself.coefficients[i], &rhs.coefficients[i]); } - () } #[inline(always)] #[hax_lib::fstar::verification_status(lax)] fn poly_barrett_reduce(myself: &mut PolynomialRingElement) { // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..VECTORS_IN_RING_ELEMENT { myself.coefficients[i] = Vector::barrett_reduce(myself.coefficients[i]); } - () } #[inline(always)] @@ -172,8 +166,6 @@ fn add_error_reduce( error: &PolynomialRingElement, ) { // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for j in 0..VECTORS_IN_RING_ELEMENT { let coefficient_normal_form = Vector::montgomery_multiply_by_constant(myself.coefficients[j], 1441); @@ -181,7 +173,6 @@ fn add_error_reduce( myself.coefficients[j] = Vector::barrett_reduce(Vector::add(coefficient_normal_form, &error.coefficients[j])); } - () } #[inline(always)] @@ -191,8 +182,6 @@ fn add_standard_error_reduce( error: &PolynomialRingElement, ) { // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for j in 0..VECTORS_IN_RING_ELEMENT { // The coefficients are of the form aR^{-1} mod q, which means // calling to_montgomery_domain() on them should return a mod q. @@ -201,7 +190,6 @@ fn add_standard_error_reduce( myself.coefficients[j] = Vector::barrett_reduce(Vector::add(coefficient_normal_form, &error.coefficients[j])); } - () } /// Given two `KyberPolynomialRingElement`s in their NTT representations, diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs index c63bf39a4..6c496a785 100644 --- a/libcrux-ml-kem/src/serialize.rs +++ b/libcrux-ml-kem/src/serialize.rs @@ -297,8 +297,6 @@ fn compress_then_serialize_4( serialized: &mut [u8], ) { hax_lib::fstar!(r#"assert_norm (pow2 4 == 16)"#); - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..VECTORS_IN_RING_ELEMENT { // NOTE: Using `$serialized` in loop_invariant doesn't work here hax_lib::loop_invariant!(|i: usize| { @@ -317,7 +315,6 @@ fn compress_then_serialize_4( let bytes = Vector::serialize_4(coefficient); serialized[8 * i..8 * i + 8].copy_from_slice(&bytes); } - () } #[inline(always)] @@ -332,8 +329,6 @@ fn compress_then_serialize_5( re: PolynomialRingElement, serialized: &mut [u8], ) { - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..VECTORS_IN_RING_ELEMENT { let coefficients = Vector::compress::<5>(to_unsigned_representative::(re.coefficients[i])); @@ -341,7 +336,6 @@ fn compress_then_serialize_5( let bytes = Vector::serialize_5(coefficients); serialized[10 * i..10 * i + 10].copy_from_slice(&bytes); } - () } #[inline(always)]