Improve the heuristic to find pretty names for the variables in the loops

14 files changed, 451 insertions, 382 deletions

diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 532271c3..2c8d5081 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -521,7 +521,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
       let meta_s = meta_to_string fmt meta in
       let e = texpression_to_string fmt inside indent indent_incr e in
       match meta with
-      | Assignment _ | Tag _ ->
+      | Assignment _ | SymbolicAssignment _ | Tag _ ->
           let e = meta_s ^ "\n" ^ indent ^ e in
           if inside then "(" ^ e ^ ")" else e
       | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
@@ -665,6 +665,10 @@ and meta_to_string (fmt : ast_formatter) (meta : meta) : string =
         "@assign(" ^ mplace_to_string fmt lp ^ " := "
         ^ texpression_to_string fmt false "" "" rv
         ^ rp ^ ")"
+    | SymbolicAssignment (var_id, rv) ->
+        "@symb_assign(" ^ VarId.to_string var_id ^ " := "
+        ^ texpression_to_string fmt false "" "" rv
+        ^ ")"
     | MPlace mp -> "@mplace=" ^ mplace_to_string fmt mp
     | Tag msg -> "@tag \"" ^ msg ^ "\""
   in
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 118aec50..fe30a650 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -358,7 +358,7 @@ type qualif_id =
  *)
 type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]
 
-type var_id = VarId.id [@@deriving show]
+type var_id = VarId.id [@@deriving show, ord]
 
 (** Ancestor for {!iter_expression} visitor *)
 class ['self] iter_expression_base =
@@ -513,14 +513,21 @@ and texpression = { e : expression; ty : ty }
  *)
 and mvalue = (texpression[@opaque])
 
+(** Meta-information stored in the AST *)
 and meta =
   | Assignment of mplace * mvalue * mplace option
