Library extensions

engine/backends/fstar/fstar_backend.ml

@@ -276,23 +276,23 @@ struct
     [
       (c Rust_primitives__hax__array_of_list, (3, ".[]<-"));
       (c Core__ops__index__Index__index, (2, ".[]"));
-      (c Core__ops__bit__BitXor__bitxor, (2, "^."));
-      (c Core__ops__bit__BitAnd__bitand, (2, "&."));
-      (c Core__ops__bit__BitOr__bitor, (2, "|."));
-      (c Core__ops__bit__Not__not, (1, "~."));
-      (c Core__ops__arith__Add__add, (2, "+!"));
-      (c Core__ops__arith__Sub__sub, (2, "-!"));
-      (c Core__ops__arith__Mul__mul, (2, "*!"));
-      (c Core__ops__arith__Div__div, (2, "/!"));
-      (c Core__ops__arith__Rem__rem, (2, "%!"));
-      (c Core__ops__bit__Shl__shl, (2, "<<!"));
-      (c Core__ops__bit__Shr__shr, (2, ">>!"));
-      (c Core__cmp__PartialEq__eq, (2, "=."));
-      (c Core__cmp__PartialOrd__lt, (2, "<."));
-      (c Core__cmp__PartialOrd__le, (2, "<=."));
-      (c Core__cmp__PartialEq__ne, (2, "<>."));
-      (c Core__cmp__PartialOrd__ge, (2, ">=."));
-      (c Core__cmp__PartialOrd__gt, (2, ">."));
+      (c Rust_primitives__hax__machine_int__not, (1, "~."));
+      (c Rust_primitives__hax__machine_int__add, (2, "+!"));
+      (c Rust_primitives__hax__machine_int__sub, (2, "-!"));
+      (c Rust_primitives__hax__machine_int__div, (2, "/!"));
+      (c Rust_primitives__hax__machine_int__mul, (2, "*!"));
+      (c Rust_primitives__hax__machine_int__rem, (2, "%!"));
+      (c Rust_primitives__hax__machine_int__shl, (2, "<<!"));
+      (c Rust_primitives__hax__machine_int__shr, (2, ">>!"));
+      (c Rust_primitives__hax__machine_int__bitxor, (2, "^."));
+      (c Rust_primitives__hax__machine_int__bitor, (2, "|."));
+      (c Rust_primitives__hax__machine_int__bitand, (2, "&."));
+      (c Rust_primitives__hax__machine_int__eq, (2, "=."));
+      (c Rust_primitives__hax__machine_int__ne, (2, "<>."));
+      (c Rust_primitives__hax__machine_int__le, (2, "<=."));
+      (c Rust_primitives__hax__machine_int__lt, (2, "<."));
+      (c Rust_primitives__hax__machine_int__gt, (2, ">."));
+      (c Rust_primitives__hax__machine_int__ge, (2, ">=."));
       (`Primitive (LogicalOp And), (2, "&&"));
       (`Primitive (LogicalOp Or), (2, "||"));
       (c Rust_primitives__hax__int__add, (2, "+"));

engine/lib/phases/phase_specialize.ml

@@ -59,6 +59,9 @@ module Make (F : Features.T) =
           let is_int : (ty, unit) predicate =
             tapp0 >>& eq_global_ident Hax_lib__int__Int >>& erase
 
+          let is_machine_int : (ty, unit) predicate =
+           fun t -> match t with TInt _ -> Some () | _ -> None
+
           let any _ = Some ()
           let int_any = mk [ etyp >> is_int ] any
           let int_int_any = mk [ etyp >> is_int; etyp >> is_int ] any
@@ -69,11 +72,50 @@ module Make (F : Features.T) =
             mk [ etyp >> (tref >>& is_int); etyp >> (tref >>& is_int) ] any
 
           let any_rint = mk [ any ] (tref >>& is_int)
+
+          let mint_mint_any =
+            mk [ etyp >> is_machine_int; etyp >> is_machine_int ] any
+
+          let mint_any = mk [ etyp >> is_machine_int ] any
         end
 
         (** The list of replacements *)
         let patterns =
           [
+            mint_mint_any Core__ops__arith__Add__add
+              Rust_primitives__hax__machine_int__add;
+            mint_mint_any Core__ops__arith__Sub__sub
+              Rust_primitives__hax__machine_int__sub;
+            mint_mint_any Core__ops__arith__Mul__mul
+              Rust_primitives__hax__machine_int__mul;
+            mint_mint_any Core__ops__arith__Div__div
+              Rust_primitives__hax__machine_int__div;
+            mint_mint_any Core__ops__arith__Rem__rem
+              Rust_primitives__hax__machine_int__rem;
+            mint_mint_any Core__ops__bit__Shl__shl
+              Rust_primitives__hax__machine_int__shl;
+            mint_mint_any Core__ops__bit__Shr__shr
+              Rust_primitives__hax__machine_int__shr;
+            mint_mint_any Core__ops__bit__BitXor__bitxor
+              Rust_primitives__hax__machine_int__bitxor;
+            mint_mint_any Core__ops__bit__BitAnd__bitand
+              Rust_primitives__hax__machine_int__bitand;
+            mint_mint_any Core__ops__bit__BitOr__bitor
+              Rust_primitives__hax__machine_int__bitor;
+            mint_any Core__ops__bit__Not__not
+              Rust_primitives__hax__machine_int__not;
+            mint_mint_any Core__cmp__PartialOrd__gt
+              Rust_primitives__hax__machine_int__gt;
+            mint_mint_any Core__cmp__PartialOrd__ge
+              Rust_primitives__hax__machine_int__ge;
+            mint_mint_any Core__cmp__PartialOrd__lt
+              Rust_primitives__hax__machine_int__lt;
+            mint_mint_any Core__cmp__PartialOrd__le
+              Rust_primitives__hax__machine_int__le;
+            mint_mint_any Core__cmp__PartialEq__ne
+              Rust_primitives__hax__machine_int__ne;
+            mint_mint_any Core__cmp__PartialEq__eq
+              Rust_primitives__hax__machine_int__eq;
             int_int_any Core__ops__arith__Add__add
               Rust_primitives__hax__int__add;
             int_int_any Core__ops__arith__Sub__sub

engine/names/src/lib.rs

@@ -219,6 +219,28 @@ mod hax {
         fn into_machine() {}
     }
 
+    mod machine_int {
+        fn add() {}
+        fn sub() {}
+        fn div() {}
+        fn mul() {}
+        fn rem() {}
+
+        fn not() {}
+        fn bitxor() {}
+        fn bitor() {}
+        fn bitand() {}
+        fn shl() {}
+        fn shr() {}
+
+        fn eq() {}
+        fn ne() {}
+        fn le() {}
+        fn lt() {}
+        fn ge() {}
+        fn gt() {}
+    }
+
     mod control_flow_monad {
         trait ControlFlowMonad {
             fn lift() {}

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

@@ -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 #t #r (x:t_Slice t): t_Vec t r = x

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

@@ -4,6 +4,10 @@ module Core.Marker
 type t_PhantomData (t:Type0) = 
      | PhantomData: t_PhantomData t
 
+class t_StructuralPartialEq (h: Type) = {
+  dummy_structural_partial_eq_field: unit
+}
+
 class t_Send (h: Type) = {
   dummy_send_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

@@ -10,6 +10,8 @@ val impl__u16__to_be_bytes: u16 -> t_Array u8 (sz 2)
 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
 
+val impl__u16__from_be_bytes: t_Array u8 (sz 2) -> u16
+
 let impl__i16__wrapping_add: i16 -> i16 -> i16 = add_mod
 let impl__i16__wrapping_sub: i16 -> i16 -> i16 = sub_mod
 let impl__i16__wrapping_mul: i16 -> i16 -> i16 = mul_mod

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

@@ -36,3 +36,5 @@ val impl__split_at #t (s: t_Slice t) (mid: usize): Pure (t_Slice t * t_Slice t)
 
 let impl__is_empty (s: t_Slice 'a): bool = Seq.length s = 0
 
+let impl__clone_from_slice #t (x:t_Slice t) (y:t_Slice t) : t_Slice t = y
+

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
+
+
+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;
+}
+