(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [betree_main]: function definitions *)
module BetreeMain.Funs
open Primitives
include BetreeMain.Types
include BetreeMain.Opaque
include BetreeMain.Clauses

#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** [betree_main::betree::load_internal_node] *)
let betree_load_internal_node_fwd
  (id : u64) (st : state) :
  result (state & (betree_list_t (u64 & betree_message_t)))
  =
  betree_utils_load_internal_node_fwd id st

(** [betree_main::betree::store_internal_node] *)
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

(** [betree_main::betree::load_leaf_node] *)
let betree_load_leaf_node_fwd
  (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) =
  betree_utils_load_leaf_node_fwd id st

(** [betree_main::betree::store_leaf_node] *)
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

(** [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

(** [betree_main::betree::fresh_node_id] *)
let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1

(** [betree_main::betree::NodeIdCounter::{0}::new] *)
let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
  Return (Mkbetree_node_id_counter_t 0)

(** [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

(** [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

(** [core::num::u64::{10}::MAX] *)
let core_num_u64_max_body : result u64 = Return 18446744073709551615
let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body

(** [betree_main::betree::upsert_update] *)
let betree_upsert_update_fwd
  (prev : option u64) (st : betree_upsert_fun_state_t) : result u64 =
  begin match prev with
  | None ->
    begin match st with
    | BetreeUpsertFunStateAdd v -> Return v
    | BetreeUpsertFunStateSub i -> Return 0
    end
  | 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
    | BetreeUpsertFunStateSub v ->
      if prev0 >= v then u64_sub prev0 v else Return 0
    end
  end

(** [betree_main::betree::List::{1}::len] *)
let rec betree_list_len_fwd
  (t : Type0) (self : betree_list_t t) :
  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
  | BetreeListNil -> Return 0
  end

(** [betree_main::betree::List::{1}::split_at] *)
let rec betree_list_split_at_fwd
  (t : Type0) (self : betree_list_t t) (n : u64) :
  Tot (result ((betree_list_t t) & (betree_list_t t)))
  (decreases (betree_list_split_at_decreases t self n))
  =
  if n = 0
  then Return (BetreeListNil, self)
  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
    | BetreeListNil -> Fail Failure
    end

(** [betree_main::betree::List::{1}::push_front] *)
let betree_list_push_front_fwd_back
  (t : Type0) (self : betree_list_t t) (x : t) : result (betree_list_t t) =
  let tl = mem_replace_fwd (betree_list_t t) self BetreeListNil in
  let l = tl in
  Return (BetreeListCons x l)

(** [betree_main::betree::List::{1}::pop_front] *)
let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t =
  let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
  begin match ls with
  | BetreeListCons x tl -> Return x
  | BetreeListNil -> Fail Failure
  end

(** [betree_main::betree::List::{1}::pop_front] *)
let betree_list_pop_front_back
  (t : Type0) (self : betree_list_t t) : result (betree_list_t t) =
  let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
  begin match ls with
  | BetreeListCons x tl -> Return tl
  | BetreeListNil -> Fail Failure
  end

(** [betree_main::betree::List::{1}::hd] *)
let betree_list_hd_fwd (t : Type0) (self : betree_list_t t) : result t =
  begin match self with
  | BetreeListCons hd l -> Return hd
  | BetreeListNil -> Fail Failure
  end

(** [betree_main::betree::List::{2}::head_has_key] *)
let betree_list_head_has_key_fwd
  (t : Type0) (self : betree_list_t (u64 & t)) (key : u64) : result bool =
  begin match self with
  | BetreeListCons hd l -> let (i, _) = hd in Return (i = key)
  | BetreeListNil -> Return false
  end

(** [betree_main::betree::List::{2}::partition_at_pivot] *)
let rec betree_list_partition_at_pivot_fwd
  (t : Type0) (self : betree_list_t (u64 & t)) (pivot : u64) :
  Tot (result ((betree_list_t (u64 & t)) & (betree_list_t (u64 & t))))
  (decreases (betree_list_partition_at_pivot_decreases t self pivot))
  =
  begin match self with
  | BetreeListCons hd tl ->
    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
  | BetreeListNil -> Return (BetreeListNil, BetreeListNil)
  end

(** [betree_main::betree::Leaf::{3}::split] *)
let betree_leaf_split_fwd
  (self : betree_leaf_t) (content : betree_list_t (u64 & u64))
  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
  (st : state) :
  result (state & betree_internal_t)
  =
  begin match
    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

(** [betree_main::betree::Leaf::{3}::split] *)
let betree_leaf_split_back0
  (self : betree_leaf_t) (content : betree_list_t (u64 & u64))
  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
  (st : state) (st0 : state) :
  result (state & unit)
  =
  begin match
    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

(** [betree_main::betree::Leaf::{3}::split] *)
let betree_leaf_split_back1
  (self : betree_leaf_t) (content : betree_list_t (u64 & u64))
  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
  (st : state) (st0 : state) :
  result (state & unit)
  =
  begin match
    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

(** [betree_main::betree::Leaf::{3}::split] *)
let betree_leaf_split_back2
  (self : betree_leaf_t) (content : betree_list_t (u64 & u64))
  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
  (st : state) (st0 : state) :
  result (state & betree_node_id_counter_t)
  =
  begin match
    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

(** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
let rec betree_node_lookup_in_bindings_fwd
  (key : u64) (bindings : betree_list_t (u64 & u64)) :
  Tot (result (option u64))
  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
  =
  begin match bindings with
  | BetreeListCons hd tl ->
    let (i, i0) = hd in
    if i = key
    then Return (Some i0)
    else
      if i > key
      then Return None
      else betree_node_lookup_in_bindings_fwd key tl
  | BetreeListNil -> Return None
  end

(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
let rec betree_node_lookup_first_message_for_key_fwd
  (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_for_key_decreases key msgs))
  =
  begin match msgs with
  | BetreeListCons x next_msgs ->
    let (i, m) = x in
    if i >= key
    then Return (BetreeListCons (i, m) next_msgs)
    else betree_node_lookup_first_message_for_key_fwd key next_msgs
  | BetreeListNil -> Return BetreeListNil
  end

(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
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
  | BetreeListCons x next_msgs ->
    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
  | BetreeListNil -> Return ret
  end

(** [betree_main::betree::Node::{5}::apply_upserts] *)
let rec betree_node_apply_upserts_fwd
  (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))
  =
  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

(** [betree_main::betree::Node::{5}::apply_upserts] *)
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))))
  (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

(** [betree_main::betree::Node::{5}::lookup] *)
let rec betree_node_lookup_fwd
  (self : betree_node_t) (key : u64) (st : state) :
  Tot (result (state & (option u64)))
  (decreases (betree_node_lookup_decreases self key st))
  =
  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
        end
      end
    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
  end

(** [betree_main::betree::Node::{5}::lookup] *)
and betree_node_lookup_back
  (self : betree_node_t) (key : u64) (st : state) (st0 : state) :
  Tot (result (state & betree_node_t))
  (decreases (betree_node_lookup_decreases self key st))
  =
  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
            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
        end
      end
    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
  end

(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
and betree_internal_lookup_in_children_fwd
  (self : betree_internal_t) (key : u64) (st : state) :
  Tot (result (state & (option u64)))
  (decreases (betree_internal_lookup_in_children_decreases self key st))
  =
  if key < self.betree_internal_pivot
  then betree_node_lookup_fwd self.betree_internal_left key st
  else betree_node_lookup_fwd self.betree_internal_right key st

(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
and betree_internal_lookup_in_children_back
  (self : betree_internal_t) (key : u64) (st : state) (st0 : state) :
  Tot (result (state & betree_internal_t))
  (decreases (betree_internal_lookup_in_children_decreases self key st))
  =
  if key < self.betree_internal_pivot
  then
    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

(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
let rec betree_node_lookup_mut_in_bindings_fwd
  (key : u64) (bindings : betree_list_t (u64 & u64)) :
  Tot (result (betree_list_t (u64 & u64)))
  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
  =
  begin match bindings with
  | BetreeListCons hd tl ->
    let (i, i0) = hd in
    if i >= key
    then Return (BetreeListCons (i, i0) tl)
    else betree_node_lookup_mut_in_bindings_fwd key tl
  | BetreeListNil -> Return BetreeListNil
  end

(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
let rec betree_node_lookup_mut_in_bindings_back
  (key : u64) (bindings : betree_list_t (u64 & u64))
  (ret : betree_list_t (u64 & u64)) :
  Tot (result (betree_list_t (u64 & u64)))
  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
  =
  begin match bindings with
  | BetreeListCons hd tl ->
    let (i, i0) = hd in
    if i >= key
    then Return ret
    else
      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
  | BetreeListNil -> Return ret
  end

(** [betree_main::betree::Node::{5}::apply_to_leaf] *)
let betree_node_apply_to_leaf_fwd_back
  (bindings : betree_list_t (u64 & u64)) (key : u64)
  (new_msg : betree_message_t) :
  result (betree_list_t (u64 & u64))
  =
  begin match 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
    end
  end

(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *)
let rec betree_node_apply_messages_to_leaf_fwd_back
  (bindings : betree_list_t (u64 & u64))
  (new_msgs : betree_list_t (u64 & betree_message_t)) :
  Tot (result (betree_list_t (u64 & u64)))
  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
  =
  begin match new_msgs with
  | BetreeListCons new_msg new_msgs_tl ->
    let (i, m) = new_msg in
    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
  | BetreeListNil -> Return bindings
  end

(** [betree_main::betree::Node::{5}::filter_messages_for_key] *)
let rec betree_node_filter_messages_for_key_fwd_back
  (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
  Tot (result (betree_list_t (u64 & betree_message_t)))
  (decreases (betree_node_filter_messages_for_key_decreases key msgs))
  =
  begin match msgs with
  | BetreeListCons p l ->
    let (k, m) = p in
    if k = key
    then
      begin match
        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
    else Return (BetreeListCons (k, m) l)
  | BetreeListNil -> Return BetreeListNil
  end

(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
let rec betree_node_lookup_first_message_after_key_fwd
  (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
  | BetreeListCons p next_msgs ->
    let (k, m) = p in
    if k = key
    then betree_node_lookup_first_message_after_key_fwd key next_msgs
    else Return (BetreeListCons (k, m) next_msgs)
  | BetreeListNil -> Return BetreeListNil
  end

(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
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)))
  (decreases (betree_node_lookup_first_message_after_key_decreases key msgs))
  =
  begin match msgs with
  | 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
    else Return ret
  | BetreeListNil -> Return ret
  end

(** [betree_main::betree::Node::{5}::apply_to_internal] *)
let betree_node_apply_to_internal_fwd_back
  (msgs : betree_list_t (u64 & betree_message_t)) (key : u64)
  (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
    end
  end

(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
let rec betree_node_apply_messages_to_internal_fwd_back
  (msgs : betree_list_t (u64 & betree_message_t))
  (new_msgs : betree_list_t (u64 & betree_message_t)) :
  Tot (result (betree_list_t (u64 & betree_message_t)))
  (decreases (betree_node_apply_messages_to_internal_decreases msgs new_msgs))
  =
  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
  | BetreeListNil -> Return msgs
  end

(** [betree_main::betree::Node::{5}::apply_messages] *)
let rec betree_node_apply_messages_fwd
  (self : betree_node_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t)
  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
  Tot (result (state & unit))
  (decreases (
    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
  =
  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
  | 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
  end

(** [betree_main::betree::Node::{5}::apply_messages] *)
and betree_node_apply_messages_back'a
  (self : betree_node_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t)
  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
  Tot (result (state & (betree_node_t & betree_node_id_counter_t)))
  (decreases (
    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
  =
  begin match self with
  | BetreeNodeInternal node ->
    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
  | 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
  end

(** [betree_main::betree::Node::{5}::apply_messages] *)
and betree_node_apply_messages_back1
  (self : betree_node_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t)
  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
  Tot (result (state & unit))
  (decreases (
    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
  =
  begin match self with
  | BetreeNodeInternal node ->
    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
  | 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
  end

(** [betree_main::betree::Internal::{4}::flush] *)
and betree_internal_flush_fwd
  (self : betree_internal_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t)
  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
  Tot (result (state & (betree_list_t (u64 & betree_message_t))))
  (decreases (
    betree_internal_flush_decreases self params node_id_cnt content st))
  =
  begin match
    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

(** [betree_main::betree::Internal::{4}::flush] *)
and betree_internal_flush_back'a
  (self : betree_internal_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t)
  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state)
  :
  Tot (result (state & (betree_internal_t & betree_node_id_counter_t)))
  (decreases (
    betree_internal_flush_decreases self params node_id_cnt content st))
  =
  begin match
    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
    end
  end

(** [betree_main::betree::Internal::{4}::flush] *)
and betree_internal_flush_back1
  (self : betree_internal_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t)
  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state)
  :
  Tot (result (state & unit))
  (decreases (
    betree_internal_flush_decreases self params node_id_cnt content st))
  =
  begin match
    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

(** [betree_main::betree::Node::{5}::apply] *)
let betree_node_apply_fwd
  (self : betree_node_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t) (key : u64)
  (new_msg : betree_message_t) (st : state) :
  result (state & unit)
  =
  let l = BetreeListNil in
  begin match
    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

(** [betree_main::betree::Node::{5}::apply] *)
let betree_node_apply_back'a
  (self : betree_node_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t) (key : u64)
  (new_msg : betree_message_t) (st : state) (st0 : state) :
  result (state & (betree_node_t & betree_node_id_counter_t))
  =
  let l = BetreeListNil in
  begin match
    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

(** [betree_main::betree::Node::{5}::apply] *)
let betree_node_apply_back1
  (self : betree_node_t) (params : betree_params_t)
  (node_id_cnt : betree_node_id_counter_t) (key : u64)
  (new_msg : betree_message_t) (st : state) (st0 : state) :
  result (state & unit)
  =
  let l = BetreeListNil in
  begin match
    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

(** [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

(** [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
    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

(** [betree_main::betree::BeTree::{6}::apply] *)
let betree_be_tree_apply_back
  (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state)
  (st0 : state) :
  result (state & betree_be_tree_t)
  =
  begin match
    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

(** [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

(** [betree_main::betree::BeTree::{6}::insert] *)
let betree_be_tree_insert_back
  (self : betree_be_tree_t) (key : u64) (value : u64) (st : state)
  (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

(** [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

(** [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

(** [betree_main::betree::BeTree::{6}::upsert] *)
let betree_be_tree_upsert_fwd
  (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t)
  (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

(** [betree_main::betree::BeTree::{6}::upsert] *)
let betree_be_tree_upsert_back
  (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t)
  (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

(** [betree_main::betree::BeTree::{6}::lookup] *)
let betree_be_tree_lookup_fwd
  (self : betree_be_tree_t) (key : u64) (st : state) :
  result (state & (option u64))
  =
  betree_node_lookup_fwd self.betree_be_tree_root key st

(** [betree_main::betree::BeTree::{6}::lookup] *)
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

(** [betree_main::main] *)
let main_fwd : result unit = Return ()

(** Unit test for [betree_main::main] *)
let _ = assert_norm (main_fwd = Return ())