-      (** Meta-information stored in the AST.
+      (** Information about an assignment which occured in LLBC.
+          We use this to guide the heuristics which derive pretty names.
 
           The first mplace stores the destination.
           The mvalue stores the value which is put in the destination
           The second (optional) mplace stores the origin.
         *)
+  | SymbolicAssignment of (var_id[@opaque]) * mvalue
+      (** Informationg linking a variable (from the pure AST) to an
+          expression.
+          We use this to guide the heuristics which derive pretty names.
+        *)
   | MPlace of mplace  (** Meta-information about the origin of a value *)
   | Tag of string  (** A tag - typically used for debugging *)
 [@@deriving
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b9441397..09cc2533 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -290,6 +290,17 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     (* Add the constraint *)
     match (unmeta rv).e with Var vid -> add_constraint mp vid ctx | _ -> ctx
   in
+  let add_pure_var_value_constraint (var_id : VarId.id) (rv : texpression)
+      (ctx : pn_ctx) : pn_ctx =
+    (* Add the constraint *)
+    match (unmeta rv).e with
+    | Var vid -> (
+        (* Try to find a name for the vid *)
+        match VarId.Map.find_opt vid ctx.pure_vars with
+        | None -> ctx
+        | Some name -> add_pure_var_constraint var_id name ctx)
+    | _ -> ctx
+  in
   (* Specific case of constraint on left values *)
   let add_left_constraint (lv : typed_pattern) (ctx : pn_ctx) : pn_ctx =
     let obj =
@@ -484,6 +495,8 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
             | _ -> ctx
           in
           ctx
+      | SymbolicAssignment (var_id, rvalue) ->
+          add_pure_var_value_constraint var_id rvalue ctx
       | MPlace mp -> add_right_constraint mp e ctx
       | Tag _ -> ctx
     in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index a60bcd78..e86d2a78 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -57,6 +57,8 @@ let compute_primitive_value_ty (cv : primitive_value) : ty =
   | Char _ -> Char
   | String _ -> Str
 
+let var_get_id (v : var) : VarId.id = v.id
+
 let mk_typed_pattern_from_primitive_value (cv : primitive_value) : typed_pattern
     =
   let ty = compute_primitive_value_ty cv in
@@ -73,6 +75,10 @@ let mk_tag (msg : string) (next_e : texpression) : texpression =
   let ty = next_e.ty in
   { e; ty }
 
+let mk_mplace (var_id : E.VarId.id) (name : string option)
+    (projection : mprojection) : mplace =
+  { var_id; name; projection }
+
 (** Type substitution *)
 let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty =
   let obj =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 49b696b2..ab9e40df 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -103,6 +103,7 @@ type call_info = {
  *)
 type loop_info = {
   loop_id : LoopId.id;
+  input_vars : var list;
   input_svl : V.symbolic_value list;
   type_args : ty list;
   forward_inputs : texpression list option;
@@ -149,7 +150,7 @@ type bs_ctx = {
   fuel0 : VarId.id;
       (** The original fuel taken as input by the function (if we use fuel) *)
   fuel : VarId.id;
-  (* The fuel to use for the recursive calls (if we use fuel) *)
+      (** The fuel to use for the recursive calls (if we use fuel) *)
   forward_inputs : var list;
       (** The input parameters for the forward function corresponding to the
           translated Rust inputs (no fuel, no state).
@@ -169,6 +170,8 @@ type bs_ctx = {
           [None] if we are not inside a loop, [Some] otherwise (and whatever
           the kind of function we are translating: it will be [Some] even
           though we are synthesizing a forward function).
+
+          TODO: move to {!loop_info}
        *)
   calls : call_info V.FunCallId.Map.t;
       (** The function calls we encountered so far *)
@@ -2254,6 +2257,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       let args =
         List.map (typed_value_to_texpression ctx ectx) loop_input_values
       in
+      let org_args = args in
 
       (* Lookup the effect info for the loop function *)
       let fid = A.Regular ctx.fun_decl.A.def_id in
@@ -2316,7 +2320,31 @@ and translate_forward_end (ectx : C.eval_ctx)
       in
 
       (* Create the let expression with the loop call *)
-      mk_let effect_info.can_fail out_pat loop_call next_e
+      let e = mk_let effect_info.can_fail out_pat loop_call next_e in
+
+      (* Add meta-information linking the loop input parameters and the
+         loop input values - we use this to derive proper names.
+
+         There is something important here: as we group the end of the function
+         and the loop body in a {!Loop} node, when exploring the function
+         and applying micro passes, we introduce the variables specific to
+         the loop body before exploring both the loop body and the end of
+         the function. It means it is ok to reference some variables which might
+         actually be defined, in the end, in a different branch.
+
+         We then remove all the meta information from the body *before* calling
+         {!PureMicroPasses.decompose_loops}.
+      *)
+      let e =
+        let var_values = List.combine loop_info.input_vars org_args in
+        List.fold_right
+          (fun (var, arg) e ->
+            mk_meta (SymbolicAssignment (var_get_id var, arg)) e)
+          var_values e
+      in
+
+      (* Return *)
+      e
 
 and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in
@@ -2416,6 +2444,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
     let loop_info =
       {
         loop_id;
+        input_vars = inputs;
         input_svl = loop.input_svalues;
         type_args;
         forward_inputs = None;
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 5ec021d1..1cbff379 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -13,7 +13,7 @@ Definition hash_key_fwd (k : usize) : result usize := Return k.
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 Fixpoint hash_map_allocate_slots_loop_fwd
-  (T : Type) (n : nat) (v : vec (List_t T)) (n0 : usize) :
+  (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
   result (vec (List_t T))
   :=
   match n with
@@ -21,10 +21,10 @@ Fixpoint hash_map_allocate_slots_loop_fwd
   | S n1 =>
     if n0 s> 0%usize
     then (
-      slots <- vec_push_back (List_t T) v ListNil;
+      slots0 <- vec_push_back (List_t T) slots ListNil;
       n2 <- usize_sub n0 1%usize;
-      hash_map_allocate_slots_loop_fwd T n1 slots n2)
-    else Return v
+      hash_map_allocate_slots_loop_fwd T n1 slots0 n2)
+    else Return slots
   end
 .
 
@@ -57,19 +57,19 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
 Fixpoint hash_map_clear_slots_loop_fwd_back
-  (T : Type) (n : nat) (v : vec (List_t T)) (i : usize) :
+  (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
   result (vec (List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (List_t T) v in
+    let i0 := vec_len (List_t T) slots in
     if i s< i0
     then (
       i1 <- usize_add i 1%usize;
-      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
+      slots0 <- vec_index_mut_back (List_t T) slots i ListNil;
+      hash_map_clear_slots_loop_fwd_back T n0 slots0 i1)
+    else Return slots
   end
 .
 
@@ -176,7 +176,7 @@ 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_loop_fwd_back
-  (T : Type) (n : nat) (hm : Hash_map_t T) (ls : List_t T) :
+  (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
   result (Hash_map_t T)
   :=
   match n with
@@ -184,9 +184,9 @@ Fixpoint hash_map_move_elements_from_list_loop_fwd_back
   | S n0 =>
     match ls with
     | ListCons k v tl =>
-      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
+      ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v;
+      hash_map_move_elements_from_list_loop_fwd_back T n0 ntable0 tl
+    | ListNil => Return ntable
     end
   end
 .
@@ -201,23 +201,24 @@ Definition hash_map_move_elements_from_list_fwd_back
 
 (** [hashmap::HashMap::{0}::move_elements] *)
 Fixpoint hash_map_move_elements_loop_fwd_back
-  (T : Type) (n : nat) (hm : Hash_map_t T) (v : vec (List_t T)) (i : usize) :
+  (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
+  (i : usize) :
   result ((Hash_map_t T) * (vec (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (List_t T) v in
+    let i0 := vec_len (List_t T) slots in
     if i s< i0
     then (
-      l <- vec_index_mut_fwd (List_t T) v i;
+      l <- vec_index_mut_fwd (List_t T) slots i;
       let ls := mem_replace_fwd (List_t T) l ListNil in
-      ntable <- hash_map_move_elements_from_list_fwd_back T n0 hm ls;
+      ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
       i1 <- usize_add i 1%usize;
       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)
+      slots0 <- vec_index_mut_back (List_t T) slots i l0;
+      hash_map_move_elements_loop_fwd_back T n0 ntable0 slots0 i1)
+    else Return (ntable, slots)
   end
 .
 
@@ -267,15 +268,15 @@ Definition hash_map_insert_fwd_back
 
 (** [hashmap::HashMap::{0}::contains_key_in_list] *)
 Fixpoint hash_map_contains_key_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result bool :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then Return true
-      else hash_map_contains_key_in_list_loop_fwd T n0 i tl
+      else hash_map_contains_key_in_list_loop_fwd T n0 key tl
     | ListNil => Return false
     end
   end
@@ -299,15 +300,15 @@ Definition hash_map_contains_key_fwd
 
 (** [hashmap::HashMap::{0}::get_in_list] *)
 Fixpoint hash_map_get_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return cvalue
-      else hash_map_get_in_list_loop_fwd T n0 i tl
+      else hash_map_get_in_list_loop_fwd T n0 key tl
     | ListNil => Fail_ Failure
     end
   end
@@ -331,15 +332,15 @@ Definition hash_map_get_fwd
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hash_map_get_mut_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return cvalue
-      else hash_map_get_mut_in_list_loop_fwd T n0 i tl
+      else hash_map_get_mut_in_list_loop_fwd T n0 key tl
     | ListNil => Fail_ Failure
     end
   end
@@ -353,7 +354,7 @@ Definition hash_map_get_mut_in_list_fwd
 
 (** [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) :
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) :
   result (List_t T)
   :=
   match n with
@@ -361,10 +362,10 @@ Fixpoint hash_map_get_mut_in_list_loop_back
   | S n0 =>
     match ls with
     | ListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return (ListCons ckey ret tl)
       else (
-        l <- hash_map_get_mut_in_list_loop_back T n0 i tl ret;
+        l <- hash_map_get_mut_in_list_loop_back T n0 key tl ret;
         Return (ListCons ckey cvalue l))
     | ListNil => Fail_ Failure
     end
@@ -406,20 +407,20 @@ Definition hash_map_get_mut_back
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 Fixpoint hash_map_remove_from_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (option T) :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then
         let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
         match mv_ls with
-        | ListCons i0 cvalue tl0 => Return (Some cvalue)
+        | ListCons i cvalue tl0 => Return (Some cvalue)
         | ListNil => Fail_ Failure
         end
-      else hash_map_remove_from_list_loop_fwd T n0 i tl
+      else hash_map_remove_from_list_loop_fwd T n0 key tl
     | ListNil => Return None
     end
   end
@@ -433,21 +434,21 @@ Definition hash_map_remove_from_list_fwd
 
 (** [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) :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then
         let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
         match mv_ls with
-        | ListCons i0 cvalue tl0 => Return tl0
+        | ListCons i cvalue tl0 => Return tl0
         | ListNil => Fail_ Failure
         end
       else (
-        l <- hash_map_remove_from_list_loop_back T n0 i tl;
+        l <- hash_map_remove_from_list_loop_back T n0 key tl;
         Return (ListCons ckey t l))
     | ListNil => Return ListNil
     end
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 9ae7942c..2a8ab5b5 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -15,7 +15,7 @@ Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
 Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
-  (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (n0 : usize) :
+  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
   result (vec (Hashmap_list_t T))
   :=
   match n with
@@ -23,10 +23,10 @@ Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
   | S n1 =>
     if n0 s> 0%usize
     then (
-      slots <- vec_push_back (Hashmap_list_t T) v HashmapListNil;
+      slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil;
       n2 <- usize_sub n0 1%usize;
-      hashmap_hash_map_allocate_slots_loop_fwd T n1 slots n2)
-    else Return v
+      hashmap_hash_map_allocate_slots_loop_fwd T n1 slots0 n2)
+    else Return slots
   end
 .
 
@@ -60,19 +60,19 @@ Definition hashmap_hash_map_new_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
 Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back
-  (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (i : usize) :
+  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
   result (vec (Hashmap_list_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (Hashmap_list_t T) v in
+    let i0 := vec_len (Hashmap_list_t T) slots in
     if i s< i0
     then (
       i1 <- usize_add i 1%usize;
-      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
+      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
+      hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots0 i1)
+    else Return slots
   end
 .
 
@@ -192,7 +192,8 @@ 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_loop_fwd_back
-  (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) :
+  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
+  :
   result (Hashmap_hash_map_t T)
   :=
   match n with
@@ -200,9 +201,9 @@ Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
   | S n0 =>
     match ls with
     | HashmapListCons k v tl =>
-      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
+      ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v;
+      hashmap_hash_map_move_elements_from_list_loop_fwd_back T n0 ntable0 tl
+    | HashmapListNil => Return ntable
     end
   end
 .
@@ -218,24 +219,25 @@ Definition hashmap_hash_map_move_elements_from_list_fwd_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
 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) :
+  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
+  (slots : vec (Hashmap_list_t T)) (i : usize) :
   result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (Hashmap_list_t T) v in
+    let i0 := vec_len (Hashmap_list_t T) slots in
     if i s< i0
     then (
-      l <- vec_index_mut_fwd (Hashmap_list_t T) v i;
+      l <- vec_index_mut_fwd (Hashmap_list_t T) slots i;
       let ls := mem_replace_fwd (Hashmap_list_t T) l HashmapListNil in
-      ntable <- hashmap_hash_map_move_elements_from_list_fwd_back T n0 hm ls;
+      ntable0 <-
+        hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
       i1 <- usize_add i 1%usize;
       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)
+      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0;
+      hashmap_hash_map_move_elements_loop_fwd_back T n0 ntable0 slots0 i1)
+    else Return (ntable, slots)
   end
 .
 
@@ -288,15 +290,15 @@ Definition hashmap_hash_map_insert_fwd_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
 Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result bool :=
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | HashmapListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then Return true
-      else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 i tl
+      else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 key tl
     | HashmapListNil => Return false
     end
   end
@@ -322,15 +324,15 @@ Definition hashmap_hash_map_contains_key_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
 Fixpoint hashmap_hash_map_get_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T :=
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | HashmapListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return cvalue
-      else hashmap_hash_map_get_in_list_loop_fwd T n0 i tl
+      else hashmap_hash_map_get_in_list_loop_fwd T n0 key tl
     | HashmapListNil => Fail_ Failure
     end
   end
@@ -356,15 +358,15 @@ Definition hashmap_hash_map_get_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T :=
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | HashmapListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return cvalue
-      else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 i tl
+      else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 key tl
     | HashmapListNil => Fail_ Failure
     end
   end
@@ -378,7 +380,7 @@ Definition hashmap_hash_map_get_mut_in_list_fwd
 
 (** [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) :
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) :
   result (Hashmap_list_t T)
   :=
   match n with
@@ -386,10 +388,10 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
   | S n0 =>
     match ls with
     | HashmapListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return (HashmapListCons ckey ret tl)
       else (
-        l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 i tl ret;
+        l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 key tl ret;
         Return (HashmapListCons ckey cvalue l))
     | HashmapListNil => Fail_ Failure
     end
@@ -437,7 +439,7 @@ Definition hashmap_hash_map_get_mut_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) :
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
   result (option T)
   :=
   match n with
@@ -445,16 +447,16 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
   | S n0 =>
     match ls with
     | HashmapListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then
         let mv_ls :=
           mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
             HashmapListNil in
         match mv_ls with
-        | HashmapListCons i0 cvalue tl0 => Return (Some cvalue)
+        | HashmapListCons i cvalue tl0 => Return (Some cvalue)
         | HashmapListNil => Fail_ Failure
         end
-      else hashmap_hash_map_remove_from_list_loop_fwd T n0 i tl
+      else hashmap_hash_map_remove_from_list_loop_fwd T n0 key tl
     | HashmapListNil => Return None
     end
   end
@@ -470,7 +472,7 @@ Definition hashmap_hash_map_remove_from_list_fwd
 
 (** [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) :
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
   result (Hashmap_list_t T)
   :=
   match n with
@@ -478,17 +480,17 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back
   | S n0 =>
     match ls with
     | HashmapListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then
         let mv_ls :=
           mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
             HashmapListNil in
         match mv_ls with
-        | HashmapListCons i0 cvalue tl0 => Return tl0
+        | HashmapListCons i cvalue tl0 => Return tl0
         | HashmapListNil => Fail_ Failure
         end
       else (
-        l <- hashmap_hash_map_remove_from_list_loop_back T n0 i tl;
+        l <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl;
         Return (HashmapListCons ckey t l))
     | HashmapListNil => Return HashmapListNil
     end
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 22c2fd19..4fbb7da0 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -94,13 +94,13 @@ Arguments ListNil {T}.
 
 (** [loops::list_mem] *)
 Fixpoint list_mem_loop_fwd
-  (n : nat) (i : u32) (ls : List_t u32) : result bool :=
+  (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons y tl =>
-      if y s= i then Return true else list_mem_loop_fwd n0 i tl
+      if y s= x then Return true else list_mem_loop_fwd n0 x tl
     | ListNil => Return false
     end
   end
@@ -235,16 +235,16 @@ Definition get_elem_mut_back
 
 (** [loops::get_elem_shared] *)
 Fixpoint get_elem_shared_loop_fwd
-  (n : nat) (x : usize) (v : vec (List_t usize)) (l : List_t usize)
-  (ls : List_t usize) :
+  (n : nat) (x : usize) (slots : vec (List_t usize)) (ls : List_t usize)
+  (ls0 : List_t usize) :
   result usize
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match ls with
+    match ls0 with
     | ListCons y tl =>
-      if y s= x then Return y else get_elem_shared_loop_fwd n0 x v l tl
+      if y s= x then Return y else get_elem_shared_loop_fwd n0 x slots ls tl
     | ListNil => Fail_ Failure
     end
   end
@@ -329,17 +329,17 @@ Definition list_nth_mut_loop_with_id_back
 
 (** [loops::list_nth_shared_loop_with_id] *)
 Fixpoint list_nth_shared_loop_with_id_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (i : u32) (ls : List_t T) : result T :=
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ls0 : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match ls with
+    match ls0 with
     | ListCons x tl =>
       if i s= 0%u32
       then Return x
       else (
         i0 <- u32_sub i 1%u32;
-        list_nth_shared_loop_with_id_loop_fwd T n0 l i0 tl)
+        list_nth_shared_loop_with_id_loop_fwd T n0 ls i0 tl)
     | ListNil => Fail_ Failure
     end
   end
@@ -353,15 +353,15 @@ Definition list_nth_shared_loop_with_id_fwd
 
 (** [loops::list_nth_mut_loop_pair] *)
 Fixpoint list_nth_mut_loop_pair_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -385,22 +385,22 @@ Definition list_nth_mut_loop_pair_fwd
 
 (** [loops::list_nth_mut_loop_pair] *)
 Fixpoint list_nth_mut_loop_pair_loop_back'a
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l1))
+          l <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
+          Return (ListCons x0 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -418,22 +418,22 @@ Definition list_nth_mut_loop_pair_back'a
 
 (** [loops::list_nth_mut_loop_pair] *)
 Fixpoint list_nth_mut_loop_pair_loop_back'b
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l1))
+          l <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
+          Return (ListCons x1 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -451,15 +451,15 @@ Definition list_nth_mut_loop_pair_back'b
 
 (** [loops::list_nth_shared_loop_pair] *)
 Fixpoint list_nth_shared_loop_pair_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -483,15 +483,15 @@ Definition list_nth_shared_loop_pair_fwd
 
 (** [loops::list_nth_mut_loop_pair_merge] *)
 Fixpoint list_nth_mut_loop_pair_merge_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -515,24 +515,24 @@ Definition list_nth_mut_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_loop_pair_merge] *)
 Fixpoint list_nth_mut_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : (T * T))
-  :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32)
+  (ret : (T * T)) :
   result ((List_t T) * (List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then let (t, t0) := ret in Return (ListCons t tl0, ListCons t0 tl1)
         else (
           i0 <- u32_sub i 1%u32;
           p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          let (l1, l2) := p in
-          Return (ListCons x0 l1, ListCons x1 l2))
+          let (l, l0) := p in
+          Return (ListCons x0 l, ListCons x1 l0))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -551,15 +551,15 @@ Definition list_nth_mut_loop_pair_merge_back
 
 (** [loops::list_nth_shared_loop_pair_merge] *)
 Fixpoint list_nth_shared_loop_pair_merge_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -583,15 +583,15 @@ Definition list_nth_shared_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair] *)
 Fixpoint list_nth_mut_shared_loop_pair_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -615,22 +615,22 @@ Definition list_nth_mut_shared_loop_pair_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair] *)
 Fixpoint list_nth_mut_shared_loop_pair_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l1))
+          l <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x0 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -648,15 +648,15 @@ Definition list_nth_mut_shared_loop_pair_back
 
 (** [loops::list_nth_mut_shared_loop_pair_merge] *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -680,23 +680,23 @@ Definition list_nth_mut_shared_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair_merge] *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <-
+          l <-
             list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l1))
+          Return (ListCons x0 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -714,15 +714,15 @@ Definition list_nth_mut_shared_loop_pair_merge_back
 
 (** [loops::list_nth_shared_mut_loop_pair] *)
 Fixpoint list_nth_shared_mut_loop_pair_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -746,22 +746,22 @@ Definition list_nth_shared_mut_loop_pair_fwd
 
 (** [loops::list_nth_shared_mut_loop_pair] *)
 Fixpoint list_nth_shared_mut_loop_pair_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l1))
+          l <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x1 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -779,15 +779,15 @@ Definition list_nth_shared_mut_loop_pair_back
 
 (** [loops::list_nth_shared_mut_loop_pair_merge] *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -811,23 +811,23 @@ Definition list_nth_shared_mut_loop_pair_merge_fwd
 
 (** [loops::list_nth_shared_mut_loop_pair_merge] *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <-
+          l <-
             list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l1))
+          Return (ListCons x1 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index b8890f86..3e51c6f1 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) (v : vec (list_t t))
+let hash_map_allocate_slots_decreases (t : Type0) (slots : vec (list_t t))
   (n : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::clear_slots]: decreases clause *)
 unfold
