Regenerate the test files and add the fstar-split tests

3 files changed, 302 insertions, 883 deletions

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 6c3c2161..a3065f3d 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -8,7 +8,7 @@ include BetreeMain.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::load_internal_node]: forward function
+(** [betree_main::betree::load_internal_node]:
     Source: 'src/betree.rs', lines 36:0-36:52 *)
 let betree_load_internal_node
   (id : u64) (st : state) :
@@ -16,58 +16,48 @@ let betree_load_internal_node
   =
   betree_utils_load_internal_node id st
 
-(** [betree_main::betree::store_internal_node]: forward function
+(** [betree_main::betree::store_internal_node]:
     Source: 'src/betree.rs', lines 41:0-41:60 *)
 let betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
   result (state & unit)
   =
-  let* (st0, _) = betree_utils_store_internal_node id content st in
-  Return (st0, ())
+  let* (st1, _) = betree_utils_store_internal_node id content st in
+  Return (st1, ())
 
-(** [betree_main::betree::load_leaf_node]: forward function
+(** [betree_main::betree::load_leaf_node]:
     Source: 'src/betree.rs', lines 46:0-46:44 *)
 let betree_load_leaf_node
   (id : u64) (st : state) : result (state & (betree_List_t (u64 & u64))) =
   betree_utils_load_leaf_node id st
 
-(** [betree_main::betree::store_leaf_node]: forward function
+(** [betree_main::betree::store_leaf_node]:
     Source: 'src/betree.rs', lines 51:0-51:52 *)
 let betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
   result (state & unit)
   =
-  let* (st0, _) = betree_utils_store_leaf_node id content st in
-  Return (st0, ())
-
-(** [betree_main::betree::fresh_node_id]: forward function
-    Source: 'src/betree.rs', lines 55:0-55:48 *)
-let betree_fresh_node_id (counter : u64) : result u64 =
-  let* _ = u64_add counter 1 in Return counter
+  let* (st1, _) = betree_utils_store_leaf_node id content st in
+  Return (st1, ())
 
-(** [betree_main::betree::fresh_node_id]: backward function 0
+(** [betree_main::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
-let betree_fresh_node_id_back (counter : u64) : result u64 =
-  u64_add counter 1
+let betree_fresh_node_id (counter : u64) : result (u64 & u64) =
+  let* counter1 = u64_add counter 1 in Return (counter, counter1)
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
     Source: 'src/betree.rs', lines 206:4-206:20 *)
 let betree_NodeIdCounter_new : result betree_NodeIdCounter_t =
   Return { next_node_id = 0 }
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
     Source: 'src/betree.rs', lines 210:4-210:36 *)
 let betree_NodeIdCounter_fresh_id
-  (self : betree_NodeIdCounter_t) : result u64 =
-  let* _ = u64_add self.next_node_id 1 in Return self.next_node_id
+  (self : betree_NodeIdCounter_t) : result (u64 & betree_NodeIdCounter_t) =
+  let* i = u64_add self.next_node_id 1 in
+  Return (self.next_node_id, { next_node_id = i })
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0
-    Source: 'src/betree.rs', lines 210:4-210:36 *)
-let betree_NodeIdCounter_fresh_id_back
-  (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t =
-  let* i = u64_add self.next_node_id 1 in Return { next_node_id = i }
-
-(** [betree_main::betree::upsert_update]: forward function
+(** [betree_main::betree::upsert_update]:
     Source: 'src/betree.rs', lines 234:0-234:70 *)
 let betree_upsert_update
   (prev : option u64) (st : betree_UpsertFunState_t) : result u64 =
@@ -75,30 +65,30 @@ let betree_upsert_update
   | None ->
     begin match st with
     | Betree_UpsertFunState_Add v -> Return v
-    | Betree_UpsertFunState_Sub i -> Return 0
+    | Betree_UpsertFunState_Sub _ -> Return 0
     end
-  | Some prev0 ->
+  | Some prev1 ->
     begin match st with
     | Betree_UpsertFunState_Add v ->
-      let* margin = u64_sub core_u64_max prev0 in
-      if margin >= v then u64_add prev0 v else Return core_u64_max
+      let* margin = u64_sub core_u64_max prev1 in
+      if margin >= v then u64_add prev1 v else Return core_u64_max
     | Betree_UpsertFunState_Sub v ->
-      if prev0 >= v then u64_sub prev0 v else Return 0
+      if prev1 >= v then u64_sub prev1 v else Return 0
     end
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
     Source: 'src/betree.rs', lines 276:4-276:24 *)
 let rec betree_List_len
   (t : Type0) (self : betree_List_t t) :
   Tot (result u64) (decreases (betree_List_len_decreases t self))
   =
   begin match self with
-  | Betree_List_Cons x tl -> let* i = betree_List_len t tl in u64_add 1 i
+  | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i
   | Betree_List_Nil -> Return 0
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
     Source: 'src/betree.rs', lines 284:4-284:51 *)
 let rec betree_List_split_at
   (t : Type0) (self : betree_List_t t) (n : u64) :
@@ -118,52 +108,42 @@ let rec betree_List_split_at
     | Betree_List_Nil -> Fail Failure
     end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
     Source: 'src/betree.rs', lines 299:4-299:34 *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
-  let tl = core_mem_replace (betree_List_t t) self Betree_List_Nil in
+  let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   let l = tl in
   Return (Betree_List_Cons x l)
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
-    Source: 'src/betree.rs', lines 306:4-306:32 *)
-let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
-  let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
-  begin match ls with
-  | Betree_List_Cons x tl -> Return x
-  | Betree_List_Nil -> Fail Failure
-  end
-
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
     Source: 'src/betree.rs', lines 306:4-306:32 *)
-let betree_List_pop_front_back
-  (t : Type0) (self : betree_List_t t) : result (betree_List_t t) =
-  let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
+let betree_List_pop_front
+  (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) =
+  let (ls, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   begin match ls with
-  | Betree_List_Cons x tl -> Return tl
+  | Betree_List_Cons x tl -> Return (x, tl)
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
     Source: 'src/betree.rs', lines 318:4-318:22 *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
-  | Betree_List_Cons hd l -> Return hd
+  | Betree_List_Cons hd _ -> Return hd
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
     Source: 'src/betree.rs', lines 327:4-327:44 *)
 let betree_ListTupleU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
-  | Betree_List_Cons hd l -> let (i, _) = hd in Return (i = key)
+  | Betree_List_Cons hd _ -> let (i, _) = hd in Return (i = key)
   | Betree_List_Nil -> Return false
   end
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
     Source: 'src/betree.rs', lines 339:4-339:73 *)
 let rec betree_ListTupleU64T_partition_at_pivot
   (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
@@ -183,119 +163,54 @@ let rec betree_ListTupleU64T_partition_at_pivot
   | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
   end
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
     Source: 'src/betree.rs', lines 359:4-364:17 *)
 let betree_Leaf_split
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
   (st : state) :
