Do not unfold the monadic lets for the generated F* code

2 files changed, 640 insertions, 1342 deletions

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 2a336271..201778df 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -20,10 +20,8 @@ let betree_store_internal_node_fwd
   (id : u64) (content : betree_list_t (u64 & betree_message_t)) (st : state) :
   result (state & unit)
   =
-  begin match betree_utils_store_internal_node_fwd id content st with
-  | Fail e -> Fail e
-  | Return (st0, _) -> Return (st0, ())
-  end
+  let* (st0, _) = betree_utils_store_internal_node_fwd id content st in
+  Return (st0, ())
 
 (** [betree_main::betree::load_leaf_node] *)
 let betree_load_leaf_node_fwd
@@ -35,17 +33,12 @@ let betree_store_leaf_node_fwd
   (id : u64) (content : betree_list_t (u64 & u64)) (st : state) :
   result (state & unit)
   =
-  begin match betree_utils_store_leaf_node_fwd id content st with
-  | Fail e -> Fail e
-  | Return (st0, _) -> Return (st0, ())
-  end
+  let* (st0, _) = betree_utils_store_leaf_node_fwd id content st in
+  Return (st0, ())
 
 (** [betree_main::betree::fresh_node_id] *)
 let betree_fresh_node_id_fwd (counter : u64) : result u64 =
-  begin match u64_add counter 1 with
-  | Fail e -> Fail e
-  | Return _ -> Return counter
-  end
+  let* _ = u64_add counter 1 in Return counter
 
 (** [betree_main::betree::fresh_node_id] *)
 let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1
@@ -57,18 +50,14 @@ let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 let betree_node_id_counter_fresh_id_fwd
   (self : betree_node_id_counter_t) : result u64 =
-  begin match u64_add self.betree_node_id_counter_next_node_id 1 with
-  | Fail e -> Fail e
-  | Return _ -> Return self.betree_node_id_counter_next_node_id
-  end
+  let* _ = u64_add self.betree_node_id_counter_next_node_id 1 in
+  Return self.betree_node_id_counter_next_node_id
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 let betree_node_id_counter_fresh_id_back
   (self : betree_node_id_counter_t) : result betree_node_id_counter_t =
-  begin match u64_add self.betree_node_id_counter_next_node_id 1 with
-  | Fail e -> Fail e
-  | Return i -> Return (Mkbetree_node_id_counter_t i)
-  end
+  let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
+  Return (Mkbetree_node_id_counter_t i)
 
 (** [core::num::u64::{10}::MAX] *)
 let core_num_u64_max_body : result u64 = Return 18446744073709551615
@@ -86,11 +75,8 @@ let betree_upsert_update_fwd
   | Some prev0 ->
     begin match st with
     | BetreeUpsertFunStateAdd v ->
-      begin match u64_sub core_num_u64_max_c prev0 with
-      | Fail e -> Fail e
-      | Return margin ->
-        if margin >= v then u64_add prev0 v else Return core_num_u64_max_c
-      end
+      let* margin = u64_sub core_num_u64_max_c prev0 in
+      if margin >= v then u64_add prev0 v else Return core_num_u64_max_c
     | BetreeUpsertFunStateSub v ->
       if prev0 >= v then u64_sub prev0 v else Return 0
     end
@@ -102,11 +88,7 @@ let rec betree_list_len_fwd
   Tot (result u64) (decreases (betree_list_len_decreases t self))
   =
   begin match self with
-  | BetreeListCons x tl ->
-    begin match betree_list_len_fwd t tl with
-    | Fail e -> Fail e
-    | Return i -> u64_add 1 i
-    end
+  | BetreeListCons x tl -> let* i = betree_list_len_fwd t tl in u64_add 1 i
   | BetreeListNil -> Return 0
   end
 
@@ -121,17 +103,11 @@ let rec betree_list_split_at_fwd
   else
     begin match self with
     | BetreeListCons hd tl ->
-      begin match u64_sub n 1 with
-      | Fail e -> Fail e
-      | Return i ->
-        begin match betree_list_split_at_fwd t tl i with
-        | Fail e -> Fail e
-        | Return p ->
-          let (ls0, ls1) = p in
-          let l = ls0 in
-          Return (BetreeListCons hd l, ls1)
-        end
-      end
+      let* i = u64_sub n 1 in
+      let* p = betree_list_split_at_fwd t tl i in
+      let (ls0, ls1) = p in
+      let l = ls0 in
+      Return (BetreeListCons hd l, ls1)
     | BetreeListNil -> Fail Failure
     end
 
@@ -185,14 +161,11 @@ let rec betree_list_partition_at_pivot_fwd
     let (i, x) = hd in
     if i >= pivot
     then Return (BetreeListNil, BetreeListCons (i, x) tl)
-    else
-      begin match betree_list_partition_at_pivot_fwd t tl pivot with
-      | Fail e -> Fail e
-      | Return p ->
-        let (ls0, ls1) = p in
-        let l = ls0 in
-        Return (BetreeListCons (i, x) l, ls1)
-      end
+    else begin
+      let* p = betree_list_partition_at_pivot_fwd t tl pivot in
+      let (ls0, ls1) = p in
+      let l = ls0 in
+      Return (BetreeListCons (i, x) l, ls1) end
   | BetreeListNil -> Return (BetreeListNil, BetreeListNil)
   end
 
@@ -203,44 +176,22 @@ let betree_leaf_split_fwd
   (st : state) :
   result (state & betree_internal_t)
   =
-  begin match
+  let* p =
     betree_list_split_at_fwd (u64 & u64) content
-      params.betree_params_split_size with
-  | Fail e -> Fail e
-  | Return p ->
-    let (content0, content1) = p in
-    begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail e -> Fail e
-    | Return p0 ->
-      let (pivot, _) = p0 in
-      begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail e -> Fail e
-      | Return id0 ->
-        begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail e -> Fail e
-        | Return node_id_cnt0 ->
-          begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail e -> Fail e
-          | Return id1 ->
-            begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail e -> Fail e
-            | Return (st0, _) ->
-              begin match betree_store_leaf_node_fwd id1 content1 st0 with
-              | Fail e -> Fail e
-              | Return (st1, _) ->
-                let n = BetreeNodeLeaf (Mkbetree_leaf_t id0
-                  params.betree_params_split_size) in
-                let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1
-                  params.betree_params_split_size) in
-                Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n
-                  n0)
-              end
-            end
-          end
-        end
-      end
-    end
-  end
+      params.betree_params_split_size in
+  let (content0, content1) = p in
+  let* p0 = betree_list_hd_fwd (u64 & u64) content1 in
+  let (pivot, _) = p0 in
+  let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in
+  let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
+  let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in
+  let* (st0, _) = betree_store_leaf_node_fwd id0 content0 st in
+  let* (st1, _) = betree_store_leaf_node_fwd id1 content1 st0 in
+  let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size)
+    in
+  let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 params.betree_params_split_size)
+    in
+  Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n n0)
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 let betree_leaf_split_back0
@@ -249,37 +200,17 @@ let betree_leaf_split_back0
   (st : state) (st0 : state) :
   result (state & unit)
   =
-  begin match
+  let* p =
     betree_list_split_at_fwd (u64 & u64) content
-      params.betree_params_split_size with
-  | Fail e -> Fail e
-  | Return p ->
-    let (content0, content1) = p in
-    begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail e -> Fail e
-    | Return _ ->
-      begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail e -> Fail e
-      | Return id0 ->
-        begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail e -> Fail e
-        | Return node_id_cnt0 ->
-          begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail e -> Fail e
-          | Return id1 ->
-            begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail e -> Fail e
-            | Return (st1, _) ->
-              begin match betree_store_leaf_node_fwd id1 content1 st1 with
-              | Fail e -> Fail e
-              | Return _ -> Return (st0, ())
-              end
-            end
-          end
-        end
-      end
-    end
-  end
+      params.betree_params_split_size in
+  let (content0, content1) = p in
+  let* _ = betree_list_hd_fwd (u64 & u64) content1 in
+  let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in
+  let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
+  let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in
+  let* (st1, _) = betree_store_leaf_node_fwd id0 content0 st in
+  let* _ = betree_store_leaf_node_fwd id1 content1 st1 in
+  Return (st0, ())
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 let betree_leaf_split_back1
@@ -288,37 +219,17 @@ let betree_leaf_split_back1
   (st : state) (st0 : state) :
   result (state & unit)
   =
-  begin match
+  let* p =
     betree_list_split_at_fwd (u64 & u64) content
