Fix an issue with the names of the loop decreases clauses

13 files changed, 186 insertions, 154 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index b3d7b49e..518e8979 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -427,13 +427,14 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     fname ^ suffix
   in
 
-  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string
-      =
+  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name)
+      (num_loops : int) (loop_id : LoopId.id option) : string =
     let fname = fun_name_to_snake_case fname in
+    let lp_suffix = default_fun_loop_suffix num_loops loop_id in
     (* Compute the suffix *)
     let suffix = "_decreases" in
     (* Concatenate *)
-    fname ^ suffix
+    fname ^ lp_suffix ^ suffix
   in
 
   let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index a9b44017..3ad55d37 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -189,7 +189,8 @@ type formatter = {
               filtered some of them.
           TODO: use the fun id for the assumed functions.
        *)
-  decreases_clause_name : A.FunDeclId.id -> fun_name -> string;
+  decreases_clause_name :
+    A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string;
       (** Generates the name of the definition used to prove/reason about
           termination. The generated code uses this clause where needed,
           but its body must be defined by the user.
@@ -198,6 +199,9 @@ type formatter = {
           - function id: this is especially useful to identify whether the
             function is an assumed function or a local function
           - function basename
+          - the number of loops in the parent function. This is used for
+            the same purpose as in {!field:fun_name}.
+          - loop identifier, if this is for a loop
        *)
   var_basename : StringSet.t -> string option -> ty -> string;
       (** Generates a variable basename.
@@ -678,7 +682,10 @@ let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
 
 let ctx_add_decreases_clause (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
-  let name = ctx.fmt.decreases_clause_name def.def_id def.basename in
+  let name =
+    ctx.fmt.decreases_clause_name def.def_id def.basename def.num_loops
+      def.loop_id
+  in
   ctx_add (DecreasesClauseId (Regular def.def_id, def.loop_id)) name ctx
 
 let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
@@ -801,6 +808,18 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
 let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
   fmt.type_name def.name
 
+(** Helper function: generate a suffix for a function name, i.e., generates
+    a suffix like "_loop", "loop1", etc. to append to a function name.
+ *)
+let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) :
+    string =
+  match loop_id with
+  | None -> ""
+  | Some loop_id ->
+      (* If this is for a loop, generally speaking, we append the loop index.
+         If this function admits only one loop, we omit it. *)
+      if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id
+
 (** A helper function: generates a function suffix from a region group
     information.
     TODO: move all those helpers.
@@ -808,6 +827,8 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
 let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
     (num_region_groups : int) (rg : region_group_info option)
     ((keep_fwd, num_backs) : bool * int) : string =
+  let lp_suff = default_fun_loop_suffix num_loops loop_id in
+
   (* There are several cases:
      - [rg] is [Some]: this is a forward function:
        - we add "_fwd"
@@ -823,13 +844,6 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
      we could not add the "_fwd" suffix) to prevent name clashes between
      definitions (in particular between type and function definitions).
   *)
-  let lp_suff =
-    match loop_id with
-    | None -> ""
-    | Some loop_id ->
-        if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id
-  in
-
   let rg_suff =
     match rg with
     | None -> "_fwd"
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 66280ed7..966ccf70 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -545,6 +545,16 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   if config.extract_template_decreases_clauses then
     List.iter
       (fun (_, ((fwd, loop_fwds), _)) ->
+        (* We only generate decreases clauses for the forward functions, because
+           the termination argument should only depend on the forward inputs.
+           The backward functions thus use the same decreases clauses as the
+           forward function.
+
+           Rem.: we might filter backward functions in {!PureMicroPasses}, but
+           we don't remove forward functions. Instead, we remember if we should
+           filter those functions at extraction time with a boolean (see the
+           type of the [pure_ls] input parameter).
+        *)
         let extract_decrease decl =
           let has_decr_clause = has_decreases_clause decl in
           if has_decr_clause then
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index ce86071c..4e490b6c 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -8,20 +8,20 @@ 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_loop_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) (slots : vec (list_t t))
+let hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (list_t t))
   (i : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
 unfold
-let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
-  (ls : list_t t) : nat =
+let hash_map_insert_in_list_loop_decreases (t : Type0) (key : usize)
+  (value : t) (ls : list_t t) : nat =
   admit ()
 
 (** [core::num::u32::{9}::MAX] *)
@@ -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)
+let hash_map_move_elements_from_list_loop_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) (ntable : hash_map_t t)
+let hash_map_move_elements_loop_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) (key : usize)
+let hash_map_contains_key_in_list_loop_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) (key : usize) (ls : list_t t) :
-  nat =
+let hash_map_get_in_list_loop_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) (ls : list_t t)
+let hash_map_get_mut_in_list_loop_decreases (t : Type0) (ls : list_t t)
   (key : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
 unfold
-let hash_map_remove_from_list_decreases (t : Type0) (key : usize)
+let hash_map_remove_from_list_loop_decreases (t : Type0) (key : usize)
   (ls : list_t t) : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.fst b/tests/fstar/hashmap/Hashmap.Clauses.fst
index 2a9c0242..b525880a 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.fst
@@ -8,54 +8,54 @@ open Hashmap.Types
 
 (** [hashmap::HashMap::allocate_slots]: decreases clause *)
 unfold
-let hash_map_allocate_slots_decreases (t : Type0) (slots : vec (list_t t))
+let hash_map_allocate_slots_loop_decreases (t : Type0) (slots : vec (list_t t))
   (n : usize) : nat = n
 
 (** [hashmap::HashMap::clear_slots]: decreases clause *)
 unfold
-let hash_map_clear_slots_decreases (t : Type0) (slots : vec (list_t t))
+let hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (list_t t))
   (i : usize) : nat =
   if i < length slots then length slots - i else 0
 
 (** [hashmap::HashMap::insert_in_list]: decreases clause *)
 unfold
