F* core changes for type-checking of sandwixh.

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)

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

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
+
+
+

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

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

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

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