diff options
author | Son Ho | 2022-02-13 15:49:30 +0100 |
---|---|---|
committer | Son Ho | 2022-02-13 15:49:30 +0100 |
commit | f2c90fa184fbb9e79547b7176e9b30287f17b758 (patch) | |
tree | d2e9b40eab0cca4968182119beca348ff9e165d0 /tests/hashmap | |
parent | fd3694d71a03022c7fb1423c7f6fbbd528eeb987 (diff) |
State and prove the final lemma about remove'back
Diffstat (limited to 'tests/hashmap')
-rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 8b53268b..9cb8c465 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -3411,3 +3411,26 @@ let hash_map_remove_s_lem #t self key = let slot' = hash_map_remove_from_list_s key slot in let hm' = list_update self hash slot' in assert(hash_map_slots_s_inv self) + +/// Final lemma about [remove'back] +val hash_map_remove_back_lem + (#t : Type0) (self : hash_map_t_nes t) (key : usize) : + Lemma + (requires (hash_map_t_inv self)) + (ensures ( + match hash_map_remove_back t self key with + | Fail -> False + | Return hm' -> + hash_map_t_inv self /\ + hash_map_same_params hm' self /\ + hash_map_t_slots_v hm' == hash_map_remove_s (hash_map_t_slots_v self) key /\ + // The length is decremented iff the key was in the map + (let len = hash_map_t_len_s self in + let len' = hash_map_t_len_s hm' in + match hash_map_t_find_s self key with + | None -> len = len' + | Some _ -> len = len' + 1))) + +let hash_map_remove_back_lem #t self key = + hash_map_remove_back_lem_refin self key; + hash_map_remove_s_lem (hash_map_t_slots_v self) key |