From f3cb86b9ea93000fa4e26c618dc34ed5133a3c78 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 13 Feb 2022 19:42:34 +0100
Subject: Start cleaning up

---
 tests/hashmap/Hashmap.Properties.fst | 208 ++++-------------------------------
 1 file changed, 20 insertions(+), 188 deletions(-)

(limited to 'tests')

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 2339d6af..649334c8 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -7,9 +7,6 @@ open Hashmap.Types
 open Hashmap.Clauses
 open Hashmap.Funs
 
-// To help with the proofs - TODO: remove
-module InteractiveHelpers = FStar.InteractiveHelpers
-
 #set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
 
 /// The proofs actually caused a lot more trouble than expected, because of the
@@ -218,28 +215,6 @@ let rec index_map_lem #a #b f ls i =
     else index_map_lem f ls' (i-1)
 #pop-options
 
-// TODO: remove?
-// Returns the index of the value which satisfies the predicate
-val find_index :
-    #a:Type
-  -> f:(a -> Tot bool)
-  -> ls:list a{Some? (find f ls)}
-  -> Tot (i:nat{
-    i < length ls /\
-    begin match find f ls with
-    | None -> False
-    | Some x -> x == index ls i
-    end})
-
-#push-options "--fuel 1"
-let rec find_index #a f ls =
-  match ls with
-  | [] -> assert(False); 0
-  | x :: ls' ->
-    if f x then 0
-    else 1 + find_index f ls'
-#pop-options
-
 val for_all_append (#a : Type0) (f : a -> Tot bool) (ls0 ls1 : list a) :
   Lemma (for_all f (ls0 @ ls1) = (for_all f ls0 && for_all f ls1))
 
@@ -368,7 +343,6 @@ let rec length_flatten_update #a ls i x =
       end
 #pop-options
 
-
 val length_flatten_index :
      #a:Type
   -> ls:list (list a)
@@ -424,12 +398,15 @@ let rec pairwise_distinct (#a : eqtype) (ls : list a) : Tot bool =
   | [] -> true
   | x :: ls' -> List.Tot.for_all (fun y -> x <> y) ls' && pairwise_distinct ls'
 
+(*
 val for_allP: #a:Type -> f:(a -> Tot Type0) -> list a -> Tot Type0
 let rec for_allP (f : 'a -> Tot Type0) (l : list 'a) : Tot Type0 =
   match l with
   | [] -> True
   | hd::tl -> f hd /\ for_allP f tl
+*)
 
+(*
 val for_all_i_aux: #a:Type -> f:(nat -> a -> Tot bool) -> list a -> nat -> Tot bool
 let rec for_all_i_aux (f : nat -> 'a -> Tot bool) (l : list 'a) (i : nat) : Tot bool =
   match l with
@@ -439,13 +416,15 @@ let rec for_all_i_aux (f : nat -> 'a -> Tot bool) (l : list 'a) (i : nat) : Tot
 val for_all_i: #a:Type -> f:(nat -> a -> Tot bool) -> list a -> Tot bool
 let for_all_i (f : nat -> 'a -> Tot bool) (l : list 'a) : Tot bool =
   for_all_i_aux f l 0
+*)
 
-val pairwise_relP : #a:Type -> pred:(a -> a -> Tot Type0) -> ls:list a -> Tot Type0
+(*val pairwise_relP : #a:Type -> pred:(a -> a -> Tot Type0) -> ls:list a -> Tot Type0
 let rec pairwise_relP #a pred ls =
   match ls with
   | [] -> True
   | x :: ls' ->
     for_allP (pred x) ls' /\ pairwise_relP pred ls'
+*)
 
 val pairwise_rel : #a:Type -> pred:(a -> a -> Tot bool) -> ls:list a -> Tot bool
 let rec pairwise_rel #a pred ls =
@@ -574,9 +553,6 @@ let same_key (#t : Type0) (k : key) (b : binding t) : bool = fst b = k
 let same_hash_mod_key (#t : Type0) (len : usize{len > 0}) (h : nat) (b : binding t) : bool =
   hash_mod_key (fst b) len = h
 
-// We take a [nat] instead of a [hash] on purpose
-(*let same_hash (#t : Type0) (h : nat) (b : binding t) : bool = hash_key (fst b) = h *)
-
 let binding_neq (#t : Type0) (b0 b1 : binding t) : bool = fst b0 <> fst b1
 
 let has_same_binding (#t : Type0) (al : assoc_list t) ((k,v) : binding t) : Type0 =
@@ -605,7 +581,6 @@ let slot_t_find_s (#t : Type0) (k : key) (slot : list_t t) : option t =
 
 // This is a simpler version of the "find" function, which captures the essence
 // of what happens and operates on [hash_map_slots_s].
-// TODO: useful?
 let hash_map_slots_s_find
   (#t : Type0) (hm : hash_map_slots_s_nes t)
   (k : key) : option t =
@@ -629,45 +604,6 @@ let hash_map_t_find_s
   let slot = index slots i in
   slot_t_find_s k slot
 
-(*let hash_map_t_find_s (#t : Type0) (hm : hash_map_t t) (k : key) : option t =
- match find (same_key k) (hash_map_t_v hm) with
- | None -> None
- | Some (_, v) -> Some v*)
-
-/// Auxiliary function stating that two associative lists are "equivalent"
-let assoc_list_equiv (#t : Type0) (al0 al1 : assoc_list t) : Type0 =
-  // All the bindings in al0 can be found in al1
-  for_allP (has_same_binding al1) al0 /\
-  // And the reverse is true
-  for_allP (has_same_binding al0) al1
-
-(*
-// Introducing auxiliary definitions to help deal with the quantifiers
-
-let not_same_keys_at_j_k
-  (#t : Type0) (ls : list_t t) (j:nat{j < list_t_len ls}) (k:nat{k < list_t_len ls}) :
-  Type0 =
-  fst (list_t_index ls j) <> fst (list_t_index ls k)
-
-(*let not_same_keys_at_j_k
-  (#t : Type0) (ls : list_t t) (j:nat{j < list_t_len ls}) (k:nat{k < list_t_len ls}) :
-  Type0 =
-  fst (list_t_index ls j) <> fst (list_t_index ls k)*)
-
-type slot_t_inv_hash_key_f (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t) =
-  (j:nat{j < list_t_len slot}) ->
-  Lemma (hash_mod_key (fst (list_t_index slot j)) len = i)
-  [SMTPat (hash_mod_key (fst (list_t_index slot j)) len)]
-  
-type slot_t_inv_not_same_keys_f (#t : Type0) (i : usize) (slot : list_t t) =
-     (j:nat{j < list_t_len slot})
-  -> (k:nat{k < list_t_len slot /\ j < k})
-  -> Lemma (not_same_keys_at_j_k slot j k)
-  [SMTPat (not_same_keys_at_j_k slot j k)]
-*)
-
-(**)
-
 /// Invariants for the slots
 
 let slot_s_inv
@@ -683,52 +619,6 @@ let slot_t_inv (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t)
   // All the keys are pairwise distinct
   pairwise_rel binding_neq (list_t_v slot)
 
-(*
-/// Invariants for the slots
-/// Rk.: making sure the quantifiers instantiations work was painful. As always.
-let slot_t_inv (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t) : Type0 =
-  // All the hashes of the keys are equal to the current hash
-  (forall (j:nat{j < list_t_len slot}).
-    {:pattern (list_t_index slot j)}
-    hash_mod_key (fst (list_t_index slot j)) len = i) /\
-  // All the keys are pairwise distinct
-  (forall (j:nat{j < list_t_len slot}) (k:nat{k < list_t_len slot /\ j < k}).
-    {:pattern not_same_keys_at_j_k slot j k}
-    k <> j ==> not_same_keys_at_j_k slot j k)
-
-/// Helpers to deal with the quantifier proofs
-let slot_t_inv_to_funs
-  (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t{slot_t_inv len i slot}) :
-  slot_t_inv_hash_key_f len i slot & slot_t_inv_not_same_keys_f i slot =
-  let f : slot_t_inv_hash_key_f len i slot =
-    fun j -> ()
-  in
-  let g : slot_t_inv_not_same_keys_f i slot =
-    fun j k -> ()
-  in
-  (f, g)
-
-let slot_t_inv_from_funs_lem
-  (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t)
-  (f : slot_t_inv_hash_key_f len i slot)
-  (g : slot_t_inv_not_same_keys_f i slot) :
-  Lemma (slot_t_inv len i slot) =
-  // Dealing with quantifiers is annoying, like always
-  let f' (j:nat{j < list_t_len slot}) :
-    Lemma (hash_mod_key (fst (list_t_index slot j)) len = i)
-    [SMTPat (hash_mod_key (fst (list_t_index slot j)) len)]
-    =
-    f j
-  in
-  let g' (j:nat{j < list_t_len slot}) (k:nat{k < list_t_len slot /\ j < k}) :
-    Lemma (not_same_keys_at_j_k slot j k)
-    [SMTPat (not_same_keys_at_j_k slot j k)]
-    =
-    g j k
-  in
-  ()
-*)
-
 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}
@@ -739,30 +629,6 @@ let slots_t_inv (#t : Type0) (slots : slots_t t{length slots <= usize_max}) : Ty
   {:pattern index slots i}
   slot_t_inv (length slots) i (index slots i)
 
-(*
-type slots_t_inv_f (#t : Type0) (slots : slots_t t{length slots <= usize_max}) =
-  (i:nat{i < length slots}) ->
-  Lemma (slot_t_inv (length slots) i (index slots i))
-
-let slots_t_inv_to_fun
-  (#t : Type0) (slots : slots_t t{length slots <= usize_max /\ slots_t_inv slots}) :
-  slots_t_inv_f slots =
-  fun i -> ()
-
-let slots_t_from_fun
-  (#t : Type0) (slots : slots_t t{length slots <= usize_max})
-  (f : slots_t_inv_f slots) :
-  Lemma (slots_t_inv slots) =
-  let f' (i:nat{i < length slots}) :
-    Lemma (slot_t_inv (length slots) i (index slots i))
-    [SMTPat (slot_t_inv (length slots) i (index slots i))]
-    =
-    f i
-  in
-  ()
-*)
-
-// TODO: hash_map_slots -> hash_map_slots_s
 let hash_map_slots_s_inv (#t : Type0) (hm : hash_map_slots_s t) : Type0 =
   length hm <= usize_max /\
   length hm > 0 /\
@@ -800,28 +666,12 @@ let hash_map_t_inv (#t : Type0) (hm : hash_map_t t) : Type0 =
    hm.hash_map_num_entries <= hm.hash_map_max_load
    || length hm.hash_map_slots * 2 * dividend > usize_max)
 
-/// The following predicate links the hashmap to an associative list.
-/// Note that it does not compute the representant: different (permuted)
-/// lists can be used to represent the same hashmap!
-let hash_map_t_is_al (#t : Type0) (hm : hash_map_t t) (al : assoc_list t) : Type0 =
-  let hm_al = hash_map_t_v hm in
-  assoc_list_equiv hm_al al
-
 /// We often need to frame some values
 let hash_map_same_params (#t : Type0) (hm0 hm1 : hash_map_t t) : Type0 =
   length hm0.hash_map_slots = length hm1.hash_map_slots /\
   hm0.hash_map_max_load = hm1.hash_map_max_load /\
   hm0.hash_map_max_load_factor = hm1.hash_map_max_load_factor
   
-(*
-/// The invariant we reveal to the user
-let hash_map_t_inv_repr (#t : Type0) (hm : hash_map_t t) (al : assoc_list t) : Type0 =
-  // The hash map invariant is satisfied
-  hash_map_t_inv hm /\
-  // And it can be seen as the given associative list
-  hash_map_t_is_al hm al
-*)
-
 (*** allocate_slots *)
 
 /// Auxiliary lemma
@@ -1042,8 +892,7 @@ let hash_map_clear_fwd_back_lem_fun t self =
     slots_t_al_v_all_nil_is_empty_lem slots1;
     let hm1 = Mkhash_map_t 0 p i slots1 in
     assert(hash_map_t_base_inv hm1);
-    assert(hash_map_t_inv hm1);
-    assert(hash_map_t_is_al hm1 [])
+    assert(hash_map_t_inv hm1)
   end
 #pop-options
 
@@ -1599,7 +1448,7 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
 
 (**** insert_{no_fail,no_resize}: invariants *)
 
-let hash_map_t_updated_binding
+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 =
   // [key] maps to [value]
@@ -1612,7 +1461,7 @@ let insert_post (#t : Type0) (hm : hash_map_slots_s_nes t)
   // The invariant is preserved
   hash_map_slots_s_inv hm' /\
   // [key] maps to [value] and the other bindings are preserved
-  hash_map_t_updated_binding hm key (Some value) hm' /\
+  hash_map_slots_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
@@ -2708,7 +2557,7 @@ let times_divid_lem (n m p : pos) :
   assert(((n * (m / p)) * p) / p = n * (m / p))
 #pop-options
 
-#push-options "--z3rlimit 100"
+#push-options "--z3rlimit 100 --z3cliopt smt.arith.nl=false"
 let new_max_load_lem
   (len : usize) (capacity : usize{capacity > 0})
   (divid : usize{divid > 0}) (divis : usize{divis > 0}) :
@@ -2718,7 +2567,7 @@ let new_max_load_lem
     let ncapacity = 2 * capacity in
     let nmax_load = (ncapacity * divid) / divis in
     capacity > 0 /\ 0 < divid /\ divid < divis /\
-    capacity * divid >= divis /\ // TODO: add to invariant
+    capacity * divid >= divis /\
     len = max_load + 1))
   (ensures (
     let max_load = (capacity * divid) / divis in
@@ -2731,7 +2580,9 @@ let new_max_load_lem
   assert(nmax_load = (2 * capacity * divid) / divis);
   times_divid_lem 2 (capacity * divid) divis;
   assert(nmax_load >= 2 * ((capacity * divid) / divis));
-  assert(nmax_load >= 2 * max_load)
+  assert(nmax_load >= 2 * max_load);
+  assert(nmax_load >= max_load + max_load);
+  assert(nmax_load >= max_load + 1)
 #pop-options
 
 val hash_map_try_resize_s_simpl_lem (#t : Type0) (hm : hash_map_t t) :
@@ -2891,7 +2742,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_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm') /\
+      hash_map_slots_s_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_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
@@ -2902,10 +2753,12 @@ let hash_map_insert_fwd_back_bindings_lem
   (hm' hm'' : hash_map_t_nes t) :
   Lemma
   (requires (
-     hash_map_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm') /\
+     hash_map_slots_s_updated_binding (hash_map_t_slots_v self) key
+                                      (Some value) (hash_map_t_slots_v hm') /\
      hash_map_t_same_bindings hm' hm''))
   (ensures (
-     hash_map_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm'')))
+     hash_map_slots_s_updated_binding (hash_map_t_slots_v self) key
+                                      (Some value) (hash_map_t_slots_v hm'')))
   = ()
 
 #restart-solver
@@ -3345,25 +3198,6 @@ let hash_map_remove_from_list_s
   slot_s t =
   filter_one (not_same_key key) ls
 
-(*
-// TODO: remove?
-val filter_one_find (#a : Type) (f g : a -> bool) (ls : list a) :
-  Lemma
-  (requires (forall x. f x <> g x))
-  (ensures (
-    let ls' = filter_one f ls in
-    match find g ls with
-    | None -> length ls' = length ls
-    | Some _ -> length ls' + 1 = length ls))
-
-#push-options "--fuel 1"
-let rec filter_one_find #a f g ls =
-  match ls with
-  | [] -> ()
-  | x :: ls' -> filter_one_find f g ls'
-#pop-options
-*)
-
 /// Refinement lemma
 val hash_map_remove_from_list_back_lem_refin
   (#t : Type0) (key : usize) (ls : list_t t) :
@@ -3531,8 +3365,6 @@ let rec hash_map_remove_from_list_s_lem #t key slot len i =
       end
 #pop-options
 
-// TODO: rename hash_map_t_updated_binding to hash_map_slots_updated_binding
-
 val hash_map_remove_s_lem
   (#t : Type0) (self : hash_map_slots_s_nes t) (key : usize) :
   Lemma
@@ -3542,7 +3374,7 @@ val hash_map_remove_s_lem
     // The invariant is preserved
     hash_map_slots_s_inv hm' /\
     // We updated the binding
-    hash_map_t_updated_binding self key None hm'))
+    hash_map_slots_s_updated_binding self key None hm'))
 
 let hash_map_remove_s_lem #t self key =
   let len = length self in
-- 
cgit v1.2.3