-  result (state & betree_Internal_t)
-  =
-  let* p = betree_List_split_at (u64 & u64) content params.split_size in
-  let (content0, content1) = p in
-  let* p0 = betree_List_hd (u64 & u64) content1 in
-  let (pivot, _) = p0 in
-  let* id0 = betree_NodeIdCounter_fresh_id node_id_cnt in
-  let* node_id_cnt0 = betree_NodeIdCounter_fresh_id_back node_id_cnt in
-  let* id1 = betree_NodeIdCounter_fresh_id node_id_cnt0 in
-  let* (st0, _) = betree_store_leaf_node id0 content0 st in
-  let* (st1, _) = betree_store_leaf_node id1 content1 st0 in
-  let n = Betree_Node_Leaf { id = id0; size = params.split_size } in
-  let n0 = Betree_Node_Leaf { id = id1; size = params.split_size } in
-  Return (st1, { id = self.id; pivot = pivot; left = n; right = n0 })
-
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 0
-    Source: 'src/betree.rs', lines 359:4-364:17 *)
-let betree_Leaf_split_back0
-  (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
-  (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
-  (st : state) (st0 : state) :
-  result (state & unit)
-  =
-  let* p = betree_List_split_at (u64 & u64) content params.split_size in
-  let (content0, content1) = p in
-  let* _ = betree_List_hd (u64 & u64) content1 in
-  let* id0 = betree_NodeIdCounter_fresh_id node_id_cnt in
-  let* node_id_cnt0 = betree_NodeIdCounter_fresh_id_back node_id_cnt in
-  let* id1 = betree_NodeIdCounter_fresh_id node_id_cnt0 in
-  let* (st1, _) = betree_store_leaf_node id0 content0 st in
-  let* _ = betree_store_leaf_node id1 content1 st1 in
-  Return (st0, ())
-
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 1
-    Source: 'src/betree.rs', lines 359:4-364:17 *)
-let betree_Leaf_split_back1
-  (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
-  (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
-  (st : state) (st0 : state) :
-  result (state & unit)
+  result (state & (betree_Internal_t & betree_NodeIdCounter_t))
   =
   let* p = betree_List_split_at (u64 & u64) content params.split_size in
   let (content0, content1) = p in
-  let* _ = betree_List_hd (u64 & u64) content1 in
-  let* id0 = betree_NodeIdCounter_fresh_id node_id_cnt in
-  let* node_id_cnt0 = betree_NodeIdCounter_fresh_id_back node_id_cnt in
-  let* id1 = betree_NodeIdCounter_fresh_id node_id_cnt0 in
+  let* p1 = betree_List_hd (u64 & u64) content1 in
+  let (pivot, _) = p1 in
+  let* (id0, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in
+  let* (id1, nic1) = betree_NodeIdCounter_fresh_id nic in
   let* (st1, _) = betree_store_leaf_node id0 content0 st in
-  let* _ = betree_store_leaf_node id1 content1 st1 in
-  Return (st0, ())
-
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2
-    Source: 'src/betree.rs', lines 359:4-364:17 *)
-let betree_Leaf_split_back2
-  (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
-  (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
-  (st : state) (st0 : state) :
-  result (state & betree_NodeIdCounter_t)
-  =
-  let* p = betree_List_split_at (u64 & u64) content params.split_size in
-  let (content0, content1) = p in
-  let* _ = betree_List_hd (u64 & u64) content1 in
-  let* id0 = betree_NodeIdCounter_fresh_id node_id_cnt in
-  let* node_id_cnt0 = betree_NodeIdCounter_fresh_id_back node_id_cnt in
-  let* id1 = betree_NodeIdCounter_fresh_id node_id_cnt0 in
-  let* (st1, _) = betree_store_leaf_node id0 content0 st in
-  let* _ = betree_store_leaf_node id1 content1 st1 in
-  let* node_id_cnt1 = betree_NodeIdCounter_fresh_id_back node_id_cnt0 in
-  Return (st0, node_id_cnt1)
+  let* (st2, _) = betree_store_leaf_node id1 content1 st1 in
+  let n = Betree_Node_Leaf { id = id0; size = params.split_size } in
+  let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in
+  Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, nic1))
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
     Source: 'src/betree.rs', lines 789:4-792:34 *)
 let rec betree_Node_lookup_first_message_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
-  Tot (result (betree_List_t (u64 & betree_Message_t)))
+  Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
+    betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))))
   (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs))
   =
   begin match msgs with
   | Betree_List_Cons x next_msgs ->
     let (i, m) = x in
     if i >= key
-    then Return (Betree_List_Cons (i, m) next_msgs)
-    else betree_Node_lookup_first_message_for_key key next_msgs
-  | Betree_List_Nil -> Return Betree_List_Nil
-  end
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0
-    Source: 'src/betree.rs', lines 789:4-792:34 *)
-let rec betree_Node_lookup_first_message_for_key_back
-  (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
-  (ret : betree_List_t (u64 & betree_Message_t)) :
-  Tot (result (betree_List_t (u64 & betree_Message_t)))
-  (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs))
-  =
-  begin match msgs with
-  | Betree_List_Cons x next_msgs ->
-    let (i, m) = x in
-    if i >= key
-    then Return ret
+    then
+      let back_'a = fun ret -> Return ret in
+      Return (Betree_List_Cons (i, m) next_msgs, back_'a)
     else
-      let* next_msgs0 =
-        betree_Node_lookup_first_message_for_key_back key next_msgs ret in
-      Return (Betree_List_Cons (i, m) next_msgs0)
-  | Betree_List_Nil -> Return ret
+      let* (l, lookup_first_message_for_key_back) =
+        betree_Node_lookup_first_message_for_key key next_msgs in
+      let back_'a =
+        fun ret ->
+          let* next_msgs1 = lookup_first_message_for_key_back ret in
+          Return (Betree_List_Cons (i, m) next_msgs1) in
+      Return (l, back_'a)
+  | Betree_List_Nil ->
+    let back_'a = fun ret -> Return ret in Return (Betree_List_Nil, back_'a)
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
     Source: 'src/betree.rs', lines 636:4-636:80 *)
 let rec betree_Node_lookup_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
@@ -304,221 +219,110 @@ let rec betree_Node_lookup_in_bindings
   =
   begin match bindings with
   | Betree_List_Cons hd tl ->
-    let (i, i0) = hd in
+    let (i, i1) = hd in
     if i = key
-    then Return (Some i0)
+    then Return (Some i1)
     else if i > key then Return None else betree_Node_lookup_in_bindings key tl
   | Betree_List_Nil -> Return None
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 let rec betree_Node_apply_upserts
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
-  Tot (result (state & u64))
-  (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
-  =
-  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in
-  if b
-  then
-    let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in
-    let (_, m) = msg in
-    begin match m with
-    | Betree_Message_Insert i -> Fail Failure
-    | Betree_Message_Delete -> Fail Failure
-    | Betree_Message_Upsert s ->
-      let* v = betree_upsert_update prev s in
-      let* msgs0 = betree_List_pop_front_back (u64 & betree_Message_t) msgs in
-      betree_Node_apply_upserts msgs0 (Some v) key st
-    end
-  else
-    let* (st0, v) = core_option_Option_unwrap u64 prev st in
-    let* _ =
-      betree_List_push_front (u64 & betree_Message_t) msgs (key,
-        Betree_Message_Insert v) in
-    Return (st0, v)
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0
-    Source: 'src/betree.rs', lines 819:4-819:90 *)
-let rec betree_Node_apply_upserts_back
-  (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) (st0 : state) :
-  Tot (result (state & (betree_List_t (u64 & betree_Message_t))))
+  Tot (result (state & (u64 & (betree_List_t (u64 & betree_Message_t)))))
   (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
   =
   let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in
   if b
   then
-    let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in
+    let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in
     let (_, m) = msg in
     begin match m with
-    | Betree_Message_Insert i -> Fail Failure
+    | Betree_Message_Insert _ -> Fail Failure
     | Betree_Message_Delete -> Fail Failure
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update prev s in
-      let* msgs0 = betree_List_pop_front_back (u64 & betree_Message_t) msgs in
-      betree_Node_apply_upserts_back msgs0 (Some v) key st st0
+      betree_Node_apply_upserts l (Some v) key st
     end
   else
-    let* (_, v) = core_option_Option_unwrap u64 prev st in
-    let* msgs0 =
+    let* (st1, v) = core_option_Option_unwrap u64 prev st in
+    let* l =
       betree_List_push_front (u64 & betree_Message_t) msgs (key,
         Betree_Message_Insert v) in
-    Return (st0, msgs0)
+    Return (st1, (v, l))
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
     Source: 'src/betree.rs', lines 395:4-395:63 *)
 let rec betree_Internal_lookup_in_children
   (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.pivot
-  then betree_Node_lookup self.left key st
-  else betree_Node_lookup self.right key st
-
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0
-    Source: 'src/betree.rs', lines 395:4-395:63 *)
-and betree_Internal_lookup_in_children_back
-  (self : betree_Internal_t) (key : u64) (st : state) (st0 : state) :
-  Tot (result (state & betree_Internal_t))
+  Tot (result (state & ((option u64) & betree_Internal_t)))
   (decreases (betree_Internal_lookup_in_children_decreases self key st))
   =
   if key < self.pivot
   then
-    let* (st1, n) = betree_Node_lookup_back self.left key st st0 in
-    Return (st1, { self with left = n })
+    let* (st1, (o, n)) = betree_Node_lookup self.left key st in
+    Return (st1, (o, { self with left = n }))
   else
-    let* (st1, n) = betree_Node_lookup_back self.right key st st0 in
-    Return (st1, { self with right = n })
+    let* (st1, (o, n)) = betree_Node_lookup self.right key st in
+    Return (st1, (o, { self with right = n }))
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
     Source: 'src/betree.rs', lines 709:4-709:58 *)
 and betree_Node_lookup
   (self : betree_Node_t) (key : u64) (st : state) :
