Merge pull request #574 from hacspec/bertie-core-additions

feat(proof-libs/fstar): add missing implementations for Bertie

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

@@ -0,0 +1,12 @@
+module Alloc.Fmt
+open Rust_primitives
+
+include Core.Fmt
+
+val impl_2__new_v1 (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments
+val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Result
+
+val format (args: t_Arguments): string
+
+
+

proof-libs/fstar/core/Alloc.String.fst

@@ -0,0 +1,5 @@
+module Alloc.String
+
+type t_String = string
+
+

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

@@ -71,3 +71,5 @@ class t_AsRef self t = {
   f_as_ref_post: self -> t -> bool;
   f_as_ref: self -> t;
 }
+
+type t_Infallible = _:unit{False}

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

@@ -0,0 +1,5 @@
+module Core.Fmt.Rt
+
+val t_Argument: Type0
+val impl_1__new_display (#t:Type0) (x: t): t_Argument
+val impl_1__new_debug (#t:Type0) (x: t): t_Argument

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

@@ -1,3 +1,19 @@
 module Core.Fmt
+open Rust_primitives
+
+val t_Error: Type0
+
+type t_Result = Core.Result.t_Result unit t_Error
+
+val t_Formatter: Type0
+class t_Display t_Self = {
+  f_fmt_pre: t_Self -> Core.Fmt.t_Formatter -> bool;
+  f_fmt_post: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) -> bool;
+  f_fmt: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error)
+}
 
 val t_Arguments: Type0
+val impl_2__new_v1 (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
+

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

@@ -4,6 +4,7 @@ open Rust_primitives
 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)
 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.Panicking.fst

@@ -10,3 +10,6 @@ let panic (message: string {False}): t_Never
 
 let assert_failed (k: t_AssertKind) x y (z: Core.Option.t_Option unit {False}): t_Never
   = match () with
+
+let panic_fmt (fmt: Core.Fmt.t_Arguments {False}): t_Never
+  = match () with

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

@@ -33,3 +33,6 @@ val impl__split_at #t (s: t_Slice t) (mid: usize): Pure (t_Slice t * t_Slice t)
     (ensures (fun (x,y) -> Seq.length x == v mid /\ Seq.length y == Seq.length s - v mid /\
                         x == Seq.slice s 0 (v mid) /\ y == Seq.slice s (v mid) (Seq.length s) /\
                         s == Seq.append x y))
+
+let impl__is_empty (s: t_Slice 'a): bool = Seq.length s = 0
+

proof-libs/fstar/core/Core.fst

@@ -4,5 +4,3 @@ include Rust_primitives
 include Core.Num
 include Core.Iter
 include Core.Ops
-
-

proof-libs/fstar/core/Rand_core.fsti

@@ -0,0 +1,12 @@
+module Rand_core
+open Rust_primitives
+
+class t_RngCore (t_Self: Type0) = {
+  f_next_u32: t_Self -> t_Self & u32;
+  f_next_u64: t_Self -> t_Self & u64;
+  f_fill_bytes: t_Self -> t_Slice u8 -> t_Self & t_Slice u8
+}
+
+class t_CryptoRng (t_Self: Type0) = {
+  marker_trait: unit
+}

proof-libs/fstar/core/Std.Io.Stdio.fsti

@@ -0,0 +1,4 @@
+module Std.Io.Stdio
+
+val v__eprint: Core.Fmt.t_Arguments -> unit
+

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

@@ -0,0 +1,7 @@
+module Rust_primitives.Hax.Control_flow_monad.Mexception
+open Core.Ops.Control_flow
+
+let run #a: t_ControlFlow a a -> a
+    = function | ControlFlow_Continue v | ControlFlow_Break v -> v
+
+

proof-libs/fstar/rust_primitives/Rust_primitives.fst

@@ -17,6 +17,15 @@ let (let|) (#e #a #b: Type) (x: Core.Result.t_Result a e) (f: a -> Core.Result.t
     | Core.Result.Result_Ok x -> f x
     | Core.Result.Result_Err e -> Core.Result.Result_Err e
 
+let (let!)
+    #break #continue #continue'
+    (v: Core.Ops.Control_flow.t_ControlFlow break continue)
+    (f: continue -> Core.Ops.Control_flow.t_ControlFlow break continue')
+    : Core.Ops.Control_flow.t_ControlFlow break continue'
+    = match v with
+    | Core.Ops.Control_flow.ControlFlow_Continue v -> f v
+    | Core.Ops.Control_flow.ControlFlow_Break b -> Core.Ops.Control_flow.ControlFlow_Break b
+
 class cast_tc a b = {
   cast: a -> b; 
 }