Merge pull request #64 from AeneasVerif/son/merge_back

Merge the forward/backward functions

1 files changed, 117 insertions, 0 deletions

diff --git a/tests/fstar-split/betree/BetreeMain.Clauses.Template.fst b/tests/fstar-split/betree/BetreeMain.Clauses.Template.fst
new file mode 100644
index 00000000..537705c5
--- /dev/null
+++ b/tests/fstar-split/betree/BetreeMain.Clauses.Template.fst
@@ -0,0 +1,117 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: templates for the decreases clauses *)
+module BetreeMain.Clauses.Template
+open Primitives
+open BetreeMain.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause
+    Source: 'src/betree.rs', lines 276:4-276:24 *)
+unfold
+let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause
+    Source: 'src/betree.rs', lines 284:4-284:51 *)
+unfold
+let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
+  (n : u64) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
+    Source: 'src/betree.rs', lines 339:4-339:73 *)
+unfold
+let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
+  (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
+unfold
+let betree_Node_lookup_first_message_for_key_decreases (key : u64)
+  (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause
+    Source: 'src/betree.rs', lines 636:4-636:80 *)
+unfold
+let betree_Node_lookup_in_bindings_decreases (key : u64)
+  (bindings : betree_List_t (u64 & u64)) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
+unfold
+let betree_Node_apply_upserts_decreases
+  (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
+  (key : u64) (st : state) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
+unfold
+let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
+  (key : u64) (st : state) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
+unfold
+let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
+  (st : state) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause
+    Source: 'src/betree.rs', lines 674:4-674:77 *)
+unfold
+let betree_Node_filter_messages_for_key_decreases (key : u64)
+  (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
+unfold
+let betree_Node_lookup_first_message_after_key_decreases (key : u64)
+  (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause
+    Source: 'src/betree.rs', lines 502:4-505:5 *)
+unfold
+let betree_Node_apply_messages_to_internal_decreases
+  (msgs : betree_List_t (u64 & betree_Message_t))
+  (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
+unfold
+let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
+  (bindings : betree_List_t (u64 & u64)) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause
+    Source: 'src/betree.rs', lines 444:4-447:5 *)
+unfold
+let betree_Node_apply_messages_to_leaf_decreases
+  (bindings : betree_List_t (u64 & u64))
+  (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
+unfold
+let betree_Internal_flush_decreases (self : betree_Internal_t)
+  (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
+  (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat =
+  admit ()
+
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
+unfold
+let betree_Node_apply_messages_decreases (self : betree_Node_t)
+  (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
+  (msgs : betree_List_t (u64 & betree_Message_t)) (st : state) : nat =
+  admit ()
+