Generate record field projectors for Coq

13 files changed, 843 insertions, 778 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index f4280e80..7c3ce538 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -89,13 +89,11 @@ let return_unit_end_abs_with_no_loans = true
        ...
     ]}
 
-    We use this for instance for Coq, because in Coq we can't define groups
+    Rem.: this used to be useful for Coq, because in Coq we can't define groups
     of mutually recursive records and inductives. In such cases, we extract
     the structures as inductives, which means that field projectors are not
-    always available.
-
-    TODO: we could define a notation to take care of this.
-    TODO: today dont_use_field_projectors is not useful actually.
+    always available. As of today, we generate field projectors definitions
+    (together with the appropriate notations).
  *)
 let dont_use_field_projectors = ref false
 
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 15ad5a26..42fd0122 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -112,13 +112,6 @@ let () =
         (* F* supports monadic notations, but the encoding loses information *)
         unfold_monadic_let_bindings := true
     | Coq ->
-        (* In the case of Coq, we forbid using field projectors (see the comments for
-           [dont_use_field_projectors]).
-           Also, we always decompose ADT values with matches (decomposing with
-           let-bindings is not supported).
-        *)
-        dont_use_field_projectors := true;
-        always_deconstruct_adts_with_matches := true;
         (* Some patterns are not supported *)
         decompose_monadic_let_bindings := true;
         decompose_nested_let_patterns := true
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 4770d16d..ce0609f5 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -662,8 +662,8 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
     (type_name : string) (type_params : string list) (cons_name : string)
     (fields : field list) : unit =
   F.pp_print_space fmt ();
-  F.pp_open_hvbox fmt ctx.indent_incr;
   (* variant box *)
+  F.pp_open_hvbox fmt ctx.indent_incr;
   (* [| Cons :]
    * Note that we really don't want any break above so we print everything
    * at once. *)
@@ -951,86 +951,243 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0
 
