Regenerate the test files

7 files changed, 559 insertions, 559 deletions

diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index 5a9776ab..823df03a 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/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 ()
+
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index f1bc1191..bd4e37d4 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -222,24 +222,6 @@ let betree_leaf_split_back
   let* _ = betree_store_leaf_node_fwd id1 content1 st0 in
   betree_node_id_counter_fresh_id_back node_id_cnt0
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-let rec betree_node_lookup_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (option u64))
-  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i = key
-    then Return (Some i0)
-    else
-      if i > key
-      then Return None
-      else betree_node_lookup_in_bindings_fwd key tl
-  | BetreeListNil -> Return None
-  end
-
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
 let rec betree_node_lookup_first_message_for_key_fwd
   (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
@@ -326,8 +308,50 @@ let rec betree_node_apply_upserts_back
     betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
       BetreeMessageInsert v)
 
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+let rec betree_node_lookup_in_bindings_fwd
+  (key : u64) (bindings : betree_list_t (u64 & u64)) :
+  Tot (result (option u64))
+  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i = key
+    then Return (Some i0)
+    else
+      if i > key
+      then Return None
+      else betree_node_lookup_in_bindings_fwd key tl
+  | BetreeListNil -> Return None
+  end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+let rec betree_internal_lookup_in_children_fwd
+  (self : betree_internal_t) (key : u64) (st : state) :
+  Tot (result (state & (option u64)))
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then betree_node_lookup_fwd self.betree_internal_left key st
+  else betree_node_lookup_fwd self.betree_internal_right key st
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+and betree_internal_lookup_in_children_back
+  (self : betree_internal_t) (key : u64) (st : state) :
+  Tot (result betree_internal_t)
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then
+    let* n = betree_node_lookup_back self.betree_internal_left key st in
+    Return { self with betree_internal_left = n }
+  else
+    let* n = betree_node_lookup_back self.betree_internal_right key st in
+    Return { self with betree_internal_right = n }
+
 (** [betree_main::betree::Node::{5}::lookup]: forward function *)
