From 03cab42f960860b39108b410c2ca8a06c44186d3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 31 May 2023 11:23:54 +0200
Subject: Prove hash_map_insert_fwd_back_spec

---
 tests/hol4/hashmap/hashmap_PropertiesScript.sml | 60 ++++++++++++++++++++++++-
 1 file changed, 59 insertions(+), 1 deletion(-)

diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 38a1a09c..4eceed97 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -476,7 +476,7 @@ val _ = save_spec_thm "hash_map_clear_fwd_back_spec"
 
 Theorem hash_map_len_spec:
   ∀ hm.
-    hash_map_t_inv hm ⇒
+    hash_map_t_base_inv hm ⇒
     ∃ x. hash_map_len_fwd hm = Return x ∧
     usize_to_int x = len_s hm
 Proof
@@ -1440,6 +1440,64 @@ Proof
 QED
 val _ = save_spec_thm "hash_map_try_resize_fwd_back_spec"
 
+Theorem hash_map_insert_fwd_back_spec:
+  ∀ hm key value.
+    hash_map_t_inv hm ⇒
+    (* We can insert *)
+    (lookup_s hm key = NONE ⇒ len_s hm < usize_max) ⇒
+    ∃ hm1. hash_map_insert_fwd_back hm key value = Return hm1 ∧
+    (* We preserve the invariant *)
+    hash_map_t_inv hm1 ∧
+    (* We updated the binding for key *)
+    lookup_s hm1 key = SOME value /\
+    (* The other bindings are left unchanged *)
+    (!k. k <> key ==> lookup_s hm k = lookup_s hm1 k) ∧
+    (* Reasoning about the length *)
+    (case lookup_s hm key of
+     | NONE => len_s hm1 = len_s hm + 1
+     | SOME _ => len_s hm1 = len_s hm)
+Proof
+  rw [hash_map_insert_fwd_back_def] >>
+  progress
+  >- (fs [hash_map_t_inv_def]) >>
+  gvs [] >>
+  progress >>
+  Cases_on ‘~(usize_gt x a.hash_map_max_load)’ >> fs []
+  >-(
+    gvs [hash_map_t_inv_def, hash_map_same_params_def] >>
+    sg ‘len_s a = usize_to_int a.hash_map_num_entries’
+    >- (fs [hash_map_t_base_inv_def, len_s_def]) >>
+    fs [usize_gt_def] >>
+    sg ‘usize_to_int a.hash_map_num_entries ≤ usize_to_int hm.hash_map_max_load’ >- int_tac >>
+    fs [] >>
+    Cases_on ‘hm.hash_map_max_load_factor’ >> fs []
+  ) >>
+  gvs [] >>
+  progress >>
+  fs [hash_map_just_before_resize_pred_def, usize_gt_def, hash_map_same_params_def] >>
+  (* The length is the same: two cases depending on whether the map was already saturated or not *)
+  fs [hash_map_t_inv_def] >> Cases_on ‘hm.hash_map_max_load_factor’ >> fs [] >>
+  (* Remaining case: the map was not saturated *)
+  (* Reasoning about the length in the cases the key was already present or not *)
+  Cases_on ‘lookup_s hm key’ >> gvs []
+  >-(
+    Cases_on ‘~(len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q ≤ usize_max)’ >> fs []
+    >- int_tac >>
+    (* Not already present: we incremented the length. The map is also not saturated *)
+    disj1_tac >>
+    sg ‘len_s hm ≤ usize_to_int hm.hash_map_max_load’
+    >- (gvs [hash_map_t_base_inv_def, len_s_def]) >>
+    fs [hash_map_t_base_inv_def, len_s_def] >>
+    int_tac
+  ) >>
+  (* The length is the same and the map was not saturated but we resized: contradiction *)
+  exfalso >>
+  sg ‘len_s hm ≤ usize_to_int hm.hash_map_max_load’
+  >- (gvs [hash_map_t_base_inv_def, len_s_def]) >>
+  int_tac  
+QED
+val _ = save_spec_thm "hash_map_insert_fwd_back_spec"
+
 (*
 Theorem nth_mut_fwd_spec:
   !(ls : 't list_t) (i : u32).
-- 
cgit v1.2.3