feat(lib) New sandwich core changes

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)

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)]

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

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

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

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

proof-libs/fstar/core/Std.Hash.Random.fsti

@@ -1,3 +1,3 @@
 module Std.Hash.Random
 
-type t_RandomState
+type t_RandomState: eqtype

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