-      params.betree_params_split_size with
-  | Fail e -> Fail e
-  | Return p ->
-    let (content0, content1) = p in
-    begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail e -> Fail e
-    | Return _ ->
-      begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail e -> Fail e
-      | Return id0 ->
-        begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail e -> Fail e
-        | Return node_id_cnt0 ->
-          begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail e -> Fail e
-          | Return id1 ->
-            begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail e -> Fail e
-            | Return (st1, _) ->
-              begin match betree_store_leaf_node_fwd id1 content1 st1 with
-              | Fail e -> Fail e
-              | Return _ -> Return (st0, ())
-              end
-            end
-          end
-        end
-      end
-    end
-  end
+      params.betree_params_split_size in
+  let (content0, content1) = p in
+  let* _ = betree_list_hd_fwd (u64 & u64) content1 in
+  let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in
+  let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
+  let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in
+  let* (st1, _) = betree_store_leaf_node_fwd id0 content0 st in
+  let* _ = betree_store_leaf_node_fwd id1 content1 st1 in
+  Return (st0, ())
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 let betree_leaf_split_back2
@@ -327,42 +238,18 @@ let betree_leaf_split_back2
   (st : state) (st0 : state) :
   result (state & betree_node_id_counter_t)
   =
-  begin match
+  let* p =
     betree_list_split_at_fwd (u64 & u64) content
-      params.betree_params_split_size with
-  | Fail e -> Fail e
-  | Return p ->
-    let (content0, content1) = p in
-    begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail e -> Fail e
-    | Return _ ->
-      begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail e -> Fail e
-      | Return id0 ->
-        begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail e -> Fail e
-        | Return node_id_cnt0 ->
-          begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail e -> Fail e
-          | Return id1 ->
-            begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail e -> Fail e
-            | Return (st1, _) ->
-              begin match betree_store_leaf_node_fwd id1 content1 st1 with
-              | Fail e -> Fail e
-              | Return _ ->
-                begin match betree_node_id_counter_fresh_id_back node_id_cnt0
-                  with
-                | Fail e -> Fail e
-                | Return node_id_cnt1 -> Return (st0, node_id_cnt1)
-                end
-              end
-            end
-          end
-        end
-      end
-    end
-  end
+      params.betree_params_split_size in
+  let (content0, content1) = p in
+  let* _ = betree_list_hd_fwd (u64 & u64) content1 in
+  let* id0 = betree_node_id_counter_fresh_id_fwd node_id_cnt in
+  let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
+  let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in
+  let* (st1, _) = betree_store_leaf_node_fwd id0 content0 st in
+  let* _ = betree_store_leaf_node_fwd id1 content1 st1 in
+  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] *)
 let rec betree_node_lookup_in_bindings_fwd
@@ -409,12 +296,10 @@ let rec betree_node_lookup_first_message_for_key_back
     let (i, m) = x in
     if i >= key
     then Return ret
-    else
-      begin match
-        betree_node_lookup_first_message_for_key_back key next_msgs ret with
-      | Fail e -> Fail e
-      | Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0)
-      end
+    else begin
+      let* next_msgs0 =
+        betree_node_lookup_first_message_for_key_back key next_msgs ret in
+      Return (BetreeListCons (i, m) next_msgs0) end
   | BetreeListNil -> Return ret
   end
 
@@ -425,43 +310,25 @@ let rec betree_node_apply_upserts_fwd
   Tot (result (state & u64))
   (decreases (betree_node_apply_upserts_decreases msgs prev key st))
   =
-  begin match betree_list_head_has_key_fwd betree_message_t msgs key with
-  | Fail e -> Fail e
-  | Return b ->
-    if b
-    then
-      begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
-      | Fail e -> Fail e
-      | Return msg ->
-        let (_, m) = msg in
-        begin match m with
-        | BetreeMessageInsert i -> Fail Failure
-        | BetreeMessageDelete -> Fail Failure
-        | BetreeMessageUpsert s ->
-          begin match betree_upsert_update_fwd prev s with
-          | Fail e -> Fail e
-          | Return v ->
-            begin match
-              betree_list_pop_front_back (u64 & betree_message_t) msgs with
-            | Fail e -> Fail e
-            | Return msgs0 ->
-              betree_node_apply_upserts_fwd msgs0 (Some v) key st
-            end
-          end
-        end
-      end
-    else
-      begin match core_option_option_unwrap_fwd u64 prev st with
-      | Fail e -> Fail e
-      | Return (st0, v) ->
-        begin match
-          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
-            BetreeMessageInsert v) with
-        | Fail e -> Fail e
-        | Return _ -> Return (st0, v)
-        end
-      end
-  end
+  let* b = betree_list_head_has_key_fwd betree_message_t msgs key in
+  if b
+  then begin
+    let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in
+    let (_, m) = msg in
+    begin match m with
+    | BetreeMessageInsert i -> Fail Failure
+    | BetreeMessageDelete -> Fail Failure
+    | BetreeMessageUpsert s ->
+      let* v = betree_upsert_update_fwd prev s in
+      let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in
+      betree_node_apply_upserts_fwd msgs0 (Some v) key st
+    end end
+  else begin
+    let* (st0, v) = core_option_option_unwrap_fwd u64 prev st in
+    let* _ =
+      betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
+        BetreeMessageInsert v) in
+    Return (st0, v) end
 
 (** [betree_main::betree::Node::{5}::apply_upserts] *)
 let rec betree_node_apply_upserts_back
@@ -470,43 +337,25 @@ let rec betree_node_apply_upserts_back
   Tot (result (state & (betree_list_t (u64 & betree_message_t))))
   (decreases (betree_node_apply_upserts_decreases msgs prev key st))
   =
-  begin match betree_list_head_has_key_fwd betree_message_t msgs key with
-  | Fail e -> Fail e
-  | Return b ->
-    if b
-    then
-      begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
-      | Fail e -> Fail e
-      | Return msg ->
-        let (_, m) = msg in
-        begin match m with
-        | BetreeMessageInsert i -> Fail Failure
-        | BetreeMessageDelete -> Fail Failure
-        | BetreeMessageUpsert s ->
-          begin match betree_upsert_update_fwd prev s with
-          | Fail e -> Fail e
-          | Return v ->
-            begin match
-              betree_list_pop_front_back (u64 & betree_message_t) msgs with
-            | Fail e -> Fail e
-            | Return msgs0 ->
-              betree_node_apply_upserts_back msgs0 (Some v) key st st0
-            end
-          end
-        end
-      end
-    else
-      begin match core_option_option_unwrap_fwd u64 prev st with
-      | Fail e -> Fail e
-      | Return (_, v) ->
-        begin match
-          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
-            BetreeMessageInsert v) with
-        | Fail e -> Fail e
-        | Return msgs0 -> Return (st0, msgs0)
-        end
-      end
-  end
+  let* b = betree_list_head_has_key_fwd betree_message_t msgs key in
+  if b
+  then begin
+    let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in
+    let (_, m) = msg in
+    begin match m with
+    | BetreeMessageInsert i -> Fail Failure
+    | BetreeMessageDelete -> Fail Failure
+    | BetreeMessageUpsert s ->
+      let* v = betree_upsert_update_fwd 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
+    end end
+  else begin
+    let* (_, v) = core_option_option_unwrap_fwd u64 prev st in
+    let* msgs0 =
+      betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
+        BetreeMessageInsert v) in
+    Return (st0, msgs0) end
 
 (** [betree_main::betree::Node::{5}::lookup] *)
 let rec betree_node_lookup_fwd
@@ -516,104 +365,60 @@ let rec betree_node_lookup_fwd
   =
   begin match self with
   | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail e -> Fail e