-(** Extract extra information for a type (e.g., [Arguments] information in Coq).
+(** Auxiliary function.
 
-    Note that all the names used for extraction should already have been
-    registered.
+    Generate [Arguments] instructions in Coq.
  *)
-let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (decl : type_decl) : unit =
-  match !backend with
-  | FStar -> ()
-  | Coq -> (
-      if
-        (* Generate the [Arguments] instruction - this is useful only if there
-           are type parameters *)
-        decl.type_params = []
-      then ()
-      else
-        (* Add the type params - note that we need those bindings only for the
-         * body translation (they are not top-level) *)
-        let _ctx_body, type_params = ctx_add_type_params decl.type_params ctx in
-        (* Auxiliary function to extract an [Arguments Cons {T} _ _.] instruction *)
-        let extract_arguments_info (cons_name : string) (fields : 'a list) :
-            unit =
-          (* Add a break before *)
-          F.pp_print_break fmt 0 0;
-          (* Open a box *)
+  assert (!backend = Coq);
+  (* Generating the [Arguments] instructions is useful only if there are type parameters *)
+  if decl.type_params = [] then ()
+  else
+    (* Add the type params - note that we need those bindings only for the
+     * body translation (they are not top-level) *)
+    let _ctx_body, type_params = ctx_add_type_params decl.type_params ctx in
+    (* Auxiliary function to extract an [Arguments Cons {T} _ _.] instruction *)
+    let extract_arguments_info (cons_name : string) (fields : 'a list) : unit =
+      (* Add a break before *)
+      F.pp_print_break fmt 0 0;
+      (* Open a box *)
+      F.pp_open_hovbox fmt ctx.indent_incr;
+      (* Small utility *)
+      let print_type_vars () =
+        List.iter
+          (fun (var : string) ->
+            F.pp_print_space fmt ();
+            F.pp_print_string fmt ("{" ^ var ^ "}"))
+          type_params
+      in
+      let print_fields () =
+        List.iter
+          (fun _ ->
+            F.pp_print_space fmt ();
+            F.pp_print_string fmt "_")
+          fields
+      in
+      F.pp_print_break fmt 0 0;
+      F.pp_print_string fmt "Arguments";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt cons_name;
+      print_type_vars ();
+      print_fields ();
+      F.pp_print_string fmt ".";
+
+      (* Close the box *)
+      F.pp_close_box fmt ()
+    in
+
+    (* Generate the [Arguments] instruction *)
+    match decl.kind with
+    | Opaque -> ()
+    | Struct fields ->
+        let adt_id = AdtId decl.def_id in
+        (* Generate the instruction for the record constructor *)
+        let cons_name = ctx_get_struct adt_id ctx in
+        extract_arguments_info cons_name fields;
+        (* Generate the instruction for the record projectors, if there are *)
+        let is_rec = decl_is_from_rec_group kind in
+        if not is_rec then
+          FieldId.iteri
+            (fun fid _ ->
+              let cons_name = ctx_get_field adt_id fid ctx in
+              extract_arguments_info cons_name [])
+            fields;
+        (* Add breaks to insert new lines between definitions *)
+        F.pp_print_break fmt 0 0
+    | Enum variants ->
+        (* Generate the instructions *)
+        VariantId.iteri
+          (fun vid (v : variant) ->
+            let cons_name = ctx_get_variant (AdtId decl.def_id) vid ctx in
+            extract_arguments_info cons_name v.fields)
+          variants;
+        (* Add breaks to insert new lines between definitions *)
+        F.pp_print_break fmt 0 0
+
+(** Auxiliary function.
+
+    Generate field projectors in Coq.
+
+    Sometimes we extract records as inductives in Coq: when this happens we
+    have to define the field projectors afterwards.
+ *)
+let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
+    (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
+  assert (!backend = Coq);
+  match decl.kind with
+  | Opaque | Enum _ -> ()
+  | Struct fields ->
+      (* Records are extracted as inductives only if they are recursive *)
+      let is_rec = decl_is_from_rec_group kind in
+      if is_rec then
+        (* Add the type params *)
+        let ctx, type_params = ctx_add_type_params decl.type_params ctx in
+        let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
+        let ctx, field_var = ctx_add_var "x" (VarId.of_int 1) ctx in
+        let def_name = ctx_get_local_type decl.def_id ctx in
+        let cons_name = ctx_get_struct (AdtId decl.def_id) ctx in
+        let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
+          F.pp_print_space fmt ();
+          (* Outer box for the projector definition *)
+          F.pp_open_hvbox fmt 0;
+          (* Inner box for the projector definition *)
+          F.pp_open_hvbox fmt ctx.indent_incr;
+          (* Open a box for the [Definition PROJ ... :=] *)
           F.pp_open_hovbox fmt ctx.indent_incr;
-          (* Small utility *)
-          let print_type_vars () =
-            List.iter
-              (fun (var : string) ->
-                F.pp_print_space fmt ();
-                F.pp_print_string fmt ("{" ^ var ^ "}"))
-              type_params
-          in
-          let print_fields () =
+          F.pp_print_string fmt "Definition";
+          F.pp_print_space fmt ();
+          let field_name = ctx_get_field (AdtId decl.def_id) field_id ctx in
+          F.pp_print_string fmt field_name;
+          F.pp_print_space fmt ();
+          (* Print the type parameters *)
+          if type_params <> [] then (
+            F.pp_print_string fmt "{";
             List.iter
-              (fun _ ->
-                F.pp_print_space fmt ();
-                F.pp_print_string fmt "_")
-              fields
-          in
-          F.pp_print_break fmt 0 0;
-          F.pp_print_string fmt "Arguments";
+              (fun p ->
+                F.pp_print_string fmt p;
+                F.pp_print_space fmt ())
+              type_params;
+            F.pp_print_string fmt ":";
+            F.pp_print_space fmt ();
+            F.pp_print_string fmt "Type}";
+            F.pp_print_space fmt ());
+          (* Print the record parameter *)
+          F.pp_print_string fmt "(";
+          F.pp_print_string fmt record_var;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt def_name;
+          List.iter
+            (fun p ->
+              F.pp_print_space fmt ();
+              F.pp_print_string fmt p)
+            type_params;
+          F.pp_print_string fmt ")";
+          (* *)
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":=";
+          (* Close the box for the [Definition PROJ ... :=] *)
+          F.pp_close_box fmt ();
+          F.pp_print_space fmt ();
+          (* Open a box for the whole match *)
+          F.pp_open_hvbox fmt 0;
+          (* Open a box for the [match ... with] *)
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          F.pp_print_string fmt "match";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt record_var;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "with";
+          (* Close the box for the [match ... with] *)
+          F.pp_close_box fmt ();
+
+          (* Open a box for the branch *)
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          (* Print the match branch *)
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "|";
           F.pp_print_space fmt ();
           F.pp_print_string fmt cons_name;
-          print_type_vars ();
-          print_fields ();
-          F.pp_print_string fmt ".";
+          FieldId.iteri
+            (fun id _ ->
+              F.pp_print_space fmt ();
+              if field_id = id then F.pp_print_string fmt field_var
+              else F.pp_print_string fmt "_")
+            fields;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "=>";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt field_var;
+          (* Close the box for the branch *)
+          F.pp_close_box fmt ();
+          (* Print the [end] *)
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "end";
+          (* Close the box for the whole match *)
+          F.pp_close_box fmt ();
+          (* Close the inner box projector *)
+          F.pp_close_box fmt ();
+          (* If Coq: end the definition with a "." *)
+          print_decl_end_delimiter fmt kind;
+          (* Close the outer box projector  *)
+          F.pp_close_box fmt ();
+          (* Add breaks to insert new lines between definitions *)
+          F.pp_print_break fmt 0 0
+        in
 
-          (* Close the box *)
-          F.pp_close_box fmt ()
+        let extract_proj_notation (field_id : FieldId.id) (_ : field) : unit =
+          F.pp_print_space fmt ();
+          (* Outer box for the projector definition *)
+          F.pp_open_hvbox fmt 0;
+          (* Inner box for the projector definition *)
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
+          F.pp_print_string fmt "Notation";
+          F.pp_print_space fmt ();
+          let field_name = ctx_get_field (AdtId decl.def_id) field_id ctx in
+          F.pp_print_string fmt ("\"" ^ record_var ^ " .(" ^ field_name ^ ")\"");
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":=";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "(";
+          F.pp_print_string fmt field_name;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt record_var;
+          F.pp_print_string fmt ")";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "(at level 9)";
+          (* Close the inner box projector *)
+          F.pp_close_box fmt ();
+          (* If Coq: end the definition with a "." *)
+          print_decl_end_delimiter fmt kind;
+          (* Close the outer box projector  *)
+          F.pp_close_box fmt ();
+          (* Add breaks to insert new lines between definitions *)
+          F.pp_print_break fmt 0 0
+        in
+
+        let extract_field_proj_and_notation (field_id : FieldId.id)
+            (field : field) : unit =
+          extract_field_proj field_id field;
+          extract_proj_notation field_id field
         in
 
-        (* Generate the [Arguments] instruction *)
-        match decl.kind with
-        | Opaque -> ()
-        | Struct fields ->
-            let adt_id = AdtId decl.def_id in
-            (* Generate the instruction for the record constructor *)
-            let cons_name = ctx_get_struct adt_id ctx in
-            extract_arguments_info cons_name fields;
-            (* Generate the instruction for the record projectors, if there are *)
-            let is_rec = decl_is_from_rec_group kind in
-            if not is_rec then
-              FieldId.iteri
-                (fun fid _ ->
-                  let cons_name = ctx_get_field adt_id fid ctx in
-                  extract_arguments_info cons_name [])
-                fields;
-            (* Add breaks to insert new lines between definitions *)
-            F.pp_print_break fmt 0 0
-        | Enum variants ->
-            (* Generate the instructions *)
-            VariantId.iteri
-              (fun vid (v : variant) ->
-                let cons_name = ctx_get_variant (AdtId decl.def_id) vid ctx in
-                extract_arguments_info cons_name v.fields)
-              variants;
-            (* Add breaks to insert new lines between definitions *)
-            F.pp_print_break fmt 0 0)
+        FieldId.iteri extract_field_proj_and_notation fields
+
+(** Extract extra information for a type (e.g., [Arguments] instructions in Coq).
+
+    Note that all the names used for extraction should already have been
+    registered.
+ *)
+let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
+    (kind : decl_kind) (decl : type_decl) : unit =
+  match !backend with
+  | FStar -> ()
+  | Coq ->
+      extract_type_decl_coq_arguments ctx fmt kind decl;
+      extract_type_decl_record_field_projectors ctx fmt kind decl
 
 (** Extract the state type declaration. *)
 let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 3129614c..d60ef718 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -66,19 +66,16 @@ Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t :=
 (** [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
+  i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
+  let _ := i in
+  Return self.(Betree_node_id_counter_next_node_id)
 .
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 Definition betree_node_id_counter_fresh_id_back
   (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t :=
-  match self with
-  | mkBetree_node_id_counter_t id =>
-    i <- u64_add id 1%u64; Return (mkBetree_node_id_counter_t i)
-  end
+  i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
+  Return (mkBetree_node_id_counter_t i)
 .
 
 (** [core::num::u64::{10}::MAX] *)
@@ -224,26 +221,24 @@ Definition betree_leaf_split_fwd
   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
+    p <-
+      betree_list_split_at_fwd (u64 * u64) n0 content
+        params.(Betree_params_split_size);
+    let (content0, content1) := p in
+    p0 <- betree_list_hd_fwd (u64 * u64) content1;
+    let (pivot, _) := p0 in
+    id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
+    node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
+    id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
+    p1 <- betree_store_leaf_node_fwd id0 content0 st;
+    let (st0, _) := p1 in
+    p2 <- betree_store_leaf_node_fwd id1 content1 st0;
+    let (st1, _) := p2 in
+    let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0
+      params.(Betree_params_split_size)) in
+    let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1
+      params.(Betree_params_split_size)) in
+    Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n1 n2)
   end
 .
 
@@ -257,25 +252,21 @@ Definition betree_leaf_split_back
   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
+    p <-
+      betree_list_split_at_fwd (u64 * u64) n0 content
+        params.(Betree_params_split_size);
+    let (content0, content1) := p in
+    p0 <- betree_list_hd_fwd (u64 * u64) content1;
+    let _ := p0 in
+    id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt;
+    node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
+    id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0;
+    p1 <- betree_store_leaf_node_fwd id0 content0 st;
+    let (st0, _) := p1 in
+    p2 <- betree_store_leaf_node_fwd id1 content1 st0;
+    let (_, _) := p2 in
+    node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0;
+    Return node_id_cnt1
   end
 .
 
@@ -423,84 +414,69 @@ Fixpoint betree_node_lookup_fwd
   | 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
+      p <- betree_load_internal_node_fwd node.(Betree_internal_id) st;
+      let (st0, msgs) := p in
+      pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs;
+      match pending with
+      | BetreeListCons p0 l =>
+        let (k, msg) := p0 in
+        if k s<> key
+        then (
+          p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
+          let (st1, opt) := p1 in
+          l0 <-
+            betree_node_lookup_first_message_for_key_back n0 key msgs
+              (BetreeListCons (k, msg) l);
+          let _ := l0 in
+          Return (st1, opt))
+        else
+          match msg with
+          | BetreeMessageInsert v =>
             l0 <-
               betree_node_lookup_first_message_for_key_back n0 key msgs
-                (BetreeListCons (k, msg) l);
+                (BetreeListCons (k, BetreeMessageInsert v) 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
+            Return (st0, Some v)
+          | BetreeMessageDelete =>
+            l0 <-
+              betree_node_lookup_first_message_for_key_back n0 key msgs
+                (BetreeListCons (k, BetreeMessageDelete) l);
+            let _ := l0 in
+            Return (st0, None)
+          | BetreeMessageUpsert ufs =>
+            p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
+            let (st1, v) := p1 in
+            p2 <-
+              betree_node_apply_upserts_fwd n0 (BetreeListCons (k,
+                BetreeMessageUpsert ufs) l) v key st1;
+            let (st2, v0) := p2 in
+            node0 <- betree_internal_lookup_in_children_back n0 node key st0;
+            pending0 <-
+              betree_node_apply_upserts_back n0 (BetreeListCons (k,
+                BetreeMessageUpsert ufs) l) v key st1;
+            msgs0 <-
+              betree_node_lookup_first_message_for_key_back n0 key msgs
+                pending0;
+            p3 <-
+              betree_store_internal_node_fwd node0.(Betree_internal_id) msgs0
+                st2;
+            let (st3, _) := p3 in
+            Return (st3, Some v0)
+          end
+      | BetreeListNil =>
+        p0 <- betree_internal_lookup_in_children_fwd n0 node key st0;
+        let (st1, opt) := p0 in
+        l <-
+          betree_node_lookup_first_message_for_key_back n0 key msgs
+            BetreeListNil;
+        let _ := l in
+        Return (st1, opt)
       end
     | BetreeNodeLeaf node =>
-      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
+      p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
+      let (st0, bindings) := p in
+      opt <- betree_node_lookup_in_bindings_fwd n0 key bindings;
+      Return (st0, opt)
     end
   end
 
@@ -514,83 +490,68 @@ with betree_node_lookup_back
   | 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 (
+      p <- betree_load_internal_node_fwd node.(Betree_internal_id) st;
+      let (st0, msgs) := p in
+      pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs;
+      match pending with
+      | BetreeListCons p0 l =>
+        let (k, msg) := p0 in
+        if k s<> key
+        then (
+          l0 <-
+            betree_node_lookup_first_message_for_key_back n0 key msgs
+              (BetreeListCons (k, msg) l);
+          let _ := l0 in
+          node0 <- betree_internal_lookup_in_children_back n0 node key st0;
+          Return (BetreeNodeInternal node0))
+        else
+          match msg with
+          | BetreeMessageInsert v =>
             l0 <-
               betree_node_lookup_first_message_for_key_back n0 key msgs
-                (BetreeListCons (k, msg) l);
+                (BetreeListCons (k, BetreeMessageInsert v) 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
+            Return (BetreeNodeInternal node)
+          | BetreeMessageDelete =>
+            l0 <-
+              betree_node_lookup_first_message_for_key_back n0 key msgs
+                (BetreeListCons (k, BetreeMessageDelete) l);
+            let _ := l0 in
+            Return (BetreeNodeInternal node)
+          | BetreeMessageUpsert ufs =>
+            p1 <- betree_internal_lookup_in_children_fwd n0 node key st0;
+            let (st1, v) := p1 in
+            p2 <-
+              betree_node_apply_upserts_fwd n0 (BetreeListCons (k,
+                BetreeMessageUpsert ufs) l) v key st1;
+            let (st2, _) := p2 in
+            node0 <- betree_internal_lookup_in_children_back n0 node key st0;
+            pending0 <-
+              betree_node_apply_upserts_back n0 (BetreeListCons (k,
+                BetreeMessageUpsert ufs) l) v key st1;
+            msgs0 <-
+              betree_node_lookup_first_message_for_key_back n0 key msgs
+                pending0;
+            p3 <-
+              betree_store_internal_node_fwd node0.(Betree_internal_id) msgs0
+                st2;
+            let (_, _) := p3 in
+            Return (BetreeNodeInternal node0)
+          end
+      | BetreeListNil =>
+        l <-
+          betree_node_lookup_first_message_for_key_back n0 key msgs
+            BetreeListNil;
+        let _ := l in
+        node0 <- betree_internal_lookup_in_children_back n0 node key st0;
+        Return (BetreeNodeInternal node0)
       end
     | BetreeNodeLeaf node =>
-      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
+      p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
+      let (_, bindings) := p in
+      opt <- betree_node_lookup_in_bindings_fwd n0 key bindings;
+      let _ := opt in
+      Return (BetreeNodeLeaf node)
     end
   end
 
@@ -602,18 +563,15 @@ with betree_internal_lookup_in_children_fwd
   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
+    if key s< self.(Betree_internal_pivot)
+    then (
+      p <- betree_node_lookup_fwd n0 self.(Betree_internal_left) key st;
+      let (st0, opt) := p in
+      Return (st0, opt))
+    else (
+      p <- betree_node_lookup_fwd n0 self.(Betree_internal_right) key st;
+      let (st0, opt) := p in
+      Return (st0, opt))
   end
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children] *)
@@ -624,16 +582,15 @@ with betree_internal_lookup_in_children_back
   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
+    if key s< self.(Betree_internal_pivot)
+    then (
+      n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st;
+      Return (mkBetree_internal_t self.(Betree_internal_id)
+        self.(Betree_internal_pivot) n1 self.(Betree_internal_right)))
+    else (
+      n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st;
+      Return (mkBetree_internal_t self.(Betree_internal_id)
+        self.(Betree_internal_pivot) self.(Betree_internal_left) n1))
   end
 .
 
@@ -933,63 +890,47 @@ Fixpoint betree_node_apply_messages_fwd
   | 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
+      p <- betree_load_internal_node_fwd node.(Betree_internal_id) st;
+      let (st0, content) := p in
+      content0 <-
+        betree_node_apply_messages_to_internal_fwd_back n0 content msgs;
+      num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0;
+      if num_msgs s>= params.(Betree_params_min_flush_size)
+      then (
+        p0 <-
+          betree_internal_flush_fwd n0 node params node_id_cnt content0 st0;
+        let (st1, content1) := p0 in
+        p1 <-
+          betree_internal_flush_back n0 node params node_id_cnt content0 st0;
+        let (node0, _) := p1 in
+        p2 <-
+          betree_store_internal_node_fwd node0.(Betree_internal_id) content1
+            st1;
+        let (st2, _) := p2 in
+        Return (st2, tt))
+      else (
+        p0 <-
+          betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0;
+        let (st1, _) := p0 in
+        Return (st1, tt))
     | BetreeNodeLeaf node =>
-      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
+      p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
+      let (st0, content) := p in
+      content0 <- betree_node_apply_messages_to_leaf_fwd_back n0 content msgs;
+      len <- betree_list_len_fwd (u64 * u64) n0 content0;
+      i <- u64_mul 2%u64 params.(Betree_params_split_size);
+      if len s>= i
+      then (
+        p0 <- betree_leaf_split_fwd n0 node content0 params node_id_cnt st0;
+        let (st1, _) := p0 in
+        p1 <-
+          betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1;
+        let (st2, _) := p1 in
+        Return (st2, tt))
+      else (
+        p0 <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
+        let (st1, _) := p0 in
+        Return (st1, tt))
     end
   end
 
@@ -1005,68 +946,50 @@ with betree_node_apply_messages_back
   | 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
+      p <- betree_load_internal_node_fwd node.(Betree_internal_id) st;
+      let (st0, content) := p in
+      content0 <-
+        betree_node_apply_messages_to_internal_fwd_back n0 content msgs;
+      num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0;
+      if num_msgs s>= params.(Betree_params_min_flush_size)
+      then (
+        p0 <-
+          betree_internal_flush_fwd n0 node params node_id_cnt content0 st0;
+        let (st1, content1) := p0 in
+        p1 <-
+          betree_internal_flush_back n0 node params node_id_cnt content0 st0;
+        let (node0, node_id_cnt0) := p1 in
+        p2 <-
+          betree_store_internal_node_fwd node0.(Betree_internal_id) content1
+            st1;
+        let (_, _) := p2 in
+        Return (BetreeNodeInternal node0, node_id_cnt0))
+      else (
+        p0 <-
+          betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0;
+        let (_, _) := p0 in
+        Return (BetreeNodeInternal node, node_id_cnt))
     | BetreeNodeLeaf node =>
-      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
+      p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st;
+      let (st0, content) := p in
+      content0 <- betree_node_apply_messages_to_leaf_fwd_back n0 content msgs;
+      len <- betree_list_len_fwd (u64 * u64) n0 content0;
+      i <- u64_mul 2%u64 params.(Betree_params_split_size);
+      if len s>= i
+      then (
+        p0 <- betree_leaf_split_fwd n0 node content0 params node_id_cnt st0;
+        let (st1, new_node) := p0 in
+        p1 <-
+          betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1;
+        let (_, _) := p1 in
+        node_id_cnt0 <-
+          betree_leaf_split_back n0 node content0 params node_id_cnt st0;
+        Return (BetreeNodeInternal new_node, node_id_cnt0))
+      else (
+        p0 <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
+        let (_, _) := p0 in
+        Return (BetreeNodeLeaf (mkBetree_leaf_t node.(Betree_leaf_id) len),
+          node_id_cnt))
     end
   end
 
@@ -1080,49 +1003,44 @@ with betree_internal_flush_fwd
   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
+    p <-
+      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+        self.(Betree_internal_pivot);
+    let (msgs_left, msgs_right) := p in
+    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+    if len_left s>= params.(Betree_params_min_flush_size)
+    then (
+      p0 <-
+        betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
+          node_id_cnt msgs_left st;
+      let (st0, _) := p0 in
+      p1 <-
+        betree_node_apply_messages_back n0 self.(Betree_internal_left) params
+          node_id_cnt msgs_left st;
+      let (_, node_id_cnt0) := p1 in
+      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
+      if len_right s>= params.(Betree_params_min_flush_size)
+      then (
+        p2 <-
+          betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
+            node_id_cnt0 msgs_right st0;
+        let (st1, _) := p2 in
+        p3 <-
+          betree_node_apply_messages_back n0 self.(Betree_internal_right)
+            params node_id_cnt0 msgs_right st0;
+        let (_, _) := p3 in
+        Return (st1, BetreeListNil))
+      else Return (st0, msgs_right))
+    else (
+      p0 <-
+        betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
+          node_id_cnt msgs_right st;
+      let (st0, _) := p0 in
+      p1 <-
+        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
+          node_id_cnt msgs_right st;
+      let (_, _) := p1 in
+      Return (st0, msgs_left))
   end
 
 (** [betree_main::betree::Internal::{4}::flush] *)
@@ -1135,41 +1053,42 @@ with betree_internal_flush_back
   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
+    p <-
+      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+        self.(Betree_internal_pivot);
+    let (msgs_left, msgs_right) := p in
+    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+    if len_left s>= params.(Betree_params_min_flush_size)
+    then (
+      p0 <-
+        betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
+          node_id_cnt msgs_left st;
+      let (st0, _) := p0 in
+      p1 <-
+        betree_node_apply_messages_back n0 self.(Betree_internal_left) params
+          node_id_cnt msgs_left st;
+      let (n1, node_id_cnt0) := p1 in
+      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
+      if len_right s>= params.(Betree_params_min_flush_size)
+      then (
+        p2 <-
+          betree_node_apply_messages_back n0 self.(Betree_internal_right)
+            params node_id_cnt0 msgs_right st0;
+        let (n2, node_id_cnt1) := p2 in
+        Return (mkBetree_internal_t self.(Betree_internal_id)
+          self.(Betree_internal_pivot) n1 n2, node_id_cnt1))
+      else
+        Return (mkBetree_internal_t self.(Betree_internal_id)
+          self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
+          node_id_cnt0))
+    else (
+      p0 <-
+        betree_node_apply_messages_back n0 self.(Betree_internal_right) params
+          node_id_cnt msgs_right st;
+      let (n1, node_id_cnt0) := p0 in
+      Return (mkBetree_internal_t self.(Betree_internal_id)
+        self.(Betree_internal_pivot) self.(Betree_internal_left) n1,
+        node_id_cnt0))
   end
 .
 
@@ -1238,14 +1157,17 @@ Definition betree_be_tree_apply_fwd
   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
+    p <-
+      betree_node_apply_fwd n0 self.(Betree_be_tree_root)
+        self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg
+        st;
+    let (st0, _) := p in
+    p0 <-
+      betree_node_apply_back n0 self.(Betree_be_tree_root)
+        self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg
+        st;
+    let (_, _) := p0 in
+    Return (st0, tt)
   end
 .
 
@@ -1258,12 +1180,12 @@ Definition betree_be_tree_apply_back
   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
+    p <-
+      betree_node_apply_back n0 self.(Betree_be_tree_root)
+        self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg
+        st;
+    let (n1, nic) := p in
+    Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n1)
   end
 .
 
@@ -1366,12 +1288,9 @@ Definition betree_be_tree_lookup_fwd
   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
+    p <- betree_node_lookup_fwd n0 self.(Betree_be_tree_root) key st;
+    let (st0, opt) := p in
+    Return (st0, opt)
   end
 .
 
@@ -1383,11 +1302,9 @@ Definition betree_be_tree_lookup_back
   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
+    n1 <- betree_node_lookup_back n0 self.(Betree_be_tree_root) key st;
+    Return (mkBetree_be_tree_t self.(Betree_be_tree_params)
+      self.(Betree_be_tree_node_id_cnt) n1)
   end
 .
 
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index 672b2ebd..d02289de 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -50,6 +50,35 @@ with Betree_internal_t :=
   Betree_internal_t
 .
 
+Definition Betree_internal_id (x : Betree_internal_t) :=
+  match x with | mkBetree_internal_t x0 _ _ _ => x0 end
+.
+
+Notation "x1 .(Betree_internal_id)" := (Betree_internal_id x1) (at level 9).
+
+Definition Betree_internal_pivot (x : Betree_internal_t) :=
+  match x with | mkBetree_internal_t _ x0 _ _ => x0 end
+.
+
+Notation "x1 .(Betree_internal_pivot)" := (Betree_internal_pivot x1)
+  (at level 9)
+.
+
+Definition Betree_internal_left (x : Betree_internal_t) :=
+  match x with | mkBetree_internal_t _ _ x0 _ => x0 end
+.
+
+Notation "x1 .(Betree_internal_left)" := (Betree_internal_left x1) (at level 9)
+.
+
+Definition Betree_internal_right (x : Betree_internal_t) :=
+  match x with | mkBetree_internal_t _ _ _ x0 => x0 end
+.
+
+Notation "x1 .(Betree_internal_right)" := (Betree_internal_right x1)
+  (at level 9)
+.
+
 (** [betree_main::betree::Params] *)
 Record Betree_params_t :=
 mkBetree_params_t {
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 5e08a7a6..3cf45746 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -4,6 +4,6 @@
 
 Primitives.v
 
-BetreeMain__Funs.v
-BetreeMain__Opaque.v
-BetreeMain__Types.v
\ No newline at end of file
+BetreeMain_Funs.v
+BetreeMain_Opaque.v
+BetreeMain_Types.v
\ No newline at end of file
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 912b7fe2..d12ee1b9 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -82,17 +82,15 @@ Definition hash_map_clear_fwd_back
   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
+    v <- hash_map_clear_slots_fwd_back T n0 self.(Hash_map_slots) (0%usize);
+    Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor)
+      self.(Hash_map_max_load) v)
   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
+  Return self.(Hash_map_num_entries)
 .
 
 (** [hashmap::HashMap::{0}::insert_in_list] *)
@@ -142,23 +140,22 @@ Definition hash_map_insert_no_resize_fwd_back
   | 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
+    let i := vec_len (List_t T) self.(Hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+    inserted <- hash_map_insert_in_list_fwd T n0 key value l;
+    if inserted
+    then (
+      i0 <- usize_add self.(Hash_map_num_entries) 1%usize;
+      l0 <- hash_map_insert_in_list_back T n0 key value l;
+      v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+      Return (mkHash_map_t i0 self.(Hash_map_max_load_factor)
+        self.(Hash_map_max_load) v))
+    else (
+      l0 <- hash_map_insert_in_list_back T n0 key value l;
+      v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+      Return (mkHash_map_t self.(Hash_map_num_entries)
+        self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v))
   end
 .
 
@@ -216,23 +213,23 @@ Definition hash_map_try_resize_fwd_back
   | 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
+    let capacity := vec_len (List_t T) self.(Hash_map_slots) in
+    n1 <- usize_div max_usize 2%usize;
+    let (i, i0) := self.(Hash_map_max_load_factor) in
+    i1 <- usize_div n1 i;
+    if capacity s<= i1
+    then (
+      i2 <- usize_mul capacity 2%usize;
+      ntable <- hash_map_new_with_capacity_fwd T n0 i2 i i0;
+      p <-
+        hash_map_move_elements_fwd_back T n0 ntable self.(Hash_map_slots)
+          (0%usize);
+      let (ntable0, _) := p in
+      Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0)
+        ntable0.(Hash_map_max_load) ntable0.(Hash_map_slots)))
+    else
+      Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0)
+        self.(Hash_map_max_load) self.(Hash_map_slots))
   end
 .
 
