From ca77353c20e425c687ba207023d56828de6495b6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 23:50:36 +0100
Subject: Start updating simplify_aggregates

---
 tests/coq/betree/BetreeMain_Funs.v                 |  52 +++--
 tests/coq/hashmap/Hashmap_Funs.v                   |  81 ++++++--
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v       |  89 ++++++--
 tests/coq/misc/Constants.v                         |   6 +-
 tests/coq/misc/NoNestedBorrows.v                   |   8 +-
 tests/fstar/betree/BetreeMain.Funs.fst             |  98 ++++++---
 .../fstar/betree_back_stateful/BetreeMain.Funs.fst |  98 ++++++---
 tests/fstar/hashmap/Hashmap.Funs.fst               |  80 ++++++--
 tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst   |  85 ++++++--
 tests/fstar/misc/Constants.fst                     |   6 +-
 tests/fstar/misc/NoNestedBorrows.fst               |   8 +-
 tests/lean/betree/BetreeMain/Funs.lean             | 227 +++++++++------------
 tests/lean/hashmap_on_disk/HashmapMain/Funs.lean   |  22 +-
 .../misc-no_nested_borrows/NoNestedBorrows.lean    |  21 +-
 14 files changed, 589 insertions(+), 292 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index fe22b029..dc97a9e9 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -56,7 +56,7 @@ Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
 
 (** [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))
+  Return {| Betree_node_id_counter_next_node_id := (0%u64) |}
 .
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
@@ -70,7 +70,7 @@ Definition betree_node_id_counter_fresh_id_fwd
 Definition betree_node_id_counter_fresh_id_back
   (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t :=
   i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64;
-  Return (mkBetree_node_id_counter_t i)
+  Return {| Betree_node_id_counter_next_node_id := i |}
 .
 
 (** [core::num::u64::{10}::MAX] *)
@@ -223,10 +223,16 @@ Definition betree_leaf_split_fwd
   let (st0, _) := p1 in
   p2 <- betree_store_leaf_node_fwd id1 content1 st0;
   let (st1, _) := p2 in
-  let n0 := BetreeNodeLeaf (mkBetree_leaf_t id0
-    params.(Betree_params_split_size)) in
-  let n1 := BetreeNodeLeaf (mkBetree_leaf_t id1
-    params.(Betree_params_split_size)) in
+  let n0 := BetreeNodeLeaf
+    {|
+      Betree_leaf_id := id0;
+      Betree_leaf_size := params.(Betree_params_split_size)
+    |} in
+  let n1 := BetreeNodeLeaf
+    {|
+      Betree_leaf_id := id1;
+      Betree_leaf_size := params.(Betree_params_split_size)
+    |} in
   Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n0 n1)
 .
 
@@ -903,8 +909,9 @@ with betree_node_apply_messages_back
         Return (BetreeNodeInternal new_node, node_id_cnt0))
       else (
         _ <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0;
-        Return (BetreeNodeLeaf (mkBetree_leaf_t node.(Betree_leaf_id) len),
-          node_id_cnt))
+        Return (BetreeNodeLeaf
+          {| Betree_leaf_id := node.(Betree_leaf_id); Betree_leaf_size := len
+          |}, node_id_cnt))
     end
   end
 
@@ -1045,8 +1052,18 @@ Definition betree_be_tree_new_fwd
   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))))
+  Return (st0,
+    {|
+      Betree_be_tree_params :=
+        {|
+          Betree_params_min_flush_size := min_flush_size;
+          Betree_params_split_size := split_size
+        |};
+      Betree_be_tree_node_id_cnt := node_id_cnt0;
+      Betree_be_tree_root :=
+        (BetreeNodeLeaf
+          {| Betree_leaf_id := id; Betree_leaf_size := (0%u64) |})
+    |})
 .
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
@@ -1075,7 +1092,12 @@ Definition betree_be_tree_apply_back
     betree_node_apply_back n self.(Betree_be_tree_root)
       self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st;
   let (n0, nic) := p in
-  Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n0)
+  Return
+    {|
+      Betree_be_tree_params := self.(Betree_be_tree_params);
+      Betree_be_tree_node_id_cnt := nic;
+      Betree_be_tree_root := n0
+    |}
 .
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
@@ -1151,8 +1173,12 @@ Definition betree_be_tree_lookup_back
   result Betree_be_tree_t
   :=
   n0 <- betree_node_lookup_back n self.(Betree_be_tree_root) key st;
-  Return (mkBetree_be_tree_t self.(Betree_be_tree_params)
-    self.(Betree_be_tree_node_id_cnt) n0)
+  Return
+    {|
+      Betree_be_tree_params := self.(Betree_be_tree_params);
+      Betree_be_tree_node_id_cnt := self.(Betree_be_tree_node_id_cnt);
+      Betree_be_tree_root := n0
+    |}
 .
 
 (** [betree_main::main] *)
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index b952e60c..1245c654 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -47,8 +47,13 @@ Definition hash_map_new_with_capacity_fwd
   slots <- hash_map_allocate_slots_fwd T n 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)
+  Return
+    {|
+      Hash_map_num_entries := (0%usize);
+      Hash_map_max_load_factor := (max_load_dividend, max_load_divisor);
+      Hash_map_max_load := i0;
+      Hash_map_slots := slots
+    |}
 .
 
 (** [hashmap::HashMap::{0}::new] *)
@@ -78,8 +83,13 @@ Fixpoint hash_map_clear_loop_fwd_back
 Definition hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
   v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) (0%usize);
-  Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor)
-    self.(Hash_map_max_load) v)
+  Return
+    {|
+      Hash_map_num_entries := (0%usize);
+      Hash_map_max_load_factor := self.(Hash_map_max_load_factor);
+      Hash_map_max_load := self.(Hash_map_max_load);
+      Hash_map_slots := v
+    |}
 .
 
 (** [hashmap::HashMap::{0}::len] *)
@@ -156,13 +166,23 @@ Definition hash_map_insert_no_resize_fwd_back
     i0 <- usize_add self.(Hash_map_num_entries) 1%usize;
     l0 <- hash_map_insert_in_list_back T n 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))
+    Return
+      {|
+        Hash_map_num_entries := i0;
+        Hash_map_max_load_factor := self.(Hash_map_max_load_factor);
+        Hash_map_max_load := self.(Hash_map_max_load);
+        Hash_map_slots := v
+      |})
   else (
     l0 <- hash_map_insert_in_list_back T n 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))
+    Return
+      {|
+        Hash_map_num_entries := self.(Hash_map_num_entries);
+        Hash_map_max_load_factor := self.(Hash_map_max_load_factor);
+        Hash_map_max_load := self.(Hash_map_max_load);
+        Hash_map_slots := v
+      |})
 .
 
 (** [core::num::u32::{9}::MAX] *)
@@ -242,11 +262,21 @@ Definition hash_map_try_resize_fwd_back
       hash_map_move_elements_fwd_back T n 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)))
+    Return
+      {|
+        Hash_map_num_entries := self.(Hash_map_num_entries);
+        Hash_map_max_load_factor := (i, i0);
+        Hash_map_max_load := ntable0.(Hash_map_max_load);
+        Hash_map_slots := 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))
+    Return
+      {|
+        Hash_map_num_entries := self.(Hash_map_num_entries);
+        Hash_map_max_load_factor := (i, i0);
+        Hash_map_max_load := self.(Hash_map_max_load);
+        Hash_map_slots := self.(Hash_map_slots)
+      |}
 .
 
 (** [hashmap::HashMap::{0}::insert] *)
@@ -396,8 +426,13 @@ Definition hash_map_get_mut_back
   l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod;
   l0 <- hash_map_get_mut_in_list_back T n l key 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)