-let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
+let hash_map_insert_in_list_loop_decreases (t : Type0) (key : usize) (value : t)
   (ls : list_t t) : list_t t =
   ls
 
 (** [hashmap::HashMap::move_elements_from_list]: decreases clause *)
 unfold
-let hash_map_move_elements_from_list_decreases (t : Type0)
+let hash_map_move_elements_from_list_loop_decreases (t : Type0)
   (ntable : hash_map_t t) (ls : list_t t) : list_t t =
   ls
 
 (** [hashmap::HashMap::move_elements]: decreases clause *)
 unfold
-let hash_map_move_elements_decreases (t : Type0) (ntable : hash_map_t t)
+let hash_map_move_elements_loop_decreases (t : Type0) (ntable : hash_map_t t)
   (slots : vec (list_t t)) (i : usize) : nat =
   if i < length slots then length slots - i else 0
 
 (** [hashmap::HashMap::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_loop_decreases (t : Type0) (key : usize)
   (ls : list_t t) : list_t t =
   ls
 
 (** [hashmap::HashMap::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_loop_decreases (t : Type0) (key : usize) (ls : list_t t) :
   list_t t =
   ls
 
 (** [hashmap::HashMap::get_mut_in_list]: decreases clause *)
 unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (ls : list_t t)
+let hash_map_get_mut_in_list_loop_decreases (t : Type0) (ls : list_t t)
   (key : usize) : list_t t =
   ls
 
 (** [hashmap::HashMap::remove_from_list]: decreases clause *)
 unfold
-let hash_map_remove_from_list_decreases (t : Type0) (key : usize)
+let hash_map_remove_from_list_loop_decreases (t : Type0) (key : usize)
   (ls : list_t t) : list_t t =
   ls
 
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 14cea9cb..2074d02e 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -14,7 +14,7 @@ let hash_key_fwd (k : usize) : result usize = Return k
 let rec hash_map_allocate_slots_loop_fwd
   (t : Type0) (slots : 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_loop_decreases t slots n))
   =
   if n > 0
   then
@@ -62,7 +62,7 @@ let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
 let rec hash_map_clear_slots_loop_fwd_back
   (t : Type0) (slots : 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_loop_decreases t slots i))
   =
   let i0 = vec_len (list_t t) slots in
   if i < i0
@@ -100,7 +100,7 @@ let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
 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))
+  (decreases (hash_map_insert_in_list_loop_decreases t key value ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
@@ -119,7 +119,7 @@ let hash_map_insert_in_list_fwd
 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))
+  (decreases (hash_map_insert_in_list_loop_decreases t key value ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
@@ -201,7 +201,7 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 let rec hash_map_move_elements_from_list_loop_fwd_back
   (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 ntable ls))
+  (decreases (hash_map_move_elements_from_list_loop_decreases t ntable ls))
   =
   begin match ls with
   | ListCons k v tl ->
@@ -222,7 +222,7 @@ let hash_map_move_elements_from_list_fwd_back
 let rec hash_map_move_elements_loop_fwd_back
   (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 ntable slots i))
+  (decreases (hash_map_move_elements_loop_decreases t ntable slots i))
   =
   let i0 = vec_len (list_t t) slots in
   if i < i0
