From 3400e59d1feb387080b9f52b64fb1dc6e954769e Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 29 Oct 2024 20:44:50 +0100 Subject: [PATCH] cleanup --- libcrux-intrinsics/Cargo.toml | 2 + .../Libcrux_intrinsics.Arm64_extract.fsti | 2 +- .../Libcrux_intrinsics.Avx2_extract.fsti | 348 +++++++----------- libcrux-intrinsics/src/arm64_extract.rs | 9 - libcrux-intrinsics/src/avx2_extract.rs | 158 +------- 5 files changed, 141 insertions(+), 378 deletions(-) diff --git a/libcrux-intrinsics/Cargo.toml b/libcrux-intrinsics/Cargo.toml index 144f7137d..cdc0acc2b 100644 --- a/libcrux-intrinsics/Cargo.toml +++ b/libcrux-intrinsics/Cargo.toml @@ -10,6 +10,8 @@ readme.workspace = true description = "Libcrux intrinsics crate" exclude = ["/proofs"] +[dependencies] + [features] simd128 = [] simd256 = [] diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti index d4014e6a8..a03c287ec 100644 --- a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti +++ b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti @@ -1,5 +1,5 @@ module Libcrux_intrinsics.Arm64_extract -#set-options "--fuel 0 --ifuel 1 --z3rlimit 80" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti index 16d93fb14..5ac496e48 100644 --- a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti +++ b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti @@ -1,301 +1,207 @@ module Libcrux_intrinsics.Avx2_extract -#set-options "--fuel 0 --ifuel 1 --z3rlimit 80" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -val mm256_movemask_ps (a: u8) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True) +val mm256_abs_epi32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + +val mm256_add_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + +val mm256_add_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + +val mm256_add_epi64 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + +val mm256_and_si256 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -unfold type t_Vec128 = bit_vec 128 -val vec128_as_i16x8 (x: bit_vec 128) : t_Array i16 (sz 8) -let get_lane128 (v: bit_vec 128) (i:nat{i < 8}) = Seq.index (vec128_as_i16x8 v) i +val mm256_andnot_si256 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -unfold type t_Vec256 = bit_vec 256 -val vec256_as_i16x16 (x: bit_vec 256) : t_Array i16 (sz 16) -let get_lane (v: bit_vec 256) (i:nat{i < 16}) = Seq.index (vec256_as_i16x16 v) i +val mm256_blend_epi16 (v_CONTROL: i32) (lhs rhs: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_abs_epi32 (a: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_blend_epi32 (v_CONTROL: i32) (lhs rhs: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_add_epi16 (lhs rhs: t_Vec256) - : Prims.Pure t_Vec256 - Prims.l_True - (ensures - fun result -> - let result:t_Vec256 = result in - vec256_as_i16x16 result == - Spec.Utils.map2 ( +. ) (vec256_as_i16x16 lhs) (vec256_as_i16x16 rhs)) +val mm256_bsrli_epi128 (v_SHIFT_BY: i32) (x: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_add_epi32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_castsi128_si256 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_add_epi64 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_castsi256_ps (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_andnot_si256 (a b: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_castsi256_si128 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_blend_epi16 (v_CONTROL: i32) (lhs rhs: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_cmpeq_epi32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_blend_epi32 (v_CONTROL: i32) (lhs rhs: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_cmpgt_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_bsrli_epi128 (v_SHIFT_BY: i32) (x: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_cmpgt_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_castsi128_si256 (vector: t_Vec128) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_cvtepi16_epi32 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_castsi256_ps (a: t_Vec256) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) +val mm256_extracti128_si256 (v_CONTROL: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_cmpeq_epi32 (a b: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_inserti128_si256 (v_CONTROL: i32) (vector vector_i128: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_cmpgt_epi16 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_loadu_si256_i16 (input: t_Slice i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_cmpgt_epi32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_loadu_si256_i32 (input: t_Slice i32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_cvtepi16_epi32 (vector: t_Vec128) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_loadu_si256_u8 (input: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_inserti128_si256 (v_CONTROL: i32) (vector: t_Vec256) (vector_i128: t_Vec128) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_madd_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_loadu_si256_i16 (input: t_Slice i16) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_movemask_ps (a: u8) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True) + +val mm256_mul_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_loadu_si256_i32 (input: t_Slice i32) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_mul_epu32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_loadu_si256_u8 (input: t_Slice u8) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_mulhi_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_mul_epi32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_mullo_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_mul_epu32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_mullo_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_mulhi_epi16 (lhs rhs: t_Vec256) - : Prims.Pure t_Vec256 - Prims.l_True - (ensures - fun result -> - let result:t_Vec256 = result in - vec256_as_i16x16 result == - Spec.Utils.map2 (fun x y -> cast (((cast x <: i32) *. (cast y <: i32)) >>! 16l) <: i16) - (vec256_as_i16x16 lhs) - (vec256_as_i16x16 rhs)) +val mm256_or_si256 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_mullo_epi32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_packs_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_or_si256 (a b: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_permute2x128_si256 (v_IMM8: i32) (a b: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_packs_epi32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_permute4x64_epi64 (v_CONTROL: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_permute2x128_si256 (v_IMM8: i32) (a b: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_permutevar8x32_epi32 (vector control: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_permute4x64_epi64 (v_CONTROL: i32) (vector: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_set1_epi16 (constant: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_permutevar8x32_epi32} +val mm256_set1_epi32 (constant: i32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_set1_epi32 (constant: i32) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_set1_epi64x (a: i64) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_set1_epi64x (a: i64) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_set_epi16 + (input15 input14 input13 input12 input11 input10 input9 input8 input7 input6 input5 input4 input3 input2 input1 input0: + i16) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_set_epi32} +val mm256_set_epi32 (input7 input6 input5 input4 input3 input2 input1 input0: i32) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) val mm256_set_epi64x (input3 input2 input1 input0: i64) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + +val mm256_set_epi8 + (byte31 byte30 byte29 byte28 byte27 byte26 byte25 byte24 byte23 byte22 byte21 byte20 byte19 byte18 byte17 byte16 byte15 byte14 byte13 byte12 byte11 byte10 byte9 byte8 byte7 byte6 byte5 byte4 byte3 byte2 byte1 byte0: + i8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + +val mm256_set_m128i (hi lo: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + +val mm256_setzero_si256: Prims.unit -> Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_set_epi8} +val mm256_shuffle_epi32 (v_CONTROL: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_set_m128i (hi lo: t_Vec128) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_shuffle_epi8 (vector control: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_setzero_si256: Prims.unit -> Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_sign_epi32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_shuffle_epi32 (v_CONTROL: i32) (vector: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_slli_epi16 (v_SHIFT_BY: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_shuffle_epi8} +val mm256_slli_epi32 (v_SHIFT_BY: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_sign_epi32 (a b: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_slli_epi64 (v_LEFT: i32) (x: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_slli_epi32 (v_SHIFT_BY: i32) (vector: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_sllv_epi32 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_slli_epi64 (v_LEFT: i32) (x: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_srai_epi16 (v_SHIFT_BY: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_sllv_epi32} +val mm256_srai_epi32 (v_SHIFT_BY: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_srai_epi16 (v_SHIFT_BY: i32) (vector: t_Vec256) - : Prims.Pure t_Vec256 - (requires v_SHIFT_BY >=. 0l && v_SHIFT_BY <. 16l) - (ensures - fun result -> - let result:t_Vec256 = result in - vec256_as_i16x16 result == - Spec.Utils.map_array (fun x -> x >>! v_SHIFT_BY) (vec256_as_i16x16 vector)) +val mm256_srli_epi16 (v_SHIFT_BY: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_srai_epi32 (v_SHIFT_BY: i32) (vector: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_srli_epi32 (v_SHIFT_BY: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_srli_epi32 (v_SHIFT_BY: i32) (vector: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_srli_epi64 (v_SHIFT_BY: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_srlv_epi32 (vector counts: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_srlv_epi32 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_srlv_epi64 (vector counts: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm256_srlv_epi64 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm256_storeu_si256_i16 (output: t_Slice i16) (vector: t_Vec256) - : Prims.Pure (t_Slice i16) - Prims.l_True - (ensures - fun output_future -> - let output_future:t_Slice i16 = output_future in - (Core.Slice.impl__len #i16 output_future <: usize) =. - (Core.Slice.impl__len #i16 output <: usize)) +val mm256_storeu_si256_i16 (output: t_Slice i16) (vector: u8) + : Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True) -val mm256_storeu_si256_i32 (output: t_Slice i32) (vector: t_Vec256) +val mm256_storeu_si256_i32 (output: t_Slice i32) (vector: u8) : Prims.Pure (t_Slice i32) Prims.l_True (fun _ -> Prims.l_True) -val mm256_storeu_si256_u8 (output: t_Slice u8) (vector: t_Vec256) +val mm256_storeu_si256_u8 (output: t_Slice u8) (vector: u8) : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True) -val mm256_sub_epi16 (lhs rhs: t_Vec256) - : Prims.Pure t_Vec256 - Prims.l_True - (ensures - fun result -> - let result:t_Vec256 = result in - vec256_as_i16x16 result == - Spec.Utils.map2 ( -. ) (vec256_as_i16x16 lhs) (vec256_as_i16x16 rhs)) - -val mm256_sub_epi32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) - -val mm256_testz_si256 (lhs rhs: t_Vec256) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True) - -val mm256_unpackhi_epi32 (lhs rhs: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) - -val mm256_unpackhi_epi64 (lhs rhs: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) - -val mm256_unpacklo_epi32 (lhs rhs: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) - -val mm256_unpacklo_epi64 (a b: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) - -val mm256_xor_si256 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) - -val mm_add_epi16 (lhs rhs: t_Vec128) - : Prims.Pure t_Vec128 - Prims.l_True - (ensures - fun result -> - let result:t_Vec128 = result in - vec128_as_i16x8 result == - Spec.Utils.map2 ( +. ) (vec128_as_i16x8 lhs) (vec128_as_i16x8 rhs)) - -include BitVec.Intrinsics {mm_loadu_si128} - -val mm_mulhi_epi16 (lhs rhs: t_Vec128) - : Prims.Pure t_Vec128 - Prims.l_True - (ensures - fun result -> - let result:t_Vec128 = result in - vec128_as_i16x8 result == - Spec.Utils.map2 (fun x y -> cast (((cast x <: i32) *. (cast y <: i32)) >>! 16l) <: i16) - (vec128_as_i16x8 lhs) - (vec128_as_i16x8 rhs)) - -val mm_mullo_epi16 (lhs rhs: t_Vec128) - : Prims.Pure t_Vec128 - Prims.l_True - (ensures - fun result -> - let result:t_Vec128 = result in - vec128_as_i16x8 result == - Spec.Utils.map2 mul_mod (vec128_as_i16x8 lhs) (vec128_as_i16x8 rhs)) - -val mm_set1_epi16 (constant: i16) - : Prims.Pure t_Vec128 - Prims.l_True - (ensures - fun result -> - let result:t_Vec128 = result in - vec128_as_i16x8 result == Spec.Utils.create (sz 8) constant) +val mm256_sub_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm_set_epi32 (input3 input2 input1 input0: i32) - : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True) +val mm256_sub_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm_set_epi8} +val mm256_testz_si256 (lhs rhs: u8) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm_shuffle_epi8} +val mm256_unpackhi_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm_sllv_epi32 (vector counts: t_Vec128) - : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True) +val mm256_unpackhi_epi64 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm_srli_epi64 (v_SHIFT_BY: i32) (vector: t_Vec128) - : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True) +val mm256_unpacklo_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm_storeu_bytes_si128} +val mm256_unpacklo_epi64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm_storeu_si128 (output: t_Slice i16) (vector: t_Vec128) - : Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True) +val mm256_xor_si256 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm_storeu_si128_i32 (output: t_Slice i32) (vector: t_Vec128) - : Prims.Pure (t_Slice i32) Prims.l_True (fun _ -> Prims.l_True) +val mm_add_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + +val mm_loadu_si128 (input: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -val mm_sub_epi16 (lhs rhs: t_Vec128) - : Prims.Pure t_Vec128 - Prims.l_True - (ensures - fun result -> - let result:t_Vec128 = result in - vec128_as_i16x8 result == - Spec.Utils.map2 ( -. ) (vec128_as_i16x8 lhs) (vec128_as_i16x8 rhs)) +val mm_movemask_epi8 (vector: u8) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True) -val vec256_blendv_epi32 (a b mask: t_Vec256) - : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) +val mm_mulhi_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_and_si256 as mm256_and_si256} -val lemma_mm256_and_si256 lhs rhs - : Lemma ( vec256_as_i16x16 (mm256_and_si256 lhs rhs) - == Spec.Utils.map2 (&.) (vec256_as_i16x16 lhs) (vec256_as_i16x16 rhs) - ) - [SMTPat (vec256_as_i16x16 (mm256_and_si256 lhs rhs))] +val mm_mullo_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_castsi256_si128 as mm256_castsi256_si128} +val mm_packs_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_extracti128_si256 as mm256_extracti128_si256} +val mm_set1_epi16 (constant: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_madd_epi16 as mm256_madd_epi16} +val mm_set_epi32 (input3 input2 input1 input0: i32) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_mullo_epi16 as mm256_mullo_epi16} -let lemma_mm256_mullo_epi16 v1 v2 : - Lemma (vec256_as_i16x16 (mm256_mullo_epi16 v1 v2) == - Spec.Utils.map2 mul_mod (vec256_as_i16x16 v1) (vec256_as_i16x16 v2)) - [SMTPat (vec256_as_i16x16 (mm256_mullo_epi16 v1 v2))] = admit() +val mm_set_epi8 + (byte15 byte14 byte13 byte12 byte11 byte10 byte9 byte8 byte7 byte6 byte5 byte4 byte3 byte2 byte1 byte0: + u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_set1_epi16 as mm256_set1_epi16} -val lemma_mm256_set1_epi16 constant - : Lemma ( vec256_as_i16x16 (mm256_set1_epi16 constant) - == Spec.Utils.create (sz 16) constant - ) - [SMTPat (vec256_as_i16x16 (mm256_set1_epi16 constant))] +val mm_shuffle_epi8 (vector control: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_set_epi16 as mm256_set_epi16} -let lemma_mm256_set_epi16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0 : - Lemma (vec256_as_i16x16 (mm256_set_epi16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0) == - Spec.Utils.create16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15) - [SMTPat (vec256_as_i16x16 (mm256_set_epi16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0))] = admit() +val mm_sllv_epi32 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_slli_epi16 as mm256_slli_epi16} +val mm_srli_epi64 (v_SHIFT_BY: i32) (vector: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_srli_epi16 as mm256_srli_epi16} +val mm_storeu_bytes_si128 (output: t_Slice u8) (vector: u8) + : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm256_srli_epi64 as mm256_srli_epi64} +val mm_storeu_si128 (output: t_Slice i16) (vector: u8) + : Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True) + +val mm_storeu_si128_i32 (output: t_Slice i32) (vector: u8) + : Prims.Pure (t_Slice i32) Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm_movemask_epi8 as mm_movemask_epi8} +val mm_sub_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) -include BitVec.Intrinsics {mm_packs_epi16 as mm_packs_epi16} +val vec256_blendv_epi32 (a b mask: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-intrinsics/src/arm64_extract.rs b/libcrux-intrinsics/src/arm64_extract.rs index d41241275..e43abc8f4 100644 --- a/libcrux-intrinsics/src/arm64_extract.rs +++ b/libcrux-intrinsics/src/arm64_extract.rs @@ -3,23 +3,14 @@ #![allow(non_camel_case_types, unsafe_code, unused_variables)] -#[hax_lib::opaque_type] pub type _uint16x4_t = u8; -#[hax_lib::opaque_type] pub type _int16x4_t = u8; -#[hax_lib::opaque_type] pub type _int16x8_t = u8; -#[hax_lib::opaque_type] pub type _uint8x16_t = u8; -#[hax_lib::opaque_type] pub type _uint16x8_t = u8; -#[hax_lib::opaque_type] pub type _uint32x4_t = u8; -#[hax_lib::opaque_type] pub type _int32x4_t = u8; -#[hax_lib::opaque_type] pub type _uint64x2_t = u8; -#[hax_lib::opaque_type] pub type _int64x2_t = u8; #[inline(always)] diff --git a/libcrux-intrinsics/src/avx2_extract.rs b/libcrux-intrinsics/src/avx2_extract.rs index ce78d81e5..8afb4ab49 100644 --- a/libcrux-intrinsics/src/avx2_extract.rs +++ b/libcrux-intrinsics/src/avx2_extract.rs @@ -3,33 +3,7 @@ #![allow(unused_variables, non_camel_case_types)] -#[cfg(hax)] -#[derive(Clone, Copy)] -#[hax_lib::fstar::replace( - interface, - r#" -unfold type $:{Vec256} = bit_vec 256 -val vec256_as_i16x16 (x: bit_vec 256) : t_Array i16 (sz 16) -let get_lane (v: bit_vec 256) (i:nat{i < 16}) = Seq.index (vec256_as_i16x16 v) i -"# -)] -pub struct Vec256(u8); - -#[cfg(hax)] -#[derive(Copy, Clone)] -#[hax_lib::fstar::replace( - interface, - r#" -unfold type $:{Vec128} = bit_vec 128 -val vec128_as_i16x8 (x: bit_vec 128) : t_Array i16 (sz 8) -let get_lane128 (v: bit_vec 128) (i:nat{i < 8}) = Seq.index (vec128_as_i16x8 v) i -"# -)] -pub struct Vec128(u8); - -#[cfg(not(hax))] pub type Vec256 = u8; -#[cfg(not(hax))] pub type Vec128 = u8; pub type Vec256Float = u8; @@ -37,8 +11,6 @@ pub fn mm256_storeu_si256_u8(output: &mut [u8], vector: Vec256) { debug_assert_eq!(output.len(), 32); unimplemented!() } - -#[hax_lib::ensures(|()| future(output).len() == output.len())] pub fn mm256_storeu_si256_i16(output: &mut [i16], vector: Vec256) { debug_assert_eq!(output.len(), 16); unimplemented!() @@ -57,13 +29,11 @@ pub fn mm_storeu_si128_i32(output: &mut [i32], vector: Vec128) { unimplemented!() } -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm_storeu_bytes_si128}")] pub fn mm_storeu_bytes_si128(output: &mut [u8], vector: Vec128) { debug_assert_eq!(output.len(), 16); unimplemented!() } -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm_loadu_si128}")] pub fn mm_loadu_si128(input: &[u8]) -> Vec128 { debug_assert_eq!(input.len(), 16); unimplemented!() @@ -89,7 +59,6 @@ pub fn mm256_set_m128i(hi: Vec128, lo: Vec128) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm_set_epi8}")] pub fn mm_set_epi8( byte15: u8, byte14: u8, @@ -111,7 +80,6 @@ pub fn mm_set_epi8( unimplemented!() } -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm256_set_epi8}")] pub fn mm256_set_epi8( byte31: i8, byte30: i8, @@ -149,33 +117,9 @@ pub fn mm256_set_epi8( unimplemented!() } -#[hax_lib::ensures(|result| fstar!("vec256_as_i16x16 $result == - Spec.Utils.create (sz 16) $constant"))] -#[hax_lib::fstar::replace( - interface, - r#" -include BitVec.Intrinsics {mm256_set1_epi16 as ${mm256_set1_epi16}} -val lemma_mm256_set1_epi16 constant - : Lemma ( vec256_as_i16x16 (mm256_set1_epi16 constant) - == Spec.Utils.create (sz 16) constant - ) - [SMTPat (vec256_as_i16x16 (mm256_set1_epi16 constant))] -"# -)] pub fn mm256_set1_epi16(constant: i16) -> Vec256 { unimplemented!() } - -#[hax_lib::fstar::replace( - interface, - r#" -include BitVec.Intrinsics {mm256_set_epi16 as ${mm256_set_epi16}} -let lemma_mm256_set_epi16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0 : - Lemma (vec256_as_i16x16 (${mm256_set_epi16} v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0) == - Spec.Utils.create16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15) - [SMTPat (vec256_as_i16x16 (${mm256_set_epi16} v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0))] = admit() -"# -)] pub fn mm256_set_epi16( input15: i16, input14: i16, @@ -197,8 +141,6 @@ pub fn mm256_set_epi16( unimplemented!() } -#[hax_lib::ensures(|result| fstar!("vec128_as_i16x8 $result == - Spec.Utils.create (sz 8) $constant"))] #[inline(always)] pub fn mm_set1_epi16(constant: i16) -> Vec128 { unimplemented!() @@ -213,8 +155,6 @@ pub fn mm256_set1_epi32(constant: i32) -> Vec256 { pub fn mm_set_epi32(input3: i32, input2: i32, input1: i32, input0: i32) -> Vec128 { unimplemented!() } - -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm256_set_epi32}")] #[inline(always)] pub fn mm256_set_epi32( input7: i32, @@ -229,27 +169,15 @@ pub fn mm256_set_epi32( unimplemented!() } -#[hax_lib::ensures(|result| fstar!("vec128_as_i16x8 $result == - Spec.Utils.map2 (+.) (vec128_as_i16x8 $lhs) (vec128_as_i16x8 $rhs)"))] +#[inline(always)] pub fn mm_add_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 { unimplemented!() } - -#[hax_lib::ensures(|result| fstar!("vec128_as_i16x8 $result == - Spec.Utils.map2 (-.) (vec128_as_i16x8 $lhs) (vec128_as_i16x8 $rhs)"))] -pub fn mm_sub_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 { - unimplemented!() -} - -#[hax_lib::ensures(|result| fstar!("vec256_as_i16x16 $result == - Spec.Utils.map2 (+.) (vec256_as_i16x16 $lhs) (vec256_as_i16x16 $rhs)"))] +#[inline(always)] pub fn mm256_add_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace( - interface, - "include BitVec.Intrinsics {mm256_madd_epi16 as ${mm256_madd_epi16}}" -)] +#[inline(always)] pub fn mm256_madd_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } @@ -258,12 +186,6 @@ pub fn mm256_add_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::ensures(|result| fstar!("vec256_as_i16x16 $result == - Spec.Utils.map2 (-.) (vec256_as_i16x16 $lhs) (vec256_as_i16x16 $rhs)"))] -pub fn mm256_sub_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 { - unimplemented!() -} - #[inline(always)] pub fn mm256_add_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() @@ -274,26 +196,21 @@ pub fn mm256_abs_epi32(a: Vec256) -> Vec256 { unimplemented!() } +pub fn mm256_sub_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 { + unimplemented!() +} pub fn mm256_sub_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace( - interface, - r#" -include BitVec.Intrinsics {mm256_mullo_epi16 as ${mm256_mullo_epi16}} -let lemma_mm256_mullo_epi16 v1 v2 : - Lemma (vec256_as_i16x16 (${mm256_mullo_epi16} v1 v2) == - Spec.Utils.map2 mul_mod (vec256_as_i16x16 v1) (vec256_as_i16x16 v2)) - [SMTPat (vec256_as_i16x16 (${mm256_mullo_epi16} v1 v2))] = admit() -"# -)] +pub fn mm_sub_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 { + unimplemented!() +} + pub fn mm256_mullo_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::ensures(|result| fstar!("vec128_as_i16x8 $result == - Spec.Utils.map2 mul_mod (vec128_as_i16x8 $lhs) (vec128_as_i16x8 $rhs)"))] pub fn mm_mullo_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 { unimplemented!() } @@ -326,9 +243,6 @@ pub fn mm256_movemask_ps(a: Vec256Float) -> i32 { unimplemented!() } -#[hax_lib::ensures(|result| fstar!("vec128_as_i16x8 $result == - Spec.Utils.map2 (fun x y -> cast (((cast x <: i32) *. (cast y <: i32)) >>! 16l) <: i16) - (vec128_as_i16x8 $lhs) (vec128_as_i16x8 $rhs)"))] pub fn mm_mulhi_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 { unimplemented!() } @@ -337,8 +251,6 @@ pub fn mm256_mullo_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::ensures(|result| fstar!("vec256_as_i16x16 $result == - Spec.Utils.map2 (fun x y -> cast (((cast x <: i32) *. (cast y <: i32)) >>! 16l) <: i16) (vec256_as_i16x16 $lhs) (vec256_as_i16x16 $rhs)"))] pub fn mm256_mulhi_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } @@ -352,17 +264,6 @@ pub fn mm256_mul_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace( - interface, - r#" -include BitVec.Intrinsics {mm256_and_si256 as ${mm256_and_si256}} -val lemma_mm256_and_si256 lhs rhs - : Lemma ( vec256_as_i16x16 (mm256_and_si256 lhs rhs) - == Spec.Utils.map2 (&.) (vec256_as_i16x16 lhs) (vec256_as_i16x16 rhs) - ) - [SMTPat (vec256_as_i16x16 (mm256_and_si256 lhs rhs))] -"# -)] #[inline(always)] pub fn mm256_and_si256(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() @@ -381,9 +282,6 @@ pub fn mm256_xor_si256(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::requires(SHIFT_BY >= 0 && SHIFT_BY < 16)] -#[hax_lib::ensures(|result| fstar!("vec256_as_i16x16 $result == - Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (vec256_as_i16x16 $vector)"))] pub fn mm256_srai_epi16(vector: Vec256) -> Vec256 { debug_assert!(SHIFT_BY >= 0 && SHIFT_BY < 16); unimplemented!() @@ -393,10 +291,6 @@ pub fn mm256_srai_epi32(vector: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace( - interface, - "include BitVec.Intrinsics {mm256_srli_epi16 as ${mm256_srli_epi16::<0>}}" -)] pub fn mm256_srli_epi16(vector: Vec256) -> Vec256 { debug_assert!(SHIFT_BY >= 0 && SHIFT_BY < 16); unimplemented!() @@ -410,20 +304,11 @@ pub fn mm_srli_epi64(vector: Vec128) -> Vec128 { debug_assert!(SHIFT_BY >= 0 && SHIFT_BY < 64); unimplemented!() } - -#[hax_lib::fstar::replace( - interface, - "include BitVec.Intrinsics {mm256_srli_epi64 as ${mm256_srli_epi64::<0>}}" -)] pub fn mm256_srli_epi64(vector: Vec256) -> Vec256 { debug_assert!(SHIFT_BY >= 0 && SHIFT_BY < 64); unimplemented!() } -#[hax_lib::fstar::replace( - interface, - "include BitVec.Intrinsics {mm256_slli_epi16 as ${mm256_slli_epi16::<0>}}" -)] pub fn mm256_slli_epi16(vector: Vec256) -> Vec256 { debug_assert!(SHIFT_BY >= 0 && SHIFT_BY < 16); unimplemented!() @@ -434,11 +319,9 @@ pub fn mm256_slli_epi32(vector: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm_shuffle_epi8}")] pub fn mm_shuffle_epi8(vector: Vec128, control: Vec128) -> Vec128 { unimplemented!() } -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm256_shuffle_epi8}")] pub fn mm256_shuffle_epi8(vector: Vec256, control: Vec256) -> Vec256 { unimplemented!() } @@ -464,10 +347,6 @@ pub fn mm256_unpackhi_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace( - interface, - "include BitVec.Intrinsics {mm256_castsi256_si128 as ${mm256_castsi256_si128}}" -)] pub fn mm256_castsi256_si128(vector: Vec256) -> Vec128 { unimplemented!() } @@ -479,10 +358,6 @@ pub fn mm256_cvtepi16_epi32(vector: Vec128) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace( - interface, - "include BitVec.Intrinsics {mm_packs_epi16 as ${mm_packs_epi16}}" -)] pub fn mm_packs_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 { unimplemented!() } @@ -490,10 +365,6 @@ pub fn mm256_packs_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace( - interface, - "include BitVec.Intrinsics {mm256_extracti128_si256 as ${mm256_extracti128_si256::<0>}}" -)] pub fn mm256_extracti128_si256(vector: Vec256) -> Vec128 { debug_assert!(CONTROL == 0 || CONTROL == 1); unimplemented!() @@ -523,21 +394,17 @@ pub fn vec256_blendv_epi32(a: Vec256, b: Vec256, mask: Vec256) -> Vec256 { unimplemented!() } -#[hax_lib::fstar::replace( - interface, - "include BitVec.Intrinsics {mm_movemask_epi8 as ${mm_movemask_epi8}}" -)] #[inline(always)] pub fn mm_movemask_epi8(vector: Vec128) -> i32 { unimplemented!() } -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm256_permutevar8x32_epi32}")] #[inline(always)] pub fn mm256_permutevar8x32_epi32(vector: Vec256, control: Vec256) -> Vec256 { unimplemented!() } +#[inline(always)] pub fn mm256_srlv_epi32(vector: Vec256, counts: Vec256) -> Vec256 { unimplemented!() } @@ -549,9 +416,6 @@ pub fn mm256_srlv_epi64(vector: Vec256, counts: Vec256) -> Vec256 { pub fn mm_sllv_epi32(vector: Vec128, counts: Vec128) -> Vec128 { unimplemented!() } - -#[inline(always)] -#[hax_lib::fstar::replace(interface, "include BitVec.Intrinsics {mm256_sllv_epi32}")] pub fn mm256_sllv_epi32(vector: Vec256, counts: Vec256) -> Vec256 { unimplemented!() }