-  Tot (result (state & (option u64)))
-  (decreases (betree_Node_lookup_decreases self key st))
-  =
-  begin match self with
-  | Betree_Node_Internal node ->
-    let* (st0, msgs) = betree_load_internal_node node.id st in
-    let* pending = betree_Node_lookup_first_message_for_key key msgs in
-    begin match pending with
-    | Betree_List_Cons p l ->
-      let (k, msg) = p in
-      if k <> key
-      then
-        let* (st1, o) = betree_Internal_lookup_in_children node key st0 in
-        let* _ =
-          betree_Node_lookup_first_message_for_key_back key msgs
-            (Betree_List_Cons (k, msg) l) in
-        Return (st1, o)
-      else
-        begin match msg with
-        | Betree_Message_Insert v ->
-          let* _ =
-            betree_Node_lookup_first_message_for_key_back key msgs
-              (Betree_List_Cons (k, Betree_Message_Insert v) l) in
-          Return (st0, Some v)
-        | Betree_Message_Delete ->
-          let* _ =
-            betree_Node_lookup_first_message_for_key_back key msgs
-              (Betree_List_Cons (k, Betree_Message_Delete) l) in
-          Return (st0, None)
-        | Betree_Message_Upsert ufs ->
-          let* (st1, v) = betree_Internal_lookup_in_children node key st0 in
-          let* (st2, v0) =
-            betree_Node_apply_upserts (Betree_List_Cons (k,
-              Betree_Message_Upsert ufs) l) v key st1 in
-          let* (st3, node0) =
-            betree_Internal_lookup_in_children_back node key st0 st2 in
-          let* (st4, pending0) =
-            betree_Node_apply_upserts_back (Betree_List_Cons (k,
-              Betree_Message_Upsert ufs) l) v key st1 st3 in
-          let* msgs0 =
-            betree_Node_lookup_first_message_for_key_back key msgs pending0 in
-          let* (st5, _) = betree_store_internal_node node0.id msgs0 st4 in
-          Return (st5, Some v0)
-        end
-    | Betree_List_Nil ->
-      let* (st1, o) = betree_Internal_lookup_in_children node key st0 in
-      let* _ =
-        betree_Node_lookup_first_message_for_key_back key msgs Betree_List_Nil
-        in
-      Return (st1, o)
-    end
-  | Betree_Node_Leaf node ->
-    let* (st0, bindings) = betree_load_leaf_node node.id st in
-    let* o = betree_Node_lookup_in_bindings key bindings in
-    Return (st0, o)
-  end
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0
-    Source: 'src/betree.rs', lines 709:4-709:58 *)
-and betree_Node_lookup_back
-  (self : betree_Node_t) (key : u64) (st : state) (st0 : state) :
-  Tot (result (state & betree_Node_t))
+  Tot (result (state & ((option u64) & betree_Node_t)))
   (decreases (betree_Node_lookup_decreases self key st))
   =
   begin match self with
   | Betree_Node_Internal node ->
     let* (st1, msgs) = betree_load_internal_node node.id st in
-    let* pending = betree_Node_lookup_first_message_for_key key msgs in
+    let* (pending, lookup_first_message_for_key_back) =
+      betree_Node_lookup_first_message_for_key key msgs in
     begin match pending with
     | Betree_List_Cons p l ->
       let (k, msg) = p in
       if k <> key
       then
+        let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in
         let* _ =
-          betree_Node_lookup_first_message_for_key_back key msgs
-            (Betree_List_Cons (k, msg) l) in
-        let* (st2, node0) =
-          betree_Internal_lookup_in_children_back node key st1 st0 in
-        Return (st2, Betree_Node_Internal node0)
+          lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in
+        Return (st2, (o, Betree_Node_Internal i))
       else
         begin match msg with
         | Betree_Message_Insert v ->
           let* _ =
-            betree_Node_lookup_first_message_for_key_back key msgs
-              (Betree_List_Cons (k, Betree_Message_Insert v) l) in
-          Return (st0, Betree_Node_Internal node)
+            lookup_first_message_for_key_back (Betree_List_Cons (k,
+              Betree_Message_Insert v) l) in
+          Return (st1, (Some v, Betree_Node_Internal node))
         | Betree_Message_Delete ->
           let* _ =
-            betree_Node_lookup_first_message_for_key_back key msgs
-              (Betree_List_Cons (k, Betree_Message_Delete) l) in
-          Return (st0, Betree_Node_Internal node)
+            lookup_first_message_for_key_back (Betree_List_Cons (k,
+              Betree_Message_Delete) l) in
+          Return (st1, (None, Betree_Node_Internal node))
         | Betree_Message_Upsert ufs ->
-          let* (st2, v) = betree_Internal_lookup_in_children node key st1 in
-          let* (st3, _) =
+          let* (st2, (v, i)) = betree_Internal_lookup_in_children node key st1
+            in
+          let* (st3, (v1, l1)) =
             betree_Node_apply_upserts (Betree_List_Cons (k,
               Betree_Message_Upsert ufs) l) v key st2 in
-          let* (st4, node0) =
-            betree_Internal_lookup_in_children_back node key st1 st3 in
-          let* (st5, pending0) =
-            betree_Node_apply_upserts_back (Betree_List_Cons (k,
-              Betree_Message_Upsert ufs) l) v key st2 st4 in
-          let* msgs0 =
-            betree_Node_lookup_first_message_for_key_back key msgs pending0 in
-          let* _ = betree_store_internal_node node0.id msgs0 st5 in
-          Return (st0, Betree_Node_Internal node0)
+          let* msgs1 = lookup_first_message_for_key_back l1 in
+          let* (st4, _) = betree_store_internal_node i.id msgs1 st3 in
+          Return (st4, (Some v1, Betree_Node_Internal i))
         end
     | Betree_List_Nil ->
-      let* _ =
-        betree_Node_lookup_first_message_for_key_back key msgs Betree_List_Nil
-        in
-      let* (st2, node0) =
-        betree_Internal_lookup_in_children_back node key st1 st0 in
-      Return (st2, Betree_Node_Internal node0)
+      let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in
+      let* _ = lookup_first_message_for_key_back Betree_List_Nil in
+      Return (st2, (o, Betree_Node_Internal i))
     end
   | Betree_Node_Leaf node ->
-    let* (_, bindings) = betree_load_leaf_node node.id st in
-    let* _ = betree_Node_lookup_in_bindings key bindings in
-    Return (st0, Betree_Node_Leaf node)
+    let* (st1, bindings) = betree_load_leaf_node node.id st in
+    let* o = betree_Node_lookup_in_bindings key bindings in
+    Return (st1, (o, Betree_Node_Leaf node))
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]:
     Source: 'src/betree.rs', lines 674:4-674:77 *)
 let rec betree_Node_filter_messages_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -530,36 +334,20 @@ let rec betree_Node_filter_messages_for_key
     let (k, m) = p in
     if k = key
     then
-      let* msgs0 =
-        betree_List_pop_front_back (u64 & betree_Message_t) (Betree_List_Cons
-          (k, m) l) in
-      betree_Node_filter_messages_for_key key msgs0
+      let* (_, l1) =
+        betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m)
+          l) in
+      betree_Node_filter_messages_for_key key l1
     else Return (Betree_List_Cons (k, m) l)
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
     Source: 'src/betree.rs', lines 689:4-692:34 *)
 let rec betree_Node_lookup_first_message_after_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
-  Tot (result (betree_List_t (u64 & betree_Message_t)))
-  (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs))
-  =
-  begin match msgs with
-  | Betree_List_Cons p next_msgs ->
-    let (k, m) = p in
-    if k = key
-    then betree_Node_lookup_first_message_after_key key next_msgs
-    else Return (Betree_List_Cons (k, m) next_msgs)
-  | Betree_List_Nil -> Return Betree_List_Nil
-  end
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0
-    Source: 'src/betree.rs', lines 689:4-692:34 *)
-let rec betree_Node_lookup_first_message_after_key_back
-  (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
-  (ret : betree_List_t (u64 & betree_Message_t)) :
-  Tot (result (betree_List_t (u64 & betree_Message_t)))
+  Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
+    betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))))
   (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs))
   =
   begin match msgs with
@@ -567,75 +355,79 @@ let rec betree_Node_lookup_first_message_after_key_back
     let (k, m) = p in
     if k = key
     then
