diff --git a/proof-libs/fstar/core/Core.Array.fst b/proof-libs/fstar/core/Core.Array.fst
index c17a58262..44f48c19a 100644
--- a/proof-libs/fstar/core/Core.Array.fst
+++ b/proof-libs/fstar/core/Core.Array.fst
@@ -3,8 +3,10 @@ open Rust_primitives
 
 type t_TryFromSliceError = | TryFromSliceError
 
-let impl_23__map #a #b n (arr: t_Array a n) (f: a -> b): t_Array b n 
+let impl_23__map #a n #b (arr: t_Array a n) (f: a -> b): t_Array b n 
   = map_array arr f
 
 let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 
+let from_fn #a len (f: usize -> a): t_Array a len = admit()
+
diff --git a/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti b/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti
index 5772fa15c..08219c554 100644
--- a/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti
+++ b/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti
@@ -1,6 +1,7 @@
 module Core.Core_arch.Arm_shared.Neon
 
 val t_int16x4_t:Type0
+val t_int16x8_t:Type0
 val t_int32x2_t:Type0
 val t_int32x4_t:Type0
 val t_int64x2_t:Type0
diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.fsti
index 6cae37564..5056e0e34 100644
--- a/proof-libs/fstar/core/Core.Core_arch.X86.fsti
+++ b/proof-libs/fstar/core/Core.Core_arch.X86.fsti
@@ -1,3 +1,5 @@
 module Core.Core_arch.X86
 
+val t____m128i:Type0
+
 val t____m256i:Type0
diff --git a/proof-libs/fstar/core/Core.Hint.fsti b/proof-libs/fstar/core/Core.Hint.fsti
new file mode 100644
index 000000000..ad1d9e6b6
--- /dev/null
+++ b/proof-libs/fstar/core/Core.Hint.fsti
@@ -0,0 +1,3 @@
+module Core.Hint
+
+val black_box: #a:Type0 -> x:a -> y:a{y == x}
\ No newline at end of file
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
index 12de64b69..8e8af77d7 100644
--- a/proof-libs/fstar/core/Core.Num.fsti
+++ b/proof-libs/fstar/core/Core.Num.fsti
@@ -38,8 +38,11 @@ val impl__u16__pow (base: u16) (exponent: u32): result : u16 {v base == 2 /\ v e
 val impl__u32__pow (base: u32) (exponent: u32): result : u32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.U32 (pow2 (v exponent))}
 val impl__u64__pow: u64 -> u32 -> u64
 val impl__u128__pow: u128 -> u32 -> u128
+val impl__i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 15 ==> result == mk_int #Lib.IntTypes.S16 (pow2 (v exponent))}
 val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.S32 (pow2 (v exponent))}
 
+val impl__u8__count_ones: u8 -> u32
+
 val impl__u8__from_str_radix: string -> u32 -> Core.Result.t_Result u8 Core.Num.Error.t_ParseIntError
 
 val impl__usize__ilog2: i32 -> u32