(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [betree_main]: function definitions *)
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
Local Open Scope Primitives_scope.
Require Export BetreeMain_Types.
Import BetreeMain_Types.
Require Export BetreeMain_Opaque.
Import BetreeMain_Opaque.
Module BetreeMain_Funs.

(** [betree_main::betree::load_internal_node] *)
Definition 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] *)
Definition betree_store_internal_node_fwd
  (id : u64) (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
  result (state * unit)
  :=
  p <- betree_utils_store_internal_node_fwd id content st;
  let (st0, _) := p in
  Return (st0, tt)
.

(** [betree_main::betree::load_leaf_node] *)
Definition 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] *)
Definition betree_store_leaf_node_fwd
  (id : u64) (content : Betree_list_t (u64 * u64)) (st : state) :
  result (state * unit)
  :=
  p <- betree_utils_store_leaf_node_fwd id content st;
  let (st0, _) := p in
  Return (st0, tt)
.

(** [betree_main::betree::fresh_node_id] *)
Definition betree_fresh_node_id_fwd (counter : u64) : result u64 :=
  i <- u64_add counter 1%u64; let _ := i in Return counter
.

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

(** [betree_main::betree::NodeIdCounter::{0}::new] *)
Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t :=
  Return (mkBetree_node_id_counter_t (0%u64))
.

