Reorganize the project to prepare for new backends

7 files changed, 0 insertions, 2398 deletions

diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst
deleted file mode 100644
index d48213d3..00000000
--- a/tests/betree/BetreeMain.Clauses.Template.fst
+++ /dev/null
@@ -1,106 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: templates for the decreases clauses *)
-module BetreeMain.Clauses.Template
-open Primitives
-open BetreeMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::num::u64::{10}::MAX] *)
-let core_num_u64_max_body : result u64 = Return 18446744073709551615
-let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
-
-(** [betree_main::betree::List::{1}::len]: decreases clause *)
-unfold
-let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : nat =
-  admit ()
-
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
-unfold
-let betree_list_split_at_decreases (t : Type0) (self : betree_list_t t)
-  (n : u64) : nat =
-  admit ()
-
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
-unfold
-let betree_list_partition_at_pivot_decreases (t : Type0)
-  (self : betree_list_t (u64 & t)) (pivot : u64) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
-unfold
-let betree_node_lookup_first_message_for_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
-unfold
-let betree_node_apply_upserts_decreases
-  (msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
-  (key : u64) (st : state) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
-unfold
-let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
-  (st : state) : nat =
-  admit ()
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
-unfold
-let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
-  (key : u64) (st : state) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_mut_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
-unfold
-let betree_node_apply_messages_to_leaf_decreases
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
-unfold
-let betree_node_filter_messages_for_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
-unfold
-let betree_node_lookup_first_message_after_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases clause *)
-unfold
-let betree_node_apply_messages_to_internal_decreases
-  (msgs : betree_list_t (u64 & betree_message_t))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
-unfold
-let betree_node_apply_messages_decreases (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) : nat =
-  admit ()
-
-(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
-unfold
-let betree_internal_flush_decreases (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) : nat =
-  admit ()
-
diff --git a/tests/betree/BetreeMain.Clauses.fst b/tests/betree/BetreeMain.Clauses.fst
deleted file mode 100644
index 07484711..00000000
--- a/tests/betree/BetreeMain.Clauses.fst
+++ /dev/null
@@ -1,210 +0,0 @@
-(** [betree_main]: templates for the decreases clauses *)
-module BetreeMain.Clauses
-open Primitives
-open BetreeMain.Types
-
-#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
-
-(*** Well-founded relations *)
-
-(* We had a few issues when proving termination of the mutually recursive functions:
- * - betree_internal_flush
- * - betree_node_apply_messages
- *
- * The quantity which effectively decreases is:
- *   (betree_size, messages_length)
- *   where messages_length is 0 when there are no messages
- *   (and where we use the lexicographic ordering, of course)
- *
- * However, the `%[...]` and `{:well-founded ...} notations are not available outside
- * of `decrease` clauses.
- * 
- * We thus resorted to writing and proving correct a well-founded relation over
- * pairs of natural numbers. The trick is that `<<` can be used outside of decrease
- * clauses, and can be used to trigger SMT patterns.
- *
- * What follows is adapted from:
- * https://www.fstar-lang.org/tutorial/book/part2/part2_well_founded.html
- *
- * Also, the following PR might make things easier:
- * https://github.com/FStarLang/FStar/pull/2561
- *)
-
-module P = FStar.Preorder
-module W = FStar.WellFounded
-module L = FStar.LexicographicOrdering
-
-let lt_nat (x y:nat) : Type = x < y == true
-let rec wf_lt_nat (x:nat)
-  : W.acc lt_nat x
-  = W.AccIntro (fun y _ -> wf_lt_nat y)
-
-// A type abbreviation for a pair of nats
-let nat_pair = (x:nat & nat)
-
-// Making a lexicographic ordering from a pair of nat ordering
-let lex_order_nat_pair  : P.relation nat_pair =
-  L.lex_t lt_nat (fun _ -> lt_nat)
-
-// The lex order on nat pairs is well-founded, using our general proof
-// of lexicographic composition of well-founded orders
-let lex_order_nat_pair_wf : W.well_founded lex_order_nat_pair =
-  L.lex_t_wf wf_lt_nat (fun _ -> wf_lt_nat)
-
-// A utility to introduce lt_nat
-let mk_lt_nat (x:nat) (y:nat { x < y }) : lt_nat x y =
-  let _ : equals (x < y) true = Refl in
-  ()
-    
-// A utility to make a lex ordering of nat pairs
-let mk_lex_order_nat_pair (xy0:nat_pair) 
-                          (xy1:nat_pair {
-                            let (|x0, y0|) = xy0 in
-                            let (|x1, y1|) = xy1 in
-                            x0 < x1 \/ (x0 == x1 /\ y0 < y1)
-                          }) : lex_order_nat_pair xy0 xy1 =
-  let (|x0, y0|) = xy0 in
-  let (|x1, y1|) = xy1 in
-  if x0 < x1 then L.Left_lex x0 x1 y0 y1 (mk_lt_nat x0 x1)
-  else L.Right_lex x0 y0 y1 (mk_lt_nat y0 y1)
-
-let rec coerce #a #r #x (p:W.acc #a r x) : Tot (W.acc r x) (decreases p) =
-  W.AccIntro (fun y r -> coerce (p.access_smaller y r))
-
-let coerce_wf #a #r (p: (x:a -> W.acc r x)) : x:a -> W.acc r x =
-  fun x -> coerce (p x)
-
-(* We need this axiom, which comes from the following discussion:
- * https://github.com/FStarLang/FStar/issues/1916
- * An issue here is that the `{well-founded ... }` notation
- *)
-assume
-val axiom_well_founded (a : Type) (rel : a -> a -> Type0)
-  (rwf : W.well_founded #a rel) (x y : a) :
-  Lemma (requires (rel x y)) (ensures (x << y))
-
-(* This lemma has a pattern (which makes it work) *)
-let wf_nat_pair_lem (p0 p1 : nat_pair) :
-  Lemma
-  (requires (
-    let (|x0, y0|) = p0 in
-    let (|x1, y1|) = p1 in
-    x0 < x1 || (x0 = x1 && y0 < y1)))
-  (ensures (p0 << p1))
-  [SMTPat (p0 << p1)] =
-  let rel = lex_order_nat_pair in
-  let rel_wf = lex_order_nat_pair_wf in
-  let _ = mk_lex_order_nat_pair p0 p1 in
-  assert(rel p0 p1);
-  axiom_well_founded nat_pair rel rel_wf p0 p1
-
-(*** Decrease clauses *)
-/// "Standard" decrease clauses
-
-(** [betree_main::betree::List::{1}::len]: decreases clause *)
-unfold
-let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : betree_list_t t =
-  self
-
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
-unfold
-let betree_list_split_at_decreases (t : Type0) (self : betree_list_t t)
-  (n : u64) : nat =
-  n
-
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
-unfold
-let betree_list_partition_at_pivot_decreases (t : Type0)
-  (self : betree_list_t (u64 & t)) (pivot : u64) : betree_list_t (u64 & t) =
-  self
-
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : betree_list_t (u64 & u64) =
-  bindings
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
-unfold
-let betree_node_lookup_first_message_for_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
-  msgs
-
-(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
-unfold
-let betree_node_apply_upserts_decreases
-  (msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
-  (key : u64) (st : state) : betree_list_t (u64 & betree_message_t) =
-  msgs
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
-unfold
-let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
-  (key : u64) (st : state) : betree_internal_t =
-  self
-
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
-unfold
-let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
-  (st : state) : betree_node_t =
-  self
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_mut_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : betree_list_t (u64 & u64) =
-  bindings
-
-unfold
-let betree_node_apply_messages_to_leaf_decreases
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
-  new_msgs
-
-(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
-unfold
-let betree_node_filter_messages_for_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
-  msgs
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
-unfold
-let betree_node_lookup_first_message_after_key_decreases (key : u64)
-  (msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
-  msgs
-
-let betree_node_apply_messages_to_internal_decreases
-  (msgs : betree_list_t (u64 & betree_message_t))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
-  new_msgs
-
-(*** Decrease clauses - nat_pair *)
-/// The following decrease clauses use the [nat_pair] definition and the well-founded
-/// relation proven above.
-
-let rec betree_size (bt : betree_node_t) : nat =
-  match bt with
-  | BetreeNodeInternal node -> 1 + betree_internal_size node
-  | BetreeNodeLeaf _ -> 1
-
-and betree_internal_size (node : betree_internal_t) : nat =
-  1 + betree_size node.betree_internal_left + betree_size node.betree_internal_right
-
-let rec betree_list_len (#a : Type0) (ls : betree_list_t a) : nat =
-  match ls with
-  | BetreeListCons _ tl -> 1 + betree_list_len tl
-  | BetreeListNil -> 0
-
-(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
-unfold
-let betree_internal_flush_decreases (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) : nat_pair =
-  (|betree_internal_size self, 0|)
-
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
-unfold
-let betree_node_apply_messages_decreases (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) : nat_pair =
-  (|betree_size self, betree_list_len msgs|)
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
deleted file mode 100644
index 9ba5d3e7..00000000
--- a/tests/betree/BetreeMain.Funs.fst
+++ /dev/null
@@ -1,1654 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: function definitions *)
-module BetreeMain.Funs
-open Primitives
-include BetreeMain.Types
-include BetreeMain.Opaque
-include BetreeMain.Clauses
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree::load_internal_node] *)
-let betree_load_internal_node_fwd
-  (id : u64) (st : state) :
-  result (state & (betree_list_t (u64 & betree_message_t)))
-  =
-  begin match betree_utils_load_internal_node_fwd id st with
-  | Fail -> Fail
-  | Return (st0, l) -> Return (st0, l)
-  end
-
-(** [betree_main::betree::store_internal_node] *)
-let betree_store_internal_node_fwd
-  (id : u64) (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  result (state & unit)
-  =
-  begin match betree_utils_store_internal_node_fwd id content st with
-  | Fail -> Fail
-  | Return (st0, _) -> Return (st0, ())
-  end
-
-(** [betree_main::betree::load_leaf_node] *)
-let betree_load_leaf_node_fwd
-  (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) =
-  begin match betree_utils_load_leaf_node_fwd id st with
-  | Fail -> Fail
-  | Return (st0, l) -> Return (st0, l)
-  end
-
-(** [betree_main::betree::store_leaf_node] *)
-let betree_store_leaf_node_fwd
-  (id : u64) (content : betree_list_t (u64 & u64)) (st : state) :
-  result (state & unit)
-  =
-  begin match betree_utils_store_leaf_node_fwd id content st with
-  | Fail -> Fail
-  | Return (st0, _) -> Return (st0, ())
-  end
-
-(** [betree_main::betree::fresh_node_id] *)
-let betree_fresh_node_id_fwd (counter : u64) : result u64 =
-  begin match u64_add counter 1 with
-  | Fail -> Fail
-  | Return _ -> Return counter
-  end
-
-(** [betree_main::betree::fresh_node_id] *)
-let betree_fresh_node_id_back (counter : u64) : result u64 =
-  begin match u64_add counter 1 with
-  | Fail -> Fail
-  | Return counter0 -> Return counter0
-  end
-
-(** [betree_main::betree::NodeIdCounter::{0}::new] *)
-let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
-  Return (Mkbetree_node_id_counter_t 0)
-
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
-let betree_node_id_counter_fresh_id_fwd
-  (self : betree_node_id_counter_t) : result u64 =
-  begin match u64_add self.betree_node_id_counter_next_node_id 1 with
-  | Fail -> Fail
-  | Return _ -> Return self.betree_node_id_counter_next_node_id
-  end
-
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
-let betree_node_id_counter_fresh_id_back
-  (self : betree_node_id_counter_t) : result betree_node_id_counter_t =
-  begin match u64_add self.betree_node_id_counter_next_node_id 1 with
-  | Fail -> Fail
-  | Return i -> Return (Mkbetree_node_id_counter_t i)
-  end
-
-(** [core::num::u64::{10}::MAX] *)
-let core_num_u64_max_body : result u64 = Return 18446744073709551615
-let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
-
-(** [betree_main::betree::upsert_update] *)
-let betree_upsert_update_fwd
-  (prev : option u64) (st : betree_upsert_fun_state_t) : result u64 =
-  begin match prev with
-  | None ->
-    begin match st with
-    | BetreeUpsertFunStateAdd v -> Return v
-    | BetreeUpsertFunStateSub i -> Return 0
-    end
-  | Some prev0 ->
-    begin match st with
-    | BetreeUpsertFunStateAdd v ->
-      begin match u64_sub core_num_u64_max_c prev0 with
-      | Fail -> Fail
-      | Return margin ->
-        if margin >= v
-        then
-          begin match u64_add prev0 v with
-          | Fail -> Fail
-          | Return i -> Return i
-          end
-        else Return core_num_u64_max_c
-      end
-    | BetreeUpsertFunStateSub v ->
-      if prev0 >= v
-      then
-        begin match u64_sub prev0 v with
-        | Fail -> Fail
-        | Return i -> Return i
-        end
-      else Return 0
-    end
-  end
-
-(** [betree_main::betree::List::{1}::len] *)
-let rec betree_list_len_fwd
-  (t : Type0) (self : betree_list_t t) :
-  Tot (result u64) (decreases (betree_list_len_decreases t self))
-  =
-  begin match self with
-  | BetreeListCons x tl ->
-    begin match betree_list_len_fwd t tl with
-    | Fail -> Fail
-    | Return i ->
-      begin match u64_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
-    end
-  | BetreeListNil -> Return 0
-  end
-
-(** [betree_main::betree::List::{1}::split_at] *)
-let rec betree_list_split_at_fwd
-  (t : Type0) (self : betree_list_t t) (n : u64) :
-  Tot (result ((betree_list_t t) & (betree_list_t t)))
-  (decreases (betree_list_split_at_decreases t self n))
-  =
-  if n = 0
-  then Return (BetreeListNil, self)
-  else
-    begin match self with
-    | BetreeListCons hd tl ->
-      begin match u64_sub n 1 with
-      | Fail -> Fail
-      | Return i ->
-        begin match betree_list_split_at_fwd t tl i with
-        | Fail -> Fail
-        | Return p ->
-          let (ls0, ls1) = p in
-          let l = ls0 in Return (BetreeListCons hd l, ls1)
-        end
-      end
-    | BetreeListNil -> Fail
-    end
-
-(** [betree_main::betree::List::{1}::push_front] *)
-let betree_list_push_front_fwd_back
-  (t : Type0) (self : betree_list_t t) (x : t) : result (betree_list_t t) =
-  let tl = mem_replace_fwd (betree_list_t t) self BetreeListNil in
-  let l = tl in Return (BetreeListCons x l)
-
-(** [betree_main::betree::List::{1}::pop_front] *)
-let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t =
-  let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
-  begin match ls with
-  | BetreeListCons x tl -> Return x
-  | BetreeListNil -> Fail
-  end
-
-(** [betree_main::betree::List::{1}::pop_front] *)
-let betree_list_pop_front_back
-  (t : Type0) (self : betree_list_t t) : result (betree_list_t t) =
-  let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
-  begin match ls with
-  | BetreeListCons x tl -> Return tl
-  | BetreeListNil -> Fail
-  end
-
-(** [betree_main::betree::List::{1}::hd] *)
-let betree_list_hd_fwd (t : Type0) (self : betree_list_t t) : result t =
-  begin match self with
-  | BetreeListCons hd l -> Return hd
-  | BetreeListNil -> Fail
-  end
-
-(** [betree_main::betree::List::{2}::head_has_key] *)
-let betree_list_head_has_key_fwd
-  (t : Type0) (self : betree_list_t (u64 & t)) (key : u64) : result bool =
-  begin match self with
-  | BetreeListCons hd l -> let (i, _) = hd in Return (i = key)
-  | BetreeListNil -> Return false
-  end
-
-(** [betree_main::betree::List::{2}::partition_at_pivot] *)
-let rec betree_list_partition_at_pivot_fwd
-  (t : Type0) (self : betree_list_t (u64 & t)) (pivot : u64) :
-  Tot (result ((betree_list_t (u64 & t)) & (betree_list_t (u64 & t))))
-  (decreases (betree_list_partition_at_pivot_decreases t self pivot))
-  =
-  begin match self with
-  | BetreeListCons hd tl ->
-    let (i, x) = hd in
-    if i >= pivot
-    then Return (BetreeListNil, BetreeListCons (i, x) tl)
-    else
-      begin match betree_list_partition_at_pivot_fwd t tl pivot with
-      | Fail -> Fail
-      | Return p ->
-        let (ls0, ls1) = p in
-        let l = ls0 in Return (BetreeListCons (i, x) l, ls1)
-      end
-  | BetreeListNil -> Return (BetreeListNil, BetreeListNil)
-  end
-
-(** [betree_main::betree::Leaf::{3}::split] *)
-let betree_leaf_split_fwd
-  (self : betree_leaf_t) (content : betree_list_t (u64 & u64))
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (st : state) :
-  result (state & betree_internal_t)
-  =
-  begin match
-    betree_list_split_at_fwd (u64 & u64) content
-      params.betree_params_split_size with
-  | Fail -> Fail
-  | Return p ->
-    let (content0, content1) = p in
-    begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail -> Fail
-    | Return p0 ->
-      let (pivot, _) = p0 in
-      begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail -> Fail
-      | Return id0 ->
-        begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
-        | Return node_id_cnt0 ->
-          begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail -> Fail
-          | Return id1 ->
-            begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail -> Fail
-            | Return (st0, _) ->
-              begin match betree_store_leaf_node_fwd id1 content1 st0 with
-              | Fail -> Fail
-              | Return (st1, _) ->
-                let n = BetreeNodeLeaf (Mkbetree_leaf_t id0
-                  params.betree_params_split_size) in
-                let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1
-                  params.betree_params_split_size) in
-                Return
-                (st1,
-                Mkbetree_internal_t
-                self.betree_leaf_id
-                pivot
-                n
-                n0)
-              end
-            end
-          end
-        end
-      end
-    end
-  end
-
-(** [betree_main::betree::Leaf::{3}::split] *)
-let betree_leaf_split_back
-  (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
-  =
-  begin match
-    betree_list_split_at_fwd (u64 & u64) content
-      params.betree_params_split_size with
-  | Fail -> Fail
-  | Return p ->
-    let (content0, content1) = p in
-    begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail -> Fail
-    | Return _ ->
-      begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail -> Fail
-      | Return id0 ->
-        begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
-        | Return node_id_cnt0 ->
-          begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail -> Fail
-          | Return id1 ->
-            begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail -> Fail
-            | Return (st0, _) ->
-              begin match betree_store_leaf_node_fwd id1 content1 st0 with
-              | Fail -> Fail
-              | Return (_, _) ->
-                begin match betree_node_id_counter_fresh_id_back node_id_cnt0
-                  with
-                | Fail -> Fail
-                | Return node_id_cnt1 -> Return node_id_cnt1
-                end
-              end
-            end
-          end
-        end
-      end
-    end
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
-let rec betree_node_lookup_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (option u64))
-  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i = key
-    then Return (Some i0)
-    else
-      if i > key
-      then Return None
-      else
-        begin match betree_node_lookup_in_bindings_fwd key tl with
-        | Fail -> Fail
-        | Return opt -> Return opt
-        end
-  | BetreeListNil -> Return None
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
-let rec betree_node_lookup_first_message_for_key_fwd
-  (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & betree_message_t)))
-  (decreases (betree_node_lookup_first_message_for_key_decreases key msgs))
-  =
-  begin match msgs with
-  | BetreeListCons x next_msgs ->
-    let (i, m) = x in
-    if i >= key
-    then Return (BetreeListCons (i, m) next_msgs)
-    else
-      begin match betree_node_lookup_first_message_for_key_fwd key next_msgs
-        with
-      | Fail -> Fail
-      | Return l -> Return l
-      end
-  | BetreeListNil -> Return BetreeListNil
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
-let rec betree_node_lookup_first_message_for_key_back
-  (key : u64) (msgs : betree_list_t (u64 & betree_message_t))
-  (ret : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & betree_message_t)))
-  (decreases (betree_node_lookup_first_message_for_key_decreases key msgs))
-  =
-  begin match msgs with
-  | BetreeListCons x next_msgs ->
-    let (i, m) = x in
-    if i >= key
-    then Return ret
-    else
-      begin match
-        betree_node_lookup_first_message_for_key_back key next_msgs ret with
-      | Fail -> Fail
-      | Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0)
-      end
-  | BetreeListNil -> Return ret
-  end
-
-(** [betree_main::betree::Node::{5}::apply_upserts] *)
-let rec betree_node_apply_upserts_fwd
-  (msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
-  (key : u64) (st : state) :
-  Tot (result (state & u64))
-  (decreases (betree_node_apply_upserts_decreases msgs prev key st))
-  =
-  begin match betree_list_head_has_key_fwd betree_message_t msgs key with
-  | Fail -> Fail
-  | Return b ->
-    if b
-    then
-      begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
-      | Fail -> Fail
-      | Return msg ->
-        let (_, m) = msg in
-        begin match m with
-        | BetreeMessageInsert i -> Fail
-        | BetreeMessageDelete -> Fail
-        | BetreeMessageUpsert s ->
-          begin match betree_upsert_update_fwd prev s with
-          | Fail -> Fail
-          | Return v ->
-            begin match
-              betree_list_pop_front_back (u64 & betree_message_t) msgs with
-            | Fail -> Fail
-            | Return msgs0 ->
-              begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st
-                with
-              | Fail -> Fail
-              | Return (st0, i) -> Return (st0, i)
-              end
-            end
-          end
-        end
-      end
-    else
-      begin match core_option_option_unwrap_fwd u64 prev st with
-      | Fail -> Fail
-      | Return (st0, v) ->
-        begin match
-          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
-            BetreeMessageInsert v) with
-        | Fail -> Fail
-        | Return _ -> Return (st0, v)
-        end
-      end
-  end
-
-(** [betree_main::betree::Node::{5}::apply_upserts] *)
-let rec betree_node_apply_upserts_back
-  (msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
-  (key : u64) (st : state) :
-  Tot (result (betree_list_t (u64 & betree_message_t)))
-  (decreases (betree_node_apply_upserts_decreases msgs prev key st))
-  =
-  begin match betree_list_head_has_key_fwd betree_message_t msgs key with
-  | Fail -> Fail
-  | Return b ->
-    if b
-    then
-      begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
-      | Fail -> Fail
-      | Return msg ->
-        let (_, m) = msg in
-        begin match m with
-        | BetreeMessageInsert i -> Fail
-        | BetreeMessageDelete -> Fail
-        | BetreeMessageUpsert s ->
-          begin match betree_upsert_update_fwd prev s with
-          | Fail -> Fail
-          | Return v ->
-            begin match
-              betree_list_pop_front_back (u64 & betree_message_t) msgs with
-            | Fail -> Fail
-            | Return msgs0 ->
-              begin match betree_node_apply_upserts_back msgs0 (Some v) key st
-                with
-              | Fail -> Fail
-              | Return msgs1 -> Return msgs1
-              end
-            end
-          end
-        end
-      end
-    else
-      begin match core_option_option_unwrap_fwd u64 prev st with
-      | Fail -> Fail
-      | Return (_, v) ->
-        begin match
-          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
-            BetreeMessageInsert v) with
-        | Fail -> Fail
-        | Return msgs0 -> Return msgs0
-        end
-      end
-  end
-
-(** [betree_main::betree::Node::{5}::lookup] *)
-let rec betree_node_lookup_fwd
-  (self : betree_node_t) (key : u64) (st : state) :
-  Tot (result (state & (option u64)))
-  (decreases (betree_node_lookup_decreases self key st))
-  =
-  begin match self with
-  | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
-    | Return (st0, msgs) ->
-      begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-      | Fail -> Fail
-      | Return pending ->
-        begin match pending with
-        | BetreeListCons p l ->
-          let (k, msg) = p in
-          if k <> key
-          then
-            begin match betree_internal_lookup_in_children_fwd node key st0
-              with
-            | Fail -> Fail
-            | Return (st1, opt) ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, msg) l) with
-              | Fail -> Fail
-              | Return _ -> Return (st1, opt)
-              end
-            end
-          else
-            begin match msg with
-            | BetreeMessageInsert v ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, BetreeMessageInsert v) l) with
-              | Fail -> Fail
-              | Return _ -> Return (st0, Some v)
-              end
-            | BetreeMessageDelete ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, BetreeMessageDelete) l) with
-              | Fail -> Fail
-              | Return _ -> Return (st0, None)
-              end
-            | BetreeMessageUpsert ufs ->
-              begin match betree_internal_lookup_in_children_fwd node key st0
-                with
-              | Fail -> Fail
-              | Return (st1, v) ->
-                begin match
-                  betree_node_apply_upserts_fwd (BetreeListCons (k,
-                    BetreeMessageUpsert ufs) l) v key st1 with
-                | Fail -> Fail
-                | Return (st2, v0) ->
-                  begin match
-                    betree_internal_lookup_in_children_back node key st0 with
-                  | Fail -> Fail
-                  | Return node0 ->
-                    begin match
-                      betree_node_apply_upserts_back (BetreeListCons (k,
-                        BetreeMessageUpsert ufs) l) v key st1 with
-                    | Fail -> Fail
-                    | Return pending0 ->
-                      begin match
-                        betree_node_lookup_first_message_for_key_back key msgs
-                          pending0 with
-                      | Fail -> Fail
-                      | Return msgs0 ->
-                        begin match
-                          betree_store_internal_node_fwd
-                            node0.betree_internal_id msgs0 st2 with
-                        | Fail -> Fail
-                        | Return (st3, _) -> Return (st3, Some v0)
-                        end
-                      end
-                    end
-                  end
-                end
-              end
-            end
-        | BetreeListNil ->
-          begin match betree_internal_lookup_in_children_fwd node key st0 with
-          | Fail -> Fail
-          | Return (st1, opt) ->
-            begin match
-              betree_node_lookup_first_message_for_key_back key msgs
-                BetreeListNil with
-            | Fail -> Fail
-            | Return _ -> Return (st1, opt)
-            end
-          end
-        end
-      end
-    end
-  | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
-    | Return (st0, bindings) ->
-      begin match betree_node_lookup_in_bindings_fwd key bindings with
-      | Fail -> Fail
-      | Return opt -> Return (st0, opt)
-      end
-    end
-  end
-
-(** [betree_main::betree::Node::{5}::lookup] *)
-and betree_node_lookup_back
-  (self : betree_node_t) (key : u64) (st : state) :
-  Tot (result betree_node_t)
-  (decreases (betree_node_lookup_decreases self key st))
-  =
-  begin match self with
-  | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
-    | Return (st0, msgs) ->
-      begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-      | Fail -> Fail
-      | Return pending ->
-        begin match pending with
-        | BetreeListCons p l ->
-          let (k, msg) = p in
-          if k <> key
-          then
-            begin match
-              betree_node_lookup_first_message_for_key_back key msgs
-                (BetreeListCons (k, msg) l) with
-            | Fail -> Fail
-            | Return _ ->
-              begin match betree_internal_lookup_in_children_back node key st0
-                with
-              | Fail -> Fail
-              | Return node0 -> Return (BetreeNodeInternal node0)
-              end
-            end
-          else
-            begin match msg with
-            | BetreeMessageInsert v ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, BetreeMessageInsert v) l) with
-              | Fail -> Fail
-              | Return _ -> Return (BetreeNodeInternal node)
-              end
-            | BetreeMessageDelete ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs
-                  (BetreeListCons (k, BetreeMessageDelete) l) with
-              | Fail -> Fail
-              | Return _ -> Return (BetreeNodeInternal node)
-              end
-            | BetreeMessageUpsert ufs ->
-              begin match betree_internal_lookup_in_children_fwd node key st0
-                with
-              | Fail -> Fail
-              | Return (st1, v) ->
-                begin match
-                  betree_node_apply_upserts_fwd (BetreeListCons (k,
-                    BetreeMessageUpsert ufs) l) v key st1 with
-                | Fail -> Fail
-                | Return (st2, _) ->
-                  begin match
-                    betree_internal_lookup_in_children_back node key st0 with
-                  | Fail -> Fail
-                  | Return node0 ->
-                    begin match
-                      betree_node_apply_upserts_back (BetreeListCons (k,
-                        BetreeMessageUpsert ufs) l) v key st1 with
-                    | Fail -> Fail
-                    | Return pending0 ->
-                      begin match
-                        betree_node_lookup_first_message_for_key_back key msgs
-                          pending0 with
-                      | Fail -> Fail
-                      | Return msgs0 ->
-                        begin match
-                          betree_store_internal_node_fwd
-                            node0.betree_internal_id msgs0 st2 with
-                        | Fail -> Fail
-                        | Return (_, _) -> Return (BetreeNodeInternal node0)
-                        end
-                      end
-                    end
-                  end
-                end
-              end
-            end
-        | BetreeListNil ->
-          begin match
-            betree_node_lookup_first_message_for_key_back key msgs
-              BetreeListNil with
-          | Fail -> Fail
-          | Return _ ->
-            begin match betree_internal_lookup_in_children_back node key st0
-              with
-            | Fail -> Fail
-            | Return node0 -> Return (BetreeNodeInternal node0)
-            end
-          end
-        end
-      end
-    end
-  | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
-    | Return (_, bindings) ->
-      begin match betree_node_lookup_in_bindings_fwd key bindings with
-      | Fail -> Fail
-      | Return _ -> Return (BetreeNodeLeaf node)
-      end
-    end
-  end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
-and betree_internal_lookup_in_children_fwd
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result (state & (option u64)))
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then
-    begin match betree_node_lookup_fwd self.betree_internal_left key st with
-    | Fail -> Fail
-    | Return (st0, opt) -> Return (st0, opt)
-    end
-  else
-    begin match betree_node_lookup_fwd self.betree_internal_right key st with
-    | Fail -> Fail
-    | Return (st0, opt) -> Return (st0, opt)
-    end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
-and betree_internal_lookup_in_children_back
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result betree_internal_t)
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then
-    begin match betree_node_lookup_back self.betree_internal_left key st with
-    | Fail -> Fail
-    | Return n ->
-      Return (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n self.betree_internal_right)
-    end
-  else
-    begin match betree_node_lookup_back self.betree_internal_right key st with
-    | Fail -> Fail
-    | Return n ->
-      Return (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot self.betree_internal_left n)
-    end
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
-let rec betree_node_lookup_mut_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return (BetreeListCons (i, i0) tl)
-    else
-      begin match betree_node_lookup_mut_in_bindings_fwd key tl with
-      | Fail -> Fail
-      | Return l -> Return l
-      end
-  | BetreeListNil -> Return BetreeListNil
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
-let rec betree_node_lookup_mut_in_bindings_back
-  (key : u64) (bindings : betree_list_t (u64 & u64))
-  (ret : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return ret
-    else
-      begin match betree_node_lookup_mut_in_bindings_back key tl ret with
-      | Fail -> Fail
-      | Return tl0 -> Return (BetreeListCons (i, i0) tl0)
-      end
-  | BetreeListNil -> Return ret
-  end
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf] *)
-let betree_node_apply_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64)) (key : u64)
-  (new_msg : betree_message_t) :
-  result (betree_list_t (u64 & u64))
-  =
-  begin match betree_node_lookup_mut_in_bindings_fwd key bindings with
-  | Fail -> Fail
-  | Return bindings0 ->
-    begin match betree_list_head_has_key_fwd u64 bindings0 key with
-    | Fail -> Fail
-    | Return b ->
-      if b
-      then
-        begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with
-        | Fail -> Fail
-        | Return hd ->
-          begin match new_msg with
-          | BetreeMessageInsert v ->
-            begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-            | Fail -> Fail
-            | Return bindings1 ->
-              begin match
-                betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v)
-                with
-              | Fail -> Fail
-              | Return bindings2 ->
-                begin match
-                  betree_node_lookup_mut_in_bindings_back key bindings
-                    bindings2 with
-                | Fail -> Fail
-                | Return bindings3 -> Return bindings3
-                end
-              end
-            end
-          | BetreeMessageDelete ->
-            begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-            | Fail -> Fail
-            | Return bindings1 ->
-              begin match
-                betree_node_lookup_mut_in_bindings_back key bindings bindings1
-                with
-              | Fail -> Fail
-              | Return bindings2 -> Return bindings2
-              end
-            end
-          | BetreeMessageUpsert s ->
-            let (_, i) = hd in
-            begin match betree_upsert_update_fwd (Some i) s with
-            | Fail -> Fail
-            | Return v ->
-              begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-              | Fail -> Fail
-              | Return bindings1 ->
-                begin match
-                  betree_list_push_front_fwd_back (u64 & u64) bindings1 (key,
-                    v) with
-                | Fail -> Fail
-                | Return bindings2 ->
-                  begin match
-                    betree_node_lookup_mut_in_bindings_back key bindings
-                      bindings2 with
-                  | Fail -> Fail
-                  | Return bindings3 -> Return bindings3
-                  end
-                end
-              end
-            end
-          end
-        end
-      else
-        begin match new_msg with
-        | BetreeMessageInsert v ->
-          begin match
-            betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with
-          | Fail -> Fail
-          | Return bindings1 ->
-            begin match
-              betree_node_lookup_mut_in_bindings_back key bindings bindings1
-              with
-            | Fail -> Fail
-            | Return bindings2 -> Return bindings2
-            end
-          end
-        | BetreeMessageDelete ->
-          begin match
-            betree_node_lookup_mut_in_bindings_back key bindings bindings0 with
-          | Fail -> Fail
-          | Return bindings1 -> Return bindings1
-          end
-        | BetreeMessageUpsert s ->
-          begin match betree_upsert_update_fwd None s with
-          | Fail -> Fail
-          | Return v ->
-            begin match
-              betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v)
-              with
-            | Fail -> Fail
-            | Return bindings1 ->
-              begin match
-                betree_node_lookup_mut_in_bindings_back key bindings bindings1
-                with
-              | Fail -> Fail
-              | Return bindings2 -> Return bindings2
-              end
-            end
-          end
-        end
-    end
-  end
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *)
-let rec betree_node_apply_messages_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
-  =
-  begin match new_msgs with
-  | BetreeListCons new_msg new_msgs_tl ->
-    let (i, m) = new_msg in
-    begin match betree_node_apply_to_leaf_fwd_back bindings i m with
-    | Fail -> Fail
-    | Return bindings0 ->
-      begin match
-        betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with
-      | Fail -> Fail
-      | Return bindings1 -> Return bindings1
-      end
-    end
-  | BetreeListNil -> Return bindings
-  end
-
-(** [betree_main::betree::Node::{5}::filter_messages_for_key] *)
-let rec betree_node_filter_messages_for_key_fwd_back
-  (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & betree_message_t)))
-  (decreases (betree_node_filter_messages_for_key_decreases key msgs))
-  =
-  begin match msgs with
-  | BetreeListCons p l ->
-    let (k, m) = p in
-    if k = key
-    then
-      begin match
-        betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
-          m) l) with
-      | Fail -> Fail
-      | Return msgs0 ->
-        begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with
-        | Fail -> Fail
-        | Return msgs1 -> Return msgs1
-        end
-      end
-    else Return (BetreeListCons (k, m) l)
-  | BetreeListNil -> Return BetreeListNil
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
-let rec betree_node_lookup_first_message_after_key_fwd
-  (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & betree_message_t)))
-  (decreases (betree_node_lookup_first_message_after_key_decreases key msgs))
-  =
-  begin match msgs with
-  | BetreeListCons p next_msgs ->
-    let (k, m) = p in
-    if k = key
-    then
-      begin match betree_node_lookup_first_message_after_key_fwd key next_msgs
-        with
-      | Fail -> Fail
-      | Return l -> Return l
-      end
-    else Return (BetreeListCons (k, m) next_msgs)
-  | BetreeListNil -> Return BetreeListNil
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
-let rec betree_node_lookup_first_message_after_key_back
-  (key : u64) (msgs : betree_list_t (u64 & betree_message_t))
-  (ret : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & betree_message_t)))
-  (decreases (betree_node_lookup_first_message_after_key_decreases key msgs))
-  =
-  begin match msgs with
-  | BetreeListCons p next_msgs ->
-    let (k, m) = p in
-    if k = key
-    then
-      begin match
-        betree_node_lookup_first_message_after_key_back key next_msgs ret with
-      | Fail -> Fail
-      | Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0)
-      end
-    else Return ret
-  | BetreeListNil -> Return ret
-  end
-
-(** [betree_main::betree::Node::{5}::apply_to_internal] *)
-let betree_node_apply_to_internal_fwd_back
-  (msgs : betree_list_t (u64 & betree_message_t)) (key : u64)
-  (new_msg : betree_message_t) :
-  result (betree_list_t (u64 & betree_message_t))
-  =
-  begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-  | Fail -> Fail
-  | Return msgs0 ->
-    begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with
-    | Fail -> Fail
-    | Return b ->
-      if b
-      then
-        begin match new_msg with
-        | BetreeMessageInsert i ->
-          begin match betree_node_filter_messages_for_key_fwd_back key msgs0
-            with
-          | Fail -> Fail
-          | Return msgs1 ->
-            begin match
-              betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
-                (key, BetreeMessageInsert i) with
-            | Fail -> Fail
-            | Return msgs2 ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs msgs2
-                with
-              | Fail -> Fail
-              | Return msgs3 -> Return msgs3
-              end
-            end
-          end
-        | BetreeMessageDelete ->
-          begin match betree_node_filter_messages_for_key_fwd_back key msgs0
-            with
-          | Fail -> Fail
-          | Return msgs1 ->
-            begin match
-              betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
-                (key, BetreeMessageDelete) with
-            | Fail -> Fail
-            | Return msgs2 ->
-              begin match
-                betree_node_lookup_first_message_for_key_back key msgs msgs2
-                with
-              | Fail -> Fail
-              | Return msgs3 -> Return msgs3
-              end
-            end
-          end
-        | BetreeMessageUpsert s ->
-          begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with
-          | Fail -> Fail
-          | Return p ->
-            let (_, m) = p in
-            begin match m with
-            | BetreeMessageInsert prev ->
-              begin match betree_upsert_update_fwd (Some prev) s with
-              | Fail -> Fail
-              | Return v ->
-                begin match
-                  betree_list_pop_front_back (u64 & betree_message_t) msgs0
-                  with
-                | Fail -> Fail
-                | Return msgs1 ->
-                  begin match
-                    betree_list_push_front_fwd_back (u64 & betree_message_t)
-                      msgs1 (key, BetreeMessageInsert v) with
-                  | Fail -> Fail
-                  | Return msgs2 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs2 with
-                    | Fail -> Fail
-                    | Return msgs3 -> Return msgs3
-                    end
-                  end
-                end
-              end
-            | BetreeMessageDelete ->
-              begin match betree_upsert_update_fwd None s with
-              | Fail -> Fail
-              | Return v ->
-                begin match
-                  betree_list_pop_front_back (u64 & betree_message_t) msgs0
-                  with
-                | Fail -> Fail
-                | Return msgs1 ->
-                  begin match
-                    betree_list_push_front_fwd_back (u64 & betree_message_t)
-                      msgs1 (key, BetreeMessageInsert v) with
-                  | Fail -> Fail
-                  | Return msgs2 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs2 with
-                    | Fail -> Fail
-                    | Return msgs3 -> Return msgs3
-                    end
-                  end
-                end
-              end
-            | BetreeMessageUpsert ufs ->
-              begin match
-                betree_node_lookup_first_message_after_key_fwd key msgs0 with
-              | Fail -> Fail
-              | Return msgs1 ->
-                begin match
-                  betree_list_push_front_fwd_back (u64 & betree_message_t)
-                    msgs1 (key, BetreeMessageUpsert s) with
-                | Fail -> Fail
-                | Return msgs2 ->
-                  begin match
-                    betree_node_lookup_first_message_after_key_back key msgs0
-                      msgs2 with
-                  | Fail -> Fail
-                  | Return msgs3 ->
-                    begin match
-                      betree_node_lookup_first_message_for_key_back key msgs
-                        msgs3 with
-                    | Fail -> Fail
-                    | Return msgs4 -> Return msgs4
-                    end
-                  end
-                end
-              end
-            end
-          end
-        end
-      else
-        begin match
-          betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
-            new_msg) with
-        | Fail -> Fail
-        | Return msgs1 ->
-          begin match
-            betree_node_lookup_first_message_for_key_back key msgs msgs1 with
-          | Fail -> Fail
-          | Return msgs2 -> Return msgs2
-          end
-        end
-    end
-  end
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
-let rec betree_node_apply_messages_to_internal_fwd_back
-  (msgs : betree_list_t (u64 & betree_message_t))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & betree_message_t)))
-  (decreases (betree_node_apply_messages_to_internal_decreases msgs new_msgs))
-  =
-  begin match new_msgs with
-  | BetreeListCons new_msg new_msgs_tl ->
-    let (i, m) = new_msg in
-    begin match betree_node_apply_to_internal_fwd_back msgs i m with
-    | Fail -> Fail
-    | Return msgs0 ->
-      begin match
-        betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with
-      | Fail -> Fail
-      | Return msgs1 -> Return msgs1
-      end
-    end
-  | BetreeListNil -> Return msgs
-  end
-
-(** [betree_main::betree::Node::{5}::apply_messages] *)
-let rec betree_node_apply_messages_fwd
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (state & unit))
-  (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
-  st))
-  =
-  begin match self with
-  | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
-    | Return (st0, content) ->
-      begin match betree_node_apply_messages_to_internal_fwd_back content msgs
-        with
-      | Fail -> Fail
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail -> Fail
-        | Return num_msgs ->
-          if num_msgs >= params.betree_params_min_flush_size
-          then
-            begin match
-              betree_internal_flush_fwd node params node_id_cnt content0 st0
-              with
-            | Fail -> Fail
-            | Return (st1, content1) ->
-              begin match
-                betree_internal_flush_back node params node_id_cnt content0 st0
-                with
-              | Fail -> Fail
-              | Return (node0, _) ->
-                begin match
-                  betree_store_internal_node_fwd node0.betree_internal_id
-                    content1 st1 with
-                | Fail -> Fail
-                | Return (st2, _) -> Return (st2, ())
-                end
-              end
-            end
-          else
-            begin match
-              betree_store_internal_node_fwd node.betree_internal_id content0
-                st0 with
-            | Fail -> Fail
-            | Return (st1, _) -> Return (st1, ())
-            end
-        end
-      end
-    end
-  | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
-    | Return (st0, content) ->
-      begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail -> Fail
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail -> Fail
-        | Return len ->
-          begin match u64_mul 2 params.betree_params_split_size with
-          | Fail -> Fail
-          | Return i ->
-            if len >= i
-            then
-              begin match
-                betree_leaf_split_fwd node content0 params node_id_cnt st0 with
-              | Fail -> Fail
-              | Return (st1, _) ->
-                begin match
-                  betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
-                    st1 with
-                | Fail -> Fail
-                | Return (st2, _) -> Return (st2, ())
-                end
-              end
-            else
-              begin match
-                betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
-                with
-              | Fail -> Fail
-              | Return (st1, _) -> Return (st1, ())
-              end
-          end
-        end
-      end
-    end
-  end
-
-(** [betree_main::betree::Node::{5}::apply_messages] *)
-and betree_node_apply_messages_back
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (betree_node_t & betree_node_id_counter_t))
-  (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
-  st))
-  =
-  begin match self with
-  | BetreeNodeInternal node ->
-    begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
-    | Return (st0, content) ->
-      begin match betree_node_apply_messages_to_internal_fwd_back content msgs
-        with
-      | Fail -> Fail
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail -> Fail
-        | Return num_msgs ->
-          if num_msgs >= params.betree_params_min_flush_size
-          then
-            begin match
-              betree_internal_flush_fwd node params node_id_cnt content0 st0
-              with
-            | Fail -> Fail
-            | Return (st1, content1) ->
-              begin match
-                betree_internal_flush_back node params node_id_cnt content0 st0
-                with
-              | Fail -> Fail
-              | Return (node0, node_id_cnt0) ->
-                begin match
-                  betree_store_internal_node_fwd node0.betree_internal_id
-                    content1 st1 with
-                | Fail -> Fail
-                | Return (_, _) ->
-                  Return (BetreeNodeInternal node0, node_id_cnt0)
-                end
-              end
-            end
-          else
-            begin match
-              betree_store_internal_node_fwd node.betree_internal_id content0
-                st0 with
-            | Fail -> Fail
-            | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt)
-            end
-        end
-      end
-    end
-  | BetreeNodeLeaf node ->
-    begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
-    | Return (st0, content) ->
-      begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail -> Fail
-      | Return content0 ->
-        begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail -> Fail
-        | Return len ->
-          begin match u64_mul 2 params.betree_params_split_size with
-          | Fail -> Fail
-          | Return i ->
-            if len >= i
-            then
-              begin match
-                betree_leaf_split_fwd node content0 params node_id_cnt st0 with
-              | Fail -> Fail
-              | Return (st1, new_node) ->
-                begin match
-                  betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
-                    st1 with
-                | Fail -> Fail
-                | Return (_, _) ->
-                  begin match
-                    betree_leaf_split_back node content0 params node_id_cnt st0
-                    with
-                  | Fail -> Fail
-                  | Return node_id_cnt0 ->
-                    Return (BetreeNodeInternal new_node, node_id_cnt0)
-                  end
-                end
-              end
-            else
-              begin match
-                betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
-                with
-              | Fail -> Fail
-              | Return (_, _) ->
-                Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id
-                  len), node_id_cnt)
-              end
-          end
-        end
-      end
-    end
-  end
-
-(** [betree_main::betree::Internal::{4}::flush] *)
-and betree_internal_flush_fwd
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (state & (betree_list_t (u64 & betree_message_t))))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
-  =
-  begin match
-    betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot with
-  | Fail -> Fail
-  | Return p ->
-    let (msgs_left, msgs_right) = p in
-    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
-    | Return len_left ->
-      if len_left >= params.betree_params_min_flush_size
-      then
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st with
-        | Fail -> Fail
-        | Return (st0, _) ->
-          begin match
-            betree_node_apply_messages_back self.betree_internal_left params
-              node_id_cnt msgs_left st with
-          | Fail -> Fail
-          | Return (_, node_id_cnt0) ->
-            begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
-              with
-            | Fail -> Fail
-            | Return len_right ->
-              if len_right >= params.betree_params_min_flush_size
-              then
-                begin match
-                  betree_node_apply_messages_fwd self.betree_internal_right
-                    params node_id_cnt0 msgs_right st0 with
-                | Fail -> Fail
-                | Return (st1, _) ->
-                  begin match
-                    betree_node_apply_messages_back self.betree_internal_right
-                      params node_id_cnt0 msgs_right st0 with
-                  | Fail -> Fail
-                  | Return (_, _) -> Return (st1, BetreeListNil)
-                  end
-                end
-              else Return (st0, msgs_right)
-            end
-          end
-        end
-      else
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_right params
-            node_id_cnt msgs_right st with
-        | Fail -> Fail
-        | Return (st0, _) ->
-          begin match
-            betree_node_apply_messages_back self.betree_internal_right params
-              node_id_cnt msgs_right st with
-          | Fail -> Fail
-          | Return (_, _) -> Return (st0, msgs_left)
-          end
-        end
-    end
-  end
-
-(** [betree_main::betree::Internal::{4}::flush] *)
-and betree_internal_flush_back
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (betree_internal_t & betree_node_id_counter_t))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
-  =
-  begin match
-    betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot with
-  | Fail -> Fail
-  | Return p ->
-    let (msgs_left, msgs_right) = p in
-    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
-    | Return len_left ->
-      if len_left >= params.betree_params_min_flush_size
-      then
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st with
-        | Fail -> Fail
-        | Return (st0, _) ->
-          begin match
-            betree_node_apply_messages_back self.betree_internal_left params
-              node_id_cnt msgs_left st with
-          | Fail -> Fail
-          | Return (n, node_id_cnt0) ->
-            begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
-              with
-            | Fail -> Fail
-            | Return len_right ->
-              if len_right >= params.betree_params_min_flush_size
-              then
-                begin match
-                  betree_node_apply_messages_back self.betree_internal_right
-                    params node_id_cnt0 msgs_right st0 with
-                | Fail -> Fail
-                | Return (n0, node_id_cnt1) ->
-                  Return (Mkbetree_internal_t self.betree_internal_id
-                    self.betree_internal_pivot n n0, node_id_cnt1)
-                end
-              else
-                Return (Mkbetree_internal_t self.betree_internal_id
-                  self.betree_internal_pivot n self.betree_internal_right,
-                  node_id_cnt0)
-            end
-          end
-        end
-      else
-        begin match
-          betree_node_apply_messages_back self.betree_internal_right params
-            node_id_cnt msgs_right st with
-        | Fail -> Fail
-        | Return (n, node_id_cnt0) ->
-          Return (Mkbetree_internal_t self.betree_internal_id
-            self.betree_internal_pivot self.betree_internal_left n,
-            node_id_cnt0)
-        end
-    end
-  end
-
-(** [betree_main::betree::Node::{5}::apply] *)
-let betree_node_apply_fwd
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t) (key : u64)
-  (new_msg : betree_message_t) (st : state) :
-  result (state & unit)
-  =
-  let l = BetreeListNil in
-  begin match
-    betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
-      (key, new_msg) l) st with
-  | Fail -> Fail
-  | Return (st0, _) ->
-    begin match
-      betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
-        (key, new_msg) l) st with
-    | Fail -> Fail
-    | Return (_, _) -> Return (st0, ())
-    end
-  end
-
-(** [betree_main::betree::Node::{5}::apply] *)
-let betree_node_apply_back
-  (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
-  begin match
-    betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
-      (key, new_msg) l) st with
-  | Fail -> Fail
-  | Return (self0, node_id_cnt0) -> Return (self0, node_id_cnt0)
-  end
-
-(** [betree_main::betree::BeTree::{6}::new] *)
-let betree_be_tree_new_fwd
-  (min_flush_size : u64) (split_size : u64) (st : state) :
-  result (state & betree_be_tree_t)
-  =
-  begin match betree_node_id_counter_new_fwd with
-  | Fail -> Fail
-  | Return node_id_cnt ->
-    begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-    | Fail -> Fail
-    | Return id ->
-      begin match betree_store_leaf_node_fwd id BetreeListNil st with
-      | Fail -> Fail
-      | Return (st0, _) ->
-        begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
-        | Return node_id_cnt0 ->
-          Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size
-            split_size) node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
-        end
-      end
-    end
-  end
-
-(** [betree_main::betree::BeTree::{6}::apply] *)
-let betree_be_tree_apply_fwd
-  (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) :
-  result (state & unit)
-  =
-  begin match
-    betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
-      self.betree_be_tree_node_id_cnt key msg st with
-  | Fail -> Fail
-  | Return (st0, _) ->
-    begin match
-      betree_node_apply_back self.betree_be_tree_root
-        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-      with
-    | Fail -> Fail
-    | Return (_, _) -> Return (st0, ())
-    end
-  end
-
-(** [betree_main::betree::BeTree::{6}::apply] *)
-let betree_be_tree_apply_back
-  (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) :
-  result betree_be_tree_t
-  =
-  begin match
-    betree_node_apply_back self.betree_be_tree_root self.betree_be_tree_params
-      self.betree_be_tree_node_id_cnt key msg st with
-  | Fail -> Fail
-  | Return (n, nic) ->
-    Return (Mkbetree_be_tree_t self.betree_be_tree_params nic n)
-  end
-
-(** [betree_main::betree::BeTree::{6}::insert] *)
-let betree_be_tree_insert_fwd
-  (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) :
-  result (state & unit)
-  =
-  begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st
-    with
-  | Fail -> Fail
-  | Return (st0, _) ->
-    begin match
-      betree_be_tree_apply_back self key (BetreeMessageInsert value) st with
-    | Fail -> Fail
-    | Return _ -> Return (st0, ())
-    end
-  end
-
-(** [betree_main::betree::BeTree::{6}::insert] *)
-let betree_be_tree_insert_back
-  (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) :
-  result betree_be_tree_t
-  =
-  begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st
-    with
-  | Fail -> Fail
-  | Return self0 -> Return self0
-  end
-
-(** [betree_main::betree::BeTree::{6}::delete] *)
-let betree_be_tree_delete_fwd
-  (self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) =
-  begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with
-  | Fail -> Fail
-  | Return (st0, _) ->
-    begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
-    | Fail -> Fail
-    | Return _ -> Return (st0, ())
-    end
-  end
-
-(** [betree_main::betree::BeTree::{6}::delete] *)
-let betree_be_tree_delete_back
-  (self : betree_be_tree_t) (key : u64) (st : state) :
-  result betree_be_tree_t
-  =
-  begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
-  | Fail -> Fail
-  | Return self0 -> Return self0
-  end
-
-(** [betree_main::betree::BeTree::{6}::upsert] *)
-let betree_be_tree_upsert_fwd
-  (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t)
-  (st : state) :
-  result (state & unit)
-  =
-  begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st
-    with
-  | Fail -> Fail
-  | Return (st0, _) ->
-    begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
-      with
-    | Fail -> Fail
-    | Return _ -> Return (st0, ())
-    end
-  end
-
-(** [betree_main::betree::BeTree::{6}::upsert] *)
-let betree_be_tree_upsert_back
-  (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t)
-  (st : state) :
-  result betree_be_tree_t
-  =
-  begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
-    with
-  | Fail -> Fail
-  | Return self0 -> Return self0
-  end
-
-(** [betree_main::betree::BeTree::{6}::lookup] *)
-let betree_be_tree_lookup_fwd
-  (self : betree_be_tree_t) (key : u64) (st : state) :
-  result (state & (option u64))
-  =
-  begin match betree_node_lookup_fwd self.betree_be_tree_root key st with
-  | Fail -> Fail
-  | Return (st0, opt) -> Return (st0, opt)
-  end
-
-(** [betree_main::betree::BeTree::{6}::lookup] *)
-let betree_be_tree_lookup_back
-  (self : betree_be_tree_t) (key : u64) (st : state) :
-  result betree_be_tree_t
-  =
-  begin match betree_node_lookup_back self.betree_be_tree_root key st with
-  | Fail -> Fail
-  | Return n ->
-    Return (Mkbetree_be_tree_t self.betree_be_tree_params
-      self.betree_be_tree_node_id_cnt n)
-  end
-
-(** [betree_main::main] *)
-let main_fwd : result unit = Return ()
-
-(** Unit test for [betree_main::main] *)
-let _ = assert_norm (main_fwd = Return ())
-
diff --git a/tests/betree/BetreeMain.Opaque.fsti b/tests/betree/BetreeMain.Opaque.fsti
deleted file mode 100644
index dc49601a..00000000
--- a/tests/betree/BetreeMain.Opaque.fsti
+++ /dev/null
@@ -1,30 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: opaque function definitions *)
-module BetreeMain.Opaque
-open Primitives
-include BetreeMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree_utils::load_internal_node] *)
-val betree_utils_load_internal_node_fwd
-  : u64 -> state -> result (state & (betree_list_t (u64 & betree_message_t)))
-
-(** [betree_main::betree_utils::store_internal_node] *)
-val betree_utils_store_internal_node_fwd
-  :
-  u64 -> betree_list_t (u64 & betree_message_t) -> state -> result (state &
-    unit)
-
-(** [betree_main::betree_utils::load_leaf_node] *)
-val betree_utils_load_leaf_node_fwd
-  : u64 -> state -> result (state & (betree_list_t (u64 & u64)))
-
-(** [betree_main::betree_utils::store_leaf_node] *)
-val betree_utils_store_leaf_node_fwd
-  : u64 -> betree_list_t (u64 & u64) -> state -> result (state & unit)
-
-(** [core::option::Option::{0}::unwrap] *)
-val core_option_option_unwrap_fwd
-  (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti
deleted file mode 100644
index c81e3302..00000000
--- a/tests/betree/BetreeMain.Types.fsti
+++ /dev/null
@@ -1,64 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
-module BetreeMain.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree::List] *)
-type betree_list_t (t : Type0) =
-| BetreeListCons : t -> betree_list_t t -> betree_list_t t
-| BetreeListNil : betree_list_t t
-
-(** [betree_main::betree::UpsertFunState] *)
-type betree_upsert_fun_state_t =
-| BetreeUpsertFunStateAdd : u64 -> betree_upsert_fun_state_t
-| BetreeUpsertFunStateSub : u64 -> betree_upsert_fun_state_t
-
-(** [betree_main::betree::Message] *)
-type betree_message_t =
-| BetreeMessageInsert : u64 -> betree_message_t
-| BetreeMessageDelete : betree_message_t
-| BetreeMessageUpsert : betree_upsert_fun_state_t -> betree_message_t
-
-(** [betree_main::betree::Leaf] *)
-type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
-
-(** [betree_main::betree::Node] *)
-type betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
-(** [betree_main::betree::Internal] *)
-and betree_internal_t =
-{
-  betree_internal_id : u64;
-  betree_internal_pivot : u64;
-  betree_internal_left : betree_node_t;
-  betree_internal_right : betree_node_t;
-}
-
-(** [betree_main::betree::Params] *)
-type betree_params_t =
-{
-  betree_params_min_flush_size : u64; betree_params_split_size : u64;
-}
-
-(** [betree_main::betree::NodeIdCounter] *)
-type betree_node_id_counter_t = { betree_node_id_counter_next_node_id : u64; }
-
-(** [betree_main::betree::BeTree] *)
-type betree_be_tree_t =
-{
-  betree_be_tree_params : betree_params_t;
-  betree_be_tree_node_id_cnt : betree_node_id_counter_t;
-  betree_be_tree_root : betree_node_t;
-}
-
-(** [core::num::u64::{10}::MAX] *)
-let core_num_u64_max_body : result u64 = Return 18446744073709551615
-let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
-
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/betree/Makefile b/tests/betree/Makefile
deleted file mode 100644
index a16b0edb..00000000
--- a/tests/betree/Makefile
+++ /dev/null
@@ -1,47 +0,0 @@
-INCLUDE_DIRS = .
-
-FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
-
-FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
-
-FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
-  --warn_error '+241@247+285-274' \
-
-FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
-
-FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
-
-# The F* roots are used to compute the dependency graph, and generate the .depend file
-FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
-
-# Build all the files
-all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
-
-# This is the right way to ensure the .depend file always gets re-built.
-ifeq (,$(filter %-in,$(MAKECMDGOALS)))
-ifndef NODEPEND
-ifndef MAKE_RESTARTS
-.depend: .FORCE
-	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
-
-.PHONY: .FORCE
-.FORCE:
-endif
-endif
-
-include .depend
-endif
-
-# For the interactive mode
-%.fst-in %.fsti-in:
-	@echo $(FSTAR_OPTIONS)
-
-# Generete the .checked files in batch mode
-%.checked:
-	$(FSTAR) $(FSTAR_OPTIONS) $< && \
-	touch -c $@
-
-.PHONY: clean
-clean:
-	rm -f obj/*
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
deleted file mode 100644
index 96138e46..00000000
--- a/tests/betree/Primitives.fst
+++ /dev/null
@@ -1,287 +0,0 @@
-/// This file lists primitive and assumed functions and types
-module Primitives
-open FStar.Mul
-open FStar.List.Tot
-
-#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
-
-(*** Utilities *)
-val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
-  ls':list a{
-    length ls' = length ls /\
-    index ls' i == x
-  }
-#push-options "--fuel 1"
-let rec list_update #a ls i x =
-  match ls with
-  | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x
-#pop-options
-
-(*** Result *)
-type result (a : Type0) : Type0 =
-| Return : v:a -> result a
-| Fail : result a
-
-// Monadic bind and return.
-// Re-definining those allows us to customize the result of the monadic notations
-// like: `y <-- f x;`
-let return (#a : Type0) (x:a) : result a = Return x
-let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
-    match m with
-    | Return x -> f x
-    | Fail -> Fail
-
-// Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
-
-// Normalize and unwrap a successful result (used for globals).
-let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
-
-(*** Misc *)
-type char = FStar.Char.char
-type string = string
-
-let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
-let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
-
-(*** Scalars *)
-/// Rk.: most of the following code was at least partially generated
-
-let isize_min : int = -9223372036854775808 // TODO: should be opaque
-let isize_max : int = 9223372036854775807 // TODO: should be opaque
-let i8_min : int = -128
-let i8_max : int = 127
-let i16_min : int = -32768
-let i16_max : int = 32767
-let i32_min : int = -2147483648
-let i32_max : int = 2147483647
-let i64_min : int = -9223372036854775808
-let i64_max : int = 9223372036854775807
-let i128_min : int = -170141183460469231731687303715884105728
-let i128_max : int = 170141183460469231731687303715884105727
-let usize_min : int = 0
-let usize_max : int = 4294967295 // TODO: should be opaque
-let u8_min : int = 0
-let u8_max : int = 255
-let u16_min : int = 0
-let u16_max : int = 65535
-let u32_min : int = 0
-let u32_max : int = 4294967295
-let u64_min : int = 0
-let u64_max : int = 18446744073709551615
-let u128_min : int = 0
-let u128_max : int = 340282366920938463463374607431768211455
-
-type scalar_ty =
-| Isize
-| I8
-| I16
-| I32
-| I64
-| I128
-| Usize
-| U8
-| U16
-| U32
-| U64
-| U128
-
-let scalar_min (ty : scalar_ty) : int =
-  match ty with
-  | Isize -> isize_min
-  | I8 -> i8_min
-  | I16 -> i16_min
-  | I32 -> i32_min
-  | I64 -> i64_min
-  | I128 -> i128_min
-  | Usize -> usize_min
-  | U8 -> u8_min
-  | U16 -> u16_min
-  | U32 -> u32_min
-  | U64 -> u64_min
-  | U128 -> u128_min
-
-let scalar_max (ty : scalar_ty) : int =
-  match ty with
-  | Isize -> isize_max
-  | I8 -> i8_max
-  | I16 -> i16_max
-  | I32 -> i32_max
-  | I64 -> i64_max
-  | I128 -> i128_max
-  | Usize -> usize_max
-  | U8 -> u8_max
-  | U16 -> u16_max
-  | U32 -> u32_max
-  | U64 -> u64_max
-  | U128 -> u128_max
-
-type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
-
-let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
-
-let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
-
-let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail
-
-/// The remainder operation
-let int_rem (x : int) (y : int{y <> 0}) : int =
-  if x >= 0 then (x % y) else -(x % y)
-
-(* Checking consistency with Rust *)
-let _ = assert_norm(int_rem 1 2 = 1)
-let _ = assert_norm(int_rem (-1) 2 = -1)
-let _ = assert_norm(int_rem 1 (-2) = 1)
-let _ = assert_norm(int_rem (-1) (-2) = -1)
-
-let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail
-
-let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  mk_scalar ty (x + y)
-
-let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  mk_scalar ty (x - y)
-
-let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  mk_scalar ty (x * y)
-
-(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-// TODO: check the semantics of casts in Rust
-let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
-  mk_scalar tgt_ty x
-
-/// The scalar types
-type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
-type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
-
-/// Negation
-let isize_neg = scalar_neg #Isize
-let i8_neg = scalar_neg #I8
-let i16_neg = scalar_neg #I16
-let i32_neg = scalar_neg #I32
-let i64_neg = scalar_neg #I64
-let i128_neg = scalar_neg #I128
-
-/// Division
-let isize_div = scalar_div #Isize
-let i8_div = scalar_div #I8
-let i16_div = scalar_div #I16
-let i32_div = scalar_div #I32
-let i64_div = scalar_div #I64
-let i128_div = scalar_div #I128
-let usize_div = scalar_div #Usize
-let u8_div = scalar_div #U8
-let u16_div = scalar_div #U16
-let u32_div = scalar_div #U32
-let u64_div = scalar_div #U64
-let u128_div = scalar_div #U128
-
-/// Remainder
-let isize_rem = scalar_rem #Isize
-let i8_rem = scalar_rem #I8
-let i16_rem = scalar_rem #I16
-let i32_rem = scalar_rem #I32
-let i64_rem = scalar_rem #I64
-let i128_rem = scalar_rem #I128
-let usize_rem = scalar_rem #Usize
-let u8_rem = scalar_rem #U8
-let u16_rem = scalar_rem #U16
-let u32_rem = scalar_rem #U32
-let u64_rem = scalar_rem #U64
-let u128_rem = scalar_rem #U128
-
-/// Addition
-let isize_add = scalar_add #Isize
-let i8_add = scalar_add #I8
-let i16_add = scalar_add #I16
-let i32_add = scalar_add #I32
-let i64_add = scalar_add #I64
-let i128_add = scalar_add #I128
-let usize_add = scalar_add #Usize
-let u8_add = scalar_add #U8
-let u16_add = scalar_add #U16
-let u32_add = scalar_add #U32
-let u64_add = scalar_add #U64
-let u128_add = scalar_add #U128
-
-/// Substraction
-let isize_sub = scalar_sub #Isize
-let i8_sub = scalar_sub #I8
-let i16_sub = scalar_sub #I16
-let i32_sub = scalar_sub #I32
-let i64_sub = scalar_sub #I64
-let i128_sub = scalar_sub #I128
-let usize_sub = scalar_sub #Usize
-let u8_sub = scalar_sub #U8
-let u16_sub = scalar_sub #U16
-let u32_sub = scalar_sub #U32
-let u64_sub = scalar_sub #U64
-let u128_sub = scalar_sub #U128
-
-/// Multiplication
-let isize_mul = scalar_mul #Isize
-let i8_mul = scalar_mul #I8
-let i16_mul = scalar_mul #I16
-let i32_mul = scalar_mul #I32
-let i64_mul = scalar_mul #I64
-let i128_mul = scalar_mul #I128
-let usize_mul = scalar_mul #Usize
-let u8_mul = scalar_mul #U8
-let u16_mul = scalar_mul #U16
-let u32_mul = scalar_mul #U32
-let u64_mul = scalar_mul #U64
-let u128_mul = scalar_mul #U128
-
-(*** Vector *)
-type vec (a : Type0) = v:list a{length v <= usize_max}
-
-let vec_new (a  : Type0) : vec a = assert_norm(length #a [] == 0); []
-let vec_len (a : Type0) (v : vec a) : usize = length v
-
-// The **forward** function shouldn't be used
-let vec_push_fwd (a  : Type0) (v : vec a) (x : a) : unit = ()
-let vec_push_back (a  : Type0) (v : vec a) (x : a) :
-  Pure (result (vec a))
-  (requires True)
-  (ensures (fun res ->
-    match res with
-    | Fail -> True
-    | Return v' -> length v' = length v + 1)) =
-  if length v < usize_max then begin
-    (**) assert_norm(length [x] == 1);
-    (**) append_length v [x];
-    (**) assert(length (append v [x]) = length v + 1);
-    Return (append v [x])
-    end
-  else Fail
-
-// The **forward** function shouldn't be used
-let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
-let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
-  if i < length v then Return (list_update v i x) else Fail
-
-// The **backward** function shouldn't be used
-let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
-let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
-
-let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
-let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail
-