-      let* next_msgs0 =
-        betree_Node_lookup_first_message_after_key_back key next_msgs ret in
-      Return (Betree_List_Cons (k, m) next_msgs0)
-    else Return ret
-  | Betree_List_Nil -> Return ret
+      let* (l, lookup_first_message_after_key_back) =
+        betree_Node_lookup_first_message_after_key key next_msgs in
+      let back_'a =
+        fun ret ->
+          let* next_msgs1 = lookup_first_message_after_key_back ret in
+          Return (Betree_List_Cons (k, m) next_msgs1) in
+      Return (l, back_'a)
+    else
+      let back_'a = fun ret -> Return ret in
+      Return (Betree_List_Cons (k, m) next_msgs, back_'a)
+  | Betree_List_Nil ->
+    let back_'a = fun ret -> Return ret in Return (Betree_List_Nil, back_'a)
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
     Source: 'src/betree.rs', lines 521:4-521:89 *)
 let betree_Node_apply_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
   result (betree_List_t (u64 & betree_Message_t))
   =
-  let* msgs0 = betree_Node_lookup_first_message_for_key key msgs in
-  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key in
+  let* (msgs1, lookup_first_message_for_key_back) =
+    betree_Node_lookup_first_message_for_key key msgs in
+  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key in
   if b
   then
     begin match new_msg with
     | Betree_Message_Insert i ->
-      let* msgs1 = betree_Node_filter_messages_for_key key msgs0 in
-      let* msgs2 =
-        betree_List_push_front (u64 & betree_Message_t) msgs1 (key,
+      let* l = betree_Node_filter_messages_for_key key msgs1 in
+      let* l1 =
+        betree_List_push_front (u64 & betree_Message_t) l (key,
           Betree_Message_Insert i) in
-      betree_Node_lookup_first_message_for_key_back key msgs msgs2
+      lookup_first_message_for_key_back l1
     | Betree_Message_Delete ->
-      let* msgs1 = betree_Node_filter_messages_for_key key msgs0 in
-      let* msgs2 =
-        betree_List_push_front (u64 & betree_Message_t) msgs1 (key,
+      let* l = betree_Node_filter_messages_for_key key msgs1 in
+      let* l1 =
+        betree_List_push_front (u64 & betree_Message_t) l (key,
           Betree_Message_Delete) in
-      betree_Node_lookup_first_message_for_key_back key msgs msgs2
+      lookup_first_message_for_key_back l1
     | Betree_Message_Upsert s ->
-      let* p = betree_List_hd (u64 & betree_Message_t) msgs0 in
+      let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in
       let (_, m) = p in
       begin match m with
       | Betree_Message_Insert prev ->
         let* v = betree_upsert_update (Some prev) s in
-        let* msgs1 = betree_List_pop_front_back (u64 & betree_Message_t) msgs0
-          in
-        let* msgs2 =
-          betree_List_push_front (u64 & betree_Message_t) msgs1 (key,
+        let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in
+        let* l1 =
+          betree_List_push_front (u64 & betree_Message_t) l (key,
             Betree_Message_Insert v) in
-        betree_Node_lookup_first_message_for_key_back key msgs msgs2
+        lookup_first_message_for_key_back l1
       | Betree_Message_Delete ->
+        let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in
         let* v = betree_upsert_update None s in
-        let* msgs1 = betree_List_pop_front_back (u64 & betree_Message_t) msgs0
-          in
-        let* msgs2 =
-          betree_List_push_front (u64 & betree_Message_t) msgs1 (key,
+        let* l1 =
+          betree_List_push_front (u64 & betree_Message_t) l (key,
             Betree_Message_Insert v) in
-        betree_Node_lookup_first_message_for_key_back key msgs msgs2
-      | Betree_Message_Upsert ufs ->
-        let* msgs1 = betree_Node_lookup_first_message_after_key key msgs0 in
-        let* msgs2 =
-          betree_List_push_front (u64 & betree_Message_t) msgs1 (key,
+        lookup_first_message_for_key_back l1
+      | Betree_Message_Upsert _ ->
+        let* (msgs2, lookup_first_message_after_key_back) =
+          betree_Node_lookup_first_message_after_key key msgs1 in
+        let* l =
+          betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
             Betree_Message_Upsert s) in
-        let* msgs3 =
-          betree_Node_lookup_first_message_after_key_back key msgs0 msgs2 in
-        betree_Node_lookup_first_message_for_key_back key msgs msgs3
+        let* msgs3 = lookup_first_message_after_key_back l in
+        lookup_first_message_for_key_back msgs3
       end
     end
   else
-    let* msgs1 =
-      betree_List_push_front (u64 & betree_Message_t) msgs0 (key, new_msg) in
-    betree_Node_lookup_first_message_for_key_back key msgs msgs1
+    let* l =
+      betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in
+    lookup_first_message_for_key_back l
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
     Source: 'src/betree.rs', lines 502:4-505:5 *)
 let rec betree_Node_apply_messages_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t))
@@ -646,89 +438,75 @@ let rec betree_Node_apply_messages_to_internal
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
-    let* msgs0 = betree_Node_apply_to_internal msgs i m in
-    betree_Node_apply_messages_to_internal msgs0 new_msgs_tl
+    let* l = betree_Node_apply_to_internal msgs i m in
+    betree_Node_apply_messages_to_internal l new_msgs_tl
   | Betree_List_Nil -> Return msgs
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
     Source: 'src/betree.rs', lines 653:4-656:32 *)
 let rec betree_Node_lookup_mut_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
-  Tot (result (betree_List_t (u64 & u64)))
+  Tot (result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) ->
+    result (betree_List_t (u64 & u64)))))
   (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings))
   =
   begin match bindings with
   | Betree_List_Cons hd tl ->
-    let (i, i0) = hd in
+    let (i, i1) = hd in
     if i >= key
-    then Return (Betree_List_Cons (i, i0) tl)
-    else betree_Node_lookup_mut_in_bindings key tl
-  | Betree_List_Nil -> Return Betree_List_Nil
-  end
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0
-    Source: 'src/betree.rs', lines 653:4-656:32 *)
-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
-  | Betree_List_Cons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return ret
+    then
+      let back_'a = fun ret -> Return ret in
+      Return (Betree_List_Cons (i, i1) tl, back_'a)
     else
-      let* tl0 = betree_Node_lookup_mut_in_bindings_back key tl ret in
-      Return (Betree_List_Cons (i, i0) tl0)
-  | Betree_List_Nil -> Return ret
+      let* (l, lookup_mut_in_bindings_back) =
+        betree_Node_lookup_mut_in_bindings key tl in
+      let back_'a =
+        fun ret ->
+          let* tl1 = lookup_mut_in_bindings_back ret in
+          Return (Betree_List_Cons (i, i1) tl1) in
+      Return (l, back_'a)
+  | Betree_List_Nil ->
+    let back_'a = fun ret -> Return ret in Return (Betree_List_Nil, back_'a)
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
     Source: 'src/betree.rs', lines 460:4-460:87 *)
 let betree_Node_apply_to_leaf
   (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 key bindings in
-  let* b = betree_ListTupleU64T_head_has_key u64 bindings0 key in
+  let* (bindings1, lookup_mut_in_bindings_back) =
+    betree_Node_lookup_mut_in_bindings key bindings in
+  let* b = betree_ListTupleU64T_head_has_key u64 bindings1 key in
   if b
   then
-    let* hd = betree_List_pop_front (u64 & u64) bindings0 in
+    let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in
     begin match new_msg with
     | Betree_Message_Insert v ->
-      let* bindings1 = betree_List_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in
-      betree_Node_lookup_mut_in_bindings_back key bindings bindings2
-    | Betree_Message_Delete ->
-      let* bindings1 = betree_List_pop_front_back (u64 & u64) bindings0 in
-      betree_Node_lookup_mut_in_bindings_back key bindings bindings1
+      let* l1 = betree_List_push_front (u64 & u64) l (key, v) in
+      lookup_mut_in_bindings_back l1
+    | Betree_Message_Delete -> lookup_mut_in_bindings_back l
     | Betree_Message_Upsert s ->
       let (_, i) = hd in
       let* v = betree_upsert_update (Some i) s in
-      let* bindings1 = betree_List_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in
-      betree_Node_lookup_mut_in_bindings_back key bindings bindings2
+      let* l1 = betree_List_push_front (u64 & u64) l (key, v) in
+      lookup_mut_in_bindings_back l1
     end
   else
     begin match new_msg with
     | Betree_Message_Insert v ->
-      let* bindings1 = betree_List_push_front (u64 & u64) bindings0 (key, v) in
-      betree_Node_lookup_mut_in_bindings_back key bindings bindings1
-    | Betree_Message_Delete ->
-      betree_Node_lookup_mut_in_bindings_back key bindings bindings0
+      let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in
+      lookup_mut_in_bindings_back l
+    | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update None s in
-      let* bindings1 = betree_List_push_front (u64 & u64) bindings0 (key, v) in
-      betree_Node_lookup_mut_in_bindings_back key bindings bindings1
+      let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in
+      lookup_mut_in_bindings_back l
     end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
     Source: 'src/betree.rs', lines 444:4-447:5 *)
 let rec betree_Node_apply_messages_to_leaf
   (bindings : betree_List_t (u64 & u64))
