diff --git a/examples/barrett/proofs/fstar/extraction/Makefile b/examples/barrett/proofs/fstar/extraction/Makefile
index d8f4c3ac1..dd213720a 100644
--- a/examples/barrett/proofs/fstar/extraction/Makefile
+++ b/examples/barrett/proofs/fstar/extraction/Makefile
@@ -114,6 +114,7 @@ FSTAR_FLAGS = --cmi \
   --warn_error -331 \
   --cache_checked_modules --cache_dir $(CACHE_DIR) \
   --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
+   --ext context_pruning \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
 FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS)
diff --git a/examples/barrett/src/lib.rs b/examples/barrett/src/lib.rs
index b5bc7d40e..9109b6877 100644
--- a/examples/barrett/src/lib.rs
+++ b/examples/barrett/src/lib.rs
@@ -23,6 +23,7 @@ pub(crate) const FIELD_MODULUS: i32 = 3329;
 /// `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)
 ///
 /// In particular, if `|value| < BARRETT_R`, then `|result| < FIELD_MODULUS`.
+#[hax::fstar::options("--z3rlimit 200 --ext context_prune")]
 #[hax::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
 #[hax::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS &&
                    result % FIELD_MODULUS == value % FIELD_MODULUS)]
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.fsti b/proof-libs/fstar/core/Alloc.Slice.fsti
index 82a01332d..11429a7b8 100644
--- a/proof-libs/fstar/core/Alloc.Slice.fsti
+++ b/proof-libs/fstar/core/Alloc.Slice.fsti
@@ -5,3 +5,5 @@ 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
+
+let impl__into_vec #a #t (s: t_Slice a): t_Vec a t= s
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..935931900
--- /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
diff --git a/proof-libs/fstar/core/Core.Result.fst b/proof-libs/fstar/core/Core.Result.fst
index 00c033a7f..915c57136 100644
--- a/proof-libs/fstar/core/Core.Result.fst
+++ b/proof-libs/fstar/core/Core.Result.fst
@@ -24,3 +24,7 @@ let impl__and_then #t #e #u (self: t_Result t e) (op: t -> t_Result u e): t_Resu
   | 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/core/Std.Collections.Hash.Map.fsti b/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti
index 8d88407cb..519dda884 100644
--- a/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti
+++ b/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti
@@ -1,5 +1,5 @@
 module Std.Collections.Hash.Map
 
-type t_HashMap (k v s:Type0)
+type t_HashMap ([@@@ strictly_positive] k [@@@ strictly_positive] v [@@@ strictly_positive] s:Type0): eqtype
 
 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 d6de0c9eb..692792148 100644
--- a/proof-libs/fstar/core/Std.Hash.Random.fsti
+++ b/proof-libs/fstar/core/Std.Hash.Random.fsti
@@ -1,3 +1,3 @@
 module Std.Hash.Random
 
-type t_RandomState
+type t_RandomState: eqtype
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