diff options
author | Son Ho | 2022-02-12 00:46:38 +0100 |
---|---|---|
committer | Son Ho | 2022-02-12 00:46:38 +0100 |
commit | 62cd0b89a055ec4fa767246e63490b95ec71e8db (patch) | |
tree | 91e36b9e3bf056925216066c68d5f5e9fe53930c | |
parent | 15a4c9e0c1d41bc64a351e0768078676d5e5aa38 (diff) |
Prove the refinment lemma for hash_map_move_elements_from_list
Diffstat (limited to '')
-rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 47 |
1 files changed, 27 insertions, 20 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 69a9bc40..0f5f8c8b 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -1237,7 +1237,7 @@ let hash_map_insert_no_resize_s /// Prove that [hash_map_insert_no_resize_s] is a refinement of /// [hash_map_insert_no_resize'fwd_back] -val hash_map_insert_no_resize_fwd_back_lem +val hash_map_insert_no_resize_fwd_back_lem_s (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : Lemma (requires ( @@ -1250,13 +1250,13 @@ val hash_map_insert_no_resize_fwd_back_lem with | Fail, Fail -> True | Return hm, Return hm_v -> + hash_map_t_inv hm /\ hash_map_t_slots_v hm == hm_v /\ - hash_map_slots_s_len hm_v = hash_map_t_len_s hm /\ - True + hash_map_slots_s_len hm_v = hash_map_t_len_s hm | _ -> False end)) -let hash_map_insert_no_resize_fwd_back_lem t self key value = +let hash_map_insert_no_resize_fwd_back_lem_s t self key value = begin match hash_key_fwd key with | Fail -> () | Return i -> @@ -1265,6 +1265,7 @@ let hash_map_insert_no_resize_fwd_back_lem t self key value = let i1 = self.hash_map_max_load in let v = self.hash_map_slots in let i2 = vec_len (list_t t) v in + let len = length v in begin match usize_rem i i2 with | Fail -> () | Return hash_mod -> @@ -1279,7 +1280,7 @@ let hash_map_insert_no_resize_fwd_back_lem t self key value = | Fail -> () | Return b -> assert(b = None? (slot_find key (list_t_v l))); - hash_map_insert_in_list_back_lem_s t key value l; + hash_map_insert_in_list_back_lem t len key value l; if b then begin match usize_add i0 1 with @@ -1325,6 +1326,7 @@ let hash_map_insert_no_resize_fwd_back_lem t self key value = end end + (**** find after insert *) /// Lemmas about what happens if we call [find] after an insertion @@ -1378,6 +1380,7 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' = end end + (*** move_elements_from_list *) type hash_map_slots_s_res (t : Type0) = res:result (hash_map_slots_s t){ @@ -1386,19 +1389,17 @@ type hash_map_slots_s_res (t : Type0) = res:result (hash_map_slots_s t){ | Return hm -> is_pos_usize (length hm) } -let hash_map_move_elements_from_list_s +let rec hash_map_move_elements_from_list_s (t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)}) (ls : slot_s t) : - Tot (hash_map_slots_s_res t) = - let add_elem (hm_res : hash_map_slots_s_res t) (b : binding t) : - hash_map_slots_s_res t = - match hm_res with + Tot (hash_map_slots_s_res t) (decreases ls) = + match ls with + | [] -> Return hm + | (key, value) :: ls' -> + match hash_map_insert_no_resize_s hm key value with | Fail -> Fail - | Return hm -> - let (key,value) = b in - hash_map_insert_no_resize_s hm key value - in - fold_left add_elem (Return hm) ls + | Return hm' -> + hash_map_move_elements_from_list_s t hm' ls' /// Refinement lemma val hash_map_move_elements_from_list_fwd_back_lem @@ -1415,24 +1416,30 @@ val hash_map_move_elements_from_list_fwd_back_lem | _ -> False)) (decreases (hash_map_move_elements_from_list_decreases t ntable ls)) -#push-options "--z3rlimit 100 --fuel 1" +#push-options "--fuel 1" let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls = begin match ls with | ListCons k v tl -> - hash_map_insert_no_resize_fwd_back_lem t ntable k v; + assert(list_t_v ls == (k, v) :: list_t_v tl); + let ls_v = list_t_v ls in + let (_,_) :: tl_v = ls_v in + hash_map_insert_no_resize_fwd_back_lem_s t ntable k v; begin match hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail -> admit() + | Fail -> () | Return h -> + let h_v = Return?.v (hash_map_insert_no_resize_s (hash_map_t_slots_v ntable) k v) in + assert(hash_map_t_slots_v h == h_v); hash_map_move_elements_from_list_fwd_back_lem t h tl; begin match hash_map_move_elements_from_list_fwd_back t h tl with - | Fail -> admit() - | Return h0 -> admit() + | Fail -> () + | Return h0 -> () end end | ListNil -> () end #pop-options +(* /// Refinement lemma val hash_map_move_elements_fwd_back_lem (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) : |