-let hash_map_clear_slots_decreases (t : Type0) (v : vec (list_t t)) (i : usize)
-  : nat =
+let hash_map_clear_slots_decreases (t : Type0) (slots : 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) (hm : hash_map_t t)
-  (ls : list_t t) : nat =
+let hash_map_move_elements_from_list_decreases (t : Type0)
+  (ntable : 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) (hm : hash_map_t t)
-  (v : vec (list_t t)) (i : usize) : nat =
+let hash_map_move_elements_decreases (t : Type0) (ntable : hash_map_t t)
+  (slots : 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) (i : usize)
+let hash_map_contains_key_in_list_decreases (t : Type0) (key : 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) (i : usize) (ls : list_t t) :
+let hash_map_get_in_list_decreases (t : Type0) (key : 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) (i : usize) (ls : list_t t)
-  : nat =
+let hash_map_get_mut_in_list_decreases (t : Type0) (key : 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) (i : usize) (ls : list_t t)
-  : nat =
+let hash_map_remove_from_list_decreases (t : Type0) (key : usize)
+  (ls : list_t t) : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index d81da40b..81b253ad 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -12,21 +12,21 @@ let hash_key_fwd (k : usize) : result usize = Return k
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 let rec hash_map_allocate_slots_loop_fwd
-  (t : Type0) (v : vec (list_t t)) (n : usize) :
+  (t : Type0) (slots : vec (list_t t)) (n : usize) :
   Tot (result (vec (list_t t)))
