Fix an issue with the names of the loop decreases clauses

4 files changed, 40 insertions, 40 deletions

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