@@ -315,7 +315,7 @@ let hash_map_insert_fwd_back
 let rec hash_map_contains_key_in_list_loop_fwd
   (t : Type0) (key : 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_loop_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
@@ -350,7 +350,7 @@ let hash_map_contains_key_fwd
 (** [hashmap::HashMap::{0}::get_in_list] *)
 let rec hash_map_get_in_list_loop_fwd
   (t : Type0) (key : usize) (ls : list_t t) :
-  Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls))
+  Tot (result t) (decreases (hash_map_get_in_list_loop_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
@@ -385,7 +385,7 @@ let hash_map_get_fwd
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hash_map_get_mut_in_list_loop_fwd
   (t : Type0) (ls : list_t t) (key : usize) :
-  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t ls key))
+  Tot (result t) (decreases (hash_map_get_mut_in_list_loop_decreases t ls key))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
@@ -404,7 +404,7 @@ let hash_map_get_mut_in_list_fwd
 let rec hash_map_get_mut_in_list_loop_back
   (t : Type0) (ls : list_t t) (key : usize) (ret : t) :
   Tot (result (list_t t))
-  (decreases (hash_map_get_mut_in_list_decreases t ls key))
+  (decreases (hash_map_get_mut_in_list_loop_decreases t ls key))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
@@ -476,7 +476,7 @@ let hash_map_get_mut_back
 let rec hash_map_remove_from_list_loop_fwd
   (t : Type0) (key : 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_loop_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
@@ -500,7 +500,7 @@ let hash_map_remove_from_list_fwd
 let rec hash_map_remove_from_list_loop_back
   (t : Type0) (key : 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_loop_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index e1d0a541..b1352443 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -509,7 +509,7 @@ val hash_map_allocate_slots_fwd_lem
      (forall (i:nat{i < length slots}). index slots' i == index slots i) /\
      // We allocate n additional empty slots
      (forall (i:nat{length slots <= i /\ i < length slots'}). index slots' i == ListNil)))
-  (decreases (hash_map_allocate_slots_decreases t slots n))
+  (decreases (hash_map_allocate_slots_loop_decreases t slots n))
 
 #push-options "--fuel 1"
 let rec hash_map_allocate_slots_fwd_lem t slots n =
@@ -633,7 +633,7 @@ let rec hash_map_clear_slots_loop_fwd_back_lem
       (forall (j:nat{j < i /\ j < length slots}). index slots' j == index slots j) /\
       // The slots after i are set to ListNil
       (forall (j:nat{i <= j /\ j < length slots}). index slots' j == ListNil)))
-  (decreases (hash_map_clear_slots_decreases t slots i))
+  (decreases (hash_map_clear_slots_loop_decreases t slots i))
   =
   let i0 = vec_len (list_t t) slots in
   let b = i < i0 in
@@ -717,7 +717,7 @@ val hash_map_insert_in_list_fwd_lem
     | Fail _ -> False
     | Return b ->
       b <==> (slot_t_find_s key ls == None)))
-  (decreases (hash_map_insert_in_list_decreases t key value ls))
+  (decreases (hash_map_insert_in_list_loop_decreases t key value ls))
 
 #push-options "--fuel 1"
 let rec hash_map_insert_in_list_fwd_lem t key value ls =
@@ -772,7 +772,7 @@ val hash_map_insert_in_list_back_lem_append_s
     | Fail _ -> False
     | Return ls' ->
       list_t_v ls' == list_t_v ls @ [(key,value)]))
-  (decreases (hash_map_insert_in_list_decreases t key value ls))
+  (decreases (hash_map_insert_in_list_loop_decreases t key value ls))
 
 #push-options "--fuel 1"
 let rec hash_map_insert_in_list_back_lem_append_s t key value ls =
@@ -803,7 +803,7 @@ val hash_map_insert_in_list_back_lem_update_s
     | Fail _ -> False
     | Return ls' ->
       list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,value)))
-  (decreases (hash_map_insert_in_list_decreases t key value ls))
+  (decreases (hash_map_insert_in_list_loop_decreases t key value ls))
 
 #push-options "--fuel 1"
 let rec hash_map_insert_in_list_back_lem_update_s t key value ls =
@@ -1112,7 +1112,7 @@ val hash_map_insert_in_list_back_lem
        | Some _ ->
          list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,value) /\
          list_t_len ls' = list_t_len ls)))
-  (decreases (hash_map_insert_in_list_decreases t key value ls))
+  (decreases (hash_map_insert_in_list_loop_decreases t key value ls))
 
 let hash_map_insert_in_list_back_lem t len key value ls =
   hash_map_insert_in_list_back_lem_s t key value ls;
