1 files changed, 30 insertions, 0 deletions
diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti
new file mode 100644
index 00000000..dc49601a
--- /dev/null
+++ b/tests/fstar/betree/BetreeMain.Opaque.fsti
@@ -0,0 +1,30 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: opaque function definitions *)
+module BetreeMain.Opaque
+open Primitives
+include BetreeMain.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree_utils::load_internal_node] *)
+val betree_utils_load_internal_node_fwd
+  : u64 -> state -> result (state & (betree_list_t (u64 & betree_message_t)))
+
+(** [betree_main::betree_utils::store_internal_node] *)
+val betree_utils_store_internal_node_fwd
+  :
+  u64 -> betree_list_t (u64 & betree_message_t) -> state -> result (state &
+    unit)
+
+(** [betree_main::betree_utils::load_leaf_node] *)
+val betree_utils_load_leaf_node_fwd
+  : u64 -> state -> result (state & (betree_list_t (u64 & u64)))
+
+(** [betree_main::betree_utils::store_leaf_node] *)
+val betree_utils_store_leaf_node_fwd
+  : u64 -> betree_list_t (u64 & u64) -> state -> result (state & unit)
+
+(** [core::option::Option::{0}::unwrap] *)
+val core_option_option_unwrap_fwd
+  (t : Type0) : option t -> state -> result (state & t)
+