@@ -246,14 +243,9 @@ Definition hash_map_insert_fwd_back
   | 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
+    if i s> self0.(Hash_map_max_load)
+    then (self1 <- hash_map_try_resize_fwd_back T n0 self0; Return self1)
+    else Return self0
   end
 .
 
@@ -280,14 +272,11 @@ Definition hash_map_contains_key_fwd
   | 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
+    let i := vec_len (List_t T) self.(Hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+    b <- hash_map_contains_key_in_list_fwd T n0 key l;
+    Return b
   end
 .
 
@@ -314,14 +303,11 @@ Definition hash_map_get_fwd
   | 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
+    let i := vec_len (List_t T) self.(Hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+    t <- hash_map_get_in_list_fwd T n0 key l;
+    Return t
   end
 .
 
@@ -368,14 +354,11 @@ Definition hash_map_get_mut_fwd
   | 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
+    let i := vec_len (List_t T) self.(Hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+    t <- hash_map_get_mut_in_list_fwd T n0 key l;
+    Return t
   end
 .
 
@@ -388,15 +371,13 @@ Definition hash_map_get_mut_back
   | 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
+    let i := vec_len (List_t T) self.(Hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+    l0 <- hash_map_get_mut_in_list_back T n0 key l ret;
+    v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+    Return (mkHash_map_t self.(Hash_map_num_entries)
+      self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)
   end
 .
 
@@ -453,16 +434,16 @@ Definition hash_map_remove_fwd
   | 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
+    let i := vec_len (List_t T) self.(Hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
+    x <- hash_map_remove_from_list_fwd T n0 key l;
+    match x with
+    | None => Return None
+    | Some x0 =>
+      i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
+      let _ := i0 in
+      Return (Some x0)
     end
   end
 .
@@ -476,23 +457,22 @@ Definition hash_map_remove_back
   | 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
+    let i := vec_len (List_t T) self.(Hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) 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;
+      v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+      Return (mkHash_map_t self.(Hash_map_num_entries)
+        self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)
+    | Some x0 =>
+      i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
+      l0 <- hash_map_remove_from_list_back T n0 key l;
+      v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0;
+      Return (mkHash_map_t i0 self.(Hash_map_max_load_factor)
+        self.(Hash_map_max_load) v)
     end
   end
 .
diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject
index 2aa6b46c..94708adc 100644
--- a/tests/coq/hashmap/_CoqProject
+++ b/tests/coq/hashmap/_CoqProject
@@ -4,5 +4,5 @@
 
 Primitives.v
 
-Hashmap__Types.v
-Hashmap__Funs.v
\ No newline at end of file
+Hashmap_Types.v
+Hashmap_Funs.v
\ No newline at end of file
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index b4351dc3..94a390df 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -89,18 +89,19 @@ Definition hashmap_hash_map_clear_fwd_back
   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
+    v <-
+      hashmap_hash_map_clear_slots_fwd_back T n0 self.(Hashmap_hash_map_slots)
+        (0%usize);
+    Return (mkHashmap_hash_map_t (0%usize)
+      self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load)
+      v)
   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
+  Return self.(Hashmap_hash_map_num_entries)
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
@@ -153,23 +154,29 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
   | 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
+    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <-
+      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod;
+    inserted <- hashmap_hash_map_insert_in_list_fwd T n0 key value l;
+    if inserted
+    then (
+      i0 <- usize_add self.(Hashmap_hash_map_num_entries) 1%usize;
+      l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l;
+      v <-
+        vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+          hash_mod l0;
+      Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor)
+        self.(Hashmap_hash_map_max_load) v))
+    else (
+      l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l;
+      v <-
+        vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+          hash_mod l0;
+      Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries)
+        self.(Hashmap_hash_map_max_load_factor)
+        self.(Hashmap_hash_map_max_load) v))
   end
 .
 
