Merge pull request #1273 from cryspen/various-core-additions

Various F* core lib additions.

Author: maximebuyse

proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti

@@ -1,3 +1,12 @@
 module Alloc.Collections.Btree.Set
+open Rust_primitives
 
 val t_BTreeSet (t:Type0) (u:unit): eqtype
+
+val t_Iter (t:Type0): eqtype
+
+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)

proof-libs/fstar/core/Alloc.Slice.fsti

@@ -4,4 +4,6 @@ open Alloc.Vec
 
 let impl__to_vec #a (s: t_Slice a): t_Vec a Alloc.Alloc.t_Global = s
 
+let impl__into_vec #t #a (s: Alloc.Boxed.t_Box (t_Slice t) a): t_Vec t a = s
+
 val impl__concat #t1 #t2 (s: t_Slice t1): t_Slice t2

proof-libs/fstar/core/Core.Cmp.fsti

@@ -9,37 +9,46 @@ instance min_inttype (#t:inttype): min_tc (int_t t) = {
   min = fun a b -> if a <. b then a else b
 }
 
+class t_PartialEq (v_Self: Type) (v_Rhs: Type) = {
+  // __constraint_1069563329_t_PartialEq:t_PartialEq v_Self v_Rhs;
+  f_eq_pre: v_Self -> v_Rhs -> Type0;
+  f_eq_post: v_Self -> v_Rhs -> bool -> Type0;
+  f_eq:v_Self -> v_Rhs -> bool;
+}
+
+class t_Eq (v_Self: Type) = {
+  [@@@FStar.Tactics.Typeclasses.tcresolve]
+  __constraint_t_Eq_t_PartialEq:t_PartialEq v_Self v_Self;
+}
+
 type t_Ordering =
   | Ordering_Less : t_Ordering
   | Ordering_Equal : t_Ordering
   | Ordering_Greater : t_Ordering
 
+
+class t_PartialOrd (v_Self: Type) (v_Rhs:Type) = {
+  _super_9014672428308350468: 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;
+  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;
   // f_max:v_Self -> v_Self -> v_Self;
   // f_min:v_Self -> v_Self -> v_Self;
   // f_clamp:v_Self -> v_Self -> v_Self -> v_Self
 }
 
-class t_PartialEq (v_Self: Type) (v_Rhs: Type) = {
-  // __constraint_1069563329_t_PartialEq:t_PartialEq v_Self v_Rhs;
-  f_eq:v_Self -> v_Rhs -> bool;
-  f_ne:v_Self -> v_Rhs -> bool
-}
-
 instance all_eq (a: eqtype): t_PartialEq a a = {
+  f_eq_pre = (fun x y -> True);
+  f_eq_post = (fun x y r -> True);
   f_eq = (fun x y -> x = y);
-  f_ne = (fun x y -> x <> y);
-}
-
-class t_PartialOrd (v_Self: Type) (v_Rhs: Type) = {
-  __constraint_Rhs_t_PartialEq:t_PartialEq v_Self v_Rhs;
-  // __constraint_Rhs_t_PartialOrd:t_PartialOrd v_Self v_Rhs;
-  f_partial_cmp:v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering;
-  // f_lt:v_Self -> v_Rhs -> bool;
-  // f_le:v_Self -> v_Rhs -> bool;
-  // f_gt:v_Self -> v_Rhs -> bool;
-  // f_ge:v_Self -> v_Rhs -> bool
 }
 
 type t_Reverse t = | Reverse of t

proof-libs/fstar/core/Core.Core_arch.X86.Pclmulqdq.fsti

@@ -0,0 +1,3 @@
+module Core.Core_arch.X86.Pclmulqdq
+
+val v__mm_clmulepi64_si128 : Rust_primitives.Integers.i32 -> Core.Core_arch.X86.t____m128i -> Core.Core_arch.X86.t____m128i -> Core.Core_arch.X86.t____m128i

proof-libs/fstar/core/Core.Core_arch.X86.Sse2.fsti