+  Return
+    {|
+      Hash_map_num_entries := self.(Hash_map_num_entries);
+      Hash_map_max_load_factor := self.(Hash_map_max_load_factor);
+      Hash_map_max_load := self.(Hash_map_max_load);
+      Hash_map_slots := v
+    |}
 .
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
@@ -487,14 +522,24 @@ Definition hash_map_remove_back
   | None =>
     l0 <- hash_map_remove_from_list_back T n 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)
+    Return
+      {|
+        Hash_map_num_entries := self.(Hash_map_num_entries);
+        Hash_map_max_load_factor := self.(Hash_map_max_load_factor);
+        Hash_map_max_load := self.(Hash_map_max_load);
+        Hash_map_slots := v
+      |}
   | Some x0 =>
     i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
     l0 <- hash_map_remove_from_list_back T n 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)
+    Return
+      {|
+        Hash_map_num_entries := i0;
+        Hash_map_max_load_factor := self.(Hash_map_max_load_factor);
+        Hash_map_max_load := self.(Hash_map_max_load);
+        Hash_map_slots := v
+      |}
   end
 .
 
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 2a3ad87c..804f466a 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -49,8 +49,13 @@ Definition hashmap_hash_map_new_with_capacity_fwd
   slots <- hashmap_hash_map_allocate_slots_fwd T n 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)
+  Return
+    {|
+      Hashmap_hash_map_num_entries := (0%usize);
+      Hashmap_hash_map_max_load_factor := (max_load_dividend, max_load_divisor);
+      Hashmap_hash_map_max_load := i0;
+      Hashmap_hash_map_slots := slots
+    |}
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::new] *)
@@ -85,8 +90,14 @@ Definition hashmap_hash_map_clear_fwd_back
   v <-
     hashmap_hash_map_clear_loop_fwd_back T n 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)
+  Return
+    {|
+      Hashmap_hash_map_num_entries := (0%usize);
+      Hashmap_hash_map_max_load_factor :=
+        self.(Hashmap_hash_map_max_load_factor);
+      Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load);
+      Hashmap_hash_map_slots := v
+    |}
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::len] *)
@@ -169,16 +180,27 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
     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))
+    Return
+      {|
+        Hashmap_hash_map_num_entries := i0;
+        Hashmap_hash_map_max_load_factor :=
+          self.(Hashmap_hash_map_max_load_factor);
+        Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load);
+        Hashmap_hash_map_slots := v
+      |})
   else (
     l0 <- hashmap_hash_map_insert_in_list_back T n 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))
+    Return
+      {|
+        Hashmap_hash_map_num_entries := self.(Hashmap_hash_map_num_entries);
+        Hashmap_hash_map_max_load_factor :=
+          self.(Hashmap_hash_map_max_load_factor);
+        Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load);
+        Hashmap_hash_map_slots := v
+      |})
 .
 
 (** [core::num::u32::{9}::MAX] *)
@@ -263,11 +285,21 @@ Definition hashmap_hash_map_try_resize_fwd_back
       hashmap_hash_map_move_elements_fwd_back T n 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)))
+    Return
+      {|
+        Hashmap_hash_map_num_entries := self.(Hashmap_hash_map_num_entries);
+        Hashmap_hash_map_max_load_factor := (i, i0);
+        Hashmap_hash_map_max_load := ntable0.(Hashmap_hash_map_max_load);
+        Hashmap_hash_map_slots := 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))
+    Return
+      {|
+        Hashmap_hash_map_num_entries := self.(Hashmap_hash_map_num_entries);
+        Hashmap_hash_map_max_load_factor := (i, i0);
+        Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load);
+        Hashmap_hash_map_slots := self.(Hashmap_hash_map_slots)
+      |}
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert] *)
@@ -428,8 +460,14 @@ Definition hashmap_hash_map_get_mut_back
   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)
+  Return
+    {|
+      Hashmap_hash_map_num_entries := self.(Hashmap_hash_map_num_entries);
+      Hashmap_hash_map_max_load_factor :=
+        self.(Hashmap_hash_map_max_load_factor);
+      Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load);
+      Hashmap_hash_map_slots := v
+    |}
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
@@ -536,17 +574,28 @@ Definition hashmap_hash_map_remove_back
     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)
+    Return
+      {|
+        Hashmap_hash_map_num_entries := self.(Hashmap_hash_map_num_entries);
+        Hashmap_hash_map_max_load_factor :=
+          self.(Hashmap_hash_map_max_load_factor);
+        Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load);
+        Hashmap_hash_map_slots := v
+      |}
   | Some x0 =>
     i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
     l0 <- hashmap_hash_map_remove_from_list_back T n 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)
+    Return
+      {|
+        Hashmap_hash_map_num_entries := i0;
+        Hashmap_hash_map_max_load_factor :=
+          self.(Hashmap_hash_map_max_load_factor);
+        Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load);
+        Hashmap_hash_map_slots := v
+      |}
   end
 .
 
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 0a72558d..cd3880c2 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -44,7 +44,7 @@ Arguments Pair_y {T1} {T2}.
 
 (** [constants::mk_pair1] *)
 Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) :=
-  Return (mkPair_t x y)
+  Return {| Pair_x := x; Pair_y := y |}
 .
 
 (** [constants::P0] *)
@@ -61,7 +61,7 @@ Definition p2_c : (u32 * u32) := p2_body%global.
 
 (** [constants::P3] *)
 Definition p3_body : result (Pair_t u32 u32) :=
-  Return (mkPair_t (0%u32) (1%u32))
+  Return {| Pair_x := (0%u32); Pair_y := (1%u32) |}
 .
 Definition p3_c : Pair_t u32 u32 := p3_body%global.
 
@@ -73,7 +73,7 @@ Arguments Wrap_val {T}.
 
 (** [constants::Wrap::{0}::new] *)
 Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) :=
-  Return (mkWrap_t val)
+  Return {| Wrap_val := val |}
 .
 
 (** [constants::Y] *)
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 98ed1cf6..826b52b6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -423,17 +423,17 @@ Arguments Struct_with_tuple_p {T1} {T2}.
 
 (** [no_nested_borrows::new_tuple1] *)
 Definition new_tuple1_fwd : result (Struct_with_tuple_t u32 u32) :=
-  Return (mkStruct_with_tuple_t (1%u32, 2%u32))
+  Return {| Struct_with_tuple_p := (1%u32, 2%u32) |}
 .
 
 (** [no_nested_borrows::new_tuple2] *)
 Definition new_tuple2_fwd : result (Struct_with_tuple_t i16 i16) :=
-  Return (mkStruct_with_tuple_t (1%i16, 2%i16))
+  Return {| Struct_with_tuple_p := (1%i16, 2%i16) |}
 .
 
 (** [no_nested_borrows::new_tuple3] *)
 Definition new_tuple3_fwd : result (Struct_with_tuple_t u64 i64) :=
-  Return (mkStruct_with_tuple_t (1%u64, 2%i64))
+  Return {| Struct_with_tuple_p := (1%u64, 2%i64) |}
 .
 
 (** [no_nested_borrows::StructWithPair] *)
@@ -448,7 +448,7 @@ Arguments Struct_with_pair_p {T1} {T2}.
 
 (** [no_nested_borrows::new_pair1] *)
 Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) :=
-  Return (mkStruct_with_pair_t (mkPair_t (1%u32) (2%u32)))
+  Return {| Struct_with_pair_p := {| Pair_x := (1%u32); Pair_y := (2%u32) |} |}
 .
 
 (** [no_nested_borrows::test_constants] *)
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index f3a01884..4c541aaf 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -46,7 +46,7 @@ let betree_fresh_node_id_back (counter : u64) : result u64 =
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
-  Return (Mkbetree_node_id_counter_t 0)
+  Return { betree_node_id_counter_next_node_id = 0 }
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 let betree_node_id_counter_fresh_id_fwd
@@ -58,7 +58,7 @@ let betree_node_id_counter_fresh_id_fwd
 let betree_node_id_counter_fresh_id_back
   (self : betree_node_id_counter_t) : result betree_node_id_counter_t =
   let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
