Merge pull request #1466 from cryspen/proof-lib/fstar-support-more-rbe

Proof lib/fstar support more rbe

Author: maximebuyse

.utils/rust-by-example.js

@@ -46,7 +46,7 @@ function codeBlocksToModules(code_blocks) {
         /unsafe_asm \d+/
     ];
     let modules = {};
-    
+
     for(let {name, blocks} of code_blocks) {
         let mod_section = `section_${name}`;
         modules[mod_section] = {};
@@ -105,21 +105,27 @@ fs.writeFileSync(OUTPUT_CRATE_SRC + '/lib.rs', root_mod);
 // A list of [<module_name>, [<snippet_number>]] that are known not to be processed by hax
 let cargo_hax_denylist = [
     ['error_iter_result', [3]],
+    ['error_multiple_error_types_boxing_errors', [1]], // uses dyn
+    ['error_multiple_error_types_reenter_question_mark', [2]], // uses dyn
+    ['error_multiple_error_types_wrap_error', [1]], // uses dyn
     ['error_option_unwrap_defaults', [3,4]],
     ['flow_control_for', [1,2,3,5]],
     ['flow_control_if_let', [3]],
+    ['flow_control_let_else', [1,2]], // Let else panics, bug #1460
     ['flow_control_loop_nested', [1]],
     ['flow_control_loop_return', [1]],
     ['flow_control_loop', [1]],
     ['flow_control_match_binding', [1,2]],
     ['flow_control_match_destructuring_destructure_pointers', [1]],
     ['flow_control_match_destructuring_destructure_slice', [1]],
+    ['flow_control_match_destructuring_destructure_tuple', [1]], // .. pattern, bug #1462
     ['flow_control_match', [1]],
     ['flow_control_while_let', [1,2]],
     ['fn_closures_capture', [1]],
     ['fn_closures_input_parameters', [1]],
     ['fn', [1]],
     ['hello_print_fmt', [1]],
+    ['generics_bounds_testcase_empty', [1]], // Marker traits, bug #1221
     ['macros_dry', [1]],
     ['scope_borrow_alias', [1]],
     ['scope_borrow_ref', [1]],
@@ -135,6 +141,8 @@ let cargo_hax_denylist = [
     ['std_str', [1]],
     ['trait_iter', [1]],
     ['trait', [1]],
+    ['trait_dyn', [1]], // uses dyn
+    ['trait_supertraits', [1]], // uses dyn
     ['unsafe', [1,2]],
 ].map(([module, snippets]) => snippets.map(n => `section_${module}::snippet_${n}`)).flat();
 

hax-lib/proof-libs/fstar-secret-integers/core/Core.Str.fsti

@@ -4,3 +4,13 @@ open Rust_primitives
 val impl__str__len: string -> usize
 val impl__str__as_bytes: string -> t_Slice u8
 
+/// Parses this string slice into another type
+val impl_str__parse (#t: Type0) (#err: Type0) (s:string) :
+  (Core.Result.t_Result t err)
+
+/// Trims trailing whitespace
+val impl_str__trim : string -> string
+
+/// Split strings on patterns
+val impl_str__split : (#pattern: Type) -> string -> pattern ->
+(Core.Str.Iter.t_Split pattern)

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

@@ -15,3 +15,7 @@ let impl__String__pop (self: t_String): (Alloc.String.t_String & Core.Option.t_O
     if l > 0 then 
         (FStar.String.sub self 0 (l - 1), Core.Option.Option_Some (FStar.String.index self (l - 1)))
     else (self, Core.Option.Option_None)
+
+/// Placeholder for the to_string typeclass
+assume
+val f_to_string (#t: Type) {| Core.TypeClassPlaceHolder.t_Placeholder |} (x:t) : Alloc.String.t_String

hax-lib/proof-libs/fstar/core/Core.F32.fsti

@@ -0,0 +1,5 @@
+module Core.F32
+
+open Rust_primitives.Float
+
+val impl_f32__abs : float -> float

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

@@ -32,6 +32,12 @@ val impl_4__new_v1_formatted :
 
 val impl_11__write_fmt : Core.Fmt.t_Formatter -> Core.Fmt.t_Arguments -> Core.Fmt.t_Formatter & Core.Result_Option_bundle.t_Result unit Core.Fmt.t_Error
 
+[@FStar.Tactics.Typeclasses.tcinstance]
+val impl_t_debug_string : t_Debug Prims.string
+
+[@FStar.Tactics.Typeclasses.tcinstance]
+val impl_t_display_string : t_Display Prims.string
+
 instance debuggable_bool : t_Debug Prims.bool =
 {
   f_dbg_fmt_pre = (fun (b: Prims.bool) (fmt: Core.Fmt.t_Formatter) -> true);
@@ -56,3 +62,7 @@ instance debuggable_pair (#a:Type) (#b:Type) (x: t_Debug a) (y: t_Debug b): t_De
      | Core.Result.Result_Ok v -> f_dbg_fmt pair._2 fmt_a
      | Core.Result.Result_Err e -> (fmt_a, result_a));
 }
+
+/// Default empty implementation, used for lax-checking
+[@FStar.Tactics.Typeclasses.tcinstance]
+val derive_debug (#t: Type) : t_Debug t

hax-lib/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst

@@ -68,3 +68,7 @@ assume val repeat_with_iter (t: Type0) : Core.Iter.Traits.Iterator.t_Iterator
 [@FStar.Tactics.Typeclasses.tcinstance]
 assume val flat_map_iter (t: Type0) (u: Type0) (v: Type0) : Core.Iter.Traits.Iterator.t_Iterator 
   (Core.Iter.Adapters.Flatten.t_FlatMap t u v)
+
+[@FStar.Tactics.Typeclasses.tcinstance]
+assume val t_split_iter (pattern: Type) :
+(Core.Str.Iter.t_Split pattern) -> t_Iterator (Core.Str.Iter.t_Split pattern)

hax-lib/proof-libs/fstar/core/Core.Mem.fsti

@@ -4,3 +4,5 @@ open Rust_primitives
 // FIXME(unsafe!): remove default type (see #545)
 val size_of (#[FStar.Tactics.exact (`eqtype_as_type unit)]t:Type): unit -> usize
 val size_of_val (#t:Type) : t -> usize
+
+val drop (#t: Type) (x:t) : Prims.unit

hax-lib/proof-libs/fstar/core/Core.Ops.Arith.fsti

@@ -59,3 +59,9 @@ class t_DivAssign self rhs = {
 }
 
 let f_neg #t x = zero #t -! x
+
+/// Type class implementations
+[@FStar.Tactics.Typeclasses.tcinstance]
+val impl_float_f_mul : t_Mul float float
+[@FStar.Tactics.Typeclasses.tcinstance]
+val impl_float_f_add : t_Add float float

hax-lib/proof-libs/fstar/core/Core.Ops.Drop.fsti

@@ -0,0 +1,7 @@
+module Core.Ops.Drop
+
+class t_Drop (v_Self: Type) = {
+  f_drop_pre : v_Self -> Type;
+  f_drop_post : v_Self -> v_Self -> Type;
+  f_drop : v_Self -> v_Self;
+}

hax-lib/proof-libs/fstar/core/Core.Ops.Function.fsti

@@ -0,0 +1,35 @@
+module Core.Ops.Function
+
+[@FStar.Tactics.Typeclasses.tcclass]
+class t_FnOnce
+  (v_Self: Type0) (v_Args: Type0)
+  = {
+  f_Output:Type0;
+  f_call_once_pre:v_Self -> v_Args
+    -> Type0;
+  f_call_once_post:
+      v_Self ->
+      v_Args ->
+      f_Output
+    -> Type0;
+  f_call_once:x0: v_Self -> x1: v_Args
+    -> Prims.Pure f_Output
+        (f_call_once_pre x0 x1)
+        (fun result ->
+            f_call_once_post x0 x1 result)
+}
+
+[@FStar.Tactics.Typeclasses.tcclass]
+class t_Fn (v_Self: Type0) (v_Args: Type0)
+  = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_11844238443650317928:t_FnOnce
+    v_Self v_Args;
+  f_call_pre:v_Self -> v_Args -> Type0;
+  f_call_post:v_Self -> v_Args -> _
+    -> Type0;
+  f_call:x0: v_Self -> x1: v_Args
+    -> Prims.Pure _super_11844238443650317928.f_Output
+        (f_call_pre x0 x1)
+        (fun result ->
+            f_call_post x0 x1 result)
+}