summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst34
1 files changed, 33 insertions, 1 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 77bfaddb..ce43fc7c 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -2925,6 +2925,7 @@ let rec hash_map_get_mut_in_list_back_lem #t key ls ret =
(**** get_mut *)
+/// Refinement lemma
val hash_map_get_mut_back_lem_refin
(#t : Type0) (self : hash_map_t t{length self.hash_map_slots > 0})
(key : usize) (ret : t) :
@@ -2965,6 +2966,37 @@ let hash_map_get_mut_back_lem_refin #t self key ret =
end
end
+/// Final lemma
+val hash_map_get_mut_back_lem
+ (#t : Type0) (hm : hash_map_t t{length hm.hash_map_slots > 0})
+ (key : usize) (ret : t) :
+ Lemma
+ (requires (
+ Some? (hash_map_t_find_s hm key) /\
+ hash_map_t_inv hm))
+ (ensures (
+ match hash_map_get_mut_back t hm key ret with
+ | Fail -> False
+ | Return hm' ->
+ // Functional spec
+ hash_map_t_slots_v hm' ==
+ hash_map_insert_no_fail_s (hash_map_t_slots_v hm) key ret /\
+ // The invariant is preserved
+ hash_map_t_inv hm' /\
+ // The length is preserved
+ hash_map_t_len_s hm' = hash_map_t_len_s hm /\
+ // [key] maps to [value]
+ hash_map_t_find_s hm' key == Some ret /\
+ // The other bindings are preserved
+ (forall k'. k' <> key ==> hash_map_t_find_s hm' k' == hash_map_t_find_s hm k')))
+
+let hash_map_get_mut_back_lem #t hm key ret =
+ let hm_v = hash_map_t_slots_v hm in
+ hash_map_get_mut_back_lem_refin hm key ret;
+ match hash_map_get_mut_back t hm key ret with
+ | Fail -> assert(False)
+ | Return hm' ->
+ hash_map_insert_no_fail_s_lem hm_v key ret
-//val hash_map_insert_no_resize_s_lem
+(*** remove *)