-  Return (Mkbetree_node_id_counter_t i)
+  Return { betree_node_id_counter_next_node_id = i }
 
 (** [core::num::u64::{10}::MAX] *)
 let core_num_u64_max_body : result u64 = Return 18446744073709551615
@@ -188,11 +188,19 @@ let betree_leaf_split_fwd
   let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in
   let* (st0, _) = betree_store_leaf_node_fwd id0 content0 st in
   let* (st1, _) = betree_store_leaf_node_fwd id1 content1 st0 in
-  let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size)
-    in
-  let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 params.betree_params_split_size)
-    in
-  Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n n0)
+  let n = BetreeNodeLeaf
+    { betree_leaf_id = id0; betree_leaf_size = params.betree_params_split_size
+    } in
+  let n0 = BetreeNodeLeaf
+    { betree_leaf_id = id1; betree_leaf_size = params.betree_params_split_size
+    } in
+  Return (st1,
+    {
+      betree_internal_id = self.betree_leaf_id;
+      betree_internal_pivot = pivot;
+      betree_internal_left = n;
+      betree_internal_right = n0
+    })
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 let betree_leaf_split_back
@@ -461,12 +469,22 @@ and betree_internal_lookup_in_children_back
   if key < self.betree_internal_pivot
   then
     let* n = betree_node_lookup_back self.betree_internal_left key st in
-    Return (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot n self.betree_internal_right)
+    Return
+      {
+        betree_internal_id = self.betree_internal_id;
+        betree_internal_pivot = self.betree_internal_pivot;
+        betree_internal_left = n;
+        betree_internal_right = self.betree_internal_right
+      }
   else
     let* n = betree_node_lookup_back self.betree_internal_right key st in
-    Return (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n)
+    Return
+      {
+        betree_internal_id = self.betree_internal_id;
+        betree_internal_pivot = self.betree_internal_pivot;
+        betree_internal_left = self.betree_internal_left;
+        betree_internal_right = n
+      }
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -779,7 +797,8 @@ and betree_node_apply_messages_back
       Return (BetreeNodeInternal new_node, node_id_cnt0)
     else
       let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
-      Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len),
+      Return (BetreeNodeLeaf
+        { betree_leaf_id = node.betree_leaf_id; betree_leaf_size = len },
         node_id_cnt)
   end
 
@@ -853,17 +872,32 @@ and betree_internal_flush_back
       let* (n0, node_id_cnt1) =
         betree_node_apply_messages_back self.betree_internal_right params
           node_id_cnt0 msgs_right st0 in
-      Return (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n n0, node_id_cnt1)
+      Return
+        ({
+           betree_internal_id = self.betree_internal_id;
+           betree_internal_pivot = self.betree_internal_pivot;
+           betree_internal_left = n;
+           betree_internal_right = n0
+         }, node_id_cnt1)
     else
-      Return (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0)
+      Return
+        ({
+           betree_internal_id = self.betree_internal_id;
+           betree_internal_pivot = self.betree_internal_pivot;
+           betree_internal_left = n;
+           betree_internal_right = self.betree_internal_right
+         }, node_id_cnt0)
   else
     let* (n, node_id_cnt0) =
       betree_node_apply_messages_back self.betree_internal_right params
         node_id_cnt msgs_right st in
-    Return (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0)
+    Return
+      ({
+         betree_internal_id = self.betree_internal_id;
+         betree_internal_pivot = self.betree_internal_pivot;
+         betree_internal_left = self.betree_internal_left;
+         betree_internal_right = n
+       }, node_id_cnt0)
 
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_fwd
@@ -901,8 +935,17 @@ let betree_be_tree_new_fwd
   let* id = betree_node_id_counter_fresh_id_fwd node_id_cnt in
   let* (st0, _) = betree_store_leaf_node_fwd id BetreeListNil st in
   let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
-  Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size)
-    node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
+  Return (st0,
+    {
+      betree_be_tree_params =
+        {
+          betree_params_min_flush_size = min_flush_size;
+          betree_params_split_size = split_size
+        };
+      betree_be_tree_node_id_cnt = node_id_cnt0;
+      betree_be_tree_root =
+        (BetreeNodeLeaf { betree_leaf_id = id; betree_leaf_size = 0 })
+    })
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
 let betree_be_tree_apply_fwd
@@ -925,7 +968,12 @@ let betree_be_tree_apply_back
   let* (n, nic) =
     betree_node_apply_back self.betree_be_tree_root self.betree_be_tree_params
       self.betree_be_tree_node_id_cnt key msg st in
-  Return (Mkbetree_be_tree_t self.betree_be_tree_params nic n)
+  Return
+    {
+      betree_be_tree_params = self.betree_be_tree_params;
+      betree_be_tree_node_id_cnt = nic;
+      betree_be_tree_root = n
+    }
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 let betree_be_tree_insert_fwd
@@ -990,8 +1038,12 @@ let betree_be_tree_lookup_back
   result betree_be_tree_t
   =
   let* n = betree_node_lookup_back self.betree_be_tree_root key st in
-  Return (Mkbetree_be_tree_t self.betree_be_tree_params
-    self.betree_be_tree_node_id_cnt n)
+  Return
+    {
+      betree_be_tree_params = self.betree_be_tree_params;
+      betree_be_tree_node_id_cnt = self.betree_be_tree_node_id_cnt;
+      betree_be_tree_root = n
+    }
 
 (** [betree_main::main] *)
 let main_fwd : result unit =
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 7e44928c..1ca469ea 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -46,7 +46,7 @@ let betree_fresh_node_id_back (counter : u64) : result u64 =
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
-  Return (Mkbetree_node_id_counter_t 0)
+  Return { betree_node_id_counter_next_node_id = 0 }
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 let betree_node_id_counter_fresh_id_fwd
@@ -58,7 +58,7 @@ let betree_node_id_counter_fresh_id_fwd
 let betree_node_id_counter_fresh_id_back
   (self : betree_node_id_counter_t) : result betree_node_id_counter_t =
   let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
-  Return (Mkbetree_node_id_counter_t i)
+  Return { betree_node_id_counter_next_node_id = i }
 
 (** [core::num::u64::{10}::MAX] *)
 let core_num_u64_max_body : result u64 = Return 18446744073709551615
@@ -188,11 +188,19 @@ let betree_leaf_split_fwd
   let* id1 = betree_node_id_counter_fresh_id_fwd node_id_cnt0 in
   let* (st0, _) = betree_store_leaf_node_fwd id0 content0 st in
   let* (st1, _) = betree_store_leaf_node_fwd id1 content1 st0 in
-  let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size)
-    in
-  let n0 = BetreeNodeLeaf (Mkbetree_leaf_t id1 params.betree_params_split_size)
-    in
-  Return (st1, Mkbetree_internal_t self.betree_leaf_id pivot n n0)
+  let n = BetreeNodeLeaf
+    { betree_leaf_id = id0; betree_leaf_size = params.betree_params_split_size
+    } in
+  let n0 = BetreeNodeLeaf
+    { betree_leaf_id = id1; betree_leaf_size = params.betree_params_split_size
+    } in
+  Return (st1,
+    {
+      betree_internal_id = self.betree_leaf_id;
+      betree_internal_pivot = pivot;
+      betree_internal_left = n;
+      betree_internal_right = n0
+    })
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 let betree_leaf_split_back0
@@ -507,13 +515,23 @@ and betree_internal_lookup_in_children_back
   then
     let* (st1, n) =
       betree_node_lookup_back self.betree_internal_left key st st0 in
