From f2c90fa184fbb9e79547b7176e9b30287f17b758 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 13 Feb 2022 15:49:30 +0100
Subject: State and prove the final lemma about remove'back

---
 tests/hashmap/Hashmap.Properties.fst | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'tests/hashmap/Hashmap.Properties.fst')

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
-- 
cgit v1.2.3