-  (decreases (hash_map_allocate_slots_decreases t v n))
+  (decreases (hash_map_allocate_slots_decreases t slots n))
   =
   if n > 0
   then
-    begin match vec_push_back (list_t t) v ListNil with
+    begin match vec_push_back (list_t t) slots ListNil with
     | Fail e -> Fail e
-    | Return slots ->
+    | Return slots0 ->
       begin match usize_sub n 1 with
       | Fail e -> Fail e
-      | Return n0 -> hash_map_allocate_slots_loop_fwd t slots n0
+      | Return n0 -> hash_map_allocate_slots_loop_fwd t slots0 n0
       end
     end
-  else Return v
+  else Return slots
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 let hash_map_allocate_slots_fwd
@@ -60,22 +60,22 @@ let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
 let rec hash_map_clear_slots_loop_fwd_back
-  (t : Type0) (v : vec (list_t t)) (i : usize) :
+  (t : Type0) (slots : vec (list_t t)) (i : usize) :
   Tot (result (vec (list_t t)))
-  (decreases (hash_map_clear_slots_decreases t v i))
+  (decreases (hash_map_clear_slots_decreases t slots i))
   =
-  let i0 = vec_len (list_t t) v in
+  let i0 = vec_len (list_t t) slots in
   if i < i0
   then
     begin match usize_add i 1 with
     | Fail e -> Fail e
     | Return i1 ->
