Update the F* betree

1 files changed, 25 insertions, 15 deletions

diff --git a/tests/fstar/betree/Betree.Clauses.fst b/tests/fstar/betree/Betree.Clauses.fst
index ae201cee..c50bf421 100644
--- a/tests/fstar/betree/Betree.Clauses.fst
+++ b/tests/fstar/betree/Betree.Clauses.fst
@@ -103,36 +103,46 @@ let wf_nat_pair_lem (p0 p1 : nat_pair) :
 
 (** [betree_main::betree::List::{1}::len]: decreases clause *)
 unfold
-let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : betree_List_t t =
+let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t) (len : u64) : betree_List_t t =
   self
 
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
 unfold
-let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
-  (n : u64) : nat =
+let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t)
+  (out : betree_List_t t) =
+  self
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
+unfold
+let betree_List_split_at_loop_decreases (t : Type0) (n : u64)
+  (beg : betree_List_t t) (self : betree_List_t t) : nat =
   n
 
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
 unfold
-let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
-  (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) =
+let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0)
+  (pivot : u64) (beg : betree_List_t (u64 & t)) (end0 : betree_List_t (u64 & t))
+  (self : betree_List_t (u64 & t)) =
   self
 
 (** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
 unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
+let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) =
   bindings
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
 unfold
-let betree_Node_lookup_first_message_for_key_decreases (key : u64)
+let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
 (** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
 unfold
-let betree_Node_apply_upserts_decreases
+let betree_Node_apply_upserts_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) : betree_List_t (u64 & betree_Message_t) =
   msgs
@@ -151,29 +161,29 @@ let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
 unfold
-let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
+let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) =
   bindings
 
 unfold
-let betree_Node_apply_messages_to_leaf_decreases
+let betree_Node_apply_messages_to_leaf_loop_decreases
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   new_msgs
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
 unfold
-let betree_Node_filter_messages_for_key_decreases (key : u64)
+let betree_Node_filter_messages_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
 unfold
-let betree_Node_lookup_first_message_after_key_decreases (key : u64)
+let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
-let betree_Node_apply_messages_to_internal_decreases
+let betree_Node_apply_messages_to_internal_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   new_msgs