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