Make progress on get_mut'back

1 files changed, 20 insertions, 11 deletions

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index b2efece3..a59f297a 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -2914,31 +2914,40 @@ let rec hash_map_get_mut_in_list_back_lem #t key ls ret =
 (**** get_mut *)
 
 val hash_map_get_mut_back_lem
-  (#t : Type0) (self : hash_map_t t) (key : usize) (ret : t) :
+  (#t : Type0) (self : hash_map_t t{length self.hash_map_slots > 0})
+  (key : usize) (ret : t) :
   Lemma
-  (requires (Some? (hash_map_t_find_s self key))
+  (requires (Some? (hash_map_t_find_s self key)))
   (ensures (
     match hash_map_get_mut_back t self key ret with
     | Fail -> False
-    | Return hm' -> hash_map_t_slots_v hm' == hash_map_insert_no_fail hm key ret))
+    | Return hm' ->
+      hash_map_t_slots_v hm' == hash_map_insert_no_fail_s (hash_map_t_slots_v self) key ret))
 
-let hash_map_get_mut_back_lem #t self key =
-  begin match hash_key_back key with
+let hash_map_get_mut_back_lem #t self key ret =
+  begin match hash_key_fwd key with
   | Fail -> ()
   | Return i ->
+    let i0 = self.hash_map_num_entries in
+    let p = self.hash_map_max_load_factor in
+    let i1 = self.hash_map_max_load in
     let v = self.hash_map_slots in
-    let i0 = vec_len (list_t t) v in
-    begin match usize_rem i i0 with
+    let i2 = vec_len (list_t t) v in
+    begin match usize_rem i i2 with
     | Fail -> ()
     | Return hash_mod ->
-      begin match vec_index_back (list_t t) v hash_mod with
+      begin match vec_index_mut_fwd (list_t t) v hash_mod with
       | Fail -> ()
       | Return l ->
         begin
-        hash_map_get_mut_in_list_back_lem key l;
-        match hash_map_get_mut_in_list_back t key l with
+        hash_map_get_mut_in_list_back_lem key l ret;
+        match hash_map_get_mut_in_list_back t key l ret with
         | Fail -> ()
-        | Return x -> ()
+        | Return l0 ->
+          begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+          | Fail -> ()
+          | Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in ()
+          end
         end
       end
     end