-    | Return (st0, msgs) ->
-      begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-      | Fail e -> Fail e
-      | Return pending ->
-        begin match pending with
-        | BetreeListCons p l ->
-          let (k, msg) = p in
-          if k <> key
-          then
-            begin match betree_internal_lookup_in_children_fwd node key st0
-              with
-            | Fail e -> Fail e
-            | Return (st1, opt) ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, msg) l) with
-              | Fail e -> Fail e
-              | Return _ -> Return (st1, opt)
-              end
-            end
-          else
-            begin match msg with
-            | BetreeMessageInsert v ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, BetreeMessageInsert v) l) with
-              | Fail e -> Fail e
-              | Return _ -> Return (st0, Some v)
-              end
-            | BetreeMessageDelete ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, BetreeMessageDelete) l) with
-              | Fail e -> Fail e
-              | Return _ -> Return (st0, None)
-              end
-            | BetreeMessageUpsert ufs ->
-              begin match betree_internal_lookup_in_children_fwd node key st0
-                with
-              | Fail e -> Fail e
-              | Return (st1, v) ->
-                begin match
-                  betree_node_apply_upserts_fwd (BetreeListCons (k,
-                    BetreeMessageUpsert ufs) l) v key st1 with
-                | Fail e -> Fail e
-                | Return (st2, v0) ->
-                  begin match
-                    betree_internal_lookup_in_children_back node key st0 st2
-                    with
-                  | Fail e -> Fail e
-                  | Return (st3, node0) ->
-                    begin match
-                      betree_node_apply_upserts_back (BetreeListCons (k,
-                        BetreeMessageUpsert ufs) l) v key st1 st3 with
-                    | Fail e -> Fail e
-                    | Return (st4, pending0) ->
-                      begin match
-                        betree_node_lookup_first_message_for_key_back key msgs
-                          pending0 with
-                      | Fail e -> Fail e
-                      | Return msgs0 ->
-                        begin match
-                          betree_store_internal_node_fwd
-                            node0.betree_internal_id msgs0 st4 with
-                        | Fail e -> Fail e
-                        | Return (st5, _) -> Return (st5, Some v0)
-                        end
-                      end
-                    end
-                  end
-                end
-              end
-            end
-        | BetreeListNil ->
-          begin match betree_internal_lookup_in_children_fwd node key st0 with
-          | Fail e -> Fail e
-          | Return (st1, opt) ->
-            begin match
-              betree_node_lookup_first_message_for_key_back key msgs
-                BetreeListNil with
-            | Fail e -> Fail e
-            | Return _ -> Return (st1, opt)
-            end
-          end
+    let* (st0, msgs) = betree_load_internal_node_fwd node.betree_internal_id st
+      in
+    let* pending = betree_node_lookup_first_message_for_key_fwd key msgs in
+    begin match pending with
+    | BetreeListCons p l ->
+      let (k, msg) = p in
+      if k <> key
+      then begin
+        let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0
+          in
+        let* _ =
+          betree_node_lookup_first_message_for_key_back key msgs
+            (BetreeListCons (k, msg) l) in
+        Return (st1, opt) end
+      else
+        begin match msg with
+        | BetreeMessageInsert v ->
+          let* _ =
+            betree_node_lookup_first_message_for_key_back key msgs
+              (BetreeListCons (k, BetreeMessageInsert v) l) in
+          Return (st0, Some v)
+        | BetreeMessageDelete ->
+          let* _ =
+            betree_node_lookup_first_message_for_key_back key msgs
+              (BetreeListCons (k, BetreeMessageDelete) l) in
+          Return (st0, None)
+        | BetreeMessageUpsert ufs ->
+          let* (st1, v) = betree_internal_lookup_in_children_fwd node key st0
+            in
+          let* (st2, v0) =
+            betree_node_apply_upserts_fwd (BetreeListCons (k,
+              BetreeMessageUpsert 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 (BetreeListCons (k,
+              BetreeMessageUpsert 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_fwd node0.betree_internal_id msgs0 st4
+            in
+          Return (st5, Some v0)
         end
-      end
+    | BetreeListNil ->
+      let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0 in
+      let* _ =
+        betree_node_lookup_first_message_for_key_back key msgs BetreeListNil in
+      Return (st1, opt)
     end
   | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail e -> Fail e
-    | Return (st0, bindings) ->
-      begin match betree_node_lookup_in_bindings_fwd key bindings with
-      | Fail e -> Fail e
-      | Return opt -> Return (st0, opt)
-      end
-    end
+    let* (st0, bindings) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+    let* opt = betree_node_lookup_in_bindings_fwd key bindings in
+    Return (st0, opt)
   end
 
 (** [betree_main::betree::Node::{5}::lookup] *)
@@ -624,105 +429,61 @@ and betree_node_lookup_back
   =
   begin match self with
   | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail e -> Fail e
-    | Return (st1, msgs) ->
-      begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-      | Fail e -> Fail e
-      | Return pending ->
-        begin match pending with
-        | BetreeListCons p l ->
-          let (k, msg) = p in
-          if k <> key
-          then
-            begin match
-              betree_node_lookup_first_message_for_key_back key msgs
-                (BetreeListCons (k, msg) l) with
-            | Fail e -> Fail e
-            | Return _ ->
-              begin match
-                betree_internal_lookup_in_children_back node key st1 st0 with
-              | Fail e -> Fail e
-              | Return (st2, node0) -> Return (st2, BetreeNodeInternal node0)
-              end
-            end
-          else
-            begin match msg with
-            | BetreeMessageInsert v ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, BetreeMessageInsert v) l) with
-              | Fail e -> Fail e
-              | Return _ -> Return (st0, BetreeNodeInternal node)
-              end
-            | BetreeMessageDelete ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, BetreeMessageDelete) l) with
-              | Fail e -> Fail e
-              | Return _ -> Return (st0, BetreeNodeInternal node)
-              end
-            | BetreeMessageUpsert ufs ->
-              begin match betree_internal_lookup_in_children_fwd node key st1
-                with
-              | Fail e -> Fail e
-              | Return (st2, v) ->
-                begin match
-                  betree_node_apply_upserts_fwd (BetreeListCons (k,
-                    BetreeMessageUpsert ufs) l) v key st2 with
-                | Fail e -> Fail e
-                | Return (st3, _) ->
-                  begin match
-                    betree_internal_lookup_in_children_back node key st1 st3
-                    with
-                  | Fail e -> Fail e
-                  | Return (st4, node0) ->
-                    begin match
-                      betree_node_apply_upserts_back (BetreeListCons (k,
-                        BetreeMessageUpsert ufs) l) v key st2 st4 with
-                    | Fail e -> Fail e
-                    | Return (st5, pending0) ->
-                      begin match
-                        betree_node_lookup_first_message_for_key_back key msgs
-                          pending0 with
-                      | Fail e -> Fail e
-                      | Return msgs0 ->
-                        begin match
-                          betree_store_internal_node_fwd
-                            node0.betree_internal_id msgs0 st5 with
-                        | Fail e -> Fail e
-                        | Return _ -> Return (st0, BetreeNodeInternal node0)
-                        end
-                      end
-                    end
-                  end
-                end
-              end
-            end
-        | BetreeListNil ->
-          begin match
+    let* (st1, msgs) = betree_load_internal_node_fwd node.betree_internal_id st
+      in
+    let* pending = betree_node_lookup_first_message_for_key_fwd key msgs in
+    begin match pending with
+    | BetreeListCons p l ->
+      let (k, msg) = p in
+      if k <> key
+      then begin
+        let* _ =
+          betree_node_lookup_first_message_for_key_back key msgs
+            (BetreeListCons (k, msg) l) in
+        let* (st2, node0) =
+          betree_internal_lookup_in_children_back node key st1 st0 in
+        Return (st2, BetreeNodeInternal node0) end
+      else
+        begin match msg with
+        | BetreeMessageInsert v ->
+          let* _ =
+            betree_node_lookup_first_message_for_key_back key msgs
+              (BetreeListCons (k, BetreeMessageInsert v) l) in
+          Return (st0, BetreeNodeInternal node)
+        | BetreeMessageDelete ->
+          let* _ =
             betree_node_lookup_first_message_for_key_back key msgs
