diff --git a/proof-libs/fstar/core/Alloc.Boxed.fst b/proof-libs/fstar/core/Alloc.Boxed.fst
index fb46eea30..c5aa5553c 100644
--- a/proof-libs/fstar/core/Alloc.Boxed.fst
+++ b/proof-libs/fstar/core/Alloc.Boxed.fst
@@ -1,3 +1,5 @@
 module Alloc.Boxed
 
 type t_Box t t_Global = t
+
+assume val impl__pin #t (x: t) : Core.Pin.t_Pin (t_Box t Alloc.Alloc.t_Global)
diff --git a/proof-libs/fstar/core/Alloc.Slice.fst b/proof-libs/fstar/core/Alloc.Slice.fst
index 2927bcc63..614a8b865 100644
--- a/proof-libs/fstar/core/Alloc.Slice.fst
+++ b/proof-libs/fstar/core/Alloc.Slice.fst
@@ -3,3 +3,5 @@ open Rust_primitives.Arrays
 open Alloc.Vec
 
 let impl__to_vec #a (s: t_Slice a): t_Vec a Alloc.Alloc.t_Global = s
+
+let impl__into_vec #a #t (s: t_Slice a): t_Vec a t= s
diff --git a/proof-libs/fstar/core/Alloc.Vec.fst b/proof-libs/fstar/core/Alloc.Vec.fst
index 6e3b411e1..42aa58a32 100644
--- a/proof-libs/fstar/core/Alloc.Vec.fst
+++ b/proof-libs/fstar/core/Alloc.Vec.fst
@@ -3,6 +3,7 @@ open Rust_primitives
 
 unfold type t_Vec t (_: unit) = s:t_Slice t
 
+
 let impl__new #t (): t_Vec t () = FStar.Seq.empty
 
 let impl_2__extend_from_slice #t (#[(Tactics.exact (`()))]alloc:unit) (self: t_Vec t alloc) (other: t_Slice t{Seq.length self + Seq.length other <= max_usize}): t_Vec t alloc
@@ -38,3 +39,6 @@ instance update_at_tc_array t n: update_at_tc (t_Vec t ()) (int_t n) = {
 
 let impl_1__is_empty #t (#[(Tactics.exact (`()))]alloc:unit) (v: t_Vec t alloc): bool =
   Seq.length v = 0
+
+
+
diff --git a/proof-libs/fstar/core/Core.Pin.fsti b/proof-libs/fstar/core/Core.Pin.fsti
new file mode 100644
index 000000000..16f5d3098
--- /dev/null
+++ b/proof-libs/fstar/core/Core.Pin.fsti
@@ -0,0 +1,7 @@
+module Core.Pin
+
+val t_Pin (v_T: Type0) : eqtype
+
+val impl_6__as_ref #t (x: t_Pin t): t_Pin t
+
+val impl_8__into_inner_unchecked #t (x: t_Pin t): t
diff --git a/proof-libs/fstar/core/Core.Ptr.Non_null.fsti b/proof-libs/fstar/core/Core.Ptr.Non_null.fsti
new file mode 100644
index 000000000..144534ea4
--- /dev/null
+++ b/proof-libs/fstar/core/Core.Ptr.Non_null.fsti
@@ -0,0 +1,3 @@
+module Core.Ptr.Non_null
+
+val t_NonNull (v_T: Type0) : eqtype
\ No newline at end of file
diff --git a/proof-libs/fstar/core/Core.Result.fst b/proof-libs/fstar/core/Core.Result.fst
index ab3cd15d9..9c976c178 100644
--- a/proof-libs/fstar/core/Core.Result.fst
+++ b/proof-libs/fstar/core/Core.Result.fst
@@ -21,3 +21,8 @@ let impl__and_then #t #e #u (self: t_Result t e) (op: t -> t_Result u e): t_Resu
   match self with 
   | Result_Ok v -> op v 
   | Result_Err e -> Result_Err e
+
+let impl__is_err #t #e (self: t_Result t e) : bool =
+  match self with 
+  | Result_Ok v -> true
+  | Result_Err e -> false
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
index f009fd4c0..e6e4bd603 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
+++ b/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