From fa6dcd3ebbdc7a508157ff2a12f91e70d2012a86 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 15 Nov 2022 15:25:47 +0100
Subject: Change the name of the generated Coq modules

---
 tests/coq/betree/BetreeMain_Funs.v              | 1397 +++++++++++++++++++++++
 tests/coq/betree/BetreeMain_Opaque.v            |   38 +
 tests/coq/betree/BetreeMain_Types.v             |   85 ++
 tests/coq/betree/BetreeMain__Funs.v             | 1397 -----------------------
 tests/coq/betree/BetreeMain__Opaque.v           |   38 -
 tests/coq/betree/BetreeMain__Types.v            |   85 --
 tests/coq/hashmap/Hashmap_Funs.v                |  541 +++++++++
 tests/coq/hashmap/Hashmap_Types.v               |   38 +
 tests/coq/hashmap/Hashmap__Funs.v               |  541 ---------
 tests/coq/hashmap/Hashmap__Types.v              |   38 -
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v    |  598 ++++++++++
 tests/coq/hashmap_on_disk/HashmapMain_Opaque.v  |   21 +
 tests/coq/hashmap_on_disk/HashmapMain_Types.v   |   41 +
 tests/coq/hashmap_on_disk/HashmapMain__Funs.v   |  598 ----------
 tests/coq/hashmap_on_disk/HashmapMain__Opaque.v |   21 -
 tests/coq/hashmap_on_disk/HashmapMain__Types.v  |   41 -
 tests/coq/misc/External_Funs.v                  |  114 ++
 tests/coq/misc/External_Opaque.v                |   36 +
 tests/coq/misc/External_Types.v                 |   15 +
 tests/coq/misc/External__Funs.v                 |  114 --
 tests/coq/misc/External__Opaque.v               |   36 -
 tests/coq/misc/External__Types.v                |   15 -
 22 files changed, 2924 insertions(+), 2924 deletions(-)
 create mode 100644 tests/coq/betree/BetreeMain_Funs.v
 create mode 100644 tests/coq/betree/BetreeMain_Opaque.v
 create mode 100644 tests/coq/betree/BetreeMain_Types.v
 delete mode 100644 tests/coq/betree/BetreeMain__Funs.v
 delete mode 100644 tests/coq/betree/BetreeMain__Opaque.v
 delete mode 100644 tests/coq/betree/BetreeMain__Types.v
 create mode 100644 tests/coq/hashmap/Hashmap_Funs.v
 create mode 100644 tests/coq/hashmap/Hashmap_Types.v
 delete mode 100644 tests/coq/hashmap/Hashmap__Funs.v
 delete mode 100644 tests/coq/hashmap/Hashmap__Types.v
 create mode 100644 tests/coq/hashmap_on_disk/HashmapMain_Funs.v
 create mode 100644 tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
 create mode 100644 tests/coq/hashmap_on_disk/HashmapMain_Types.v
 delete mode 100644 tests/coq/hashmap_on_disk/HashmapMain__Funs.v
 delete mode 100644 tests/coq/hashmap_on_disk/HashmapMain__Opaque.v
 delete mode 100644 tests/coq/hashmap_on_disk/HashmapMain__Types.v
 create mode 100644 tests/coq/misc/External_Funs.v
 create mode 100644 tests/coq/misc/External_Opaque.v
 create mode 100644 tests/coq/misc/External_Types.v
 delete mode 100644 tests/coq/misc/External__Funs.v
 delete mode 100644 tests/coq/misc/External__Opaque.v
 delete mode 100644 tests/coq/misc/External__Types.v