@@ -0,0 +1,3 @@
+module Core.Core_arch.X86.Sse2
+
+val v__mm_set_epi64x: Rust_primitives.Integers.i64 -> Rust_primitives.Integers.i64 -> Core.Core_arch.X86.t____m128i

proof-libs/fstar/core/Core.Core_arch.X86_64_.Sse2.fsti

@@ -0,0 +1,3 @@
+module Core.Core_arch.X86_64_.Sse2
+
+val v__mm_cvtsi128_si64: Core.Core_arch.X86.t____m128i -> Rust_primitives.Integers.i64

proof-libs/fstar/core/Core.Fmt.fsti

@@ -21,6 +21,6 @@ class t_Debug t_Self = {
 val t_Arguments: Type0
 val impl_2__new_v1 (sz1: usize) (sz2: usize) (pieces: t_Slice string) (args: t_Slice Core.Fmt.Rt.t_Argument): t_Arguments
 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
+val impl_2__new_const (u:usize) (args: t_Slice string): t_Arguments
 
 

proof-libs/fstar/core/Core.Iter.Adapters.Map.fsti

@@ -0,0 +1,3 @@
+module Core.Iter.Adapters.Map
+
+type t_Map (k:Type0) (v:Type0)

proof-libs/fstar/core/Core.Iter.Adapters.Zip.fsti

@@ -0,0 +1,3 @@
+module Core.Iter.Adapters.Zip
+
+type t_Zip (t1:Type0) (t2:Type0)

proof-libs/fstar/core/Core.Marker.fst

@@ -48,3 +48,7 @@ class t_Clone (h: Type) = {
 instance t_Clone_all t: t_Clone t = {
   dummy_clone_field = ()
 }
+
+class t_StructuralPartialEq (h: Type) = {
+  dummy_eq_field: unit
+}

proof-libs/fstar/core/Core.Num.Error.fsti

@@ -2,3 +2,5 @@ module Core.Num.Error
 open Rust_primitives
 
 type t_ParseIntError = unit
+type t_TryFromIntError = unit
+

proof-libs/fstar/core/Core.Num.fsti

@@ -7,6 +7,7 @@ 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
 val impl__u16__to_be_bytes: u16 -> t_Array u8 (sz 2)
+val impl__u16__from_be_bytes: t_Array u8 (sz 2) -> u16
 let impl__i32__wrapping_add: i32 -> i32 -> i32 = add_mod
 let impl__i32__abs (a:i32{minint i32_inttype < v a}) : i32 = abs_int a
 

proof-libs/fstar/core/Core.Slice.fsti

@@ -27,6 +27,7 @@ instance impl__index t n: t_Index (t_Slice t) (int_t n)
     }
 
 let impl__copy_from_slice #t (x: t_Slice t) (y:t_Slice t) : t_Slice t = y
+let impl__clone_from_slice #t (x: t_Slice t) (y:t_Slice t) : t_Slice t = y
 
 val impl__split_at #t (s: t_Slice t) (mid: usize): Pure (t_Slice t * t_Slice t)
     (requires (v mid <= Seq.length s))

proof-libs/fstar/core/Rand.Distributions.Distribution.fsti

@@ -0,0 +1 @@
+module Rand.Distributions.Distribution

proof-libs/fstar/core/Rand.Distributions.Integer.fsti

@@ -0,0 +1 @@
+module Rand.Distributions.Integer

proof-libs/fstar/core/Rand.Rng.fsti

@@ -0,0 +1 @@
+module Rand.Rng

proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst

@@ -55,3 +55,11 @@ 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
+
+class iterator_return (self: Type u#0): Type u#1 = {
+  [@@@FStar.Tactics.Typeclasses.tcresolve]
+  parent_iterator: Core.Iter.Traits.Iterator.iterator self;
+  f_fold_return: #b:Type0 -> s:self -> b -> (b -> i:parent_iterator.f_Item{parent_iterator.f_contains s i} -> Core.Ops.Control_flow.t_ControlFlow b b) -> Core.Ops.Control_flow.t_ControlFlow b b;
+}