-              BetreeListNil with
-          | Fail e -> Fail e
-          | Return _ ->
-            begin match
-              betree_internal_lookup_in_children_back node key st1 st0 with
-            | Fail e -> Fail e
-            | Return (st2, node0) -> Return (st2, BetreeNodeInternal node0)
-            end
-          end
+              (BetreeListCons (k, BetreeMessageDelete) l) in
+          Return (st0, BetreeNodeInternal node)
+        | BetreeMessageUpsert ufs ->
+          let* (st2, v) = betree_internal_lookup_in_children_fwd node key st1
+            in
+          let* (st3, _) =
+            betree_node_apply_upserts_fwd (BetreeListCons (k,
+              BetreeMessageUpsert 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 (BetreeListCons (k,
+              BetreeMessageUpsert 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_fwd node0.betree_internal_id msgs0 st5
+            in
+          Return (st0, BetreeNodeInternal node0)
         end
-      end
+    | BetreeListNil ->
+      let* _ =
+        betree_node_lookup_first_message_for_key_back key msgs BetreeListNil in
+      let* (st2, node0) =
+        betree_internal_lookup_in_children_back node key st1 st0 in
+      Return (st2, BetreeNodeInternal node0)
     end
   | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail e -> Fail e
-    | Return (_, bindings) ->
-      begin match betree_node_lookup_in_bindings_fwd key bindings with
-      | Fail e -> Fail e
-      | Return _ -> Return (st0, BetreeNodeLeaf node)
-      end
-    end
+    let* (_, bindings) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+    let* _ = betree_node_lookup_in_bindings_fwd key bindings in
+    Return (st0, BetreeNodeLeaf node)
   end
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children] *)
@@ -742,22 +503,16 @@ and betree_internal_lookup_in_children_back
   (decreases (betree_internal_lookup_in_children_decreases self key st))
   =
   if key < self.betree_internal_pivot
-  then
-    begin match betree_node_lookup_back self.betree_internal_left key st st0
-      with
-    | Fail e -> Fail e
-    | Return (st1, n) ->
-      Return (st1, Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n self.betree_internal_right)
-    end
-  else
-    begin match betree_node_lookup_back self.betree_internal_right key st st0
-      with
-    | Fail e -> Fail e
-    | Return (st1, n) ->
-      Return (st1, Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot self.betree_internal_left n)
-    end
+  then begin
+    let* (st1, n) =
+      betree_node_lookup_back self.betree_internal_left key st st0 in
+    Return (st1, Mkbetree_internal_t self.betree_internal_id
+      self.betree_internal_pivot n self.betree_internal_right) end
+  else begin
+    let* (st1, n) =
+      betree_node_lookup_back self.betree_internal_right key st st0 in
+    Return (st1, Mkbetree_internal_t self.betree_internal_id
+      self.betree_internal_pivot self.betree_internal_left n) end
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -786,11 +541,9 @@ let rec betree_node_lookup_mut_in_bindings_back
     let (i, i0) = hd in
     if i >= key
     then Return ret
-    else
-      begin match betree_node_lookup_mut_in_bindings_back key tl ret with
-      | Fail e -> Fail e
-      | Return tl0 -> Return (BetreeListCons (i, i0) tl0)
-      end
+    else begin
+      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
+      Return (BetreeListCons (i, i0) tl0) end
   | BetreeListNil -> Return ret
   end
 
@@ -800,82 +553,42 @@ let betree_node_apply_to_leaf_fwd_back
   (new_msg : betree_message_t) :
   result (betree_list_t (u64 & u64))
   =
-  begin match betree_node_lookup_mut_in_bindings_fwd key bindings with
-  | Fail e -> Fail e
-  | Return bindings0 ->
-    begin match betree_list_head_has_key_fwd u64 bindings0 key with
-    | Fail e -> Fail e
-    | Return b ->
-      if b
-      then
-        begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with
-        | Fail e -> Fail e
-        | Return hd ->
-          begin match new_msg with
-          | BetreeMessageInsert v ->
-            begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-            | Fail e -> Fail e
-            | Return bindings1 ->
-              begin match
-                betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v)
-                with
-              | Fail e -> Fail e
-              | Return bindings2 ->
-                betree_node_lookup_mut_in_bindings_back key bindings bindings2
-              end
-            end
-          | BetreeMessageDelete ->
-            begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-            | Fail e -> Fail e
-            | Return bindings1 ->
-              betree_node_lookup_mut_in_bindings_back key bindings bindings1
-            end
-          | BetreeMessageUpsert s ->
-            let (_, i) = hd in
-            begin match betree_upsert_update_fwd (Some i) s with
-            | Fail e -> Fail e
-            | Return v ->
-              begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-              | Fail e -> Fail e
-              | Return bindings1 ->
-                begin match
-                  betree_list_push_front_fwd_back (u64 & u64) bindings1 (key,
-                    v) with
-                | Fail e -> Fail e
-                | Return bindings2 ->
-                  betree_node_lookup_mut_in_bindings_back key bindings
-                    bindings2
-                end
-              end
-            end
-          end
-        end
-      else
-        begin match new_msg with
-        | BetreeMessageInsert v ->
-          begin match
-            betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with
-          | Fail e -> Fail e
-          | Return bindings1 ->
-            betree_node_lookup_mut_in_bindings_back key bindings bindings1
-          end
-        | BetreeMessageDelete ->
-          betree_node_lookup_mut_in_bindings_back key bindings bindings0
-        | BetreeMessageUpsert s ->
-          begin match betree_upsert_update_fwd None s with
-          | Fail e -> Fail e
-          | Return v ->
-            begin match
-              betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v)
-              with
-            | Fail e -> Fail e
-            | Return bindings1 ->
-              betree_node_lookup_mut_in_bindings_back key bindings bindings1
-            end
-          end
-        end
+  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 begin
+    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 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
-  end
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *)
 let rec betree_node_apply_messages_to_leaf_fwd_back
@@ -887,11 +600,8 @@ let rec betree_node_apply_messages_to_leaf_fwd_back
   begin match new_msgs with
   | BetreeListCons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
-    begin match betree_node_apply_to_leaf_fwd_back bindings i m with
-    | Fail e -> Fail e
-    | Return bindings0 ->
-      betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
-    end
+    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
 
@@ -905,13 +615,11 @@ let rec betree_node_filter_messages_for_key_fwd_back
   | BetreeListCons p l ->
     let (k, m) = p in
     if k = key
-    then
-      begin match
+    then begin
+      let* msgs0 =
         betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
-          m) l) with
-      | Fail e -> Fail e
-      | Return msgs0 -> betree_node_filter_messages_for_key_fwd_back key msgs0
-      end
+          m) l) in
+      betree_node_filter_messages_for_key_fwd_back key msgs0 end
     else Return (BetreeListCons (k, m) l)
   | BetreeListNil -> Return BetreeListNil
   end
@@ -942,12 +650,10 @@ let rec betree_node_lookup_first_message_after_key_back
   | BetreeListCons p next_msgs ->
     let (k, m) = p in
     if k = key
-    then
-      begin match
-        betree_node_lookup_first_message_after_key_back key next_msgs ret with
-      | Fail e -> Fail e
-      | Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0)
-      end
+    then begin
+      let* next_msgs0 =
+        betree_node_lookup_first_message_after_key_back key next_msgs ret in
+      Return (BetreeListCons (k, m) next_msgs0) end
     else Return ret
   | BetreeListNil -> Return ret
   end
@@ -958,118 +664,59 @@ let betree_node_apply_to_internal_fwd_back
   (new_msg : betree_message_t) :
   result (betree_list_t (u64 & betree_message_t))
   =
-  begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-  | Fail e -> Fail e
-  | Return msgs0 ->
-    begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with
-    | Fail e -> Fail e
-    | Return b ->
-      if b
-      then
-        begin match new_msg with
-        | BetreeMessageInsert i ->
-          begin match betree_node_filter_messages_for_key_fwd_back key msgs0
-            with
-          | Fail e -> Fail e
-          | Return msgs1 ->
-            begin match
-              betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
-                (key, BetreeMessageInsert i) with
-            | Fail e -> Fail e
-            | Return msgs2 ->
-              betree_node_lookup_first_message_for_key_back key msgs msgs2
-            end
-          end
-        | BetreeMessageDelete ->
-          begin match betree_node_filter_messages_for_key_fwd_back key msgs0
-            with
-          | Fail e -> Fail e
-          | Return msgs1 ->
-            begin match
-              betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
-                (key, BetreeMessageDelete) with
-            | Fail e -> Fail e
-            | Return msgs2 ->
-              betree_node_lookup_first_message_for_key_back key msgs msgs2
-            end
-          end
-        | BetreeMessageUpsert s ->
-          begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with
-          | Fail e -> Fail e
-          | Return p ->
-            let (_, m) = p in
-            begin match m with
-            | BetreeMessageInsert prev ->
-              begin match betree_upsert_update_fwd (Some prev) s with
-              | Fail e -> Fail e
-              | Return v ->
-                begin match
-                  betree_list_pop_front_back (u64 & betree_message_t) msgs0
-                  with
-                | Fail e -> Fail e
-                | Return msgs1 ->
-                  begin match
-                    betree_list_push_front_fwd_back (u64 & betree_message_t)
-                      msgs1 (key, BetreeMessageInsert v) with
-                  | Fail e -> Fail e
-                  | Return msgs2 ->
-                    betree_node_lookup_first_message_for_key_back key msgs
-                      msgs2
-                  end
-                end
-              end
-            | BetreeMessageDelete ->
-              begin match betree_upsert_update_fwd None s with
-              | Fail e -> Fail e
-              | Return v ->
-                begin match
-                  betree_list_pop_front_back (u64 & betree_message_t) msgs0
-                  with
-                | Fail e -> Fail e
-                | Return msgs1 ->
-                  begin match
-                    betree_list_push_front_fwd_back (u64 & betree_message_t)
-                      msgs1 (key, BetreeMessageInsert v) with
-                  | Fail e -> Fail e
-                  | Return msgs2 ->
-                    betree_node_lookup_first_message_for_key_back key msgs
-                      msgs2
-                  end
-                end
-              end
-            | BetreeMessageUpsert ufs ->
-              begin match
-                betree_node_lookup_first_message_after_key_fwd key msgs0 with
-              | Fail e -> Fail e
-              | Return msgs1 ->
-                begin match
-                  betree_list_push_front_fwd_back (u64 & betree_message_t)
-                    msgs1 (key, BetreeMessageUpsert s) with
-                | Fail e -> Fail e
-                | Return msgs2 ->
-                  begin match
-                    betree_node_lookup_first_message_after_key_back key msgs0
-                      msgs2 with
-                  | Fail e -> Fail e
-                  | Return msgs3 ->
-                    betree_node_lookup_first_message_for_key_back key msgs
-                      msgs3
-                  end
-                end
-              end
-            end
-          end
-        end
-      else
-        begin match
-          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
-            new_msg) with
-        | Fail e -> Fail e
-        | Return msgs1 ->
-          betree_node_lookup_first_message_for_key_back key msgs msgs1
-        end
+  let* msgs0 = betree_node_lookup_first_message_for_key_fwd key msgs in
+  let* b = betree_list_head_has_key_fwd betree_message_t msgs0 key in
+  if b
+  then
+    begin match new_msg with
+    | BetreeMessageInsert i ->
+      let* msgs1 = betree_node_filter_messages_for_key_fwd_back key msgs0 in
+      let* msgs2 =
+        betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key,
+          BetreeMessageInsert i) in
+      betree_node_lookup_first_message_for_key_back key msgs msgs2
+    | BetreeMessageDelete ->
+      let* msgs1 = betree_node_filter_messages_for_key_fwd_back key msgs0 in
+      let* msgs2 =
+        betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key,
+          BetreeMessageDelete) in
+      betree_node_lookup_first_message_for_key_back key msgs msgs2
+    | BetreeMessageUpsert s ->
+      let* p = betree_list_hd_fwd (u64 & betree_message_t) msgs0 in
+      let (_, m) = p in
+      begin match m with
+      | BetreeMessageInsert prev ->
+        let* v = betree_upsert_update_fwd (Some prev) s in
+        let* msgs1 = betree_list_pop_front_back (u64 & betree_message_t) msgs0
+          in
+        let* msgs2 =
+          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key,
+            BetreeMessageInsert v) in
+        betree_node_lookup_first_message_for_key_back key msgs msgs2
+      | BetreeMessageDelete ->
+        let* v = betree_upsert_update_fwd None s in
+        let* msgs1 = betree_list_pop_front_back (u64 & betree_message_t) msgs0
+          in
+        let* msgs2 =
+          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key,
+            BetreeMessageInsert v) in
+        betree_node_lookup_first_message_for_key_back key msgs msgs2
+      | BetreeMessageUpsert ufs ->
+        let* msgs1 = betree_node_lookup_first_message_after_key_fwd key msgs0
+          in
+        let* msgs2 =
+          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key,
+            BetreeMessageUpsert 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
+      end
     end