@@ -232,24 +239,23 @@ Definition hashmap_hash_map_try_resize_fwd_back
   | 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
+    let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+    n1 <- usize_div max_usize 2%usize;
+    let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in
+    i1 <- usize_div n1 i;
+    if capacity s<= i1
+    then (
+      i2 <- usize_mul capacity 2%usize;
+      ntable <- hashmap_hash_map_new_with_capacity_fwd T n0 i2 i i0;
+      p <-
+        hashmap_hash_map_move_elements_fwd_back T n0 ntable
+          self.(Hashmap_hash_map_slots) (0%usize);
+      let (ntable0, _) := p in
+      Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0)
+        ntable0.(Hashmap_hash_map_max_load) ntable0.(Hashmap_hash_map_slots)))
+    else
+      Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0)
+        self.(Hashmap_hash_map_max_load) self.(Hashmap_hash_map_slots))
   end
 .
 
@@ -264,16 +270,10 @@ Definition hashmap_hash_map_insert_fwd_back
   | 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
+    if i s> self0.(Hashmap_hash_map_max_load)
+    then (
+      self1 <- hashmap_hash_map_try_resize_fwd_back T n0 self0; Return self1)
+    else Return self0
   end
 .
 
@@ -303,14 +303,12 @@ Definition hashmap_hash_map_contains_key_fwd
   | 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