@@ -1396,7 +1396,7 @@ val hash_map_move_elements_from_list_fwd_back_lem
       hash_map_t_v hm' == hm_v /\
       hash_map_t_same_params hm' ntable
     | _ -> False))
-  (decreases (hash_map_move_elements_from_list_decreases t ntable ls))
+  (decreases (hash_map_move_elements_from_list_loop_decreases t ntable ls))
 
 #push-options "--fuel 1"
 let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls =
@@ -1455,7 +1455,7 @@ let rec hash_map_move_elements_s_simpl
       ntable1 == ntable2 /\
       slots1 == slots2
     | _ -> False))
-  (decreases (hash_map_move_elements_decreases t ntable slots i))
+  (decreases (hash_map_move_elements_loop_decreases t ntable slots i))
   =
   if i < length slots
   then
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index 871de28a..f3afa008 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -8,19 +8,19 @@ open HashmapMain.Types
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
 unfold
-let hashmap_hash_map_allocate_slots_decreases (t : Type0)
+let hashmap_hash_map_allocate_slots_loop_decreases (t : Type0)
   (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)
+let hashmap_hash_map_clear_slots_loop_decreases (t : Type0)
   (slots : vec (hashmap_list_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize)
+let hashmap_hash_map_insert_in_list_loop_decreases (t : Type0) (key : usize)
   (value : t) (ls : hashmap_list_t t) : nat =
   admit ()
 
@@ -30,38 +30,38 @@ 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)
+let hashmap_hash_map_move_elements_from_list_loop_decreases (t : Type0)
   (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)
+let hashmap_hash_map_move_elements_loop_decreases (t : Type0)
   (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) (key : usize)
-  (ls : hashmap_list_t t) : nat =
+let hashmap_hash_map_contains_key_in_list_loop_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) (key : usize)
+let hashmap_hash_map_get_in_list_loop_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)
+let hashmap_hash_map_get_mut_in_list_loop_decreases (t : Type0)
   (ls : hashmap_list_t t) (key : usize) : 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_loop_decreases (t : Type0) (key : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
index 8afe2523..2f6a0acc 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
@@ -8,54 +8,54 @@ open HashmapMain.Types
 
 (** [hashmap::HashMap::allocate_slots]: decreases clause *)
 unfold
-let hashmap_hash_map_allocate_slots_decreases (t : Type0) (slots : vec (hashmap_list_t t))
+let hashmap_hash_map_allocate_slots_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t))
   (n : usize) : nat = n
 
 (** [hashmap::HashMap::clear_slots]: decreases clause *)
 unfold
