9 files changed, 37 insertions, 62 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 0d55b171..f1af0c21 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -55,8 +55,8 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
   hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize)
 .
 
-(** [hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hash_map_clear_slots_loop_fwd_back
+(** [hashmap::HashMap::{0}::clear] *)
+Fixpoint hash_map_clear_loop_fwd_back
   (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
   result (vec (List_t T))
   :=
@@ -68,21 +68,15 @@ Fixpoint hash_map_clear_slots_loop_fwd_back
     then (
       i1 <- usize_add i 1%usize;
       slots0 <- vec_index_mut_back (List_t T) slots i ListNil;
-      hash_map_clear_slots_loop_fwd_back T n0 slots0 i1)
+      hash_map_clear_loop_fwd_back T n0 slots0 i1)
     else Return slots
   end
 .
 
-(** [hashmap::HashMap::{0}::clear_slots] *)
-Definition hash_map_clear_slots_fwd_back
-  (T : Type) (n : nat) (slots : vec (List_t T)) : result (vec (List_t T)) :=
-  hash_map_clear_slots_loop_fwd_back T n slots (0%usize)
-.
-
 (** [hashmap::HashMap::{0}::clear] *)
 Definition hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
-  v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots);
+  v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) (0%usize);
   Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor)
     self.(Hash_map_max_load) v)
 .
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 670e527a..7c86dbe1 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -58,8 +58,8 @@ Definition hashmap_hash_map_new_fwd
   hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize)
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back
+(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+Fixpoint hashmap_hash_map_clear_loop_fwd_back
   (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
   result (vec (Hashmap_list_t T))
   :=
@@ -71,25 +71,19 @@ Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back
     then (
       i1 <- usize_add i 1%usize;
       slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
-      hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots0 i1)
+      hashmap_hash_map_clear_loop_fwd_back T n0 slots0 i1)
     else Return slots
   end
 .
 
-(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-Definition hashmap_hash_map_clear_slots_fwd_back
-  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) :
-  result (vec (Hashmap_list_t T))
-  :=
-  hashmap_hash_map_clear_slots_loop_fwd_back T n slots (0%usize)
-.
-
 (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
 Definition hashmap_hash_map_clear_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
   result (Hashmap_hash_map_t T)
   :=
-  v <- hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots);
+  v <-
+    hashmap_hash_map_clear_loop_fwd_back T n self.(Hashmap_hash_map_slots)
+      (0%usize);
   Return (mkHashmap_hash_map_t (0%usize)
     self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v)
 .
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index 4e490b6c..aef5e25e 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -12,9 +12,9 @@ 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 *)
+(** [hashmap::HashMap::{0}::clear]: decreases clause *)
 unfold
-let hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (list_t t))
+let hash_map_clear_loop_decreases (t : Type0) (slots : vec (list_t t))
   (i : usize) : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.fst b/tests/fstar/hashmap/Hashmap.Clauses.fst
index b525880a..d8bb8d20 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.fst
@@ -11,9 +11,9 @@ unfold
 let hash_map_allocate_slots_loop_decreases (t : Type0) (slots : vec (list_t t))
   (n : usize) : nat = n
 
-(** [hashmap::HashMap::clear_slots]: decreases clause *)
+(** [hashmap::HashMap::clear]: decreases clause *)
 unfold
-let hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (list_t t))
+let hash_map_clear_loop_decreases (t : Type0) (slots : vec (list_t t))
   (i : usize) : nat =
   if i < length slots then length slots - i else 0
 
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 7137e92a..68bda221 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -58,11 +58,11 @@ let hash_map_new_with_capacity_fwd
 let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
   hash_map_new_with_capacity_fwd t 32 4 5
 
-(** [hashmap::HashMap::{0}::clear_slots] *)
-let rec hash_map_clear_slots_loop_fwd_back
+(** [hashmap::HashMap::{0}::clear] *)
+let rec hash_map_clear_loop_fwd_back
   (t : Type0) (slots : vec (list_t t)) (i : usize) :
   Tot (result (vec (list_t t)))
-  (decreases (hash_map_clear_slots_loop_decreases t slots i))
+  (decreases (hash_map_clear_loop_decreases t slots i))
   =
   let i0 = vec_len (list_t t) slots in
   if i < i0
@@ -72,20 +72,15 @@ let rec hash_map_clear_slots_loop_fwd_back
     | Return i1 ->
       begin match vec_index_mut_back (list_t t) slots i ListNil with
       | Fail e -> Fail e
-      | Return slots0 -> hash_map_clear_slots_loop_fwd_back t slots0 i1
+      | Return slots0 -> hash_map_clear_loop_fwd_back t slots0 i1
       end
     end
   else Return slots
 
-(** [hashmap::HashMap::{0}::clear_slots] *)
-let hash_map_clear_slots_fwd_back
-  (t : Type0) (slots : vec (list_t t)) : result (vec (list_t t)) =
-  hash_map_clear_slots_loop_fwd_back t slots 0
-
 (** [hashmap::HashMap::{0}::clear] *)
 let hash_map_clear_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