-  end
+  else begin
+    let* msgs1 =
+      betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
+        new_msg) in
+    betree_node_lookup_first_message_for_key_back key msgs msgs1 end
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
 let rec betree_node_apply_messages_to_internal_fwd_back
@@ -1081,11 +728,8 @@ let rec betree_node_apply_messages_to_internal_fwd_back
   begin match new_msgs with
   | BetreeListCons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
-    begin match betree_node_apply_to_internal_fwd_back msgs i m with
-    | Fail e -> Fail e
-    | Return msgs0 ->
-      betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl
-    end
+    let* msgs0 = betree_node_apply_to_internal_fwd_back msgs i m in
+    betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl
   | BetreeListNil -> Return msgs
   end
 
@@ -1100,85 +744,41 @@ let rec betree_node_apply_messages_fwd
   =
   begin match self with
   | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail e -> Fail e
-    | Return (st0, content) ->
-      begin match betree_node_apply_messages_to_internal_fwd_back content msgs
-        with
-      | Fail e -> Fail e
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail e -> Fail e
-        | Return num_msgs ->
-          if num_msgs >= params.betree_params_min_flush_size
-          then
-            begin match
-              betree_internal_flush_fwd node params node_id_cnt content0 st0
-              with
-            | Fail e -> Fail e
-            | Return (st1, content1) ->
-              begin match
-                betree_internal_flush_back'a node params node_id_cnt content0
-                  st0 st1 with
-              | Fail e -> Fail e
-              | Return (st2, (node0, _)) ->
-                begin match
-                  betree_store_internal_node_fwd node0.betree_internal_id
-                    content1 st2 with
-                | Fail e -> Fail e
-                | Return (st3, _) -> Return (st3, ())
-                end
-              end
-            end
-          else
-            begin match
-              betree_store_internal_node_fwd node.betree_internal_id content0
-                st0 with
-            | Fail e -> Fail e
-            | Return (st1, _) -> Return (st1, ())
-            end
-        end
-      end
-    end
+    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 begin
+      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, ()) end
+    else begin
+      let* (st1, _) =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
+      Return (st1, ()) end
   | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail e -> Fail e
-    | Return (st0, content) ->
-      begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail e -> Fail e
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail e -> Fail e
-        | Return len ->
-          begin match u64_mul 2 params.betree_params_split_size with
-          | Fail e -> Fail e
-          | Return i ->
-            if len >= i
-            then
-              begin match
-                betree_leaf_split_fwd node content0 params node_id_cnt st0 with
-              | Fail e -> Fail e
-              | Return (st1, _) ->
-                begin match
-                  betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
-                    st1 with
-                | Fail e -> Fail e
-                | Return (st2, _) ->
-                  betree_leaf_split_back0 node content0 params node_id_cnt st0
-                    st2
-                end
-              end
-            else
-              begin match
-                betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
-                with
-              | Fail e -> Fail e
-              | Return (st1, _) -> Return (st1, ())
-              end
-          end
-        end
-      end
-    end
+    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 begin
+      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 end
+    else begin
+      let* (st1, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
+      Return (st1, ()) end
   end
 
 (** [betree_main::betree::Node::{5}::apply_messages] *)
@@ -1192,99 +792,45 @@ and betree_node_apply_messages_back'a
   =
   begin match self with
   | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail e -> Fail e
-    | Return (st1, content) ->
-      begin match betree_node_apply_messages_to_internal_fwd_back content msgs
-        with
-      | Fail e -> Fail e
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail e -> Fail e
-        | Return num_msgs ->
-          if num_msgs >= params.betree_params_min_flush_size
-          then
-            begin match
-              betree_internal_flush_fwd node params node_id_cnt content0 st1
-              with
-            | Fail e -> Fail e
-            | Return (st2, content1) ->
-              begin match
-                betree_internal_flush_back'a node params node_id_cnt content0
-                  st1 st2 with
-              | Fail e -> Fail e
-              | Return (st3, (node0, node_id_cnt0)) ->
-                begin match
-                  betree_store_internal_node_fwd node0.betree_internal_id
-                    content1 st3 with
-                | Fail e -> Fail e
-                | Return _ ->
-                  Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
-                end
-              end
-            end
-          else
-            begin match
-              betree_store_internal_node_fwd node.betree_internal_id content0
-                st1 with
-            | Fail e -> Fail e
-            | Return _ -> Return (st0, (BetreeNodeInternal node, node_id_cnt))
-            end
-        end
-      end
-    end
+    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 begin
+      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)) end
+    else begin
+      let* _ =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
+      Return (st0, (BetreeNodeInternal node, node_id_cnt)) end
   | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail e -> Fail e
-    | Return (st1, content) ->
-      begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail e -> Fail e
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail e -> Fail e
-        | Return len ->
-          begin match u64_mul 2 params.betree_params_split_size with
-          | Fail e -> Fail e
-          | Return i ->
-            if len >= i
-            then
-              begin match
-                betree_leaf_split_fwd node content0 params node_id_cnt st1 with
-              | Fail e -> Fail e
-              | Return (st2, new_node) ->
-                begin match
-                  betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
-                    st2 with
-                | Fail e -> Fail e
-                | Return (st3, _) ->
-                  begin match
-                    betree_leaf_split_back0 node content0 params node_id_cnt
-                      st1 st3 with
-                  | Fail e -> Fail e
-                  | Return _ ->
-                    begin match
-                      betree_leaf_split_back2 node content0 params node_id_cnt
-                        st1 st0 with
-                    | Fail e -> Fail e
-                    | Return (st4, node_id_cnt0) ->
-                      Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
-                    end
-                  end
-                end
-              end
-            else
-              begin match
-                betree_store_leaf_node_fwd node.betree_leaf_id content0 st1
-                with
-              | Fail e -> Fail e
-              | Return _ ->
-                Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t
-                  node.betree_leaf_id len), node_id_cnt))
-              end
-          end
-        end
-      end
-    end
+    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 begin
+      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)) end
+    else begin
+      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
+      Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len),
+        node_id_cnt)) end
   end
 
 (** [betree_main::betree::Node::{5}::apply_messages] *)
@@ -1298,93 +844,42 @@ and betree_node_apply_messages_back1
   =
   begin match self with
   | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail e -> Fail e