-let hashmap_hash_map_clear_slots_decreases (t : Type0) (slots : vec (hashmap_list_t t))
+let hashmap_hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t))
   (i : usize) : nat =
   if i < length slots then length slots - i else 0
 
 (** [hashmap::HashMap::insert_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
+let hashmap_hash_map_insert_in_list_loop_decreases (t : Type0) (key : usize) (value : t)
   (ls : hashmap_list_t t) : hashmap_list_t t =
   ls
 
 (** [hashmap::HashMap::move_elements_from_list]: decreases clause *)
 unfold
-let hashmap_hash_map_move_elements_from_list_decreases (t : Type0)
+let hashmap_hash_map_move_elements_from_list_loop_decreases (t : Type0)
   (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : hashmap_list_t t =
   ls
 
 (** [hashmap::HashMap::move_elements]: decreases clause *)
 unfold
-let hashmap_hash_map_move_elements_decreases (t : Type0) (ntable : hashmap_hash_map_t t)
+let hashmap_hash_map_move_elements_loop_decreases (t : Type0) (ntable : hashmap_hash_map_t t)
   (slots : vec (hashmap_list_t t)) (i : usize) : nat =
   if i < length slots then length slots - i else 0
 
 (** [hashmap::HashMap::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_loop_decreases (t : Type0) (key : usize)
   (ls : hashmap_list_t t) : hashmap_list_t t =
   ls
 
 (** [hashmap::HashMap::get_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+let hashmap_hash_map_get_in_list_loop_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   hashmap_list_t t =
   ls
 
 (** [hashmap::HashMap::get_mut_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_get_mut_in_list_decreases (t : Type0)
+let hashmap_hash_map_get_mut_in_list_loop_decreases (t : Type0)
   (ls : hashmap_list_t t) (key : usize) : hashmap_list_t t =
   ls
 
 (** [hashmap::HashMap::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_loop_decreases (t : Type0) (key : usize)
   (ls : hashmap_list_t t) : hashmap_list_t t =
   ls
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 42ee2a17..d2b87305 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -15,7 +15,7 @@ let hashmap_hash_key_fwd (k : usize) : result usize = Return k
 let rec hashmap_hash_map_allocate_slots_loop_fwd
   (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 slots n))
+  (decreases (hashmap_hash_map_allocate_slots_loop_decreases t slots n))
   =
   if n > 0
   then
@@ -66,7 +66,7 @@ let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
 let rec hashmap_hash_map_clear_slots_loop_fwd_back
   (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 slots i))
+  (decreases (hashmap_hash_map_clear_slots_loop_decreases t slots i))
   =
   let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
@@ -109,7 +109,7 @@ let hashmap_hash_map_len_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))
+  (decreases (hashmap_hash_map_insert_in_list_loop_decreases t key value ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
@@ -128,7 +128,7 @@ let hashmap_hash_map_insert_in_list_fwd
 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))
+  (decreases (hashmap_hash_map_insert_in_list_loop_decreases t key value ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
@@ -217,7 +217,8 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
   (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 ntable ls))
+  (decreases (
+    hashmap_hash_map_move_elements_from_list_loop_decreases t ntable ls))
   =
   begin match ls with
   | HashmapListCons k v tl ->
@@ -241,7 +242,7 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back
   (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 ntable slots i))
+  (decreases (hashmap_hash_map_move_elements_loop_decreases t ntable slots i))
   =
   let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
@@ -337,7 +338,7 @@ let hashmap_hash_map_insert_fwd_back
 let rec hashmap_hash_map_contains_key_in_list_loop_fwd
   (t : Type0) (key : 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_loop_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
@@ -374,7 +375,8 @@ 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) (key : usize) (ls : hashmap_list_t t) :
-  Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t key ls))
+  Tot (result t)
+  (decreases (hashmap_hash_map_get_in_list_loop_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
@@ -412,7 +414,7 @@ let hashmap_hash_map_get_fwd
 let rec hashmap_hash_map_get_mut_in_list_loop_fwd
   (t : Type0) (ls : hashmap_list_t t) (key : usize) :
   Tot (result t)
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t ls key))
+  (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases t ls key))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
@@ -431,7 +433,7 @@ let hashmap_hash_map_get_mut_in_list_fwd
 let rec hashmap_hash_map_get_mut_in_list_loop_back
   (t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
   Tot (result (hashmap_list_t t))
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t ls key))
+  (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases t ls key))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
@@ -509,7 +511,7 @@ let hashmap_hash_map_get_mut_back
 let rec hashmap_hash_map_remove_from_list_loop_fwd
   (t : Type0) (key : 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_loop_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
@@ -535,7 +537,7 @@ let hashmap_hash_map_remove_from_list_fwd
 let rec hashmap_hash_map_remove_from_list_loop_back
   (t : Type0) (key : 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_loop_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 8cdc6e2c..bc5ed046 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -7,102 +7,106 @@ open Loops.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [loops::sum]: decreases clause *)
-unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
+unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
 
 (** [loops::sum_with_mut_borrows]: decreases clause *)
 unfold
-let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat
+  =
   admit ()
 
 (** [loops::sum_with_shared_borrows]: decreases clause *)
 unfold
-let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
+let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) :
+  nat =
   admit ()
 
 (** [loops::clear]: decreases clause *)
-unfold let clear_decreases (v : vec u32) (i : usize) : nat = admit ()
+unfold let clear_loop_decreases (v : vec u32) (i : usize) : nat = admit ()
 
 (** [loops::list_mem]: decreases clause *)
-unfold let list_mem_decreases (x : u32) (ls : list_t u32) : nat = admit ()
+unfold let list_mem_loop_decreases (x : u32) (ls : list_t u32) : nat = admit ()
 
 (** [loops::list_nth_mut_loop]: decreases clause *)
 unfold
-let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
+let list_nth_mut_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) :
+  nat =
   admit ()
 
 (** [loops::list_nth_shared_loop]: decreases clause *)
 unfold
-let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat
-  =
+let list_nth_shared_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) :
+  nat =
   admit ()
 
 (** [loops::get_elem_mut]: decreases clause *)
 unfold
-let get_elem_mut_decreases (x : usize) (ls : list_t usize) : nat = admit ()
+let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : nat =
+  admit ()
 
 (** [loops::get_elem_shared]: decreases clause *)
 unfold
-let get_elem_shared_decreases (slots : vec (list_t usize)) (x : usize)
+let get_elem_shared_loop_decreases (slots : vec (list_t usize)) (x : usize)
   (ls : list_t usize) (ls0 : list_t usize) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_with_id]: decreases clause *)
 unfold
