diff options
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 59 |
1 files changed, 45 insertions, 14 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 0f5f8c8b..8c36cec9 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -302,6 +302,14 @@ type hash_map_slots_s t = list (slot_s t) /// High-level type for the hash-map, seen as a an associative list type hash_map_s t = assoc_list t +// TODO: move +let is_pos_usize (n : nat) : Type0 = 0 < n /\ n <= usize_max + +// 'nes': "non-empty slots" +// TODO: use more +type hash_map_slots_s_nes (t : Type0) : Type0 = + hm:hash_map_slots_s t{is_pos_usize (length hm)} + /// Representation function for [hash_map_t] as a list of slots let hash_map_t_slots_v (#t : Type0) (hm : hash_map_t t) : hash_map_slots_s t = map list_t_v hm.hash_map_slots @@ -310,10 +318,7 @@ let hash_map_t_slots_v (#t : Type0) (hm : hash_map_t t) : hash_map_slots_s t = let hash_map_t_v (#t : Type0) (hm : hash_map_t t) : hash_map_s t = flatten (hash_map_t_slots_v hm) -// TODO: move -let is_pos_usize (n : nat) : Type0 = 0 < n /\ n <= usize_max - -// 'ne': "non-empty slots" +// 'nes': "non-empty slots" // TODO: use more type hash_map_t_nes (t : Type0) : Type0 = hm:hash_map_t t{is_pos_usize (length hm.hash_map_slots)} @@ -1390,7 +1395,7 @@ type hash_map_slots_s_res (t : Type0) = res:result (hash_map_slots_s t){ } let rec hash_map_move_elements_from_list_s - (t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)}) + (#t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)}) (ls : slot_s t) : Tot (hash_map_slots_s_res t) (decreases ls) = match ls with @@ -1399,7 +1404,7 @@ let rec hash_map_move_elements_from_list_s match hash_map_insert_no_resize_s hm key value with | Fail -> Fail | Return hm' -> - hash_map_move_elements_from_list_s t hm' ls' + hash_map_move_elements_from_list_s hm' ls' /// Refinement lemma val hash_map_move_elements_from_list_fwd_back_lem @@ -1407,7 +1412,7 @@ val hash_map_move_elements_from_list_fwd_back_lem Lemma (requires (hash_map_t_inv ntable)) (ensures ( match hash_map_move_elements_from_list_fwd_back t ntable ls, - hash_map_move_elements_from_list_s t (hash_map_t_slots_v ntable) (slot_t_v ls) + hash_map_move_elements_from_list_s (hash_map_t_slots_v ntable) (slot_t_v ls) with | Fail, Fail -> True | Return hm', Return hm_v -> @@ -1439,17 +1444,43 @@ let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls = end #pop-options +(*** move_elements *) + +// Note that we ignore the returned slots (we thus don't return a pair: +// only the new hash map in which we moved the elements from the slots): +// this returned value is not used. +let rec hash_map_move_elements_s + (#t : Type0) (hm : hash_map_slots_s_nes t) + (slots : slots_s t) (i : usize{i <= length slots /\ length slots <= usize_max}) : + Tot (result (hash_map_slots_s_nes t)) + (decreases (length slots - i)) = + let len = length slots in + if i < len then + begin + let slot = index slots i in + match hash_map_move_elements_from_list_s hm slot with + | Fail -> Fail + | Return hm' -> + let slots' = list_update slots i [] in + hash_map_move_elements_s hm' slots' (i+1) + end + else Return hm + (* -/// Refinement lemma -val hash_map_move_elements_fwd_back_lem - (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) : - Lemma (requires (is_pos_usize (ntable.hash_map_num_entries))) +val hash_map_move_elements_fwd_back + (t : Type0) (ntable : hash_map_t t) + (slots : vec (list_t t)) (i : usize{i <= length ntable.hash_map_slots}) : + Lemma (requires (hash_map_t_inv ntable)) (ensures ( match hash_map_move_elements_fwd_back t ntable slots i, - hash_map_move_elements_from_list_s t ntable slots + hash_map_move_elements_s (hash_map_t_slots_v ntable) (slots_t_v slots) i with - | Fail -> - )) + | Fail, Fail -> True // We will prove later that this is not possible + | Return hm, Return hm_v -> + hash_map_t_inv hm /\ + hash_map_t_slots_v hm)) + + Tot (result ((hash_map_t t) & (vec (list_t t)))) (decreases (hash_map_move_elements_decreases t ntable slots i)) let rec hash_map_move_elements_fwd_back |