+    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <-
+      vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+    b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key l;
+    Return b
   end
 .
 
@@ -339,14 +337,12 @@ Definition hashmap_hash_map_get_fwd
   | 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
+    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <-
+      vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
+    t <- hashmap_hash_map_get_in_list_fwd T n0 key l;
+    Return t
   end
 .
 
@@ -395,14 +391,13 @@ Definition hashmap_hash_map_get_mut_fwd
   | 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
+    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <-
+      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod;
+    t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key l;
+    Return t
   end
 .
 
@@ -415,15 +410,18 @@ Definition hashmap_hash_map_get_mut_back
   | 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
+    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <-
+      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod;
+    l0 <- hashmap_hash_map_get_mut_in_list_back T n0 key l ret;
+    v <-
+      vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod l0;
+    Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries)
+      self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load)
+      v)
   end
 .
 
@@ -489,16 +487,18 @@ Definition hashmap_hash_map_remove_fwd
   | 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
+    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <-
+      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        hash_mod;
+    x <- hashmap_hash_map_remove_from_list_fwd T n0 key l;
+    match x with
+    | None => Return None
+    | Some x0 =>
+      i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
+      let _ := i0 in
+      Return (Some x0)
     end
   end
 .
@@ -512,23 +512,29 @@ Definition hashmap_hash_map_remove_back
   | 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