-      begin match vec_index_mut_back (list_t t) v i ListNil with
+      begin match vec_index_mut_back (list_t t) slots i ListNil with
       | Fail e -> Fail e
-      | Return slots -> hash_map_clear_slots_loop_fwd_back t slots i1
+      | Return slots0 -> hash_map_clear_slots_loop_fwd_back t slots0 i1
       end
     end
-  else Return v
+  else Return slots
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
 let hash_map_clear_slots_fwd_back
@@ -199,18 +199,18 @@ 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_loop_fwd_back
-  (t : Type0) (hm : hash_map_t t) (ls : list_t t) :
+  (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
   Tot (result (hash_map_t t))
-  (decreases (hash_map_move_elements_from_list_decreases t hm ls))
+  (decreases (hash_map_move_elements_from_list_decreases t ntable ls))
   =
   begin match ls with
   | ListCons k v tl ->
-    begin match hash_map_insert_no_resize_fwd_back t hm k v with
+    begin match hash_map_insert_no_resize_fwd_back t ntable k v with
     | Fail e -> Fail e
-    | Return ntable ->
-      hash_map_move_elements_from_list_loop_fwd_back t ntable tl
+    | Return ntable0 ->
+      hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl
     end
-  | ListNil -> Return hm
+  | ListNil -> Return ntable
   end
 
 (** [hashmap::HashMap::{0}::move_elements_from_list] *)
@@ -220,33 +220,33 @@ let hash_map_move_elements_from_list_fwd_back
 
 (** [hashmap::HashMap::{0}::move_elements] *)
 let rec hash_map_move_elements_loop_fwd_back
-  (t : Type0) (hm : hash_map_t t) (v : vec (list_t t)) (i : usize) :
+  (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
   Tot (result ((hash_map_t t) & (vec (list_t t))))
-  (decreases (hash_map_move_elements_decreases t hm v i))
+  (decreases (hash_map_move_elements_decreases t ntable slots i))
   =
-  let i0 = vec_len (list_t t) v in
+  let i0 = vec_len (list_t t) slots in
   if i < i0
   then
-    begin match vec_index_mut_fwd (list_t t) v i with
+    begin match vec_index_mut_fwd (list_t t) slots 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 hm ls with
+      begin match hash_map_move_elements_from_list_fwd_back t ntable ls with
       | Fail e -> Fail e
-      | Return ntable ->
+      | Return ntable0 ->
         begin match usize_add i 1 with
         | Fail e -> Fail e
         | 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
+          begin match vec_index_mut_back (list_t t) slots i l0 with
           | Fail e -> Fail e
-          | Return slots ->
-            hash_map_move_elements_loop_fwd_back t ntable slots i1
+          | Return slots0 ->
+            hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
           end
         end
       end
     end
-  else Return (hm, v)
+  else Return (ntable, slots)
 
 (** [hashmap::HashMap::{0}::move_elements] *)
 let hash_map_move_elements_fwd_back
@@ -313,15 +313,15 @@ let hash_map_insert_fwd_back
 
 (** [hashmap::HashMap::{0}::contains_key_in_list] *)
 let rec hash_map_contains_key_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : list_t t) :
+  (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result bool)
-  (decreases (hash_map_contains_key_in_list_decreases t i ls))
+  (decreases (hash_map_contains_key_in_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then Return true
-    else hash_map_contains_key_in_list_loop_fwd t i tl
+    else hash_map_contains_key_in_list_loop_fwd t key tl
   | ListNil -> Return false
   end
 
@@ -349,12 +349,14 @@ let hash_map_contains_key_fwd
 
 (** [hashmap::HashMap::{0}::get_in_list] *)
 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))
+  (t : Type0) (key : usize) (ls : list_t t) :
+  Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
-    if ckey = i then Return cvalue else hash_map_get_in_list_loop_fwd t i tl
+    if ckey = key
+    then Return cvalue
+    else hash_map_get_in_list_loop_fwd t key tl
   | ListNil -> Fail Failure
   end
 
@@ -382,14 +384,14 @@ let hash_map_get_fwd
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 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))
+  (t : Type0) (key : usize) (ls : list_t t) :
+  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return cvalue
-    else hash_map_get_mut_in_list_loop_fwd t i tl
+    else hash_map_get_mut_in_list_loop_fwd t key tl
   | ListNil -> Fail Failure
   end
 
