(** 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]: forward function *)
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]: forward function *)
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]: forward function *)
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]: forward function *)
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]: forward function *)
Definition betree_fresh_node_id_fwd (counter : u64) : result u64 :=
  _ <- u64_add counter 1%u64; Return counter
.

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

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

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

(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
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 {| Betree_node_id_counter_next_node_id := 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]: forward function *)
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]: forward function *)
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]: forward function *)
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]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) *)
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]: forward function *)
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]: backward function 0 *)
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]: forward function *)
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]: forward function *)
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]: forward function *)
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]: forward function *)
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
    {|
      Betree_leaf_id := id0;
      Betree_leaf_size := params.(Betree_params_split_size)
    |} in
  let n1 := BetreeNodeLeaf
    {|
      Betree_leaf_id := id1;
      Betree_leaf_size := params.(Betree_params_split_size)
    |} in
  Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n0 n1)
.

(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *)
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
  _ <- betree_list_hd_fwd (u64 * u64) content1;
  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;
  p0 <- betree_store_leaf_node_fwd id0 content0 st;
  let (st0, _) := p0 in
  _ <- betree_store_leaf_node_fwd id1 content1 st0;
  betree_node_id_counter_fresh_id_back node_id_cnt0
.

(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
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]: forward function *)
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]: backward function 0 *)
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]: forward function *)
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
      _ <-
        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
          BetreeMessageInsert v);
      Return (st0, v))
  end
.

(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *)
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]: forward function *)
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
          _ <-
            betree_node_lookup_first_message_for_key_back n0 key msgs
              (BetreeListCons (k, msg) l);
          Return (st1, opt))
        else
          match msg with
          | BetreeMessageInsert v =>
            _ <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                (BetreeListCons (k, BetreeMessageInsert v) l);
            Return (st0, Some v)
          | BetreeMessageDelete =>
            _ <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                (BetreeListCons (k, BetreeMessageDelete) l);
            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
        _ <-
          betree_node_lookup_first_message_for_key_back n0 key msgs
            BetreeListNil;
        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]: backward function 0 *)
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 (
          _ <-
            betree_node_lookup_first_message_for_key_back n0 key msgs
              (BetreeListCons (k, msg) l);
          node0 <- betree_internal_lookup_in_children_back n0 node key st0;
          Return (BetreeNodeInternal node0))
        else
          match msg with
          | BetreeMessageInsert v =>
            _ <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                (BetreeListCons (k, BetreeMessageInsert v) l);
            Return (BetreeNodeInternal node)
          | BetreeMessageDelete =>
            _ <-
              betree_node_lookup_first_message_for_key_back n0 key msgs
                (BetreeListCons (k, BetreeMessageDelete) l);
            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;
            _ <-
              betree_store_internal_node_fwd node0.(Betree_internal_id) msgs0
                st2;
            Return (BetreeNodeInternal node0)
          end
      | BetreeListNil =>
        _ <-
          betree_node_lookup_first_message_for_key_back n0 key msgs
            BetreeListNil;
        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
      _ <- betree_node_lookup_in_bindings_fwd n0 key bindings;
      Return (BetreeNodeLeaf node)
    end
  end

(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
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]: backward function 0 *)
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]: forward function *)
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]: backward function 0 *)
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]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) *)
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]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) *)
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]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) *)
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]: forward function *)
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]: backward function 0 *)
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]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) *)
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]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) *)
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]: forward function *)
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]: backward function 0 *)
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
        _ <-
          betree_store_internal_node_fwd node0.(Betree_internal_id) content1
            st1;
        Return (BetreeNodeInternal node0, node_id_cnt0))
      else (
        _ <-
          betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0;
        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
        _ <-
          betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1;
        node_id_cnt0 <-
          betree_leaf_split_back n0 node content0 params node_id_cnt st0;
        Return (BetreeNodeInternal new_node, node_id_cnt0))
      else (
        _ <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
        Return (BetreeNodeLeaf
          {| Betree_leaf_id := node.(Betree_leaf_id); Betree_leaf_size := len
          |}, node_id_cnt))
    end
  end

(** [betree_main::betree::Internal::{4}::flush]: forward function *)
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
        _ <-
          betree_node_apply_messages_back n0 self.(Betree_internal_right)
            params node_id_cnt0 msgs_right st0;
        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
      _ <-
        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
          node_id_cnt msgs_right st;
      Return (st0, msgs_left))
  end

(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
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]: forward function *)
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
  _ <-
    betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons
      (key, new_msg) l) st;
  Return (st0, tt)
.

(** [betree_main::betree::Node::{5}::apply]: backward function 0 *)
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]: forward function *)
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,
    {|
      Betree_be_tree_params :=
        {|
          Betree_params_min_flush_size := min_flush_size;
          Betree_params_split_size := split_size
        |};
      Betree_be_tree_node_id_cnt := node_id_cnt0;
      Betree_be_tree_root :=
        (BetreeNodeLeaf {| Betree_leaf_id := id; Betree_leaf_size := 0%u64 |})
    |})
.

(** [betree_main::betree::BeTree::{6}::apply]: forward function *)
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
  _ <-
    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;
  Return (st0, tt)
.

(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *)
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
    {|
      Betree_be_tree_params := self.(Betree_be_tree_params);
      Betree_be_tree_node_id_cnt := nic;
      Betree_be_tree_root := n0
    |}
.

(** [betree_main::betree::BeTree::{6}::insert]: forward function *)
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
  _ <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st;
  Return (st0, tt)
.

(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *)
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]: forward function *)
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
  _ <- betree_be_tree_apply_back n self key BetreeMessageDelete st;
  Return (st0, tt)
.

(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *)
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]: forward function *)
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
  _ <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st;
  Return (st0, tt)
.

(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *)
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]: forward function *)
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]: backward function 0 *)
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
    {|
      Betree_be_tree_params := self.(Betree_be_tree_params);
      Betree_be_tree_node_id_cnt := self.(Betree_be_tree_node_id_cnt);
      Betree_be_tree_root := n0
    |}
.

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

End BetreeMain_Funs .