-let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) :
-  nat =
+let list_nth_mut_loop_with_id_loop_decreases (t : Type0) (i : u32)
+  (ls : list_t t) : nat =
   admit ()
 
 (** [loops::list_nth_shared_loop_with_id]: decreases clause *)
 unfold
-let list_nth_shared_loop_with_id_decreases (t : Type0) (ls : list_t t)
+let list_nth_shared_loop_with_id_loop_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) (ls0 : list_t t)
+let list_nth_mut_loop_pair_loop_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) (ls0 : list_t t)
+let list_nth_shared_loop_pair_loop_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) (ls0 : list_t t)
+let list_nth_mut_loop_pair_merge_loop_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) (ls0 : list_t t)
+let list_nth_shared_loop_pair_merge_loop_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) (ls0 : list_t t)
+let list_nth_mut_shared_loop_pair_loop_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) (ls0 : list_t t)
-  (ls1 : list_t t) (i : u32) : nat =
+let list_nth_mut_shared_loop_pair_merge_loop_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) (ls0 : list_t t)
+let list_nth_shared_mut_loop_pair_loop_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) (ls0 : list_t t)
-  (ls1 : list_t t) (i : u32) : nat =
+let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0)
+  (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index a03f0302..c748da71 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -6,103 +6,103 @@ open Loops.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [loops::sum]: decreases clause *)
-unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat =
+unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
   if i <= max then max - i else 0
 
 (** [loops::sum_with_mut_borrows]: decreases clause *)
 unfold
-let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat =
   if max >= mi then max - mi else 0
 
 (** [loops::sum_with_shared_borrows]: decreases clause *)
 unfold
-let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
+let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
   if max >= i then max - i else 0
 
 (** [loops::clear]: decreases clause *)
-unfold let clear_decreases (v : vec u32) (i : usize) : nat =
+unfold let clear_loop_decreases (v : vec u32) (i : usize) : nat =
   if i <= List.Tot.length v then List.Tot.length v - i else 0
 
 (** [loops::list_mem]: decreases clause *)
-unfold let list_mem_decreases (i : u32) (ls : list_t u32) : list_t u32 =
+unfold let list_mem_loop_decreases (i : u32) (ls : list_t u32) : list_t u32 =
   ls
 
 (** [loops::list_nth_mut_loop]: decreases clause *)
 unfold
-let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
+let list_nth_mut_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
   i
 
 (** [loops::list_nth_shared_loop]: decreases clause *)
 unfold
-let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t =
+let list_nth_shared_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t =
   ls
 
 (** [loops::get_elem_mut]: decreases clause *)
 unfold
-let get_elem_mut_decreases (x : usize) (ls : list_t usize) : list_t usize = ls
+let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : list_t usize = ls
 
 (** [loops::get_elem_shared]: decreases clause *)
 unfold
-let get_elem_shared_decreases (slots : vec (list_t usize)) (x : usize)
+let get_elem_shared_loop_decreases (slots : vec (list_t usize)) (x : usize)
   (ls : list_t usize) (ls0 : list_t usize) : list_t usize =
   ls
 
 (** [loops::list_nth_mut_loop_with_id]: decreases clause *)
 unfold
-let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) :
+let list_nth_mut_loop_with_id_loop_decreases (t : Type0) (i : u32) (ls : list_t t) :
   list_t t =
   ls
 
 (** [loops::list_nth_shared_loop_with_id]: decreases clause *)
 unfold