(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
Definition betree_node_id_counter_fresh_id_fwd
  (self : Betree_node_id_counter_t) : result u64 :=
  i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
  let _ := i in
  Return self.(Betree_node_id_counter_next_node_id)
.

(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
Definition betree_node_id_counter_fresh_id_back
  (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t :=
  i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
  Return (mkBetree_node_id_counter_t i)
.

(** [core::num::u64::{10}::MAX] *)
Definition core_num_u64_max_body : result u64 :=
  Return (18446744073709551615%u64)
.
Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.

(** [betree_main::betree::upsert_update] *)
Definition betree_upsert_update_fwd
  (prev : option u64) (st : Betree_upsert_fun_state_t) : result u64 :=
  match prev with
  | None =>
    match st with
    | BetreeUpsertFunStateAdd v => Return v
    | BetreeUpsertFunStateSub i => Return (0%u64)
    end
  | Some prev0 =>
    match st with
    | BetreeUpsertFunStateAdd v =>
      margin <- u64_sub core_num_u64_max_c prev0;
      if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c
    | BetreeUpsertFunStateSub v =>
      if prev0 s>= v then u64_sub prev0 v else Return (0%u64)
    end
  end
.

(** [betree_main::betree::List::{1}::len] *)
Fixpoint betree_list_len_fwd
  (T : Type) (n : nat) (self : Betree_list_t T) : result u64 :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match self with
    | BetreeListCons t tl => i <- betree_list_len_fwd T n0 tl; u64_add 1%u64 i
    | BetreeListNil => Return (0%u64)
    end
  end
.

(** [betree_main::betree::List::{1}::split_at] *)
Fixpoint betree_list_split_at_fwd
  (T : Type) (n : nat) (self : Betree_list_t T) (n0 : u64) :
  result ((Betree_list_t T) * (Betree_list_t T))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n1 =>
    if n0 s= 0%u64
    then Return (BetreeListNil, self)
    else
      match self with
      | BetreeListCons hd tl =>
        i <- u64_sub n0 1%u64;
        p <- betree_list_split_at_fwd T n1 tl i;
        let (ls0, ls1) := p in
        let l := ls0 in
        Return (BetreeListCons hd l, ls1)
      | BetreeListNil => Fail_ Failure
      end
  end
.

(** [betree_main::betree::List::{1}::push_front] *)
Definition betree_list_push_front_fwd_back
  (T : Type) (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] *)
Definition betree_list_pop_front_fwd
  (T : Type) (self : Betree_list_t T) : result T :=
  let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in
  match ls with
  | BetreeListCons x tl => Return x
  | BetreeListNil => Fail_ Failure
  end
.

(** [betree_main::betree::List::{1}::pop_front] *)
Definition betree_list_pop_front_back
  (T : Type) (self : Betree_list_t T) : result (Betree_list_t T) :=
  let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in
  match ls with
  | BetreeListCons x tl => Return tl
  | BetreeListNil => Fail_ Failure
  end
.

(** [betree_main::betree::List::{1}::hd] *)
Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T :=
  match self with
  | BetreeListCons hd l => Return hd
  | BetreeListNil => Fail_ Failure
  end
.

(** [betree_main::betree::List::{2}::head_has_key] *)
Definition betree_list_head_has_key_fwd
  (T : Type) (self : Betree_list_t (u64 * T)) (key : u64) : result bool :=
  match self with
  | BetreeListCons hd l => let (i, _) := hd in Return (i s= key)
  | BetreeListNil => Return false
  end
.

(** [betree_main::betree::List::{2}::partition_at_pivot] *)
Fixpoint betree_list_partition_at_pivot_fwd
  (T : Type) (n : nat) (self : Betree_list_t (u64 * T)) (pivot : u64) :
  result ((Betree_list_t (u64 * T)) * (Betree_list_t (u64 * T)))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match self with
    | BetreeListCons hd tl =>
      let (i, t) := hd in
      if i s>= pivot
      then Return (BetreeListNil, BetreeListCons (i, t) tl)
      else (
        p <- betree_list_partition_at_pivot_fwd T n0 tl pivot;
        let (ls0, ls1) := p in
        let l := ls0 in
        Return (BetreeListCons (i, t) l, ls1))
    | BetreeListNil => Return (BetreeListNil, BetreeListNil)
    end
  end
.

(** [betree_main::betree::Leaf::{3}::split] *)
Definition betree_leaf_split_fwd
  (n : nat) (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)
  :=
  p <-
    betree_list_split_at_fwd (u64 * u64) n content
      params.(Betree_params_split_size);
  let (content0, content1) := p in
  p0 <- betree_list_hd_fwd (u64 * u64) content1;
  let (pivot, _) := p0 in
  id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
  node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
  id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
  p1 <- betree_store_leaf_node_fwd id0 content0 st;
  let (st0, _) := p1 in
  p2 <- betree_store_leaf_node_fwd id1 content1 st0;
  let (st1, _) := p2 in
  let n0 := BetreeNodeLeaf (mkBetree_leaf_t id0
    params.(Betree_params_split_size)) in
  let n1 := BetreeNodeLeaf (mkBetree_leaf_t id1
    params.(Betree_params_split_size)) in
  Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n0 n1)
.

(** [betree_main::betree::Leaf::{3}::split] *)
Definition betree_leaf_split_back
  (n : nat) (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 Betree_node_id_counter_t
  :=
  p <-
    betree_list_split_at_fwd (u64 * u64) n content
      params.(Betree_params_split_size);
  let (content0, content1) := p in
  p0 <- betree_list_hd_fwd (u64 * u64) content1;
  let _ := p0 in
  id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
  node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
  id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
  p1 <- betree_store_leaf_node_fwd id0 content0 st;
  let (st0, _) := p1 in
  p2 <- betree_store_leaf_node_fwd id1 content1 st0;
  let (_, _) := p2 in
  betree_node_id_counter_fresh_id_back node_id_cnt0
.

(** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
Fixpoint betree_node_lookup_in_bindings_fwd
  (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
  result (option u64)
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match bindings with
    | BetreeListCons hd tl =>
      let (i, i0) := hd in
      if i s= key
      then Return (Some i0)
      else
        if i s> key
        then Return None
        else betree_node_lookup_in_bindings_fwd n0 key tl
    | BetreeListNil => Return None
    end
  end
.

(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
Fixpoint betree_node_lookup_first_message_for_key_fwd
  (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
  result (Betree_list_t (u64 * Betree_message_t))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match msgs with
    | BetreeListCons x next_msgs =>
      let (i, m) := x in
      if i s>= key
      then Return (BetreeListCons (i, m) next_msgs)
      else betree_node_lookup_first_message_for_key_fwd n0 key next_msgs
    | BetreeListNil => Return BetreeListNil
    end
  end
.

(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
Fixpoint betree_node_lookup_first_message_for_key_back
  (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t))
  (ret : Betree_list_t (u64 * Betree_message_t)) :
  result (Betree_list_t (u64 * Betree_message_t))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match msgs with
    | BetreeListCons x next_msgs =>
      let (i, m) := x in
      if i s>= key
      then Return ret
      else (
        next_msgs0 <-
          betree_node_lookup_first_message_for_key_back n0 key next_msgs ret;
        Return (BetreeListCons (i, m) next_msgs0))
    | BetreeListNil => Return ret
    end
  end
.

(** [betree_main::betree::Node::{5}::apply_upserts] *)
Fixpoint betree_node_apply_upserts_fwd
  (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64)
  (key : u64) (st : state) :
  result (state * u64)
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    b <- betree_list_head_has_key_fwd Betree_message_t msgs key;
    if b
    then (
      msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs;
      let (_, m) := msg in
      match m with
      | BetreeMessageInsert i => Fail_ Failure
      | BetreeMessageDelete => Fail_ Failure
      | BetreeMessageUpsert s =>
        v <- betree_upsert_update_fwd prev s;
        msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs;
        betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st
      end)
    else (
      p <- core_option_option_unwrap_fwd u64 prev st;
      let (st0, v) := p in
      l <-
        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
          BetreeMessageInsert v);
      let _ := l in
      Return (st0, v))
  end
.

(** [betree_main::betree::Node::{5}::apply_upserts] *)
Fixpoint betree_node_apply_upserts_back
  (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64)
  (key : u64) (st : state) :
  result (Betree_list_t (u64 * Betree_message_t))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    b <- betree_list_head_has_key_fwd Betree_message_t msgs key;
    if b
    then (
      msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs;
      let (_, m) := msg in
      match m with
      | BetreeMessageInsert i => Fail_ Failure
      | BetreeMessageDelete => Fail_ Failure
      | BetreeMessageUpsert s =>
        v <- betree_upsert_update_fwd prev s;
        msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs;
        betree_node_apply_upserts_back n0 msgs0 (Some v) key st
      end)
    else (
      p <- core_option_option_unwrap_fwd u64 prev st;
      let (_, v) := p in
      betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
        BetreeMessageInsert v))
  end
.

(** [betree_main::betree::Node::{5}::lookup] *)
Fixpoint betree_node_lookup_fwd
  (n : nat) (self : Betree_node_t) (key : u64) (st : state) :
  result (state * (option u64))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match self with
    | BetreeNodeInternal node =>
      p <- betree_load_internal_node_fwd node.(Betree_internal_id) st;
      let (st0, msgs) := p in
      pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs;
      match pending with
      | BetreeListCons p0 l =>
        let (k, msg) := p0 in
        if k s<> key
        then (
          p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
          let (st1, opt) := p1 in
          l0 <-
            betree_node_lookup_first_message_for_key_back n0 key msgs
              (BetreeListCons (k, msg) l);
          let _ := l0 in
          Return (st1, opt))
        else
          match msg with
          | BetreeMessageInsert v =>
            l0 <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                (BetreeListCons (k, BetreeMessageInsert v) l);
            let _ := l0 in
            Return (st0, Some v)
          | BetreeMessageDelete =>
            l0 <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                (BetreeListCons (k, BetreeMessageDelete) l);
            let _ := l0 in
            Return (st0, None)
          | BetreeMessageUpsert ufs =>
            p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
            let (st1, v) := p1 in
            p2 <-
              betree_node_apply_upserts_fwd n0 (BetreeListCons (k,
                BetreeMessageUpsert ufs) l) v key st1;
            let (st2, v0) := p2 in
            node0 <- betree_internal_lookup_in_children_back n0 node key st0;
            pending0 <-
              betree_node_apply_upserts_back n0 (BetreeListCons (k,
                BetreeMessageUpsert ufs) l) v key st1;
            msgs0 <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                pending0;
            p3 <-
              betree_store_internal_node_fwd node0.(Betree_internal_id) msgs0
                st2;
            let (st3, _) := p3 in
            Return (st3, Some v0)
          end
      | BetreeListNil =>
        p0 <- betree_internal_lookup_in_children_fwd n0 node key st0;
        let (st1, opt) := p0 in
        l <-
          betree_node_lookup_first_message_for_key_back n0 key msgs
            BetreeListNil;
        let _ := l in
        Return (st1, opt)
      end
    | BetreeNodeLeaf node =>
      p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
      let (st0, bindings) := p in
      opt <- betree_node_lookup_in_bindings_fwd n0 key bindings;
      Return (st0, opt)
    end
  end

(** [betree_main::betree::Node::{5}::lookup] *)
with betree_node_lookup_back
  (n : nat) (self : Betree_node_t) (key : u64) (st : state) :
  result Betree_node_t
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match self with
    | BetreeNodeInternal node =>
      p <- betree_load_internal_node_fwd node.(Betree_internal_id) st;
      let (st0, msgs) := p in
      pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs;
      match pending with
      | BetreeListCons p0 l =>
        let (k, msg) := p0 in
        if k s<> key
        then (
          l0 <-
            betree_node_lookup_first_message_for_key_back n0 key msgs
              (BetreeListCons (k, msg) l);
          let _ := l0 in
          node0 <- betree_internal_lookup_in_children_back n0 node key st0;
          Return (BetreeNodeInternal node0))
        else
          match msg with
          | BetreeMessageInsert v =>
            l0 <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                (BetreeListCons (k, BetreeMessageInsert v) l);
            let _ := l0 in
            Return (BetreeNodeInternal node)
          | BetreeMessageDelete =>
            l0 <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                (BetreeListCons (k, BetreeMessageDelete) l);
            let _ := l0 in
            Return (BetreeNodeInternal node)
          | BetreeMessageUpsert ufs =>
            p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
            let (st1, v) := p1 in
            p2 <-
              betree_node_apply_upserts_fwd n0 (BetreeListCons (k,
                BetreeMessageUpsert ufs) l) v key st1;
            let (st2, _) := p2 in
            node0 <- betree_internal_lookup_in_children_back n0 node key st0;
            pending0 <-
              betree_node_apply_upserts_back n0 (BetreeListCons (k,
                BetreeMessageUpsert ufs) l) v key st1;
            msgs0 <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                pending0;
            p3 <-
              betree_store_internal_node_fwd node0.(Betree_internal_id) msgs0
                st2;
            let (_, _) := p3 in
            Return (BetreeNodeInternal node0)
          end
      | BetreeListNil =>
        l <-
          betree_node_lookup_first_message_for_key_back n0 key msgs
            BetreeListNil;
        let _ := l in
        node0 <- betree_internal_lookup_in_children_back n0 node key st0;
        Return (BetreeNodeInternal node0)
      end
    | BetreeNodeLeaf node =>
      p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
      let (_, bindings) := p in
      opt <- betree_node_lookup_in_bindings_fwd n0 key bindings;
      let _ := opt in
      Return (BetreeNodeLeaf node)
    end
  end

(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
with betree_internal_lookup_in_children_fwd
  (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
  result (state * (option u64))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    if key s< self.(Betree_internal_pivot)
    then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st
    else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
  end

(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
with betree_internal_lookup_in_children_back
  (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
  result Betree_internal_t
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    if key s< self.(Betree_internal_pivot)
    then (
      n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st;
      Return (mkBetree_internal_t self.(Betree_internal_id)
        self.(Betree_internal_pivot) n1 self.(Betree_internal_right)))
    else (
      n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st;
      Return (mkBetree_internal_t self.(Betree_internal_id)
        self.(Betree_internal_pivot) self.(Betree_internal_left) n1))
  end
.

(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
Fixpoint betree_node_lookup_mut_in_bindings_fwd
  (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
  result (Betree_list_t (u64 * u64))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match bindings with
    | BetreeListCons hd tl =>
      let (i, i0) := hd in
      if i s>= key
      then Return (BetreeListCons (i, i0) tl)
      else betree_node_lookup_mut_in_bindings_fwd n0 key tl
    | BetreeListNil => Return BetreeListNil
    end
  end
.

(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
Fixpoint betree_node_lookup_mut_in_bindings_back
  (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64))
  (ret : Betree_list_t (u64 * u64)) :
  result (Betree_list_t (u64 * u64))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match bindings with
    | BetreeListCons hd tl =>
      let (i, i0) := hd in
      if i s>= key
      then Return ret
      else (
        tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
        Return (BetreeListCons (i, i0) tl0))
    | BetreeListNil => Return ret
    end
  end
.

(** [betree_main::betree::Node::{5}::apply_to_leaf] *)
Definition betree_node_apply_to_leaf_fwd_back
  (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64)
  (new_msg : Betree_message_t) :
  result (Betree_list_t (u64 * u64))
  :=
  bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings;
  b <- betree_list_head_has_key_fwd u64 bindings0 key;
  if b
  then (
    hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
    match new_msg with
    | BetreeMessageInsert v =>
      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
      bindings2 <-
        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
    | BetreeMessageDelete =>
      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
    | BetreeMessageUpsert s =>
      let (_, i) := hd in
      v <- betree_upsert_update_fwd (Some i) s;
      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
      bindings2 <-
        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
    end)
  else
    match new_msg with
    | BetreeMessageInsert v =>
      bindings1 <-
        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
    | BetreeMessageDelete =>
      betree_node_lookup_mut_in_bindings_back n key bindings bindings0
    | BetreeMessageUpsert s =>
      v <- betree_upsert_update_fwd None s;
      bindings1 <-
        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
    end
.

(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *)
Fixpoint betree_node_apply_messages_to_leaf_fwd_back
  (n : nat) (bindings : Betree_list_t (u64 * u64))
  (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
  result (Betree_list_t (u64 * u64))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match new_msgs with
    | BetreeListCons new_msg new_msgs_tl =>
      let (i, m) := new_msg in
      bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
      betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
    | BetreeListNil => Return bindings
    end
  end
.

(** [betree_main::betree::Node::{5}::filter_messages_for_key] *)
Fixpoint betree_node_filter_messages_for_key_fwd_back
  (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
  result (Betree_list_t (u64 * Betree_message_t))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match msgs with
    | BetreeListCons p l =>
      let (k, m) := p in
      if k s= key
      then (
        msgs0 <-
          betree_list_pop_front_back (u64 * Betree_message_t) (BetreeListCons
            (k, m) l);
        betree_node_filter_messages_for_key_fwd_back n0 key msgs0)
      else Return (BetreeListCons (k, m) l)
    | BetreeListNil => Return BetreeListNil
    end
  end
.

(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
Fixpoint betree_node_lookup_first_message_after_key_fwd
  (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
  result (Betree_list_t (u64 * Betree_message_t))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match msgs with
    | BetreeListCons p next_msgs =>
      let (k, m) := p in
      if k s= key
      then betree_node_lookup_first_message_after_key_fwd n0 key next_msgs
      else Return (BetreeListCons (k, m) next_msgs)
    | BetreeListNil => Return BetreeListNil
    end
  end
.

(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
Fixpoint betree_node_lookup_first_message_after_key_back
  (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t))
  (ret : Betree_list_t (u64 * Betree_message_t)) :
  result (Betree_list_t (u64 * Betree_message_t))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match msgs with
    | BetreeListCons p next_msgs =>
      let (k, m) := p in
      if k s= key
      then (
        next_msgs0 <-
          betree_node_lookup_first_message_after_key_back n0 key next_msgs ret;
        Return (BetreeListCons (k, m) next_msgs0))
      else Return ret
    | BetreeListNil => Return ret
    end
  end
.

(** [betree_main::betree::Node::{5}::apply_to_internal] *)
Definition betree_node_apply_to_internal_fwd_back
  (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (key : u64)
  (new_msg : Betree_message_t) :
  result (Betree_list_t (u64 * Betree_message_t))
  :=
  msgs0 <- betree_node_lookup_first_message_for_key_fwd n key msgs;
  b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key;
  if b
  then
    match new_msg with
    | BetreeMessageInsert i =>
      msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0;
      msgs2 <-
        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
          BetreeMessageInsert i);
      betree_node_lookup_first_message_for_key_back n key msgs msgs2
    | BetreeMessageDelete =>
      msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0;
      msgs2 <-
        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
          BetreeMessageDelete);
      betree_node_lookup_first_message_for_key_back n key msgs msgs2
    | BetreeMessageUpsert s =>
      p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0;
      let (_, m) := p in
      match m with
      | BetreeMessageInsert prev =>
        v <- betree_upsert_update_fwd (Some prev) s;
        msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0;
        msgs2 <-
          betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
            BetreeMessageInsert v);
        betree_node_lookup_first_message_for_key_back n key msgs msgs2
      | BetreeMessageDelete =>
        v <- betree_upsert_update_fwd None s;
        msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0;
        msgs2 <-
          betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
            BetreeMessageInsert v);
        betree_node_lookup_first_message_for_key_back n key msgs msgs2
      | BetreeMessageUpsert ufs =>
        msgs1 <- betree_node_lookup_first_message_after_key_fwd n key msgs0;
        msgs2 <-
          betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
            BetreeMessageUpsert s);
        msgs3 <-
          betree_node_lookup_first_message_after_key_back n key msgs0 msgs2;
        betree_node_lookup_first_message_for_key_back n key msgs msgs3
      end
    end
  else (
    msgs1 <-
      betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key,
        new_msg);
    betree_node_lookup_first_message_for_key_back n key msgs msgs1)
.

(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
Fixpoint betree_node_apply_messages_to_internal_fwd_back
  (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t))
  (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
  result (Betree_list_t (u64 * Betree_message_t))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match new_msgs with
    | BetreeListCons new_msg new_msgs_tl =>
      let (i, m) := new_msg in
      msgs0 <- betree_node_apply_to_internal_fwd_back n0 msgs i m;
      betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl
    | BetreeListNil => Return msgs
    end
  end
.

(** [betree_main::betree::Node::{5}::apply_messages] *)
Fixpoint betree_node_apply_messages_fwd
  (n : nat) (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) :
  result (state * unit)
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match self with
    | BetreeNodeInternal node =>
      p <- betree_load_internal_node_fwd node.(Betree_internal_id) st;
      let (st0, content) := p in
      content0 <-
        betree_node_apply_messages_to_internal_fwd_back n0 content msgs;
      num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0;
      if num_msgs s>= params.(Betree_params_min_flush_size)
      then (
        p0 <-
          betree_internal_flush_fwd n0 node params node_id_cnt content0 st0;
        let (st1, content1) := p0 in
        p1 <-
          betree_internal_flush_back n0 node params node_id_cnt content0 st0;
        let (node0, _) := p1 in
        p2 <-
          betree_store_internal_node_fwd node0.(Betree_internal_id) content1
            st1;
        let (st2, _) := p2 in
        Return (st2, tt))
      else (
        p0 <-
          betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0;
        let (st1, _) := p0 in
        Return (st1, tt))
    | BetreeNodeLeaf node =>
      p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
      let (st0, content) := p in
      content0 <- betree_node_apply_messages_to_leaf_fwd_back n0 content msgs;
      len <- betree_list_len_fwd (u64 * u64) n0 content0;
      i <- u64_mul 2%u64 params.(Betree_params_split_size);
      if len s>= i
      then (
        p0 <- betree_leaf_split_fwd n0 node content0 params node_id_cnt st0;
        let (st1, _) := p0 in
        p1 <-
          betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1;
        let (st2, _) := p1 in
        Return (st2, tt))
      else (
        p0 <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
        let (st1, _) := p0 in
        Return (st1, tt))
    end
  end

(** [betree_main::betree::Node::{5}::apply_messages] *)
with betree_node_apply_messages_back
  (n : nat) (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) :
  result (Betree_node_t * Betree_node_id_counter_t)
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match self with
    | BetreeNodeInternal node =>
      p <- betree_load_internal_node_fwd node.(Betree_internal_id) st;
      let (st0, content) := p in
      content0 <-
        betree_node_apply_messages_to_internal_fwd_back n0 content msgs;
      num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0;
      if num_msgs s>= params.(Betree_params_min_flush_size)
      then (
        p0 <-
          betree_internal_flush_fwd n0 node params node_id_cnt content0 st0;
        let (st1, content1) := p0 in
        p1 <-
          betree_internal_flush_back n0 node params node_id_cnt content0 st0;
        let (node0, node_id_cnt0) := p1 in
        p2 <-
          betree_store_internal_node_fwd node0.(Betree_internal_id) content1
            st1;
        let (_, _) := p2 in
        Return (BetreeNodeInternal node0, node_id_cnt0))
      else (
        p0 <-
          betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0;
        let (_, _) := p0 in
        Return (BetreeNodeInternal node, node_id_cnt))
    | BetreeNodeLeaf node =>
      p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
      let (st0, content) := p in
      content0 <- betree_node_apply_messages_to_leaf_fwd_back n0 content msgs;
      len <- betree_list_len_fwd (u64 * u64) n0 content0;
      i <- u64_mul 2%u64 params.(Betree_params_split_size);
      if len s>= i
      then (
        p0 <- betree_leaf_split_fwd n0 node content0 params node_id_cnt st0;
        let (st1, new_node) := p0 in
        p1 <-
          betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1;
        let (_, _) := p1 in
        node_id_cnt0 <-
          betree_leaf_split_back n0 node content0 params node_id_cnt st0;
        Return (BetreeNodeInternal new_node, node_id_cnt0))
      else (
        p0 <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
        let (_, _) := p0 in
        Return (BetreeNodeLeaf (mkBetree_leaf_t node.(Betree_leaf_id) len),
          node_id_cnt))
    end
  end

(** [betree_main::betree::Internal::{4}::flush] *)
with betree_internal_flush_fwd
  (n : nat) (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) :
  result (state * (Betree_list_t (u64 * Betree_message_t)))
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    p <-
      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
        self.(Betree_internal_pivot);
    let (msgs_left, msgs_right) := p in
    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
    if len_left s>= params.(Betree_params_min_flush_size)
    then (
      p0 <-
        betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
          node_id_cnt msgs_left st;
      let (st0, _) := p0 in
      p1 <-
        betree_node_apply_messages_back n0 self.(Betree_internal_left) params
          node_id_cnt msgs_left st;
      let (_, node_id_cnt0) := p1 in
      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
      if len_right s>= params.(Betree_params_min_flush_size)
      then (
        p2 <-
          betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
            node_id_cnt0 msgs_right st0;
        let (st1, _) := p2 in
        p3 <-
          betree_node_apply_messages_back n0 self.(Betree_internal_right)
            params node_id_cnt0 msgs_right st0;
        let (_, _) := p3 in
        Return (st1, BetreeListNil))
      else Return (st0, msgs_right))
    else (
      p0 <-
        betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
          node_id_cnt msgs_right st;
      let (st0, _) := p0 in
      p1 <-
        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
          node_id_cnt msgs_right st;
      let (_, _) := p1 in
      Return (st0, msgs_left))
  end

(** [betree_main::betree::Internal::{4}::flush] *)
with betree_internal_flush_back
  (n : nat) (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) :
  result (Betree_internal_t * Betree_node_id_counter_t)
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    p <-
      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
        self.(Betree_internal_pivot);
    let (msgs_left, msgs_right) := p in
    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
    if len_left s>= params.(Betree_params_min_flush_size)
    then (
      p0 <-
        betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
          node_id_cnt msgs_left st;
      let (st0, _) := p0 in
      p1 <-
        betree_node_apply_messages_back n0 self.(Betree_internal_left) params
          node_id_cnt msgs_left st;
      let (n1, node_id_cnt0) := p1 in
      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
      if len_right s>= params.(Betree_params_min_flush_size)
      then (
        p2 <-
          betree_node_apply_messages_back n0 self.(Betree_internal_right)
            params node_id_cnt0 msgs_right st0;
        let (n2, node_id_cnt1) := p2 in
        Return (mkBetree_internal_t self.(Betree_internal_id)
          self.(Betree_internal_pivot) n1 n2, node_id_cnt1))
      else
        Return (mkBetree_internal_t self.(Betree_internal_id)
          self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
          node_id_cnt0))
    else (
      p0 <-
        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
          node_id_cnt msgs_right st;
      let (n1, node_id_cnt0) := p0 in
      Return (mkBetree_internal_t self.(Betree_internal_id)
        self.(Betree_internal_pivot) self.(Betree_internal_left) n1,
        node_id_cnt0))
  end
.

(** [betree_main::betree::Node::{5}::apply] *)
Definition betree_node_apply_fwd
  (n : nat) (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
  p <-
    betree_node_apply_messages_fwd n self params node_id_cnt (BetreeListCons
      (key, new_msg) l) st;
  let (st0, _) := p in
  p0 <-
    betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
      (key, new_msg) l) st;
  let (_, _) := p0 in
  Return (st0, tt)
.

(** [betree_main::betree::Node::{5}::apply] *)
Definition betree_node_apply_back
  (n : nat) (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 (Betree_node_t * Betree_node_id_counter_t)
  :=
  let l := BetreeListNil in
  betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
    (key, new_msg) l) st
.

(** [betree_main::betree::BeTree::{6}::new] *)
Definition betree_be_tree_new_fwd
  (min_flush_size : u64) (split_size : u64) (st : state) :
  result (state * Betree_be_tree_t)
  :=
  node_id_cnt <- betree_node_id_counter_new_fwd;
  id <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
  p <- betree_store_leaf_node_fwd id BetreeListNil st;
  let (st0, _) := p in
  node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
  Return (st0, mkBetree_be_tree_t (mkBetree_params_t min_flush_size split_size)
    node_id_cnt0 (BetreeNodeLeaf (mkBetree_leaf_t id (0%u64))))
.

(** [betree_main::betree::BeTree::{6}::apply] *)
Definition betree_be_tree_apply_fwd
  (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t)
  (st : state) :
  result (state * unit)
  :=
  p <-
    betree_node_apply_fwd n self.(Betree_be_tree_root)
      self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
  let (st0, _) := p in
  p0 <-
    betree_node_apply_back n self.(Betree_be_tree_root)
      self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
  let (_, _) := p0 in
  Return (st0, tt)
.

(** [betree_main::betree::BeTree::{6}::apply] *)
Definition betree_be_tree_apply_back
  (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t)
  (st : state) :
  result Betree_be_tree_t
  :=
  p <-
    betree_node_apply_back n self.(Betree_be_tree_root)
      self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
  let (n0, nic) := p in
  Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n0)
.

(** [betree_main::betree::BeTree::{6}::insert] *)
Definition betree_be_tree_insert_fwd
  (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) :
  result (state * unit)
  :=
  p <- betree_be_tree_apply_fwd n self key (BetreeMessageInsert value) st;
  let (st0, _) := p in
  bt <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st;
  let _ := bt in
  Return (st0, tt)
.

(** [betree_main::betree::BeTree::{6}::insert] *)
Definition betree_be_tree_insert_back
  (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) :
  result Betree_be_tree_t
  :=
  betree_be_tree_apply_back n self key (BetreeMessageInsert value) st
.

(** [betree_main::betree::BeTree::{6}::delete] *)
Definition betree_be_tree_delete_fwd
  (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
  result (state * unit)
  :=
  p <- betree_be_tree_apply_fwd n self key BetreeMessageDelete st;
  let (st0, _) := p in
  bt <- betree_be_tree_apply_back n self key BetreeMessageDelete st;
  let _ := bt in
  Return (st0, tt)
.

(** [betree_main::betree::BeTree::{6}::delete] *)
Definition betree_be_tree_delete_back
  (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
  result Betree_be_tree_t
  :=
  betree_be_tree_apply_back n self key BetreeMessageDelete st
.

(** [betree_main::betree::BeTree::{6}::upsert] *)
Definition betree_be_tree_upsert_fwd
  (n : nat) (self : Betree_be_tree_t) (key : u64)
  (upd : Betree_upsert_fun_state_t) (st : state) :
  result (state * unit)
  :=
  p <- betree_be_tree_apply_fwd n self key (BetreeMessageUpsert upd) st;
  let (st0, _) := p in
  bt <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st;
  let _ := bt in
  Return (st0, tt)
.

(** [betree_main::betree::BeTree::{6}::upsert] *)
Definition betree_be_tree_upsert_back
  (n : nat) (self : Betree_be_tree_t) (key : u64)
  (upd : Betree_upsert_fun_state_t) (st : state) :
  result Betree_be_tree_t
  :=
  betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st
.

(** [betree_main::betree::BeTree::{6}::lookup] *)
Definition betree_be_tree_lookup_fwd
  (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
  result (state * (option u64))
  :=
  betree_node_lookup_fwd n self.(Betree_be_tree_root) key st
.

(** [betree_main::betree::BeTree::{6}::lookup] *)
Definition betree_be_tree_lookup_back
  (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) :
  result Betree_be_tree_t
  :=
  n0 <- betree_node_lookup_back n self.(Betree_be_tree_root) key st;
  Return (mkBetree_be_tree_t self.(Betree_be_tree_params)
    self.(Betree_be_tree_node_id_cnt) n0)
.

(** [betree_main::main] *)
Definition main_fwd : result unit := Return tt.

End BetreeMain_Funs .