-    Return (st1, Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot n self.betree_internal_right)
+    Return (st1,
+      {
+        betree_internal_id = self.betree_internal_id;
+        betree_internal_pivot = self.betree_internal_pivot;
+        betree_internal_left = n;
+        betree_internal_right = self.betree_internal_right
+      })
   else
     let* (st1, n) =
       betree_node_lookup_back self.betree_internal_right key st st0 in
-    Return (st1, Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n)
+    Return (st1,
+      {
+        betree_internal_id = self.betree_internal_id;
+        betree_internal_pivot = self.betree_internal_pivot;
+        betree_internal_left = self.betree_internal_left;
+        betree_internal_right = n
+      })
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
@@ -830,7 +848,8 @@ and betree_node_apply_messages_back'a
       Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
     else
       let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
-      Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len),
+      Return (st0, (BetreeNodeLeaf
+        { betree_leaf_id = node.betree_leaf_id; betree_leaf_size = len },
         node_id_cnt))
   end
 
@@ -972,11 +991,21 @@ and betree_internal_flush_back'a
       let* _ =
         betree_node_apply_messages_back1 self.betree_internal_right params
           node_id_cnt0 msgs_right st3 st5 in
-      Return (st0, (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n n0, node_id_cnt1))
+      Return (st0,
+        ({
+           betree_internal_id = self.betree_internal_id;
+           betree_internal_pivot = self.betree_internal_pivot;
+           betree_internal_left = n;
+           betree_internal_right = n0
+         }, node_id_cnt1))
     else
-      Return (st0, (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0))
+      Return (st0,
+        ({
+           betree_internal_id = self.betree_internal_id;
+           betree_internal_pivot = self.betree_internal_pivot;
+           betree_internal_left = n;
+           betree_internal_right = self.betree_internal_right
+         }, node_id_cnt0))
   else
     let* (st1, _) =
       betree_node_apply_messages_fwd self.betree_internal_right params
@@ -987,8 +1016,13 @@ and betree_internal_flush_back'a
     let* _ =
       betree_node_apply_messages_back1 self.betree_internal_right params
         node_id_cnt msgs_right st st2 in
-    Return (st0, (Mkbetree_internal_t self.betree_internal_id
-      self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0))
+    Return (st0,
+      ({
+         betree_internal_id = self.betree_internal_id;
+         betree_internal_pivot = self.betree_internal_pivot;
+         betree_internal_left = self.betree_internal_left;
+         betree_internal_right = n
+       }, node_id_cnt0))
 
 (** [betree_main::betree::Internal::{4}::flush] *)
 and betree_internal_flush_back1
@@ -1106,8 +1140,17 @@ let betree_be_tree_new_fwd
   let* id = betree_node_id_counter_fresh_id_fwd node_id_cnt in
   let* (st0, _) = betree_store_leaf_node_fwd id BetreeListNil st in
   let* node_id_cnt0 = betree_node_id_counter_fresh_id_back node_id_cnt in
-  Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size)
-    node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
+  Return (st0,
+    {
+      betree_be_tree_params =
+        {
+          betree_params_min_flush_size = min_flush_size;
+          betree_params_split_size = split_size
+        };
+      betree_be_tree_node_id_cnt = node_id_cnt0;
+      betree_be_tree_root =
+        (BetreeNodeLeaf { betree_leaf_id = id; betree_leaf_size = 0 })
+    })
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
 let betree_be_tree_apply_fwd
@@ -1140,7 +1183,12 @@ let betree_be_tree_apply_back
   let* _ =
     betree_node_apply_back1 self.betree_be_tree_root self.betree_be_tree_params
       self.betree_be_tree_node_id_cnt key msg st st2 in
-  Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n)
+  Return (st0,
+    {
+      betree_be_tree_params = self.betree_be_tree_params;
+      betree_be_tree_node_id_cnt = nic;
+      betree_be_tree_root = n
+    })
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 let betree_be_tree_insert_fwd
@@ -1221,8 +1269,12 @@ let betree_be_tree_lookup_back
   =
   let* (st1, n) = betree_node_lookup_back self.betree_be_tree_root key st st0
     in
-  Return (st1, Mkbetree_be_tree_t self.betree_be_tree_params
-    self.betree_be_tree_node_id_cnt n)
+  Return (st1,
+    {
+      betree_be_tree_params = self.betree_be_tree_params;
+      betree_be_tree_node_id_cnt = self.betree_be_tree_node_id_cnt;
+      betree_be_tree_root = n
+    })
 
 (** [betree_main::main] *)
 let main_fwd : result unit =
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 62799976..120f8323 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -39,7 +39,13 @@ let hash_map_new_with_capacity_fwd
   let* slots = hash_map_allocate_slots_fwd t v capacity in
   let* i = usize_mul capacity max_load_dividend in
   let* i0 = usize_div i max_load_divisor in
-  Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots)
+  Return
+    {
+      hash_map_num_entries = 0;
+      hash_map_max_load_factor = (max_load_dividend, max_load_divisor);
+      hash_map_max_load = i0;
+      hash_map_slots = slots
+    }
 
 (** [hashmap::HashMap::{0}::new] *)
 let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
@@ -63,8 +69,13 @@ let rec hash_map_clear_loop_fwd_back
 let hash_map_clear_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
   let* v = hash_map_clear_loop_fwd_back t self.hash_map_slots 0 in
-  Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load
-    v)
+  Return
+    {
+      hash_map_num_entries = 0;
+      hash_map_max_load_factor = self.hash_map_max_load_factor;
+      hash_map_max_load = self.hash_map_max_load;
+      hash_map_slots = v
+    }
 
 (** [hashmap::HashMap::{0}::len] *)
 let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
@@ -125,13 +136,23 @@ let hash_map_insert_no_resize_fwd_back
     let* i0 = usize_add self.hash_map_num_entries 1 in
     let* l0 = hash_map_insert_in_list_back t key value l in
     let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
-    Return (Mkhash_map_t i0 self.hash_map_max_load_factor
-      self.hash_map_max_load v)
+    Return
+      {
+        hash_map_num_entries = i0;
+        hash_map_max_load_factor = self.hash_map_max_load_factor;
+        hash_map_max_load = self.hash_map_max_load;
+        hash_map_slots = v
+      }
   else
     let* l0 = hash_map_insert_in_list_back t key value l in
     let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
-    Return (Mkhash_map_t self.hash_map_num_entries
-      self.hash_map_max_load_factor self.hash_map_max_load v)
+    Return
+      {
+        hash_map_num_entries = self.hash_map_num_entries;
+        hash_map_max_load_factor = self.hash_map_max_load_factor;
+        hash_map_max_load = self.hash_map_max_load;
+        hash_map_slots = v
+      }
 
 (** [core::num::u32::{9}::MAX] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -194,11 +215,21 @@ let hash_map_try_resize_fwd_back
     let* ntable = hash_map_new_with_capacity_fwd t i2 i i0 in
     let* (ntable0, _) =
       hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 in
-    Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
-      ntable0.hash_map_max_load ntable0.hash_map_slots)
+    Return
+      {
+        hash_map_num_entries = self.hash_map_num_entries;
+        hash_map_max_load_factor = (i, i0);
+        hash_map_max_load = ntable0.hash_map_max_load;
+        hash_map_slots = 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)
+    Return
+      {
+        hash_map_num_entries = self.hash_map_num_entries;
+        hash_map_max_load_factor = (i, i0);
+        hash_map_max_load = self.hash_map_max_load;
+        hash_map_slots = self.hash_map_slots
+      }
 
 (** [hashmap::HashMap::{0}::insert] *)
 let hash_map_insert_fwd_back
@@ -325,8 +356,13 @@ let hash_map_get_mut_back
   let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in
   let* l0 = hash_map_get_mut_in_list_back t l key ret in
   let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
