diff --git a/proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti b/proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti
new file mode 100644
index 000000000..990c55d41
--- /dev/null
+++ b/proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti
@@ -0,0 +1,3 @@
+module Alloc.Collections.Btree.Set
+
+val t_BTreeSet (t:Type0) (u:unit): eqtype
diff --git a/proof-libs/fstar/core/Alloc.Slice.fst b/proof-libs/fstar/core/Alloc.Slice.fsti
similarity index 70%
rename from proof-libs/fstar/core/Alloc.Slice.fst
rename to proof-libs/fstar/core/Alloc.Slice.fsti
index 2927bcc63..82a01332d 100644
--- a/proof-libs/fstar/core/Alloc.Slice.fst
+++ b/proof-libs/fstar/core/Alloc.Slice.fsti
@@ -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
+
+val impl__concat #t1 #t2 (s: t_Slice t1): t_Slice t2
diff --git a/proof-libs/fstar/core/Alloc.Vec.fst b/proof-libs/fstar/core/Alloc.Vec.fst
index 6e3b411e1..846e05694 100644
--- a/proof-libs/fstar/core/Alloc.Vec.fst
+++ b/proof-libs/fstar/core/Alloc.Vec.fst
@@ -1,7 +1,7 @@
 module Alloc.Vec
 open Rust_primitives
 
-unfold type t_Vec t (_: unit) = s:t_Slice t
+unfold type t_Vec t (_: unit) = t_Slice t
 
 let impl__new #t (): t_Vec t () = FStar.Seq.empty
 
@@ -26,6 +26,8 @@ let impl_1__len #t (#[(Tactics.exact (`()))]alloc:unit) (v: t_Vec t alloc) =
   assert (n <= maxint usize_inttype);
   mk_int #usize_inttype (Seq.length v)
 
+let impl_1__as_slice #t (#[(Tactics.exact (`()))]alloc:unit) (v: t_Vec t alloc) : t_Slice t = v
+
 let from_elem #a (item: a) (len: usize) = Seq.create (v len) item
 
 open Rust_primitives.Hax
diff --git a/proof-libs/fstar/core/Core.Array.fst b/proof-libs/fstar/core/Core.Array.fsti
similarity index 64%
rename from proof-libs/fstar/core/Core.Array.fst
rename to proof-libs/fstar/core/Core.Array.fsti
index 44f48c19a..e02274be0 100644
--- a/proof-libs/fstar/core/Core.Array.fst
+++ b/proof-libs/fstar/core/Core.Array.fsti
@@ -8,5 +8,6 @@ let impl_23__map #a n #b (arr: t_Array a n) (f: a -> b): t_Array b n
 
 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()
+val from_fn #a len (f: usize -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
+    
 