-let list_nth_shared_loop_with_id_decreases (t : Type0) (l : list_t t)
+let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (l : list_t t)
   (i : u32) (ls : list_t t) : list_t t =
   ls
 
 (** [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)
+let list_nth_mut_loop_pair_loop_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
   (i : u32) : nat =
   i
 
 (** [loops::list_nth_shared_loop_pair]: decreases clause *)
 unfold
-let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+let list_nth_shared_loop_pair_loop_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : list_t t =
   l
 
 (** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
 unfold
-let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+let list_nth_mut_loop_pair_merge_loop_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : nat =
   i
 
 (** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
 unfold
-let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+let list_nth_shared_loop_pair_merge_loop_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : list_t t =
   l
 
 (** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
 unfold
-let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+let list_nth_mut_shared_loop_pair_loop_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : list_t t =
   l
 
 (** [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)
+let list_nth_mut_shared_loop_pair_merge_loop_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : list_t t =
   l
 
 (** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
 unfold
-let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
+let list_nth_shared_mut_loop_pair_loop_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : list_t t =
   l
 
 (** [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)
+let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0) (l : list_t t)
   (l0 : list_t t) (i : u32) : list_t t =
   l
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index e8fb89e9..ebf30654 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -10,7 +10,7 @@ include Loops.Clauses
 (** [loops::sum] *)
 let rec sum_loop_fwd
   (max : u32) (i : u32) (s : u32) :
-  Tot (result u32) (decreases (sum_decreases max i s))
+  Tot (result u32) (decreases (sum_loop_decreases max i s))
   =
   if i < max
   then
@@ -30,7 +30,7 @@ let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0
 (** [loops::sum_with_mut_borrows] *)
 let rec sum_with_mut_borrows_loop_fwd
   (max : u32) (mi : u32) (ms : u32) :
-  Tot (result u32) (decreases (sum_with_mut_borrows_decreases max mi ms))
+  Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms))
   =
   if mi < max
   then
@@ -51,7 +51,7 @@ let sum_with_mut_borrows_fwd (max : u32) : result u32 =
 (** [loops::sum_with_shared_borrows] *)
 let rec sum_with_shared_borrows_loop_fwd
   (max : u32) (i : u32) (s : u32) :
-  Tot (result u32) (decreases (sum_with_shared_borrows_decreases max i s))
+  Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s))
   =
   if i < max
   then
@@ -72,7 +72,7 @@ let sum_with_shared_borrows_fwd (max : u32) : result u32 =
 (** [loops::clear] *)
 let rec clear_loop_fwd_back
   (v : vec u32) (i : usize) :
-  Tot (result (vec u32)) (decreases (clear_decreases v i))
+  Tot (result (vec u32)) (decreases (clear_loop_decreases v i))
   =
   let i0 = vec_len u32 v in
   if i < i0
@@ -93,7 +93,7 @@ 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
   (x : u32) (ls : list_t u32) :
-  Tot (result bool) (decreases (list_mem_decreases x ls))
+  Tot (result bool) (decreases (list_mem_loop_decreases x ls))
   =
   begin match ls with
   | ListCons y tl -> if y = x then Return true else list_mem_loop_fwd x tl
@@ -107,7 +107,7 @@ let list_mem_fwd (x : u32) (ls : list_t u32) : result bool =
 (** [loops::list_nth_mut_loop] *)
 let rec list_nth_mut_loop_loop_fwd
   (t : Type0) (ls : list_t t) (i : u32) :
-  Tot (result t) (decreases (list_nth_mut_loop_decreases t ls i))
+  Tot (result t) (decreases (list_nth_mut_loop_loop_decreases t ls i))
   =
   begin match ls with
   | ListCons x tl ->
@@ -128,7 +128,7 @@ let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
 (** [loops::list_nth_mut_loop] *)
 let rec list_nth_mut_loop_loop_back
   (t : Type0) (ls : list_t t) (i : u32) (ret : t) :
-  Tot (result (list_t t)) (decreases (list_nth_mut_loop_decreases t ls i))
+  Tot (result (list_t t)) (decreases (list_nth_mut_loop_loop_decreases t ls i))
   =
   begin match ls with
   | ListCons x tl ->
@@ -154,7 +154,7 @@ let list_nth_mut_loop_back
 (** [loops::list_nth_shared_loop] *)
 let rec list_nth_shared_loop_loop_fwd
   (t : Type0) (ls : list_t t) (i : u32) :
-  Tot (result t) (decreases (list_nth_shared_loop_decreases t ls i))
+  Tot (result t) (decreases (list_nth_shared_loop_loop_decreases t ls i))
   =
   begin match ls with
   | ListCons x tl ->
@@ -175,7 +175,7 @@ let list_nth_shared_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
 (** [loops::get_elem_mut] *)
 let rec get_elem_mut_loop_fwd
   (x : usize) (ls : list_t usize) :
-  Tot (result usize) (decreases (get_elem_mut_decreases x ls))
+  Tot (result usize) (decreases (get_elem_mut_loop_decreases x ls))
   =
   begin match ls with
   | ListCons y tl -> if y = x then Return y else get_elem_mut_loop_fwd x tl
@@ -192,7 +192,7 @@ let get_elem_mut_fwd (slots : vec (list_t usize)) (x : usize) : result usize =
 (** [loops::get_elem_mut] *)
 let rec get_elem_mut_loop_back
   (x : usize) (ls : list_t usize) (ret : usize) :
-  Tot (result (list_t usize)) (decreases (get_elem_mut_decreases x ls))
+  Tot (result (list_t usize)) (decreases (get_elem_mut_loop_decreases x ls))
   =
   begin match ls with
   | ListCons y tl ->
@@ -224,7 +224,8 @@ let get_elem_mut_back
 let rec get_elem_shared_loop_fwd
   (slots : vec (list_t usize)) (x : usize) (ls : list_t usize)
   (ls0 : list_t usize) :
-  Tot (result usize) (decreases (get_elem_shared_decreases slots x ls ls0))
+  Tot (result usize)
+  (decreases (get_elem_shared_loop_decreases slots x ls ls0))
   =
   begin match ls with
   | ListCons y tl ->
@@ -254,7 +255,7 @@ let id_shared_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls
 (** [loops::list_nth_mut_loop_with_id] *)
 let rec list_nth_mut_loop_with_id_loop_fwd
   (t : Type0) (i : u32) (ls : list_t t) :
-  Tot (result t) (decreases (list_nth_mut_loop_with_id_decreases t i ls))
+  Tot (result t) (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls))
   =
   begin match ls with
   | ListCons x tl ->
@@ -280,7 +281,7 @@ let list_nth_mut_loop_with_id_fwd
 let rec list_nth_mut_loop_with_id_loop_back
   (t : Type0) (i : u32) (ls : list_t t) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_loop_with_id_decreases t i ls))