-    | Return (st1, content) ->
-      begin match betree_node_apply_messages_to_internal_fwd_back content msgs
-        with
-      | Fail e -> Fail e
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail e -> Fail e
-        | Return num_msgs ->
-          if num_msgs >= params.betree_params_min_flush_size
-          then
-            begin match
-              betree_internal_flush_fwd node params node_id_cnt content0 st1
-              with
-            | Fail e -> Fail e
-            | Return (st2, content1) ->
-              begin match
-                betree_internal_flush_back'a node params node_id_cnt content0
-                  st1 st2 with
-              | Fail e -> Fail e
-              | Return (st3, (node0, _)) ->
-                begin match
-                  betree_store_internal_node_fwd node0.betree_internal_id
-                    content1 st3 with
-                | Fail e -> Fail e
-                | Return _ ->
-                  betree_internal_flush_back1 node params node_id_cnt content0
-                    st1 st0
-                end
-              end
-            end
-          else
-            begin match
-              betree_store_internal_node_fwd node.betree_internal_id content0
-                st1 with
-            | Fail e -> Fail e
-            | Return _ -> Return (st0, ())
-            end
-        end
-      end
-    end
+    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 begin
+      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 end
+    else begin
+      let* _ =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
+      Return (st0, ()) end
   | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail e -> Fail e
-    | Return (st1, content) ->
-      begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail e -> Fail e
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail e -> Fail e
-        | Return len ->
-          begin match u64_mul 2 params.betree_params_split_size with
-          | Fail e -> Fail e
-          | Return i ->
-            if len >= i
-            then
-              begin match
-                betree_leaf_split_fwd node content0 params node_id_cnt st1 with
-              | Fail e -> Fail e
-              | Return (st2, _) ->
-                begin match
-                  betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
-                    st2 with
-                | Fail e -> Fail e
-                | Return (st3, _) ->
-                  begin match
-                    betree_leaf_split_back0 node content0 params node_id_cnt
-                      st1 st3 with
-                  | Fail e -> Fail e
-                  | Return _ ->
-                    betree_leaf_split_back1 node content0 params node_id_cnt
-                      st1 st0
-                  end
-                end
-              end
-            else
-              begin match
-                betree_store_leaf_node_fwd node.betree_leaf_id content0 st1
-                with
-              | Fail e -> Fail e
-              | Return _ -> Return (st0, ())
-              end
-          end
-        end
-      end
-    end
+    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 begin
+      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 end
+    else begin
+      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
+      Return (st0, ()) end
   end
 
 (** [betree_main::betree::Internal::{4}::flush] *)
@@ -1396,84 +891,47 @@ and betree_internal_flush_fwd
   (decreases (
     betree_internal_flush_decreases self params node_id_cnt content st))
   =
-  begin match
+  let* p =
     betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot with
-  | Fail e -> Fail e
-  | Return p ->
-    let (msgs_left, msgs_right) = p in
-    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail e -> Fail e
-    | Return len_left ->
-      if len_left >= params.betree_params_min_flush_size
-      then
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st with
-        | Fail e -> Fail e
-        | Return (st0, _) ->
-          begin match
-            betree_node_apply_messages_back'a self.betree_internal_left params
-              node_id_cnt msgs_left st st0 with
-          | Fail e -> Fail e
-          | Return (st1, (_, node_id_cnt0)) ->
-            begin match
-              betree_node_apply_messages_back1 self.betree_internal_left params
-                node_id_cnt msgs_left st st1 with
-            | Fail e -> Fail e
-            | Return (st2, ()) ->
-              begin match
-                betree_list_len_fwd (u64 & betree_message_t) msgs_right with
-              | Fail e -> Fail e
-              | Return len_right ->
-                if len_right >= params.betree_params_min_flush_size
-                then
-                  begin match
-                    betree_node_apply_messages_fwd self.betree_internal_right
-                      params node_id_cnt0 msgs_right st2 with
-                  | Fail e -> Fail e
-                  | Return (st3, _) ->
-                    begin match
-                      betree_node_apply_messages_back'a
-                        self.betree_internal_right params node_id_cnt0
-                        msgs_right st2 st3 with
-                    | Fail e -> Fail e
-                    | Return (st4, (_, _)) ->
-                      begin match
-                        betree_node_apply_messages_back1
-                          self.betree_internal_right params node_id_cnt0
-                          msgs_right st2 st4 with
-                      | Fail e -> Fail e
-                      | Return (st5, ()) -> Return (st5, BetreeListNil)
-                      end
-                    end
-                  end
-                else Return (st2, msgs_right)
-              end
-            end
-          end
-        end
-      else
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_right params
-            node_id_cnt msgs_right st with
-        | Fail e -> Fail e
-        | Return (st0, _) ->
-          begin match
-            betree_node_apply_messages_back'a self.betree_internal_right params
-              node_id_cnt msgs_right st st0 with
-          | Fail e -> Fail e
-          | Return (st1, (_, _)) ->
-            begin match
-              betree_node_apply_messages_back1 self.betree_internal_right
-                params node_id_cnt msgs_right st st1 with
-            | Fail e -> Fail e
-            | Return (st2, ()) -> Return (st2, msgs_left)
-            end
-          end
-        end
-    end
-  end
+      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 begin
+    let* (st0, _) =
+      betree_node_apply_messages_fwd self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* (st1, (_, node_id_cnt0)) =
+      betree_node_apply_messages_back'a self.betree_internal_left params
+        node_id_cnt msgs_left st st0 in
+    let* (st2, ()) =
+      betree_node_apply_messages_back1 self.betree_internal_left params
+        node_id_cnt msgs_left st st1 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 begin
+      let* (st3, _) =
+        betree_node_apply_messages_fwd self.betree_internal_right params
+          node_id_cnt0 msgs_right st2 in
+      let* (st4, (_, _)) =
+        betree_node_apply_messages_back'a self.betree_internal_right params
+          node_id_cnt0 msgs_right st2 st3 in
+      let* (st5, ()) =
+        betree_node_apply_messages_back1 self.betree_internal_right params
+          node_id_cnt0 msgs_right st2 st4 in
+      Return (st5, BetreeListNil) end
+    else Return (st2, msgs_right) end
+  else begin
+    let* (st0, _) =
+      betree_node_apply_messages_fwd self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    let* (st1, (_, _)) =
+      betree_node_apply_messages_back'a self.betree_internal_right params
+        node_id_cnt msgs_right st st0 in
+    let* (st2, ()) =
+      betree_node_apply_messages_back1 self.betree_internal_right params
+        node_id_cnt msgs_right st st1 in
+    Return (st2, msgs_left) end
 
 (** [betree_main::betree::Internal::{4}::flush] *)
 and betree_internal_flush_back'a
@@ -1485,93 +943,53 @@ and betree_internal_flush_back'a
   (decreases (
     betree_internal_flush_decreases self params node_id_cnt content st))
   =
-  begin match
+  let* p =
     betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot with
