Change the name of the generated Coq modules

1 files changed, 0 insertions, 1397 deletions

diff --git a/tests/coq/betree/BetreeMain__Funs.v b/tests/coq/betree/BetreeMain__Funs.v
deleted file mode 100644
index 3ce86f6b..00000000
--- a/tests/coq/betree/BetreeMain__Funs.v
+++ /dev/null
@@ -1,1397 +0,0 @@
-(** 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)))
-  :=
-  p <- betree_utils_load_internal_node_fwd id st;
-  let (st0, l) := p in
-  Return (st0, l)
-.
-
-(** [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))) :=
-  p <- betree_utils_load_leaf_node_fwd id st;
-  let (st0, l) := p in
-  Return (st0, l)
-.
-
-(** [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 :=
-  counter0 <- u64_add counter 1%u64; Return counter0
-.
-
-(** [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 :=
-  match self with
-  | mkBetree_node_id_counter_t id =>
-    i <- u64_add id 1%u64; let _ := i in Return id
-  end
-.
-
-(** [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 :=
-  match self with
-  | mkBetree_node_id_counter_t id =>
-    i <- u64_add id 1%u64; Return (mkBetree_node_id_counter_t i)
-  end
-.
-
-(** [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 (i <- u64_add prev0 v; Return i)
-      else Return core_num_u64_max_c
-    | BetreeUpsertFunStateSub v =>
-      if prev0 s>= v then (i <- u64_sub prev0 v; Return i) 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; i0 <- u64_add 1%u64 i; Return i0
-    | 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)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match params with
-    | mkBetree_params_t i i0 =>
-      p <- betree_list_split_at_fwd (u64 * u64) n0 content i0;
-      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
-      match self with
-      | mkBetree_leaf_t i1 i2 =>
-        let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0 i0) in
-        let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1 i0) in
-        Return (st1, mkBetree_internal_t i1 pivot n1 n2)
-      end
-    end
-  end
-.
-
-(** [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
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match params with
-    | mkBetree_params_t i i0 =>
-      p <- betree_list_split_at_fwd (u64 * u64) n0 content i0;
-      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
-      match self with
-      | mkBetree_leaf_t i1 i2 =>
-        node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0;
-        Return node_id_cnt1
-      end
-    end
-  end
-.
-
-(** [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 (opt <- betree_node_lookup_in_bindings_fwd n0 key tl; Return opt)
-    | 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 (
-        l <- betree_node_lookup_first_message_for_key_fwd n0 key next_msgs;
-        Return l)
-    | 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;
-        p <- betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st;
-        let (st0, i) := p in
-        Return (st0, i)
-      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;
-        msgs1 <- betree_node_apply_upserts_back n0 msgs0 (Some v) key st;
-        Return msgs1
-      end)
-    else (
-      p <- core_option_option_unwrap_fwd u64 prev st;
-      let (_, v) := p in
-      msgs0 <-
-        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key,
-          BetreeMessageInsert v);
-      Return msgs0)
-  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 =>
-      match node with
-      | mkBetree_internal_t i i0 n1 n2 =>
-        p <- betree_load_internal_node_fwd i 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 (mkBetree_internal_t i
-                i0 n1 n2) 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 (mkBetree_internal_t
-                  i i0 n1 n2) 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 (mkBetree_internal_t
-                  i i0 n1 n2) key st0;
-              match node0 with
-              | mkBetree_internal_t i1 i2 n3 n4 =>
-                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 i1 msgs0 st2;
-                let (st3, _) := p3 in
-                Return (st3, Some v0)
-              end
-            end
-        | BetreeListNil =>
-          p0 <-
-            betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i i0
-              n1 n2) 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
-      end
-    | BetreeNodeLeaf node =>
-      match node with
-      | mkBetree_leaf_t i i0 =>
-        p <- betree_load_leaf_node_fwd i st;
-        let (st0, bindings) := p in
-        opt <- betree_node_lookup_in_bindings_fwd n0 key bindings;
-        Return (st0, opt)
-      end
-    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 =>
-      match node with
-      | mkBetree_internal_t i i0 n1 n2 =>
-        p <- betree_load_internal_node_fwd i 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 (mkBetree_internal_t i
-                i0 n1 n2) 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 (mkBetree_internal_t i i0 n1 n2))
-            | BetreeMessageDelete =>
-              l0 <-
-                betree_node_lookup_first_message_for_key_back n0 key msgs
-                  (BetreeListCons (k, BetreeMessageDelete) l);
-              let _ := l0 in
-              Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2))
-            | BetreeMessageUpsert ufs =>
-              p1 <-
-                betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t
-                  i i0 n1 n2) 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 (mkBetree_internal_t
-                  i i0 n1 n2) key st0;
-              match node0 with
-              | mkBetree_internal_t i1 i2 n3 n4 =>
-                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 i1 msgs0 st2;
-                let (_, _) := p3 in
-                Return (BetreeNodeInternal (mkBetree_internal_t i1 i2 n3 n4))
-              end
-            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 (mkBetree_internal_t i
-              i0 n1 n2) key st0;
-          Return (BetreeNodeInternal node0)
-        end
-      end
-    | BetreeNodeLeaf node =>
-      match node with
-      | mkBetree_leaf_t i i0 =>
-        p <- betree_load_leaf_node_fwd i st;
-        let (_, bindings) := p in
-        opt <- betree_node_lookup_in_bindings_fwd n0 key bindings;
-        let _ := opt in
-        Return (BetreeNodeLeaf (mkBetree_leaf_t i i0))
-      end
-    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 =>
-    match self with
-    | mkBetree_internal_t i i0 n1 n2 =>
-      if key s< i0
-      then (
-        p <- betree_node_lookup_fwd n0 n1 key st;
-        let (st0, opt) := p in
-        Return (st0, opt))
-      else (
-        p <- betree_node_lookup_fwd n0 n2 key st;
-        let (st0, opt) := p in
-        Return (st0, opt))
-    end
-  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 =>
-    match self with
-    | mkBetree_internal_t i i0 n1 n2 =>
-      if key s< i0
-      then (
-        n3 <- betree_node_lookup_back n0 n1 key st;
-        Return (mkBetree_internal_t i i0 n3 n2))
-      else (
-        n3 <- betree_node_lookup_back n0 n2 key st;
-        Return (mkBetree_internal_t i i0 n1 n3))
-    end
-  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 (l <- betree_node_lookup_mut_in_bindings_fwd n0 key tl; Return l)
-    | 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))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    bindings0 <- betree_node_lookup_mut_in_bindings_fwd n0 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);
-        bindings3 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2;
-        Return bindings3
-      | BetreeMessageDelete =>
-        bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-        bindings2 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1;
-        Return bindings2
-      | 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);
-        bindings3 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2;
-        Return bindings3
-      end)
-    else
-      match new_msg with
-      | BetreeMessageInsert v =>
-        bindings1 <-
-          betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
-        bindings2 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1;
-        Return bindings2
-      | BetreeMessageDelete =>
-        bindings1 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings0;
-        Return bindings1
-      | BetreeMessageUpsert s =>
-        v <- betree_upsert_update_fwd None s;
-        bindings1 <-
-          betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
-        bindings2 <-
-          betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1;
-        Return bindings2
-      end
-  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;
-      bindings1 <-
-        betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl;
-      Return bindings1
-    | 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);
-        msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0;
-        Return msgs1)
-      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 (
-        l <- betree_node_lookup_first_message_after_key_fwd n0 key next_msgs;
-        Return l)
-      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))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    msgs0 <- betree_node_lookup_first_message_for_key_fwd n0 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 n0 key msgs0;
-        msgs2 <-
-          betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
-            BetreeMessageInsert i);
-        msgs3 <-
-          betree_node_lookup_first_message_for_key_back n0 key msgs msgs2;
-        Return msgs3
-      | BetreeMessageDelete =>
-        msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0;
-        msgs2 <-
-          betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key,
-            BetreeMessageDelete);
-        msgs3 <-
-          betree_node_lookup_first_message_for_key_back n0 key msgs msgs2;
-        Return msgs3
-      | 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);
-          msgs3 <-
-            betree_node_lookup_first_message_for_key_back n0 key msgs msgs2;
-          Return msgs3
-        | 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);
-          msgs3 <-
-            betree_node_lookup_first_message_for_key_back n0 key msgs msgs2;
-          Return msgs3
-        | BetreeMessageUpsert ufs =>
-          msgs1 <- betree_node_lookup_first_message_after_key_fwd n0 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 n0 key msgs0 msgs2;
-          msgs4 <-
-            betree_node_lookup_first_message_for_key_back n0 key msgs msgs3;
-          Return msgs4
-        end
-      end
-    else (
-      msgs1 <-
-        betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key,
-          new_msg);
-      msgs2 <- betree_node_lookup_first_message_for_key_back n0 key msgs msgs1;
-      Return msgs2)
-  end
-.
-
-(** [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;
-      msgs1 <-
-        betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl;
-      Return msgs1
-    | 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 =>
-      match node with
-      | mkBetree_internal_t i i0 n1 n2 =>
-        p <- betree_load_internal_node_fwd i 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;
-        match params with
-        | mkBetree_params_t i1 i2 =>
-          if num_msgs s>= i1
-          then (
-            p0 <-
-              betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2)
-                (mkBetree_params_t i1 i2) node_id_cnt content0 st0;
-            let (st1, content1) := p0 in
-            p1 <-
-              betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2)
-                (mkBetree_params_t i1 i2) node_id_cnt content0 st0;
-            let (node0, _) := p1 in
-            match node0 with
-            | mkBetree_internal_t i3 i4 n3 n4 =>
-              p2 <- betree_store_internal_node_fwd i3 content1 st1;
-              let (st2, _) := p2 in
-              Return (st2, tt)
-            end)
-          else (
-            p0 <- betree_store_internal_node_fwd i content0 st0;
-            let (st1, _) := p0 in
-            Return (st1, tt))
-        end
-      end
-    | BetreeNodeLeaf node =>
-      match node with
-      | mkBetree_leaf_t i i0 =>
-        p <- betree_load_leaf_node_fwd i 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;
-        match params with
-        | mkBetree_params_t i1 i2 =>
-          i3 <- u64_mul 2%u64 i2;
-          if len s>= i3
-          then (
-            p0 <-
-              betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0
-                (mkBetree_params_t i1 i2) node_id_cnt st0;
-            let (st1, _) := p0 in
-            p1 <- betree_store_leaf_node_fwd i BetreeListNil st1;
-            let (st2, _) := p1 in
-            Return (st2, tt))
-          else (
-            p0 <- betree_store_leaf_node_fwd i content0 st0;
-            let (st1, _) := p0 in
-            Return (st1, tt))
-        end
-      end
-    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 =>
-      match node with
-      | mkBetree_internal_t i i0 n1 n2 =>
-        p <- betree_load_internal_node_fwd i 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;
-        match params with
-        | mkBetree_params_t i1 i2 =>
-          if num_msgs s>= i1
-          then (
-            p0 <-
-              betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2)
-                (mkBetree_params_t i1 i2) node_id_cnt content0 st0;
-            let (st1, content1) := p0 in
-            p1 <-
-              betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2)
-                (mkBetree_params_t i1 i2) node_id_cnt content0 st0;
-            let (node0, node_id_cnt0) := p1 in
-            match node0 with
-            | mkBetree_internal_t i3 i4 n3 n4 =>
-              p2 <- betree_store_internal_node_fwd i3 content1 st1;
-              let (_, _) := p2 in
-              Return (BetreeNodeInternal (mkBetree_internal_t i3 i4 n3 n4),
-                node_id_cnt0)
-            end)
-          else (
-            p0 <- betree_store_internal_node_fwd i content0 st0;
-            let (_, _) := p0 in
-            Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2),
-              node_id_cnt))
-        end
-      end
-    | BetreeNodeLeaf node =>
-      match node with
-      | mkBetree_leaf_t i i0 =>
-        p <- betree_load_leaf_node_fwd i 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;
-        match params with
-        | mkBetree_params_t i1 i2 =>
-          i3 <- u64_mul 2%u64 i2;
-          if len s>= i3
-          then (
-            p0 <-
-              betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0
-                (mkBetree_params_t i1 i2) node_id_cnt st0;
-            let (st1, new_node) := p0 in
-            p1 <- betree_store_leaf_node_fwd i BetreeListNil st1;
-            let (_, _) := p1 in
-            node_id_cnt0 <-
-              betree_leaf_split_back n0 (mkBetree_leaf_t i i0) content0
-                (mkBetree_params_t i1 i2) node_id_cnt st0;
-            Return (BetreeNodeInternal new_node, node_id_cnt0))
-          else (
-            p0 <- betree_store_leaf_node_fwd i content0 st0;
-            let (_, _) := p0 in
-            Return (BetreeNodeLeaf (mkBetree_leaf_t i len), node_id_cnt))
-        end
-      end
-    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 =>
-    match self with
-    | mkBetree_internal_t i i0 n1 n2 =>
-      p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0;
-      let (msgs_left, msgs_right) := p in
-      len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
-      match params with
-      | mkBetree_params_t i1 i2 =>
-        if len_left s>= i1
-        then (
-          p0 <-
-            betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2)
-              node_id_cnt msgs_left st;
-          let (st0, _) := p0 in
-          p1 <-
-            betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2)
-              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>= i1
-          then (
-            p2 <-
-              betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2)
-                node_id_cnt0 msgs_right st0;
-            let (st1, _) := p2 in
-            p3 <-
-              betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2)
-                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 n2 (mkBetree_params_t i1 i2)
-              node_id_cnt msgs_right st;
-          let (st0, _) := p0 in
-          p1 <-
-            betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2)
-              node_id_cnt msgs_right st;
-          let (_, _) := p1 in
-          Return (st0, msgs_left))
-      end
-    end
-  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 =>
-    match self with
-    | mkBetree_internal_t i i0 n1 n2 =>
-      p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0;
-      let (msgs_left, msgs_right) := p in
-      len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
-      match params with
-      | mkBetree_params_t i1 i2 =>
-        if len_left s>= i1
-        then (
-          p0 <-
-            betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2)
-              node_id_cnt msgs_left st;
-          let (st0, _) := p0 in
-          p1 <-
-            betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2)
-              node_id_cnt msgs_left st;
-          let (n3, node_id_cnt0) := p1 in
-          len_right <-
-            betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
-          if len_right s>= i1
-          then (
-            p2 <-
-              betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2)
-                node_id_cnt0 msgs_right st0;
-            let (n4, node_id_cnt1) := p2 in
-            Return (mkBetree_internal_t i i0 n3 n4, node_id_cnt1))
-          else Return (mkBetree_internal_t i i0 n3 n2, node_id_cnt0))
-        else (
-          p0 <-
-            betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2)
-              node_id_cnt msgs_right st;
-          let (n3, node_id_cnt0) := p0 in
-          Return (mkBetree_internal_t i i0 n1 n3, node_id_cnt0))
-      end
-    end
-  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)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let l := BetreeListNil in
-    p <-
-      betree_node_apply_messages_fwd n0 self params node_id_cnt (BetreeListCons
-        (key, new_msg) l) st;
-    let (st0, _) := p in
-    p0 <-
-      betree_node_apply_messages_back n0 self params node_id_cnt
-        (BetreeListCons (key, new_msg) l) st;
-    let (_, _) := p0 in
-    Return (st0, tt)
-  end
-.
-
-(** [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)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let l := BetreeListNil in
-    p <-
-      betree_node_apply_messages_back n0 self params node_id_cnt
-        (BetreeListCons (key, new_msg) l) st;
-    let (self0, node_id_cnt0) := p in
-    Return (self0, node_id_cnt0)
-  end
-.
-
-(** [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)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match self with
-    | mkBetree_be_tree_t p nic n1 =>
-      p0 <- betree_node_apply_fwd n0 n1 p nic key msg st;
-      let (st0, _) := p0 in
-      p1 <- betree_node_apply_back n0 n1 p nic key msg st;
-      let (_, _) := p1 in
-      Return (st0, tt)
-    end
-  end
-.
-
-(** [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
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match self with
-    | mkBetree_be_tree_t p nic n1 =>
-      p0 <- betree_node_apply_back n0 n1 p nic key msg st;
-      let (n2, nic0) := p0 in
-      Return (mkBetree_be_tree_t p nic0 n2)
-    end
-  end
-.
-
-(** [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)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageInsert value) st;
-    let (st0, _) := p in
-    bt <- betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st;
-    let _ := bt in
-    Return (st0, tt)
-  end
-.
-
-(** [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
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <-
-      betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st;
-    Return self0
-  end
-.
-
-(** [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)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- betree_be_tree_apply_fwd n0 self key BetreeMessageDelete st;
-    let (st0, _) := p in
-    bt <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st;
-    let _ := bt in
-    Return (st0, tt)
-  end
-.
-
-(** [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
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st;
-    Return self0
-  end
-.
-
-(** [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)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageUpsert upd) st;
-    let (st0, _) := p in
-    bt <- betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st;
-    let _ := bt in
-    Return (st0, tt)
-  end
-.
-
-(** [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
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <-
-      betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st;
-    Return self0
-  end
-.
-
-(** [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))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match self with
-    | mkBetree_be_tree_t p nic n1 =>
-      p0 <- betree_node_lookup_fwd n0 n1 key st;
-      let (st0, opt) := p0 in
-      Return (st0, opt)
-    end
-  end
-.
-
-(** [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
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match self with
-    | mkBetree_be_tree_t p nic n1 =>
-      n2 <- betree_node_lookup_back n0 n1 key st;
-      Return (mkBetree_be_tree_t p nic n2)
-    end
-  end
-.
-
-(** [betree_main::main] *)
-Definition main_fwd : result unit := Return tt.
-
-End BetreeMain__Funs .