-  Return (Mkhash_map_t self.hash_map_num_entries self.hash_map_max_load_factor
-    self.hash_map_max_load v)
+  Return
+    {
+      hash_map_num_entries = self.hash_map_num_entries;
+      hash_map_max_load_factor = self.hash_map_max_load_factor;
+      hash_map_max_load = self.hash_map_max_load;
+      hash_map_slots = v
+    }
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 let rec hash_map_remove_from_list_loop_fwd
@@ -404,14 +440,24 @@ let hash_map_remove_back
   | None ->
     let* l0 = hash_map_remove_from_list_back t key l in
     let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
-    Return (Mkhash_map_t self.hash_map_num_entries
-      self.hash_map_max_load_factor self.hash_map_max_load v)
+    Return
+      {
+        hash_map_num_entries = self.hash_map_num_entries;
+        hash_map_max_load_factor = self.hash_map_max_load_factor;
+        hash_map_max_load = self.hash_map_max_load;
+        hash_map_slots = v
+      }
   | Some x0 ->
     let* i0 = usize_sub self.hash_map_num_entries 1 in
     let* l0 = hash_map_remove_from_list_back t key l in
     let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
-    Return (Mkhash_map_t i0 self.hash_map_max_load_factor
-      self.hash_map_max_load v)
+    Return
+      {
+        hash_map_num_entries = i0;
+        hash_map_max_load_factor = self.hash_map_max_load_factor;
+        hash_map_max_load = self.hash_map_max_load;
+        hash_map_slots = v
+      }
   end
 
 (** [hashmap::test1] *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 7e1a7636..ae98386a 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -42,8 +42,13 @@ let hashmap_hash_map_new_with_capacity_fwd
   let* slots = hashmap_hash_map_allocate_slots_fwd t v capacity in
   let* i = usize_mul capacity max_load_dividend in
   let* i0 = usize_div i max_load_divisor in
-  Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0
-    slots)
+  Return
+    {
+      hashmap_hash_map_num_entries = 0;
+      hashmap_hash_map_max_load_factor = (max_load_dividend, max_load_divisor);
+      hashmap_hash_map_max_load = i0;
+      hashmap_hash_map_slots = slots
+    }
 
 (** [hashmap_main::hashmap::HashMap::{0}::new] *)
 let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
@@ -69,8 +74,13 @@ let hashmap_hash_map_clear_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
   let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0
     in
-  Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
-    self.hashmap_hash_map_max_load v)
+  Return
+    {
+      hashmap_hash_map_num_entries = 0;
+      hashmap_hash_map_max_load_factor = self.hashmap_hash_map_max_load_factor;
+      hashmap_hash_map_max_load = self.hashmap_hash_map_max_load;
+      hashmap_hash_map_slots = v
+    }
 
 (** [hashmap_main::hashmap::HashMap::{0}::len] *)
 let hashmap_hash_map_len_fwd
@@ -139,15 +149,27 @@ let hashmap_hash_map_insert_no_resize_fwd_back
     let* v =
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
-    Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor
-      self.hashmap_hash_map_max_load v)
+    Return
+      {
+        hashmap_hash_map_num_entries = i0;
+        hashmap_hash_map_max_load_factor =
+          self.hashmap_hash_map_max_load_factor;
+        hashmap_hash_map_max_load = self.hashmap_hash_map_max_load;
+        hashmap_hash_map_slots = v
+      }
   else
     let* l0 = hashmap_hash_map_insert_in_list_back t key value l in
     let* v =
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
-    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)
+    Return
+      {
+        hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries;
+        hashmap_hash_map_max_load_factor =
+          self.hashmap_hash_map_max_load_factor;
+        hashmap_hash_map_max_load = self.hashmap_hash_map_max_load;
+        hashmap_hash_map_slots = v
+      }
 
 (** [core::num::u32::{9}::MAX] *)
 let core_num_u32_max_body : result u32 = Return 4294967295
@@ -217,11 +239,21 @@ let hashmap_hash_map_try_resize_fwd_back
     let* (ntable0, _) =
       hashmap_hash_map_move_elements_fwd_back t ntable
         self.hashmap_hash_map_slots 0 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)
+    Return
+      {
+        hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries;
+        hashmap_hash_map_max_load_factor = (i, i0);
+        hashmap_hash_map_max_load = ntable0.hashmap_hash_map_max_load;
+        hashmap_hash_map_slots = 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)
+    Return
+      {
+        hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries;
+        hashmap_hash_map_max_load_factor = (i, i0);
+        hashmap_hash_map_max_load = self.hashmap_hash_map_max_load;
+        hashmap_hash_map_slots = self.hashmap_hash_map_slots
+      }
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert] *)
 let hashmap_hash_map_insert_fwd_back
@@ -360,8 +392,13 @@ let hashmap_hash_map_get_mut_back
   let* v =
     vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
       l0 in
-  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)
+  Return
+    {
+      hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries;
+      hashmap_hash_map_max_load_factor = self.hashmap_hash_map_max_load_factor;
+      hashmap_hash_map_max_load = self.hashmap_hash_map_max_load;
+      hashmap_hash_map_slots = v
+    }
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 let rec hashmap_hash_map_remove_from_list_loop_fwd
@@ -453,16 +490,28 @@ let hashmap_hash_map_remove_back
     let* v =
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
-    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)
+    Return
+      {
+        hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries;
+        hashmap_hash_map_max_load_factor =
+          self.hashmap_hash_map_max_load_factor;
+        hashmap_hash_map_max_load = self.hashmap_hash_map_max_load;
+        hashmap_hash_map_slots = v
+      }
   | Some x0 ->
     let* i0 = usize_sub self.hashmap_hash_map_num_entries 1 in
     let* l0 = hashmap_hash_map_remove_from_list_back t key l in
     let* v =
       vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
         hash_mod l0 in
-    Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor
-      self.hashmap_hash_map_max_load v)
+    Return
+      {
+        hashmap_hash_map_num_entries = i0;
+        hashmap_hash_map_max_load_factor =
+          self.hashmap_hash_map_max_load_factor;
+        hashmap_hash_map_max_load = self.hashmap_hash_map_max_load;
+        hashmap_hash_map_slots = v
+      }
   end
 
 (** [hashmap_main::hashmap::test1] *)
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index bf13ad43..bf2f0b1b 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -38,7 +38,7 @@ type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
 
 (** [constants::mk_pair1] *)
 let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
-  Return (Mkpair_t x y)
+  Return { pair_x = x; pair_y = y }
 
 (** [constants::P0] *)
 let p0_body : result (u32 & u32) = mk_pair0_fwd 0 1
@@ -53,7 +53,7 @@ let p2_body : result (u32 & u32) = Return (0, 1)
 let p2_c : (u32 & u32) = eval_global p2_body
 
 (** [constants::P3] *)
-let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
+let p3_body : result (pair_t u32 u32) = Return { pair_x = 0; pair_y = 1 }
 let p3_c : pair_t u32 u32 = eval_global p3_body
 
 (** [constants::Wrap] *)
@@ -61,7 +61,7 @@ type wrap_t (t : Type0) = { wrap_val : t; }
 
 (** [constants::Wrap::{0}::new] *)
 let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
-  Return (Mkwrap_t val0)
+  Return { wrap_val = val0 }
 
 (** [constants::Y] *)
 let y_body : result (wrap_t i32) = wrap_new_fwd i32 2
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 1e186c79..3770ab5d 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -353,15 +353,15 @@ type struct_with_tuple_t (t1 t2 : Type0) = { struct_with_tuple_p : (t1 & t2); }
 
 (** [no_nested_borrows::new_tuple1] *)
 let new_tuple1_fwd : result (struct_with_tuple_t u32 u32) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::new_tuple2] *)
 let new_tuple2_fwd : result (struct_with_tuple_t i16 i16) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::new_tuple3] *)
 let new_tuple3_fwd : result (struct_with_tuple_t u64 i64) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::StructWithPair] *)
 type struct_with_pair_t (t1 t2 : Type0) =