@@ -739,69 +517,19 @@ let rec betree_Node_apply_messages_to_leaf
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
-    let* bindings0 = betree_Node_apply_to_leaf bindings i m in
-    betree_Node_apply_messages_to_leaf bindings0 new_msgs_tl
+    let* l = betree_Node_apply_to_leaf bindings i m in
+    betree_Node_apply_messages_to_leaf l new_msgs_tl
   | Betree_List_Nil -> Return bindings
   end
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
     Source: 'src/betree.rs', lines 410:4-415:26 *)
 let rec betree_Internal_flush
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_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_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
-    in
-  let (msgs_left, msgs_right) = p in
-  let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in
-  if len_left >= params.min_flush_size
-  then
-    let* (st0, _) =
-      betree_Node_apply_messages self.left params node_id_cnt msgs_left st in
-    let* (st1, (_, node_id_cnt0)) =
-      betree_Node_apply_messages_back'a self.left params node_id_cnt msgs_left
-        st st0 in
-    let* (st2, ()) =
-      betree_Node_apply_messages_back1 self.left params node_id_cnt msgs_left
-        st st1 in
-    let* len_right = betree_List_len (u64 & betree_Message_t) msgs_right in
-    if len_right >= params.min_flush_size
-    then
-      let* (st3, _) =
-        betree_Node_apply_messages self.right params node_id_cnt0 msgs_right
-          st2 in
-      let* (st4, (_, _)) =
-        betree_Node_apply_messages_back'a self.right params node_id_cnt0
-          msgs_right st2 st3 in
-      let* (st5, ()) =
-        betree_Node_apply_messages_back1 self.right params node_id_cnt0
-          msgs_right st2 st4 in
-      Return (st5, Betree_List_Nil)
-    else Return (st2, msgs_right)
-  else
-    let* (st0, _) =
-      betree_Node_apply_messages self.right params node_id_cnt msgs_right st in
-    let* (st1, (_, _)) =
-      betree_Node_apply_messages_back'a self.right params node_id_cnt
-        msgs_right st st0 in
-    let* (st2, ()) =
-      betree_Node_apply_messages_back1 self.right params node_id_cnt msgs_right
-        st st1 in
-    Return (st2, msgs_left)
-
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
-and betree_Internal_flush_back'a
-  (self : betree_Internal_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_t)
-  (content : betree_List_t (u64 & betree_Message_t)) (st : state) (st0 : state)
-  :
-  Tot (result (state & (betree_Internal_t & betree_NodeIdCounter_t)))
+  Tot (result (state & ((betree_List_t (u64 & betree_Message_t)) &
+    (betree_Internal_t & betree_NodeIdCounter_t))))
   (decreases (
     betree_Internal_flush_decreases self params node_id_cnt content st))
   =
@@ -812,138 +540,31 @@ and betree_Internal_flush_back'a
   let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in
   if len_left >= params.min_flush_size
   then
-    let* (st1, _) =
+    let* (st1, p1) =
       betree_Node_apply_messages self.left params node_id_cnt msgs_left st in
-    let* (st2, (n, node_id_cnt0)) =
-      betree_Node_apply_messages_back'a self.left params node_id_cnt msgs_left
-        st st1 in
-    let* (st3, ()) =
-      betree_Node_apply_messages_back1 self.left params node_id_cnt msgs_left
-        st st2 in
+    let (n, node_id_cnt1) = p1 in
     let* len_right = betree_List_len (u64 & betree_Message_t) msgs_right in
     if len_right >= params.min_flush_size
     then
-      let* (st4, _) =
-        betree_Node_apply_messages self.right params node_id_cnt0 msgs_right
-          st3 in
-      let* (st5, (n0, node_id_cnt1)) =
-        betree_Node_apply_messages_back'a self.right params node_id_cnt0
-          msgs_right st3 st4 in
-      let* _ =
-        betree_Node_apply_messages_back1 self.right params node_id_cnt0
-          msgs_right st3 st5 in
-      Return (st0, ({ self with left = n; right = n0 }, node_id_cnt1))
-    else Return (st0, ({ self with left = n }, node_id_cnt0))
+      let* (st2, p2) =
+        betree_Node_apply_messages self.right params node_id_cnt1 msgs_right
+          st1 in
+      let (n1, node_id_cnt2) = p2 in
+      Return (st2, (Betree_List_Nil, ({ self with left = n; right = n1 },
+        node_id_cnt2)))
+    else Return (st1, (msgs_right, ({ self with left = n }, node_id_cnt1)))
   else
-    let* (st1, _) =
+    let* (st1, p1) =
       betree_Node_apply_messages self.right params node_id_cnt msgs_right st in
-    let* (st2, (n, node_id_cnt0)) =
-      betree_Node_apply_messages_back'a self.right params node_id_cnt
-        msgs_right st st1 in
-    let* _ =
-      betree_Node_apply_messages_back1 self.right params node_id_cnt msgs_right
-        st st2 in
-    Return (st0, ({ self with right = n }, node_id_cnt0))
+    let (n, node_id_cnt1) = p1 in
+    Return (st1, (msgs_left, ({ self with right = n }, node_id_cnt1)))
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 1
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
-and betree_Internal_flush_back1
-  (self : betree_Internal_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_t)
-  (content : betree_List_t (u64 & betree_Message_t)) (st : state) (st0 : state)
-  :
-  Tot (result (state & unit))
-  (decreases (
-    betree_Internal_flush_decreases self params node_id_cnt content st))
-  =
-  let* p =
-    betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
-    in
-  let (msgs_left, msgs_right) = p in
-  let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in
-  if len_left >= params.min_flush_size
-  then
-    let* (st1, _) =
-      betree_Node_apply_messages self.left params node_id_cnt msgs_left st in
-    let* (st2, (_, node_id_cnt0)) =
-      betree_Node_apply_messages_back'a self.left params node_id_cnt msgs_left
-        st st1 in
-    let* (st3, ()) =
-      betree_Node_apply_messages_back1 self.left params node_id_cnt msgs_left
-        st st2 in
-    let* len_right = betree_List_len (u64 & betree_Message_t) msgs_right in
-    if len_right >= params.min_flush_size
-    then
-      let* (st4, _) =
-        betree_Node_apply_messages self.right params node_id_cnt0 msgs_right
-          st3 in
-      let* (st5, (_, _)) =
-        betree_Node_apply_messages_back'a self.right params node_id_cnt0
-          msgs_right st3 st4 in
-      let* _ =
-        betree_Node_apply_messages_back1 self.right params node_id_cnt0
-          msgs_right st3 st5 in
-      Return (st0, ())
-    else Return (st0, ())
-  else
-    let* (st1, _) =
-      betree_Node_apply_messages self.right params node_id_cnt msgs_right st in
-    let* (st2, (_, _)) =
-      betree_Node_apply_messages_back'a self.right params node_id_cnt
-        msgs_right st st1 in
-    let* _ =
-      betree_Node_apply_messages_back1 self.right params node_id_cnt msgs_right
-        st st2 in
-    Return (st0, ())
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
     Source: 'src/betree.rs', lines 588:4-593:5 *)
 and betree_Node_apply_messages
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_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
-  | Betree_Node_Internal node ->
-    let* (st0, content) = betree_load_internal_node node.id st in
-    let* content0 = betree_Node_apply_messages_to_internal content msgs in
-    let* num_msgs = betree_List_len (u64 & betree_Message_t) content0 in
-    if num_msgs >= params.min_flush_size
-    then
-      let* (st1, content1) =
-        betree_Internal_flush 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 node0.id content1 st2 in
-      Return (st3, ())
-    else
-      let* (st1, _) = betree_store_internal_node node.id content0 st0 in
-      Return (st1, ())
-  | Betree_Node_Leaf node ->
-    let* (st0, content) = betree_load_leaf_node node.id st in
-    let* content0 = betree_Node_apply_messages_to_leaf content msgs in
-    let* len = betree_List_len (u64 & u64) content0 in
-    let* i = u64_mul 2 params.split_size in
-    if len >= i
-    then
-      let* (st1, _) = betree_Leaf_split node content0 params node_id_cnt st0 in
-      let* (st2, _) = betree_store_leaf_node node.id Betree_List_Nil st1 in
-      betree_Leaf_split_back0 node content0 params node_id_cnt st0 st2
-    else
-      let* (st1, _) = betree_store_leaf_node node.id content0 st0 in
-      Return (st1, ())
-  end
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
-and betree_Node_apply_messages_back'a
-  (self : betree_Node_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_t)
-  (msgs : betree_List_t (u64 & betree_Message_t)) (st : state) (st0 : state) :
   Tot (result (state & (betree_Node_t & betree_NodeIdCounter_t)))
   (decreases (
     betree_Node_apply_messages_decreases self params node_id_cnt msgs st))