+  (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls))
   =
   begin match ls with
   | ListCons x tl ->
@@ -314,7 +315,7 @@ let list_nth_mut_loop_with_id_back
 let rec list_nth_shared_loop_with_id_loop_fwd
   (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))
+  (decreases (list_nth_shared_loop_with_id_loop_decreases t ls i ls0))
   =
   begin match ls0 with
   | ListCons x tl ->
@@ -340,7 +341,7 @@ let list_nth_shared_loop_with_id_fwd
 let rec list_nth_mut_loop_pair_loop_fwd
   (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))
+  (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -367,7 +368,7 @@ let list_nth_mut_loop_pair_fwd
 let rec list_nth_mut_loop_pair_loop_back'a
   (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 ls0 ls1 i))
+  (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -400,7 +401,7 @@ let list_nth_mut_loop_pair_back'a
 let rec list_nth_mut_loop_pair_loop_back'b
   (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 ls0 ls1 i))
+  (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -433,7 +434,7 @@ let list_nth_mut_loop_pair_back'b
 let rec list_nth_shared_loop_pair_loop_fwd
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_loop_pair_decreases t ls0 ls1 i))
+  (decreases (list_nth_shared_loop_pair_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -460,7 +461,7 @@ let list_nth_shared_loop_pair_fwd
 let rec list_nth_mut_loop_pair_merge_loop_fwd
   (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 ls0 ls1 i))
+  (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -487,7 +488,7 @@ let list_nth_mut_loop_pair_merge_fwd
 let rec list_nth_mut_loop_pair_merge_loop_back
   (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 ls0 ls1 i))
+  (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -521,7 +522,7 @@ let list_nth_mut_loop_pair_merge_back
 let rec list_nth_shared_loop_pair_merge_loop_fwd
   (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 ls0 ls1 i))
+  (decreases (list_nth_shared_loop_pair_merge_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -548,7 +549,7 @@ let list_nth_shared_loop_pair_merge_fwd
 let rec list_nth_mut_shared_loop_pair_loop_fwd
   (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 ls0 ls1 i))
+  (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -575,7 +576,7 @@ let list_nth_mut_shared_loop_pair_fwd
 let rec list_nth_mut_shared_loop_pair_loop_back
   (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 ls0 ls1 i))
+  (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -609,7 +610,7 @@ let list_nth_mut_shared_loop_pair_back
 let rec list_nth_mut_shared_loop_pair_merge_loop_fwd
   (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 ls0 ls1 i))
+  (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -637,7 +638,7 @@ let list_nth_mut_shared_loop_pair_merge_fwd
 let rec list_nth_mut_shared_loop_pair_merge_loop_back
   (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 ls0 ls1 i))
+  (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -671,7 +672,7 @@ let list_nth_mut_shared_loop_pair_merge_back
 let rec list_nth_shared_mut_loop_pair_loop_fwd
   (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 ls0 ls1 i))
+  (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -698,7 +699,7 @@ let list_nth_shared_mut_loop_pair_fwd
 let rec list_nth_shared_mut_loop_pair_loop_back
   (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 ls0 ls1 i))
+  (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -732,7 +733,7 @@ let list_nth_shared_mut_loop_pair_back
 let rec list_nth_shared_mut_loop_pair_merge_loop_fwd
   (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 ls0 ls1 i))
+  (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->
@@ -760,7 +761,7 @@ let list_nth_shared_mut_loop_pair_merge_fwd
 let rec list_nth_shared_mut_loop_pair_merge_loop_back
   (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 ls0 ls1 i))
+  (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i))
   =
   begin match ls0 with
   | ListCons x0 tl0 ->