Various F* core lib additions.

proof-libs/fstar/core/Alloc.Slice.fsti

@@ -4,4 +4,6 @@ open Alloc.Vec
 
 let impl__to_vec #a (s: t_Slice a): t_Vec a Alloc.Alloc.t_Global = s
 
+let impl__into_vec #t #a (s: Alloc.Boxed.t_Box (t_Slice t) a): t_Vec t a = s
+
 val impl__concat #t1 #t2 (s: t_Slice t1): t_Slice t2

proof-libs/fstar/core/Core.Cmp.fsti

@@ -51,3 +51,9 @@ val ord_u64: t_Ord u64
 
 [@FStar.Tactics.Typeclasses.tcinstance]
 val ord_reverse t {| t_Ord t |}: t_Ord (t_Reverse t)
+
+class t_Eq (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_14765399066043115604:Core.Cmp.t_PartialEq
+    v_Self v_Self
+}
+

proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti

@@ -0,0 +1,3 @@
+module Core.Core_arch.X86.Pclmulqdq
+
+val v__mm_clmulepi64_si128 : Rust_primitives.Integers.i32 -> Core.Core_arch.X86.t____m128i -> Core.Core_arch.X86.t____m128i -> Core.Core_arch.X86.t____m128i

proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti

@@ -0,0 +1,3 @@
+module Core.Core_arch.X86.Sse2
+
+val v__mm_set_epi64x: Rust_primitives.Integers.i64 -> Rust_primitives.Integers.i64 -> Core.Core_arch.X86.t____m128i

proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti

@@ -0,0 +1,3 @@
+module Core.Core_arch.X86_64_.Sse2
+
+val v__mm_cvtsi128_si64: Core.Core_arch.X86.t____m128i -> Rust_primitives.Integers.i64

proof-libs/fstar/core/Core.Marker.fst

@@ -48,3 +48,7 @@ class t_Clone (h: Type) = {
 instance t_Clone_all t: t_Clone t = {
   dummy_clone_field = ()
 }
+
+class t_StructuralPartialEq (h: Type) = {
+  dummy_eq_field: unit
+}

proof-libs/fstar/core/Core.Num.fsti

@@ -7,6 +7,7 @@ let impl__u8__wrapping_add: u8 -> u8 -> u8 = add_mod
 let impl__u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod
 let impl__u16__wrapping_add: u16 -> u16 ->  u16 = add_mod
 val impl__u16__to_be_bytes: u16 -> t_Array u8 (sz 2)
+val impl__u16__from_be_bytes: t_Array u8 (sz 2) -> u16
 let impl__i32__wrapping_add: i32 -> i32 -> i32 = add_mod
 let impl__i32__abs (a:i32{minint i32_inttype < v a}) : i32 = abs_int a
 

proof-libs/fstar/core/Core.Slice.fsti

@@ -27,6 +27,7 @@ instance impl__index t n: t_Index (t_Slice t) (int_t n)
     }
 
 let impl__copy_from_slice #t (x: t_Slice t) (y:t_Slice t) : t_Slice t = y
+let impl__clone_from_slice #t (x: t_Slice t) (y:t_Slice t) : t_Slice t = y
 
 val impl__split_at #t (s: t_Slice t) (mid: usize): Pure (t_Slice t * t_Slice t)
     (requires (v mid <= Seq.length s))

proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst

@@ -55,3 +55,5 @@ unfold let array_of_list (#t:Type)
   (l: list t {FStar.List.Tot.length l == n})
   : t_Array t (sz n)
   = Seq.seq_of_list l
+
+let box_new (#t:Type) (v: t): Alloc.Boxed.t_Box t Alloc.Alloc.t_Global = v