-let rec betree_node_lookup_fwd
+and betree_node_lookup_fwd
   (self : betree_node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
   (decreases (betree_node_lookup_decreases self key st))
@@ -451,123 +475,6 @@ and betree_node_lookup_back
     Return (BetreeNodeLeaf node)
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-and betree_internal_lookup_in_children_fwd
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result (state & (option u64)))
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then betree_node_lookup_fwd self.betree_internal_left key st
-  else betree_node_lookup_fwd self.betree_internal_right key st
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-and betree_internal_lookup_in_children_back
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result betree_internal_t)
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then
-    let* n = betree_node_lookup_back self.betree_internal_left key st in
-    Return { self with betree_internal_left = n }
-  else
-    let* n = betree_node_lookup_back self.betree_internal_right key st in
-    Return { self with betree_internal_right = n }
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-let rec betree_node_lookup_mut_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return (BetreeListCons (i, i0) tl)
-    else betree_node_lookup_mut_in_bindings_fwd key tl
-  | BetreeListNil -> Return BetreeListNil
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-let rec betree_node_lookup_mut_in_bindings_back
-  (key : u64) (bindings : betree_list_t (u64 & u64))
-  (ret : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return ret
-    else
-      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
-      Return (BetreeListCons (i, i0) tl0)
-  | BetreeListNil -> Return ret
-  end
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-let betree_node_apply_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64)) (key : u64)
-  (new_msg : betree_message_t) :
-  result (betree_list_t (u64 & u64))
-  =
-  let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
-  let* b = betree_list_head_has_key_fwd u64 bindings0 key in
-  if b
-  then
-    let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
-    begin match new_msg with
-    | BetreeMessageInsert v ->
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    | BetreeMessageDelete ->
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    | BetreeMessageUpsert s ->
-      let (_, i) = hd in
-      let* v = betree_upsert_update_fwd (Some i) s in
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    end
-  else
-    begin match new_msg with
-    | BetreeMessageInsert v ->
-      let* bindings1 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    | BetreeMessageDelete ->
-      betree_node_lookup_mut_in_bindings_back key bindings bindings0
-    | BetreeMessageUpsert s ->
-      let* v = betree_upsert_update_fwd None s in
-      let* bindings1 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    end
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-let rec betree_node_apply_messages_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
-  =
-  begin match new_msgs with
-  | BetreeListCons new_msg new_msgs_tl ->
-    let (i, m) = new_msg in
-    let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
-    betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
-  | BetreeListNil -> Return bindings
-  end
-
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_node_filter_messages_for_key_fwd_back
@@ -699,8 +606,181 @@ let rec betree_node_apply_messages_to_internal_fwd_back
   | BetreeListNil -> Return msgs
   end
 
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+let rec betree_node_lookup_mut_in_bindings_fwd
+  (key : u64) (bindings : betree_list_t (u64 & u64)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i >= key
+    then Return (BetreeListCons (i, i0) tl)
+    else betree_node_lookup_mut_in_bindings_fwd key tl
+  | BetreeListNil -> Return BetreeListNil
+  end
+
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+let rec betree_node_lookup_mut_in_bindings_back
+  (key : u64) (bindings : betree_list_t (u64 & u64))
+  (ret : betree_list_t (u64 & u64)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i >= key
+    then Return ret
+    else
+      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
+      Return (BetreeListCons (i, i0) tl0)
+  | BetreeListNil -> Return ret
+  end
+
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let betree_node_apply_to_leaf_fwd_back
+  (bindings : betree_list_t (u64 & u64)) (key : u64)
+  (new_msg : betree_message_t) :
+  result (betree_list_t (u64 & u64))
+  =
+  let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
+  let* b = betree_list_head_has_key_fwd u64 bindings0 key in
+  if b
+  then
+    let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
+    begin match new_msg with
+    | BetreeMessageInsert v ->
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      let* bindings2 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings2
+    | BetreeMessageDelete ->
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    | BetreeMessageUpsert s ->
+      let (_, i) = hd in
+      let* v = betree_upsert_update_fwd (Some i) s in
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      let* bindings2 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings2
+    end
+  else
+    begin match new_msg with
+    | BetreeMessageInsert v ->
+      let* bindings1 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    | BetreeMessageDelete ->
+      betree_node_lookup_mut_in_bindings_back key bindings bindings0
+    | BetreeMessageUpsert s ->
+      let* v = betree_upsert_update_fwd None s in
+      let* bindings1 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    end
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let rec betree_node_apply_messages_to_leaf_fwd_back
+  (bindings : betree_list_t (u64 & u64))
+  (new_msgs : betree_list_t (u64 & betree_message_t)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
+  =
+  begin match new_msgs with
+  | BetreeListCons new_msg new_msgs_tl ->
+    let (i, m) = new_msg in
+    let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
+    betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
+  | BetreeListNil -> Return bindings
+  end
+
+(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+let rec betree_internal_flush_fwd
+  (self : betree_internal_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
+  Tot (result (state & (betree_list_t (u64 & betree_message_t))))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
+  =
+  let* p =
+    betree_list_partition_at_pivot_fwd betree_message_t content
+      self.betree_internal_pivot in
+  let (msgs_left, msgs_right) = p in
+  let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
+  if len_left >= params.betree_params_min_flush_size
+  then
+    let* (st0, _) =
+      betree_node_apply_messages_fwd self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* (_, node_id_cnt0) =
+      betree_node_apply_messages_back self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
+    if len_right >= params.betree_params_min_flush_size
+    then
+      let* (st1, _) =
+        betree_node_apply_messages_fwd self.betree_internal_right params
+          node_id_cnt0 msgs_right st0 in
+      let* _ =
+        betree_node_apply_messages_back self.betree_internal_right params
+          node_id_cnt0 msgs_right st0 in
+      Return (st1, BetreeListNil)
+    else Return (st0, msgs_right)
+  else
+    let* (st0, _) =
+      betree_node_apply_messages_fwd self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    let* _ =
+      betree_node_apply_messages_back self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    Return (st0, msgs_left)
+
+(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+and betree_internal_flush_back
+  (self : betree_internal_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
+  Tot (result (betree_internal_t & betree_node_id_counter_t))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
+  =
+  let* p =
+    betree_list_partition_at_pivot_fwd betree_message_t content
+      self.betree_internal_pivot in
+  let (msgs_left, msgs_right) = p in
+  let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
+  if len_left >= params.betree_params_min_flush_size
+  then
+    let* (st0, _) =
+      betree_node_apply_messages_fwd self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* (n, node_id_cnt0) =
+      betree_node_apply_messages_back self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
+    if len_right >= params.betree_params_min_flush_size
+    then
+      let* (n0, node_id_cnt1) =
+        betree_node_apply_messages_back self.betree_internal_right params
+          node_id_cnt0 msgs_right st0 in
+      Return
+        ({ self with betree_internal_left = n; betree_internal_right = n0 },
+        node_id_cnt1)
+    else Return ({ self with betree_internal_left = n }, node_id_cnt0)
+  else
+    let* (n, node_id_cnt0) =
+      betree_node_apply_messages_back self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    Return ({ self with betree_internal_right = n }, node_id_cnt0)
+
 (** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-let rec betree_node_apply_messages_fwd
+and betree_node_apply_messages_fwd
   (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) :
@@ -794,86 +874,6 @@ and betree_node_apply_messages_back
       Return (BetreeNodeLeaf { node with betree_leaf_size = len }, node_id_cnt)
   end
 
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
-and betree_internal_flush_fwd
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (state & (betree_list_t (u64 & betree_message_t))))
-  (decreases (
-    betree_internal_flush_decreases self params node_id_cnt content st))
-  =
-  let* p =
-    betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot in
-  let (msgs_left, msgs_right) = p in
-  let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
-  if len_left >= params.betree_params_min_flush_size
-  then
-    let* (st0, _) =
-      betree_node_apply_messages_fwd self.betree_internal_left params
-        node_id_cnt msgs_left st in
-    let* (_, node_id_cnt0) =
-      betree_node_apply_messages_back self.betree_internal_left params
-        node_id_cnt msgs_left st in
-    let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
-    if len_right >= params.betree_params_min_flush_size
-    then
-      let* (st1, _) =
-        betree_node_apply_messages_fwd self.betree_internal_right params
-          node_id_cnt0 msgs_right st0 in
-      let* _ =
-        betree_node_apply_messages_back self.betree_internal_right params
-          node_id_cnt0 msgs_right st0 in
-      Return (st1, BetreeListNil)
-    else Return (st0, msgs_right)
-  else
-    let* (st0, _) =
-      betree_node_apply_messages_fwd self.betree_internal_right params
-        node_id_cnt msgs_right st in
-    let* _ =
-      betree_node_apply_messages_back self.betree_internal_right params
-        node_id_cnt msgs_right st in
-    Return (st0, msgs_left)
-
-(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
-and betree_internal_flush_back
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (betree_internal_t & betree_node_id_counter_t))
-  (decreases (
-    betree_internal_flush_decreases self params node_id_cnt content st))
-  =
-  let* p =
-    betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot in
-  let (msgs_left, msgs_right) = p in
-  let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
-  if len_left >= params.betree_params_min_flush_size
-  then
-    let* (st0, _) =
-      betree_node_apply_messages_fwd self.betree_internal_left params
-        node_id_cnt msgs_left st in
-    let* (n, node_id_cnt0) =
-      betree_node_apply_messages_back self.betree_internal_left params
-        node_id_cnt msgs_left st in
-    let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
-    if len_right >= params.betree_params_min_flush_size
-    then
-      let* (n0, node_id_cnt1) =
-        betree_node_apply_messages_back self.betree_internal_right params
-          node_id_cnt0 msgs_right st0 in
-      Return
-        ({ self with betree_internal_left = n; betree_internal_right = n0 },
-        node_id_cnt1)
-    else Return ({ self with betree_internal_left = n }, node_id_cnt0)
-  else
-    let* (n, node_id_cnt0) =
-      betree_node_apply_messages_back self.betree_internal_right params
-        node_id_cnt msgs_right st in
-    Return ({ self with betree_internal_right = n }, node_id_cnt0)
-
 (** [betree_main::betree::Node::{5}::apply]: forward function *)
 let betree_node_apply_fwd
   (self : betree_node_t) (params : betree_params_t)
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti
index aad9cb43..a937c726 100644
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ b/tests/fstar/betree/BetreeMain.Types.fsti
@@ -24,13 +24,8 @@ type betree_message_t =
 (** [betree_main::betree::Leaf] *)
 type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
 
-(** [betree_main::betree::Node] *)
-type betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
 (** [betree_main::betree::Internal] *)
-and betree_internal_t =
+type betree_internal_t =
 {
   betree_internal_id : u64;
   betree_internal_pivot : u64;
@@ -38,6 +33,11 @@ and betree_internal_t =
   betree_internal_right : betree_node_t;
 }
 
+(** [betree_main::betree::Node] *)
+and betree_node_t =
+| BetreeNodeInternal : betree_internal_t -> betree_node_t
+| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+
 (** [betree_main::betree::Params] *)
 type betree_params_t =
 {
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 ()
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 12402fb4..be8ac438 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -261,24 +261,6 @@ let betree_leaf_split_back2
   let* node_id_cnt1 = betree_node_id_counter_fresh_id_back node_id_cnt0 in
   Return (st0, node_id_cnt1)
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-let rec betree_node_lookup_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (option u64))
-  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i = key
-    then Return (Some i0)
-    else
-      if i > key
-      then Return None
-      else betree_node_lookup_in_bindings_fwd key tl
-  | BetreeListNil -> Return None
-  end
-
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
 let rec betree_node_lookup_first_message_for_key_fwd
   (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
@@ -367,8 +349,52 @@ let rec betree_node_apply_upserts_back
         BetreeMessageInsert v) in
     Return (st0, msgs0)
 
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+let rec betree_node_lookup_in_bindings_fwd
+  (key : u64) (bindings : betree_list_t (u64 & u64)) :
+  Tot (result (option u64))
+  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i = key
+    then Return (Some i0)
+    else
+      if i > key
+      then Return None
+      else betree_node_lookup_in_bindings_fwd key tl
+  | BetreeListNil -> Return None
+  end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+let rec betree_internal_lookup_in_children_fwd
+  (self : betree_internal_t) (key : u64) (st : state) :
+  Tot (result (state & (option u64)))
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then betree_node_lookup_fwd self.betree_internal_left key st
+  else betree_node_lookup_fwd self.betree_internal_right key st
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+and betree_internal_lookup_in_children_back
+  (self : betree_internal_t) (key : u64) (st : state) (st0 : state) :
+  Tot (result (state & betree_internal_t))
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then
+    let* (st1, n) =
+      betree_node_lookup_back self.betree_internal_left key st st0 in
+    Return (st1, { self with betree_internal_left = n })
+  else
+    let* (st1, n) =
+      betree_node_lookup_back self.betree_internal_right key st st0 in
+    Return (st1, { self with betree_internal_right = n })
+
 (** [betree_main::betree::Node::{5}::lookup]: forward function *)
-let rec betree_node_lookup_fwd
+and betree_node_lookup_fwd
   (self : betree_node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
   (decreases (betree_node_lookup_decreases self key st))
@@ -496,125 +522,6 @@ and betree_node_lookup_back
     Return (st0, BetreeNodeLeaf node)
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-and betree_internal_lookup_in_children_fwd
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result (state & (option u64)))
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then betree_node_lookup_fwd self.betree_internal_left key st
-  else betree_node_lookup_fwd self.betree_internal_right key st
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-and betree_internal_lookup_in_children_back
-  (self : betree_internal_t) (key : u64) (st : state) (st0 : state) :
-  Tot (result (state & betree_internal_t))
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then
-    let* (st1, n) =
-      betree_node_lookup_back self.betree_internal_left key st st0 in
-    Return (st1, { self with betree_internal_left = n })
-  else
-    let* (st1, n) =
-      betree_node_lookup_back self.betree_internal_right key st st0 in
-    Return (st1, { self with betree_internal_right = n })
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-let rec betree_node_lookup_mut_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return (BetreeListCons (i, i0) tl)
-    else betree_node_lookup_mut_in_bindings_fwd key tl
-  | BetreeListNil -> Return BetreeListNil
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-let rec betree_node_lookup_mut_in_bindings_back
-  (key : u64) (bindings : betree_list_t (u64 & u64))
-  (ret : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return ret
-    else
-      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
-      Return (BetreeListCons (i, i0) tl0)
-  | BetreeListNil -> Return ret
-  end
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-let betree_node_apply_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64)) (key : u64)
-  (new_msg : betree_message_t) :
-  result (betree_list_t (u64 & u64))
-  =
-  let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
-  let* b = betree_list_head_has_key_fwd u64 bindings0 key in
-  if b
-  then
-    let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
-    begin match new_msg with
-    | BetreeMessageInsert v ->
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    | BetreeMessageDelete ->
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    | BetreeMessageUpsert s ->
-      let (_, i) = hd in
-      let* v = betree_upsert_update_fwd (Some i) s in
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    end
-  else
-    begin match new_msg with
-    | BetreeMessageInsert v ->
-      let* bindings1 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    | BetreeMessageDelete ->
-      betree_node_lookup_mut_in_bindings_back key bindings bindings0
-    | BetreeMessageUpsert s ->
-      let* v = betree_upsert_update_fwd None s in
-      let* bindings1 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    end
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-let rec betree_node_apply_messages_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
-  =
-  begin match new_msgs with
-  | BetreeListCons new_msg new_msgs_tl ->
-    let (i, m) = new_msg in
-    let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
-    betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
-  | BetreeListNil -> Return bindings
-  end
-
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_node_filter_messages_for_key_fwd_back
@@ -746,157 +653,101 @@ let rec betree_node_apply_messages_to_internal_fwd_back
   | BetreeListNil -> Return msgs
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-let rec betree_node_apply_messages_fwd
-  (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) :
-  Tot (result (state & unit))
-  (decreases (
-    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+let rec betree_node_lookup_mut_in_bindings_fwd
+  (key : u64) (bindings : betree_list_t (u64 & u64)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
   =
-  begin match self with
-  | BetreeNodeInternal node ->
-    let* (st0, content) =
-      betree_load_internal_node_fwd node.betree_internal_id st in
-    let* content0 =
-      betree_node_apply_messages_to_internal_fwd_back content msgs in
-    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
-    if num_msgs >= params.betree_params_min_flush_size
-    then
-      let* (st1, content1) =
-        betree_internal_flush_fwd node params node_id_cnt content0 st0 in
-      let* (st2, (node0, _)) =
-        betree_internal_flush_back'a node params node_id_cnt content0 st0 st1
-        in
-      let* (st3, _) =
-        betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in
-      Return (st3, ())
-    else
-      let* (st1, _) =
-        betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
-      Return (st1, ())
-  | BetreeNodeLeaf node ->
-    let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
-    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
-    let* len = betree_list_len_fwd (u64 & u64) content0 in
-    let* i = u64_mul 2 params.betree_params_split_size in
-    if len >= i
-    then
-      let* (st1, _) =
-        betree_leaf_split_fwd node content0 params node_id_cnt st0 in
-      let* (st2, _) =
-        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in
-      betree_leaf_split_back0 node content0 params node_id_cnt st0 st2
-    else
-      let* (st1, _) =
-        betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
-      Return (st1, ())
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i >= key
+    then Return (BetreeListCons (i, i0) tl)
+    else betree_node_lookup_mut_in_bindings_fwd key tl
+  | BetreeListNil -> Return BetreeListNil
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
-and betree_node_apply_messages_back'a
-  (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) (st0 : state) :
-  Tot (result (state & (betree_node_t & betree_node_id_counter_t)))
-  (decreases (
-    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+let rec betree_node_lookup_mut_in_bindings_back
+  (key : u64) (bindings : betree_list_t (u64 & u64))
+  (ret : betree_list_t (u64 & u64)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
   =
-  begin match self with
-  | BetreeNodeInternal node ->
-    let* (st1, content) =
-      betree_load_internal_node_fwd node.betree_internal_id st in
-    let* content0 =
-      betree_node_apply_messages_to_internal_fwd_back content msgs in
-    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
-    if num_msgs >= params.betree_params_min_flush_size
-    then
-      let* (st2, content1) =
-        betree_internal_flush_fwd node params node_id_cnt content0 st1 in
-      let* (st3, (node0, node_id_cnt0)) =
-        betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
-        in
-      let* _ =
-        betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
-      Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
-    else
-      let* _ =
-        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
-      Return (st0, (BetreeNodeInternal node, node_id_cnt))
-  | BetreeNodeLeaf node ->
-    let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
-    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
-    let* len = betree_list_len_fwd (u64 & u64) content0 in
-    let* i = u64_mul 2 params.betree_params_split_size in
-    if len >= i
-    then
-      let* (st2, new_node) =
-        betree_leaf_split_fwd node content0 params node_id_cnt st1 in
-      let* (st3, _) =
-        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
-      let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
-        in
-      let* (st4, node_id_cnt0) =
-        betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in
-      Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i >= key
+    then Return ret
     else
-      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
-      Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len },
-        node_id_cnt))
+      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
+      Return (BetreeListCons (i, i0) tl0)
+  | BetreeListNil -> Return ret
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *)
-and betree_node_apply_messages_back1
-  (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) (st0 : state) :
-  Tot (result (state & unit))
-  (decreases (
-    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let betree_node_apply_to_leaf_fwd_back
+  (bindings : betree_list_t (u64 & u64)) (key : u64)
+  (new_msg : betree_message_t) :
+  result (betree_list_t (u64 & u64))
   =
-  begin match self with
-  | BetreeNodeInternal node ->
-    let* (st1, content) =
-      betree_load_internal_node_fwd node.betree_internal_id st in
-    let* content0 =
-      betree_node_apply_messages_to_internal_fwd_back content msgs in
-    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
-    if num_msgs >= params.betree_params_min_flush_size
-    then
-      let* (st2, content1) =
-        betree_internal_flush_fwd node params node_id_cnt content0 st1 in
-      let* (st3, (node0, _)) =
-        betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
-        in
-      let* _ =
-        betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
-      betree_internal_flush_back1 node params node_id_cnt content0 st1 st0
-    else
-      let* _ =
-        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
-      Return (st0, ())
-  | BetreeNodeLeaf node ->
-    let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
-    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
-    let* len = betree_list_len_fwd (u64 & u64) content0 in
-    let* i = u64_mul 2 params.betree_params_split_size in
-    if len >= i
-    then
-      let* (st2, _) =
-        betree_leaf_split_fwd node content0 params node_id_cnt st1 in
-      let* (st3, _) =
-        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
-      let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
-        in
-      betree_leaf_split_back1 node content0 params node_id_cnt st1 st0
-    else
-      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
-      Return (st0, ())
+  let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
+  let* b = betree_list_head_has_key_fwd u64 bindings0 key in
+  if b
+  then
+    let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
+    begin match new_msg with
+    | BetreeMessageInsert v ->
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      let* bindings2 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings2
+    | BetreeMessageDelete ->
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    | BetreeMessageUpsert s ->
+      let (_, i) = hd in
+      let* v = betree_upsert_update_fwd (Some i) s in
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      let* bindings2 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings2
+    end
+  else
+    begin match new_msg with
+    | BetreeMessageInsert v ->
+      let* bindings1 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    | BetreeMessageDelete ->
+      betree_node_lookup_mut_in_bindings_back key bindings bindings0
+    | BetreeMessageUpsert s ->
+      let* v = betree_upsert_update_fwd None s in
+      let* bindings1 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    end
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let rec betree_node_apply_messages_to_leaf_fwd_back
+  (bindings : betree_list_t (u64 & u64))
+  (new_msgs : betree_list_t (u64 & betree_message_t)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
+  =
+  begin match new_msgs with
+  | BetreeListCons new_msg new_msgs_tl ->
+    let (i, m) = new_msg in
+    let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
+    betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
+  | BetreeListNil -> Return bindings
   end
 
 (** [betree_main::betree::Internal::{4}::flush]: forward function *)
-and betree_internal_flush_fwd
+let rec betree_internal_flush_fwd
   (self : betree_internal_t) (params : betree_params_t)
   (node_id_cnt : betree_node_id_counter_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) :
@@ -1052,6 +903,155 @@ and betree_internal_flush_back1
         node_id_cnt msgs_right st st2 in
     Return (st0, ())
 
+(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
+and betree_node_apply_messages_fwd
+  (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) :
+  Tot (result (state & unit))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+  =
+  begin match self with
+  | BetreeNodeInternal node ->
+    let* (st0, content) =
+      betree_load_internal_node_fwd node.betree_internal_id st in
+    let* content0 =
+      betree_node_apply_messages_to_internal_fwd_back content msgs in
+    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+    if num_msgs >= params.betree_params_min_flush_size
+    then
+      let* (st1, content1) =
+        betree_internal_flush_fwd node params node_id_cnt content0 st0 in
+      let* (st2, (node0, _)) =
+        betree_internal_flush_back'a node params node_id_cnt content0 st0 st1
+        in
+      let* (st3, _) =
+        betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in
+      Return (st3, ())
+    else
+      let* (st1, _) =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
+      Return (st1, ())
+  | BetreeNodeLeaf node ->
+    let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+    let* len = betree_list_len_fwd (u64 & u64) content0 in
+    let* i = u64_mul 2 params.betree_params_split_size in
+    if len >= i
+    then
+      let* (st1, _) =
+        betree_leaf_split_fwd node content0 params node_id_cnt st0 in
+      let* (st2, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in
+      betree_leaf_split_back0 node content0 params node_id_cnt st0 st2
+    else
+      let* (st1, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
+      Return (st1, ())
+  end
+
+(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
+and betree_node_apply_messages_back'a
+  (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) (st0 : state) :
+  Tot (result (state & (betree_node_t & betree_node_id_counter_t)))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+  =
+  begin match self with
+  | BetreeNodeInternal node ->
+    let* (st1, content) =
+      betree_load_internal_node_fwd node.betree_internal_id st in
+    let* content0 =
+      betree_node_apply_messages_to_internal_fwd_back content msgs in
+    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+    if num_msgs >= params.betree_params_min_flush_size
+    then
+      let* (st2, content1) =
+        betree_internal_flush_fwd node params node_id_cnt content0 st1 in
+      let* (st3, (node0, node_id_cnt0)) =
+        betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
+        in
+      let* _ =
+        betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
+      Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
+    else
+      let* _ =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
+      Return (st0, (BetreeNodeInternal node, node_id_cnt))
+  | BetreeNodeLeaf node ->
+    let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+    let* len = betree_list_len_fwd (u64 & u64) content0 in
+    let* i = u64_mul 2 params.betree_params_split_size in
+    if len >= i
+    then
+      let* (st2, new_node) =
+        betree_leaf_split_fwd node content0 params node_id_cnt st1 in
+      let* (st3, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
+      let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
+        in
+      let* (st4, node_id_cnt0) =
+        betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in
+      Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
+    else
+      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
+      Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len },
+        node_id_cnt))
+  end
+
+(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *)
+and betree_node_apply_messages_back1
+  (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) (st0 : state) :
+  Tot (result (state & unit))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+  =
+  begin match self with
+  | BetreeNodeInternal node ->
+    let* (st1, content) =
+      betree_load_internal_node_fwd node.betree_internal_id st in
+    let* content0 =
+      betree_node_apply_messages_to_internal_fwd_back content msgs in
+    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+    if num_msgs >= params.betree_params_min_flush_size
+    then
+      let* (st2, content1) =
+        betree_internal_flush_fwd node params node_id_cnt content0 st1 in
+      let* (st3, (node0, _)) =
+        betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
+        in
+      let* _ =
+        betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
+      betree_internal_flush_back1 node params node_id_cnt content0 st1 st0
+    else
+      let* _ =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
+      Return (st0, ())
+  | BetreeNodeLeaf node ->
+    let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+    let* len = betree_list_len_fwd (u64 & u64) content0 in
+    let* i = u64_mul 2 params.betree_params_split_size in
+    if len >= i
+    then
+      let* (st2, _) =
+        betree_leaf_split_fwd node content0 params node_id_cnt st1 in
+      let* (st3, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
+      let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
+        in
+      betree_leaf_split_back1 node content0 params node_id_cnt st1 st0
+    else
+      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
+      Return (st0, ())
+  end
+
 (** [betree_main::betree::Node::{5}::apply]: forward function *)
 let betree_node_apply_fwd
   (self : betree_node_t) (params : betree_params_t)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
index aad9cb43..a937c726 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
@@ -24,13 +24,8 @@ type betree_message_t =
 (** [betree_main::betree::Leaf] *)
 type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
 
-(** [betree_main::betree::Node] *)
-type betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
 (** [betree_main::betree::Internal] *)
-and betree_internal_t =
+type betree_internal_t =
 {
   betree_internal_id : u64;
   betree_internal_pivot : u64;
@@ -38,6 +33,11 @@ and betree_internal_t =
   betree_internal_right : betree_node_t;
 }
 
+(** [betree_main::betree::Node] *)
+and betree_node_t =
+| BetreeNodeInternal : betree_internal_t -> betree_node_t
+| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+
 (** [betree_main::betree::Params] *)
 type betree_params_t =
 {
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index d790bfa9..2cdd6e21 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -202,16 +202,16 @@ let _ = assert_norm (choose_test_fwd = Return ())
 let test_char_fwd : result char =
   Return 'a'
 
-(** [no_nested_borrows::NodeElem] *)
-type node_elem_t (t : Type0) =
-| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
-| NodeElemNil : node_elem_t t
-
 (** [no_nested_borrows::Tree] *)
-and tree_t (t : Type0) =
+type tree_t (t : Type0) =
 | TreeLeaf : t -> tree_t t
 | TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
 
+(** [no_nested_borrows::NodeElem] *)
+and node_elem_t (t : Type0) =
+| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
+| NodeElemNil : node_elem_t t
+
 (** [no_nested_borrows::list_length]: forward function *)
 let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
   begin match l with