+    let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
+    hash_mod <- usize_rem hash i;
+    l <-
+      vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+        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;
+      v <-
+        vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+          hash_mod l0;
+      Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries)
+        self.(Hashmap_hash_map_max_load_factor)
+        self.(Hashmap_hash_map_max_load) v)
+    | Some x0 =>
+      i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
+      l0 <- hashmap_hash_map_remove_from_list_back T n0 key l;
+      v <-
+        vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
+          hash_mod l0;
+      Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor)
+        self.(Hashmap_hash_map_max_load) v)
     end
   end
 .
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index 10e247ae..95b82c41 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -4,6 +4,6 @@
 
 Primitives.v
 
-HashmapMain__Funs.v
-HashmapMain__Opaque.v
-HashmapMain__Types.v
\ No newline at end of file
+HashmapMain_Funs.v
+HashmapMain_Opaque.v
+HashmapMain_Types.v
\ No newline at end of file
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index c9ec0daf..7d3e5a34 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -86,9 +86,7 @@ Definition y_body : result (Wrap_t i32) :=
 Definition y_c : Wrap_t i32 := y_body%global.
 
 (** [constants::unwrap_y] *)
-Definition unwrap_y_fwd : result i32 :=
-  match y_c with | mkWrap_t i => Return i end
-.
+Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val).
 
 (** [constants::YVAL] *)
 Definition yval_body : result i32 := i <- unwrap_y_fwd; Return i.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 7c5212b2..a5f6126b 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -460,37 +460,24 @@ Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) :=
 (** [no_nested_borrows::test_constants] *)
 Definition test_constants_fwd : result unit :=
   swt <- new_tuple1_fwd;
