diff options
| -rw-r--r-- | tests/hashmap/Hashmap.Clauses.fst | 6 | ||||
| -rw-r--r-- | tests/hashmap/Hashmap.Funs.fst | 41 | ||||
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 372 |
3 files changed, 376 insertions, 43 deletions
diff --git a/tests/hashmap/Hashmap.Clauses.fst b/tests/hashmap/Hashmap.Clauses.fst index 81727b5a..4f3e37e9 100644 --- a/tests/hashmap/Hashmap.Clauses.fst +++ b/tests/hashmap/Hashmap.Clauses.fst @@ -35,6 +35,12 @@ let hash_map_move_elements_decreases (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) : nat = if i < length slots then length slots - i else 0 +(** [hashmap::HashMap::contains_key_in_list]: decreases clause *) +unfold +let hash_map_contains_key_in_list_decreases (t : Type0) (key : usize) + (ls : list_t t) : list_t t = + ls + (** [hashmap::HashMap::get_in_list]: decreases clause *) unfold let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) : diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst index 3828ae98..d3d09765 100644 --- a/tests/hashmap/Hashmap.Funs.fst +++ b/tests/hashmap/Hashmap.Funs.fst @@ -310,6 +310,47 @@ let hash_map_insert_fwd_back end end +(** [hashmap::HashMap::contains_key_in_list] *) +let rec hash_map_contains_key_in_list_fwd + (t : Type0) (key : usize) (ls : list_t t) : + Tot (result bool) + (decreases (hash_map_contains_key_in_list_decreases t key ls)) + = + begin match ls with + | ListCons ckey x ls0 -> + let b = ckey = key in + if b + then Return true + else + begin match hash_map_contains_key_in_list_fwd t key ls0 with + | Fail -> Fail + | Return b0 -> Return b0 + end + | ListNil -> Return false + end + +(** [hashmap::HashMap::contains_key] *) +let hash_map_contains_key_fwd + (t : Type0) (self : hash_map_t t) (key : usize) : result bool = + begin match hash_key_fwd key with + | Fail -> Fail + | Return i -> + let v = self.hash_map_slots in + let i0 = vec_len (list_t t) v in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match vec_index_fwd (list_t t) v hash_mod with + | Fail -> Fail + | Return l -> + begin match hash_map_contains_key_in_list_fwd t key l with + | Fail -> Fail + | Return b -> Return b + end + end + end + end + (** [hashmap::HashMap::get_in_list] *) let rec hash_map_get_in_list_fwd (t : Type0) (key : usize) (ls : list_t t) : diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 822b630b..8053c911 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -1401,6 +1401,18 @@ let hash_map_insert_in_list_back_lem t len key value ls = /// We work on [hash_map_slots_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 t{length hm <= usize_max /\ length hm > 0}) + (key : usize) (value : t) : + hash_map_slots_s t = + let len = length hm in + let i = hash_mod_key key len in + let slot = index hm i in + let slot' = hash_map_insert_in_list_s key value slot in + 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 let hash_map_insert_no_resize_s (#t : Type0) (hm : hash_map_slots_s t{length hm <= usize_max /\ length hm > 0}) @@ -1409,15 +1421,7 @@ let hash_map_insert_no_resize_s // 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 - else - begin - let len = length hm in - let i = hash_mod_key key len in - let slot = index hm i in - let slot' = hash_map_insert_in_list_s key value slot in - let hm' = list_update hm i slot' in - Return hm' - end + else Return (hash_map_insert_no_fail_s hm key value) /// Prove that [hash_map_insert_no_resize_s] is a refinement of /// [hash_map_insert_no_resize'fwd_back] @@ -1676,8 +1680,54 @@ let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls = (*** move_elements *) +(**** move_elements: refinement 0 *) +/// The proof for [hash_map_move_elements_fwd_back_lem_refin] broke so many times +/// (while it is supposed to be super simple!) that we decided to add one refinement +/// level, to really do things step by step... +/// Doing this refinement layer made me notice that maybe the problem came from +/// the fact that at some point we have to prove `list_t_v ListNil == []`: I +/// added the corresponding assert to help Z3 and everything became stable. +/// I finally didn't use this "simple" refinement lemma, but I still keep it here +/// because it allows for easy comparisons with [hash_map_move_elements_s]. + +/// [hash_map_move_elements_fwd] refines this function, which is actually almost +/// the same (just a little bit shorter and cleaner, and has a pre). +/// +/// The way I wrote the refinement is the following: +/// - I copy-pasted the definition of [hash_map_move_elements_fwd], wrote the +/// signature which links this new definition to [hash_map_move_elements_fwd] and +/// checked that the proof passed +/// - I gradually simplified it, while making sure the proof still passes +#push-options "--fuel 1" +let rec hash_map_move_elements_s_simpl + (t : Type0) (ntable : hash_map_t t) + (slots : vec (list_t t)) + (i : usize{i <= length slots /\ length slots <= usize_max}) : + Pure (result ((hash_map_t t) & (vec (list_t t)))) + (requires (True)) + (ensures (fun res -> + match res, hash_map_move_elements_fwd_back t ntable slots i with + | Fail, Fail -> True + | Return (ntable1, slots1), Return (ntable2, slots2) -> + ntable1 == ntable2 /\ + slots1 == slots2 + | _ -> False)) + (decreases (hash_map_move_elements_decreases t ntable slots i)) + = + if i < length slots + then + let slot = index slots i in + begin match hash_map_move_elements_from_list_fwd_back t ntable slot with + | Fail -> Fail + | Return hm' -> + let slots' = list_update slots i ListNil in + hash_map_move_elements_s_simpl t hm' slots' (i+1) + end + else Return (ntable, slots) +#pop-options + (**** move_elements: refinement 1 *) -/// We prove a first refinement lemma: calling [move_elements] refines a function +/// We prove a second refinement lemma: calling [move_elements] refines a function /// which, for every slot, moves the element out of the slot. This first version is /// almost exactly the translated function, it just uses `list` instead of `list_t`. @@ -1743,13 +1793,22 @@ val hash_map_move_elements_fwd_back_lem_refin // the ifuel to unreasonable amounts). // // Finally, as I had succeeded in fixing the proof, I thought that maybe the -// initial problem with the type abbreviations fixed: I thus tried to use +// initial problem with the type abbreviations was fixed: I thus tried to use // them. Of course, it made the proof fail again, and this time no ifuel setting -// seemed to work (maybe my initial guess about the type inferencer was right?...). +// seemed to work. // // At this point I was just fed up and leave things as they were, without trying // to cleanup the previous definitions. // +// Finally, even later it broke, again, at which point I had no choice but to +// introduce an even simpler refinement proof (with [hash_map_move_elements_s_simpl]). +// Doing this allowed me to see that maybe the problem came from the fact that +// Z3 had to prove that `list_t_v ListNil == []` at some point, so I added the +// corresponding assertion and miraculously everything becamse stable... I then +// removed all the postconditions I had manually instanciated and inserted in +// the proof, and which took a lot of place. +// I still have no clue why `ifuel 4` made it work earlier. +// // The terrible thing is that this refinement proof is conceptually super simple: // - there are maybe two arithmetic proofs, which are directly solved by the // precondition @@ -1757,7 +1816,7 @@ val hash_map_move_elements_fwd_back_lem_refin // this is proven by another refinement lemma we proved above // - there is the recursive call (trivial) #restart-solver -#push-options "--z3rlimit 300 --fuel 1 --ifuel 4" +#push-options "--fuel 1" let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i = assert(hash_map_t_base_inv ntable); let i0 = vec_len (list_t t) slots in @@ -1770,22 +1829,12 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i = let l0 = mem_replace_fwd (list_t t) l ListNil in assert(l0 == l); hash_map_move_elements_from_list_fwd_back_lem t ntable l0; - begin - match hash_map_move_elements_from_list_fwd_back t ntable l0, - hash_map_move_elements_from_list_s (hash_map_t_slots_v ntable) (slot_t_v l0) - with - | Fail, Fail -> () - | Return hm', Return hm_v -> - assert(hash_map_t_base_inv hm'); - assert(hash_map_t_slots_v hm' == hm_v); - assert(hash_map_same_params hm' ntable) - | _ -> assert(False) - end; begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with | Fail -> () | Return h -> let l1 = mem_replace_back (list_t t) l ListNil in assert(l1 == ListNil); + assert(slot_t_v #t ListNil == []); // THIS IS IMPORTANT begin match vec_index_mut_back (list_t t) slots i l1 with | Fail -> () | Return v -> @@ -1793,28 +1842,11 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i = | Fail -> () | Return i1 -> hash_map_move_elements_fwd_back_lem_refin t h v i1; - begin - match hash_map_move_elements_fwd_back t h v i1, - hash_map_move_elements_s (hash_map_t_slots_v h) (slots_t_v v) i1 - with - | Fail, Fail -> () - | Return (ntable', _), Return ntable'_v -> - assert(hash_map_t_base_inv ntable'); - assert(hash_map_t_slots_v ntable' == ntable'_v); - assert(hash_map_same_params ntable' ntable) - | _ -> assert(False) - end; begin match hash_map_move_elements_fwd_back t h v i1 with | Fail -> assert(hash_map_move_elements_fwd_back t ntable slots i == Fail); () - | Return (ntable', v0) -> - begin - // Trying to prove the postcondition - match hash_map_move_elements_fwd_back t ntable slots i with - | Fail -> assert(False) - | Return (ntable'', _) -> assert(ntable'' == ntable') - end + | Return (ntable', v0) -> () end end end @@ -2656,10 +2688,264 @@ let hash_map_insert_fwd_back_lem t self key value = end else () -(*** contains *) +(*** contains_key *) + +(**** contains_key_in_list *) + +val hash_map_contains_key_in_list_fwd_lem + (#t : Type0) (key : usize) (ls : list_t t) : + Lemma + (ensures ( + match hash_map_contains_key_in_list_fwd t key ls with + | Fail -> False + | Return b -> + b = Some? (slot_t_find_s key ls))) + + +#push-options "--fuel 1" +let rec hash_map_contains_key_in_list_fwd_lem #t key ls = + match ls with + | ListCons ckey x ls0 -> + let b = ckey = key in + if b + then () + else + begin + hash_map_contains_key_in_list_fwd_lem key ls0; + match hash_map_contains_key_in_list_fwd t key ls0 with + | Fail -> () + | Return b0 -> () + end + | ListNil -> () +#pop-options + +(**** contains_key *) + +val hash_map_contains_key_fwd_lem + (#t : Type0) (self : hash_map_t_nes t) (key : usize) : + Lemma + (ensures ( + match hash_map_contains_key_fwd t self key with + | Fail -> False + | Return b -> b = Some? (hash_map_t_find_s self key))) + +let hash_map_contains_key_fwd_lem #t self key = + begin match hash_key_fwd key with + | Fail -> () + | Return i -> + let v = self.hash_map_slots in + let i0 = vec_len (list_t t) v in + begin match usize_rem i i0 with + | Fail -> () + | Return hash_mod -> + begin match vec_index_fwd (list_t t) v hash_mod with + | Fail -> () + | Return l -> + hash_map_contains_key_in_list_fwd_lem key l; + begin match hash_map_contains_key_in_list_fwd t key l with + | Fail -> () + | Return b -> () + end + end + end + end (*** get *) +(**** get_in_list *) + +val hash_map_get_in_list_fwd_lem + (#t : Type0) (key : usize) (ls : list_t t) : + Lemma + (ensures ( + match hash_map_get_in_list_fwd t key ls, slot_t_find_s key ls with + | Fail, None -> True + | Return x, Some x' -> x == x' + | _ -> False)) + +#push-options "--fuel 1" +let rec hash_map_get_in_list_fwd_lem #t key ls = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then () + else + begin + hash_map_get_in_list_fwd_lem key ls0; + match hash_map_get_in_list_fwd t key ls0 with + | Fail -> () + | Return x -> () + end + | ListNil -> () + end +#pop-options + +(**** get *) + +val hash_map_get_fwd_lem + (#t : Type0) (self : hash_map_t_nes t) (key : usize) : + Lemma + (ensures ( + match hash_map_get_fwd t self key, hash_map_t_find_s self key with + | Fail, None -> True + | Return x, Some x' -> x == x' + | _ -> False)) + +let hash_map_get_fwd_lem #t self key = + begin match hash_key_fwd key with + | Fail -> () + | Return i -> + let v = self.hash_map_slots in + let i0 = vec_len (list_t t) v in + begin match usize_rem i i0 with + | Fail -> () + | Return hash_mod -> + begin match vec_index_fwd (list_t t) v hash_mod with + | Fail -> () + | Return l -> + begin + hash_map_get_in_list_fwd_lem key l; + match hash_map_get_in_list_fwd t key l with + | Fail -> () + | Return x -> () + end + end + end + end + + (*** get_mut'fwd *) + +(**** get_mut_in_list *) + +val hash_map_get_mut_in_list_fwd_lem + (#t : Type0) (key : usize) (ls : list_t t) : + Lemma + (ensures ( + match hash_map_get_mut_in_list_fwd t key ls, slot_t_find_s key ls with + | Fail, None -> True + | Return x, Some x' -> x == x' + | _ -> False)) + +#push-options "--fuel 1" +let rec hash_map_get_mut_in_list_fwd_lem #t key ls = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then () + else + begin + hash_map_get_mut_in_list_fwd_lem key ls0; + match hash_map_get_mut_in_list_fwd t key ls0 with + | Fail -> () + | Return x -> () + end + | ListNil -> () + end +#pop-options + +(**** get_mut *) + +val hash_map_get_mut_fwd_lem + (#t : Type0) (self : hash_map_t_nes t) (key : usize) : + Lemma + (ensures ( + match hash_map_get_mut_fwd t self key, hash_map_t_find_s self key with + | Fail, None -> True + | Return x, Some x' -> x == x' + | _ -> False)) + +let hash_map_get_mut_fwd_lem #t self key = + begin match hash_key_fwd key with + | Fail -> () + | Return i -> + let v = self.hash_map_slots in + let i0 = vec_len (list_t t) v in + begin match usize_rem i i0 with + | Fail -> () + | Return hash_mod -> + begin match vec_index_fwd (list_t t) v hash_mod with + | Fail -> () + | Return l -> + begin + hash_map_get_mut_in_list_fwd_lem key l; + match hash_map_get_mut_in_list_fwd t key l with + | Fail -> () + | Return x -> () + end + end + end + end + + (*** get_mut'back *) + +(**** get_mut_in_list *) + +val hash_map_get_mut_in_list_back_lem + (#t : Type0) (key : usize) (ls : list_t t) (ret : t) : + Lemma + (requires (Some? (slot_t_find_s key ls))) + (ensures ( + match hash_map_get_mut_in_list_back t key ls ret with + | Fail -> False + | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret) + | _ -> False)) + +#push-options "--fuel 1" +let rec hash_map_get_mut_in_list_back_lem #t key ls ret = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then let ls1 = ListCons ckey ret ls0 in () + else + begin + hash_map_get_mut_in_list_back_lem key ls0 ret; + match hash_map_get_mut_in_list_back t key ls0 ret with + | Fail -> () + | Return l -> let ls1 = ListCons ckey cvalue l in () + end + | ListNil -> () + end +#pop-options + +(**** get_mut *) + +val hash_map_get_mut_back_lem + (#t : Type0) (self : hash_map_t t) (key : usize) (ret : t) : + Lemma + (requires (Some? (hash_map_t_find_s self key)) + (ensures ( + match hash_map_get_mut_back t self key ret with + | Fail -> False + | Return hm' -> hash_map_t_slots_v hm' == hash_map_insert_no_fail hm key ret)) + +let hash_map_get_mut_back_lem #t self key = + begin match hash_key_back key with + | Fail -> () + | Return i -> + let v = self.hash_map_slots in + let i0 = vec_len (list_t t) v in + begin match usize_rem i i0 with + | Fail -> () + | Return hash_mod -> + begin match vec_index_back (list_t t) v hash_mod with + | Fail -> () + | Return l -> + begin + hash_map_get_mut_in_list_back_lem key l; + match hash_map_get_mut_in_list_back t key l with + | Fail -> () + | Return x -> () + end + end + end + end + + + +//val hash_map_insert_no_resize_s_lem |