-  begin match hash_map_clear_slots_fwd_back t self.hash_map_slots with
+  begin match hash_map_clear_loop_fwd_back t self.hash_map_slots 0 with
   | Fail e -> Fail e
   | Return v ->
     Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index b1352443..49d96cd5 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -617,14 +617,14 @@ let hash_map_new_fwd_lem_aux t =
 /// The lemma we reveal in the .fsti
 let hash_map_new_fwd_lem t = hash_map_new_fwd_lem_aux t
 
-(*** clear_slots *)
-/// [clear_slots] doesn't fail and simply clears the slots starting at index i
+(*** clear *)
+/// [clear]: the loop doesn't fail and simply clears the slots starting at index i
 #push-options "--fuel 1"
-let rec hash_map_clear_slots_loop_fwd_back_lem
+let rec hash_map_clear_loop_fwd_back_lem
   (t : Type0) (slots : vec (list_t t)) (i : usize) :
   Lemma
   (ensures (
-    match hash_map_clear_slots_loop_fwd_back t slots i with
+    match hash_map_clear_loop_fwd_back t slots i with
     | Fail _ -> False
     | Return slots' ->
       // The length is preserved
@@ -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_loop_decreases t slots i))
+  (decreases (hash_map_clear_loop_decreases t slots i))
   =
   let i0 = vec_len (list_t t) slots in
   let b = i < i0 in
@@ -645,8 +645,8 @@ let rec hash_map_clear_slots_loop_fwd_back_lem
       begin match usize_add i 1 with
       | Fail _ -> ()
       | Return i1 ->
-        hash_map_clear_slots_loop_fwd_back_lem t v i1;
-        begin match hash_map_clear_slots_loop_fwd_back t v i1 with
+        hash_map_clear_loop_fwd_back_lem t v i1;
+        begin match hash_map_clear_loop_fwd_back t v i1 with
         | Fail _ -> ()
         | Return slots1 ->
           assert(length slots1 == length slots);
@@ -658,7 +658,6 @@ let rec hash_map_clear_slots_loop_fwd_back_lem
   else ()
 #pop-options
 
-(*** clear *)
 /// [clear] doesn't fail and turns the hash map into an empty map
 val hash_map_clear_fwd_back_lem_aux
   (#t : Type0) (self : hash_map_t t) :
@@ -683,8 +682,8 @@ let hash_map_clear_fwd_back_lem_aux #t self =
   let p = self.hash_map_max_load_factor in
   let i = self.hash_map_max_load in
   let v = self.hash_map_slots in
-  hash_map_clear_slots_loop_fwd_back_lem t v 0;
-  begin match hash_map_clear_slots_loop_fwd_back t v 0 with
+  hash_map_clear_loop_fwd_back_lem t v 0;
+  begin match hash_map_clear_loop_fwd_back t v 0 with
   | Fail _ -> ()
   | Return slots1 ->
     slots_t_al_v_all_nil_is_empty_lem slots1;
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index f3afa008..1e15d1f9 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -12,9 +12,9 @@ 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 *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: decreases clause *)
 unfold
-let hashmap_hash_map_clear_slots_loop_decreases (t : Type0)
+let hashmap_hash_map_clear_loop_decreases (t : Type0)
   (slots : vec (hashmap_list_t t)) (i : usize) : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
index 2f6a0acc..699ff3b2 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
@@ -11,9 +11,9 @@ unfold
 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 *)
+(** [hashmap::HashMap::clear]: decreases clause *)
 unfold
-let hashmap_hash_map_clear_slots_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t))
+let hashmap_hash_map_clear_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t))
   (i : usize) : nat =
   if i < length slots then length slots - i else 0
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index f3b480c3..56cff453 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -62,11 +62,11 @@ let hashmap_hash_map_new_with_capacity_fwd
 let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
   hashmap_hash_map_new_with_capacity_fwd t 32 4 5
 
-(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-let rec hashmap_hash_map_clear_slots_loop_fwd_back
+(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+let rec hashmap_hash_map_clear_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_loop_decreases t slots i))
+  (decreases (hashmap_hash_map_clear_loop_decreases t slots i))
   =
   let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
@@ -77,23 +77,16 @@ let rec hashmap_hash_map_clear_slots_loop_fwd_back
       begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
         with
       | Fail e -> Fail e
-      | Return slots0 -> hashmap_hash_map_clear_slots_loop_fwd_back t slots0 i1
+      | Return slots0 -> hashmap_hash_map_clear_loop_fwd_back t slots0 i1
       end
     end
   else Return slots
 
-(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-let hashmap_hash_map_clear_slots_fwd_back
-  (t : Type0) (slots : vec (hashmap_list_t t)) :
-  result (vec (hashmap_list_t t))
-  =
-  hashmap_hash_map_clear_slots_loop_fwd_back t slots 0
-
 (** [hashmap_main::hashmap::HashMap::{0}::clear] *)
 let hashmap_hash_map_clear_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
   begin match
-    hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots with
+    hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 with
   | Fail e -> Fail e
   | Return v ->
     Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor