Regenerate the hashmap code and update the proofs

10 files changed, 681 insertions, 380 deletions

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 1ff3e576..5ec021d1 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -12,22 +12,30 @@ Module Hashmap_Funs.
 Definition hash_key_fwd (k : usize) : result usize := Return k.
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
-Fixpoint hash_map_allocate_slots_fwd
-  (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
+Fixpoint hash_map_allocate_slots_loop_fwd
+  (T : Type) (n : nat) (v : vec (List_t T)) (n0 : usize) :
   result (vec (List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    if n0 s= 0%usize
-    then Return slots
-    else (
-      slots0 <- vec_push_back (List_t T) slots ListNil;
-      i <- usize_sub n0 1%usize;
-      hash_map_allocate_slots_fwd T n1 slots0 i)
+    if n0 s> 0%usize
+    then (
+      slots <- vec_push_back (List_t T) v ListNil;
+      n2 <- usize_sub n0 1%usize;
+      hash_map_allocate_slots_loop_fwd T n1 slots n2)
+    else Return v
   end
 .
 
+(** [hashmap::HashMap::{0}::allocate_slots] *)
+Definition hash_map_allocate_slots_fwd
+  (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
+  result (vec (List_t T))
+  :=
+  hash_map_allocate_slots_loop_fwd T n slots n0
+.
+
 (** [hashmap::HashMap::{0}::new_with_capacity] *)
 Definition hash_map_new_with_capacity_fwd
   (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
@@ -48,27 +56,33 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
 .
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hash_map_clear_slots_fwd_back
-  (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
+Fixpoint hash_map_clear_slots_loop_fwd_back
+  (T : Type) (n : nat) (v : vec (List_t T)) (i : usize) :
   result (vec (List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (List_t T) slots in
+    let i0 := vec_len (List_t T) v in
     if i s< i0
     then (
-      slots0 <- vec_index_mut_back (List_t T) slots i ListNil;
       i1 <- usize_add i 1%usize;
-      hash_map_clear_slots_fwd_back T n0 slots0 i1)
-    else Return slots
+      slots <- vec_index_mut_back (List_t T) v i ListNil;
+      hash_map_clear_slots_loop_fwd_back T n0 slots i1)
+    else Return v
   end
 .
 
+(** [hashmap::HashMap::{0}::clear_slots] *)
+Definition hash_map_clear_slots_fwd_back
+  (T : Type) (n : nat) (slots : vec (List_t T)) : result (vec (List_t T)) :=
+  hash_map_clear_slots_loop_fwd_back T n slots (0%usize)
+.
+
 (** [hashmap::HashMap::{0}::clear] *)
 Definition hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
-  v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots) (0%usize);
+  v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots);
   Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor)
     self.(Hash_map_max_load) v)
 .
@@ -79,7 +93,7 @@ Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize :=
 .
 
 (** [hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hash_map_insert_in_list_fwd
+Fixpoint hash_map_insert_in_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
   result bool
   :=
@@ -87,17 +101,25 @@ Fixpoint hash_map_insert_in_list_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons ckey cvalue ls0 =>
+    | ListCons ckey cvalue tl =>
       if ckey s= key
       then Return false
-      else hash_map_insert_in_list_fwd T n0 key value ls0
+      else hash_map_insert_in_list_loop_fwd T n0 key value tl
     | ListNil => Return true
     end
   end
 .
 
 (** [hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hash_map_insert_in_list_back
+Definition hash_map_insert_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
+  result bool
+  :=
+  hash_map_insert_in_list_loop_fwd T n key value ls
+.
+
+(** [hashmap::HashMap::{0}::insert_in_list] *)
+Fixpoint hash_map_insert_in_list_loop_back
   (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
   result (List_t T)
   :=
@@ -105,17 +127,25 @@ Fixpoint hash_map_insert_in_list_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons ckey cvalue ls0 =>
+    | ListCons ckey cvalue tl =>
       if ckey s= key
-      then Return (ListCons ckey value ls0)
+      then Return (ListCons ckey value tl)
       else (
-        ls1 <- hash_map_insert_in_list_back T n0 key value ls0;
-        Return (ListCons ckey cvalue ls1))
+        l <- hash_map_insert_in_list_loop_back T n0 key value tl;
+        Return (ListCons ckey cvalue l))
     | ListNil => let l := ListNil in Return (ListCons key value l)
     end
   end
 .
 
+(** [hashmap::HashMap::{0}::insert_in_list] *)
+Definition hash_map_insert_in_list_back
+  (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
+  result (List_t T)
+  :=
+  hash_map_insert_in_list_loop_back T n key value ls
+.
+
 (** [hashmap::HashMap::{0}::insert_no_resize] *)
 Definition hash_map_insert_no_resize_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
@@ -145,8 +175,8 @@ Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
 Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
 
 (** [hashmap::HashMap::{0}::move_elements_from_list] *)
-Fixpoint hash_map_move_elements_from_list_fwd_back
-  (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
+Fixpoint hash_map_move_elements_from_list_loop_fwd_back
+  (T : Type) (n : nat) (hm : Hash_map_t T) (ls : List_t T) :
   result (Hash_map_t T)
   :=
   match n with
@@ -154,36 +184,52 @@ Fixpoint hash_map_move_elements_from_list_fwd_back
   | S n0 =>
     match ls with
     | ListCons k v tl =>
-      ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v;
-      hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl
-    | ListNil => Return ntable
+      ntable <- hash_map_insert_no_resize_fwd_back T n0 hm k v;
+      hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl
+    | ListNil => Return hm
     end
   end
 .
 
+(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+Definition hash_map_move_elements_from_list_fwd_back
+  (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
+  result (Hash_map_t T)
+  :=
+  hash_map_move_elements_from_list_loop_fwd_back T n ntable ls
+.
+
 (** [hashmap::HashMap::{0}::move_elements] *)
-Fixpoint hash_map_move_elements_fwd_back
-  (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
-  (i : usize) :
+Fixpoint hash_map_move_elements_loop_fwd_back
+  (T : Type) (n : nat) (hm : Hash_map_t T) (v : vec (List_t T)) (i : usize) :
   result ((Hash_map_t T) * (vec (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (List_t T) slots in
+    let i0 := vec_len (List_t T) v in
     if i s< i0
     then (
-      l <- vec_index_mut_fwd (List_t T) slots i;
+      l <- vec_index_mut_fwd (List_t T) v i;
       let ls := mem_replace_fwd (List_t T) l ListNil in
-      ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
-      let l0 := mem_replace_back (List_t T) l ListNil in
-      slots0 <- vec_index_mut_back (List_t T) slots i l0;
+      ntable <- hash_map_move_elements_from_list_fwd_back T n0 hm ls;
       i1 <- usize_add i 1%usize;
-      hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1)
-    else Return (ntable, slots)
+      let l0 := mem_replace_back (List_t T) l ListNil in
+      slots <- vec_index_mut_back (List_t T) v i l0;
+      hash_map_move_elements_loop_fwd_back T n0 ntable slots i1)
+    else Return (hm, v)
   end
 .
 
+(** [hashmap::HashMap::{0}::move_elements] *)
+Definition hash_map_move_elements_fwd_back
+  (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
+  (i : usize) :
+  result ((Hash_map_t T) * (vec (List_t T)))
+  :=
+  hash_map_move_elements_loop_fwd_back T n ntable slots i
+.
+
 (** [hashmap::HashMap::{0}::try_resize] *)
 Definition hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
@@ -220,21 +266,27 @@ Definition hash_map_insert_fwd_back
 .
 
 (** [hashmap::HashMap::{0}::contains_key_in_list] *)
-Fixpoint hash_map_contains_key_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
+Fixpoint hash_map_contains_key_in_list_loop_fwd
+  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons ckey t ls0 =>
-      if ckey s= key
+    | ListCons ckey t tl =>
+      if ckey s= i
       then Return true
-      else hash_map_contains_key_in_list_fwd T n0 key ls0
+      else hash_map_contains_key_in_list_loop_fwd T n0 i tl
     | ListNil => Return false
     end
   end
 .
 
+(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+Definition hash_map_contains_key_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
+  hash_map_contains_key_in_list_loop_fwd T n key ls
+.
+
 (** [hashmap::HashMap::{0}::contains_key] *)
 Definition hash_map_contains_key_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result bool :=
@@ -246,21 +298,27 @@ Definition hash_map_contains_key_fwd
 .
 
 (** [hashmap::HashMap::{0}::get_in_list] *)
-Fixpoint hash_map_get_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
+Fixpoint hash_map_get_in_list_loop_fwd
+  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons ckey cvalue ls0 =>
-      if ckey s= key
+    | ListCons ckey cvalue tl =>
+      if ckey s= i
       then Return cvalue
-      else hash_map_get_in_list_fwd T n0 key ls0
+      else hash_map_get_in_list_loop_fwd T n0 i tl
     | ListNil => Fail_ Failure
     end
   end
 .
 
+(** [hashmap::HashMap::{0}::get_in_list] *)
+Definition hash_map_get_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
+  hash_map_get_in_list_loop_fwd T n key ls
+.
+
 (** [hashmap::HashMap::{0}::get] *)
 Definition hash_map_get_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
@@ -272,41 +330,55 @@ Definition hash_map_get_fwd
 .
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hash_map_get_mut_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
+Fixpoint hash_map_get_mut_in_list_loop_fwd
+  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons ckey cvalue ls0 =>
-      if ckey s= key
+    | ListCons ckey cvalue tl =>
+      if ckey s= i
       then Return cvalue
-      else hash_map_get_mut_in_list_fwd T n0 key ls0
+      else hash_map_get_mut_in_list_loop_fwd T n0 i tl
     | ListNil => Fail_ Failure
     end
   end
 .
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hash_map_get_mut_in_list_back
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) :
+Definition hash_map_get_mut_in_list_fwd
+  (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
+  hash_map_get_mut_in_list_loop_fwd T n key ls
+.
+
+(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+Fixpoint hash_map_get_mut_in_list_loop_back
+  (T : Type) (n : nat) (i : usize) (ls : List_t T) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | ListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return (ListCons ckey ret ls0)
+    | ListCons ckey cvalue tl =>
+      if ckey s= i
+      then Return (ListCons ckey ret tl)
       else (
-        ls1 <- hash_map_get_mut_in_list_back T n0 key ls0 ret;
-        Return (ListCons ckey cvalue ls1))
+        l <- hash_map_get_mut_in_list_loop_back T n0 i tl ret;
+        Return (ListCons ckey cvalue l))
     | ListNil => Fail_ Failure
     end
   end
 .
 
+(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+Definition hash_map_get_mut_in_list_back
+  (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
+  result (List_t T)
+  :=
+  hash_map_get_mut_in_list_loop_back T n key ls ret
+.
+
 (** [hashmap::HashMap::{0}::get_mut] *)
 Definition hash_map_get_mut_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
@@ -314,7 +386,7 @@ Definition hash_map_get_mut_fwd
   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;
-  hash_map_get_mut_in_list_fwd T n key l
+  hash_map_get_mut_in_list_fwd T n l key
 .
 
 (** [hashmap::HashMap::{0}::get_mut] *)
@@ -326,56 +398,68 @@ Definition hash_map_get_mut_back
   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 n key l ret;
+  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)
 .
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hash_map_remove_from_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
+Fixpoint hash_map_remove_from_list_loop_fwd
+  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (option T) :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey t tl =>
-      if ckey s= key
+      if ckey s= i
       then
         let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
         match mv_ls with
-        | ListCons i cvalue tl0 => Return (Some cvalue)
+        | ListCons i0 cvalue tl0 => Return (Some cvalue)
         | ListNil => Fail_ Failure
         end
-      else hash_map_remove_from_list_fwd T n0 key tl
+      else hash_map_remove_from_list_loop_fwd T n0 i tl
     | ListNil => Return None
     end
   end
 .
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hash_map_remove_from_list_back
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
+Definition hash_map_remove_from_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
+  hash_map_remove_from_list_loop_fwd T n key ls
+.
+
+(** [hashmap::HashMap::{0}::remove_from_list] *)
+Fixpoint hash_map_remove_from_list_loop_back
+  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (List_t T) :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey t tl =>
-      if ckey s= key
+      if ckey s= i
       then
         let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
         match mv_ls with
-        | ListCons i cvalue tl0 => Return tl0
+        | ListCons i0 cvalue tl0 => Return tl0
         | ListNil => Fail_ Failure
         end
       else (
-        tl0 <- hash_map_remove_from_list_back T n0 key tl;
-        Return (ListCons ckey t tl0))
+        l <- hash_map_remove_from_list_loop_back T n0 i tl;
+        Return (ListCons ckey t l))
     | ListNil => Return ListNil
     end
   end
 .
 
+(** [hashmap::HashMap::{0}::remove_from_list] *)
+Definition hash_map_remove_from_list_back
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
+  hash_map_remove_from_list_loop_back T n key ls
+.
+
 (** [hashmap::HashMap::{0}::remove] *)
 Definition hash_map_remove_fwd
   (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
@@ -389,9 +473,7 @@ Definition hash_map_remove_fwd
   match x with
   | None => Return None
   | Some x0 =>
-    i0 <- usize_sub self.(Hash_map_num_entries) 1%usize;
-    let _ := i0 in
-    Return (Some x0)
+    _ <- usize_sub self.(Hash_map_num_entries) 1%usize; Return (Some x0)
   end
 .
 
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 3eaaec8a..9ae7942c 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -14,22 +14,30 @@ Module HashmapMain_Funs.
 Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
-Fixpoint hashmap_hash_map_allocate_slots_fwd
-  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
+Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
+  (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (n0 : usize) :
   result (vec (Hashmap_list_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    if n0 s= 0%usize
-    then Return slots
-    else (
-      slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil;
-      i <- usize_sub n0 1%usize;
-      hashmap_hash_map_allocate_slots_fwd T n1 slots0 i)
+    if n0 s> 0%usize
+    then (
+      slots <- vec_push_back (Hashmap_list_t T) v HashmapListNil;
+      n2 <- usize_sub n0 1%usize;
+      hashmap_hash_map_allocate_slots_loop_fwd T n1 slots n2)
+    else Return v
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+Definition hashmap_hash_map_allocate_slots_fwd
+  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
+  result (vec (Hashmap_list_t T))
+  :=
+  hashmap_hash_map_allocate_slots_loop_fwd T n slots n0
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
 Definition hashmap_hash_map_new_with_capacity_fwd
   (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
@@ -51,31 +59,37 @@ Definition hashmap_hash_map_new_fwd
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hashmap_hash_map_clear_slots_fwd_back
-  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
+Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back
+  (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (i : usize) :
   result (vec (Hashmap_list_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (Hashmap_list_t T) slots in
+    let i0 := vec_len (Hashmap_list_t T) v in
     if i s< i0
     then (
-      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
       i1 <- usize_add i 1%usize;
-      hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1)
-    else Return slots
+      slots <- vec_index_mut_back (Hashmap_list_t T) v i HashmapListNil;
+      hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots i1)
+    else Return v
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
+Definition hashmap_hash_map_clear_slots_fwd_back
+  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) :
+  result (vec (Hashmap_list_t T))
+  :=
+  hashmap_hash_map_clear_slots_loop_fwd_back T n slots (0%usize)
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
 Definition hashmap_hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
   result (Hashmap_hash_map_t T)
   :=
-  v <-
-    hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots)
-      (0%usize);
+  v <- hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots);
   Return (mkHashmap_hash_map_t (0%usize)
     self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v)
 .
@@ -87,7 +101,7 @@ Definition hashmap_hash_map_len_fwd
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hashmap_hash_map_insert_in_list_fwd
+Fixpoint hashmap_hash_map_insert_in_list_loop_fwd
   (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
   result bool
   :=
@@ -95,17 +109,25 @@ Fixpoint hashmap_hash_map_insert_in_list_fwd
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | HashmapListCons ckey cvalue ls0 =>
+    | HashmapListCons ckey cvalue tl =>
       if ckey s= key
       then Return false
-      else hashmap_hash_map_insert_in_list_fwd T n0 key value ls0
+      else hashmap_hash_map_insert_in_list_loop_fwd T n0 key value tl
     | HashmapListNil => Return true
     end
   end
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hashmap_hash_map_insert_in_list_back
+Definition hashmap_hash_map_insert_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
+  result bool
+  :=
+  hashmap_hash_map_insert_in_list_loop_fwd T n key value ls
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+Fixpoint hashmap_hash_map_insert_in_list_loop_back
   (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
   result (Hashmap_list_t T)
   :=
@@ -113,18 +135,26 @@ Fixpoint hashmap_hash_map_insert_in_list_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | HashmapListCons ckey cvalue ls0 =>
+    | HashmapListCons ckey cvalue tl =>
       if ckey s= key
-      then Return (HashmapListCons ckey value ls0)
+      then Return (HashmapListCons ckey value tl)
       else (
-        ls1 <- hashmap_hash_map_insert_in_list_back T n0 key value ls0;
-        Return (HashmapListCons ckey cvalue ls1))
+        l <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl;
+        Return (HashmapListCons ckey cvalue l))
     | HashmapListNil =>
       let l := HashmapListNil in Return (HashmapListCons key value l)
     end
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+Definition hashmap_hash_map_insert_in_list_back
+  (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
+  result (Hashmap_list_t T)
+  :=
+  hashmap_hash_map_insert_in_list_loop_back T n key value ls
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
 Definition hashmap_hash_map_insert_no_resize_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
@@ -161,9 +191,8 @@ Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
 Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
-Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back
-  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
-  :
+Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
+  (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) :
   result (Hashmap_hash_map_t T)
   :=
   match n with
@@ -171,37 +200,54 @@ Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back
   | S n0 =>
     match ls with
     | HashmapListCons k v tl =>
-      ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v;
-      hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl
-    | HashmapListNil => Return ntable
+      ntable <- hashmap_hash_map_insert_no_resize_fwd_back T n0 hm k v;
+      hashmap_hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl
+    | HashmapListNil => Return hm
     end
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+Definition hashmap_hash_map_move_elements_from_list_fwd_back
+  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
+  :
+  result (Hashmap_hash_map_t T)
+  :=
+  hashmap_hash_map_move_elements_from_list_loop_fwd_back T n ntable ls
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
-Fixpoint hashmap_hash_map_move_elements_fwd_back
-  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
-  (slots : vec (Hashmap_list_t T)) (i : usize) :
+Fixpoint hashmap_hash_map_move_elements_loop_fwd_back
+  (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (v : vec (Hashmap_list_t T))
+  (i : usize) :
   result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (Hashmap_list_t T) slots in
+    let i0 := vec_len (Hashmap_list_t T) v in
     if i s< i0
     then (
-      l <- vec_index_mut_fwd (Hashmap_list_t T) slots i;
+      l <- vec_index_mut_fwd (Hashmap_list_t T) v i;
       let ls := mem_replace_fwd (Hashmap_list_t T) l HashmapListNil in
-      ntable0 <-
-        hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
-      let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in
-      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0;
+      ntable <- hashmap_hash_map_move_elements_from_list_fwd_back T n0 hm ls;
       i1 <- usize_add i 1%usize;
-      hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1)
-    else Return (ntable, slots)
+      let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in
+      slots <- vec_index_mut_back (Hashmap_list_t T) v i l0;
+      hashmap_hash_map_move_elements_loop_fwd_back T n0 ntable slots i1)
+    else Return (hm, v)
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+Definition hashmap_hash_map_move_elements_fwd_back
+  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
+  (slots : vec (Hashmap_list_t T)) (i : usize) :
+  result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T)))
+  :=
+  hashmap_hash_map_move_elements_loop_fwd_back T n ntable slots i
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
 Definition hashmap_hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
@@ -241,21 +287,27 @@ Definition hashmap_hash_map_insert_fwd_back
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
-Fixpoint hashmap_hash_map_contains_key_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
+Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd
+  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | HashmapListCons ckey t ls0 =>
-      if ckey s= key
+    | HashmapListCons ckey t tl =>
+      if ckey s= i
       then Return true
-      else hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0
+      else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 i tl
     | HashmapListNil => Return false
     end
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+Definition hashmap_hash_map_contains_key_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
+  hashmap_hash_map_contains_key_in_list_loop_fwd T n key ls
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
 Definition hashmap_hash_map_contains_key_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
@@ -269,21 +321,27 @@ Definition hashmap_hash_map_contains_key_fwd
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
-Fixpoint hashmap_hash_map_get_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+Fixpoint hashmap_hash_map_get_in_list_loop_fwd
+  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | HashmapListCons ckey cvalue ls0 =>
-      if ckey s= key
+    | HashmapListCons ckey cvalue tl =>
+      if ckey s= i
       then Return cvalue
-      else hashmap_hash_map_get_in_list_fwd T n0 key ls0
+      else hashmap_hash_map_get_in_list_loop_fwd T n0 i tl
     | HashmapListNil => Fail_ Failure
     end
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+Definition hashmap_hash_map_get_in_list_fwd
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+  hashmap_hash_map_get_in_list_loop_fwd T n key ls
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::get] *)
 Definition hashmap_hash_map_get_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
@@ -297,41 +355,55 @@ Definition hashmap_hash_map_get_fwd
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hashmap_hash_map_get_mut_in_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
+  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | HashmapListCons ckey cvalue ls0 =>
-      if ckey s= key
+    | HashmapListCons ckey cvalue tl =>
+      if ckey s= i
       then Return cvalue
-      else hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0
+      else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 i tl
     | HashmapListNil => Fail_ Failure
     end
   end
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hashmap_hash_map_get_mut_in_list_back
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) :
+Definition hashmap_hash_map_get_mut_in_list_fwd
+  (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
+  hashmap_hash_map_get_mut_in_list_loop_fwd T n key ls
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
+  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) (ret : T) :
   result (Hashmap_list_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
-    | HashmapListCons ckey cvalue ls0 =>
-      if ckey s= key
-      then Return (HashmapListCons ckey ret ls0)
+    | HashmapListCons ckey cvalue tl =>
+      if ckey s= i
+      then Return (HashmapListCons ckey ret tl)
       else (
-        ls1 <- hashmap_hash_map_get_mut_in_list_back T n0 key ls0 ret;
-        Return (HashmapListCons ckey cvalue ls1))
+        l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 i tl ret;
+        Return (HashmapListCons ckey cvalue l))
     | HashmapListNil => Fail_ Failure
     end
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+Definition hashmap_hash_map_get_mut_in_list_back
+  (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
+  result (Hashmap_list_t T)
+  :=
+  hashmap_hash_map_get_mut_in_list_loop_back T n key ls ret
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
 Definition hashmap_hash_map_get_mut_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
@@ -342,7 +414,7 @@ Definition hashmap_hash_map_get_mut_fwd
   hash_mod <- usize_rem hash i;
   l <-
     vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
-  hashmap_hash_map_get_mut_in_list_fwd T n key l
+  hashmap_hash_map_get_mut_in_list_fwd T n l key
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
@@ -355,7 +427,7 @@ Definition hashmap_hash_map_get_mut_back
   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 n key l ret;
+  l0 <- hashmap_hash_map_get_mut_in_list_back T n l key ret;
   v <-
     vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
       hash_mod l0;
@@ -364,8 +436,8 @@ Definition hashmap_hash_map_get_mut_back
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hashmap_hash_map_remove_from_list_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
+Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
+  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) :
   result (option T)
   :=
   match n with
@@ -373,24 +445,32 @@ Fixpoint hashmap_hash_map_remove_from_list_fwd
   | S n0 =>
     match ls with
     | HashmapListCons ckey t tl =>
-      if ckey s= key
+      if ckey s= i
       then
         let mv_ls :=
           mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
             HashmapListNil in
         match mv_ls with
-        | HashmapListCons i cvalue tl0 => Return (Some cvalue)
+        | HashmapListCons i0 cvalue tl0 => Return (Some cvalue)
         | HashmapListNil => Fail_ Failure
         end
-      else hashmap_hash_map_remove_from_list_fwd T n0 key tl
+      else hashmap_hash_map_remove_from_list_loop_fwd T n0 i tl
     | HashmapListNil => Return None
     end
   end
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hashmap_hash_map_remove_from_list_back
+Definition hashmap_hash_map_remove_from_list_fwd
   (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
+  result (option T)
+  :=
+  hashmap_hash_map_remove_from_list_loop_fwd T n key ls
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+Fixpoint hashmap_hash_map_remove_from_list_loop_back
+  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) :
   result (Hashmap_list_t T)
   :=
   match n with
@@ -398,23 +478,31 @@ Fixpoint hashmap_hash_map_remove_from_list_back
   | S n0 =>
     match ls with
     | HashmapListCons ckey t tl =>
-      if ckey s= key
+      if ckey s= i
       then
         let mv_ls :=
           mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
             HashmapListNil in
         match mv_ls with
-        | HashmapListCons i cvalue tl0 => Return tl0
+        | HashmapListCons i0 cvalue tl0 => Return tl0
         | HashmapListNil => Fail_ Failure
         end
       else (
-        tl0 <- hashmap_hash_map_remove_from_list_back T n0 key tl;
-        Return (HashmapListCons ckey t tl0))
+        l <- hashmap_hash_map_remove_from_list_loop_back T n0 i tl;
+        Return (HashmapListCons ckey t l))
     | HashmapListNil => Return HashmapListNil
     end
   end
 .
 
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+Definition hashmap_hash_map_remove_from_list_back
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
+  result (Hashmap_list_t T)
+  :=
+  hashmap_hash_map_remove_from_list_loop_back T n key ls
+.
+
 (** [hashmap_main::hashmap::HashMap::{0}::remove] *)
 Definition hashmap_hash_map_remove_fwd
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
@@ -429,8 +517,7 @@ Definition hashmap_hash_map_remove_fwd
   match x with
   | None => Return None
   | Some x0 =>
-    i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
-    let _ := i0 in
+    _ <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
     Return (Some x0)
   end
 .
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 90390c1b..b5476f25 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -46,10 +46,7 @@ Definition test_new_non_zero_u32_fwd
 
 (** [external::test_vec] *)
 Definition test_vec_fwd : result unit :=
-  let v := vec_new u32 in
-  v0 <- vec_push_back u32 v (0%u32);
-  let _ := v0 in
-  Return tt
+  let v := vec_new u32 in _ <- vec_push_back u32 v (0%u32); Return tt
 .
 
 (** Unit test for [external::test_vec] *)
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index e91cf81a..10654887 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -67,9 +67,7 @@ Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y.
 Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x.
 
 (** [no_nested_borrows::test2] *)
-Definition test2_fwd : result unit :=
-  i <- u32_add 23%u32 44%u32; let _ := i in Return tt
-.
+Definition test2_fwd : result unit := _ <- u32_add 23%u32 44%u32; Return tt.
 
 (** Unit test for [no_nested_borrows::test2] *)
 Check (test2_fwd )%return.
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index c06a6b9e..01fc457e 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -272,7 +272,7 @@ let betree_leaf_split_back0
             | Return (st1, _) ->
               begin match betree_store_leaf_node_fwd id1 content1 st1 with
               | Fail e -> Fail e
-              | Return (_, _) -> Return (st0, ())
+              | Return _ -> Return (st0, ())
               end
             end
           end
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index 3e51c6f1..b8890f86 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -8,14 +8,14 @@ open Hashmap.Types
 
 (** [hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
 unfold
-let hash_map_allocate_slots_decreases (t : Type0) (slots : vec (list_t t))
+let hash_map_allocate_slots_decreases (t : Type0) (v : vec (list_t t))
   (n : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::clear_slots]: decreases clause *)
 unfold
-let hash_map_clear_slots_decreases (t : Type0) (slots : vec (list_t t))
-  (i : usize) : nat =
+let hash_map_clear_slots_decreases (t : Type0) (v : vec (list_t t)) (i : usize)
+  : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
@@ -30,37 +30,37 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 
 (** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
 unfold
-let hash_map_move_elements_from_list_decreases (t : Type0)
-  (ntable : hash_map_t t) (ls : list_t t) : nat =
+let hash_map_move_elements_from_list_decreases (t : Type0) (hm : hash_map_t t)
+  (ls : list_t t) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::move_elements]: decreases clause *)
 unfold
-let hash_map_move_elements_decreases (t : Type0) (ntable : hash_map_t t)
-  (slots : vec (list_t t)) (i : usize) : nat =
+let hash_map_move_elements_decreases (t : Type0) (hm : hash_map_t t)
+  (v : vec (list_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *)
 unfold
-let hash_map_contains_key_in_list_decreases (t : Type0) (key : usize)
+let hash_map_contains_key_in_list_decreases (t : Type0) (i : usize)
   (ls : list_t t) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::get_in_list]: decreases clause *)
 unfold
-let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
+let hash_map_get_in_list_decreases (t : Type0) (i : usize) (ls : list_t t) :
   nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
 unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
-  (ls : list_t t) : nat =
+let hash_map_get_mut_in_list_decreases (t : Type0) (i : usize) (ls : list_t t)
+  : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
 unfold
-let hash_map_remove_from_list_decreases (t : Type0) (key : usize)
-  (ls : list_t t) : nat =
+let hash_map_remove_from_list_decreases (t : Type0) (i : usize) (ls : list_t t)
+  : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 59c4e125..d81da40b 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -11,22 +11,27 @@ include Hashmap.Clauses
 let hash_key_fwd (k : usize) : result usize = Return k
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
-let rec hash_map_allocate_slots_fwd
-  (t : Type0) (slots : vec (list_t t)) (n : usize) :
+let rec hash_map_allocate_slots_loop_fwd
+  (t : Type0) (v : vec (list_t t)) (n : usize) :
   Tot (result (vec (list_t t)))
-  (decreases (hash_map_allocate_slots_decreases t slots n))
+  (decreases (hash_map_allocate_slots_decreases t v n))
   =
-  if n = 0
-  then Return slots
-  else
-    begin match vec_push_back (list_t t) slots ListNil with
+  if n > 0
+  then
+    begin match vec_push_back (list_t t) v ListNil with
     | Fail e -> Fail e
-    | Return slots0 ->
+    | Return slots ->
       begin match usize_sub n 1 with
       | Fail e -> Fail e
-      | Return i -> hash_map_allocate_slots_fwd t slots0 i
+      | Return n0 -> hash_map_allocate_slots_loop_fwd t slots n0
       end
     end
+  else Return v
+
+(** [hashmap::HashMap::{0}::allocate_slots] *)
+let hash_map_allocate_slots_fwd
+  (t : Type0) (slots : vec (list_t t)) (n : usize) : result (vec (list_t t)) =
+  hash_map_allocate_slots_loop_fwd t slots n
 
 (** [hashmap::HashMap::{0}::new_with_capacity] *)
 let hash_map_new_with_capacity_fwd
@@ -54,28 +59,33 @@ let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
   hash_map_new_with_capacity_fwd t 32 4 5
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
-let rec hash_map_clear_slots_fwd_back
-  (t : Type0) (slots : vec (list_t t)) (i : usize) :
+let rec hash_map_clear_slots_loop_fwd_back
+  (t : Type0) (v : vec (list_t t)) (i : usize) :
   Tot (result (vec (list_t t)))
-  (decreases (hash_map_clear_slots_decreases t slots i))
+  (decreases (hash_map_clear_slots_decreases t v i))
   =
-  let i0 = vec_len (list_t t) slots in
+  let i0 = vec_len (list_t t) v in
   if i < i0
   then
-    begin match vec_index_mut_back (list_t t) slots i ListNil with
+    begin match usize_add i 1 with
     | Fail e -> Fail e
-    | Return slots0 ->
-      begin match usize_add i 1 with
+    | Return i1 ->
+      begin match vec_index_mut_back (list_t t) v i ListNil with
       | Fail e -> Fail e
-      | Return i1 -> hash_map_clear_slots_fwd_back t slots0 i1
+      | Return slots -> hash_map_clear_slots_loop_fwd_back t slots i1
       end
     end
-  else Return slots
+  else Return v
+
+(** [hashmap::HashMap::{0}::clear_slots] *)
+let hash_map_clear_slots_fwd_back
+  (t : Type0) (slots : vec (list_t t)) : result (vec (list_t t)) =
+  hash_map_clear_slots_loop_fwd_back t slots 0
 
 (** [hashmap::HashMap::{0}::clear] *)
 let hash_map_clear_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
-  begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with
+  begin match hash_map_clear_slots_fwd_back t self.hash_map_slots with
   | Fail e -> Fail e
   | Return v ->
     Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load
@@ -87,37 +97,47 @@ let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
   Return self.hash_map_num_entries
 
 (** [hashmap::HashMap::{0}::insert_in_list] *)
-let rec hash_map_insert_in_list_fwd
+let rec hash_map_insert_in_list_loop_fwd
   (t : Type0) (key : usize) (value : t) (ls : list_t t) :
   Tot (result bool)
   (decreases (hash_map_insert_in_list_decreases t key value ls))
   =
   begin match ls with
-  | ListCons ckey cvalue ls0 ->
+  | ListCons ckey cvalue tl ->
     if ckey = key
     then Return false
-    else hash_map_insert_in_list_fwd t key value ls0
+    else hash_map_insert_in_list_loop_fwd t key value tl
   | ListNil -> Return true
   end
 
 (** [hashmap::HashMap::{0}::insert_in_list] *)
-let rec hash_map_insert_in_list_back
+let hash_map_insert_in_list_fwd
+  (t : Type0) (key : usize) (value : t) (ls : list_t t) : result bool =
+  hash_map_insert_in_list_loop_fwd t key value ls
+
+(** [hashmap::HashMap::{0}::insert_in_list] *)
+let rec hash_map_insert_in_list_loop_back
   (t : Type0) (key : usize) (value : t) (ls : list_t t) :
   Tot (result (list_t t))
   (decreases (hash_map_insert_in_list_decreases t key value ls))
   =
   begin match ls with
-  | ListCons ckey cvalue ls0 ->
+  | ListCons ckey cvalue tl ->
     if ckey = key
-    then Return (ListCons ckey value ls0)
+    then Return (ListCons ckey value tl)
     else
-      begin match hash_map_insert_in_list_back t key value ls0 with
+      begin match hash_map_insert_in_list_loop_back t key value tl with
       | Fail e -> Fail e
-      | Return ls1 -> Return (ListCons ckey cvalue ls1)
+      | Return l -> Return (ListCons ckey cvalue l)
       end
   | ListNil -> let l = ListNil in Return (ListCons key value l)
   end
 
+(** [hashmap::HashMap::{0}::insert_in_list] *)
+let hash_map_insert_in_list_back
+  (t : Type0) (key : usize) (value : t) (ls : list_t t) : result (list_t t) =
+  hash_map_insert_in_list_loop_back t key value ls
+
 (** [hashmap::HashMap::{0}::insert_no_resize] *)
 let hash_map_insert_no_resize_fwd_back
   (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
@@ -178,48 +198,62 @@ let core_num_u32_max_body : result u32 = Return 4294967295
 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 
 (** [hashmap::HashMap::{0}::move_elements_from_list] *)
-let rec hash_map_move_elements_from_list_fwd_back
-  (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
+let rec hash_map_move_elements_from_list_loop_fwd_back
+  (t : Type0) (hm : hash_map_t t) (ls : list_t t) :
   Tot (result (hash_map_t t))
-  (decreases (hash_map_move_elements_from_list_decreases t ntable ls))
+  (decreases (hash_map_move_elements_from_list_decreases t hm ls))
   =
   begin match ls with
   | ListCons k v tl ->
-    begin match hash_map_insert_no_resize_fwd_back t ntable k v with
+    begin match hash_map_insert_no_resize_fwd_back t hm k v with
     | Fail e -> Fail e
-    | Return ntable0 -> hash_map_move_elements_from_list_fwd_back t ntable0 tl
+    | Return ntable ->
+      hash_map_move_elements_from_list_loop_fwd_back t ntable tl
     end
-  | ListNil -> Return ntable
+  | ListNil -> Return hm
   end
 
+(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+let hash_map_move_elements_from_list_fwd_back
+  (t : Type0) (ntable : hash_map_t t) (ls : list_t t) : result (hash_map_t t) =
+  hash_map_move_elements_from_list_loop_fwd_back t ntable ls
+
 (** [hashmap::HashMap::{0}::move_elements] *)
-let rec hash_map_move_elements_fwd_back
-  (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
+let rec hash_map_move_elements_loop_fwd_back
+  (t : Type0) (hm : hash_map_t t) (v : vec (list_t t)) (i : usize) :
   Tot (result ((hash_map_t t) & (vec (list_t t))))
-  (decreases (hash_map_move_elements_decreases t ntable slots i))
+  (decreases (hash_map_move_elements_decreases t hm v i))
   =
-  let i0 = vec_len (list_t t) slots in
+  let i0 = vec_len (list_t t) v in
   if i < i0
   then
-    begin match vec_index_mut_fwd (list_t t) slots i with
+    begin match vec_index_mut_fwd (list_t t) v i with
     | Fail e -> Fail e
     | Return l ->
       let ls = mem_replace_fwd (list_t t) l ListNil in
-      begin match hash_map_move_elements_from_list_fwd_back t ntable ls with
+      begin match hash_map_move_elements_from_list_fwd_back t hm ls with
       | Fail e -> Fail e
-      | Return ntable0 ->
-        let l0 = mem_replace_back (list_t t) l ListNil in
-        begin match vec_index_mut_back (list_t t) slots i l0 with
+      | Return ntable ->
+        begin match usize_add i 1 with
         | Fail e -> Fail e
-        | Return slots0 ->
-          begin match usize_add i 1 with
+        | Return i1 ->
+          let l0 = mem_replace_back (list_t t) l ListNil in
+          begin match vec_index_mut_back (list_t t) v i l0 with
           | Fail e -> Fail e
-          | Return i1 -> hash_map_move_elements_fwd_back t ntable0 slots0 i1
+          | Return slots ->
+            hash_map_move_elements_loop_fwd_back t ntable slots i1
           end
         end
       end
     end
-  else Return (ntable, slots)
+  else Return (hm, v)
+
+(** [hashmap::HashMap::{0}::move_elements] *)
+let hash_map_move_elements_fwd_back
+  (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
+  result ((hash_map_t t) & (vec (list_t t)))
+  =
+  hash_map_move_elements_loop_fwd_back t ntable slots i
 
 (** [hashmap::HashMap::{0}::try_resize] *)
 let hash_map_try_resize_fwd_back
@@ -278,19 +312,24 @@ let hash_map_insert_fwd_back
   end
 
 (** [hashmap::HashMap::{0}::contains_key_in_list] *)
-let rec hash_map_contains_key_in_list_fwd
-  (t : Type0) (key : usize) (ls : list_t t) :
+let rec hash_map_contains_key_in_list_loop_fwd
+  (t : Type0) (i : usize) (ls : list_t t) :
   Tot (result bool)
-  (decreases (hash_map_contains_key_in_list_decreases t key ls))
+  (decreases (hash_map_contains_key_in_list_decreases t i ls))
   =
   begin match ls with
-  | ListCons ckey x ls0 ->
-    if ckey = key
+  | ListCons ckey x tl ->
+    if ckey = i
     then Return true
-    else hash_map_contains_key_in_list_fwd t key ls0
+    else hash_map_contains_key_in_list_loop_fwd t i tl
   | ListNil -> Return false
   end
 
+(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+let hash_map_contains_key_in_list_fwd
+  (t : Type0) (key : usize) (ls : list_t t) : result bool =
+  hash_map_contains_key_in_list_loop_fwd t key ls
+
 (** [hashmap::HashMap::{0}::contains_key] *)
 let hash_map_contains_key_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result bool =
@@ -309,16 +348,21 @@ let hash_map_contains_key_fwd
   end
 
 (** [hashmap::HashMap::{0}::get_in_list] *)
-let rec hash_map_get_in_list_fwd
-  (t : Type0) (key : usize) (ls : list_t t) :
-  Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls))
+let rec hash_map_get_in_list_loop_fwd
+  (t : Type0) (i : usize) (ls : list_t t) :
+  Tot (result t) (decreases (hash_map_get_in_list_decreases t i ls))
   =
   begin match ls with
-  | ListCons ckey cvalue ls0 ->
-    if ckey = key then Return cvalue else hash_map_get_in_list_fwd t key ls0
+  | ListCons ckey cvalue tl ->
+    if ckey = i then Return cvalue else hash_map_get_in_list_loop_fwd t i tl
   | ListNil -> Fail Failure
   end
 
+(** [hashmap::HashMap::{0}::get_in_list] *)
+let hash_map_get_in_list_fwd
+  (t : Type0) (key : usize) (ls : list_t t) : result t =
+  hash_map_get_in_list_loop_fwd t key ls
+
 (** [hashmap::HashMap::{0}::get] *)
 let hash_map_get_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result t =
@@ -337,36 +381,46 @@ let hash_map_get_fwd
   end
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
-let rec hash_map_get_mut_in_list_fwd
-  (t : Type0) (key : usize) (ls : list_t t) :
-  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
+let rec hash_map_get_mut_in_list_loop_fwd
+  (t : Type0) (i : usize) (ls : list_t t) :
+  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t i ls))
   =
   begin match ls with
-  | ListCons ckey cvalue ls0 ->
-    if ckey = key
+  | ListCons ckey cvalue tl ->
+    if ckey = i
     then Return cvalue
-    else hash_map_get_mut_in_list_fwd t key ls0
+    else hash_map_get_mut_in_list_loop_fwd t i tl
   | ListNil -> Fail Failure
   end
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
-let rec hash_map_get_mut_in_list_back
-  (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
+let hash_map_get_mut_in_list_fwd
+  (t : Type0) (ls : list_t t) (key : usize) : result t =
+  hash_map_get_mut_in_list_loop_fwd t key ls
+
+(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+let rec hash_map_get_mut_in_list_loop_back
+  (t : Type0) (i : usize) (ls : list_t t) (ret : t) :
   Tot (result (list_t t))
-  (decreases (hash_map_get_mut_in_list_decreases t key ls))
+  (decreases (hash_map_get_mut_in_list_decreases t i ls))
   =
   begin match ls with
-  | ListCons ckey cvalue ls0 ->
-    if ckey = key
-    then Return (ListCons ckey ret ls0)
+  | ListCons ckey cvalue tl ->
+    if ckey = i
+    then Return (ListCons ckey ret tl)
     else
-      begin match hash_map_get_mut_in_list_back t key ls0 ret with
+      begin match hash_map_get_mut_in_list_loop_back t i tl ret with
       | Fail e -> Fail e
-      | Return ls1 -> Return (ListCons ckey cvalue ls1)
+      | Return l -> Return (ListCons ckey cvalue l)
       end
   | ListNil -> Fail Failure
   end
 
+(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+let hash_map_get_mut_in_list_back
+  (t : Type0) (ls : list_t t) (key : usize) (ret : t) : result (list_t t) =
+  hash_map_get_mut_in_list_loop_back t key ls ret
+
 (** [hashmap::HashMap::{0}::get_mut] *)
 let hash_map_get_mut_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result t =
@@ -380,7 +434,7 @@ let hash_map_get_mut_fwd
       begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
         with
       | Fail e -> Fail e
-      | Return l -> hash_map_get_mut_in_list_fwd t key l
+      | Return l -> hash_map_get_mut_in_list_fwd t l key
       end
     end
   end
@@ -401,7 +455,7 @@ let hash_map_get_mut_back
         with
       | Fail e -> Fail e
       | Return l ->
-        begin match hash_map_get_mut_in_list_back t key l ret with
+        begin match hash_map_get_mut_in_list_back t l key ret with
         | Fail e -> Fail e
         | Return l0 ->
           begin match
@@ -417,47 +471,57 @@ let hash_map_get_mut_back
   end
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
-let rec hash_map_remove_from_list_fwd
-  (t : Type0) (key : usize) (ls : list_t t) :
+let rec hash_map_remove_from_list_loop_fwd
+  (t : Type0) (i : usize) (ls : list_t t) :
   Tot (result (option t))
-  (decreases (hash_map_remove_from_list_decreases t key ls))
+  (decreases (hash_map_remove_from_list_decreases t i ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
-    if ckey = key
+    if ckey = i
     then
       let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
       begin match mv_ls with
-      | ListCons i cvalue tl0 -> Return (Some cvalue)
+      | ListCons i0 cvalue tl0 -> Return (Some cvalue)
       | ListNil -> Fail Failure
       end
-    else hash_map_remove_from_list_fwd t key tl
+    else hash_map_remove_from_list_loop_fwd t i tl
   | ListNil -> Return None
   end
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
-let rec hash_map_remove_from_list_back
-  (t : Type0) (key : usize) (ls : list_t t) :
+let hash_map_remove_from_list_fwd
+  (t : Type0) (key : usize) (ls : list_t t) : result (option t) =
+  hash_map_remove_from_list_loop_fwd t key ls
+
+(** [hashmap::HashMap::{0}::remove_from_list] *)
+let rec hash_map_remove_from_list_loop_back
+  (t : Type0) (i : usize) (ls : list_t t) :
   Tot (result (list_t t))
-  (decreases (hash_map_remove_from_list_decreases t key ls))
+  (decreases (hash_map_remove_from_list_decreases t i ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
-    if ckey = key
+    if ckey = i
     then
       let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
       begin match mv_ls with
-      | ListCons i cvalue tl0 -> Return tl0
+      | ListCons i0 cvalue tl0 -> Return tl0
       | ListNil -> Fail Failure
       end
     else
-      begin match hash_map_remove_from_list_back t key tl with
+      begin match hash_map_remove_from_list_loop_back t i tl with
       | Fail e -> Fail e
-      | Return tl0 -> Return (ListCons ckey x tl0)
+      | Return l -> Return (ListCons ckey x l)
       end
   | ListNil -> Return ListNil
   end
 
+(** [hashmap::HashMap::{0}::remove_from_list] *)
+let hash_map_remove_from_list_back
+  (t : Type0) (key : usize) (ls : list_t t) : result (list_t t) =
+  hash_map_remove_from_list_loop_back t key ls
+
 (** [hashmap::HashMap::{0}::remove] *)
 let hash_map_remove_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 9d1a6469..724ca741 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -620,11 +620,11 @@ let hash_map_new_fwd_lem t = hash_map_new_fwd_lem_aux t
 (*** clear_slots *)
 /// [clear_slots] doesn't fail and simply clears the slots starting at index i
 #push-options "--fuel 1"
-let rec hash_map_clear_slots_fwd_back_lem
+let rec hash_map_clear_slots_loop_fwd_back_lem
   (t : Type0) (slots : vec (list_t t)) (i : usize) :
   Lemma
   (ensures (
-    match hash_map_clear_slots_fwd_back t slots i with
+    match hash_map_clear_slots_loop_fwd_back t slots i with
     | Fail _ -> False
     | Return slots' ->
       // The length is preserved
@@ -645,8 +645,8 @@ let rec hash_map_clear_slots_fwd_back_lem
       begin match usize_add i 1 with
       | Fail _ -> ()
       | Return i1 ->
-        hash_map_clear_slots_fwd_back_lem t v i1;
-        begin match hash_map_clear_slots_fwd_back t v i1 with
+        hash_map_clear_slots_loop_fwd_back_lem t v i1;
+        begin match hash_map_clear_slots_loop_fwd_back t v i1 with
         | Fail _ -> ()
         | Return slots1 ->
           assert(length slots1 == length slots);
@@ -683,8 +683,8 @@ let hash_map_clear_fwd_back_lem_aux #t self =
   let p = self.hash_map_max_load_factor in
   let i = self.hash_map_max_load in
   let v = self.hash_map_slots in
-  hash_map_clear_slots_fwd_back_lem t v 0;
-  begin match hash_map_clear_slots_fwd_back t v 0 with
+  hash_map_clear_slots_loop_fwd_back_lem t v 0;
+  begin match hash_map_clear_slots_loop_fwd_back t v 0 with
   | Fail _ -> ()
   | Return slots1 ->
     slots_t_al_v_all_nil_is_empty_lem slots1;
@@ -2703,17 +2703,17 @@ let hash_map_get_fwd_lem #t self key = hash_map_get_fwd_lem_aux #t self key
 
 (**** get_mut_in_list'fwd *)
 
-val hash_map_get_mut_in_list_fwd_lem
+val hash_map_get_mut_in_list_loop_fwd_lem
   (#t : Type0) (key : usize) (ls : list_t t) :
   Lemma
   (ensures (
-    match hash_map_get_mut_in_list_fwd t key ls, slot_t_find_s key ls with
+    match hash_map_get_mut_in_list_loop_fwd t key ls, slot_t_find_s key ls with
     | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
 #push-options "--fuel 1"
-let rec hash_map_get_mut_in_list_fwd_lem #t key ls =
+let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls =
   begin match ls with
   | ListCons ckey cvalue ls0 ->
     let b = ckey = key in
@@ -2721,8 +2721,8 @@ let rec hash_map_get_mut_in_list_fwd_lem #t key ls =
     then ()
     else
       begin
-      hash_map_get_mut_in_list_fwd_lem key ls0;
-      match hash_map_get_mut_in_list_fwd t key ls0 with
+      hash_map_get_mut_in_list_loop_fwd_lem key ls0;
+      match hash_map_get_mut_in_list_loop_fwd t key ls0 with
       | Fail _ -> ()
       | Return x -> ()
       end
@@ -2754,8 +2754,8 @@ let hash_map_get_mut_fwd_lem_aux #t self key =
       | Fail _ -> ()
       | Return l ->
         begin
-        hash_map_get_mut_in_list_fwd_lem key l;
-        match hash_map_get_mut_in_list_fwd t key l with
+        hash_map_get_mut_in_list_loop_fwd_lem key l;
+        match hash_map_get_mut_in_list_loop_fwd t key l with
         | Fail _ -> ()
         | Return x -> ()
         end
@@ -2770,18 +2770,18 @@ let hash_map_get_mut_fwd_lem #t self key =
 
 (**** get_mut_in_list'back *)
 
-val hash_map_get_mut_in_list_back_lem
+val hash_map_get_mut_in_list_loop_back_lem
   (#t : Type0) (key : usize) (ls : list_t t) (ret : t) :
   Lemma
   (requires (Some? (slot_t_find_s key ls)))
   (ensures (
-    match hash_map_get_mut_in_list_back t key ls ret with
+    match hash_map_get_mut_in_list_loop_back t key ls ret with
     | Fail _ -> False
     | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret)
     | _ -> False))
 
 #push-options "--fuel 1"
-let rec hash_map_get_mut_in_list_back_lem #t key ls ret =
+let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret =
   begin match ls with
   | ListCons ckey cvalue ls0 ->
     let b = ckey = key in
@@ -2789,8 +2789,8 @@ let rec hash_map_get_mut_in_list_back_lem #t key ls ret =
     then let ls1 = ListCons ckey ret ls0 in ()
     else
       begin
-      hash_map_get_mut_in_list_back_lem key ls0 ret;
-      match hash_map_get_mut_in_list_back t key ls0 ret with
+      hash_map_get_mut_in_list_loop_back_lem key ls0 ret;
+      match hash_map_get_mut_in_list_loop_back t key ls0 ret with
       | Fail _ -> ()
       | Return l -> let ls1 = ListCons ckey cvalue l in ()
       end
@@ -2828,8 +2828,8 @@ let hash_map_get_mut_back_lem_refin #t self key ret =
       | Fail _ -> ()
       | Return l ->
         begin
-        hash_map_get_mut_in_list_back_lem key l ret;
-        match hash_map_get_mut_in_list_back t key l ret with
+        hash_map_get_mut_in_list_loop_back_lem key l ret;
+        match hash_map_get_mut_in_list_loop_back t key l ret with
         | Fail _ -> ()
         | Return l0 ->
           begin match vec_index_mut_back (list_t t) v hash_mod l0 with
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index 55685114..b3081cd6 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -9,13 +9,13 @@ open HashmapMain.Types
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
 unfold
 let hashmap_hash_map_allocate_slots_decreases (t : Type0)
-  (slots : vec (hashmap_list_t t)) (n : usize) : nat =
+  (v : vec (hashmap_list_t t)) (n : usize) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots]: decreases clause *)
 unfold
 let hashmap_hash_map_clear_slots_decreases (t : Type0)
-  (slots : vec (hashmap_list_t t)) (i : usize) : nat =
+  (v : vec (hashmap_list_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
@@ -31,37 +31,36 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
 unfold
 let hashmap_hash_map_move_elements_from_list_decreases (t : Type0)
-  (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat =
+  (hm : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: decreases clause *)
 unfold
 let hashmap_hash_map_move_elements_decreases (t : Type0)
-  (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) (i : usize)
-  : nat =
+  (hm : hashmap_hash_map_t t) (v : vec (hashmap_list_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (key : usize)
+let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (i : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize)
+let hashmap_hash_map_get_in_list_decreases (t : Type0) (i : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
+let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (i : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
 unfold
-let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : usize)
+let hashmap_hash_map_remove_from_list_decreases (t : Type0) (i : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index c4f2b039..3da56f41 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -12,22 +12,29 @@ include HashmapMain.Clauses
 let hashmap_hash_key_fwd (k : usize) : result usize = Return k
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
-let rec hashmap_hash_map_allocate_slots_fwd
-  (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
+let rec hashmap_hash_map_allocate_slots_loop_fwd
+  (t : Type0) (v : vec (hashmap_list_t t)) (n : usize) :
   Tot (result (vec (hashmap_list_t t)))
-  (decreases (hashmap_hash_map_allocate_slots_decreases t slots n))
+  (decreases (hashmap_hash_map_allocate_slots_decreases t v n))
   =
-  if n = 0
-  then Return slots
-  else
-    begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
+  if n > 0
+  then
+    begin match vec_push_back (hashmap_list_t t) v HashmapListNil with
     | Fail e -> Fail e
-    | Return slots0 ->
+    | Return slots ->
       begin match usize_sub n 1 with
       | Fail e -> Fail e
-      | Return i -> hashmap_hash_map_allocate_slots_fwd t slots0 i
+      | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots n0
       end
     end
+  else Return v
+
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+let hashmap_hash_map_allocate_slots_fwd
+  (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
+  result (vec (hashmap_list_t t))
+  =
+  hashmap_hash_map_allocate_slots_loop_fwd t slots n
 
 (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
 let hashmap_hash_map_new_with_capacity_fwd
@@ -56,30 +63,36 @@ let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
   hashmap_hash_map_new_with_capacity_fwd t 32 4 5
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-let rec hashmap_hash_map_clear_slots_fwd_back
-  (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) :
+let rec hashmap_hash_map_clear_slots_loop_fwd_back
+  (t : Type0) (v : vec (hashmap_list_t t)) (i : usize) :
   Tot (result (vec (hashmap_list_t t)))
-  (decreases (hashmap_hash_map_clear_slots_decreases t slots i))
+  (decreases (hashmap_hash_map_clear_slots_decreases t v i))
   =
-  let i0 = vec_len (hashmap_list_t t) slots in
+  let i0 = vec_len (hashmap_list_t t) v in
   if i < i0
   then
-    begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
-      with
+    begin match usize_add i 1 with
     | Fail e -> Fail e
-    | Return slots0 ->
-      begin match usize_add i 1 with
+    | Return i1 ->
+      begin match vec_index_mut_back (hashmap_list_t t) v i HashmapListNil with
       | Fail e -> Fail e
-      | Return i1 -> hashmap_hash_map_clear_slots_fwd_back t slots0 i1
+      | Return slots -> hashmap_hash_map_clear_slots_loop_fwd_back t slots i1
       end
     end
-  else Return slots
+  else Return v
+
+(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
+let hashmap_hash_map_clear_slots_fwd_back
+  (t : Type0) (slots : vec (hashmap_list_t t)) :
+  result (vec (hashmap_list_t t))
+  =
+  hashmap_hash_map_clear_slots_loop_fwd_back t slots 0
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
 let hashmap_hash_map_clear_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
   begin match
-    hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots 0 with
+    hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots with
   | Fail e -> Fail e
   | Return v ->
     Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
@@ -92,38 +105,50 @@ let hashmap_hash_map_len_fwd
   Return self.hashmap_hash_map_num_entries
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
-let rec hashmap_hash_map_insert_in_list_fwd
+let rec hashmap_hash_map_insert_in_list_loop_fwd
   (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
   Tot (result bool)
   (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls))
   =
   begin match ls with
-  | HashmapListCons ckey cvalue ls0 ->
+  | HashmapListCons ckey cvalue tl ->
     if ckey = key
     then Return false
-    else hashmap_hash_map_insert_in_list_fwd t key value ls0
+    else hashmap_hash_map_insert_in_list_loop_fwd t key value tl
   | HashmapListNil -> Return true
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
-let rec hashmap_hash_map_insert_in_list_back
+let hashmap_hash_map_insert_in_list_fwd
+  (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : result bool =
+  hashmap_hash_map_insert_in_list_loop_fwd t key value ls
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+let rec hashmap_hash_map_insert_in_list_loop_back
   (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
   Tot (result (hashmap_list_t t))
   (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls))
   =
   begin match ls with
-  | HashmapListCons ckey cvalue ls0 ->
+  | HashmapListCons ckey cvalue tl ->
     if ckey = key
-    then Return (HashmapListCons ckey value ls0)
+    then Return (HashmapListCons ckey value tl)
     else
-      begin match hashmap_hash_map_insert_in_list_back t key value ls0 with
+      begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with
       | Fail e -> Fail e
-      | Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
+      | Return l -> Return (HashmapListCons ckey cvalue l)
       end
   | HashmapListNil ->
     let l = HashmapListNil in Return (HashmapListCons key value l)
   end
 
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+let hashmap_hash_map_insert_in_list_back
+  (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
+  result (hashmap_list_t t)
+  =
+  hashmap_hash_map_insert_in_list_loop_back t key value ls
+
 (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
 let hashmap_hash_map_insert_no_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) :
@@ -188,52 +213,67 @@ let core_num_u32_max_body : result u32 = Return 4294967295
 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
-let rec hashmap_hash_map_move_elements_from_list_fwd_back
-  (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
+let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
+  (t : Type0) (hm : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
   Tot (result (hashmap_hash_map_t t))
-  (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls))
+  (decreases (hashmap_hash_map_move_elements_from_list_decreases t hm ls))
   =
   begin match ls with
   | HashmapListCons k v tl ->
-    begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
+    begin match hashmap_hash_map_insert_no_resize_fwd_back t hm k v with
     | Fail e -> Fail e
-    | Return ntable0 ->
-      hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl
+    | Return ntable ->
+      hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable tl
     end
-  | HashmapListNil -> Return ntable
+  | HashmapListNil -> Return hm
   end
 
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+let hashmap_hash_map_move_elements_from_list_fwd_back
+  (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
+  result (hashmap_hash_map_t t)
+  =
+  hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable ls
+
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
-let rec hashmap_hash_map_move_elements_fwd_back
-  (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
+let rec hashmap_hash_map_move_elements_loop_fwd_back
+  (t : Type0) (hm : hashmap_hash_map_t t) (v : vec (hashmap_list_t t))
   (i : usize) :
   Tot (result ((hashmap_hash_map_t t) & (vec (hashmap_list_t t))))
-  (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i))
+  (decreases (hashmap_hash_map_move_elements_decreases t hm v i))
   =
-  let i0 = vec_len (hashmap_list_t t) slots in
+  let i0 = vec_len (hashmap_list_t t) v in
   if i < i0
   then
-    begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
+    begin match vec_index_mut_fwd (hashmap_list_t t) v i with
     | Fail e -> Fail e
     | Return l ->
       let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
-      begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls
+      begin match hashmap_hash_map_move_elements_from_list_fwd_back t hm ls
         with
       | Fail e -> Fail e
-      | Return ntable0 ->
-        let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
-        begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
+      | Return ntable ->
+        begin match usize_add i 1 with
         | Fail e -> Fail e
-        | Return slots0 ->
-          begin match usize_add i 1 with
+        | Return i1 ->
+          let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
+          begin match vec_index_mut_back (hashmap_list_t t) v i l0 with
           | Fail e -> Fail e
-          | Return i1 ->
-            hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1
+          | Return slots ->
+            hashmap_hash_map_move_elements_loop_fwd_back t ntable slots i1
           end
         end
       end
     end
-  else Return (ntable, slots)
+  else Return (hm, v)
+
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+let hashmap_hash_map_move_elements_fwd_back
+  (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
+  (i : usize) :
+  result ((hashmap_hash_map_t t) & (vec (hashmap_list_t t)))
+  =
+  hashmap_hash_map_move_elements_loop_fwd_back t ntable slots i
 
 (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
 let hashmap_hash_map_try_resize_fwd_back
@@ -293,19 +333,24 @@ let hashmap_hash_map_insert_fwd_back
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
-let rec hashmap_hash_map_contains_key_in_list_fwd
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+let rec hashmap_hash_map_contains_key_in_list_loop_fwd
+  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
   Tot (result bool)
-  (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls))
+  (decreases (hashmap_hash_map_contains_key_in_list_decreases t i ls))
   =
   begin match ls with
-  | HashmapListCons ckey x ls0 ->
-    if ckey = key
+  | HashmapListCons ckey x tl ->
+    if ckey = i
     then Return true
-    else hashmap_hash_map_contains_key_in_list_fwd t key ls0
+    else hashmap_hash_map_contains_key_in_list_loop_fwd t i tl
   | HashmapListNil -> Return false
   end
 
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+let hashmap_hash_map_contains_key_in_list_fwd
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) : result bool =
+  hashmap_hash_map_contains_key_in_list_loop_fwd t key ls
+
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
 let hashmap_hash_map_contains_key_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool =
@@ -326,18 +371,23 @@ let hashmap_hash_map_contains_key_fwd
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
-let rec hashmap_hash_map_get_in_list_fwd
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
-  Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t key ls))
+let rec hashmap_hash_map_get_in_list_loop_fwd
+  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
+  Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t i ls))
   =
   begin match ls with
-  | HashmapListCons ckey cvalue ls0 ->
-    if ckey = key
+  | HashmapListCons ckey cvalue tl ->
+    if ckey = i
     then Return cvalue
-    else hashmap_hash_map_get_in_list_fwd t key ls0
+    else hashmap_hash_map_get_in_list_loop_fwd t i tl
   | HashmapListNil -> Fail Failure
   end
 
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+let hashmap_hash_map_get_in_list_fwd
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) : result t =
+  hashmap_hash_map_get_in_list_loop_fwd t key ls
+
 (** [hashmap_main::hashmap::HashMap::{0}::get] *)
 let hashmap_hash_map_get_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
@@ -358,37 +408,49 @@ let hashmap_hash_map_get_fwd
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
-let rec hashmap_hash_map_get_mut_in_list_fwd
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+let rec hashmap_hash_map_get_mut_in_list_loop_fwd
+  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
   Tot (result t)
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls))
   =
   begin match ls with
-  | HashmapListCons ckey cvalue ls0 ->
-    if ckey = key
+  | HashmapListCons ckey cvalue tl ->
+    if ckey = i
     then Return cvalue
-    else hashmap_hash_map_get_mut_in_list_fwd t key ls0
+    else hashmap_hash_map_get_mut_in_list_loop_fwd t i tl
   | HashmapListNil -> Fail Failure
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
-let rec hashmap_hash_map_get_mut_in_list_back
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) :
+let hashmap_hash_map_get_mut_in_list_fwd
+  (t : Type0) (ls : hashmap_list_t t) (key : usize) : result t =
+  hashmap_hash_map_get_mut_in_list_loop_fwd t key ls
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+let rec hashmap_hash_map_get_mut_in_list_loop_back
+  (t : Type0) (i : usize) (ls : hashmap_list_t t) (ret : t) :
   Tot (result (hashmap_list_t t))
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls))
   =
   begin match ls with
-  | HashmapListCons ckey cvalue ls0 ->
-    if ckey = key
-    then Return (HashmapListCons ckey ret ls0)
+  | HashmapListCons ckey cvalue tl ->
+    if ckey = i
+    then Return (HashmapListCons ckey ret tl)
     else
-      begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret with
+      begin match hashmap_hash_map_get_mut_in_list_loop_back t i tl ret with
       | Fail e -> Fail e
-      | Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
+      | Return l -> Return (HashmapListCons ckey cvalue l)
       end
   | HashmapListNil -> Fail Failure
   end
 
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+let hashmap_hash_map_get_mut_in_list_back
+  (t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
+  result (hashmap_list_t t)
+  =
+  hashmap_hash_map_get_mut_in_list_loop_back t key ls ret
+
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
 let hashmap_hash_map_get_mut_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
@@ -403,7 +465,7 @@ let hashmap_hash_map_get_mut_fwd
         vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
           hash_mod with
       | Fail e -> Fail e
-      | Return l -> hashmap_hash_map_get_mut_in_list_fwd t key l
+      | Return l -> hashmap_hash_map_get_mut_in_list_fwd t l key
       end
     end
   end
@@ -425,7 +487,7 @@ let hashmap_hash_map_get_mut_back
           hash_mod with
       | Fail e -> Fail e
       | Return l ->
-        begin match hashmap_hash_map_get_mut_in_list_back t key l ret with
+        begin match hashmap_hash_map_get_mut_in_list_back t l key ret with
         | Fail e -> Fail e
         | Return l0 ->
           begin match
@@ -443,51 +505,63 @@ let hashmap_hash_map_get_mut_back
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
-let rec hashmap_hash_map_remove_from_list_fwd
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+let rec hashmap_hash_map_remove_from_list_loop_fwd
+  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
   Tot (result (option t))
-  (decreases (hashmap_hash_map_remove_from_list_decreases t key ls))
+  (decreases (hashmap_hash_map_remove_from_list_decreases t i ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
-    if ckey = key
+    if ckey = i
     then
       let mv_ls =
         mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
           HashmapListNil in
       begin match mv_ls with
-      | HashmapListCons i cvalue tl0 -> Return (Some cvalue)
+      | HashmapListCons i0 cvalue tl0 -> Return (Some cvalue)
       | HashmapListNil -> Fail Failure
       end
-    else hashmap_hash_map_remove_from_list_fwd t key tl
+    else hashmap_hash_map_remove_from_list_loop_fwd t i tl
   | HashmapListNil -> Return None
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
-let rec hashmap_hash_map_remove_from_list_back
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+let hashmap_hash_map_remove_from_list_fwd
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) : result (option t) =
+  hashmap_hash_map_remove_from_list_loop_fwd t key ls
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+let rec hashmap_hash_map_remove_from_list_loop_back
+  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
   Tot (result (hashmap_list_t t))
-  (decreases (hashmap_hash_map_remove_from_list_decreases t key ls))
+  (decreases (hashmap_hash_map_remove_from_list_decreases t i ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
-    if ckey = key
+    if ckey = i
     then
       let mv_ls =
         mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
           HashmapListNil in
       begin match mv_ls with
-      | HashmapListCons i cvalue tl0 -> Return tl0
+      | HashmapListCons i0 cvalue tl0 -> Return tl0
       | HashmapListNil -> Fail Failure
       end
     else
-      begin match hashmap_hash_map_remove_from_list_back t key tl with
+      begin match hashmap_hash_map_remove_from_list_loop_back t i tl with
       | Fail e -> Fail e
-      | Return tl0 -> Return (HashmapListCons ckey x tl0)
+      | Return l -> Return (HashmapListCons ckey x l)
       end
   | HashmapListNil -> Return HashmapListNil
   end
 
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+let hashmap_hash_map_remove_from_list_back
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+  result (hashmap_list_t t)
+  =
+  hashmap_hash_map_remove_from_list_loop_back t key ls
+
 (** [hashmap_main::hashmap::HashMap::{0}::remove] *)
 let hashmap_hash_map_remove_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) =