@@ -951,277 +572,111 @@ and betree_Node_apply_messages_back'a
   begin match self with
   | Betree_Node_Internal node ->
     let* (st1, content) = betree_load_internal_node node.id st in
-    let* content0 = betree_Node_apply_messages_to_internal content msgs in
-    let* num_msgs = betree_List_len (u64 & betree_Message_t) content0 in
-    if num_msgs >= params.min_flush_size
-    then
-      let* (st2, content1) =
-        betree_Internal_flush 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 node0.id content1 st3 in
-      Return (st0, (Betree_Node_Internal node0, node_id_cnt0))
-    else
-      let* _ = betree_store_internal_node node.id content0 st1 in
-      Return (st0, (Betree_Node_Internal node, node_id_cnt))
-  | Betree_Node_Leaf node ->
-    let* (st1, content) = betree_load_leaf_node node.id st in
-    let* content0 = betree_Node_apply_messages_to_leaf content msgs in
-    let* len = betree_List_len (u64 & u64) content0 in
-    let* i = u64_mul 2 params.split_size in
-    if len >= i
-    then
-      let* (st2, new_node) =
-        betree_Leaf_split node content0 params node_id_cnt st1 in
-      let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil 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, (Betree_Node_Internal new_node, node_id_cnt0))
-    else
-      let* _ = betree_store_leaf_node node.id content0 st1 in
-      Return (st0, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
-  end
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 1
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
-and betree_Node_apply_messages_back1
-  (self : betree_Node_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_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
-  | Betree_Node_Internal node ->
-    let* (st1, content) = betree_load_internal_node node.id st in
-    let* content0 = betree_Node_apply_messages_to_internal content msgs in
-    let* num_msgs = betree_List_len (u64 & betree_Message_t) content0 in
+    let* l = betree_Node_apply_messages_to_internal content msgs in
+    let* num_msgs = betree_List_len (u64 & betree_Message_t) l in
     if num_msgs >= params.min_flush_size
     then
-      let* (st2, content1) =
-        betree_Internal_flush 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 node0.id content1 st3 in
-      betree_Internal_flush_back1 node params node_id_cnt content0 st1 st0
+      let* (st2, (content1, p)) =
+        betree_Internal_flush node params node_id_cnt l st1 in
+      let (node1, node_id_cnt1) = p in
+      let* (st3, _) = betree_store_internal_node node1.id content1 st2 in
+      Return (st3, (Betree_Node_Internal node1, node_id_cnt1))
     else
-      let* _ = betree_store_internal_node node.id content0 st1 in
-      Return (st0, ())
+      let* (st2, _) = betree_store_internal_node node.id l st1 in
+      Return (st2, (Betree_Node_Internal node, node_id_cnt))
   | Betree_Node_Leaf node ->
     let* (st1, content) = betree_load_leaf_node node.id st in
-    let* content0 = betree_Node_apply_messages_to_leaf content msgs in
-    let* len = betree_List_len (u64 & u64) content0 in
+    let* l = betree_Node_apply_messages_to_leaf content msgs in
+    let* len = betree_List_len (u64 & u64) l in
     let* i = u64_mul 2 params.split_size in
     if len >= i
     then
-      let* (st2, _) = betree_Leaf_split node content0 params node_id_cnt st1 in
+      let* (st2, (new_node, nic)) =
+        betree_Leaf_split node l params node_id_cnt st1 in
       let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil 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
+      Return (st3, (Betree_Node_Internal new_node, nic))
     else
-      let* _ = betree_store_leaf_node node.id content0 st1 in Return (st0, ())
+      let* (st2, _) = betree_store_leaf_node node.id l st1 in
+      Return (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]:
     Source: 'src/betree.rs', lines 576:4-582:5 *)
 let betree_Node_apply
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
   (new_msg : betree_Message_t) (st : state) :
-  result (state & unit)
-  =
-  let l = Betree_List_Nil in
-  let* (st0, _) =
-    betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key,
-      new_msg) l) st in
-  let* (st1, (_, _)) =
-    betree_Node_apply_messages_back'a self params node_id_cnt (Betree_List_Cons
-      (key, new_msg) l) st st0 in
-  betree_Node_apply_messages_back1 self params node_id_cnt (Betree_List_Cons
-    (key, new_msg) l) st st1
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
-    Source: 'src/betree.rs', lines 576:4-582:5 *)
-let betree_Node_apply_back'a
-  (self : betree_Node_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
-  (new_msg : betree_Message_t) (st : state) (st0 : state) :
   result (state & (betree_Node_t & betree_NodeIdCounter_t))
   =
   let l = Betree_List_Nil in
-  let* (st1, _) =
+  let* (st1, p) =
     betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key,
       new_msg) l) st in
-  let* (st2, (self0, node_id_cnt0)) =
-    betree_Node_apply_messages_back'a self params node_id_cnt (Betree_List_Cons
-      (key, new_msg) l) st st1 in
-  let* _ =
-    betree_Node_apply_messages_back1 self params node_id_cnt (Betree_List_Cons
-      (key, new_msg) l) st st2 in
-  Return (st0, (self0, node_id_cnt0))
+  let (self1, node_id_cnt1) = p in
+  Return (st1, (self1, node_id_cnt1))
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 1
-    Source: 'src/betree.rs', lines 576:4-582:5 *)
-let betree_Node_apply_back1
-  (self : betree_Node_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
-  (new_msg : betree_Message_t) (st : state) (st0 : state) :
-  result (state & unit)
-  =
-  let l = Betree_List_Nil in
-  let* (st1, _) =
-    betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key,
-      new_msg) l) st in
-  let* (st2, (_, _)) =
-    betree_Node_apply_messages_back'a self params node_id_cnt (Betree_List_Cons
-      (key, new_msg) l) st st1 in
-  let* _ =
-    betree_Node_apply_messages_back1 self params node_id_cnt (Betree_List_Cons
-      (key, new_msg) l) st st2 in
-  Return (st0, ())
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
     Source: 'src/betree.rs', lines 849:4-849:60 *)
 let betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state & betree_BeTree_t)
   =
   let* node_id_cnt = betree_NodeIdCounter_new in
-  let* id = betree_NodeIdCounter_fresh_id node_id_cnt in
-  let* (st0, _) = betree_store_leaf_node id Betree_List_Nil st in
-  let* node_id_cnt0 = betree_NodeIdCounter_fresh_id_back node_id_cnt in
-  Return (st0,
+  let* (id, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in
+  let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in
+  Return (st1,
     {
       params = { min_flush_size = min_flush_size; split_size = split_size };
-      node_id_cnt = node_id_cnt0;
+      node_id_cnt = nic;
       root = (Betree_Node_Leaf { id = id; size = 0 })
     })
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]:
     Source: 'src/betree.rs', lines 868:4-868:47 *)
 let betree_BeTree_apply
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
-  result (state & unit)
-  =
-  let* (st0, _) =
-    betree_Node_apply self.root self.params self.node_id_cnt key msg st in
-  let* (st1, (_, _)) =
-    betree_Node_apply_back'a self.root self.params self.node_id_cnt key msg st
-      st0 in
-  betree_Node_apply_back1 self.root self.params self.node_id_cnt key msg st st1
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0
-    Source: 'src/betree.rs', lines 868:4-868:47 *)
-let betree_BeTree_apply_back
-  (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state)
-  (st0 : state) :
   result (state & betree_BeTree_t)
   =
-  let* (st1, _) =
+  let* (st1, p) =
     betree_Node_apply self.root self.params self.node_id_cnt key msg st in
