Merge pull request #33 from AeneasVerif/son_refactor

Update the code following Charon's refactor

1 files changed, 23 insertions, 23 deletions

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index 5a9776ab..823df03a 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
@@ -23,12 +23,6 @@ let betree_list_partition_at_pivot_decreases (t : Type0)
   (self : betree_list_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
 unfold
 let betree_node_lookup_first_message_for_key_decreases (key : u64)
@@ -42,10 +36,10 @@ let betree_node_apply_upserts_decreases
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
 unfold
-let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
-  (st : state) : nat =
+let betree_node_lookup_in_bindings_decreases (key : u64)
+  (bindings : betree_list_t (u64 & u64)) : nat =
   admit ()
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
@@ -54,17 +48,10 @@ let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_mut_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
 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 =
+let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
+  (st : state) : nat =
   admit ()
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
@@ -86,11 +73,17 @@ let betree_node_apply_messages_to_internal_decreases
   (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
 unfold
-let betree_node_apply_messages_decreases (self : betree_node_t)
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+let betree_node_lookup_mut_in_bindings_decreases (key : u64)
+  (bindings : betree_list_t (u64 & u64)) : nat =
+  admit ()
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
+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::Internal::{4}::flush]: decreases clause *)
@@ -100,3 +93,10 @@ let betree_internal_flush_decreases (self : betree_internal_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
   admit ()
 
+(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+unfold
+let betree_node_apply_messages_decreases (self : betree_node_t)
+  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
+  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+  admit ()
+