@@ -371,7 +371,7 @@ type struct_with_pair_t (t1 t2 : Type0) =
 
 (** [no_nested_borrows::new_pair1] *)
 let new_pair1_fwd : result (struct_with_pair_t u32 u32) =
-  Return (Mkstruct_with_pair_t (Mkpair_t 1 2))
+  Return { struct_with_pair_p = { pair_x = 1; pair_y = 2 } }
 
 (** [no_nested_borrows::test_constants] *)
 let test_constants_fwd : result unit =
diff --git a/tests/lean/betree/BetreeMain/Funs.lean b/tests/lean/betree/BetreeMain/Funs.lean
index e40ca4ca..5d355677 100644
--- a/tests/lean/betree/BetreeMain/Funs.lean
+++ b/tests/lean/betree/BetreeMain/Funs.lean
@@ -223,13 +223,7 @@ def betree_leaf_split_fwd
         betree_leaf_id := id1,
         betree_leaf_size := params.betree_params_split_size
       }
-    Result.ret (st1,
-      {
-        betree_internal_id := self.betree_leaf_id,
-        betree_internal_pivot := pivot,
-        betree_internal_left := n,
-        betree_internal_right := n0
-      })
+    Result.ret (st1, mkbetree_internal_t self.betree_leaf_id pivot n n0)
 
 /- [betree_main::betree::Leaf::{3}::split] -/
 def betree_leaf_split_back
@@ -380,8 +374,8 @@ mutual def betree_node_lookup_fwd
   match h: self with
   | betree_node_t.BetreeNodeInternal node =>
     do
-      let (st0, msgs) ←
-        betree_load_internal_node_fwd node.betree_internal_id st
+      let (mkbetree_internal_t i i0 n n0) := node
+      let (st0, msgs) ← betree_load_internal_node_fwd i st
       let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
       match h: pending with
       | betree_list_t.BetreeListCons p l =>
@@ -390,7 +384,8 @@ mutual def betree_node_lookup_fwd
         then
           do
             let (st1, opt) ←
-              betree_internal_lookup_in_children_fwd node key st0
+              betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0
+                n n0) key st0
             let _ ←
               betree_node_lookup_first_message_for_key_back key msgs
                 (betree_list_t.BetreeListCons (k, msg) l)
@@ -414,25 +409,27 @@ mutual def betree_node_lookup_fwd
           | betree_message_t.BetreeMessageUpsert ufs =>
             do
               let (st1, v) ←
-                betree_internal_lookup_in_children_fwd node key st0
+                betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
+                  i0 n n0) key st0
               let (st2, v0) ←
                 betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k,
                   betree_message_t.BetreeMessageUpsert ufs) l) v key st1
               let node0 ←
-                betree_internal_lookup_in_children_back node key st0
+                betree_internal_lookup_in_children_back (mkbetree_internal_t i
+                  i0 n n0) key st0
+              let (mkbetree_internal_t i1 _ _ _) := node0
               let pending0 ←
                 betree_node_apply_upserts_back (betree_list_t.BetreeListCons
                   (k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1
               let msgs0 ←
                 betree_node_lookup_first_message_for_key_back key msgs pending0
-              let (st3, _) ←
-                betree_store_internal_node_fwd node0.betree_internal_id msgs0
-                  st2
+              let (st3, _) ← betree_store_internal_node_fwd i1 msgs0 st2
               Result.ret (st3, Option.some v0)
       | betree_list_t.BetreeListNil =>
         do
           let (st1, opt) ←
-            betree_internal_lookup_in_children_fwd node key st0
+            betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n
+              n0) key st0
           let _ ←
             betree_node_lookup_first_message_for_key_back key msgs
               betree_list_t.BetreeListNil
@@ -454,8 +451,8 @@ def betree_node_lookup_back
   match h: self with
   | betree_node_t.BetreeNodeInternal node =>
     do
-      let (st0, msgs) ←
-        betree_load_internal_node_fwd node.betree_internal_id st
+      let (mkbetree_internal_t i i0 n n0) := node
+      let (st0, msgs) ← betree_load_internal_node_fwd i st
       let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
       match h: pending with
       | betree_list_t.BetreeListCons p l =>
@@ -466,7 +463,9 @@ def betree_node_lookup_back
             let _ ←
               betree_node_lookup_first_message_for_key_back key msgs
                 (betree_list_t.BetreeListCons (k, msg) l)
-            let node0 ← betree_internal_lookup_in_children_back node key st0
+            let node0 ←
+              betree_internal_lookup_in_children_back (mkbetree_internal_t i i0
+                n n0) key st0
             Result.ret (betree_node_t.BetreeNodeInternal node0)
         else
           match h: msg with
@@ -476,38 +475,44 @@ def betree_node_lookup_back
                 betree_node_lookup_first_message_for_key_back key msgs
                   (betree_list_t.BetreeListCons (k,
                   betree_message_t.BetreeMessageInsert v) l)
-              Result.ret (betree_node_t.BetreeNodeInternal node)
+              Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
+                i i0 n n0))
           | betree_message_t.BetreeMessageDelete =>
             do
               let _ ←
                 betree_node_lookup_first_message_for_key_back key msgs
                   (betree_list_t.BetreeListCons (k,
                   betree_message_t.BetreeMessageDelete) l)
-              Result.ret (betree_node_t.BetreeNodeInternal node)
+              Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
+                i i0 n n0))
           | betree_message_t.BetreeMessageUpsert ufs =>
             do
               let (st1, v) ←
-                betree_internal_lookup_in_children_fwd node key st0
+                betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
+                  i0 n n0) key st0
               let (st2, _) ←
                 betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k,
                   betree_message_t.BetreeMessageUpsert ufs) l) v key st1
               let node0 ←
-                betree_internal_lookup_in_children_back node key st0
+                betree_internal_lookup_in_children_back (mkbetree_internal_t i
+                  i0 n n0) key st0
+              let (mkbetree_internal_t i1 i2 n1 n2) := node0
               let pending0 ←
                 betree_node_apply_upserts_back (betree_list_t.BetreeListCons
                   (k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1
               let msgs0 ←
                 betree_node_lookup_first_message_for_key_back key msgs pending0
-              let _ ←
-                betree_store_internal_node_fwd node0.betree_internal_id msgs0
-                  st2
-              Result.ret (betree_node_t.BetreeNodeInternal node0)
+              let _ ← betree_store_internal_node_fwd i1 msgs0 st2
+              Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
+                i1 i2 n1 n2))
       | betree_list_t.BetreeListNil =>
         do
           let _ ←
             betree_node_lookup_first_message_for_key_back key msgs
               betree_list_t.BetreeListNil
-          let node0 ← betree_internal_lookup_in_children_back node key st0
+          let node0 ←
+            betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n
+              n0) key st0
           Result.ret (betree_node_t.BetreeNodeInternal node0)
   | betree_node_t.BetreeNodeLeaf node =>
     do
@@ -523,9 +528,10 @@ def betree_internal_lookup_in_children_fwd
   (self : betree_internal_t) (key : UInt64) (st : State) :
   (Result (State × (Option UInt64)))
   :=
-  if h: key < self.betree_internal_pivot
-  then betree_node_lookup_fwd self.betree_internal_left key st
-  else betree_node_lookup_fwd self.betree_internal_right key st
+  let (mkbetree_internal_t _ i n n0) := self
+  if h: key < i
+  then betree_node_lookup_fwd n key st
+  else betree_node_lookup_fwd n0 key st
 termination_by betree_internal_lookup_in_children_fwd self key st =>
   betree_internal_lookup_in_children_terminates self key st
 decreasing_by betree_internal_lookup_in_children_decreases self key st