diff --git a/proof-libs/fstar/core/Core.Fmt.fsti b/proof-libs/fstar/core/Core.Fmt.fsti
index 50b2d5be2..b865ea0d4 100644
--- a/proof-libs/fstar/core/Core.Fmt.fsti
+++ b/proof-libs/fstar/core/Core.Fmt.fsti
@@ -23,3 +23,4 @@ val impl_2__new_v1 (sz1: usize) (sz2: usize) (pieces: t_Slice string) (args: t_S
 val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Formatter & t_Result
 val impl_2__new_const (args: t_Slice string): t_Arguments
 
+
diff --git a/proof-libs/fstar/core/Core.Marker.fst b/proof-libs/fstar/core/Core.Marker.fst
index f624d969e..8a3ac3d9d 100644
--- a/proof-libs/fstar/core/Core.Marker.fst
+++ b/proof-libs/fstar/core/Core.Marker.fst
@@ -1,6 +1,8 @@
+
 module Core.Marker
 
-type t_PhantomData (t: Type) = t
+type t_PhantomData (t:Type0) = 
+     | PhantomData: t_PhantomData t
 
 class t_Send (h: Type) = {
   dummy_send_field: unit
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
index 7c994c747..1b50fa95a 100644
--- a/proof-libs/fstar/core/Core.Num.fsti
+++ b/proof-libs/fstar/core/Core.Num.fsti
@@ -1,6 +1,8 @@
 module Core.Num
 open Rust_primitives
 
+let impl__u16__MAX: u16 = mk_u16 (maxint u16_inttype)
+
 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
diff --git a/proof-libs/fstar/core/Core.Ops.Arith.fsti b/proof-libs/fstar/core/Core.Ops.Arith.fsti
index a3d75535f..db0911455 100644
--- a/proof-libs/fstar/core/Core.Ops.Arith.fsti
+++ b/proof-libs/fstar/core/Core.Ops.Arith.fsti
@@ -46,3 +46,16 @@ class t_SubAssign self rhs = {
   f_sub_assign: x:self -> y:rhs -> Pure self (f_sub_assign_pre x y) (fun r -> f_sub_assign_post x y r);
 }
 
+class t_MulAssign self rhs = {
+   f_mul_assign_pre: self -> rhs -> bool;
+   f_mul_assign_post: self -> rhs -> self -> bool;
+   f_mul_assign: x:self -> y:rhs -> Pure self (f_mul_assign_pre x y) (fun r -> f_mul_assign_post x y r);
+}
+
+class t_DivAssign self rhs = {
+   f_div_assign_pre: self -> rhs -> bool;
+   f_div_assign_post: self -> rhs -> self -> bool;
+   f_div_assign: x:self -> y:rhs -> Pure self (f_div_assign_pre x y) (fun r -> f_div_assign_post x y r);
+}
+
+
diff --git a/proof-libs/fstar/core/Core.Option.fst b/proof-libs/fstar/core/Core.Option.fst
index 9f514751d..6025de2c6 100644
--- a/proof-libs/fstar/core/Core.Option.fst
+++ b/proof-libs/fstar/core/Core.Option.fst
@@ -18,6 +18,8 @@ let impl__is_some #t_Self (self: t_Option t_Self): bool =  Option_Some? self
 
 let impl__is_none #t_Self (self: t_Option t_Self): bool =  Option_None? self
 
+let impl__take #t (x: t_Option t) : (t_Option t & t_Option t) = (x, Option_None)
+	
 let impl__as_ref #t_Self (self: t_Option t_Self): t_Option t_Self = self
 
 let impl__unwrap_or_default 
diff --git a/proof-libs/fstar/core/Core.Result.fst b/proof-libs/fstar/core/Core.Result.fst
index ab3cd15d9..00c033a7f 100644
--- a/proof-libs/fstar/core/Core.Result.fst
+++ b/proof-libs/fstar/core/Core.Result.fst
@@ -12,6 +12,8 @@ let impl__map_err #e1 #e2 (x: t_Result 't e1) (f: e1 -> e2): t_Result 't e2
 let impl__is_ok #t #e (self: t_Result t e): bool
   = Result_Ok? self
 
+let impl__expect #t #e (x: t_Result t e {Result_Ok? x}) (y: string): t = Result_Ok?.v x
+
 let impl__map #t #e #u (self: t_Result t e) (f: t -> u): t_Result u e =
   match self with 
   | Result_Ok v -> Result_Ok (f v)
@@ -21,3 +23,4 @@ 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
+
diff --git a/proof-libs/fstar/core/Rand_core.Os.fsti b/proof-libs/fstar/core/Rand_core.Os.fsti
new file mode 100644
index 000000000..42fa75dc1
--- /dev/null
+++ b/proof-libs/fstar/core/Rand_core.Os.fsti
@@ -0,0 +1,9 @@
+module Rand_core.Os
+
+type t_OsRng
+
+[@FStar.Tactics.Typeclasses.tcinstance]
+val impl_rng_core: Rand_core.t_RngCore t_OsRng
+
+[@FStar.Tactics.Typeclasses.tcinstance]
+val impl_crypto_rng_core: Rand_core.t_CryptoRngCore t_OsRng
diff --git a/proof-libs/fstar/core/Rand_core.fsti b/proof-libs/fstar/core/Rand_core.fsti
index 60f53bb75..2dfc1cc25 100644
--- a/proof-libs/fstar/core/Rand_core.fsti
+++ b/proof-libs/fstar/core/Rand_core.fsti
@@ -10,3 +10,9 @@ class t_RngCore (t_Self: Type0) = {
 class t_CryptoRng (t_Self: Type0) = {
   marker_trait: unit
 }
+
+class t_CryptoRngCore (t_Self: Type0) = {
+  f_rngcore: t_Self -> t_Self
+}
+
+
diff --git a/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti b/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti
index 82dd99551..8d88407cb 100644
--- a/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti
+++ b/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti
@@ -1,8 +1,5 @@
 module Std.Collections.Hash.Map
 
-open Core
-open FStar.Mul
+type t_HashMap (k v s:Type0)
 
-type t_HashMap (v_K: Type0) (v_V: Type0) (v_S: Type0) = {
-  f__hax_placeholder:unit
-}
+val impl__new #k #v: unit -> t_HashMap k v Std.Hash.Random.t_RandomState
diff --git a/proof-libs/fstar/core/Std.Hash.Random.fsti b/proof-libs/fstar/core/Std.Hash.Random.fsti
index f2148d3fd..d6de0c9eb 100644
--- a/proof-libs/fstar/core/Std.Hash.Random.fsti
+++ b/proof-libs/fstar/core/Std.Hash.Random.fsti
@@ -1,5 +1,3 @@
 module Std.Hash.Random
 
-type t_RandomState = {
-    dummy_random_state_field: unit
-}
+type t_RandomState
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fst
deleted file mode 100644
index df8e01342..000000000
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Arrays.fst
+++ /dev/null
@@ -1,21 +0,0 @@
-module Rust_primitives.Arrays
-
-open Rust_primitives.Integers
-
-let of_list (#t:Type) (l: list t {FStar.List.Tot.length l < maxint Lib.IntTypes.U16}): t_Slice t = Seq.seq_of_list l
-let to_list (#t:Type) (s: t_Slice t): list t = Seq.seq_to_list s
-
-let to_of_list_lemma t l = Seq.lemma_list_seq_bij l
-let of_to_list_lemma t l = Seq.lemma_seq_list_bij l
-
-let map_array #a #b #n (arr: t_Array a n) (f: a -> b): t_Array b n 
-  = FStar.Seq.map_seq_len f arr;
-    FStar.Seq.map_seq f arr 
-
-let createi #t l f = admit() // see issue #423
-
-let lemma_index_concat x y i = admit() // see issue #423
-
-let lemma_index_slice x y i = admit() // see issue #423
-
-let eq_intro a b = admit() // see issue #423
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fst
deleted file mode 100644
index 5bb914e52..000000000
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fst
+++ /dev/null
@@ -1,66 +0,0 @@
-module Rust_primitives.BitVectors
-
-open FStar.Mul
-open Rust_primitives.Arrays
-open Rust_primitives.Integers
-
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 40"
-
-let lemma_get_bit_bounded #t x d i = admit() // see issue #423
-
-let lemma_get_bit_bounded' #t x d = admit() // see issue #423
-
-let pow2_minus_one_mod_lemma1 (n: nat) (m: nat {m < n})
-   : Lemma (((pow2 n - 1) / pow2 m) % 2 == 1)
-   = let d: pos = n - m in
-     Math.Lemmas.pow2_plus m d;
-     Math.Lemmas.lemma_div_plus (-1) (pow2 d) (pow2 m);
-     if d > 0 then Math.Lemmas.pow2_double_mult (d-1)
-
-let pow2_minus_one_mod_lemma2 (n: nat) (m: nat {n <= m})
-  : Lemma (((pow2 n - 1) / pow2 m) % 2 == 0)
-  = Math.Lemmas.pow2_le_compat m n;
-    Math.Lemmas.small_div (pow2 n - 1) (pow2 m)
-
-let bit_vec_to_int_t #t (d: num_bits t) (bv: bit_vec d) = admit ()
-
-let bit_vec_to_int_t_lemma #t (d: num_bits t) (bv: bit_vec d) i = admit ()
-
-let bit_vec_to_int_t_array d bv = admit () // see issue #423
-let bit_vec_to_nat_array d bv = admit () // see issue #423
-
-let get_bit_pow2_minus_one #t n nth
-  = reveal_opaque (`%get_bit) (get_bit (mk_int #t (pow2 n - 1)) nth);
-    if v nth < n then pow2_minus_one_mod_lemma1 n (v nth)
-                 else pow2_minus_one_mod_lemma2 n (v nth)
-
-let mask_inv_opt_in_range #t (mask: int_t t {Some? (mask_inv_opt (v mask))})
-  : Lemma (range (Some?.v (mask_inv_opt (v mask))) t)
-          [SMTPat (mask_inv_opt (v mask))]
-  = let n = (Some?.v (mask_inv_opt (v mask))) in
-    assert (pow2 n - 1 == v mask)
-
-let get_bit_pow2_minus_one_i32 x nth
-  = let n = Some?.v (mask_inv_opt x) in
-    mk_int_equiv_lemma #i32_inttype x;
-    get_bit_pow2_minus_one #i32_inttype n nth
-
-let get_bit_pow2_minus_one_i16 x nth
-  = let n = Some?.v (mask_inv_opt x) in
-    mk_int_equiv_lemma #i16_inttype x;
-    get_bit_pow2_minus_one #i16_inttype n nth
-
-let get_bit_pow2_minus_one_u32 x nth
-  = let n = Some?.v (mask_inv_opt x) in
-    mk_int_equiv_lemma #u32_inttype x;
-    get_bit_pow2_minus_one #u32_inttype n nth
-
-let get_bit_pow2_minus_one_u16 x nth
-  = let n = Some?.v (mask_inv_opt x) in
-    mk_int_equiv_lemma #u16_inttype x;
-    get_bit_pow2_minus_one #u16_inttype n nth
-
-let get_bit_pow2_minus_one_u8 t x nth
-  = let n = Some?.v (mask_inv_opt x) in
-    mk_int_equiv_lemma #u8_inttype x;
-    get_bit_pow2_minus_one #u8_inttype n nth
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fst
deleted file mode 100644
index 8093a8a52..000000000
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fst
+++ /dev/null
@@ -1,27 +0,0 @@
-module Rust_primitives.Hax.Monomorphized_update_at
-
-open Rust_primitives
-open Rust_primitives.Hax
-open Core.Ops.Range
-
-let update_at_range #n s i x = 
-  let res = update_at s i x in
-  admit(); // To be proved // see issue #423
-  res
-  
-let update_at_range_to #n s i x =
-  let res = update_at s i x in
-  admit(); // see issue #423
-  res
-  
-let update_at_range_from #n s i x = 
-  let res = update_at s i x in
-  admit(); // see issue #423
-  res
-
-let update_at_range_full s i x =
-  let res = update_at s i x in
-  admit(); // see issue #423
-  res
-
-
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti
index dd335cf4e..db97e41cf 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti
@@ -14,9 +14,6 @@ let update_at_usize
   (x: t)
   : t_Array t (length s)
   = Seq.upd #t s (v i) x
-  // : Pure (t_Array t (length s))
-  //   (requires (v i < Seq.length s))
-  //   (ensures (fun res -> res == Seq.upd s (v i) x))
 
 val update_at_range #n
   (#t: Type0)
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fst
deleted file mode 100644
index 2fce084a2..000000000
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fst
+++ /dev/null
@@ -1,73 +0,0 @@
-module Rust_primitives.Integers
-
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
-
-
-let pow2_values x = 
-   let p = pow2 x in
-   assert_norm (p == normalize_term (pow2 x))
-
-let usize_inttype = LI.U32
-let isize_inttype = LI.S32
-
-let v_injective #t a = LI.v_injective #t #LI.PUB a
-let v_mk_int #t n = LI.v_mk_int #t #LI.PUB n
-
-let usize_to_uint32 x = x
-let usize_to_uint64 x = Int.Cast.uint32_to_uint64 x
-let size_to_uint64 x = Int.Cast.uint32_to_uint64 x
-
-let mk_int #t a = LI.mk_int #t #LI.PUB a
-let mk_int_equiv_lemma #_ = admit () // see issue #423
-let mk_int_v_lemma #t a = ()
-let v_mk_int_lemma #t a = ()
-let add_mod_equiv_lemma #t a b = LI.add_mod_lemma #t #LI.PUB a b
-let add_equiv_lemma #t a b = LI.add_lemma #t #LI.PUB a b
-let incr_equiv_lemma #t a = LI.incr_lemma #t #LI.PUB a
-
-let mul_mod_equiv_lemma #t a b = LI.mul_mod_lemma #t #LI.PUB a b
-let mul_equiv_lemma #t a b = LI.mul_lemma #t #LI.PUB a b
-let sub_mod_equiv_lemma #t a b = LI.sub_mod_lemma #t #LI.PUB a b
-let sub_equiv_lemma #t a b = LI.sub_lemma #t #LI.PUB a b
-let decr_equiv_lemma #t a = LI.decr_lemma #t #LI.PUB a
-
-let div_equiv_lemma #t a b = admit(); LI.div_lemma #t a b // see issue #423
-let mod_equiv_lemma #t a b = admit(); LI.mod_lemma #t a b // see issue #423
-
-let lognot #t a = LI.lognot #t #LI.PUB a
-let lognot_lemma #t a = admit() // see issue #423
-
-let logxor #t a b = LI.logxor #t #LI.PUB a b
-let logxor_lemma #t a b = admit() // see issue #423
-
-let logand #t a b = LI.logand #t #LI.PUB a b
-let logand_lemma #t a b = admit() // see issue #423
-let logand_mask_lemma #t a b = admit() // see issue #423
-
-let logor #t a b = LI.logor #t #LI.PUB a b
-let logor_lemma #t a b = admit() // see issue #423
-
-let shift_right_equiv_lemma #t a b = admit() // see issue #423
-let shift_left_equiv_lemma #t a b = admit() // see issue #423
-
-let rotate_right #t a b = LI.rotate_right #t #LI.PUB a (cast b)
-let rotate_right_equiv_lemma #t a b = ()
-let rotate_left #t a b = LI.rotate_left #t #LI.PUB a (cast b)
-let rotate_left_equiv_lemma #t a b = ()
-
-let abs_int_equiv_lemma #t a = admit() // see issue #423
-
-let neg_equiv_lemma #_ _ = admit ()
-
-let get_bit_and _x _y _i = admit () // see issue #423
-let get_bit_or _x _y _i = admit () // see issue #423
-let get_bit_shl _x _y _i = admit () // see issue #423
-let get_bit_shr _x _y _i = admit () // see issue #423
-
-let get_bit_cast #t #u x nth
-  = reveal_opaque (`%get_bit) (get_bit x nth);
-    reveal_opaque (`%get_bit) (get_bit (cast_mod #t #u x <: int_t u) nth);
-    admit () // see issue #423
-
-let get_bit_cast_extend #t #u x nth
-  = admit () // see issue #423
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti
index 9f1c5b531..84171151e 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti
@@ -238,14 +238,9 @@ val decr_equiv_lemma: #t:inttype
   -> a:int_t t{minint t < v a}
   -> Lemma (decr a == LI.decr #t #LI.PUB a)
 
-let div (#t:inttype) (a:int_t t) (b:int_t t{v b <> 0}) =
-  assume(unsigned t \/ range (v a / v b) t); // see issue #423
+let div (#t:inttype) (a:int_t t) (b:int_t t{v b <> 0 /\ (unsigned t \/ range (v a / v b) t)}) =
+  assert (unsigned t \/ range (v a / v b) t);
   mk_int #t (v a / v b)
-  
-val div_equiv_lemma: #t:inttype{~(LI.U128? t) /\ ~(LI.S128? t)}
-  -> a:int_t t
-  -> b:int_t t{v b <> 0 /\ (unsigned t \/ range FStar.Int.(v a / v b) t)}
-  -> Lemma (div a b == LI.div a b)
 
 let mod (#t:inttype) (a:int_t t) (b:int_t t{v b <> 0}) =
   mk_int #t (v a % v b)