Merge branch 'dev' into dev-panic-free

cryspen · Dec 15, 2024 · 29e08c7 · 29e08c7
2 parents cb45a8e + 0fc11d0
commit 29e08c7
Show file tree

Hide file tree

Showing 27 changed files with 285 additions and 116 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti
@@ -9,10 +9,22 @@ 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
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_3:Core.Clone.t_Clone t_Vec128
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_2:Core.Marker.t_Copy t_Vec128
+
 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
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl:Core.Clone.t_Clone t_Vec256
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_1:Core.Marker.t_Copy t_Vec256
+
 val mm256_abs_epi32 (a: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
 
 val mm256_add_epi16 (lhs rhs: t_Vec256)

diff --git a/libcrux-intrinsics/src/arm64_extract.rs b/libcrux-intrinsics/src/arm64_extract.rs
@@ -3,23 +3,23 @@
 
 #![allow(non_camel_case_types, unsafe_code, unused_variables)]
 
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _uint16x4_t = u8;
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _int16x4_t = u8;
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _int16x8_t = u8;
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _uint8x16_t = u8;
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _uint16x8_t = u8;
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _uint32x4_t = u8;
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _int32x4_t = u8;
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _uint64x2_t = u8;
-#[hax_lib::opaque_type]
+#[hax_lib::opaque]
 pub type _int64x2_t = u8;
 
 #[inline(always)]

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti
@@ -6,7 +6,7 @@ open FStar.Mul
 /// The state.
 /// It\'s only used for SHAKE128.
 /// All other functions don\'t actually use any members.
-val t_Simd256Hash:Type0
+val t_Simd256Hash:eqtype
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd256Hash v_K

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti
@@ -6,7 +6,7 @@ open FStar.Mul
 /// The state.
 /// It\'s only used for SHAKE128.
 /// All other functions don\'t actually use any members.
-val t_Simd128Hash:Type0
+val t_Simd128Hash:eqtype
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd128Hash v_K

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti
@@ -6,7 +6,7 @@ open FStar.Mul
 /// The state.
 /// It\'s only used for SHAKE128.
 /// All other functions don\'t actually use any members.
-val t_PortableHash (v_K: usize) : Type0
+val t_PortableHash (v_K: usize) : eqtype
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash (t_PortableHash v_K) v_K