@@ -400,16 +402,16 @@ let hash_map_get_mut_in_list_fwd
 
 (** [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) :
+  (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
   Tot (result (list_t t))
-  (decreases (hash_map_get_mut_in_list_decreases t i ls))
+  (decreases (hash_map_get_mut_in_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return (ListCons ckey ret tl)
     else
-      begin match hash_map_get_mut_in_list_loop_back t i tl ret with
+      begin match hash_map_get_mut_in_list_loop_back t key tl ret with
       | Fail e -> Fail e
       | Return l -> Return (ListCons ckey cvalue l)
       end
@@ -472,20 +474,20 @@ let hash_map_get_mut_back
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 let rec hash_map_remove_from_list_loop_fwd
-  (t : Type0) (i : usize) (ls : list_t t) :
+  (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result (option t))
-  (decreases (hash_map_remove_from_list_decreases t i ls))
+  (decreases (hash_map_remove_from_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then
       let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
       begin match mv_ls with
-      | ListCons i0 cvalue tl0 -> Return (Some cvalue)
+      | ListCons i cvalue tl0 -> Return (Some cvalue)
       | ListNil -> Fail Failure
       end
-    else hash_map_remove_from_list_loop_fwd t i tl
+    else hash_map_remove_from_list_loop_fwd t key tl
   | ListNil -> Return None
   end
 
@@ -496,21 +498,21 @@ let hash_map_remove_from_list_fwd
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 let rec hash_map_remove_from_list_loop_back
-  (t : Type0) (i : usize) (ls : list_t t) :
+  (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result (list_t t))
-  (decreases (hash_map_remove_from_list_decreases t i ls))
+  (decreases (hash_map_remove_from_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then
       let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
       begin match mv_ls with
-      | ListCons i0 cvalue tl0 -> Return tl0
+      | ListCons i cvalue tl0 -> Return tl0
       | ListNil -> Fail Failure
       end
     else
-      begin match hash_map_remove_from_list_loop_back t i tl with
+      begin match hash_map_remove_from_list_loop_back t key tl with
       | Fail e -> Fail e
       | Return l -> Return (ListCons ckey x l)
       end
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index b3081cd6..55685114 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)
-  (v : vec (hashmap_list_t t)) (n : usize) : nat =
+  (slots : 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)
-  (v : vec (hashmap_list_t t)) (i : usize) : nat =
+  (slots : vec (hashmap_list_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
@@ -31,36 +31,37 @@ 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)
-  (hm : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat =
+  (ntable : 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)
-  (hm : hashmap_hash_map_t t) (v : vec (hashmap_list_t t)) (i : usize) : nat =
+  (ntable : hashmap_hash_map_t t) (slots : 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) (i : usize)
+let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (key : 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) (i : usize)
+let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : 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) (i : usize)
+let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : 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) (i : usize)
+let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : 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 3da56f41..fdbf1404 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -13,21 +13,21 @@ 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_loop_fwd
-  (t : Type0) (v : vec (hashmap_list_t t)) (n : usize) :
+  (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
   Tot (result (vec (hashmap_list_t t)))
-  (decreases (hashmap_hash_map_allocate_slots_decreases t v n))
+  (decreases (hashmap_hash_map_allocate_slots_decreases t slots n))
   =
   if n > 0
   then
-    begin match vec_push_back (hashmap_list_t t) v HashmapListNil with
+    begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
     | Fail e -> Fail e
-    | Return slots ->
+    | Return slots0 ->
       begin match usize_sub n 1 with
       | Fail e -> Fail e
-      | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots n0
+      | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0
       end
     end
-  else Return v
+  else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
 let hashmap_hash_map_allocate_slots_fwd
@@ -64,22 +64,23 @@ let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
 let rec hashmap_hash_map_clear_slots_loop_fwd_back
-  (t : Type0) (v : vec (hashmap_list_t t)) (i : usize) :
+  (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) :
   Tot (result (vec (hashmap_list_t t)))
-  (decreases (hashmap_hash_map_clear_slots_decreases t v i))
+  (decreases (hashmap_hash_map_clear_slots_decreases t slots i))
   =
-  let i0 = vec_len (hashmap_list_t t) v in
+  let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
   then
     begin match usize_add i 1 with
     | Fail e -> Fail e
     | Return i1 ->
-      begin match vec_index_mut_back (hashmap_list_t t) v i HashmapListNil with
+      begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
+        with
       | Fail e -> Fail e
-      | Return slots -> hashmap_hash_map_clear_slots_loop_fwd_back t slots i1
+      | Return slots0 -> hashmap_hash_map_clear_slots_loop_fwd_back t slots0 i1
       end
     end
-  else Return v
+  else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
 let hashmap_hash_map_clear_slots_fwd_back
@@ -214,18 +215,18 @@ 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_loop_fwd_back
-  (t : Type0) (hm : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
+  (t : Type0) (ntable : 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 hm ls))
+  (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls))
   =
   begin match ls with
   | HashmapListCons k v tl ->
-    begin match hashmap_hash_map_insert_no_resize_fwd_back t hm k v with
+    begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
     | Fail e -> Fail e
-    | Return ntable ->
-      hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable tl
+    | Return ntable0 ->
+      hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl
     end
-  | HashmapListNil -> Return hm
+  | HashmapListNil -> Return ntable
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
@@ -237,35 +238,35 @@ let hashmap_hash_map_move_elements_from_list_fwd_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
 let rec hashmap_hash_map_move_elements_loop_fwd_back
-  (t : Type0) (hm : hashmap_hash_map_t t) (v : vec (hashmap_list_t t))
+  (t : Type0) (ntable : hashmap_hash_map_t t) (slots : 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 hm v i))
+  (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i))
   =
-  let i0 = vec_len (hashmap_list_t t) v in
+  let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
   then
-    begin match vec_index_mut_fwd (hashmap_list_t t) v i with
+    begin match vec_index_mut_fwd (hashmap_list_t t) slots 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 hm ls
+      begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls
         with
       | Fail e -> Fail e
-      | Return ntable ->
+      | Return ntable0 ->
         begin match usize_add i 1 with
         | Fail e -> Fail e
         | 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
+          begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
           | Fail e -> Fail e
-          | Return slots ->
-            hashmap_hash_map_move_elements_loop_fwd_back t ntable slots i1
+          | Return slots0 ->
+            hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
           end
         end
       end
     end
-  else Return (hm, v)
+  else Return (ntable, slots)
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
 let hashmap_hash_map_move_elements_fwd_back
@@ -334,15 +335,15 @@ let hashmap_hash_map_insert_fwd_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
 let rec hashmap_hash_map_contains_key_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result bool)
-  (decreases (hashmap_hash_map_contains_key_in_list_decreases t i ls))
+  (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then Return true
-    else hashmap_hash_map_contains_key_in_list_loop_fwd t i tl
+    else hashmap_hash_map_contains_key_in_list_loop_fwd t key tl
   | HashmapListNil -> Return false
   end
 
@@ -372,14 +373,14 @@ let hashmap_hash_map_contains_key_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
 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))
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+  Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return cvalue
-    else hashmap_hash_map_get_in_list_loop_fwd t i tl
+    else hashmap_hash_map_get_in_list_loop_fwd t key tl
   | HashmapListNil -> Fail Failure
   end
 
@@ -409,15 +410,15 @@ let hashmap_hash_map_get_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hashmap_hash_map_get_mut_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result t)
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return cvalue
-    else hashmap_hash_map_get_mut_in_list_loop_fwd t i tl
+    else hashmap_hash_map_get_mut_in_list_loop_fwd t key tl
   | HashmapListNil -> Fail Failure
   end
 
@@ -428,16 +429,16 @@ let hashmap_hash_map_get_mut_in_list_fwd
 
 (** [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) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) :
   Tot (result (hashmap_list_t t))
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return (HashmapListCons ckey ret tl)
     else
-      begin match hashmap_hash_map_get_mut_in_list_loop_back t i tl ret with
+      begin match hashmap_hash_map_get_mut_in_list_loop_back t key tl ret with
       | Fail e -> Fail e
       | Return l -> Return (HashmapListCons ckey cvalue l)
       end
@@ -506,22 +507,22 @@ let hashmap_hash_map_get_mut_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 let rec hashmap_hash_map_remove_from_list_loop_fwd
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result (option t))
-  (decreases (hashmap_hash_map_remove_from_list_decreases t i ls))
+  (decreases (hashmap_hash_map_remove_from_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then
       let mv_ls =
         mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
           HashmapListNil in
       begin match mv_ls with
-      | HashmapListCons i0 cvalue tl0 -> Return (Some cvalue)
+      | HashmapListCons i cvalue tl0 -> Return (Some cvalue)
       | HashmapListNil -> Fail Failure
       end
-    else hashmap_hash_map_remove_from_list_loop_fwd t i tl
+    else hashmap_hash_map_remove_from_list_loop_fwd t key tl
   | HashmapListNil -> Return None
   end
 
@@ -532,23 +533,23 @@ let hashmap_hash_map_remove_from_list_fwd
 
 (** [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) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result (hashmap_list_t t))
-  (decreases (hashmap_hash_map_remove_from_list_decreases t i ls))
+  (decreases (hashmap_hash_map_remove_from_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then
       let mv_ls =
         mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
           HashmapListNil in
       begin match mv_ls with
-      | HashmapListCons i0 cvalue tl0 -> Return tl0
+      | HashmapListCons i cvalue tl0 -> Return tl0
       | HashmapListNil -> Fail Failure
       end
     else
-      begin match hashmap_hash_map_remove_from_list_loop_back t i tl with
+      begin match hashmap_hash_map_remove_from_list_loop_back t key tl with
       | Fail e -> Fail e
       | Return l -> Return (HashmapListCons ckey x l)
       end
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 3d475d20..1b141d64 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -23,7 +23,7 @@ let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
 unfold let clear_decreases (v : vec u32) (i : usize) : nat = admit ()
 
 (** [loops::list_mem]: decreases clause *)
-unfold let list_mem_decreases (i : u32) (ls : list_t u32) : nat = admit ()
+unfold let list_mem_decreases (x : u32) (ls : list_t u32) : nat = admit ()
 
 (** [loops::list_nth_mut_loop]: decreases clause *)
 unfold
@@ -42,8 +42,8 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : nat = admit ()
 
 (** [loops::get_elem_shared]: decreases clause *)
 unfold
-let get_elem_shared_decreases (x : usize) (v : vec (list_t usize))
-  (l : list_t usize) (ls : list_t usize) : nat =
+let get_elem_shared_decreases (x : usize) (slots : vec (list_t usize))
+  (ls : list_t usize) (ls0 : list_t usize) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_with_id]: decreases clause *)
@@ -54,55 +54,55 @@ let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) :
 
 (** [loops::list_nth_shared_loop_with_id]: decreases clause *)
 unfold
-let list_nth_shared_loop_with_id_decreases (t : Type0) (l : list_t t) 
-  (i : u32) (ls : list_t t) : nat =
+let list_nth_shared_loop_with_id_decreases (t : Type0) (ls : list_t t)
+  (i : u32) (ls0 : list_t t) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_pair]: decreases clause *)
 unfold
