From 98a8863598105ce6872166da1ae9ad7751d68750 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Tue, 4 Feb 2025 17:54:52 +0100
Subject: [PATCH] Small additions and corrections in F* core lib.

---
 .../fstar/core/Alloc.Collections.Btree.Set.fsti    | 14 ++++++++++++++
 proof-libs/fstar/core/Core.Cmp.fsti                |  6 +++---
 proof-libs/fstar/core/Core.Convert.fst             | 10 +++++++++-
 3 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti b/proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti
index f18aaba17..f6b41aa58 100644
--- a/proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti
+++ b/proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti
@@ -10,3 +10,17 @@ val impl_13__new #t (): t_BTreeSet t ()
 val impl_14__len #t #u (x:t_BTreeSet t u) : usize
 
 val impl_14__insert #t #u (x:t_BTreeSet t u) (y:t) : (t_BTreeSet t u & bool)
+
+val btree_iter_iter (t: Type0): Core.Iter.Traits.Iterator.iterator (t_Iter t)
+
+val impl_14__iter #t #u (x:t_BTreeSet t u): t_Iter t
+
+unfold instance impl t : Core.Iter.Traits.Iterator.iterator (t_Iter t) = {
+  f_Item = t;
+  f_next = (btree_iter_iter t).f_next;
+  f_contains = (btree_iter_iter t).f_contains;
+  f_fold = (btree_iter_iter t).f_fold;
+  f_enumerate = (btree_iter_iter t).f_enumerate;
+  f_step_by = (btree_iter_iter t).f_step_by;
+  f_all = (btree_iter_iter t).f_all;
+}
diff --git a/proof-libs/fstar/core/Core.Cmp.fsti b/proof-libs/fstar/core/Core.Cmp.fsti
index fe1a75e5f..6dd260ebe 100644
--- a/proof-libs/fstar/core/Core.Cmp.fsti
+++ b/proof-libs/fstar/core/Core.Cmp.fsti
@@ -28,15 +28,15 @@ type t_Ordering =
 
 
 class t_PartialOrd (v_Self: Type) (v_Rhs:Type) = {
-  _super_9014672428308350468: t_PartialEq v_Self v_Rhs;
+  _super_8303539986193044559: t_PartialEq v_Self v_Rhs;
   f_partial_cmp_pre: v_Self -> v_Rhs -> Type0;
   f_partial_cmp_post: v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering -> Type0;
   f_partial_cmp:v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering;
 }
 
 class t_Ord (v_Self: Type) = {
-  _super_8099741844003281729: t_Eq v_Self;
-  _super_12866954522599331834: t_PartialOrd v_Self v_Self;
+  _super_8438227699474489191: t_Eq v_Self;
+  _super_17497397511932837737: t_PartialOrd v_Self v_Self;
   f_cmp_pre: v_Self -> v_Self -> Type0;
   f_cmp_post: v_Self -> v_Self -> t_Ordering -> Type0;
   f_cmp:v_Self -> v_Self -> t_Ordering;
diff --git a/proof-libs/fstar/core/Core.Convert.fst b/proof-libs/fstar/core/Core.Convert.fst
index 0cf837881..0280dfc31 100644
--- a/proof-libs/fstar/core/Core.Convert.fst
+++ b/proof-libs/fstar/core/Core.Convert.fst
@@ -17,7 +17,6 @@ instance impl_6 (t: Type0) (len: usize): try_into_tc (t_Slice t) (t_Array t len)
   )
 }
 
-
 instance impl_6_refined (t: Type0) (len: usize): try_into_tc (s: t_Slice t {Core.Slice.impl__len s == len}) (t_Array t len) = {
   f_Error = Core.Array.t_TryFromSliceError;
   f_try_into = (fun (s: t_Slice t {Core.Slice.impl__len s == len}) -> 
@@ -25,6 +24,15 @@ instance impl_6_refined (t: Type0) (len: usize): try_into_tc (s: t_Slice t {Core
   )
 }
 
+instance integer_try_into (t:inttype) (t':inttype) : try_into_tc (int_t t) (int_t t') = {
+  f_Error = Core.Num.Error.t_TryFromIntError;
+  f_try_into = (fun (x: int_t t) ->
+    if range (v #t x) t'
+    then Core.Result.Result_Ok (Rust_primitives.Integers.cast #t #t' x)
+    else Core.Result.Result_Err ()
+  )
+}
+
 class t_Into self t = {
   f_into_pre: self -> bool;
   f_into_post: self -> t -> bool;