-  match swt with
-  | mkStruct_with_tuple_t p =>
-    let (i, _) := p in
-    if negb (i s= 1%u32)
+  let (i, _) := swt.(Struct_with_tuple_p) in
+  if negb (i s= 1%u32)
+  then Fail_ Failure
+  else (
+    swt0 <- new_tuple2_fwd;
+    let (i0, _) := swt0.(Struct_with_tuple_p) in
+    if negb (i0 s= 1%i16)
     then Fail_ Failure
     else (
-      swt0 <- new_tuple2_fwd;
-      match swt0 with
-      | mkStruct_with_tuple_t p0 =>
-        let (i0, _) := p0 in
-        if negb (i0 s= 1%i16)
+      swt1 <- new_tuple3_fwd;
+      let (i1, _) := swt1.(Struct_with_tuple_p) in
+      if negb (i1 s= 1%u64)
+      then Fail_ Failure
+      else (
+        swp <- new_pair1_fwd;
+        if negb (swp.(Struct_with_pair_p).(Pair_x) s= 1%u32)
         then Fail_ Failure
-        else (
-          swt1 <- new_tuple3_fwd;
-          match swt1 with
-          | mkStruct_with_tuple_t p1 =>
-            let (i1, _) := p1 in
-            if negb (i1 s= 1%u64)
-            then Fail_ Failure
-            else (
-              swp <- new_pair1_fwd;
-              match swp with
-              | mkStruct_with_pair_t p2 =>
-                match p2 with
-                | mkPair_t i2 i3 =>
-                  if negb (i2 s= 1%u32) then Fail_ Failure else Return tt
-                end
-              end)
-          end)
-      end)
-  end
+        else Return tt)))
 .
 
 (** Unit test for [no_nested_borrows::test_constants] *)
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 16fcaf44..b8590272 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -5,9 +5,9 @@
 Primitives.v
 
 Constants.v
-External__Funs.v
-External__Opaque.v
-External__Types.v
+External_Funs.v
+External_Opaque.v
+External_Types.v
 NoNestedBorrows.v
 Paper.v
 PoloniusList.v
\ No newline at end of file