-let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
-  (i : u32) : nat =
+let list_nth_mut_loop_pair_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_loop_pair]: decreases clause *)
 unfold
-let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_shared_loop_pair_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
 unfold
-let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_mut_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
 unfold
-let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_shared_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
 unfold
-let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_mut_shared_loop_pair_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *)
 unfold
-let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
 unfold
-let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_shared_mut_loop_pair_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *)
 unfold
-let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index b7dcd045..ca918e35 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -92,11 +92,11 @@ let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0
 
 (** [loops::list_mem] *)
 let rec list_mem_loop_fwd
-  (i : u32) (ls : list_t u32) :
-  Tot (result bool) (decreases (list_mem_decreases i ls))
+  (x : u32) (ls : list_t u32) :
+  Tot (result bool) (decreases (list_mem_decreases x ls))
   =
   begin match ls with
-  | ListCons y tl -> if y = i then Return true else list_mem_loop_fwd i tl
+  | ListCons y tl -> if y = x then Return true else list_mem_loop_fwd x tl
   | ListNil -> Return false
   end
 
@@ -222,12 +222,13 @@ let get_elem_mut_back
 
 (** [loops::get_elem_shared] *)
 let rec get_elem_shared_loop_fwd
-  (x : usize) (v : vec (list_t usize)) (l : list_t usize) (ls : list_t usize) :
-  Tot (result usize) (decreases (get_elem_shared_decreases x v l ls))
+  (x : usize) (slots : vec (list_t usize)) (ls : list_t usize)
+  (ls0 : list_t usize) :
+  Tot (result usize) (decreases (get_elem_shared_decreases x slots ls ls0))
   =
