From 08130619b474dc87ba923e789f25dbb4a9b6ec94 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 13 Feb 2022 14:56:05 +0100 Subject: Prove the refinement lemma for remove'back --- tests/hashmap/Hashmap.Properties.fst | 149 ++++++++++++++++++++++++++++++++--- 1 file changed, 137 insertions(+), 12 deletions(-) (limited to 'tests/hashmap/Hashmap.Properties.fst') diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 1cf5fc88..08ae5714 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -247,6 +247,14 @@ let rec map_same_f_eq #a #b f g ls = | x :: ls' -> map_same_f_eq f g ls' #pop-options +/// Filter a list, stopping after we removed one element +val filter_one (#a : Type) (f : a -> bool) (ls : list a) : list a + +let rec filter_one #a f ls = + match ls with + | [] -> [] + | x :: ls' -> if f x then x :: filter_one f ls' else ls' + (*** Lemmas about Primitives *) /// TODO: move those lemmas @@ -517,6 +525,7 @@ let hash_key (k : key) : hash = let hash_mod_key (k : key) (len : usize{len > 0}) : hash = (hash_key k) % len +let not_same_key (#t : Type0) (k : key) (b : binding t) : bool = fst b <> k let same_key (#t : Type0) (k : key) (b : binding t) : bool = fst b = k // We take a [nat] instead of a [hash] on purpose @@ -1454,7 +1463,7 @@ let hash_map_insert_no_resize_s if None? (hash_map_slots_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 a refinement of +/// Prove that [hash_map_insert_no_resize_s] is refined by /// [hash_map_insert_no_resize'fwd_back] val hash_map_insert_no_resize_fwd_back_lem_s (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : @@ -1665,7 +1674,7 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' = /// 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 change and using [result_hash_map_slots_s] +/// Followingly, I'm not taking any chance and using [result_hash_map_slots_s] /// everywhere. type result_hash_map_slots_s_nes (t : Type0) : Type0 = res:result (hash_map_slots_s t) { @@ -1742,7 +1751,7 @@ let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls = /// [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: +/// The way I wrote the high-level model 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 @@ -1777,7 +1786,7 @@ let rec hash_map_move_elements_s_simpl (**** move_elements: refinement 1 *) /// 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 +/// which, for every slot, moves the element out of the slot. This first model is /// almost exactly the translated function, it just uses `list` instead of `list_t`. // Note that we ignore the returned slots (we thus don't return a pair: @@ -1861,8 +1870,8 @@ val hash_map_move_elements_fwd_back_lem_refin // 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 -// - we need to refine the call to [hash_map_move_elements_from_list_fwd_back]: -// this is proven by another refinement lemma we proved above +// - we need to prove the call to [hash_map_move_elements_from_list_fwd_back] +// refines its model: this is proven by another refinement lemma we proved above // - there is the recursive call (trivial) #restart-solver #push-options "--fuel 1" @@ -2080,6 +2089,7 @@ let rec flatten_i_same_suffix #a l0 l1 i = /// Refinement lemma: /// [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) (slots : slots_s t) @@ -2426,8 +2436,8 @@ let hash_map_move_elements_fwd_back_lem t ntable slots = (*** try_resize *) -/// Refinement 1. -/// This one is slightly "crude": we just simplify a bit the function. +/// High-level model 1. +/// This is one is slightly "crude": we just simplify a bit the function. let hash_map_try_resize_s_simpl (#t : Type0) @@ -2684,7 +2694,7 @@ let hash_map_try_resize_fwd_back_lem #t hm = (*** insert *) -/// The refinement (very close to the original function: we don't need something +/// The high-level model (very close to the original function: we don't need something /// very high level, just to clean it a bit) let hash_map_insert_s (#t : Type0) (self : hash_map_t t) (key : usize) (value : t) : @@ -2725,9 +2735,6 @@ val hash_map_insert_fwd_back_lem 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 value (hash_map_t_slots_v hm') /\ -// hash_map_t_find_s hm' key == Some value /\ - // The other bindings are preserved- TODO -// (forall k'. k' <> key ==> hash_map_t_find_s hm' k' == hash_map_t_find_s self k') /\ // 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 @@ -3172,3 +3179,121 @@ let hash_map_remove_fwd_lem t self key = end (*** remove'back *) + +/// High-level model for [remove_from_list'back] +let hash_map_remove_from_list_s + (#t : Type0) (key : usize) (ls : slot_s t) : + slot_s t = + filter_one (not_same_key key) ls + +/// Refinement lemma +val hash_map_remove_from_list_back_lem + (#t : Type0) (key : usize) (ls : list_t t) : + Lemma + (ensures ( + match hash_map_remove_from_list_back t key ls with + | Fail -> False + | Return ls' -> list_t_v ls' == hash_map_remove_from_list_s key (list_t_v ls))) + +#push-options "--fuel 1" +let rec hash_map_remove_from_list_back_lem #t key ls = + begin match ls with + | ListCons ckey x tl -> + let b = ckey = key in + if b + then + let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in + begin match mv_ls with + | ListCons i cvalue tl0 -> () + | ListNil -> () + end + else + begin + hash_map_remove_from_list_back_lem key tl; + match hash_map_remove_from_list_back t key tl with + | Fail -> () + | Return l -> let ls0 = ListCons ckey x l in () + end + | ListNil -> () + end +#pop-options + +/// 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 = + let len = length self in + let hash = hash_mod_key key len in + let slot = index self hash in + let slot' = hash_map_remove_from_list_s key slot in + list_update self hash slot' + +/// Refinement lemma +val hash_map_remove_back_lem + (#t : Type0) (self : hash_map_t_nes t) (key : usize) : + Lemma + (requires ( + // We need the invariant to prove that upon decrementing the entries counter, + // the counter doesn't become negative + hash_map_t_inv self)) + (ensures ( + match hash_map_remove_back t self key with + | Fail -> False + | Return hm' -> hash_map_t_slots_v hm' == hash_map_remove_s (hash_map_t_slots_v self) key)) + +let hash_map_remove_back_lem #t self key = + 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 -> + begin + hash_map_remove_from_list_fwd_lem key l; + match hash_map_remove_from_list_fwd t key l with + | Fail -> () + | Return x -> + begin match x with + | None -> + begin + hash_map_remove_from_list_back_lem key l; + match hash_map_remove_from_list_back t key l with + | Fail -> () + | Return l0 -> + begin match vec_index_mut_back (list_t t) v hash_mod l0 with + | Fail -> () + | Return v0 -> () + end + end + | Some x0 -> + begin + assert(l == index v hash_mod); + assert(length (list_t_v #t l) > 0); + length_flatten_index (hash_map_t_slots_v self) hash_mod; + match usize_sub i0 1 with + | Fail -> () + | Return i3 -> + begin + hash_map_remove_from_list_back_lem key l; + match hash_map_remove_from_list_back t key l with + | Fail -> () + | Return l0 -> + begin match vec_index_mut_back (list_t t) v hash_mod l0 with + | Fail -> () + | Return v0 -> () + end + end + end + end + end + end + end + end -- cgit v1.2.3