Update the hashmap and regenerate

4 files changed, 18 insertions, 24 deletions

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;