summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
authorSon Ho2022-02-13 15:49:30 +0100
committerSon Ho2022-02-13 15:49:30 +0100
commitf2c90fa184fbb9e79547b7176e9b30287f17b758 (patch)
treed2e9b40eab0cca4968182119beca348ff9e165d0 /tests/hashmap
parentfd3694d71a03022c7fb1423c7f6fbbd528eeb987 (diff)
State and prove the final lemma about remove'back
Diffstat (limited to 'tests/hashmap')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst23
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