Perform some renamings in the hashmap example

1 files changed, 51 insertions, 50 deletions

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index e7236189..aee5dbb7 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -293,13 +293,13 @@ type slots_s (t : Type0) = list (slot_s t)
 
 /// High-level type for the hash-map, seen as a list of associative lists (one
 /// list per slot)
-type hash_map_slots t = list (slot_s t)
+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
 
 /// Representation function for [hash_map_t] as a list of slots
-let hash_map_t_slots_v (#t : Type0) (hm : hash_map_t t) : hash_map_slots t =
+let hash_map_t_slots_v (#t : Type0) (hm : hash_map_t t) : hash_map_slots_s t =
   map list_t_v hm.hash_map_slots
 
 /// Representation function for [hash_map_t]
@@ -345,23 +345,23 @@ let slot_t_find_s (#t : Type0) (k : key) (slot : list_t t) : option t =
   | Some (_, v) -> Some v
 
 // This is a simpler version of the "find" function, which captures the essence
-// of what happens and operates on [hash_map_slots].
+// of what happens and operates on [hash_map_slots_s].
 // TODO: useful?
-let hash_map_slots_find_s
-  (#t : Type0) (hm : hash_map_slots t{length hm <= usize_max /\ length hm > 0})
+let hash_map_slots_s_find
+  (#t : Type0) (hm : hash_map_slots_s t{length hm <= usize_max /\ length hm > 0})
   (k : key) : option t =
   let i = hash_mod_key k (length hm) in
   let slot = index hm i in
   slot_find k slot
 
-let hash_map_slots_len_s
-  (#t : Type0) (hm : hash_map_slots t{length hm <= usize_max /\ length hm > 0}) :
+let hash_map_slots_s_len
+  (#t : Type0) (hm : hash_map_slots_s t{length hm <= usize_max /\ length hm > 0}) :
   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] then looking up an element is not the same as what we
+// [hash_map_slots_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 =
@@ -411,7 +411,7 @@ type slot_t_inv_not_same_keys_f (#t : Type0) (i : usize) (slot : list_t t) =
 
 /// Invariants for the slots
 
-let slot_inv
+let slot_s_inv
 (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list (binding t)) : bool =
   // All the bindings are in the proper slot
   for_all (same_hash_mod_key len i) slot &&
@@ -470,10 +470,10 @@ let slot_t_inv_from_funs_lem
   ()
 *)
 
-let slots_inv (#t : Type0) (slots : slots_s t{length slots <= usize_max}) : Type0 =
+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_inv (length slots) i (index slots i)
+  slot_s_inv (length slots) i (index slots i)
 
 let slots_t_inv (#t : Type0) (slots : slots_t t{length slots <= usize_max}) : Type0 =
   forall(i:nat{i < length slots}).
@@ -504,10 +504,10 @@ let slots_t_from_fun
 *)
 
 // TODO: hash_map_slots -> hash_map_slots_s
-let hash_map_slots_inv (#t : Type0) (hm : hash_map_slots t) : Type0 =
+let hash_map_slots_s_inv (#t : Type0) (hm : hash_map_slots_s t) : Type0 =
   length hm <= usize_max /\
   length hm > 0 /\
-  slots_inv hm
+  slots_s_inv hm
 
 /// Base invariant for the hashmap (the complete invariant can be temporarily
 /// broken between the moment we inserted an element and the moment we resize)
@@ -947,30 +947,30 @@ let rec slot_t_v_for_all_binding_neq_append_lem t key value ls b =
     slot_t_v_for_all_binding_neq_append_lem t key value cls b
 #pop-options
 
-val slot_inv_not_find_append_end_inv_lem
+val slot_s_inv_not_find_append_end_inv_lem
   (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list (binding t)) :
   Lemma
   (requires (
-    slot_inv len (hash_mod_key key len) ls /\
+    slot_s_inv len (hash_mod_key key len) ls /\
     slot_find key ls == None))
   (ensures (
     let ls' = ls @ [(key,value)] in
-    slot_inv len (hash_mod_key key len) ls' /\
+    slot_s_inv len (hash_mod_key key len) ls' /\
     (slot_find key ls' == Some value) /\
     (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls)))
 
 #push-options "--fuel 1"
-let rec slot_inv_not_find_append_end_inv_lem t len key value ls =
+let rec slot_s_inv_not_find_append_end_inv_lem t len key value ls =
   match ls with
   | [] -> ()
   | (ck, cv) :: cls ->
-    slot_inv_not_find_append_end_inv_lem t len key value cls;
+    slot_s_inv_not_find_append_end_inv_lem t len key value cls;
     let h = hash_mod_key key len in
     let ls' = ls @ [(key,value)] in
     assert(for_all (same_hash_mod_key len h) ls');
     slot_t_v_for_all_binding_neq_append_lem t key value cls (ck, cv);
     assert(pairwise_rel binding_neq ls');
-    assert(slot_inv len h ls')
+    assert(slot_s_inv len h ls')
 #pop-options
 
 /// [insert_in_list]: if the key is not in the map, appends a new bindings
@@ -978,20 +978,20 @@ val hash_map_insert_in_list_s_lem_append
   (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list (binding t)) :
   Lemma
   (requires (
-    slot_inv len (hash_mod_key key len) ls /\
+    slot_s_inv len (hash_mod_key key len) ls /\
     slot_find key ls == None))
   (ensures (
     let ls' = hash_map_insert_in_list_s key value ls in
     ls' == ls @ [(key,value)] /\
     // The invariant is preserved
-    slot_inv len (hash_mod_key key len) ls' /\
+    slot_s_inv len (hash_mod_key key len) ls' /\
     // [key] maps to [value]
     slot_find key ls' == Some value /\
     // The other bindings are preserved
     (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls)))
 
 let hash_map_insert_in_list_s_lem_append t len key value ls =
-  slot_inv_not_find_append_end_inv_lem t len key value ls
+  slot_s_inv_not_find_append_end_inv_lem t len key value ls
 
 /// [insert_in_list]: if the key is not in the map, appends a new bindings (quantifiers)
 /// Rk.: we don't use this lemma.
@@ -1052,20 +1052,20 @@ let rec for_all_binding_neq_value_indep #t key v0 v1 ls =
   | _ :: ls' -> for_all_binding_neq_value_indep #t key v0 v1 ls'
 #pop-options
 
-val slot_inv_find_append_end_inv_lem
+val slot_s_inv_find_append_end_inv_lem
   (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list (binding t)) :
   Lemma
   (requires (
-    slot_inv len (hash_mod_key key len) ls /\
+    slot_s_inv len (hash_mod_key key len) ls /\
     Some? (slot_find key ls)))
   (ensures (
     let ls' = find_update (same_key key) ls (key, value) in
-    slot_inv len (hash_mod_key key len) ls' /\
+    slot_s_inv len (hash_mod_key key len) ls' /\
     (slot_find key ls' == Some value) /\
     (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls)))
 
 #push-options "--z3rlimit 50 --fuel 1"
-let rec slot_inv_find_append_end_inv_lem t len key value ls =
+let rec slot_s_inv_find_append_end_inv_lem t len key value ls =
   match ls with
   | [] -> ()
   | (ck, cv) :: cls ->
@@ -1081,15 +1081,15 @@ let rec slot_inv_find_append_end_inv_lem t len key value ls =
       for_all_binding_neq_value_indep key cv value cls;
       assert(for_all (binding_neq (ck,value)) cls);
       assert(pairwise_rel binding_neq ls');
-      assert(slot_inv len (hash_mod_key key len) ls')
+      assert(slot_s_inv len (hash_mod_key key len) ls')
       end
     else
       begin
-      slot_inv_find_append_end_inv_lem t len key value cls;
+      slot_s_inv_find_append_end_inv_lem t len key value cls;
       assert(for_all (same_hash_mod_key len h) ls');
       slot_find_update_for_all_binding_neq_append_lem t key value cls (ck, cv);
       assert(pairwise_rel binding_neq ls');
-      assert(slot_inv len h ls')
+      assert(slot_s_inv len h ls')
       end
 #pop-options
 
@@ -1098,20 +1098,20 @@ val hash_map_insert_in_list_s_lem_update
   (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list (binding t)) :
   Lemma
   (requires (
-    slot_inv len (hash_mod_key key len) ls /\
+    slot_s_inv len (hash_mod_key key len) ls /\
     Some? (slot_find key ls)))
   (ensures (
     let ls' = hash_map_insert_in_list_s key value ls in
     ls' == find_update (same_key key) ls (key,value) /\
     // The invariant is preserved
-    slot_inv len (hash_mod_key key len) ls' /\
+    slot_s_inv len (hash_mod_key key len) ls' /\
     // [key] maps to [value]
     slot_find key ls' == Some value /\
     // The other bindings are preserved
     (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls)))
 
 let hash_map_insert_in_list_s_lem_update t len key value ls =
-  slot_inv_find_append_end_inv_lem t len key value ls
+  slot_s_inv_find_append_end_inv_lem t len key value ls
 
 
 /// [insert_in_list]: if the key is in the map, update the bindings
@@ -1146,11 +1146,11 @@ val hash_map_insert_in_list_s_lem
   (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list (binding t)) :
   Lemma
   (requires (
-    slot_inv len (hash_mod_key key len) ls))
+    slot_s_inv len (hash_mod_key key len) ls))
   (ensures (
     let ls' = hash_map_insert_in_list_s key value ls in
     // The invariant is preserved
-    slot_inv len (hash_mod_key key len) ls' /\
+    slot_s_inv len (hash_mod_key key len) ls' /\
     // [key] maps to [value]
     slot_find key ls' == Some value /\
     // The other bindings are preserved
@@ -1203,16 +1203,16 @@ 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] (we use a higher-level view of the hash-map, but
+/// We work on [hash_map_slots_s] (we use a higher-level view of the hash-map, but
 /// not too high).
 
 let hash_map_insert_no_resize_s
-  (#t : Type0) (hm : hash_map_slots t{length hm <= usize_max /\ length hm > 0})
+  (#t : Type0) (hm : hash_map_slots_s t{length hm <= usize_max /\ length hm > 0})
   (key : usize) (value : t) :
-  result (hash_map_slots t) =
+  result (hash_map_slots_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_find_s hm key) && num_entries = usize_max then Fail
+  if None? (hash_map_slots_s_find hm key) && num_entries = usize_max then Fail
   else
     begin
     let len = length hm in
@@ -1230,7 +1230,7 @@ val hash_map_insert_no_resize_fwd_back_lem
   Lemma
   (requires (
     hash_map_t_inv self /\
-    hash_map_slots_len_s (hash_map_t_slots_v self) = hash_map_t_len_s self))
+    hash_map_slots_s_len (hash_map_t_slots_v self) = hash_map_t_len_s self))
   (ensures (
     begin
     match hash_map_insert_no_resize_fwd_back t self key value,
@@ -1239,7 +1239,7 @@ val hash_map_insert_no_resize_fwd_back_lem
     | Fail, Fail -> True
     | Return hm, Return hm_v ->
       hash_map_t_slots_v hm == hm_v /\
-      hash_map_slots_len_s hm_v = hash_map_t_len_s hm /\
+      hash_map_slots_s_len hm_v = hash_map_t_len_s hm /\
       True
     | _ -> False
     end))
@@ -1287,7 +1287,7 @@ let hash_map_insert_no_resize_fwd_back_lem 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_len_s hm_v = hash_map_t_len_s hm)
+                  assert(hash_map_slots_s_len hm_v = hash_map_t_len_s hm)
                 end
               end
             end
@@ -1305,7 +1305,7 @@ let hash_map_insert_no_resize_fwd_back_lem 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_len_s hm_v = hash_map_t_len_s hm)
+                assert(hash_map_slots_s_len hm_v = hash_map_t_len_s hm)
               end
             end
         end
@@ -1317,18 +1317,18 @@ let hash_map_insert_no_resize_fwd_back_lem t self 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 t)
+  (#t : Type0) (hm : hash_map_slots_s t)
   (key : usize) (value : t) :
-  Lemma (requires (hash_map_slots_inv hm))
+  Lemma (requires (hash_map_slots_s_inv hm))
   (ensures (
     match hash_map_insert_no_resize_s hm key value with
     | Fail -> True
     | Return hm' ->
-      hash_map_slots_find_s hm' key == Some value))
+      hash_map_slots_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_find_s hm key) && num_entries = usize_max then ()
+  if None? (hash_map_slots_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
@@ -1339,18 +1339,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 t)
+  (#t : Type0) (hm : hash_map_slots_s t)
   (key : usize) (value : t) (key' : usize{key' <> key}) :
-  Lemma (requires (hash_map_slots_inv hm))
+  Lemma (requires (hash_map_slots_s_inv hm))
   (ensures (
     match hash_map_insert_no_resize_s hm key value with
     | Fail -> True
     | Return hm' ->
-      hash_map_slots_find_s hm' key' == hash_map_slots_find_s hm key'))
+      hash_map_slots_s_find hm' key' == hash_map_slots_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_find_s hm key) && num_entries = usize_max then ()
+  if None? (hash_map_slots_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
@@ -1368,6 +1368,7 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
 
 (*** remove_elements_from_list *)
 
+(*
 type hash_map_slots_res (t : Type0) = res:result (hash_map_slots t){
     match res with
     | Fail -> True