-  let* (st2, (n, nic)) =
-    betree_Node_apply_back'a self.root self.params self.node_id_cnt key msg st
-      st1 in
-  let* _ =
-    betree_Node_apply_back1 self.root self.params self.node_id_cnt key msg st
-      st2 in
-  Return (st0, { self with node_id_cnt = nic; root = n })
+  let (n, nic) = p in
+  Return (st1, { self with node_id_cnt = nic; root = n })
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
     Source: 'src/betree.rs', lines 874:4-874:52 *)
 let betree_BeTree_insert
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
-  result (state & unit)
-  =
-  let* (st0, _) = betree_BeTree_apply self key (Betree_Message_Insert value) st
-    in
-  let* (st1, _) =
-    betree_BeTree_apply_back self key (Betree_Message_Insert value) st st0 in
-  Return (st1, ())
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0
-    Source: 'src/betree.rs', lines 874:4-874:52 *)
-let betree_BeTree_insert_back
-  (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) (st0 : state)
-  :
   result (state & betree_BeTree_t)
   =
-  let* (st1, _) = betree_BeTree_apply self key (Betree_Message_Insert value) st
-    in
-  let* (_, self0) =
-    betree_BeTree_apply_back self key (Betree_Message_Insert value) st st1 in
-  Return (st0, self0)
+  betree_BeTree_apply self key (Betree_Message_Insert value) st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]:
     Source: 'src/betree.rs', lines 880:4-880:38 *)
 let betree_BeTree_delete
-  (self : betree_BeTree_t) (key : u64) (st : state) : result (state & unit) =
-  let* (st0, _) = betree_BeTree_apply self key Betree_Message_Delete st in
-  let* (st1, _) =
-    betree_BeTree_apply_back self key Betree_Message_Delete st st0 in
-  Return (st1, ())
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0
-    Source: 'src/betree.rs', lines 880:4-880:38 *)
-let betree_BeTree_delete_back
-  (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) :
+  (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & betree_BeTree_t)
   =
-  let* (st1, _) = betree_BeTree_apply self key Betree_Message_Delete st in
-  let* (_, self0) =
-    betree_BeTree_apply_back self key Betree_Message_Delete st st1 in
-  Return (st0, self0)
+  betree_BeTree_apply self key Betree_Message_Delete st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]:
     Source: 'src/betree.rs', lines 886:4-886:59 *)
 let betree_BeTree_upsert
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
-  result (state & unit)
-  =
-  let* (st0, _) = betree_BeTree_apply self key (Betree_Message_Upsert upd) st
-    in
-  let* (st1, _) =
-    betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st st0 in
-  Return (st1, ())
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0
-    Source: 'src/betree.rs', lines 886:4-886:59 *)
-let betree_BeTree_upsert_back
-  (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
-  (st : state) (st0 : state) :
   result (state & betree_BeTree_t)
   =
-  let* (st1, _) = betree_BeTree_apply self key (Betree_Message_Upsert upd) st
-    in
-  let* (_, self0) =
-    betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st st1 in
-  Return (st0, self0)
+  betree_BeTree_apply self key (Betree_Message_Upsert upd) st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]:
     Source: 'src/betree.rs', lines 895:4-895:62 *)
 let betree_BeTree_lookup
   (self : betree_BeTree_t) (key : u64) (st : state) :
-  result (state & (option u64))
-  =
-  betree_Node_lookup self.root key st
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0
-    Source: 'src/betree.rs', lines 895:4-895:62 *)
-let betree_BeTree_lookup_back
-  (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) :
-  result (state & betree_BeTree_t)
+  result (state & ((option u64) & betree_BeTree_t))
   =
-  let* (st1, n) = betree_Node_lookup_back self.root key st st0 in
-  Return (st1, { self with root = n })
+  let* (st1, (o, n)) = betree_Node_lookup self.root key st in
+  Return (st1, (o, { self with root = n }))
 