(limited to 'tests')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
new file mode 100644
index 00000000..3129614c
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -0,0 +1,1397 @@
+(** 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 .
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v
new file mode 100644
index 00000000..08ab530a
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_Opaque.v
@@ -0,0 +1,38 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: opaque function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export BetreeMain_Types.
+Import BetreeMain_Types.
+Module BetreeMain_Opaque.
+
+(** [betree_main::betree_utils::load_internal_node] *)
+Axiom betree_utils_load_internal_node_fwd
+  : u64 -> state -> result (state * (Betree_list_t (u64 * Betree_message_t)))
+.
+
+(** [betree_main::betree_utils::store_internal_node] *)
+Axiom 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] *)
+Axiom betree_utils_load_leaf_node_fwd
+  : u64 -> state -> result (state * (Betree_list_t (u64 * u64)))
+.
+
+(** [betree_main::betree_utils::store_leaf_node] *)
+Axiom betree_utils_store_leaf_node_fwd
+  : u64 -> Betree_list_t (u64 * u64) -> state -> result (state * unit)
+.
+
+(** [core::option::Option::{0}::unwrap] *)
+Axiom core_option_option_unwrap_fwd :
+  forall(T : Type), option T -> state -> result (state * T)
+.
+
+End BetreeMain_Opaque .
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
new file mode 100644
index 00000000..672b2ebd
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -0,0 +1,85 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: type definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module BetreeMain_Types.
+
+(** [betree_main::betree::List] *)
+Inductive Betree_list_t (T : Type) :=
+| BetreeListCons : T -> Betree_list_t T -> Betree_list_t T
+| BetreeListNil : Betree_list_t T
+.
+
+Arguments BetreeListCons {T} _ _.
+Arguments BetreeListNil {T}.
+
+(** [betree_main::betree::UpsertFunState] *)
+Inductive Betree_upsert_fun_state_t :=
+| BetreeUpsertFunStateAdd : u64 -> Betree_upsert_fun_state_t
+| BetreeUpsertFunStateSub : u64 -> Betree_upsert_fun_state_t
+.
+
+(** [betree_main::betree::Message] *)
+Inductive 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] *)
+Record Betree_leaf_t :=
+mkBetree_leaf_t {
+  Betree_leaf_id : u64; Betree_leaf_size : u64;
+}
+.
+
+(** [betree_main::betree::Node] *)
+Inductive Betree_node_t :=
+| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
+| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
+
+(** [betree_main::betree::Internal] *)
+with Betree_internal_t :=
+| mkBetree_internal_t :
+  u64 ->
+  u64 ->
+  Betree_node_t ->
+  Betree_node_t ->
+  Betree_internal_t
+.
+
+(** [betree_main::betree::Params] *)
+Record Betree_params_t :=
+mkBetree_params_t {
+  Betree_params_min_flush_size : u64; Betree_params_split_size : u64;
+}
+.
+
+(** [betree_main::betree::NodeIdCounter] *)
+Record Betree_node_id_counter_t :=
+mkBetree_node_id_counter_t {
+  Betree_node_id_counter_next_node_id : u64;
+}
+.
+
+(** [betree_main::betree::BeTree] *)
+Record Betree_be_tree_t :=
+mkBetree_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] *)
+Definition core_num_u64_max_body : result u64 :=
+  Return (18446744073709551615%u64)
+.
+Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End BetreeMain_Types .
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 .
diff --git a/tests/coq/betree/BetreeMain__Opaque.v b/tests/coq/betree/BetreeMain__Opaque.v
deleted file mode 100644
index cbd8cfb3..00000000
--- a/tests/coq/betree/BetreeMain__Opaque.v
+++ /dev/null
@@ -1,38 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: opaque function definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Require Export BetreeMain__Types.
-Import BetreeMain__Types.
-Module BetreeMain__Opaque.
-
-(** [betree_main::betree_utils::load_internal_node] *)
-Axiom betree_utils_load_internal_node_fwd
-  : u64 -> state -> result (state * (Betree_list_t (u64 * Betree_message_t)))
-.
-
-(** [betree_main::betree_utils::store_internal_node] *)
-Axiom 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] *)
-Axiom betree_utils_load_leaf_node_fwd
-  : u64 -> state -> result (state * (Betree_list_t (u64 * u64)))
-.
-
-(** [betree_main::betree_utils::store_leaf_node] *)
-Axiom betree_utils_store_leaf_node_fwd
-  : u64 -> Betree_list_t (u64 * u64) -> state -> result (state * unit)
-.
-
-(** [core::option::Option::{0}::unwrap] *)
-Axiom core_option_option_unwrap_fwd :
-  forall(T : Type), option T -> state -> result (state * T)
-.
-
-End BetreeMain__Opaque .
diff --git a/tests/coq/betree/BetreeMain__Types.v b/tests/coq/betree/BetreeMain__Types.v
deleted file mode 100644
index 2ed0d324..00000000
--- a/tests/coq/betree/BetreeMain__Types.v
+++ /dev/null
@@ -1,85 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Module BetreeMain__Types.
-
-(** [betree_main::betree::List] *)
-Inductive Betree_list_t (T : Type) :=
-| BetreeListCons : T -> Betree_list_t T -> Betree_list_t T
-| BetreeListNil : Betree_list_t T
-.
-
-Arguments BetreeListCons {T} _ _.
-Arguments BetreeListNil {T}.
-
-(** [betree_main::betree::UpsertFunState] *)
-Inductive Betree_upsert_fun_state_t :=
-| BetreeUpsertFunStateAdd : u64 -> Betree_upsert_fun_state_t
-| BetreeUpsertFunStateSub : u64 -> Betree_upsert_fun_state_t
-.
-
-(** [betree_main::betree::Message] *)
-Inductive 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] *)
-Record Betree_leaf_t :=
-mkBetree_leaf_t {
-  Betree_leaf_id : u64; Betree_leaf_size : u64;
-}
-.
-
-(** [betree_main::betree::Node] *)
-Inductive Betree_node_t :=
-| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
-| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
-
-(** [betree_main::betree::Internal] *)
-with Betree_internal_t :=
-| mkBetree_internal_t :
-  u64 ->
-  u64 ->
-  Betree_node_t ->
-  Betree_node_t ->
-  Betree_internal_t
-.
-
-(** [betree_main::betree::Params] *)
-Record Betree_params_t :=
-mkBetree_params_t {
-  Betree_params_min_flush_size : u64; Betree_params_split_size : u64;
-}
-.
-
-(** [betree_main::betree::NodeIdCounter] *)
-Record Betree_node_id_counter_t :=
-mkBetree_node_id_counter_t {
-  Betree_node_id_counter_next_node_id : u64;
-}
-.
-
-(** [betree_main::betree::BeTree] *)
-Record Betree_be_tree_t :=
-mkBetree_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] *)
-Definition core_num_u64_max_body : result u64 :=
-  Return (18446744073709551615%u64)
-.
-Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
-
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End BetreeMain__Types .
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
new file mode 100644
index 00000000..912b7fe2
--- /dev/null
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -0,0 +1,541 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export Hashmap_Types.
+Import Hashmap_Types.
+Module Hashmap_Funs.
+
+(** [hashmap::hash_key] *)
+Definition hash_key_fwd (k : usize) : result usize := Return k.
+
+(** [hashmap::HashMap::{0}::allocate_slots] *)
+Fixpoint hash_map_allocate_slots_fwd
+  (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
+  result (vec (List_t T))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if n0 s= 0%usize
+    then Return slots
+    else (
+      slots0 <- vec_push_back (List_t T) slots ListNil;
+      i <- usize_sub n0 1%usize;
+      v <- hash_map_allocate_slots_fwd T n1 slots0 i;
+      Return v)
+  end
+.
+
+(** [hashmap::HashMap::{0}::new_with_capacity] *)
+Definition hash_map_new_with_capacity_fwd
+  (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
+  (max_load_divisor : usize) :
+  result (Hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let v := vec_new (List_t T) in
+    slots <- hash_map_allocate_slots_fwd T n0 v capacity;
+    i <- usize_mul capacity max_load_dividend;
+    i0 <- usize_div i max_load_divisor;
+    Return (mkHash_map_t (0%usize) (max_load_dividend, max_load_divisor) i0
+      slots)
+  end
+.
+
+(** [hashmap::HashMap::{0}::new] *)
+Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hm <- hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize) (5%usize);
+    Return hm
+  end
+.
+
+(** [hashmap::HashMap::{0}::clear_slots] *)
+Fixpoint hash_map_clear_slots_fwd_back
+  (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
+  result (vec (List_t T))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let i0 := vec_len (List_t T) slots in
+    if i s< i0
+    then (
+      slots0 <- vec_index_mut_back (List_t T) slots i ListNil;
+      i1 <- usize_add i 1%usize;
+      slots1 <- hash_map_clear_slots_fwd_back T n0 slots0 i1;
+      Return slots1)
+    else Return slots
+  end
+.
+
+(** [hashmap::HashMap::{0}::clear] *)
+Definition hash_map_clear_fwd_back
+  (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match self with
+    | mkHash_map_t i p i0 v =>
+      v0 <- hash_map_clear_slots_fwd_back T n0 v (0%usize);
+      Return (mkHash_map_t (0%usize) p i0 v0)
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::len] *)
+Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize :=
+  match self with | mkHash_map_t i p i0 v => Return i end
+.
+
+(** [hashmap::HashMap::{0}::insert_in_list] *)
+Fixpoint hash_map_insert_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
+  result bool
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return false
+      else (b <- hash_map_insert_in_list_fwd T n0 key value ls0; Return b)
+    | ListNil => Return true
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::insert_in_list] *)
+Fixpoint hash_map_insert_in_list_back
+  (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return (ListCons ckey value ls0)
+      else (
+        ls1 <- hash_map_insert_in_list_back T n0 key value ls0;
+        Return (ListCons ckey cvalue ls1))
+    | ListNil => let l := ListNil in Return (ListCons key value l)
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::insert_no_resize] *)
+Definition hash_map_insert_no_resize_fwd_back
+  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
+  result (Hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hash_key_fwd key;
+    match self with
+    | mkHash_map_t i p i0 v =>
+      let i1 := vec_len (List_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (List_t T) v hash_mod;
+      inserted <- hash_map_insert_in_list_fwd T n0 key value l;
+      if inserted
+      then (
+        i2 <- usize_add i 1%usize;
+        l0 <- hash_map_insert_in_list_back T n0 key value l;
+        v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
+        Return (mkHash_map_t i2 p i0 v0))
+      else (
+        l0 <- hash_map_insert_in_list_back T n0 key value l;
+        v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
+        Return (mkHash_map_t i p i0 v0))
+    end
+  end
+.
+
+(** [core::num::u32::{9}::MAX] *)
+Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
+Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
+
+(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+Fixpoint hash_map_move_elements_from_list_fwd_back
+  (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
+  result (Hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons k v tl =>
+      ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v;
+      ntable1 <- hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl;
+      Return ntable1
+    | ListNil => Return ntable
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::move_elements] *)
+Fixpoint hash_map_move_elements_fwd_back
+  (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
+  (i : usize) :
+  result ((Hash_map_t T) * (vec (List_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let i0 := vec_len (List_t T) slots in
+    if i s< i0
+    then (
+      l <- vec_index_mut_fwd (List_t T) slots i;
+      let ls := mem_replace_fwd (List_t T) l ListNil in
+      ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
+      let l0 := mem_replace_back (List_t T) l ListNil in
+      slots0 <- vec_index_mut_back (List_t T) slots i l0;
+      i1 <- usize_add i 1%usize;
+      p <- hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1;
+      let (ntable1, slots1) := p in
+      Return (ntable1, slots1))
+    else Return (ntable, slots)
+  end
+.
+
+(** [hashmap::HashMap::{0}::try_resize] *)
+Definition hash_map_try_resize_fwd_back
+  (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+    match self with
+    | mkHash_map_t i p i0 v =>
+      let capacity := vec_len (List_t T) v in
+      n1 <- usize_div max_usize 2%usize;
+      let (i1, i2) := p in
+      i3 <- usize_div n1 i1;
+      if capacity s<= i3
+      then (
+        i4 <- usize_mul capacity 2%usize;
+        ntable <- hash_map_new_with_capacity_fwd T n0 i4 i1 i2;
+        p0 <- hash_map_move_elements_fwd_back T n0 ntable v (0%usize);
+        let (ntable0, _) := p0 in
+        match ntable0 with
+        | mkHash_map_t i5 p1 i6 v0 => Return (mkHash_map_t i (i1, i2) i6 v0)
+        end)
+      else Return (mkHash_map_t i (i1, i2) i0 v)
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::insert] *)
+Definition hash_map_insert_fwd_back
+  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
+  result (Hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    self0 <- hash_map_insert_no_resize_fwd_back T n0 self key value;
+    i <- hash_map_len_fwd T self0;
+    match self0 with
+    | mkHash_map_t i0 p i1 v =>
+      if i s> i1
+      then (
+        self1 <- hash_map_try_resize_fwd_back T n0 (mkHash_map_t i0 p i1 v);
+        Return self1)
+      else Return (mkHash_map_t i0 p i1 v)
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+Fixpoint hash_map_contains_key_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons ckey t ls0 =>
+      if ckey s= key
+      then Return true
+      else (b <- hash_map_contains_key_in_list_fwd T n0 key ls0; Return b)
+    | ListNil => Return false
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::contains_key] *)
+Definition hash_map_contains_key_fwd
+  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result bool :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hash_key_fwd key;
+    match self with
+    | mkHash_map_t i p i0 v =>
+      let i1 := vec_len (List_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_fwd (List_t T) v hash_mod;
+      b <- hash_map_contains_key_in_list_fwd T n0 key l;
+      Return b
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::get_in_list] *)
+Fixpoint hash_map_get_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return cvalue
+      else (t <- hash_map_get_in_list_fwd T n0 key ls0; Return t)
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::get] *)
+Definition hash_map_get_fwd
+  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hash_key_fwd key;
+    match self with
+    | mkHash_map_t i p i0 v =>
+      let i1 := vec_len (List_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_fwd (List_t T) v hash_mod;
+      t <- hash_map_get_in_list_fwd T n0 key l;
+      Return t
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+Fixpoint hash_map_get_mut_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return cvalue
+      else (t <- hash_map_get_mut_in_list_fwd T n0 key ls0; Return t)
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+Fixpoint hash_map_get_mut_in_list_back
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return (ListCons ckey ret ls0)
+      else (
+        ls1 <- hash_map_get_mut_in_list_back T n0 key ls0 ret;
+        Return (ListCons ckey cvalue ls1))
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::get_mut] *)
+Definition hash_map_get_mut_fwd
+  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hash_key_fwd key;
+    match self with
+    | mkHash_map_t i p i0 v =>
+      let i1 := vec_len (List_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (List_t T) v hash_mod;
+      t <- hash_map_get_mut_in_list_fwd T n0 key l;
+      Return t
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::get_mut] *)
+Definition hash_map_get_mut_back
+  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (ret : T) :
+  result (Hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hash_key_fwd key;
+    match self with
+    | mkHash_map_t i p i0 v =>
+      let i1 := vec_len (List_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (List_t T) v hash_mod;
+      l0 <- hash_map_get_mut_in_list_back T n0 key l ret;
+      v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
+      Return (mkHash_map_t i p i0 v0)
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::remove_from_list] *)
+Fixpoint hash_map_remove_from_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons ckey t tl =>
+      if ckey s= key
+      then
+        let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
+        match mv_ls with
+        | ListCons i cvalue tl0 => Return (Some cvalue)
+        | ListNil => Fail_ Failure
+        end
+      else (opt <- hash_map_remove_from_list_fwd T n0 key tl; Return opt)
+    | ListNil => Return None
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::remove_from_list] *)
+Fixpoint hash_map_remove_from_list_back
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons ckey t tl =>
+      if ckey s= key
+      then
+        let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
+        match mv_ls with
+        | ListCons i cvalue tl0 => Return tl0
+        | ListNil => Fail_ Failure
+        end
+      else (
+        tl0 <- hash_map_remove_from_list_back T n0 key tl;
+        Return (ListCons ckey t tl0))
+    | ListNil => Return ListNil
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::remove] *)
+Definition hash_map_remove_fwd
+  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
+  result (option T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hash_key_fwd key;
+    match self with
+    | mkHash_map_t i p i0 v =>
+      let i1 := vec_len (List_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (List_t T) v hash_mod;
+      x <- hash_map_remove_from_list_fwd T n0 key l;
+      match x with
+      | None => Return None
+      | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0)
+      end
+    end
+  end
+.
+
+(** [hashmap::HashMap::{0}::remove] *)
+Definition hash_map_remove_back
+  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
+  result (Hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hash_key_fwd key;
+    match self with
+    | mkHash_map_t i p i0 v =>
+      let i1 := vec_len (List_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (List_t T) v hash_mod;
+      x <- hash_map_remove_from_list_fwd T n0 key l;
+      match x with
+      | None =>
+        l0 <- hash_map_remove_from_list_back T n0 key l;
+        v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
+        Return (mkHash_map_t i p i0 v0)
+      | Some x0 =>
+        i2 <- usize_sub i 1%usize;
+        l0 <- hash_map_remove_from_list_back T n0 key l;
+        v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
+        Return (mkHash_map_t i2 p i0 v0)
+      end
+    end
+  end
+.
+
+(** [hashmap::test1] *)
+Definition test1_fwd (n : nat) : result unit :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hm <- hash_map_new_fwd u64 n0;
+    hm0 <- hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64);
+    hm1 <- hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64);
+    hm2 <- hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64);
+    hm3 <- hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64);
+    i <- hash_map_get_fwd u64 n0 hm3 (128%usize);
+    if negb (i s= 18%u64)
+    then Fail_ Failure
+    else (
+      hm4 <- hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64);
+      i0 <- hash_map_get_fwd u64 n0 hm4 (1024%usize);
+      if negb (i0 s= 56%u64)
+      then Fail_ Failure
+      else (
+        x <- hash_map_remove_fwd u64 n0 hm4 (1024%usize);
+        match x with
+        | None => Fail_ Failure
+        | Some x0 =>
+          if negb (x0 s= 56%u64)
+          then Fail_ Failure
+          else (
+            hm5 <- hash_map_remove_back u64 n0 hm4 (1024%usize);
+            i1 <- hash_map_get_fwd u64 n0 hm5 (0%usize);
+            if negb (i1 s= 42%u64)
+            then Fail_ Failure
+            else (
+              i2 <- hash_map_get_fwd u64 n0 hm5 (128%usize);
+              if negb (i2 s= 18%u64)
+              then Fail_ Failure
+              else (
+                i3 <- hash_map_get_fwd u64 n0 hm5 (1056%usize);
+                if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
+        end))
+  end
+.
+
+End Hashmap_Funs .
diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v
new file mode 100644
index 00000000..a3b68f9a
--- /dev/null
+++ b/tests/coq/hashmap/Hashmap_Types.v
@@ -0,0 +1,38 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: type definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module Hashmap_Types.
+
+(** [hashmap::List] *)
+Inductive List_t (T : Type) :=
+| ListCons : usize -> T -> List_t T -> List_t T
+| ListNil : List_t T
+.
+
+Arguments ListCons {T} _ _ _.
+Arguments ListNil {T}.
+
+(** [hashmap::HashMap] *)
+Record Hash_map_t (T : Type) :=
+mkHash_map_t {
+  Hash_map_num_entries : usize;
+  Hash_map_max_load_factor : (usize * usize);
+  Hash_map_max_load : usize;
+  Hash_map_slots : vec (List_t T);
+}
+.
+
+Arguments mkHash_map_t {T} _ _ _ _.
+Arguments Hash_map_num_entries {T}.
+Arguments Hash_map_max_load_factor {T}.
+Arguments Hash_map_max_load {T}.
+Arguments Hash_map_slots {T}.
+
+(** [core::num::u32::{9}::MAX] *)
+Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
+Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
+
+End Hashmap_Types .
diff --git a/tests/coq/hashmap/Hashmap__Funs.v b/tests/coq/hashmap/Hashmap__Funs.v
deleted file mode 100644
index 7d897c8a..00000000
--- a/tests/coq/hashmap/Hashmap__Funs.v
+++ /dev/null
@@ -1,541 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap]: function definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Require Export Hashmap__Types.
-Import Hashmap__Types.
-Module Hashmap__Funs.
-
-(** [hashmap::hash_key] *)
-Definition hash_key_fwd (k : usize) : result usize := Return k.
-
-(** [hashmap::HashMap::{0}::allocate_slots] *)
-Fixpoint hash_map_allocate_slots_fwd
-  (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
-  result (vec (List_t T))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n1 =>
-    if n0 s= 0%usize
-    then Return slots
-    else (
-      slots0 <- vec_push_back (List_t T) slots ListNil;
-      i <- usize_sub n0 1%usize;
-      v <- hash_map_allocate_slots_fwd T n1 slots0 i;
-      Return v)
-  end
-.
-
-(** [hashmap::HashMap::{0}::new_with_capacity] *)
-Definition hash_map_new_with_capacity_fwd
-  (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
-  (max_load_divisor : usize) :
-  result (Hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let v := vec_new (List_t T) in
-    slots <- hash_map_allocate_slots_fwd T n0 v capacity;
-    i <- usize_mul capacity max_load_dividend;
-    i0 <- usize_div i max_load_divisor;
-    Return (mkHash_map_t (0%usize) (max_load_dividend, max_load_divisor) i0
-      slots)
-  end
-.
-
-(** [hashmap::HashMap::{0}::new] *)
-Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hm <- hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize) (5%usize);
-    Return hm
-  end
-.
-
-(** [hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hash_map_clear_slots_fwd_back
-  (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
-  result (vec (List_t T))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let i0 := vec_len (List_t T) slots in
-    if i s< i0
-    then (
-      slots0 <- vec_index_mut_back (List_t T) slots i ListNil;
-      i1 <- usize_add i 1%usize;
-      slots1 <- hash_map_clear_slots_fwd_back T n0 slots0 i1;
-      Return slots1)
-    else Return slots
-  end
-.
-
-(** [hashmap::HashMap::{0}::clear] *)
-Definition hash_map_clear_fwd_back
-  (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match self with
-    | mkHash_map_t i p i0 v =>
-      v0 <- hash_map_clear_slots_fwd_back T n0 v (0%usize);
-      Return (mkHash_map_t (0%usize) p i0 v0)
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::len] *)
-Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize :=
-  match self with | mkHash_map_t i p i0 v => Return i end
-.
-
-(** [hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hash_map_insert_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
-  result bool
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return false
-      else (b <- hash_map_insert_in_list_fwd T n0 key value ls0; Return b)
-    | ListNil => Return true
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hash_map_insert_in_list_back
-  (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
-  result (List_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return (ListCons ckey value ls0)
-      else (
-        ls1 <- hash_map_insert_in_list_back T n0 key value ls0;
-        Return (ListCons ckey cvalue ls1))
-    | ListNil => let l := ListNil in Return (ListCons key value l)
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::insert_no_resize] *)
-Definition hash_map_insert_no_resize_fwd_back
-  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
-  result (Hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    match self with
-    | mkHash_map_t i p i0 v =>
-      let i1 := vec_len (List_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (List_t T) v hash_mod;
-      inserted <- hash_map_insert_in_list_fwd T n0 key value l;
-      if inserted
-      then (
-        i2 <- usize_add i 1%usize;
-        l0 <- hash_map_insert_in_list_back T n0 key value l;
-        v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
-        Return (mkHash_map_t i2 p i0 v0))
-      else (
-        l0 <- hash_map_insert_in_list_back T n0 key value l;
-        v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
-        Return (mkHash_map_t i p i0 v0))
-    end
-  end
-.
-
-(** [core::num::u32::{9}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
-(** [hashmap::HashMap::{0}::move_elements_from_list] *)
-Fixpoint hash_map_move_elements_from_list_fwd_back
-  (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
-  result (Hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons k v tl =>
-      ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v;
-      ntable1 <- hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl;
-      Return ntable1
-    | ListNil => Return ntable
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::move_elements] *)
-Fixpoint hash_map_move_elements_fwd_back
-  (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
-  (i : usize) :
-  result ((Hash_map_t T) * (vec (List_t T)))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let i0 := vec_len (List_t T) slots in
-    if i s< i0
-    then (
-      l <- vec_index_mut_fwd (List_t T) slots i;
-      let ls := mem_replace_fwd (List_t T) l ListNil in
-      ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
-      let l0 := mem_replace_back (List_t T) l ListNil in
-      slots0 <- vec_index_mut_back (List_t T) slots i l0;
-      i1 <- usize_add i 1%usize;
-      p <- hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1;
-      let (ntable1, slots1) := p in
-      Return (ntable1, slots1))
-    else Return (ntable, slots)
-  end
-.
-
-(** [hashmap::HashMap::{0}::try_resize] *)
-Definition hash_map_try_resize_fwd_back
-  (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
-    match self with
-    | mkHash_map_t i p i0 v =>
-      let capacity := vec_len (List_t T) v in
-      n1 <- usize_div max_usize 2%usize;
-      let (i1, i2) := p in
-      i3 <- usize_div n1 i1;
-      if capacity s<= i3
-      then (
-        i4 <- usize_mul capacity 2%usize;
-        ntable <- hash_map_new_with_capacity_fwd T n0 i4 i1 i2;
-        p0 <- hash_map_move_elements_fwd_back T n0 ntable v (0%usize);
-        let (ntable0, _) := p0 in
-        match ntable0 with
-        | mkHash_map_t i5 p1 i6 v0 => Return (mkHash_map_t i (i1, i2) i6 v0)
-        end)
-      else Return (mkHash_map_t i (i1, i2) i0 v)
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::insert] *)
-Definition hash_map_insert_fwd_back
-  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
-  result (Hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <- hash_map_insert_no_resize_fwd_back T n0 self key value;
-    i <- hash_map_len_fwd T self0;
-    match self0 with
-    | mkHash_map_t i0 p i1 v =>
-      if i s> i1
-      then (
-        self1 <- hash_map_try_resize_fwd_back T n0 (mkHash_map_t i0 p i1 v);
-        Return self1)
-      else Return (mkHash_map_t i0 p i1 v)
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
-Fixpoint hash_map_contains_key_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons ckey t ls0 =>
-      if ckey s= key
-      then Return true
-      else (b <- hash_map_contains_key_in_list_fwd T n0 key ls0; Return b)
-    | ListNil => Return false
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::contains_key] *)
-Definition hash_map_contains_key_fwd
-  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result bool :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    match self with
-    | mkHash_map_t i p i0 v =>
-      let i1 := vec_len (List_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_fwd (List_t T) v hash_mod;
-      b <- hash_map_contains_key_in_list_fwd T n0 key l;
-      Return b
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::get_in_list] *)
-Fixpoint hash_map_get_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return cvalue
-      else (t <- hash_map_get_in_list_fwd T n0 key ls0; Return t)
-    | ListNil => Fail_ Failure
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::get] *)
-Definition hash_map_get_fwd
-  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    match self with
-    | mkHash_map_t i p i0 v =>
-      let i1 := vec_len (List_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_fwd (List_t T) v hash_mod;
-      t <- hash_map_get_in_list_fwd T n0 key l;
-      Return t
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hash_map_get_mut_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return cvalue
-      else (t <- hash_map_get_mut_in_list_fwd T n0 key ls0; Return t)
-    | ListNil => Fail_ Failure
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hash_map_get_mut_in_list_back
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) :
-  result (List_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return (ListCons ckey ret ls0)
-      else (
-        ls1 <- hash_map_get_mut_in_list_back T n0 key ls0 ret;
-        Return (ListCons ckey cvalue ls1))
-    | ListNil => Fail_ Failure
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::get_mut] *)
-Definition hash_map_get_mut_fwd
-  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    match self with
-    | mkHash_map_t i p i0 v =>
-      let i1 := vec_len (List_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (List_t T) v hash_mod;
-      t <- hash_map_get_mut_in_list_fwd T n0 key l;
-      Return t
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::get_mut] *)
-Definition hash_map_get_mut_back
-  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (ret : T) :
-  result (Hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    match self with
-    | mkHash_map_t i p i0 v =>
-      let i1 := vec_len (List_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (List_t T) v hash_mod;
-      l0 <- hash_map_get_mut_in_list_back T n0 key l ret;
-      v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
-      Return (mkHash_map_t i p i0 v0)
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hash_map_remove_from_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons ckey t tl =>
-      if ckey s= key
-      then
-        let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
-        match mv_ls with
-        | ListCons i cvalue tl0 => Return (Some cvalue)
-        | ListNil => Fail_ Failure
-        end
-      else (opt <- hash_map_remove_from_list_fwd T n0 key tl; Return opt)
-    | ListNil => Return None
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hash_map_remove_from_list_back
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | ListCons ckey t tl =>
-      if ckey s= key
-      then
-        let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
-        match mv_ls with
-        | ListCons i cvalue tl0 => Return tl0
-        | ListNil => Fail_ Failure
-        end
-      else (
-        tl0 <- hash_map_remove_from_list_back T n0 key tl;
-        Return (ListCons ckey t tl0))
-    | ListNil => Return ListNil
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::remove] *)
-Definition hash_map_remove_fwd
-  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
-  result (option T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    match self with
-    | mkHash_map_t i p i0 v =>
-      let i1 := vec_len (List_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (List_t T) v hash_mod;
-      x <- hash_map_remove_from_list_fwd T n0 key l;
-      match x with
-      | None => Return None
-      | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0)
-      end
-    end
-  end
-.
-
-(** [hashmap::HashMap::{0}::remove] *)
-Definition hash_map_remove_back
-  (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
-  result (Hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hash_key_fwd key;
-    match self with
-    | mkHash_map_t i p i0 v =>
-      let i1 := vec_len (List_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (List_t T) v hash_mod;
-      x <- hash_map_remove_from_list_fwd T n0 key l;
-      match x with
-      | None =>
-        l0 <- hash_map_remove_from_list_back T n0 key l;
-        v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
-        Return (mkHash_map_t i p i0 v0)
-      | Some x0 =>
-        i2 <- usize_sub i 1%usize;
-        l0 <- hash_map_remove_from_list_back T n0 key l;
-        v0 <- vec_index_mut_back (List_t T) v hash_mod l0;
-        Return (mkHash_map_t i2 p i0 v0)
-      end
-    end
-  end
-.
-
-(** [hashmap::test1] *)
-Definition test1_fwd (n : nat) : result unit :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hm <- hash_map_new_fwd u64 n0;
-    hm0 <- hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64);
-    hm1 <- hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64);
-    hm2 <- hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64);
-    hm3 <- hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64);
-    i <- hash_map_get_fwd u64 n0 hm3 (128%usize);
-    if negb (i s= 18%u64)
-    then Fail_ Failure
-    else (
-      hm4 <- hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64);
-      i0 <- hash_map_get_fwd u64 n0 hm4 (1024%usize);
-      if negb (i0 s= 56%u64)
-      then Fail_ Failure
-      else (
-        x <- hash_map_remove_fwd u64 n0 hm4 (1024%usize);
-        match x with
-        | None => Fail_ Failure
-        | Some x0 =>
-          if negb (x0 s= 56%u64)
-          then Fail_ Failure
-          else (
-            hm5 <- hash_map_remove_back u64 n0 hm4 (1024%usize);
-            i1 <- hash_map_get_fwd u64 n0 hm5 (0%usize);
-            if negb (i1 s= 42%u64)
-            then Fail_ Failure
-            else (
-              i2 <- hash_map_get_fwd u64 n0 hm5 (128%usize);
-              if negb (i2 s= 18%u64)
-              then Fail_ Failure
-              else (
-                i3 <- hash_map_get_fwd u64 n0 hm5 (1056%usize);
-                if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
-        end))
-  end
-.
-
-End Hashmap__Funs .
diff --git a/tests/coq/hashmap/Hashmap__Types.v b/tests/coq/hashmap/Hashmap__Types.v
deleted file mode 100644
index e1add060..00000000
--- a/tests/coq/hashmap/Hashmap__Types.v
+++ /dev/null
@@ -1,38 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap]: type definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Module Hashmap__Types.
-
-(** [hashmap::List] *)
-Inductive List_t (T : Type) :=
-| ListCons : usize -> T -> List_t T -> List_t T
-| ListNil : List_t T
-.
-
-Arguments ListCons {T} _ _ _.
-Arguments ListNil {T}.
-
-(** [hashmap::HashMap] *)
-Record Hash_map_t (T : Type) :=
-mkHash_map_t {
-  Hash_map_num_entries : usize;
-  Hash_map_max_load_factor : (usize * usize);
-  Hash_map_max_load : usize;
-  Hash_map_slots : vec (List_t T);
-}
-.
-
-Arguments mkHash_map_t {T} _ _ _ _.
-Arguments Hash_map_num_entries {T}.
-Arguments Hash_map_max_load_factor {T}.
-Arguments Hash_map_max_load {T}.
-Arguments Hash_map_slots {T}.
-
-(** [core::num::u32::{9}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
-End Hashmap__Types .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
new file mode 100644
index 00000000..b4351dc3
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -0,0 +1,598 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export HashmapMain_Types.
+Import HashmapMain_Types.
+Require Export HashmapMain_Opaque.
+Import HashmapMain_Opaque.
+Module HashmapMain_Funs.
+
+(** [hashmap_main::hashmap::hash_key] *)
+Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
+
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+Fixpoint hashmap_hash_map_allocate_slots_fwd
+  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
+  result (vec (Hashmap_list_t T))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    if n0 s= 0%usize
+    then Return slots
+    else (
+      slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil;
+      i <- usize_sub n0 1%usize;
+      v <- hashmap_hash_map_allocate_slots_fwd T n1 slots0 i;
+      Return v)
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
+Definition hashmap_hash_map_new_with_capacity_fwd
+  (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
+  (max_load_divisor : usize) :
+  result (Hashmap_hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let v := vec_new (Hashmap_list_t T) in
+    slots <- hashmap_hash_map_allocate_slots_fwd T n0 v capacity;
+    i <- usize_mul capacity max_load_dividend;
+    i0 <- usize_div i max_load_divisor;
+    Return (mkHashmap_hash_map_t (0%usize) (max_load_dividend,
+      max_load_divisor) i0 slots)
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::new] *)
+Definition hashmap_hash_map_new_fwd
+  (T : Type) (n : nat) : result (Hashmap_hash_map_t T) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hm <-
+      hashmap_hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize)
+        (5%usize);
+    Return hm
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
+Fixpoint hashmap_hash_map_clear_slots_fwd_back
+  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
+  result (vec (Hashmap_list_t T))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let i0 := vec_len (Hashmap_list_t T) slots in
+    if i s< i0
+    then (
+      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
+      i1 <- usize_add i 1%usize;
+      slots1 <- hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1;
+      Return slots1)
+    else Return slots
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+Definition hashmap_hash_map_clear_fwd_back
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
+  result (Hashmap_hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      v0 <- hashmap_hash_map_clear_slots_fwd_back T n0 v (0%usize);
+      Return (mkHashmap_hash_map_t (0%usize) p i0 v0)
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::len] *)
+Definition hashmap_hash_map_len_fwd
+  (T : Type) (self : Hashmap_hash_map_t T) : result usize :=
+  match self with | mkHashmap_hash_map_t i p i0 v => Return i end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+Fixpoint hashmap_hash_map_insert_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
+  result bool
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return false
+      else (
+        b <- hashmap_hash_map_insert_in_list_fwd T n0 key value ls0; Return b)
+    | HashmapListNil => Return true
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+Fixpoint hashmap_hash_map_insert_in_list_back
+  (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
+  result (Hashmap_list_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return (HashmapListCons ckey value ls0)
+      else (
+        ls1 <- hashmap_hash_map_insert_in_list_back T n0 key value ls0;
+        Return (HashmapListCons ckey cvalue ls1))
+    | HashmapListNil =>
+      let l := HashmapListNil in Return (HashmapListCons key value l)
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
+Definition hashmap_hash_map_insert_no_resize_fwd_back
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
+  :
+  result (Hashmap_hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hashmap_hash_key_fwd key;
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      let i1 := vec_len (Hashmap_list_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
+      inserted <- hashmap_hash_map_insert_in_list_fwd T n0 key value l;
+      if inserted
+      then (
+        i2 <- usize_add i 1%usize;
+        l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l;
+        v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
+        Return (mkHashmap_hash_map_t i2 p i0 v0))
+      else (
+        l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l;
+        v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
+        Return (mkHashmap_hash_map_t i p i0 v0))
+    end
+  end
+.
+
+(** [core::num::u32::{9}::MAX] *)
+Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
+Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
+
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back
+  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
+  :
+  result (Hashmap_hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons k v tl =>
+      ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v;
+      ntable1 <-
+        hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl;
+      Return ntable1
+    | HashmapListNil => Return ntable
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+Fixpoint hashmap_hash_map_move_elements_fwd_back
+  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
+  (slots : vec (Hashmap_list_t T)) (i : usize) :
+  result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let i0 := vec_len (Hashmap_list_t T) slots in
+    if i s< i0
+    then (
+      l <- vec_index_mut_fwd (Hashmap_list_t T) slots i;
+      let ls := mem_replace_fwd (Hashmap_list_t T) l HashmapListNil in
+      ntable0 <-
+        hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
+      let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in
+      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0;
+      i1 <- usize_add i 1%usize;
+      p <- hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1;
+      let (ntable1, slots1) := p in
+      Return (ntable1, slots1))
+    else Return (ntable, slots)
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
+Definition hashmap_hash_map_try_resize_fwd_back
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
+  result (Hashmap_hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      let capacity := vec_len (Hashmap_list_t T) v in
+      n1 <- usize_div max_usize 2%usize;
+      let (i1, i2) := p in
+      i3 <- usize_div n1 i1;
+      if capacity s<= i3
+      then (
+        i4 <- usize_mul capacity 2%usize;
+        ntable <- hashmap_hash_map_new_with_capacity_fwd T n0 i4 i1 i2;
+        p0 <- hashmap_hash_map_move_elements_fwd_back T n0 ntable v (0%usize);
+        let (ntable0, _) := p0 in
+        match ntable0 with
+        | mkHashmap_hash_map_t i5 p1 i6 v0 =>
+          Return (mkHashmap_hash_map_t i (i1, i2) i6 v0)
+        end)
+      else Return (mkHashmap_hash_map_t i (i1, i2) i0 v)
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
+Definition hashmap_hash_map_insert_fwd_back
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
+  :
+  result (Hashmap_hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 self key value;
+    i <- hashmap_hash_map_len_fwd T self0;
+    match self0 with
+    | mkHashmap_hash_map_t i0 p i1 v =>
+      if i s> i1
+      then (
+        self1 <-
+          hashmap_hash_map_try_resize_fwd_back T n0 (mkHashmap_hash_map_t i0 p
+            i1 v);
+        Return self1)
+      else Return (mkHashmap_hash_map_t i0 p i1 v)
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+Fixpoint hashmap_hash_map_contains_key_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons ckey t ls0 =>
+      if ckey s= key
+      then Return true
+      else (
+        b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0; Return b)
+    | HashmapListNil => Return false
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
+Definition hashmap_hash_map_contains_key_fwd
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
+  result bool
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hashmap_hash_key_fwd key;
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      let i1 := vec_len (Hashmap_list_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_fwd (Hashmap_list_t T) v hash_mod;
+      b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key l;
+      Return b
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+Fixpoint hashmap_hash_map_get_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return cvalue
+      else (t <- hashmap_hash_map_get_in_list_fwd T n0 key ls0; Return t)
+    | HashmapListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::get] *)
+Definition hashmap_hash_map_get_fwd
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
+  result T
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hashmap_hash_key_fwd key;
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      let i1 := vec_len (Hashmap_list_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_fwd (Hashmap_list_t T) v hash_mod;
+      t <- hashmap_hash_map_get_in_list_fwd T n0 key l;
+      Return t
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+Fixpoint hashmap_hash_map_get_mut_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return cvalue
+      else (t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0; Return t)
+    | HashmapListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+Fixpoint hashmap_hash_map_get_mut_in_list_back
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) :
+  result (Hashmap_list_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons ckey cvalue ls0 =>
+      if ckey s= key
+      then Return (HashmapListCons ckey ret ls0)
+      else (
+        ls1 <- hashmap_hash_map_get_mut_in_list_back T n0 key ls0 ret;
+        Return (HashmapListCons ckey cvalue ls1))
+    | HashmapListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+Definition hashmap_hash_map_get_mut_fwd
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
+  result T
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hashmap_hash_key_fwd key;
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      let i1 := vec_len (Hashmap_list_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
+      t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key l;
+      Return t
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+Definition hashmap_hash_map_get_mut_back
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (ret : T) :
+  result (Hashmap_hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hashmap_hash_key_fwd key;
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      let i1 := vec_len (Hashmap_list_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
+      l0 <- hashmap_hash_map_get_mut_in_list_back T n0 key l ret;
+      v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
+      Return (mkHashmap_hash_map_t i p i0 v0)
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+Fixpoint hashmap_hash_map_remove_from_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
+  result (option T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons ckey t tl =>
+      if ckey s= key
+      then
+        let mv_ls :=
+          mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
+            HashmapListNil in
+        match mv_ls with
+        | HashmapListCons i cvalue tl0 => Return (Some cvalue)
+        | HashmapListNil => Fail_ Failure
+        end
+      else (
+        opt <- hashmap_hash_map_remove_from_list_fwd T n0 key tl; Return opt)
+    | HashmapListNil => Return None
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+Fixpoint hashmap_hash_map_remove_from_list_back
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
+  result (Hashmap_list_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | HashmapListCons ckey t tl =>
+      if ckey s= key
+      then
+        let mv_ls :=
+          mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
+            HashmapListNil in
+        match mv_ls with
+        | HashmapListCons i cvalue tl0 => Return tl0
+        | HashmapListNil => Fail_ Failure
+        end
+      else (
+        tl0 <- hashmap_hash_map_remove_from_list_back T n0 key tl;
+        Return (HashmapListCons ckey t tl0))
+    | HashmapListNil => Return HashmapListNil
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+Definition hashmap_hash_map_remove_fwd
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
+  result (option T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hashmap_hash_key_fwd key;
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      let i1 := vec_len (Hashmap_list_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
+      x <- hashmap_hash_map_remove_from_list_fwd T n0 key l;
+      match x with
+      | None => Return None
+      | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0)
+      end
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+Definition hashmap_hash_map_remove_back
+  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
+  result (Hashmap_hash_map_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hash <- hashmap_hash_key_fwd key;
+    match self with
+    | mkHashmap_hash_map_t i p i0 v =>
+      let i1 := vec_len (Hashmap_list_t T) v in
+      hash_mod <- usize_rem hash i1;
+      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
+      x <- hashmap_hash_map_remove_from_list_fwd T n0 key l;
+      match x with
+      | None =>
+        l0 <- hashmap_hash_map_remove_from_list_back T n0 key l;
+        v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
+        Return (mkHashmap_hash_map_t i p i0 v0)
+      | Some x0 =>
+        i2 <- usize_sub i 1%usize;
+        l0 <- hashmap_hash_map_remove_from_list_back T n0 key l;
+        v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
+        Return (mkHashmap_hash_map_t i2 p i0 v0)
+      end
+    end
+  end
+.
+
+(** [hashmap_main::hashmap::test1] *)
+Definition hashmap_test1_fwd (n : nat) : result unit :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    hm <- hashmap_hash_map_new_fwd u64 n0;
+    hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64);
+    hm1 <- hashmap_hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64);
+    hm2 <- hashmap_hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64);
+    hm3 <- hashmap_hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64);
+    i <- hashmap_hash_map_get_fwd u64 n0 hm3 (128%usize);
+    if negb (i s= 18%u64)
+    then Fail_ Failure
+    else (
+      hm4 <- hashmap_hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64);
+      i0 <- hashmap_hash_map_get_fwd u64 n0 hm4 (1024%usize);
+      if negb (i0 s= 56%u64)
+      then Fail_ Failure
+      else (
+        x <- hashmap_hash_map_remove_fwd u64 n0 hm4 (1024%usize);
+        match x with
+        | None => Fail_ Failure
+        | Some x0 =>
+          if negb (x0 s= 56%u64)
+          then Fail_ Failure
+          else (
+            hm5 <- hashmap_hash_map_remove_back u64 n0 hm4 (1024%usize);
+            i1 <- hashmap_hash_map_get_fwd u64 n0 hm5 (0%usize);
+            if negb (i1 s= 42%u64)
+            then Fail_ Failure
+            else (
+              i2 <- hashmap_hash_map_get_fwd u64 n0 hm5 (128%usize);
+              if negb (i2 s= 18%u64)
+              then Fail_ Failure
+              else (
+                i3 <- hashmap_hash_map_get_fwd u64 n0 hm5 (1056%usize);
+                if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
+        end))
+  end
+.
+
+(** [hashmap_main::insert_on_disk] *)
+Definition insert_on_disk_fwd
+  (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    p <- hashmap_utils_deserialize_fwd st;
+    let (st0, hm) := p in
+    hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm key value;
+    p0 <- hashmap_utils_serialize_fwd hm0 st0;
+    let (st1, _) := p0 in
+    Return (st1, tt)
+  end
+.
+
+(** [hashmap_main::main] *)
+Definition main_fwd : result unit := Return tt.
+
+(** Unit test for [hashmap_main::main] *)
+Check (main_fwd )%return.
+
+End HashmapMain_Funs .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
new file mode 100644
index 00000000..6152b94b
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
@@ -0,0 +1,21 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: opaque function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export HashmapMain_Types.
+Import HashmapMain_Types.
+Module HashmapMain_Opaque.
+
+(** [hashmap_main::hashmap_utils::deserialize] *)
+Axiom hashmap_utils_deserialize_fwd
+  : state -> result (state * (Hashmap_hash_map_t u64))
+.
+
+(** [hashmap_main::hashmap_utils::serialize] *)
+Axiom hashmap_utils_serialize_fwd
+  : Hashmap_hash_map_t u64 -> state -> result (state * unit)
+.
+
+End HashmapMain_Opaque .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
new file mode 100644
index 00000000..01243baf
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
@@ -0,0 +1,41 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: type definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module HashmapMain_Types.
+
+(** [hashmap_main::hashmap::List] *)
+Inductive Hashmap_list_t (T : Type) :=
+| HashmapListCons : usize -> T -> Hashmap_list_t T -> Hashmap_list_t T
+| HashmapListNil : Hashmap_list_t T
+.
+
+Arguments HashmapListCons {T} _ _ _.
+Arguments HashmapListNil {T}.
+
+(** [hashmap_main::hashmap::HashMap] *)
+Record Hashmap_hash_map_t (T : Type) :=
+mkHashmap_hash_map_t {
+  Hashmap_hash_map_num_entries : usize;
+  Hashmap_hash_map_max_load_factor : (usize * usize);
+  Hashmap_hash_map_max_load : usize;
+  Hashmap_hash_map_slots : vec (Hashmap_list_t T);
+}
+.
+
+Arguments mkHashmap_hash_map_t {T} _ _ _ _.
+Arguments Hashmap_hash_map_num_entries {T}.
+Arguments Hashmap_hash_map_max_load_factor {T}.
+Arguments Hashmap_hash_map_max_load {T}.
+Arguments Hashmap_hash_map_slots {T}.
+
+(** [core::num::u32::{9}::MAX] *)
+Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
+Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End HashmapMain_Types .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Funs.v b/tests/coq/hashmap_on_disk/HashmapMain__Funs.v
deleted file mode 100644
index 249adbe9..00000000
--- a/tests/coq/hashmap_on_disk/HashmapMain__Funs.v
+++ /dev/null
@@ -1,598 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: function definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Require Export HashmapMain__Types.
-Import HashmapMain__Types.
-Require Export HashmapMain__Opaque.
-Import HashmapMain__Opaque.
-Module HashmapMain__Funs.
-
-(** [hashmap_main::hashmap::hash_key] *)
-Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
-
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
-Fixpoint hashmap_hash_map_allocate_slots_fwd
-  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
-  result (vec (Hashmap_list_t T))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n1 =>
-    if n0 s= 0%usize
-    then Return slots
-    else (
-      slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil;
-      i <- usize_sub n0 1%usize;
-      v <- hashmap_hash_map_allocate_slots_fwd T n1 slots0 i;
-      Return v)
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
-Definition hashmap_hash_map_new_with_capacity_fwd
-  (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
-  (max_load_divisor : usize) :
-  result (Hashmap_hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let v := vec_new (Hashmap_list_t T) in
-    slots <- hashmap_hash_map_allocate_slots_fwd T n0 v capacity;
-    i <- usize_mul capacity max_load_dividend;
-    i0 <- usize_div i max_load_divisor;
-    Return (mkHashmap_hash_map_t (0%usize) (max_load_dividend,
-      max_load_divisor) i0 slots)
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::new] *)
-Definition hashmap_hash_map_new_fwd
-  (T : Type) (n : nat) : result (Hashmap_hash_map_t T) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hm <-
-      hashmap_hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize)
-        (5%usize);
-    Return hm
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hashmap_hash_map_clear_slots_fwd_back
-  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
-  result (vec (Hashmap_list_t T))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let i0 := vec_len (Hashmap_list_t T) slots in
-    if i s< i0
-    then (
-      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
-      i1 <- usize_add i 1%usize;
-      slots1 <- hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1;
-      Return slots1)
-    else Return slots
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
-Definition hashmap_hash_map_clear_fwd_back
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
-  result (Hashmap_hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      v0 <- hashmap_hash_map_clear_slots_fwd_back T n0 v (0%usize);
-      Return (mkHashmap_hash_map_t (0%usize) p i0 v0)
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::len] *)
-Definition hashmap_hash_map_len_fwd
-  (T : Type) (self : Hashmap_hash_map_t T) : result usize :=
-  match self with | mkHashmap_hash_map_t i p i0 v => Return i end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hashmap_hash_map_insert_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
-  result bool
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return false
-      else (
-        b <- hashmap_hash_map_insert_in_list_fwd T n0 key value ls0; Return b)
-    | HashmapListNil => Return true
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hashmap_hash_map_insert_in_list_back
-  (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
-  result (Hashmap_list_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return (HashmapListCons ckey value ls0)
-      else (
-        ls1 <- hashmap_hash_map_insert_in_list_back T n0 key value ls0;
-        Return (HashmapListCons ckey cvalue ls1))
-    | HashmapListNil =>
-      let l := HashmapListNil in Return (HashmapListCons key value l)
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
-Definition hashmap_hash_map_insert_no_resize_fwd_back
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
-  :
-  result (Hashmap_hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      let i1 := vec_len (Hashmap_list_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
-      inserted <- hashmap_hash_map_insert_in_list_fwd T n0 key value l;
-      if inserted
-      then (
-        i2 <- usize_add i 1%usize;
-        l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l;
-        v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
-        Return (mkHashmap_hash_map_t i2 p i0 v0))
-      else (
-        l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l;
-        v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
-        Return (mkHashmap_hash_map_t i p i0 v0))
-    end
-  end
-.
-
-(** [core::num::u32::{9}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
-Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back
-  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
-  :
-  result (Hashmap_hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons k v tl =>
-      ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v;
-      ntable1 <-
-        hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl;
-      Return ntable1
-    | HashmapListNil => Return ntable
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
-Fixpoint hashmap_hash_map_move_elements_fwd_back
-  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
-  (slots : vec (Hashmap_list_t T)) (i : usize) :
-  result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T)))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    let i0 := vec_len (Hashmap_list_t T) slots in
-    if i s< i0
-    then (
-      l <- vec_index_mut_fwd (Hashmap_list_t T) slots i;
-      let ls := mem_replace_fwd (Hashmap_list_t T) l HashmapListNil in
-      ntable0 <-
-        hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
-      let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in
-      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0;
-      i1 <- usize_add i 1%usize;
-      p <- hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1;
-      let (ntable1, slots1) := p in
-      Return (ntable1, slots1))
-    else Return (ntable, slots)
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
-Definition hashmap_hash_map_try_resize_fwd_back
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
-  result (Hashmap_hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      let capacity := vec_len (Hashmap_list_t T) v in
-      n1 <- usize_div max_usize 2%usize;
-      let (i1, i2) := p in
-      i3 <- usize_div n1 i1;
-      if capacity s<= i3
-      then (
-        i4 <- usize_mul capacity 2%usize;
-        ntable <- hashmap_hash_map_new_with_capacity_fwd T n0 i4 i1 i2;
-        p0 <- hashmap_hash_map_move_elements_fwd_back T n0 ntable v (0%usize);
-        let (ntable0, _) := p0 in
-        match ntable0 with
-        | mkHashmap_hash_map_t i5 p1 i6 v0 =>
-          Return (mkHashmap_hash_map_t i (i1, i2) i6 v0)
-        end)
-      else Return (mkHashmap_hash_map_t i (i1, i2) i0 v)
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
-Definition hashmap_hash_map_insert_fwd_back
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
-  :
-  result (Hashmap_hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 self key value;
-    i <- hashmap_hash_map_len_fwd T self0;
-    match self0 with
-    | mkHashmap_hash_map_t i0 p i1 v =>
-      if i s> i1
-      then (
-        self1 <-
-          hashmap_hash_map_try_resize_fwd_back T n0 (mkHashmap_hash_map_t i0 p
-            i1 v);
-        Return self1)
-      else Return (mkHashmap_hash_map_t i0 p i1 v)
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
-Fixpoint hashmap_hash_map_contains_key_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons ckey t ls0 =>
-      if ckey s= key
-      then Return true
-      else (
-        b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0; Return b)
-    | HashmapListNil => Return false
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
-Definition hashmap_hash_map_contains_key_fwd
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
-  result bool
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      let i1 := vec_len (Hashmap_list_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_fwd (Hashmap_list_t T) v hash_mod;
-      b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key l;
-      Return b
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
-Fixpoint hashmap_hash_map_get_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return cvalue
-      else (t <- hashmap_hash_map_get_in_list_fwd T n0 key ls0; Return t)
-    | HashmapListNil => Fail_ Failure
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::get] *)
-Definition hashmap_hash_map_get_fwd
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
-  result T
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      let i1 := vec_len (Hashmap_list_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_fwd (Hashmap_list_t T) v hash_mod;
-      t <- hashmap_hash_map_get_in_list_fwd T n0 key l;
-      Return t
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hashmap_hash_map_get_mut_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return cvalue
-      else (t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0; Return t)
-    | HashmapListNil => Fail_ Failure
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hashmap_hash_map_get_mut_in_list_back
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) :
-  result (Hashmap_list_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return (HashmapListCons ckey ret ls0)
-      else (
-        ls1 <- hashmap_hash_map_get_mut_in_list_back T n0 key ls0 ret;
-        Return (HashmapListCons ckey cvalue ls1))
-    | HashmapListNil => Fail_ Failure
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
-Definition hashmap_hash_map_get_mut_fwd
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
-  result T
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      let i1 := vec_len (Hashmap_list_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
-      t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key l;
-      Return t
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
-Definition hashmap_hash_map_get_mut_back
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (ret : T) :
-  result (Hashmap_hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      let i1 := vec_len (Hashmap_list_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
-      l0 <- hashmap_hash_map_get_mut_in_list_back T n0 key l ret;
-      v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
-      Return (mkHashmap_hash_map_t i p i0 v0)
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hashmap_hash_map_remove_from_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
-  result (option T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons ckey t tl =>
-      if ckey s= key
-      then
-        let mv_ls :=
-          mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
-            HashmapListNil in
-        match mv_ls with
-        | HashmapListCons i cvalue tl0 => Return (Some cvalue)
-        | HashmapListNil => Fail_ Failure
-        end
-      else (
-        opt <- hashmap_hash_map_remove_from_list_fwd T n0 key tl; Return opt)
-    | HashmapListNil => Return None
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hashmap_hash_map_remove_from_list_back
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
-  result (Hashmap_list_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match ls with
-    | HashmapListCons ckey t tl =>
-      if ckey s= key
-      then
-        let mv_ls :=
-          mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
-            HashmapListNil in
-        match mv_ls with
-        | HashmapListCons i cvalue tl0 => Return tl0
-        | HashmapListNil => Fail_ Failure
-        end
-      else (
-        tl0 <- hashmap_hash_map_remove_from_list_back T n0 key tl;
-        Return (HashmapListCons ckey t tl0))
-    | HashmapListNil => Return HashmapListNil
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
-Definition hashmap_hash_map_remove_fwd
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
-  result (option T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      let i1 := vec_len (Hashmap_list_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
-      x <- hashmap_hash_map_remove_from_list_fwd T n0 key l;
-      match x with
-      | None => Return None
-      | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0)
-      end
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
-Definition hashmap_hash_map_remove_back
-  (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
-  result (Hashmap_hash_map_t T)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hash <- hashmap_hash_key_fwd key;
-    match self with
-    | mkHashmap_hash_map_t i p i0 v =>
-      let i1 := vec_len (Hashmap_list_t T) v in
-      hash_mod <- usize_rem hash i1;
-      l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod;
-      x <- hashmap_hash_map_remove_from_list_fwd T n0 key l;
-      match x with
-      | None =>
-        l0 <- hashmap_hash_map_remove_from_list_back T n0 key l;
-        v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
-        Return (mkHashmap_hash_map_t i p i0 v0)
-      | Some x0 =>
-        i2 <- usize_sub i 1%usize;
-        l0 <- hashmap_hash_map_remove_from_list_back T n0 key l;
-        v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0;
-        Return (mkHashmap_hash_map_t i2 p i0 v0)
-      end
-    end
-  end
-.
-
-(** [hashmap_main::hashmap::test1] *)
-Definition hashmap_test1_fwd (n : nat) : result unit :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    hm <- hashmap_hash_map_new_fwd u64 n0;
-    hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64);
-    hm1 <- hashmap_hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64);
-    hm2 <- hashmap_hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64);
-    hm3 <- hashmap_hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64);
-    i <- hashmap_hash_map_get_fwd u64 n0 hm3 (128%usize);
-    if negb (i s= 18%u64)
-    then Fail_ Failure
-    else (
-      hm4 <- hashmap_hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64);
-      i0 <- hashmap_hash_map_get_fwd u64 n0 hm4 (1024%usize);
-      if negb (i0 s= 56%u64)
-      then Fail_ Failure
-      else (
-        x <- hashmap_hash_map_remove_fwd u64 n0 hm4 (1024%usize);
-        match x with
-        | None => Fail_ Failure
-        | Some x0 =>
-          if negb (x0 s= 56%u64)
-          then Fail_ Failure
-          else (
-            hm5 <- hashmap_hash_map_remove_back u64 n0 hm4 (1024%usize);
-            i1 <- hashmap_hash_map_get_fwd u64 n0 hm5 (0%usize);
-            if negb (i1 s= 42%u64)
-            then Fail_ Failure
-            else (
-              i2 <- hashmap_hash_map_get_fwd u64 n0 hm5 (128%usize);
-              if negb (i2 s= 18%u64)
-              then Fail_ Failure
-              else (
-                i3 <- hashmap_hash_map_get_fwd u64 n0 hm5 (1056%usize);
-                if negb (i3 s= 256%u64) then Fail_ Failure else Return tt)))
-        end))
-  end
-.
-
-(** [hashmap_main::insert_on_disk] *)
-Definition insert_on_disk_fwd
-  (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <- hashmap_utils_deserialize_fwd st;
-    let (st0, hm) := p in
-    hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm key value;
-    p0 <- hashmap_utils_serialize_fwd hm0 st0;
-    let (st1, _) := p0 in
-    Return (st1, tt)
-  end
-.
-
-(** [hashmap_main::main] *)
-Definition main_fwd : result unit := Return tt.
-
-(** Unit test for [hashmap_main::main] *)
-Check (main_fwd )%return.
-
-End HashmapMain__Funs .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v
deleted file mode 100644
index 4b6db927..00000000
--- a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v
+++ /dev/null
@@ -1,21 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: opaque function definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Require Export HashmapMain__Types.
-Import HashmapMain__Types.
-Module HashmapMain__Opaque.
-
-(** [hashmap_main::hashmap_utils::deserialize] *)
-Axiom hashmap_utils_deserialize_fwd
-  : state -> result (state * (Hashmap_hash_map_t u64))
-.
-
-(** [hashmap_main::hashmap_utils::serialize] *)
-Axiom hashmap_utils_serialize_fwd
-  : Hashmap_hash_map_t u64 -> state -> result (state * unit)
-.
-
-End HashmapMain__Opaque .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Types.v b/tests/coq/hashmap_on_disk/HashmapMain__Types.v
deleted file mode 100644
index 5d609937..00000000
--- a/tests/coq/hashmap_on_disk/HashmapMain__Types.v
+++ /dev/null
@@ -1,41 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: type definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Module HashmapMain__Types.
-
-(** [hashmap_main::hashmap::List] *)
-Inductive Hashmap_list_t (T : Type) :=
-| HashmapListCons : usize -> T -> Hashmap_list_t T -> Hashmap_list_t T
-| HashmapListNil : Hashmap_list_t T
-.
-
-Arguments HashmapListCons {T} _ _ _.
-Arguments HashmapListNil {T}.
-
-(** [hashmap_main::hashmap::HashMap] *)
-Record Hashmap_hash_map_t (T : Type) :=
-mkHashmap_hash_map_t {
-  Hashmap_hash_map_num_entries : usize;
-  Hashmap_hash_map_max_load_factor : (usize * usize);
-  Hashmap_hash_map_max_load : usize;
-  Hashmap_hash_map_slots : vec (Hashmap_list_t T);
-}
-.
-
-Arguments mkHashmap_hash_map_t {T} _ _ _ _.
-Arguments Hashmap_hash_map_num_entries {T}.
-Arguments Hashmap_hash_map_max_load_factor {T}.
-Arguments Hashmap_hash_map_max_load {T}.
-Arguments Hashmap_hash_map_slots {T}.
-
-(** [core::num::u32::{9}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End HashmapMain__Types .
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
new file mode 100644
index 00000000..3ddc1cf3
--- /dev/null
+++ b/tests/coq/misc/External_Funs.v
@@ -0,0 +1,114 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export External_Types.
+Import External_Types.
+Require Export External_Opaque.
+Import External_Opaque.
+Module External_Funs.
+
+(** [external::swap] *)
+Definition swap_fwd
+  (T : Type) (x : T) (y : T) (st : state) : result (state * unit) :=
+  p <- core_mem_swap_fwd T x y st;
+  let (st0, _) := p in
+  p0 <- core_mem_swap_back0 T x y st st0;
+  let (st1, _) := p0 in
+  p1 <- core_mem_swap_back1 T x y st st1;
+  let (st2, _) := p1 in
+  Return (st2, tt)
+.
+
+(** [external::swap] *)
+Definition swap_back
+  (T : Type) (x : T) (y : T) (st : state) (st0 : state) :
+  result (state * (T * T))
+  :=
+  p <- core_mem_swap_fwd T x y st;
+  let (st1, _) := p in
+  p0 <- core_mem_swap_back0 T x y st st1;
+  let (st2, x0) := p0 in
+  p1 <- core_mem_swap_back1 T x y st st2;
+  let (_, y0) := p1 in
+  Return (st0, (x0, y0))
+.
+
+(** [external::test_new_non_zero_u32] *)
+Definition test_new_non_zero_u32_fwd
+  (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) :=
+  p <- core_num_nonzero_non_zero_u32_new_fwd x st;
+  let (st0, opt) := p in
+  p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0;
+  let (st1, nzu) := p0 in
+  Return (st1, nzu)
+.
+
+(** [external::test_vec] *)
+Definition test_vec_fwd : result unit :=
+  let v := vec_new u32 in
+  v0 <- vec_push_back u32 v (0%u32);
+  let _ := v0 in
+  Return tt
+.
+
+(** Unit test for [external::test_vec] *)
+Check (test_vec_fwd )%return.
+
+(** [external::custom_swap] *)
+Definition custom_swap_fwd
+  (T : Type) (x : T) (y : T) (st : state) : result (state * T) :=
+  p <- core_mem_swap_fwd T x y st;
+  let (st0, _) := p in
+  p0 <- core_mem_swap_back0 T x y st st0;
+  let (st1, x0) := p0 in
+  p1 <- core_mem_swap_back1 T x y st st1;
+  let (st2, _) := p1 in
+  Return (st2, x0)
+.
+
+(** [external::custom_swap] *)
+Definition custom_swap_back
+  (T : Type) (x : T) (y : T) (st : state) (ret : T) (st0 : state) :
+  result (state * (T * T))
+  :=
+  p <- core_mem_swap_fwd T x y st;
+  let (st1, _) := p in
+  p0 <- core_mem_swap_back0 T x y st st1;
+  let (st2, _) := p0 in
+  p1 <- core_mem_swap_back1 T x y st st2;
+  let (_, y0) := p1 in
+  Return (st0, (ret, y0))
+.
+
+(** [external::test_custom_swap] *)
+Definition test_custom_swap_fwd
+  (x : u32) (y : u32) (st : state) : result (state * unit) :=
+  p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt)
+.
+
+(** [external::test_custom_swap] *)
+Definition test_custom_swap_back
+  (x : u32) (y : u32) (st : state) (st0 : state) :
+  result (state * (u32 * u32))
+  :=
+  p <- custom_swap_back u32 x y st (1%u32) st0;
+  let (st1, p0) := p in
+  let (x0, y0) := p0 in
+  Return (st1, (x0, y0))
+.
+
+(** [external::test_swap_non_zero] *)
+Definition test_swap_non_zero_fwd
+  (x : u32) (st : state) : result (state * u32) :=
+  p <- swap_fwd u32 x (0%u32) st;
+  let (st0, _) := p in
+  p0 <- swap_back u32 x (0%u32) st st0;
+  let (st1, p1) := p0 in
+  let (x0, _) := p1 in
+  if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0)
+.
+
+End External_Funs .
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v
new file mode 100644
index 00000000..d60251e0
--- /dev/null
+++ b/tests/coq/misc/External_Opaque.v
@@ -0,0 +1,36 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: opaque function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export External_Types.
+Import External_Types.
+Module External_Opaque.
+
+(** [core::mem::swap] *)
+Axiom core_mem_swap_fwd :
+  forall(T : Type), T -> T -> state -> result (state * unit)
+.
+
+(** [core::mem::swap] *)
+Axiom core_mem_swap_back0 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::mem::swap] *)
+Axiom core_mem_swap_back1 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::num::nonzero::NonZeroU32::{14}::new] *)
+Axiom core_num_nonzero_non_zero_u32_new_fwd
+  : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t))
+.
+
+(** [core::option::Option::{0}::unwrap] *)
+Axiom core_option_option_unwrap_fwd :
+  forall(T : Type), option T -> state -> result (state * T)
+.
+
+End External_Opaque .
diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v
new file mode 100644
index 00000000..cec5b88e
--- /dev/null
+++ b/tests/coq/misc/External_Types.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: type definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module External_Types.
+
+(** [core::num::nonzero::NonZeroU32] *)
+Axiom Core_num_nonzero_non_zero_u32_t : Type.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End External_Types .
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v
deleted file mode 100644
index e7020040..00000000
--- a/tests/coq/misc/External__Funs.v
+++ /dev/null
@@ -1,114 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: function definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Require Export External__Types.
-Import External__Types.
-Require Export External__Opaque.
-Import External__Opaque.
-Module External__Funs.
-
-(** [external::swap] *)
-Definition swap_fwd
-  (T : Type) (x : T) (y : T) (st : state) : result (state * unit) :=
-  p <- core_mem_swap_fwd T x y st;
-  let (st0, _) := p in
-  p0 <- core_mem_swap_back0 T x y st st0;
-  let (st1, _) := p0 in
-  p1 <- core_mem_swap_back1 T x y st st1;
-  let (st2, _) := p1 in
-  Return (st2, tt)
-.
-
-(** [external::swap] *)
-Definition swap_back
-  (T : Type) (x : T) (y : T) (st : state) (st0 : state) :
-  result (state * (T * T))
-  :=
-  p <- core_mem_swap_fwd T x y st;
-  let (st1, _) := p in
-  p0 <- core_mem_swap_back0 T x y st st1;
-  let (st2, x0) := p0 in
-  p1 <- core_mem_swap_back1 T x y st st2;
-  let (_, y0) := p1 in
-  Return (st0, (x0, y0))
-.
-
-(** [external::test_new_non_zero_u32] *)
-Definition test_new_non_zero_u32_fwd
-  (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) :=
-  p <- core_num_nonzero_non_zero_u32_new_fwd x st;
-  let (st0, opt) := p in
-  p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0;
-  let (st1, nzu) := p0 in
-  Return (st1, nzu)
-.
-
-(** [external::test_vec] *)
-Definition test_vec_fwd : result unit :=
-  let v := vec_new u32 in
-  v0 <- vec_push_back u32 v (0%u32);
-  let _ := v0 in
-  Return tt
-.
-
-(** Unit test for [external::test_vec] *)
-Check (test_vec_fwd )%return.
-
-(** [external::custom_swap] *)
-Definition custom_swap_fwd
-  (T : Type) (x : T) (y : T) (st : state) : result (state * T) :=
-  p <- core_mem_swap_fwd T x y st;
-  let (st0, _) := p in
-  p0 <- core_mem_swap_back0 T x y st st0;
-  let (st1, x0) := p0 in
-  p1 <- core_mem_swap_back1 T x y st st1;
-  let (st2, _) := p1 in
-  Return (st2, x0)
-.
-
-(** [external::custom_swap] *)
-Definition custom_swap_back
-  (T : Type) (x : T) (y : T) (st : state) (ret : T) (st0 : state) :
-  result (state * (T * T))
-  :=
-  p <- core_mem_swap_fwd T x y st;
-  let (st1, _) := p in
-  p0 <- core_mem_swap_back0 T x y st st1;
-  let (st2, _) := p0 in
-  p1 <- core_mem_swap_back1 T x y st st2;
-  let (_, y0) := p1 in
-  Return (st0, (ret, y0))
-.
-
-(** [external::test_custom_swap] *)
-Definition test_custom_swap_fwd
-  (x : u32) (y : u32) (st : state) : result (state * unit) :=
-  p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt)
-.
-
-(** [external::test_custom_swap] *)
-Definition test_custom_swap_back
-  (x : u32) (y : u32) (st : state) (st0 : state) :
-  result (state * (u32 * u32))
-  :=
-  p <- custom_swap_back u32 x y st (1%u32) st0;
-  let (st1, p0) := p in
-  let (x0, y0) := p0 in
-  Return (st1, (x0, y0))
-.
-
-(** [external::test_swap_non_zero] *)
-Definition test_swap_non_zero_fwd
-  (x : u32) (st : state) : result (state * u32) :=
-  p <- swap_fwd u32 x (0%u32) st;
-  let (st0, _) := p in
-  p0 <- swap_back u32 x (0%u32) st st0;
-  let (st1, p1) := p0 in
-  let (x0, _) := p1 in
-  if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0)
-.
-
-End External__Funs .
diff --git a/tests/coq/misc/External__Opaque.v b/tests/coq/misc/External__Opaque.v
deleted file mode 100644
index 93652450..00000000
--- a/tests/coq/misc/External__Opaque.v
+++ /dev/null
@@ -1,36 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: opaque function definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Require Export External__Types.
-Import External__Types.
-Module External__Opaque.
-
-(** [core::mem::swap] *)
-Axiom core_mem_swap_fwd :
-  forall(T : Type), T -> T -> state -> result (state * unit)
-.
-
-(** [core::mem::swap] *)
-Axiom core_mem_swap_back0 :
-  forall(T : Type), T -> T -> state -> state -> result (state * T)
-.
-
-(** [core::mem::swap] *)
-Axiom core_mem_swap_back1 :
-  forall(T : Type), T -> T -> state -> state -> result (state * T)
-.
-
-(** [core::num::nonzero::NonZeroU32::{14}::new] *)
-Axiom core_num_nonzero_non_zero_u32_new_fwd
-  : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t))
-.
-
-(** [core::option::Option::{0}::unwrap] *)
-Axiom core_option_option_unwrap_fwd :
-  forall(T : Type), option T -> state -> result (state * T)
-.
-
-End External__Opaque .
diff --git a/tests/coq/misc/External__Types.v b/tests/coq/misc/External__Types.v
deleted file mode 100644
index f4f74272..00000000
--- a/tests/coq/misc/External__Types.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: type definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Local Open Scope Primitives_scope.
-Module External__Types.
-
-(** [core::num::nonzero::NonZeroU32] *)
-Axiom Core_num_nonzero_non_zero_u32_t : Type.
-
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End External__Types .
-- 
cgit v1.2.3