@@ -535,27 +541,16 @@ def betree_internal_lookup_in_children_back
   (self : betree_internal_t) (key : UInt64) (st : State) :
   (Result betree_internal_t)
   :=
-  if h: key < self.betree_internal_pivot
+  let (mkbetree_internal_t i i0 n n0) := self
+  if h: key < i0
   then
     do
-      let n ← betree_node_lookup_back self.betree_internal_left key st
-      Result.ret
-        {
-          betree_internal_id := self.betree_internal_id,
-          betree_internal_pivot := self.betree_internal_pivot,
-          betree_internal_left := n,
-          betree_internal_right := self.betree_internal_right
-        }
+      let n1 ← betree_node_lookup_back n key st
+      Result.ret (mkbetree_internal_t i i0 n1 n0)
   else
     do
-      let n ← betree_node_lookup_back self.betree_internal_right key st
-      Result.ret
-        {
-          betree_internal_id := self.betree_internal_id,
-          betree_internal_pivot := self.betree_internal_pivot,
-          betree_internal_left := self.betree_internal_left,
-          betree_internal_right := n
-        }
+      let n1 ← betree_node_lookup_back n0 key st
+      Result.ret (mkbetree_internal_t i i0 n n1)
 termination_by betree_internal_lookup_in_children_back self key st =>
   betree_internal_lookup_in_children_terminates self key st
 decreasing_by betree_internal_lookup_in_children_decreases self key st
@@ -819,8 +814,8 @@ mutual def betree_node_apply_messages_fwd
   match h: self with
   | betree_node_t.BetreeNodeInternal node =>
     do
-      let (st0, content) ←
-        betree_load_internal_node_fwd node.betree_internal_id st
+      let (mkbetree_internal_t i i0 n n0) := node
+      let (st0, content) ← betree_load_internal_node_fwd i st
       let content0 ←
         betree_node_apply_messages_to_internal_fwd_back content msgs
       let num_msgs ←
@@ -829,17 +824,17 @@ mutual def betree_node_apply_messages_fwd
       then
         do
           let (st1, content1) ←
-            betree_internal_flush_fwd node params node_id_cnt content0 st0
+            betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
+              node_id_cnt content0 st0
           let (node0, _) ←
-            betree_internal_flush_back node params node_id_cnt content0 st0
-          let (st2, _) ←
-            betree_store_internal_node_fwd node0.betree_internal_id content1
-              st1
+            betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
+              node_id_cnt content0 st0
+          let (mkbetree_internal_t i1 _ _ _) := node0
+          let (st2, _) ← betree_store_internal_node_fwd i1 content1 st1
           Result.ret (st2, ())
       else
         do
-          let (st1, _) ←
-            betree_store_internal_node_fwd node.betree_internal_id content0 st0
+          let (st1, _) ← betree_store_internal_node_fwd i content0 st0
           Result.ret (st1, ())
   | betree_node_t.BetreeNodeLeaf node =>
     do
@@ -878,8 +873,8 @@ def betree_node_apply_messages_back
   match h: self with
   | betree_node_t.BetreeNodeInternal node =>
     do
-      let (st0, content) ←
-        betree_load_internal_node_fwd node.betree_internal_id st
+      let (mkbetree_internal_t i i0 n n0) := node
+      let (st0, content) ← betree_load_internal_node_fwd i st
       let content0 ←
         betree_node_apply_messages_to_internal_fwd_back content msgs
       let num_msgs ←
@@ -888,18 +883,20 @@ def betree_node_apply_messages_back
       then
         do
           let (st1, content1) ←
-            betree_internal_flush_fwd node params node_id_cnt content0 st0
+            betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
+              node_id_cnt content0 st0
           let (node0, node_id_cnt0) ←
-            betree_internal_flush_back node params node_id_cnt content0 st0
-          let _ ←
-            betree_store_internal_node_fwd node0.betree_internal_id content1
-              st1
-          Result.ret (betree_node_t.BetreeNodeInternal node0, node_id_cnt0)
+            betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
+              node_id_cnt content0 st0
+          let (mkbetree_internal_t i1 i2 n1 n2) := node0
+          let _ ← betree_store_internal_node_fwd i1 content1 st1
+          Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t i1
+            i2 n1 n2), node_id_cnt0)
       else
         do
-          let _ ←
-            betree_store_internal_node_fwd node.betree_internal_id content0 st0
-          Result.ret (betree_node_t.BetreeNodeInternal node, node_id_cnt)
+          let _ ← betree_store_internal_node_fwd i content0 st0
+          Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t i
+            i0 n n0), node_id_cnt)
   | betree_node_t.BetreeNodeLeaf node =>
     do
       let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st
@@ -938,41 +935,36 @@ def betree_internal_flush_fwd
   (Result (State × (betree_list_t (UInt64 × betree_message_t))))
   :=
   do
-    let p ←
-      betree_list_partition_at_pivot_fwd betree_message_t content
-        self.betree_internal_pivot
+    let (mkbetree_internal_t _ i n n0) := self
+    let p ← betree_list_partition_at_pivot_fwd betree_message_t content i
     let (msgs_left, msgs_right) := p
     let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left
     if h: len_left >= params.betree_params_min_flush_size
     then
       do
         let (st0, _) ←
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st
+          betree_node_apply_messages_fwd n params node_id_cnt msgs_left st
         let (_, node_id_cnt0) ←
-          betree_node_apply_messages_back self.betree_internal_left params
-            node_id_cnt msgs_left st
+          betree_node_apply_messages_back n params node_id_cnt msgs_left st
         let len_right ←
           betree_list_len_fwd (UInt64 × betree_message_t) msgs_right
         if h: len_right >= params.betree_params_min_flush_size
         then
           do
             let (st1, _) ←
-              betree_node_apply_messages_fwd self.betree_internal_right params
-                node_id_cnt0 msgs_right st0
+              betree_node_apply_messages_fwd n0 params node_id_cnt0 msgs_right
+                st0
             let _ ←
-              betree_node_apply_messages_back self.betree_internal_right params
-                node_id_cnt0 msgs_right st0
+              betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
+                st0
             Result.ret (st1, betree_list_t.BetreeListNil)
         else Result.ret (st0, msgs_right)
     else
       do
         let (st0, _) ←
-          betree_node_apply_messages_fwd self.betree_internal_right params
-            node_id_cnt msgs_right st
+          betree_node_apply_messages_fwd n0 params node_id_cnt msgs_right st
         let _ ←
-          betree_node_apply_messages_back self.betree_internal_right params
-            node_id_cnt msgs_right st
+          betree_node_apply_messages_back n0 params node_id_cnt msgs_right st
         Result.ret (st0, msgs_left)
 termination_by betree_internal_flush_fwd self params node_id_cnt content st =>
   betree_internal_flush_terminates self params node_id_cnt content st
@@ -987,55 +979,32 @@ def betree_internal_flush_back
   (Result (betree_internal_t × betree_node_id_counter_t))
   :=
   do
-    let p ←
-      betree_list_partition_at_pivot_fwd betree_message_t content
-        self.betree_internal_pivot
+    let (mkbetree_internal_t i i0 n n0) := self
+    let p ← betree_list_partition_at_pivot_fwd betree_message_t content i0
     let (msgs_left, msgs_right) := p
     let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left
     if h: len_left >= params.betree_params_min_flush_size
     then
       do
         let (st0, _) ←
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st
-        let (n, node_id_cnt0) ←
-          betree_node_apply_messages_back self.betree_internal_left params
-            node_id_cnt msgs_left st
+          betree_node_apply_messages_fwd n params node_id_cnt msgs_left st
+        let (n1, node_id_cnt0) ←
+          betree_node_apply_messages_back n params node_id_cnt msgs_left st
         let len_right ←
           betree_list_len_fwd (UInt64 × betree_message_t) msgs_right
         if h: len_right >= params.betree_params_min_flush_size
         then
           do