-(** [betree_main::main]: forward function
+(** [betree_main::main]:
     Source: 'src/betree_main.rs', lines 5:0-5:9 *)
 let main : result unit =
   Return ()
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
index cd2f956f..de9b96fd 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -6,29 +6,29 @@ include BetreeMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree_utils::load_internal_node]: forward function
+(** [betree_main::betree_utils::load_internal_node]:
     Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
 val betree_utils_load_internal_node
   : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
 
-(** [betree_main::betree_utils::store_internal_node]: forward function
+(** [betree_main::betree_utils::store_internal_node]:
     Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
 val betree_utils_store_internal_node
   :
   u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
     unit)
 
-(** [betree_main::betree_utils::load_leaf_node]: forward function
+(** [betree_main::betree_utils::load_leaf_node]:
     Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
 val betree_utils_load_leaf_node
   : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
 
-(** [betree_main::betree_utils::store_leaf_node]: forward function
+(** [betree_main::betree_utils::store_leaf_node]:
     Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
 val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+(** [core::option::{core::option::Option<T>}::unwrap]:
     Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index a3ffbde4..fca80829 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -55,8 +55,7 @@ type string = string
 let is_zero (n: nat) : bool = n = 0
 let decrease (n: nat{n > 0}) : nat = n - 1
 
-let core_mem_replace (a : Type0) (x : a) (y : a) : a = x
-let core_mem_replace_back (a : Type0) (x : a) (y : a) : a = y
+let core_mem_replace (a : Type0) (x : a) (y : a) : a & a = (x, x)
 
 // We don't really use raw pointers for now
 type mut_raw_ptr (t : Type0) = { v : t }
@@ -477,8 +476,7 @@ noeq type core_ops_index_Index (self idx : Type0) = {
 // Trait declaration: [core::ops::index::IndexMut]
 noeq type core_ops_index_IndexMut (self idx : Type0) = {
   indexInst : core_ops_index_Index self idx;
-  index_mut : self → idx → result indexInst.output;
-  index_mut_back : self → idx → indexInst.output → result self;
+  index_mut : self → idx → result (indexInst.output & (indexInst.output → result self));
 }
 
 // Trait declaration [core::ops::deref::Deref]
@@ -490,8 +488,7 @@ noeq type core_ops_deref_Deref (self : Type0) = {
 // Trait declaration [core::ops::deref::DerefMut]
 noeq type core_ops_deref_DerefMut (self : Type0) = {
   derefInst : core_ops_deref_Deref self;
-  deref_mut : self → result derefInst.target;
-  deref_mut_back : self → derefInst.target → result self;
+  deref_mut : self → result (derefInst.target & (derefInst.target → result self));
 }
 
 type core_ops_range_Range (a : Type0) = {
@@ -502,8 +499,8 @@ type core_ops_range_Range (a : Type0) = {
 (*** [alloc] *)
 
 let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
-let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x
-let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x
+let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result (t & (t -> result t)) =
+  Return (x, (fun x -> Return x))
 
 // Trait instance
 let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
@@ -515,7 +512,6 @@ let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self
 let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = {
   derefInst = alloc_boxed_Box_coreopsDerefInst self;
   deref_mut = alloc_boxed_Box_deref_mut self;
-  deref_mut_back = alloc_boxed_Box_deref_mut_back self;
 }
 
 (*** Array *)
@@ -535,10 +531,18 @@ let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : resu
   if i < length x then Return (index x i)
   else Fail Failure
 
-let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
+let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) :
+  result (array a n) =
   if i < length x then Return (list_update x i nx)
   else Fail Failure
 
+let array_index_mut_usize (a : Type0) (n : usize) (x : array a n) (i : usize) :
+  result (a & (a -> result (array a n))) =
+  match array_index_usize a n x i with
+  | Fail e -> Fail e
+  | Return v ->
+    Return (v, array_update_usize a n x i)
+
 (*** Slice *)
 type slice (a : Type0) = s:list a{length s <= usize_max}
 
@@ -552,6 +556,13 @@ let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (
   if i < length x then Return (list_update x i nx)
   else Fail Failure
 
+let slice_index_mut_usize (a : Type0) (s : slice a) (i : usize) :
+  result (a & (a -> result (slice a))) =
+  match slice_index_usize a s i with
+  | Fail e -> Fail e
+  | Return x ->
+    Return (x, slice_update_usize a s i)
+
 (*** Subslices *)
 
 let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
@@ -559,6 +570,10 @@ let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : res
   if length s = n then Return s
   else Fail Failure
 
+let array_to_slice_mut (a : Type0) (n : usize) (x : array a n) :
+  result (slice a & (slice a -> result (array a n))) =
+  Return (x, array_from_slice a n x)
+
 // TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
 let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
   admit()
@@ -588,8 +603,13 @@ let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : r
 let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Return (list_update v i x) else Fail Failure
 
-// The **forward** function shouldn't be used
-let alloc_vec_Vec_push_fwd (a  : Type0) (v : alloc_vec_Vec a) (x : a) : unit = ()
+let alloc_vec_Vec_index_mut_usize (#a : Type0) (v: alloc_vec_Vec a) (i: usize) :
+  result (a & (a → result (alloc_vec_Vec a))) =
+  match alloc_vec_Vec_index_usize v i with
+  | Return x ->
+    Return (x, alloc_vec_Vec_update_usize v i)
+  | Fail e -> Fail e
+
 let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
   Pure (result (alloc_vec_Vec a))
   (requires True)
@@ -605,9 +625,6 @@ let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
     end
   else Fail Failure
 
-// The **forward** function shouldn't be used
-let alloc_vec_Vec_insert_fwd (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail Failure
 let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Return (list_update v i x) else Fail Failure
 
@@ -619,13 +636,11 @@ noeq type core_slice_index_SliceIndex (self t : Type0) = {
   sealedInst : core_slice_index_private_slice_index_Sealed self;
   output : Type0;
   get : self → t → result (option output);
-  get_mut : self → t → result (option output);
-  get_mut_back : self → t → option output → result t;
+  get_mut : self → t → result (option output & (option output -> result t));
   get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
   get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output);
   index : self → t → result output;
-  index_mut : self → t → result output;
-  index_mut_back : self → t → output → result t;
+  index_mut : self → t → result (output & (output -> result t));
 }
 
 // [core::slice::index::[T]::index]: forward function
@@ -643,14 +658,8 @@ let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize)
   admit () // TODO
 
 // [core::slice::index::Range::get_mut]: forward function
-let core_slice_index_RangeUsize_get_mut
-  (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) =
-  admit () // TODO
-
-// [core::slice::index::Range::get_mut]: backward function 0
-let core_slice_index_RangeUsize_get_mut_back
-  (t : Type0) :
-  core_ops_range_Range usize → slice t → option (slice t) → result (slice t) =
+let core_slice_index_RangeUsize_get_mut (t : Type0) :
+  core_ops_range_Range usize → slice t → result (option (slice t) & (option (slice t) -> result (slice t))) =
   admit () // TODO
 
 // [core::slice::index::Range::get_unchecked]: forward function
@@ -675,27 +684,16 @@ let core_slice_index_RangeUsize_index
   admit () // TODO
 
 // [core::slice::index::Range::index_mut]: forward function
-let core_slice_index_RangeUsize_index_mut
-  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
-  admit () // TODO
-
-// [core::slice::index::Range::index_mut]: backward function 0
-let core_slice_index_RangeUsize_index_mut_back
-  (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) =
+let core_slice_index_RangeUsize_index_mut (t : Type0) :
+  core_ops_range_Range usize → slice t → result (slice t & (slice t -> result (slice t))) =
   admit () // TODO
 
 // [core::slice::index::[T]::index_mut]: forward function
 let core_slice_index_Slice_index_mut
   (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
-  slice t → idx → result inst.output =
+  slice t → idx → result (inst.output & (inst.output -> result (slice t))) =
   admit () // 
 
-// [core::slice::index::[T]::index_mut]: backward function 0
-let core_slice_index_Slice_index_mut_back
-  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
-  slice t → idx → inst.output → result (slice t) =
-  admit () // TODO
-
 // [core::array::[T; N]::index]: forward function
 let core_array_Array_index
   (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx)
@@ -705,13 +703,8 @@ let core_array_Array_index
 // [core::array::[T; N]::index_mut]: forward function
 let core_array_Array_index_mut
   (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
-  (a : array t n) (i : idx) : result inst.indexInst.output =
-  admit () // TODO
-
-// [core::array::[T; N]::index_mut]: backward function 0
-let core_array_Array_index_mut_back
-  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
-  (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) =
+  (a : array t n) (i : idx) :
+  result (inst.indexInst.output & (inst.indexInst.output -> result (array t n))) =
   admit () // TODO
 
 // Trait implementation: [core::slice::index::private_slice_index::Range]
@@ -725,12 +718,10 @@ let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) :
   output = slice t;
   get = core_slice_index_RangeUsize_get t;
   get_mut = core_slice_index_RangeUsize_get_mut t;
-  get_mut_back = core_slice_index_RangeUsize_get_mut_back t;
   get_unchecked = core_slice_index_RangeUsize_get_unchecked t;
   get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t;
   index = core_slice_index_RangeUsize_index t;
   index_mut = core_slice_index_RangeUsize_index_mut t;
-  index_mut_back = core_slice_index_RangeUsize_index_mut_back t;
 }
 
 // Trait implementation: [core::slice::index::[T]]
@@ -747,7 +738,6 @@ let core_ops_index_IndexMutSliceTIInst (t idx : Type0)
   core_ops_index_IndexMut (slice t) idx = {
   indexInst = core_ops_index_IndexSliceTIInst t idx inst;
   index_mut = core_slice_index_Slice_index_mut t idx inst;
-  index_mut_back = core_slice_index_Slice_index_mut_back t idx inst;
 }
 
 // Trait implementation: [core::array::[T; N]]
@@ -764,7 +754,6 @@ let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize)
   core_ops_index_IndexMut (array t n) idx = {
   indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst;
   index_mut = core_array_Array_index_mut t idx n inst;
-  index_mut_back = core_array_Array_index_mut_back t idx n inst;
 }
 
 // [core::slice::index::usize::get]: forward function
@@ -773,13 +762,8 @@ let core_slice_index_usize_get
   admit () // TODO
 
 // [core::slice::index::usize::get_mut]: forward function
-let core_slice_index_usize_get_mut
-  (t : Type0) : usize → slice t → result (option t) =
-  admit () // TODO
-
-// [core::slice::index::usize::get_mut]: backward function 0
-let core_slice_index_usize_get_mut_back
-  (t : Type0) : usize → slice t → option t → result (slice t) =
+let core_slice_index_usize_get_mut (t : Type0) :
+  usize → slice t → result (option t & (option t -> result (slice t))) =
   admit () // TODO
 
 // [core::slice::index::usize::get_unchecked]: forward function
@@ -797,12 +781,8 @@ let core_slice_index_usize_index (t : Type0) : usize → slice t → result t =
   admit () // TODO
 
 // [core::slice::index::usize::index_mut]: forward function
-let core_slice_index_usize_index_mut (t : Type0) : usize → slice t → result t =
-  admit () // TODO
-
-// [core::slice::index::usize::index_mut]: backward function 0
-let core_slice_index_usize_index_mut_back
-  (t : Type0) : usize → slice t → t → result (slice t) =
+let core_slice_index_usize_index_mut (t : Type0) :
+  usize → slice t → result (t & (t -> result (slice t))) =
   admit () // TODO
 
 // Trait implementation: [core::slice::index::private_slice_index::usize]
@@ -816,12 +796,10 @@ let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
   output = t;
   get = core_slice_index_usize_get t;
   get_mut = core_slice_index_usize_get_mut t;
-  get_mut_back = core_slice_index_usize_get_mut_back t;
   get_unchecked = core_slice_index_usize_get_unchecked t;
   get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t;
   index = core_slice_index_usize_index t;
   index_mut = core_slice_index_usize_index_mut t;
-  index_mut_back = core_slice_index_usize_index_mut_back t;
 }
 
 // [alloc::vec::Vec::index]: forward function
@@ -831,13 +809,8 @@ let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx
 
 // [alloc::vec::Vec::index_mut]: forward function
 let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
-  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
-  admit () // TODO
-
-// [alloc::vec::Vec::index_mut]: backward function 0
-let alloc_vec_Vec_index_mut_back
-  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
-  (self : alloc_vec_Vec t) (i : idx) (x : inst.output) : result (alloc_vec_Vec t) =
+  (self : alloc_vec_Vec t) (i : idx) :
+  result (inst.output & (inst.output -> result (alloc_vec_Vec t))) =
   admit () // TODO
 
 // Trait implementation: [alloc::vec::Vec]
@@ -854,7 +827,6 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
   core_ops_index_IndexMut (alloc_vec_Vec t) idx = {
   indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst;
   index_mut = alloc_vec_Vec_index_mut t idx inst;
-  index_mut_back = alloc_vec_Vec_index_mut_back t idx inst;
 }
 
 (*** Theorems *)
@@ -870,15 +842,7 @@ let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
 let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
   Lemma (
     alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
-      alloc_vec_Vec_index_usize v i)
+      alloc_vec_Vec_index_mut_usize v i)
   [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
   =
   admit()
-
-let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
-  Lemma (
-    alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x ==
-      alloc_vec_Vec_update_usize v i x)
-  [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)]
-  =
-  admit()