diff options
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 220 |
1 files changed, 219 insertions, 1 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 43f95b1b..14ca7d00 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -34,6 +34,20 @@ let rec list_update_index_dif_lem #a ls i x j = (*** Utilities *) +val find_update: + #a:Type + -> f:(a -> Tot bool) + -> ls:list a + -> x:a + -> ls':list a{length ls' == length ls} +#push-options "--fuel 1" +let rec find_update #a f ls x = + match ls with + | [] -> [] + | hd::tl -> + if f hd then x :: tl else hd :: find_update f tl x +#pop-options + val pairwise_distinct : #a:eqtype -> ls:list a -> Tot bool let rec pairwise_distinct (#a : eqtype) (ls : list a) : Tot bool = match ls with @@ -78,14 +92,25 @@ let rec flatten_append (#a : Type) (l1 l2: list (list a)) : let fst_is_disctinct (#a : eqtype) (#b : Type0) (p0 : a & b) (p1 : a & b) : Type0 = fst p0 <> fst p1 -(*** Invariants, representants *) +(*** Invariants, models *) /// "Natural" length function for [list_t] +/// TODO: remove? we can reason simply with [list_t_v] let rec list_t_len (#t : Type0) (ls : list_t t) : nat = match ls with | ListNil -> 0 | ListCons _ _ tl -> 1 + list_t_len tl +/// "Natural" append function for [list_t] +/// TODO: remove? we can reason simply with [list_t_v] +#push-options "--fuel 1" +let rec list_t_append (#t : Type0) (ls0 ls1 : list_t t) : + ls:list_t t{list_t_len ls = list_t_len ls0 + list_t_len ls1} = + match ls0 with + | ListNil -> ls1 + | ListCons x v tl -> ListCons x v (list_t_append tl ls1) +#pop-options + /// The "key" type type key = usize @@ -119,6 +144,14 @@ let has_same_binding (#t : Type0) (al : assoc_list t) ((k,v) : binding t) : Type | None -> False | Some (k',v') -> v' == v +let hash_map_t_mem (#t : Type0) (hm : hash_map_t t) (k : key) : bool = + existsb (same_key k) (hash_map_t_v hm) + +let hash_map_t_find (#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 @@ -363,6 +396,7 @@ let hash_map_clear_fwd_back_lem t self = end #pop-options + (**** len *) /// [len]: we link it to a non-failing function. @@ -378,3 +412,187 @@ let hash_map_len_fwd_lem t self = () (**** insert_in_list *) + +/// [insert_in_list_fwd]: returns true iff the key is not in the list +val hash_map_insert_in_list_fwd_lem + (t : Type0) (key : usize) (value : t) (ls : list_t t) : + Lemma + (ensures ( + match hash_map_insert_in_list_fwd t key value ls with + | Fail -> False + | Return b -> + b <==> (find (same_key key) (list_t_v ls) == None))) + (decreases (hash_map_insert_in_list_decreases t key value ls)) + +#push-options "--fuel 1" +let rec hash_map_insert_in_list_fwd_lem t key value ls = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then () + else + begin + hash_map_insert_in_list_fwd_lem t key value ls0; + match hash_map_insert_in_list_fwd t key value ls0 with + | Fail -> () + | Return b0 -> () + end + | ListNil -> + assert(list_t_v ls == []); + assert_norm(find (same_key #t key) [] == None) + end +#pop-options + +/// The proofs about [insert_in_list] backward are easier to do in several steps: +/// extrinsic proofs to the rescue! + +/// [insert_in_list]: if the key is not in the map, appends a new bindings +val hash_map_insert_in_list_back_lem_append + (t : Type0) (key : usize) (value : t) (ls : list_t t) : + Lemma + (requires ( + find (same_key key) (list_t_v ls) == None)) + (ensures ( + match hash_map_insert_in_list_back t key value ls with + | Fail -> False + | Return ls' -> + list_t_v ls' == list_t_v ls @ [(key,value)])) + (decreases (hash_map_insert_in_list_decreases t key value ls)) + +#push-options "--fuel 1" +let rec hash_map_insert_in_list_back_lem_append t key value ls = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then () //let ls1 = ListCons ckey value ls0 in Return ls1 + else + begin + hash_map_insert_in_list_back_lem_append t key value ls0; + match hash_map_insert_in_list_back t key value ls0 with + | Fail -> () + | Return l -> () + end + | ListNil -> () + end +#pop-options + +/// [insert_in_list]: if the key is in the map, we update the binding +val hash_map_insert_in_list_back_lem_update + (t : Type0) (key : usize) (value : t) (ls : list_t t) : + Lemma + (requires ( + Some? (find (same_key key) (list_t_v ls)))) + (ensures ( + match hash_map_insert_in_list_back t key value ls with + | Fail -> False + | Return ls' -> + list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,value))) + (decreases (hash_map_insert_in_list_decreases t key value ls)) + +#push-options "--fuel 1" +let rec hash_map_insert_in_list_back_lem_update t key value ls = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then () + else + begin + hash_map_insert_in_list_back_lem_update t key value ls0; + match hash_map_insert_in_list_back t key value ls0 with + | Fail -> () + | Return l -> () + end + | ListNil -> () + end +#pop-options + +(**** insert_no_resize *) + +/// Same as for [insert_in_list]: we do the proofs in several, modular steps. +/// The strategy is to study the two disjoint cases: +/// - the key is already in the map (we update the binding) +/// - the key is not in the map (we add a binding) +/// +/// We gradually prove that the resulting map, in the two cases, can be seen +/// as the result of: +/// - filtering the bindings for the key we want to insert +/// - pushing the new binding at the front +/// +/// We then prove a less "functional" variant of the result, which states that, +/// after the insertion: +/// - [key] maps to [value] +/// - forall key' <> key, the binding is unchanged +/// +/// This way, we have a consistent, high-level description of the insertion. +/// +/// Rk.: with multimaps the high-level spec would be even simpler: we would push +/// an element to the front of the list. + +/// [insert_no_resize]: if the key is in the map, we succeed and update the binding. +val hash_map_insert_no_resize_fwd_back_lem_update + (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : + Lemma + (requires ( + hash_map_t_inv self /\ + // The key is in the map + Some? (find (same_key key) (hash_map_t_v self)))) + (ensures ( + match hash_map_insert_no_resize_fwd_back t self key value with + | Fail -> False + | Return hm -> + // The invariant is preserved + hash_map_t_inv hm /\ + // The map has been updated + hash_map_t_v hm == find_update (same_key key) (hash_map_t_v self) (key,value))) + +let hash_map_insert_no_resize_fwd_back_lem_update t self key value = + begin match hash_key_fwd key with + | Fail -> () + | Return i -> + let i0 = self.hash_map_num_entries in + let p = self.hash_map_max_load_factor in + let i1 = self.hash_map_max_load in + let v = self.hash_map_slots in + let i2 = vec_len (list_t t) v in + begin match usize_rem i i2 with + | Fail -> () + | Return hash_mod -> + begin match vec_index_mut_fwd (list_t t) v hash_mod with + | Fail -> () + | Return l -> + // The key must be in the slot - TODO: update invariant + assume(Some? (find (same_key key) (list_t_v l))); + hash_map_insert_in_list_fwd_lem t key value l; + begin match hash_map_insert_in_list_fwd t key value l with + | Fail -> () + | Return b -> + assert(not b); + if b then assert(False) + else + begin + hash_map_insert_in_list_back_lem_update t key value l; + match hash_map_insert_in_list_back t key value l with + | Fail -> () + | Return l0 -> + begin + match vec_index_mut_back (list_t t) v hash_mod l0 with + | Fail -> () + | Return v0 -> + let hm1 = Mkhash_map_t i0 p i1 v0 in + assume(hash_map_t_inv hm1); + assume(hash_map_t_v hm1 == find_update (same_key key) (hash_map_t_v self) (key,value)) + end + end + end + end + end + end + + +/// [insert_in_list]: inserting a binding is equivalent to: +/// - filtering the list +/// - pushing the binding to the front + |