From 2dfccd2b9e8cd6903df709ac5373df74bd1e43e8 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Thu, 5 Dec 2024 10:33:09 +0100
Subject: [PATCH] F* core changes for type-checking of sandwixh.

---
 proof-libs/fstar/core/Alloc.Boxed.fst                    | 2 ++
 proof-libs/fstar/core/Alloc.Slice.fsti                   | 2 ++
 proof-libs/fstar/core/Alloc.Vec.fst                      | 4 ++++
 proof-libs/fstar/core/Core.Pin.fsti                      | 7 +++++++
 proof-libs/fstar/core/Core.Ptr.Non_null.fsti             | 3 +++
 proof-libs/fstar/core/Core.Result.fst                    | 4 ++++
 proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst | 2 ++
 7 files changed, 24 insertions(+)
 create mode 100644 proof-libs/fstar/core/Core.Pin.fsti
 create mode 100644 proof-libs/fstar/core/Core.Ptr.Non_null.fsti

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/Alloc.Vec.fst b/proof-libs/fstar/core/Alloc.Vec.fst
index 846e05694..b94c58aa8 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) = 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
@@ -40,3 +41,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 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/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