-  | Fail e -> Fail e
-  | Return p ->
-    let (msgs_left, msgs_right) = p in
-    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail e -> Fail e
-    | Return len_left ->
-      if len_left >= params.betree_params_min_flush_size
-      then
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st with
-        | Fail e -> Fail e
-        | Return (st1, _) ->
-          begin match
-            betree_node_apply_messages_back'a self.betree_internal_left params
-              node_id_cnt msgs_left st st1 with
-          | Fail e -> Fail e
-          | Return (st2, (n, node_id_cnt0)) ->
-            begin match
-              betree_node_apply_messages_back1 self.betree_internal_left params
-                node_id_cnt msgs_left st st2 with
-            | Fail e -> Fail e
-            | Return (st3, ()) ->
-              begin match
-                betree_list_len_fwd (u64 & betree_message_t) msgs_right with
-              | Fail e -> Fail e
-              | Return len_right ->
-                if len_right >= params.betree_params_min_flush_size
-                then
-                  begin match
-                    betree_node_apply_messages_fwd self.betree_internal_right
-                      params node_id_cnt0 msgs_right st3 with
-                  | Fail e -> Fail e
-                  | Return (st4, _) ->
-                    begin match
-                      betree_node_apply_messages_back'a
-                        self.betree_internal_right params node_id_cnt0
-                        msgs_right st3 st4 with
-                    | Fail e -> Fail e
-                    | Return (st5, (n0, node_id_cnt1)) ->
-                      begin match
-                        betree_node_apply_messages_back1
-                          self.betree_internal_right params node_id_cnt0
-                          msgs_right st3 st5 with
-                      | Fail e -> Fail e
-                      | Return _ ->
-                        Return (st0, (Mkbetree_internal_t
-                          self.betree_internal_id self.betree_internal_pivot n
-                          n0, node_id_cnt1))
-                      end
-                    end
-                  end
-                else
-                  Return (st0, (Mkbetree_internal_t self.betree_internal_id
-                    self.betree_internal_pivot n self.betree_internal_right,
-                    node_id_cnt0))
-              end
-            end
-          end
-        end
-      else
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_right params
-            node_id_cnt msgs_right st with
-        | Fail e -> Fail e
-        | Return (st1, _) ->
-          begin match
-            betree_node_apply_messages_back'a self.betree_internal_right params
-              node_id_cnt msgs_right st st1 with
-          | Fail e -> Fail e
-          | Return (st2, (n, node_id_cnt0)) ->
-            begin match
-              betree_node_apply_messages_back1 self.betree_internal_right
-                params node_id_cnt msgs_right st st2 with
-            | Fail e -> Fail e
-            | Return _ ->
-              Return (st0, (Mkbetree_internal_t self.betree_internal_id
-                self.betree_internal_pivot self.betree_internal_left n,
-                node_id_cnt0))
-            end
-          end
-        end
+      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 begin
+    let* (st1, _) =
+      betree_node_apply_messages_fwd self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* (st2, (n, node_id_cnt0)) =
+      betree_node_apply_messages_back'a self.betree_internal_left params
+        node_id_cnt msgs_left st st1 in
+    let* (st3, ()) =
+      betree_node_apply_messages_back1 self.betree_internal_left params
+        node_id_cnt msgs_left st st2 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 begin
+      let* (st4, _) =
+        betree_node_apply_messages_fwd self.betree_internal_right params
+          node_id_cnt0 msgs_right st3 in
+      let* (st5, (n0, node_id_cnt1)) =
+        betree_node_apply_messages_back'a self.betree_internal_right params
+          node_id_cnt0 msgs_right st3 st4 in
+      let* _ =
+        betree_node_apply_messages_back1 self.betree_internal_right params
+          node_id_cnt0 msgs_right st3 st5 in
+      Return (st0, (Mkbetree_internal_t self.betree_internal_id
+        self.betree_internal_pivot n n0, node_id_cnt1)) end
+    else
+      Return (st0, (Mkbetree_internal_t self.betree_internal_id
+        self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0))
+    end
+  else begin
+    let* (st1, _) =
+      betree_node_apply_messages_fwd self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    let* (st2, (n, node_id_cnt0)) =
+      betree_node_apply_messages_back'a self.betree_internal_right params
+        node_id_cnt msgs_right st st1 in
+    let* _ =
+      betree_node_apply_messages_back1 self.betree_internal_right params
+        node_id_cnt msgs_right st st2 in
+    Return (st0, (Mkbetree_internal_t self.betree_internal_id
+      self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0))
     end
-  end
 
 (** [betree_main::betree::Internal::{4}::flush] *)
 and betree_internal_flush_back1
@@ -1583,84 +1001,47 @@ and betree_internal_flush_back1
   (decreases (
     betree_internal_flush_decreases self params node_id_cnt content st))
   =
-  begin match
+  let* p =
     betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot with
-  | Fail e -> Fail e
-  | Return p ->
-    let (msgs_left, msgs_right) = p in
-    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail e -> Fail e
-    | Return len_left ->
-      if len_left >= params.betree_params_min_flush_size
-      then
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st with
-        | Fail e -> Fail e
-        | Return (st1, _) ->
-          begin match
-            betree_node_apply_messages_back'a self.betree_internal_left params
-              node_id_cnt msgs_left st st1 with
-          | Fail e -> Fail e
-          | Return (st2, (_, node_id_cnt0)) ->
-            begin match
-              betree_node_apply_messages_back1 self.betree_internal_left params
-                node_id_cnt msgs_left st st2 with
-            | Fail e -> Fail e
-            | Return (st3, ()) ->
-              begin match
-                betree_list_len_fwd (u64 & betree_message_t) msgs_right with
-              | Fail e -> Fail e
-              | Return len_right ->
-                if len_right >= params.betree_params_min_flush_size
-                then
-                  begin match
-                    betree_node_apply_messages_fwd self.betree_internal_right
-                      params node_id_cnt0 msgs_right st3 with
-                  | Fail e -> Fail e
-                  | Return (st4, _) ->
-                    begin match
-                      betree_node_apply_messages_back'a
-                        self.betree_internal_right params node_id_cnt0
-                        msgs_right st3 st4 with
-                    | Fail e -> Fail e
-                    | Return (st5, (_, _)) ->
-                      begin match
-                        betree_node_apply_messages_back1
-                          self.betree_internal_right params node_id_cnt0
-                          msgs_right st3 st5 with
-                      | Fail e -> Fail e
-                      | Return _ -> Return (st0, ())
-                      end
-                    end
-                  end
-                else Return (st0, ())
-              end
-            end
-          end
-        end
-      else
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_right params
-            node_id_cnt msgs_right st with
-        | Fail e -> Fail e
-        | Return (st1, _) ->
-          begin match
-            betree_node_apply_messages_back'a self.betree_internal_right params
-              node_id_cnt msgs_right st st1 with
-          | Fail e -> Fail e
-          | Return (st2, (_, _)) ->
-            begin match
-              betree_node_apply_messages_back1 self.betree_internal_right
-                params node_id_cnt msgs_right st st2 with
-            | Fail e -> Fail e
-            | Return _ -> Return (st0, ())
-            end
-          end
-        end
-    end
-  end
+      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 begin
+    let* (st1, _) =
+      betree_node_apply_messages_fwd self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* (st2, (_, node_id_cnt0)) =
+      betree_node_apply_messages_back'a self.betree_internal_left params
+        node_id_cnt msgs_left st st1 in
+    let* (st3, ()) =
+      betree_node_apply_messages_back1 self.betree_internal_left params
+        node_id_cnt msgs_left st st2 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 begin
+      let* (st4, _) =
+        betree_node_apply_messages_fwd self.betree_internal_right params
+          node_id_cnt0 msgs_right st3 in
+      let* (st5, (_, _)) =
+        betree_node_apply_messages_back'a self.betree_internal_right params
+          node_id_cnt0 msgs_right st3 st4 in
+      let* _ =
+        betree_node_apply_messages_back1 self.betree_internal_right params
+          node_id_cnt0 msgs_right st3 st5 in
+      Return (st0, ()) end
+    else Return (st0, ()) end
+  else begin
+    let* (st1, _) =
+      betree_node_apply_messages_fwd self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    let* (st2, (_, _)) =
+      betree_node_apply_messages_back'a self.betree_internal_right params
+        node_id_cnt msgs_right st st1 in
+    let* _ =
+      betree_node_apply_messages_back1 self.betree_internal_right params
+        node_id_cnt msgs_right st st2 in
+    Return (st0, ()) end
 
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_fwd
@@ -1670,20 +1051,14 @@ let betree_node_apply_fwd
   result (state & unit)
   =
   let l = BetreeListNil in
-  begin match
+  let* (st0, _) =
     betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
-      (key, new_msg) l) st with
-  | Fail e -> Fail e
-  | Return (st0, _) ->
-    begin match
-      betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
-        (key, new_msg) l) st st0 with
-    | Fail e -> Fail e
-    | Return (st1, (_, _)) ->
-      betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons
-        (key, new_msg) l) st st1
-    end
-  end
+      (key, new_msg) l) st in
+  let* (st1, (_, _)) =
+    betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
+      (key, new_msg) l) st st0 in
+  betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons
+    (key, new_msg) l) st st1
 
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_back'a
@@ -1693,24 +1068,16 @@ let betree_node_apply_back'a
   result (state & (betree_node_t & betree_node_id_counter_t))
   =
   let l = BetreeListNil in
-  begin match
+  let* (st1, _) =
     betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
-      (key, new_msg) l) st with
-  | Fail e -> Fail e
-  | Return (st1, _) ->
-    begin match
-      betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
-        (key, new_msg) l) st st1 with
-    | Fail e -> Fail e
-    | Return (st2, (self0, node_id_cnt0)) ->
-      begin match
-        betree_node_apply_messages_back1 self params node_id_cnt
-          (BetreeListCons (key, new_msg) l) st st2 with
-      | Fail e -> Fail e
-      | Return _ -> Return (st0, (self0, node_id_cnt0))
-      end
-    end
-  end
+      (key, new_msg) l) st in
+  let* (st2, (self0, node_id_cnt0)) =
+    betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
+      (key, new_msg) l) st st1 in
+  let* _ =
+    betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons
+      (key, new_msg) l) st st2 in
+  Return (st0, (self0, node_id_cnt0))
 
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_back1
@@ -1720,70 +1087,43 @@ let betree_node_apply_back1
   result (state & unit)
   =
   let l = BetreeListNil in
-  begin match
+  let* (st1, _) =
     betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