-  begin match ls with
+  begin match ls0 with
   | ListCons y tl ->
-    if y = x then Return y else get_elem_shared_loop_fwd x v l tl
+    if y = x then Return y else get_elem_shared_loop_fwd x slots ls tl
   | ListNil -> Fail Failure
   end
 
@@ -311,17 +312,18 @@ let list_nth_mut_loop_with_id_back
 
 (** [loops::list_nth_shared_loop_with_id] *)
 let rec list_nth_shared_loop_with_id_loop_fwd
-  (t : Type0) (l : list_t t) (i : u32) (ls : list_t t) :
-  Tot (result t) (decreases (list_nth_shared_loop_with_id_decreases t l i ls))
+  (t : Type0) (ls : list_t t) (i : u32) (ls0 : list_t t) :
+  Tot (result t)
+  (decreases (list_nth_shared_loop_with_id_decreases t ls i ls0))
   =
-  begin match ls with
+  begin match ls0 with
   | ListCons x tl ->
     if i = 0
     then Return x
     else
       begin match u32_sub i 1 with
       | Fail e -> Fail e
-      | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t l i0 tl
+      | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t ls i0 tl
       end
   | ListNil -> Fail Failure
   end
@@ -336,12 +338,13 @@ let list_nth_shared_loop_with_id_fwd
 
 (** [loops::list_nth_mut_loop_pair] *)
 let rec list_nth_mut_loop_pair_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
-  Tot (result (t & t)) (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -362,13 +365,13 @@ let list_nth_mut_loop_pair_fwd
 
 (** [loops::list_nth_mut_loop_pair] *)
 let rec list_nth_mut_loop_pair_loop_back'a
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
@@ -378,7 +381,7 @@ let rec list_nth_mut_loop_pair_loop_back'a
         | Return i0 ->
           begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x0 l1)
+          | Return l -> Return (ListCons x0 l)
           end
         end
     | ListNil -> Fail Failure
@@ -395,13 +398,13 @@ let list_nth_mut_loop_pair_back'a
 
 (** [loops::list_nth_mut_loop_pair] *)
 let rec list_nth_mut_loop_pair_loop_back'b
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
@@ -411,7 +414,7 @@ let rec list_nth_mut_loop_pair_loop_back'b
         | Return i0 ->
           begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x1 l1)
+          | Return l -> Return (ListCons x1 l)
           end
         end
     | ListNil -> Fail Failure
@@ -428,13 +431,13 @@ let list_nth_mut_loop_pair_back'b
 
 (** [loops::list_nth_shared_loop_pair] *)
 let rec list_nth_shared_loop_pair_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_shared_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -455,13 +458,13 @@ let list_nth_shared_loop_pair_fwd
 
 (** [loops::list_nth_mut_loop_pair_merge] *)
 let rec list_nth_mut_loop_pair_merge_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_mut_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -482,13 +485,13 @@ let list_nth_mut_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_loop_pair_merge] *)
 let rec list_nth_mut_loop_pair_merge_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : (t & t)) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) :
   Tot (result ((list_t t) & (list_t t)))
-  (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_mut_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1)
@@ -499,7 +502,7 @@ let rec list_nth_mut_loop_pair_merge_loop_back
           begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return (l1, l2) -> Return (ListCons x0 l1, ListCons x1 l2)
+          | Return (l, l0) -> Return (ListCons x0 l, ListCons x1 l0)
           end
         end
     | ListNil -> Fail Failure
@@ -516,13 +519,13 @@ let list_nth_mut_loop_pair_merge_back
 
 (** [loops::list_nth_shared_loop_pair_merge] *)
 let rec list_nth_shared_loop_pair_merge_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_shared_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -543,13 +546,13 @@ let list_nth_shared_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair] *)
 let rec list_nth_mut_shared_loop_pair_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_mut_shared_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -570,13 +573,13 @@ let list_nth_mut_shared_loop_pair_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair] *)
 let rec list_nth_mut_shared_loop_pair_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_mut_shared_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
@@ -587,7 +590,7 @@ let rec list_nth_mut_shared_loop_pair_loop_back
           begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x0 l1)
+          | Return l -> Return (ListCons x0 l)
           end
         end
     | ListNil -> Fail Failure
@@ -604,13 +607,13 @@ let list_nth_mut_shared_loop_pair_back
 
 (** [loops::list_nth_mut_shared_loop_pair_merge] *)
 let rec list_nth_mut_shared_loop_pair_merge_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_mut_shared_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -632,13 +635,13 @@ let list_nth_mut_shared_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair_merge] *)
 let rec list_nth_mut_shared_loop_pair_merge_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_mut_shared_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
@@ -649,7 +652,7 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back
           begin match
             list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x0 l1)
+          | Return l -> Return (ListCons x0 l)
           end
         end
     | ListNil -> Fail Failure
@@ -666,13 +669,13 @@ let list_nth_mut_shared_loop_pair_merge_back
 
 (** [loops::list_nth_shared_mut_loop_pair] *)
 let rec list_nth_shared_mut_loop_pair_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_shared_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -693,13 +696,13 @@ let list_nth_shared_mut_loop_pair_fwd
 
 (** [loops::list_nth_shared_mut_loop_pair] *)
 let rec list_nth_shared_mut_loop_pair_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_shared_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
@@ -710,7 +713,7 @@ let rec list_nth_shared_mut_loop_pair_loop_back
           begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x1 l1)
+          | Return l -> Return (ListCons x1 l)
           end
         end
     | ListNil -> Fail Failure
@@ -727,13 +730,13 @@ let list_nth_shared_mut_loop_pair_back
 
 (** [loops::list_nth_shared_mut_loop_pair_merge] *)
 let rec list_nth_shared_mut_loop_pair_merge_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_shared_mut_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -755,13 +758,13 @@ let list_nth_shared_mut_loop_pair_merge_fwd
 
 (** [loops::list_nth_shared_mut_loop_pair_merge] *)
 let rec list_nth_shared_mut_loop_pair_merge_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_shared_mut_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
@@ -772,7 +775,7 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back
           begin match
             list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x1 l1)
+          | Return l -> Return (ListCons x1 l)
           end
         end
     | ListNil -> Fail Failure