-            let (n0, node_id_cnt1) ←
-              betree_node_apply_messages_back self.betree_internal_right params
-                node_id_cnt0 msgs_right st0
-            Result.ret
-              ({
-                 betree_internal_id := self.betree_internal_id,
-                 betree_internal_pivot := self.betree_internal_pivot,
-                 betree_internal_left := n,
-                 betree_internal_right := n0
-               }, node_id_cnt1)
-        else
-          Result.ret
-            ({
-               betree_internal_id := self.betree_internal_id,
-               betree_internal_pivot := self.betree_internal_pivot,
-               betree_internal_left := n,
-               betree_internal_right := self.betree_internal_right
-             }, node_id_cnt0)
+            let (n2, node_id_cnt1) ←
+              betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
+                st0
+            Result.ret (mkbetree_internal_t i i0 n1 n2, node_id_cnt1)
+        else Result.ret (mkbetree_internal_t i i0 n1 n0, node_id_cnt0)
     else
       do
-        let (n, node_id_cnt0) ←
-          betree_node_apply_messages_back self.betree_internal_right params
-            node_id_cnt msgs_right st
-        Result.ret
-          ({
-             betree_internal_id := self.betree_internal_id,
-             betree_internal_pivot := self.betree_internal_pivot,
-             betree_internal_left := self.betree_internal_left,
-             betree_internal_right := n
-           }, node_id_cnt0)
+        let (n1, node_id_cnt0) ←
+          betree_node_apply_messages_back n0 params node_id_cnt msgs_right st
+        Result.ret (mkbetree_internal_t i i0 n n1, node_id_cnt0)
 termination_by betree_internal_flush_back self params node_id_cnt content st =>
   betree_internal_flush_terminates self params node_id_cnt content st
 decreasing_by
@@ -1082,16 +1051,18 @@ def betree_be_tree_new_fwd
     let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt
     Result.ret (st0,
       {
-        betree_be_tree_params := {
-                                   betree_params_min_flush_size := min_flush_size,
-                                   betree_params_split_size := split_size
-                                 },
+        betree_be_tree_params :=
+          {
+            betree_params_min_flush_size := min_flush_size,
+            betree_params_split_size := split_size
+          },
         betree_be_tree_node_id_cnt := node_id_cnt0,
-        betree_be_tree_root := (betree_node_t.BetreeNodeLeaf
-                                 {
-                                   betree_leaf_id := id,
-                                   betree_leaf_size := (UInt64.ofNatCore 0 (by intlit))
-                                 })
+        betree_be_tree_root :=
+          (betree_node_t.BetreeNodeLeaf
+            {
+              betree_leaf_id := id,
+              betree_leaf_size := (UInt64.ofNatCore 0 (by intlit))
+            })
       })
 
 /- [betree_main::betree::BeTree::{6}::apply] -/
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index 392c8816..2d3904bb 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -49,8 +49,8 @@ def hashmap_hash_map_new_with_capacity_fwd
     Result.ret
       {
         hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)),
-        hashmap_hash_map_max_load_factor := (max_load_dividend,
-                                              max_load_divisor),
+        hashmap_hash_map_max_load_factor :=
+          (max_load_dividend, max_load_divisor),
         hashmap_hash_map_max_load := i0,
         hashmap_hash_map_slots := slots
       }
@@ -96,7 +96,8 @@ def hashmap_hash_map_clear_fwd_back
     Result.ret
       {
         hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)),
-        hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+        hashmap_hash_map_max_load_factor :=
+          self.hashmap_hash_map_max_load_factor,
         hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
         hashmap_hash_map_slots := v
       }
@@ -177,7 +178,8 @@ def hashmap_hash_map_insert_no_resize_fwd_back
         Result.ret
           {
             hashmap_hash_map_num_entries := i0,
-            hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+            hashmap_hash_map_max_load_factor :=
+              self.hashmap_hash_map_max_load_factor,
             hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
             hashmap_hash_map_slots := v
           }
@@ -190,7 +192,8 @@ def hashmap_hash_map_insert_no_resize_fwd_back
         Result.ret
           {
             hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries,
-            hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+            hashmap_hash_map_max_load_factor :=
+              self.hashmap_hash_map_max_load_factor,
             hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
             hashmap_hash_map_slots := v
           }
@@ -431,7 +434,8 @@ def hashmap_hash_map_get_mut_back
     Result.ret
       {
         hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries,
-        hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+        hashmap_hash_map_max_load_factor :=
+          self.hashmap_hash_map_max_load_factor,
         hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
         hashmap_hash_map_slots := v
       }
@@ -532,7 +536,8 @@ def hashmap_hash_map_remove_back
         Result.ret
           {
             hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries,
-            hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+            hashmap_hash_map_max_load_factor :=
+              self.hashmap_hash_map_max_load_factor,
             hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
             hashmap_hash_map_slots := v
           }
@@ -547,7 +552,8 @@ def hashmap_hash_map_remove_back
         Result.ret
           {
             hashmap_hash_map_num_entries := i0,
-            hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor,
+            hashmap_hash_map_max_load_factor :=
+              self.hashmap_hash_map_max_load_factor,
             hashmap_hash_map_max_load := self.hashmap_hash_map_max_load,
             hashmap_hash_map_slots := v
           }
diff --git a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
index cf7783b2..12d4190c 100644
--- a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
+++ b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
@@ -458,24 +458,24 @@ structure OpaqueDefs where
   def new_tuple1_fwd : Result (struct_with_tuple_t UInt32 UInt32) :=
     Result.ret
     {
-      struct_with_tuple_p := ((UInt32.ofNatCore 1 (by intlit)),
-                               (UInt32.ofNatCore 2 (by intlit)))
+      struct_with_tuple_p :=
+        ((UInt32.ofNatCore 1 (by intlit)), (UInt32.ofNatCore 2 (by intlit)))
     }
   
   /- [no_nested_borrows::new_tuple2] -/
   def new_tuple2_fwd : Result (struct_with_tuple_t Int16 Int16) :=
     Result.ret
     {
-      struct_with_tuple_p := ((Int16.ofNatCore 1 (by intlit)),
-                               (Int16.ofNatCore 2 (by intlit)))
+      struct_with_tuple_p :=
+        ((Int16.ofNatCore 1 (by intlit)), (Int16.ofNatCore 2 (by intlit)))
     }
   
   /- [no_nested_borrows::new_tuple3] -/
   def new_tuple3_fwd : Result (struct_with_tuple_t UInt64 Int64) :=
     Result.ret
     {
-      struct_with_tuple_p := ((UInt64.ofNatCore 1 (by intlit)),
-                               (Int64.ofNatCore 2 (by intlit)))
+      struct_with_tuple_p :=
+        ((UInt64.ofNatCore 1 (by intlit)), (Int64.ofNatCore 2 (by intlit)))
     }
   
   /- [no_nested_borrows::StructWithPair] -/
@@ -486,10 +486,11 @@ structure OpaqueDefs where
   def new_pair1_fwd : Result (struct_with_pair_t UInt32 UInt32) :=
     Result.ret
     {
-      struct_with_pair_p := {
-                              pair_x := (UInt32.ofNatCore 1 (by intlit)),
-                              pair_y := (UInt32.ofNatCore 2 (by intlit))
-                            }
+      struct_with_pair_p :=
+        {
+          pair_x := (UInt32.ofNatCore 1 (by intlit)),
+          pair_y := (UInt32.ofNatCore 2 (by intlit))
+        }
     }
   
   /- [no_nested_borrows::test_constants] -/
-- 
cgit v1.2.3