-      (key, new_msg) l) st with
-  | Fail e -> Fail e
-  | Return (st1, _) ->
-    begin match
-      betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
-        (key, new_msg) l) st st1 with
-    | Fail e -> Fail e
-    | Return (st2, (_, _)) ->
-      begin match
-        betree_node_apply_messages_back1 self params node_id_cnt
-          (BetreeListCons (key, new_msg) l) st st2 with
-      | Fail e -> Fail e
-      | Return _ -> Return (st0, ())
-      end
-    end
-  end
+      (key, new_msg) l) st in
+  let* (st2, (_, _)) =
+    betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
+      (key, new_msg) l) st st1 in
+  let* _ =
+    betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons
+      (key, new_msg) l) st st2 in
+  Return (st0, ())
 
 (** [betree_main::betree::BeTree::{6}::new] *)
 let betree_be_tree_new_fwd
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state & betree_be_tree_t)
   =
-  begin match betree_node_id_counter_new_fwd with
-  | Fail e -> Fail e
-  | Return node_id_cnt ->
-    begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-    | Fail e -> Fail e
-    | Return id ->
-      begin match betree_store_leaf_node_fwd id BetreeListNil st with
-      | Fail e -> Fail e
-      | Return (st0, _) ->
-        begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail e -> Fail e
-        | Return node_id_cnt0 ->
-          Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size
-            split_size) node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
-        end
-      end
-    end
-  end
+  let* node_id_cnt = betree_node_id_counter_new_fwd in
+  let* id = betree_node_id_counter_fresh_id_fwd node_id_cnt in
+  let* (st0, _) = betree_store_leaf_node_fwd id BetreeListNil st in
+  let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
+  Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size)
+    node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
 let betree_be_tree_apply_fwd
   (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) :
   result (state & unit)
   =
-  begin match
+  let* (st0, _) =
     betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
-      self.betree_be_tree_node_id_cnt key msg st with
-  | Fail e -> Fail e
-  | Return (st0, _) ->
-    begin match
-      betree_node_apply_back'a self.betree_be_tree_root
-        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-        st0 with
-    | Fail e -> Fail e
-    | Return (st1, (_, _)) ->
-      betree_node_apply_back1 self.betree_be_tree_root
-        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-        st1
-    end
-  end
+      self.betree_be_tree_node_id_cnt key msg st in
+  let* (st1, (_, _)) =
+    betree_node_apply_back'a self.betree_be_tree_root
+      self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st0
+    in
+  betree_node_apply_back1 self.betree_be_tree_root self.betree_be_tree_params
+    self.betree_be_tree_node_id_cnt key msg st st1
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
 let betree_be_tree_apply_back
@@ -1791,44 +1131,28 @@ let betree_be_tree_apply_back
   (st0 : state) :
   result (state & betree_be_tree_t)
   =
-  begin match
+  let* (st1, _) =
     betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
-      self.betree_be_tree_node_id_cnt key msg st with
-  | Fail e -> Fail e
-  | Return (st1, _) ->
-    begin match
-      betree_node_apply_back'a self.betree_be_tree_root
-        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-        st1 with
-    | Fail e -> Fail e
-    | Return (st2, (n, nic)) ->
-      begin match
-        betree_node_apply_back1 self.betree_be_tree_root
-          self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-          st2 with
-      | Fail e -> Fail e
-      | Return _ ->
-        Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n)
-      end
-    end
-  end
+      self.betree_be_tree_node_id_cnt key msg st in
+  let* (st2, (n, nic)) =
+    betree_node_apply_back'a self.betree_be_tree_root
+      self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st1
+    in
+  let* _ =
+    betree_node_apply_back1 self.betree_be_tree_root self.betree_be_tree_params
+      self.betree_be_tree_node_id_cnt key msg st st2 in
+  Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n)
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 let betree_be_tree_insert_fwd
   (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) :
   result (state & unit)
   =
-  begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st
-    with
-  | Fail e -> Fail e
-  | Return (st0, _) ->
-    begin match
-      betree_be_tree_apply_back self key (BetreeMessageInsert value) st st0
-      with
-    | Fail e -> Fail e
-    | Return (st1, _) -> Return (st1, ())
-    end
-  end
+  let* (st0, _) =
+    betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st in
+  let* (st1, _) =
+    betree_be_tree_apply_back self key (BetreeMessageInsert value) st st0 in
+  Return (st1, ())
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 let betree_be_tree_insert_back
@@ -1836,45 +1160,29 @@ let betree_be_tree_insert_back
   (st0 : state) :
   result (state & betree_be_tree_t)
   =
-  begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st
-    with
-  | Fail e -> Fail e
-  | Return (st1, _) ->
-    begin match
-      betree_be_tree_apply_back self key (BetreeMessageInsert value) st st1
-      with
-    | Fail e -> Fail e
-    | Return (_, self0) -> Return (st0, self0)
-    end
-  end
+  let* (st1, _) =
+    betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st in
+  let* (_, self0) =
+    betree_be_tree_apply_back self key (BetreeMessageInsert value) st st1 in
+  Return (st0, self0)
 
 (** [betree_main::betree::BeTree::{6}::delete] *)
 let betree_be_tree_delete_fwd
   (self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) =
-  begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with
-  | Fail e -> Fail e
-  | Return (st0, _) ->
-    begin match betree_be_tree_apply_back self key BetreeMessageDelete st st0
-      with
-    | Fail e -> Fail e
-    | Return (st1, _) -> Return (st1, ())
-    end
-  end
+  let* (st0, _) = betree_be_tree_apply_fwd self key BetreeMessageDelete st in
+  let* (st1, _) = betree_be_tree_apply_back self key BetreeMessageDelete st st0
+    in
+  Return (st1, ())
 
 (** [betree_main::betree::BeTree::{6}::delete] *)
 let betree_be_tree_delete_back
   (self : betree_be_tree_t) (key : u64) (st : state) (st0 : state) :
   result (state & betree_be_tree_t)
   =
-  begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with
-  | Fail e -> Fail e
-  | Return (st1, _) ->
-    begin match betree_be_tree_apply_back self key BetreeMessageDelete st st1
-      with
-    | Fail e -> Fail e
-    | Return (_, self0) -> Return (st0, self0)
-    end
-  end
+  let* (st1, _) = betree_be_tree_apply_fwd self key BetreeMessageDelete st in
+  let* (_, self0) =
+    betree_be_tree_apply_back self key BetreeMessageDelete st st1 in
+  Return (st0, self0)
 
 (** [betree_main::betree::BeTree::{6}::upsert] *)
 let betree_be_tree_upsert_fwd
@@ -1882,16 +1190,11 @@ let betree_be_tree_upsert_fwd
   (st : state) :
   result (state & unit)
   =
-  begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st
-    with
-  | Fail e -> Fail e
-  | Return (st0, _) ->
-    begin match
-      betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st0 with
-    | Fail e -> Fail e
-    | Return (st1, _) -> Return (st1, ())
-    end
-  end
+  let* (st0, _) =
+    betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st in
+  let* (st1, _) =
+    betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st0 in
+  Return (st1, ())
 
 (** [betree_main::betree::BeTree::{6}::upsert] *)
 let betree_be_tree_upsert_back
@@ -1899,16 +1202,11 @@ let betree_be_tree_upsert_back
   (st : state) (st0 : state) :
   result (state & betree_be_tree_t)
   =
-  begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st
-    with
-  | Fail e -> Fail e
-  | Return (st1, _) ->
-    begin match
-      betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st1 with
-    | Fail e -> Fail e
-    | Return (_, self0) -> Return (st0, self0)
-    end
-  end
+  let* (st1, _) =
+    betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st in
+  let* (_, self0) =
+    betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st1 in
+  Return (st0, self0)
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
 let betree_be_tree_lookup_fwd
@@ -1922,12 +1220,10 @@ let betree_be_tree_lookup_back
   (self : betree_be_tree_t) (key : u64) (st : state) (st0 : state) :
   result (state & betree_be_tree_t)
   =
-  begin match betree_node_lookup_back self.betree_be_tree_root key st st0 with
-  | Fail e -> Fail e
-  | Return (st1, n) ->
-    Return (st1, Mkbetree_be_tree_t self.betree_be_tree_params
-      self.betree_be_tree_node_id_cnt n)
-  end
+  let* (st1, n) = betree_node_lookup_back self.betree_be_tree_root key st st0
+    in
+  Return (st1, Mkbetree_be_tree_t self.betree_be_tree_params
+    self.betree_be_tree_node_id_cnt n)
 
 (** [betree_main::main] *)
 let main_fwd : result unit = Return ()
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index bf0f9078..98a696b6 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x
 // let* x = y in
 // ...
 // ```
-unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b =
+unfold let (let*) (#a #b : Type0) (m: result a)
+  (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) :
+  result b =
   match m with
   | Return x -> f x
   | Fail e   -> Fail e