Do more cleaning

1 files changed, 141 insertions, 147 deletions

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index d280d537..a6becc96 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -445,6 +445,7 @@ let slot_t_v #t = list_t_v #t
 let slots_t_v (#t : Type0) (slots : slots_t t) : slots_s t =
   map slot_t_v slots
 
+/// Representation function for the slots, seen as an associative list.
 let slots_t_al_v (#t : Type0) (slots : slots_t t) : assoc_list t =
   flatten (map list_t_v slots)
 
@@ -452,21 +453,18 @@ let slots_t_al_v (#t : Type0) (slots : slots_t t) : assoc_list t =
 /// list per slot). This is the representation we use most, internally. Note that
 /// we later introduce a [map_s] representation, which is the one used in the
 /// lemmas shown to the user.
-type hash_map_slots_s t = list (slot_s t)
-
-/// High-level type for the hash-map, seen as a an associative list
-type hash_map_s t = assoc_list t
+type hash_map_s t = list (slot_s t)
 
 // 'nes': "non-empty slots"
-type hash_map_slots_s_nes (t : Type0) : Type0 =
-  hm:hash_map_slots_s t{is_pos_usize (length hm)}
+type hash_map_s_nes (t : Type0) : Type0 =
+  hm:hash_map_s t{is_pos_usize (length hm)}
 
 /// Representation function for [hash_map_t] as a list of slots
-let hash_map_t_v (#t : Type0) (hm : hash_map_t t) : hash_map_slots_s t =
+let hash_map_t_v (#t : Type0) (hm : hash_map_t t) : hash_map_s t =
   map list_t_v hm.hash_map_slots
 
 /// Representation function for [hash_map_t] as an associative list
-let hash_map_t_al_v (#t : Type0) (hm : hash_map_t t) : hash_map_s t =
+let hash_map_t_al_v (#t : Type0) (hm : hash_map_t t) : assoc_list t =
   flatten (hash_map_t_v hm)
 
 // 'nes': "non-empty slots"
@@ -491,36 +489,34 @@ let binding_neq (#t : Type0) (b0 b1 : binding t) : bool = fst b0 <> fst b1
 let hash_map_t_len_s (#t : Type0) (hm : hash_map_t t) : nat =
   hm.hash_map_num_entries
 
-let slot_s_find (#t : Type0) (k : key) (slot : list (binding t)) : option t =
+let assoc_list_find (#t : Type0) (k : key) (slot : assoc_list t) : option t =
   match find (same_key k) slot with
   | None -> None
   | Some (_, v) -> Some v
 
-let assoc_list_find (#t : Type0) (k : key) (slot : assoc_list t) : option t =
-  slot_s_find k slot
+let slot_s_find (#t : Type0) (k : key) (slot : list (binding t)) : option t =
+  assoc_list_find k slot
 
 let slot_t_find_s (#t : Type0) (k : key) (slot : list_t t) : option t =
-  match find (same_key k) (list_t_v slot) with
-  | None -> None
-  | Some (_, v) -> Some v
+  slot_s_find k (slot_t_v slot)
 
 // This is a simpler version of the "find" function, which captures the essence
-// of what happens and operates on [hash_map_slots_s].
-let hash_map_slots_s_find
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+// of what happens and operates on [hash_map_s].
+let hash_map_s_find
+  (#t : Type0) (hm : hash_map_s_nes t)
   (k : key) : option t =
   let i = hash_mod_key k (length hm) in
   let slot = index hm i in
   slot_s_find k slot
 
-let hash_map_slots_s_len
-  (#t : Type0) (hm : hash_map_slots_s_nes t) :
+let hash_map_s_len
+  (#t : Type0) (hm : hash_map_s_nes t) :
   nat =
   length (flatten hm)
 
 // Same as above, but operates on [hash_map_t]
 // Note that we don't reuse the above function on purpose: converting to a
-// [hash_map_slots_s] then looking up an element is not the same as what we
+// [hash_map_s] then looking up an element is not the same as what we
 // wrote below.
 let hash_map_t_find_s
   (#t : Type0) (hm : hash_map_t t{length hm.hash_map_slots > 0}) (k : key) : option t =
@@ -539,22 +535,20 @@ let slot_s_inv
   pairwise_rel binding_neq slot
 
 let slot_t_inv (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t) : bool =
-  // All the bindings are in the proper slot
-  for_all (same_hash_mod_key len i) (list_t_v slot) &&
-  // All the keys are pairwise distinct
-  pairwise_rel binding_neq (list_t_v slot)
+  slot_s_inv len i (slot_t_v slot)
 
 let slots_s_inv (#t : Type0) (slots : slots_s t{length slots <= usize_max}) : Type0 =
   forall(i:nat{i < length slots}).
   {:pattern index slots i}
   slot_s_inv (length slots) i (index slots i)
 
+// TODO: write that in terms of slots_s_inv
 let slots_t_inv (#t : Type0) (slots : slots_t t{length slots <= usize_max}) : Type0 =
   forall(i:nat{i < length slots}).
   {:pattern index slots i}
   slot_t_inv (length slots) i (index slots i)
 
-let hash_map_slots_s_inv (#t : Type0) (hm : hash_map_slots_s t) : Type0 =
+let hash_map_s_inv (#t : Type0) (hm : hash_map_s t) : Type0 =
   length hm <= usize_max /\
   length hm > 0 /\
   slots_s_inv hm
@@ -1254,14 +1248,14 @@ let hash_map_insert_in_list_back_lem t len key value ls =
 (**** Refinement proof *)
 /// Same strategy as for [insert_in_list]: we introduce a high-level version of
 /// the function, and reason about it.
-/// We work on [hash_map_slots_s] (we use a higher-level view of the hash-map, but
+/// We work on [hash_map_s] (we use a higher-level view of the hash-map, but
 /// not too high).
 
 /// A high-level version of insert, which doesn't check if the table is saturated
 let hash_map_insert_no_fail_s
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+  (#t : Type0) (hm : hash_map_s_nes t)
   (key : usize) (value : t) :
-  hash_map_slots_s t =
+  hash_map_s t =
   let len = length hm in
   let i = hash_mod_key key len in
   let slot = index hm i in
@@ -1269,14 +1263,14 @@ let hash_map_insert_no_fail_s
   let hm' = list_update hm i slot' in
   hm'
 
-// TODO: at some point I used hash_map_slots_s_nes and it broke proofs...x
+// TODO: at some point I used hash_map_s_nes and it broke proofs...x
 let hash_map_insert_no_resize_s
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+  (#t : Type0) (hm : hash_map_s_nes t)
   (key : usize) (value : t) :
-  result (hash_map_slots_s t) =
+  result (hash_map_s t) =
   // Check if the table is saturated (too many entries, and we need to insert one)
   let num_entries = length (flatten hm) in
-  if None? (hash_map_slots_s_find hm key) && num_entries = usize_max then Fail
+  if None? (hash_map_s_find hm key) && num_entries = usize_max then Fail
   else Return (hash_map_insert_no_fail_s hm key value)
 
 /// Prove that [hash_map_insert_no_resize_s] is refined by
@@ -1286,7 +1280,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
   Lemma
   (requires (
     hash_map_t_base_inv self /\
-    hash_map_slots_s_len (hash_map_t_v self) = hash_map_t_len_s self))
+    hash_map_s_len (hash_map_t_v self) = hash_map_t_len_s self))
   (ensures (
     begin
     match hash_map_insert_no_resize_fwd_back t self key value,
@@ -1297,7 +1291,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
       hash_map_t_base_inv hm /\
       hash_map_same_params hm self /\
       hash_map_t_v hm == hm_v /\
-      hash_map_slots_s_len hm_v == hash_map_t_len_s hm
+      hash_map_s_len hm_v == hash_map_t_len_s hm
     | _ -> False
     end))
 
@@ -1345,7 +1339,7 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
                   assert_norm(length [(key,value)] = 1);
                   assert(length (list_t_v l0) = length (list_t_v l) + 1);
                   length_flatten_update self_v hash_mod (list_t_v l0);
-                  assert(hash_map_slots_s_len hm_v = hash_map_t_len_s hm)
+                  assert(hash_map_s_len hm_v = hash_map_t_len_s hm)
                 end
               end
             end
@@ -1363,7 +1357,7 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
                 assert(hm_v == list_update self_v hash_mod (list_t_v l0));
                 assert(length (list_t_v l0) = length (list_t_v l));
                 length_flatten_update self_v hash_mod (list_t_v l0);
-                assert(hash_map_slots_s_len hm_v = hash_map_t_len_s hm)
+                assert(hash_map_s_len hm_v = hash_map_t_len_s hm)
               end
             end
         end
@@ -1373,30 +1367,30 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
 
 (**** insert_{no_fail,no_resize}: invariants *)
 
-let hash_map_slots_s_updated_binding
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
-  (key : usize) (opt_value : option t) (hm' : hash_map_slots_s_nes t) : Type0 =
+let hash_map_s_updated_binding
+  (#t : Type0) (hm : hash_map_s_nes t)
+  (key : usize) (opt_value : option t) (hm' : hash_map_s_nes t) : Type0 =
   // [key] maps to [value]
-  hash_map_slots_s_find hm' key == opt_value /\
+  hash_map_s_find hm' key == opt_value /\
   // The other bindings are preserved
-  (forall k'. k' <> key ==> hash_map_slots_s_find hm' k' == hash_map_slots_s_find hm k')
+  (forall k'. k' <> key ==> hash_map_s_find hm' k' == hash_map_s_find hm k')
 
-let insert_post (#t : Type0) (hm : hash_map_slots_s_nes t)
-  (key : usize) (value : t) (hm' : hash_map_slots_s_nes t) : Type0 =
+let insert_post (#t : Type0) (hm : hash_map_s_nes t)
+  (key : usize) (value : t) (hm' : hash_map_s_nes t) : Type0 =
   // The invariant is preserved
-  hash_map_slots_s_inv hm' /\
+  hash_map_s_inv hm' /\
   // [key] maps to [value] and the other bindings are preserved
-  hash_map_slots_s_updated_binding hm key (Some value) hm' /\
+  hash_map_s_updated_binding hm key (Some value) hm' /\
   // The length is incremented, iff we inserted a new key
-  (match hash_map_slots_s_find hm key with
-   | None -> hash_map_slots_s_len hm' = hash_map_slots_s_len hm + 1
-   | Some _ -> hash_map_slots_s_len hm' = hash_map_slots_s_len hm)
+  (match hash_map_s_find hm key with
+   | None -> hash_map_s_len hm' = hash_map_s_len hm + 1
+   | Some _ -> hash_map_s_len hm' = hash_map_s_len hm)
 
 val hash_map_insert_no_fail_s_lem
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+  (#t : Type0) (hm : hash_map_s_nes t)
   (key : usize) (value : t) :
   Lemma
-  (requires (hash_map_slots_s_inv hm))
+  (requires (hash_map_s_inv hm))
   (ensures (
     let hm' = hash_map_insert_no_fail_s hm key value in
     insert_post hm key value hm'))
@@ -1410,23 +1404,23 @@ let hash_map_insert_no_fail_s_lem #t hm key value =
   length_flatten_update hm i slot'
 
 val hash_map_insert_no_resize_s_lem
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+  (#t : Type0) (hm : hash_map_s_nes t)
   (key : usize) (value : t) :
   Lemma
-  (requires (hash_map_slots_s_inv hm))
+  (requires (hash_map_s_inv hm))
   (ensures (
     match hash_map_insert_no_resize_s hm key value with
     | Fail ->
       // Can fail only if we need to create a new binding in
       // an already saturated map
-      hash_map_slots_s_len hm = usize_max /\
-      None? (hash_map_slots_s_find hm key)
+      hash_map_s_len hm = usize_max /\
+      None? (hash_map_s_find hm key)
     | Return hm' ->
       insert_post hm key value hm'))
 
 let hash_map_insert_no_resize_s_lem #t hm key value =
   let num_entries = length (flatten hm) in
-  if None? (hash_map_slots_s_find hm key) && num_entries = usize_max then ()
+  if None? (hash_map_s_find hm key) && num_entries = usize_max then ()
   else hash_map_insert_no_fail_s_lem hm key value
 
 
@@ -1434,18 +1428,18 @@ let hash_map_insert_no_resize_s_lem #t hm key value =
 /// Lemmas about what happens if we call [find] after an insertion
 
 val hash_map_insert_no_resize_s_get_same_lem
-  (#t : Type0) (hm : hash_map_slots_s t)
+  (#t : Type0) (hm : hash_map_s t)
   (key : usize) (value : t) :
-  Lemma (requires (hash_map_slots_s_inv hm))
+  Lemma (requires (hash_map_s_inv hm))
   (ensures (
     match hash_map_insert_no_resize_s hm key value with
     | Fail -> True
     | Return hm' ->
-      hash_map_slots_s_find hm' key == Some value))
+      hash_map_s_find hm' key == Some value))
 
 let hash_map_insert_no_resize_s_get_same_lem #t hm key value =
   let num_entries = length (flatten hm) in
-  if None? (hash_map_slots_s_find hm key) && num_entries = usize_max then ()
+  if None? (hash_map_s_find hm key) && num_entries = usize_max then ()
   else
     begin
     let hm' = Return?.v (hash_map_insert_no_resize_s hm key value) in
@@ -1456,18 +1450,18 @@ let hash_map_insert_no_resize_s_get_same_lem #t hm key value =
    end
 
 val hash_map_insert_no_resize_s_get_diff_lem
-  (#t : Type0) (hm : hash_map_slots_s t)
+  (#t : Type0) (hm : hash_map_s t)
   (key : usize) (value : t) (key' : usize{key' <> key}) :
-  Lemma (requires (hash_map_slots_s_inv hm))
+  Lemma (requires (hash_map_s_inv hm))
   (ensures (
     match hash_map_insert_no_resize_s hm key value with
     | Fail -> True
     | Return hm' ->
-      hash_map_slots_s_find hm' key' == hash_map_slots_s_find hm key'))
+      hash_map_s_find hm' key' == hash_map_s_find hm key'))
 
 let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
   let num_entries = length (flatten hm) in
-  if None? (hash_map_slots_s_find hm key) && num_entries = usize_max then ()
+  if None? (hash_map_s_find hm key) && num_entries = usize_max then ()
   else
     begin
     let hm' = Return?.v (hash_map_insert_no_resize_s hm key value) in
@@ -1486,24 +1480,24 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
 
 (*** move_elements_from_list *)
 
-/// Having a great time here: if we use `result (hash_map_slots_s_res t)` as the
+/// Having a great time here: if we use `result (hash_map_s_res t)` as the
 /// return type for [hash_map_move_elements_from_list_s] instead of having this
 /// awkward match, the proof of [hash_map_move_elements_fwd_back_lem_refin] fails.
 /// I guess it comes from F*'s poor subtyping.
-/// Followingly, I'm not taking any chance and using [result_hash_map_slots_s]
+/// Followingly, I'm not taking any chance and using [result_hash_map_s]
 /// everywhere.
-type result_hash_map_slots_s_nes (t : Type0) : Type0 =
-  res:result (hash_map_slots_s t) {
+type result_hash_map_s_nes (t : Type0) : Type0 =
+  res:result (hash_map_s t) {
     match res with
     | Fail -> True
     | Return hm -> is_pos_usize (length hm)
   }
 
 let rec hash_map_move_elements_from_list_s
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+  (#t : Type0) (hm : hash_map_s_nes t)
   (ls : slot_s t) :
-  // Do *NOT* use `result (hash_map_slots_s t)`
-  Tot (result_hash_map_slots_s_nes t)
+  // Do *NOT* use `result (hash_map_s t)`
+  Tot (result_hash_map_s_nes t)
   (decreases ls) =
   match ls with
   | [] -> Return hm
@@ -1609,9 +1603,9 @@ let rec hash_map_move_elements_s_simpl
 // only the new hash map in which we moved the elements from the slots):
 // this returned value is not used.
 let rec hash_map_move_elements_s
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+  (#t : Type0) (hm : hash_map_s_nes t)
   (slots : slots_s t) (i : usize{i <= length slots /\ length slots <= usize_max}) :
-  Tot (result_hash_map_slots_s_nes t)
+  Tot (result_hash_map_s_nes t)
   (decreases (length slots - i)) =
   let len = length slots in
   if i < len then
@@ -1645,7 +1639,7 @@ val hash_map_move_elements_fwd_back_lem_refin
 
 // This proof was super unstable for some reasons.
 // 
-// For instance, using the [hash_map_slots_s_nes] type abbreviation
+// For instance, using the [hash_map_s_nes] type abbreviation
 // in some of the above definitions led to a failure (while it was just a type
 // abbreviation: the signatures were the same if we unfolded this type). This
 // behaviour led me to the hypothesis that maybe it made F*'s type inference
@@ -1740,9 +1734,9 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
 ///         as a "flat" associative list (and not a list of lists)
 /// This is actually exactly [hash_map_move_elements_from_list_s]...
 let rec hash_map_move_elements_s_flat
-  (#t : Type0) (ntable : hash_map_slots_s_nes t)
-  (slots : hash_map_s t) :
-  Tot (result_hash_map_slots_s_nes t)
+  (#t : Type0) (ntable : hash_map_s_nes t)
+  (slots : assoc_list t) :
+  Tot (result_hash_map_s_nes t)
   (decreases slots) =
   match slots with
   | [] -> Return ntable
@@ -1835,7 +1829,7 @@ let rec flatten_nil_prefix_as_flatten_i #a l i =
 /// The proof is trivial, the functions are the same.
 /// Just keeping two definitions to allow changes...
 val hash_map_move_elements_from_list_s_as_flat_lem
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+  (#t : Type0) (hm : hash_map_s_nes t)
   (ls : slot_s t) :
   Lemma
   (ensures (
@@ -1856,8 +1850,8 @@ let rec hash_map_move_elements_from_list_s_as_flat_lem #t hm ls =
 
 /// Composition of two calls to [hash_map_move_elements_s_flat]
 let hash_map_move_elements_s_flat_comp
-  (#t : Type0) (hm : hash_map_slots_s_nes t) (slot0 slot1 : slot_s t) :
-  Tot (result_hash_map_slots_s_nes t) =
+  (#t : Type0) (hm : hash_map_s_nes t) (slot0 slot1 : slot_s t) :
+  Tot (result_hash_map_s_nes t) =
   match hash_map_move_elements_s_flat hm slot0 with
   | Fail -> Fail
   | Return hm1 -> hash_map_move_elements_s_flat hm1 slot1
@@ -1865,7 +1859,7 @@ let hash_map_move_elements_s_flat_comp
 /// High-level desc:
 /// move_elements (move_elements hm slot0) slo1 == move_elements hm (slot0 @ slot1)
 val hash_map_move_elements_s_flat_append_lem
-  (#t : Type0) (hm : hash_map_slots_s_nes t) (slot0 slot1 : slot_s t) :
+  (#t : Type0) (hm : hash_map_s_nes t) (slot0 slot1 : slot_s t) :
   Lemma
   (ensures (
     match hash_map_move_elements_s_flat_comp hm slot0 slot1,
@@ -1907,7 +1901,7 @@ let rec flatten_i_same_suffix #a l0 l1 i =
 /// [hash_map_move_elements_s] refines [hash_map_move_elements_s_flat]
 /// (actually the functions are equal on all inputs).
 val hash_map_move_elements_s_lem_refin_flat
-  (#t : Type0) (hm : hash_map_slots_s_nes t)
+  (#t : Type0) (hm : hash_map_s_nes t)
   (slots : slots_s t)
   (i : nat{i <= length slots /\ length slots <= usize_max}) :
   Lemma
@@ -1947,21 +1941,21 @@ let assoc_list_inv (#t : Type0) (al : assoc_list t) : Type0 =
   pairwise_rel binding_neq al
 
 let disjoint_hm_al_on_key
-  (#t : Type0) (hm : hash_map_slots_s_nes t) (al : assoc_list t) (k : key) : Type0 =
-  match hash_map_slots_s_find hm k, assoc_list_find k al with
+  (#t : Type0) (hm : hash_map_s_nes t) (al : assoc_list t) (k : key) : Type0 =
+  match hash_map_s_find hm k, assoc_list_find k al with
   | Some _, None
   | None, Some _
   | None, None -> True
   | Some _, Some _ -> False
 
 /// Playing a dangerous game here: using forall quantifiers
-let disjoint_hm_al (#t : Type0) (hm : hash_map_slots_s_nes t) (al : assoc_list t) : Type0 =
+let disjoint_hm_al (#t : Type0) (hm : hash_map_s_nes t) (al : assoc_list t) : Type0 =
   forall (k:key). disjoint_hm_al_on_key hm al k
 
 let find_in_union_hm_al
-  (#t : Type0) (hm : hash_map_slots_s_nes t) (al : assoc_list t) (k : key) :
+  (#t : Type0) (hm : hash_map_s_nes t) (al : assoc_list t) (k : key) :
   option t =
-  match hash_map_slots_s_find hm k with
+  match hash_map_s_find hm k with
   | Some b -> Some b
   | None -> assoc_list_find k al
 
@@ -1978,25 +1972,25 @@ let rec for_all_binding_neq_find_lem #t k v al =
 #pop-options
 
 val hash_map_move_elements_s_flat_lem
-  (#t : Type0) (hm : hash_map_slots_s_nes t) (al : assoc_list t) :
+  (#t : Type0) (hm : hash_map_s_nes t) (al : assoc_list t) :
   Lemma
   (requires (
     // Invariants
-    hash_map_slots_s_inv hm /\
+    hash_map_s_inv hm /\
     assoc_list_inv al /\
     // The two are disjoint
     disjoint_hm_al hm al /\
     // We can add all the elements to the hashmap
-    hash_map_slots_s_len hm + length al <= usize_max))
+    hash_map_s_len hm + length al <= usize_max))
   (ensures (
     match hash_map_move_elements_s_flat hm al with
     | Fail -> False // We can't fail
     | Return hm' ->
       // The invariant is preserved
-      hash_map_slots_s_inv hm' /\
+      hash_map_s_inv hm' /\
       // The new hash map is the union of the two maps
-      (forall (k:key). hash_map_slots_s_find hm' k == find_in_union_hm_al hm al k) /\
-      hash_map_slots_s_len hm' = hash_map_slots_s_len hm + length al))
+      (forall (k:key). hash_map_s_find hm' k == find_in_union_hm_al hm al k) /\
+      hash_map_s_len hm' = hash_map_s_len hm + length al))
   (decreases al)
 
 #restart-solver
@@ -2009,25 +2003,25 @@ let rec hash_map_move_elements_s_flat_lem #t hm al =
     match hash_map_insert_no_resize_s hm k v with
     | Fail -> ()
     | Return hm' ->
-      assert(hash_map_slots_s_inv hm');
+      assert(hash_map_s_inv hm');
       assert(assoc_list_inv al');
       let disjoint_lem (k' : key) :
         Lemma (disjoint_hm_al_on_key hm' al' k')
         [SMTPat (disjoint_hm_al_on_key hm' al' k')] =
         if k' = k then
           begin
-          assert(hash_map_slots_s_find hm' k' == Some v);
+          assert(hash_map_s_find hm' k' == Some v);
           for_all_binding_neq_find_lem k v al';
           assert(assoc_list_find k' al' == None)
           end
         else
           begin
-          assert(hash_map_slots_s_find hm' k' == hash_map_slots_s_find hm k');
+          assert(hash_map_s_find hm' k' == hash_map_s_find hm k');
           assert(assoc_list_find k' al' == assoc_list_find k' al)
           end
       in
       assert(disjoint_hm_al hm' al');
-      assert(hash_map_slots_s_len hm' + length al' <= usize_max);
+      assert(hash_map_s_len hm' + length al' <= usize_max);
       hash_map_move_elements_s_flat_lem hm' al'
 #pop-options
 
@@ -2044,18 +2038,18 @@ let slots_t_inv_implies_slots_s_inv #t slots =
   // Problem is: I can never really predict for sure with F*...
   ()
 
-val hash_map_t_base_inv_implies_hash_map_slots_s_inv
+val hash_map_t_base_inv_implies_hash_map_s_inv
   (#t : Type0) (hm : hash_map_t t) :
   Lemma (requires (hash_map_t_base_inv hm))
-  (ensures (hash_map_slots_s_inv (hash_map_t_v hm)))
+  (ensures (hash_map_s_inv (hash_map_t_v hm)))
 
-let hash_map_t_base_inv_implies_hash_map_slots_s_inv #t hm = () // same as previous
+let hash_map_t_base_inv_implies_hash_map_s_inv #t hm = () // same as previous
 
 /// Introducing a "partial" version of the hash map invariant, which operates on
 /// a suffix of the hash map.
-let partial_hash_map_slots_s_inv
+let partial_hash_map_s_inv
   (#t : Type0) (len : usize{len > 0}) (offset : usize)
-  (hm : hash_map_slots_s t{offset + length hm <= usize_max}) : Type0 =
+  (hm : hash_map_s t{offset + length hm <= usize_max}) : Type0 =
   forall(i:nat{i < length hm}). {:pattern index hm i} slot_s_inv len (offset + i) (index hm i)
 
 /// Auxiliary lemma.
@@ -2065,13 +2059,13 @@ val binding_in_previous_slot_implies_neq
   (#t : Type0) (len : usize{len > 0})
   (i : usize) (b : binding t)
   (offset : usize{i < offset})
-  (slots : hash_map_slots_s t{offset + length slots <= usize_max}) :
+  (slots : hash_map_s t{offset + length slots <= usize_max}) :
   Lemma
   (requires (
     // The binding comes from a slot not in [slots]
     hash_mod_key (fst b) len = i /\
     // The slots are the well-formed suffix of a hash map
-    partial_hash_map_slots_s_inv len offset slots))
+    partial_hash_map_s_inv len offset slots))
   (ensures (
     for_all (binding_neq b) (flatten slots)))
   (decreases slots)
@@ -2102,17 +2096,17 @@ let rec binding_in_previous_slot_implies_neq #t len i b offset slots =
     for_all_append (binding_neq b) s (flatten slots')    
 #pop-options
 
-val partial_hash_map_slots_s_inv_implies_assoc_list_lem
+val partial_hash_map_s_inv_implies_assoc_list_lem
   (#t : Type0) (len : usize{len > 0}) (offset : usize)
-  (hm : hash_map_slots_s t{offset + length hm <= usize_max}) :
+  (hm : hash_map_s t{offset + length hm <= usize_max}) :
   Lemma
   (requires (
-    partial_hash_map_slots_s_inv len offset hm))
+    partial_hash_map_s_inv len offset hm))
   (ensures (assoc_list_inv (flatten hm)))
   (decreases (length hm + length (flatten hm)))
 
 #push-options "--fuel 1"
-let rec partial_hash_map_slots_s_inv_implies_assoc_list_lem #t len offset hm =
+let rec partial_hash_map_s_inv_implies_assoc_list_lem #t len offset hm =
   match hm with
   | [] -> ()
   | slot :: hm' ->
@@ -2121,8 +2115,8 @@ let rec partial_hash_map_slots_s_inv_implies_assoc_list_lem #t len offset hm =
     match slot with
     | [] ->
       assert(flatten hm == flatten hm');
-      assert(partial_hash_map_slots_s_inv len (offset+1) hm'); // Triggers instantiations
-      partial_hash_map_slots_s_inv_implies_assoc_list_lem len (offset+1) hm'
+      assert(partial_hash_map_s_inv len (offset+1) hm'); // Triggers instantiations
+      partial_hash_map_s_inv_implies_assoc_list_lem len (offset+1) hm'
     | x :: slot' ->
       assert(flatten (slot' :: hm') == slot' @ flatten hm');
       let hm'' = slot' :: hm' in
@@ -2131,25 +2125,25 @@ let rec partial_hash_map_slots_s_inv_implies_assoc_list_lem #t len offset hm =
       assert(index hm 0 == slot); // Triggers instantiations
       assert(slot_s_inv len offset slot);
       assert(slot_s_inv len offset slot');
-      assert(partial_hash_map_slots_s_inv len offset hm'');
-      partial_hash_map_slots_s_inv_implies_assoc_list_lem len offset (slot' :: hm');
+      assert(partial_hash_map_s_inv len offset hm'');
+      partial_hash_map_s_inv_implies_assoc_list_lem len offset (slot' :: hm');
       // Proving that the key in `x` is different from all the other keys in
       // the flattened map
       assert(for_all (binding_neq x) slot');
       for_all_append (binding_neq x) slot' (flatten hm');
-      assert(partial_hash_map_slots_s_inv len (offset+1) hm');
+      assert(partial_hash_map_s_inv len (offset+1) hm');
       binding_in_previous_slot_implies_neq #t len offset x (offset+1) hm';
       assert(for_all (binding_neq x) (flatten hm'));
       assert(for_all (binding_neq x) (flatten (slot' :: hm')))
 #pop-options
 
-val hash_map_slots_s_inv_implies_assoc_list_lem
-  (#t : Type0) (hm : hash_map_slots_s t) :
-  Lemma (requires (hash_map_slots_s_inv hm))
+val hash_map_s_inv_implies_assoc_list_lem
+  (#t : Type0) (hm : hash_map_s t) :
+  Lemma (requires (hash_map_s_inv hm))
   (ensures (assoc_list_inv (flatten hm)))
 
-let hash_map_slots_s_inv_implies_assoc_list_lem #t hm =
-  partial_hash_map_slots_s_inv_implies_assoc_list_lem (length hm) 0 hm
+let hash_map_s_inv_implies_assoc_list_lem #t hm =
+  partial_hash_map_s_inv_implies_assoc_list_lem (length hm) 0 hm
 
 val hash_map_t_base_inv_implies_assoc_list_lem
   (#t : Type0) (hm : hash_map_t t):
@@ -2157,7 +2151,7 @@ val hash_map_t_base_inv_implies_assoc_list_lem
   (ensures (assoc_list_inv (hash_map_t_al_v hm)))
 
 let hash_map_t_base_inv_implies_assoc_list_lem #t hm =
-  hash_map_slots_s_inv_implies_assoc_list_lem (hash_map_t_v hm)
+  hash_map_s_inv_implies_assoc_list_lem (hash_map_t_v hm)
 
 /// For some reason, we can't write the below [forall] directly in the [ensures]
 /// clause of the next lemma: it makes Z3 fails even with a huge rlimit.
@@ -2167,9 +2161,9 @@ let hash_map_is_assoc_list
   (al : assoc_list t) : Type0 =
   (forall (k:key). hash_map_t_find_s ntable k == assoc_list_find k al)
 
-let partial_hash_map_slots_s_find
+let partial_hash_map_s_find
   (#t : Type0) (len : usize{len > 0}) (offset : usize)
-  (hm : hash_map_slots_s_nes t{offset + length hm = len})
+  (hm : hash_map_s_nes t{offset + length hm = len})
   (k : key{hash_mod_key k len >= offset}) : option t =
   let i = hash_mod_key k len in
   let slot = index hm (i - offset) in
@@ -2199,13 +2193,13 @@ val key_in_previous_slot_implies_not_found
   (#t : Type0) (len : usize{len > 0})
   (k : key)
   (offset : usize)
-  (slots : hash_map_slots_s t{offset + length slots = len}) :
+  (slots : hash_map_s t{offset + length slots = len}) :
   Lemma
   (requires (
     // The binding comes from a slot not in [slots]
     hash_mod_key k len < offset /\
     // The slots are the well-formed suffix of a hash map
-    partial_hash_map_slots_s_inv len offset slots))
+    partial_hash_map_s_inv len offset slots))
   (ensures (
     assoc_list_find k (flatten slots) == None))
   (decreases slots)
@@ -2223,20 +2217,20 @@ let rec key_in_previous_slot_implies_not_found #t len k offset slots =
     key_in_previous_slot_implies_not_found len k (offset+1) slots'
 #pop-options  
 
-val partial_hash_map_slots_s_is_assoc_list_lem
+val partial_hash_map_s_is_assoc_list_lem
   (#t : Type0) (len : usize{len > 0}) (offset : usize)
-  (hm : hash_map_slots_s_nes t{offset + length hm = len})
+  (hm : hash_map_s_nes t{offset + length hm = len})
   (k : key{hash_mod_key k len >= offset}) :
   Lemma
   (requires (
-    partial_hash_map_slots_s_inv len offset hm))
+    partial_hash_map_s_inv len offset hm))
   (ensures (
-    partial_hash_map_slots_s_find len offset hm k == assoc_list_find k (flatten hm)))
+    partial_hash_map_s_find len offset hm k == assoc_list_find k (flatten hm)))
   (decreases hm)
 //  (decreases (length hm + length (flatten hm)))
 
 #push-options "--fuel 1"
-let rec partial_hash_map_slots_s_is_assoc_list_lem #t len offset hm k =
+let rec partial_hash_map_s_is_assoc_list_lem #t len offset hm k =
   match hm with
   | [] -> ()
   | slot :: hm' ->
@@ -2245,7 +2239,7 @@ let rec partial_hash_map_slots_s_is_assoc_list_lem #t len offset hm k =
     if i = 0 then
       begin
       // We must look in the current slot
-      assert(partial_hash_map_slots_s_find len offset hm k == slot_s_find k slot);
+      assert(partial_hash_map_s_find len offset hm k == slot_s_find k slot);
       find_append (same_key k) slot (flatten hm');
       assert(forall (i:nat{i < length hm'}). index hm' i == index hm (i+1)); // Triggers instantiations
       key_in_previous_slot_implies_not_found #t len k (offset+1) hm';
@@ -2264,13 +2258,13 @@ let rec partial_hash_map_slots_s_is_assoc_list_lem #t len offset hm k =
     else
       begin
       // We must ignore the current slot
-      assert(partial_hash_map_slots_s_find len offset hm k ==
-             partial_hash_map_slots_s_find len (offset+1) hm' k);
+      assert(partial_hash_map_s_find len offset hm k ==
+             partial_hash_map_s_find len (offset+1) hm' k);
       find_append (same_key k) slot (flatten hm');
       assert(index hm 0 == slot); // Triggers instantiations
       not_same_hash_key_not_found_in_slot #t len k offset slot;
       assert(forall (i:nat{i < length hm'}). index hm' i == index hm (i+1)); // Triggers instantiations
-      partial_hash_map_slots_s_is_assoc_list_lem #t len (offset+1) hm' k
+      partial_hash_map_s_is_assoc_list_lem #t len (offset+1) hm' k
       end
 #pop-options
 
@@ -2284,7 +2278,7 @@ let hash_map_is_assoc_list_lem #t hm =
     [SMTPat (hash_map_t_find_s hm k)] =
     let hm_v = hash_map_t_v hm in
     let len = length hm_v in
-    partial_hash_map_slots_s_is_assoc_list_lem #t len 0 hm_v k
+    partial_hash_map_s_is_assoc_list_lem #t len 0 hm_v k
   in
   ()
 
@@ -2669,7 +2663,7 @@ val hash_map_insert_fwd_back_lem
       // The invariant is preserved
       hash_map_t_inv hm' /\
       // [key] maps to [value] and the other bindings are preserved
-      hash_map_slots_s_updated_binding (hash_map_t_v self) key (Some value) (hash_map_t_v hm') /\
+      hash_map_s_updated_binding (hash_map_t_v self) key (Some value) (hash_map_t_v hm') /\
       // The length is incremented, iff we inserted a new key
       (match hash_map_t_find_s self key with
        | None -> hash_map_t_len_s hm' = hash_map_t_len_s self + 1
@@ -2680,11 +2674,11 @@ let hash_map_insert_fwd_back_bindings_lem
   (hm' hm'' : hash_map_t_nes t) :
   Lemma
   (requires (
-     hash_map_slots_s_updated_binding (hash_map_t_v self) key
+     hash_map_s_updated_binding (hash_map_t_v self) key
                                       (Some value) (hash_map_t_v hm') /\
      hash_map_t_same_bindings hm' hm''))
   (ensures (
-     hash_map_slots_s_updated_binding (hash_map_t_v self) key
+     hash_map_s_updated_binding (hash_map_t_v self) key
                                       (Some value) (hash_map_t_v hm'')))
   = ()
 
@@ -2702,15 +2696,15 @@ let hash_map_insert_fwd_back_lem t self key value =
     assert(hash_map_t_base_inv hm');
     assert(hash_map_same_params hm' self);
     assert(hash_map_t_v hm' == hm'_v);
-    assert(hash_map_slots_s_len hm'_v == hash_map_t_len_s hm');
+    assert(hash_map_s_len hm'_v == hash_map_t_len_s hm');
     // Expanding the post of [hash_map_insert_no_resize_s_lem]
     assert(insert_post self_v key value hm'_v);
     // Expanding [insert_post]
-    assert(hash_map_slots_s_inv hm'_v);
+    assert(hash_map_s_inv hm'_v);
     assert(
-      match hash_map_slots_s_find self_v key with
-      | None -> hash_map_slots_s_len hm'_v = hash_map_slots_s_len self_v + 1
-      | Some _ -> hash_map_slots_s_len hm'_v = hash_map_slots_s_len self_v);
+      match hash_map_s_find self_v key with
+      | None -> hash_map_s_len hm'_v = hash_map_s_len self_v + 1
+      | Some _ -> hash_map_s_len hm'_v = hash_map_s_len self_v);
     if hash_map_t_len_s hm' > hm'.hash_map_max_load then
       begin
       hash_map_try_resize_fwd_back_lem hm';
@@ -3166,8 +3160,8 @@ let rec hash_map_remove_from_list_back_lem_refin #t key ls =
 
 /// High-level model for [remove_from_list'back]
 let hash_map_remove_s
-  (#t : Type0) (self : hash_map_slots_s_nes t) (key : usize) :
-  hash_map_slots_s t =
+  (#t : Type0) (self : hash_map_s_nes t) (key : usize) :
+  hash_map_s t =
   let len = length self in
   let hash = hash_mod_key key len in
   let slot = index self hash in
@@ -3293,15 +3287,15 @@ let rec hash_map_remove_from_list_s_lem #t key slot len i =
 #pop-options
 
 val hash_map_remove_s_lem
-  (#t : Type0) (self : hash_map_slots_s_nes t) (key : usize) :
+  (#t : Type0) (self : hash_map_s_nes t) (key : usize) :
   Lemma
-  (requires (hash_map_slots_s_inv self))
+  (requires (hash_map_s_inv self))
   (ensures (
     let hm' = hash_map_remove_s self key in
     // The invariant is preserved
-    hash_map_slots_s_inv hm' /\
+    hash_map_s_inv hm' /\
     // We updated the binding
-    hash_map_slots_s_updated_binding self key None hm'))
+    hash_map_s_updated_binding self key None hm'))
 
 let hash_map_remove_s_lem #t self key =
   let len = length self in
@@ -3310,7 +3304,7 @@ let hash_map_remove_s_lem #t self key =
   hash_map_remove_from_list_s_lem key slot len hash;
   let slot' = hash_map_remove_from_list_s key slot in
   let hm' = list_update self hash slot' in
-  assert(hash_map_slots_s_inv self)
+  assert(hash_map_s_inv self)
 
 /// Final lemma about [remove'back]
 val hash_map_remove_back_lem