Finish the proofs of the hashmap

7 files changed, 1559 insertions, 472 deletions

diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index 2183ef77..fb0c7688 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -16,6 +16,7 @@ val len_def = Define ‘
   len [] : int = 0 /\
   len (x :: ls) : int = 1 + len ls
 ’
+val _ = BasicProvers.export_rewrites ["len_def"]
 
 (* Return the ith element of a list.
 
@@ -117,6 +118,7 @@ Theorem len_append:
 Proof
   rw [len_eq_LENGTH] >> cooper_tac
 QED
+val _ = BasicProvers.export_rewrites ["len_append"]
 
 Theorem append_len_eq:
   (∀l1 l2 l1' l2'.
@@ -129,6 +131,18 @@ Proof
   rw [len_eq_LENGTH] >> fs [APPEND_11_LENGTH]
 QED
 
+Theorem drop_more_than_length:
+  ∀ ls i.
+  len ls ≤ i ⇒
+  drop i ls = []
+Proof
+  Induct_on ‘ls’ >>
+  rw [drop_def] >>
+  qspec_assume ‘ls’ len_pos >> try_tac int_tac >>
+  last_x_assum irule >>
+  int_tac
+QED
+
 (* TODO: prove more theorems, and add rewriting theorems *)
 
 val _ = export_theory ()
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
index da7cdbb3..26f455d6 100644
--- a/backends/hol4/ilistTheory.sig
+++ b/backends/hol4/ilistTheory.sig
@@ -11,6 +11,7 @@ sig
   (*  Theorems  *)
     val append_len_eq : thm
     val drop_eq : thm
+    val drop_more_than_length : thm
     val index_eq : thm
     val index_eq_EL : thm
     val len_append : thm
@@ -62,6 +63,10 @@ sig
           drop i (x::ls) =
           if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then drop (i − 1) ls else x::ls
    
+   [drop_more_than_length]  Theorem
+      
+      ⊢ ∀ls i. len ls ≤ i ⇒ drop i ls = []
+   
    [index_eq]  Theorem
       
       ⊢ (∀x ls. index 0 (x::ls) = x) ∧
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index 84b9b67a..85a627d2 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -15,13 +15,16 @@ sig
     val le_eq_ge : thm
     val lt_eq_gt : thm
     val mul_pos_left_le : thm
+    val mul_pos_left_lt : thm
     val mul_pos_right_le : thm
+    val mul_pos_right_lt : thm
     val not_ge_eq_lt : thm
     val not_gt_eq_le : thm
     val not_le_eq_gt : thm
     val not_lt_eq_ge : thm
     val num_sub_1_eq : thm
     val num_sub_eq : thm
+    val pos_div_pos_ge : thm
     val pos_div_pos_is_pos : thm
     val pos_div_pos_le : thm
     val pos_div_pos_le_init : thm
@@ -30,9 +33,13 @@ sig
     val pos_mod_pos_is_pos : thm
     val pos_mod_pos_le_init : thm
     val pos_mod_pos_lt : thm
+    val pos_mul_2_div_pos_decompose : thm
     val pos_mul_left_pos_le : thm
+    val pos_mul_left_pos_lt : thm
+    val pos_mul_pos_div_pos_decompose : thm
     val pos_mul_pos_is_pos : thm
     val pos_mul_right_pos_le : thm
+    val pos_mul_right_pos_lt : thm
   
   val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -88,10 +95,18 @@ sig
       
       ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y
    
+   [mul_pos_left_lt]  Theorem
+      
+      ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ a * x < a * y
+   
    [mul_pos_right_le]  Theorem
       
       ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a
    
+   [mul_pos_right_lt]  Theorem
+      
+      ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ x * a < y * a
+   
    [not_ge_eq_lt]  Theorem
       
       ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
@@ -116,6 +131,10 @@ sig
       
       ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
    
+   [pos_div_pos_ge]  Theorem
+      
+      ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≥ y ⇒ x / d ≥ y / d
+   
    [pos_div_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
@@ -148,10 +167,22 @@ sig
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y
    
+   [pos_mul_2_div_pos_decompose]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y + x / y ≤ x * 2 / y
+   
    [pos_mul_left_pos_le]  Theorem
       
       ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x
    
+   [pos_mul_left_pos_lt]  Theorem
+      
+      ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < a * x
+   
+   [pos_mul_pos_div_pos_decompose]  Theorem
+      
+      ⊢ ∀x y z. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < z ⇒ x / z + y / z ≤ (x + y) / z
+   
    [pos_mul_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
@@ -160,6 +191,10 @@ sig
       
       ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a
    
+   [pos_mul_right_pos_lt]  Theorem
+      
+      ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < x * a
+   
    
 *)
 end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 4378f9c3..82da4de9 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1702,16 +1702,16 @@ QED
 
 Theorem update_spec:
   ∀ls i y.
-    0 <= i ⇒
-    i < len ls ⇒
     len (update ls i y) = len ls ∧
-    index i (update ls i y) = y ∧
-    ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+    (0 <= i ⇒
+     i < len ls ⇒
+     index i (update ls i y) = y ∧
+     ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls)
 Proof
   Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >>
   try_tac (exfalso >> cooper_tac) >>
   try_tac (
-    pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >>
+    pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >> fs [] >>
     pop_assum sg_premise_tac >- cooper_tac >>
     pop_assum sg_premise_tac >- cooper_tac >>
     rw [])
@@ -1722,6 +1722,13 @@ Proof
     rw [])
 QED
 
+Theorem len_update:
+  ∀ ls i y. len (update ls i y) = len ls
+Proof
+ fs [update_spec]
+QED
+val _ = BasicProvers.export_rewrites ["len_update"]
+
 Theorem index_update_same:
   ∀ls i j y.
     0 <= i ⇒
@@ -1832,6 +1839,18 @@ Proof
   sg_dep_rewrite_all_tac index_update_same >- cooper_tac >> fs []
 QED
 
+Theorem vec_to_list_vec_update:
+  ∀ v i x. vec_to_list (vec_update v i x) = update (vec_to_list v) (usize_to_int i) x
+Proof
+  rw [vec_update_def] >>
+  qspec_assume ‘v’ vec_len_spec >>
+  qspecl_assume [‘v’, ‘i’, ‘x’] vec_update_eq >> fs [] >>
+  qspecl_assume [‘vec_to_list v’, ‘usize_to_int i’, ‘x’] update_len >>
+  sg_dep_rewrite_all_tac mk_vec_axiom >- fs [] >>
+  fs []
+QED
+val _ = export_rewrites ["vec_to_list_vec_update"]
+
 Definition vec_index_fwd_def:
   vec_index_fwd v i =
     if usize_to_int i ≤ usize_to_int (vec_len v)
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 7e03987b..ae7f083d 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -278,6 +278,7 @@ sig
     val isize_sub_eq : thm
     val isize_to_int_int_to_isize_i16_bounds : thm
     val isize_to_int_int_to_isize_unfold : thm
+    val len_update : thm
     val mk_isize_unfold : thm
     val mk_usize_unfold : thm
     val mk_vec_unfold : thm
@@ -349,6 +350,7 @@ sig
     val vec_push_back_unfold : thm
     val vec_to_list_int_bounds : thm
     val vec_to_list_vec_new : thm
+    val vec_to_list_vec_update : thm
     val vec_update_eq : thm
   
   val primitives_grammars : type_grammar.grammar * term_grammar.grammar
@@ -1907,6 +1909,10 @@ sig
             if i16_min ≤ n ∧ n ≤ i16_max then n
             else isize_to_int (int_to_isize n)
    
+   [len_update]  Theorem
+      
+      ⊢ ∀ls i y. len (update ls i y) = len ls
+   
    [mk_isize_unfold]  Theorem
       
       [oracles: DISK_THM] [axioms: isize_bounds] []
@@ -2305,10 +2311,11 @@ sig
    [update_spec]  Theorem
       
       ⊢ ∀ls i y.
-          0 ≤ i ⇒
-          i < len ls ⇒
-          len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧
-          ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+          len (update ls i y) = len ls ∧
+          (0 ≤ i ⇒
+           i < len ls ⇒
+           index i (update ls i y) = y ∧
+           ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls)
    
    [usize_add_eq]  Theorem
       
@@ -2454,6 +2461,15 @@ sig
       [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] []
       ⊢ vec_to_list vec_new = []
    
+   [vec_to_list_vec_update]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: mk_vec_axiom, usize_to_int_bounds,
+       usize_to_int_int_to_usize, usize_bounds, vec_to_list_num_bounds] []
+      ⊢ ∀v i x.
+          vec_to_list (vec_update v i x) =
+          update (vec_to_list v) (usize_to_int i) x
+   
    [vec_update_eq]  Theorem
       
       [oracles: DISK_THM]
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 4eceed97..68ed2d4e 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -12,8 +12,8 @@ Theorem EVERY_quant_equiv:
   ∀p ls. EVERY p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
 Proof
   strip_tac >> Induct_on ‘ls’
-  >-(rw [EVERY_DEF, len_def] >> int_tac) >>
-  rw [EVERY_DEF, len_def, index_eq] >>
+  >-(rw [EVERY_DEF] >> int_tac) >>
+  rw [EVERY_DEF, index_eq] >>
   equiv_tac
   >-(
     rw [] >>
@@ -38,8 +38,8 @@ Theorem pairwise_rel_quant_equiv:
     (∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls))
 Proof
   strip_tac >> Induct_on ‘ls’
-  >-(rw [pairwise_rel_def, len_def] >> int_tac) >>
-  rw [pairwise_rel_def, len_def] >>
+  >-(rw [pairwise_rel_def] >> int_tac) >>
+  rw [pairwise_rel_def] >>
   equiv_tac
   >-(
     (* ==> *)
@@ -74,6 +74,12 @@ Proof
   fs []
 QED
 
+(* TODO: the context tends to quickly saturate. In particular:
+   - sg_prove_premise_tac leaves the proven assumption in the context, while it shouldn't
+   - maybe massage shouldn't leave the introduced inequalities in the context: it is very noisy.
+     For instance, int_tac could introduce those inequalities.
+ *)
+
 Type key_t = “:usize”
 
 val distinct_keys_def = Define ‘
@@ -86,27 +92,33 @@ Definition list_t_v_def:
   (list_t_v (ListNil : 't list_t) : (key_t # 't) list = []) /\
   (list_t_v (ListCons k v tl) = (k, v) :: list_t_v tl)
 End
+val _ = export_rewrites ["list_t_v_def"]
 
 (* Invariants *)
+(* TODO: add to srw_ss *)
 Definition lookup_def:
   lookup key [] = NONE /\
   lookup key ((k, v) :: ls) =
     if k = key then SOME v else lookup key ls
 End
+val _ = export_rewrites ["lookup_def"]
 
 Definition slot_t_lookup_def:
   slot_t_lookup key ls = lookup key (list_t_v ls)
 End
+val _ = export_rewrites ["slot_t_lookup_def"]
 
 Definition remove_def:
   remove key [] = [] ∧
   remove key ((k, v) :: ls) =
     if k = key then ls else (k, v) :: remove key ls
 End
+val _ = export_rewrites ["remove_def"]
 
 Definition slot_t_remove_def:
   slot_t_remove key ls = remove key (list_t_v ls)
 End
+val _ = export_rewrites ["slot_t_remove_def"]
 
 Definition hash_mod_key_def:
   hash_mod_key k (l : int) : int =
@@ -114,11 +126,14 @@ Definition hash_mod_key_def:
     | Return k => usize_to_int k % l
     | _ => ARB
 End
+val _ = export_rewrites ["hashmap_Funs.hash_key_fwd_def", "hash_mod_key_def"]
+val _ = export_rewrites ["primitives.mem_replace_fwd_def", "primitives.mem_replace_back_def"]
 
 Definition slot_s_inv_hash_def:
   slot_s_inv_hash (l : int) (i : int) (ls : (key_t # 'b) list) : bool =
     ∀ k v. MEM (k, v) ls ⇒ hash_mod_key k l = i
 End
+val _ = export_rewrites ["slot_s_inv_hash_def"]
 
 Definition slot_s_inv_def:
   slot_s_inv (l : int) (i : int) (ls : (key_t # 'b) list) : bool = (
@@ -126,6 +141,7 @@ Definition slot_s_inv_def:
     slot_s_inv_hash l i ls
   )
 End
+val _ = export_rewrites ["slot_s_inv_def"]
 
 (* TODO: try with this invariant:
 
@@ -159,6 +175,7 @@ Definition slots_s_inv_def:
   slots_s_inv (s : 'a list_t list) =
     ∀ (i : int). 0 ≤ i ⇒ i < len s ⇒ slot_t_inv (len s) i (index i s)
 End
+val _ = export_rewrites ["slots_s_inv_def"]
 
 Definition slots_t_inv_def:
   slots_t_inv (s : 'a list_t vec) = slots_s_inv (vec_to_list s)
@@ -173,6 +190,7 @@ Definition hash_map_t_base_inv_def:
     slots_t_inv hm.hash_map_slots ∧
     (* The capacity must be > 0 (otherwise we can't resize, because when we
        resize we multiply the capacity by two) *)
+    (* TODO: write it as 0 < ... *)
     len (vec_to_list hm.hash_map_slots) > 0 ∧
     (* Load computation *)
     (let capacity = len (vec_to_list hm.hash_map_slots) in
@@ -270,7 +288,7 @@ Proof
     sg ‘v = usize_to_int n - 1’ >- int_tac >> fs [] >>
     (* *)
     progress >>
-    fs [vec_len_def, len_append, len_def] >>
+    fs [vec_len_def] >>
     int_tac
   ) >>
   fs [] >>
@@ -288,11 +306,11 @@ Theorem hash_map_allocate_slots_fwd_spec:
 Proof
   rw [] >>
   pure_once_rewrite_tac [hash_map_allocate_slots_fwd_def] >>
-  progress >> gvs [len_def, slots_t_inv_def, slots_s_inv_def, slot_s_inv_hash_def] >>
-  rw [slot_t_inv_def, slot_s_inv_def, slot_s_inv_hash_def]
-  >- fs [EVERY_quant_equiv, distinct_keys_def, pairwise_rel_def, list_t_v_def] >>
+  progress >> gvs [slots_t_inv_def] >>
+  rw [slot_t_inv_def]
+  >- fs [EVERY_quant_equiv, distinct_keys_def, pairwise_rel_def] >>
   fs [EVERY_quant_equiv] >>
-  qpat_assum ‘∀i. _’ sg_dep_rewrite_all_tac >> gvs [list_t_v_def]
+  qpat_assum ‘∀i. _’ sg_dep_rewrite_all_tac >> gvs []
 QED
 val _ = save_spec_thm "hash_map_allocate_slots_fwd_spec"
 
@@ -300,7 +318,7 @@ val _ = save_spec_thm "hash_map_allocate_slots_fwd_spec"
 Theorem FLAT_ListNil_is_nil:
   EVERY (λx. x = ListNil) ls ⇒ FLAT (MAP list_t_v ls) = []
 Proof
-  Induct_on ‘ls’ >> fs [list_t_v_def]
+  Induct_on ‘ls’ >> fs []
 QED
 
 Theorem hash_map_new_with_capacity_fwd_spec:
@@ -323,27 +341,27 @@ Proof
   progress >>
   gvs [hash_map_t_inv_def, hash_map_t_base_inv_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
   rw []
-  >-(massage >> sg_dep_rewrite_goal_tac FLAT_ListNil_is_nil >> fs [len_def])
+  >-(massage >> sg_dep_rewrite_goal_tac FLAT_ListNil_is_nil >> fs [])
   >-(int_tac)
   >-(massage >> metis_tac [])
   >-(fs [len_s_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
-     sg_dep_rewrite_goal_tac FLAT_ListNil_is_nil >> fs [len_def]) >>
-  fs [lookup_s_def, slots_t_lookup_def, slot_t_lookup_def] >>
+     sg_dep_rewrite_goal_tac FLAT_ListNil_is_nil >> fs []) >>
+  fs [lookup_s_def, slots_t_lookup_def] >>
   fs [EVERY_quant_equiv] >>
   (* TODO: sg_dep_rewrite_goal_tac does weird things here *)
   first_x_assum (qspec_assume ‘hash_mod_key k (usize_to_int capacity)’) >>
   first_x_assum sg_premise_tac
   >- (
-    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    fs [] >>
     massage >>
     irule pos_mod_pos_is_pos >> fs []) >>
   first_x_assum sg_premise_tac
   >-(
-    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    fs [] >>
     massage >>
     irule pos_mod_pos_lt >> fs []
   ) >>  
-  fs [list_t_v_def, lookup_def]
+  fs []
 QED
 val _ = save_spec_thm "hash_map_new_with_capacity_fwd_spec"
 
@@ -442,19 +460,19 @@ Proof
   rw [hash_map_clear_fwd_back_def] >>
   progress >>
   fs [len_s_def, hash_map_t_al_v_def, hash_map_t_v_def, lookup_s_def] >>
-  fs [slots_t_lookup_def, slot_t_lookup_def, len_def] >> rw []
+  fs [slots_t_lookup_def] >> rw []
   >-((* Prove that the invariant is preserved *)
-   fs [hash_map_t_inv_def, hash_map_t_base_inv_def, hash_map_t_al_v_def, hash_map_t_v_def, len_def] >>
+   fs [hash_map_t_inv_def, hash_map_t_base_inv_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
    massage >> fs [] >>
    conj_tac
    >-(
-     fs [slots_t_inv_def, slots_s_inv_def] >>
-     rw [slot_t_inv_def, slot_s_inv_def, slot_s_inv_hash_def, list_t_v_def, distinct_keys_def, pairwise_rel_def]) >>
+     fs [slots_t_inv_def] >>
+     rw [slot_t_inv_def, distinct_keys_def, pairwise_rel_def]) >>
    Cases_on ‘hm.hash_map_max_load_factor’ >> gvs [] >>
    disj1_tac >>
    irule pos_div_pos_is_pos >>
    int_tac) >>
-  fs [hash_mod_key_def, hash_key_fwd_def] >>
+  fs [] >>
   (* TODO: would like to do: qpat_assum ‘∀j. _’ sg_dep_rewrite_goal_tac >> *)
   first_x_assum (qspec_assume ‘usize_to_int k % len (vec_to_list hm.hash_map_slots)’) >>
   fs [] >>
@@ -465,7 +483,7 @@ Proof
   >-(fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
   fs [] >>
   sg ‘~(len (vec_to_list hm.hash_map_slots) < 0)’ >- int_tac >>
-  fs [list_t_v_def, lookup_def]
+  fs []
 QED
 val _ = save_spec_thm "hash_map_clear_fwd_back_spec"
   
@@ -495,7 +513,7 @@ Theorem hash_map_insert_in_list_loop_fwd_spec:
     (b ⇔ slot_t_lookup key ls = NONE)
 Proof
   Induct_on ‘ls’ >> pure_once_rewrite_tac [hash_map_insert_in_list_loop_fwd_def] >>
-  fs [slot_t_lookup_def, lookup_def, list_t_v_def] >>
+  fs [] >>
   rw []
 QED
 val _ = save_spec_thm "hash_map_insert_in_list_loop_fwd_spec"
@@ -524,17 +542,13 @@ Theorem hash_map_insert_in_list_loop_back_spec_aux:
      | NONE => len (list_t_v ls1) = len (list_t_v ls) + 1
      | SOME _ => len (list_t_v ls1) = len (list_t_v ls))
 Proof
-  Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >>
+  Induct_on ‘ls’ >> rw [] >~ [‘ListNil’] >>
   pure_once_rewrite_tac [hash_map_insert_in_list_loop_back_def]
-  >- (rw [slot_t_lookup_def, lookup_def, list_t_v_def, len_def, slot_s_inv_hash_def]) >>
-  fs [] >>
-  case_tac >> fs []
-  >-(fs [slot_t_lookup_def, lookup_def, list_t_v_def, len_def, slot_s_inv_hash_def] >>
-     metis_tac []) >>
-  progress >>
-  fs [slot_t_lookup_def, lookup_def, list_t_v_def, len_def] >>
-  rw []
-  >-(fs [slot_s_inv_hash_def] >> metis_tac []) >>
+  >- (rw []) >>
+  fs [] >- metis_tac [] >>
+  progress >> fs [] >> rw []
+  >- (metis_tac [])
+  >- (metis_tac []) >>
   case_tac >> fs [] >> int_tac
 QED
 
@@ -548,13 +562,13 @@ Theorem hash_map_insert_in_list_loop_back_EVERY_distinct_keys:
   EVERY (λy. k1 ≠ FST y) (list_t_v ls1)
 Proof
   Induct_on ‘ls0’ >> rw [pairwise_rel_def] >~ [‘ListNil’] >>
-  gvs [list_t_v_def, pairwise_rel_def, EVERY_DEF]
-  >-(gvs [MK_BOUNDED hash_map_insert_in_list_loop_back_def 1, bind_def, list_t_v_def, EVERY_DEF]) >>
+  gvs [pairwise_rel_def, EVERY_DEF]
+  >-(gvs [MK_BOUNDED hash_map_insert_in_list_loop_back_def 1, bind_def, EVERY_DEF]) >>
   pat_undisch_tac ‘hash_map_insert_in_list_loop_back _ _ _ = _’ >>
   simp [MK_BOUNDED hash_map_insert_in_list_loop_back_def 1, bind_def] >>
-  Cases_on ‘u = k’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, EVERY_DEF] >>
+  Cases_on ‘u = k’ >> rw [] >> gvs [pairwise_rel_def, EVERY_DEF] >>
   Cases_on ‘hash_map_insert_in_list_loop_back k v ls0’ >>
-  gvs [distinct_keys_def, list_t_v_def, pairwise_rel_def, EVERY_DEF] >>
+  gvs [distinct_keys_def, pairwise_rel_def, EVERY_DEF] >>
   metis_tac []
 QED
 
@@ -566,14 +580,14 @@ Theorem hash_map_insert_in_list_loop_back_distinct_keys:
 Proof
   Induct_on ‘ls0’ >> rw [distinct_keys_def] >~ [‘ListNil’]
   >-(
-    fs [list_t_v_def, hash_map_insert_in_list_loop_back_def] >>
-    gvs [list_t_v_def, pairwise_rel_def, EVERY_DEF]) >>
+    fs [hash_map_insert_in_list_loop_back_def] >>
+    gvs [pairwise_rel_def, EVERY_DEF]) >>
   last_x_assum (qspecl_assume [‘k’, ‘v’]) >>
   pat_undisch_tac ‘hash_map_insert_in_list_loop_back _ _ _ = _’ >>
   simp [MK_BOUNDED hash_map_insert_in_list_loop_back_def 1, bind_def] >>
-  Cases_on ‘u = k’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, EVERY_DEF] >>
+  Cases_on ‘u = k’ >> rw [] >> gvs [pairwise_rel_def, EVERY_DEF] >>
   Cases_on ‘hash_map_insert_in_list_loop_back k v ls0’ >>
-  gvs [distinct_keys_def, list_t_v_def, pairwise_rel_def, EVERY_DEF] >>
+  gvs [distinct_keys_def, pairwise_rel_def, EVERY_DEF] >>
   metis_tac [hash_map_insert_in_list_loop_back_EVERY_distinct_keys]
 QED
 
@@ -599,11 +613,11 @@ Theorem hash_map_insert_in_list_loop_back_spec:
     (∀l. slot_s_inv_hash l (hash_mod_key key l) (list_t_v ls) ⇒
      insert_in_slot_t_rel l key value ls ls1)
 Proof
-  rw [slot_t_inv_def, slot_s_inv_def] >>
+  rw [slot_t_inv_def] >>
   qspecl_assume [‘ls’, ‘key’, ‘value’] hash_map_insert_in_list_loop_back_spec_aux >>
   fs [] >>
   qspecl_assume [‘key’, ‘value’, ‘ls’, ‘ls1’] hash_map_insert_in_list_loop_back_distinct_keys >>
-  gvs [insert_in_slot_t_rel_def, slot_t_inv_def, slot_s_inv_def]
+  gvs [insert_in_slot_t_rel_def, slot_t_inv_def] >> metis_tac []
 QED
 val _ = save_spec_thm "hash_map_insert_in_list_loop_back_spec"
 
@@ -655,6 +669,7 @@ Proof
   fs [hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_slots_fupd_def] >>
   fs [hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def]
 QED
+val hash_map_insert_no_resize_fwd_back_branches_eq = SIMP_RULE (srw_ss ()) [] hash_map_insert_no_resize_fwd_back_branches_eq
 
 Theorem hash_map_cond_incr_thm:
   ∀ hm key a.
@@ -713,14 +728,15 @@ Proof
   fs [hash_map_insert_no_resize_fwd_back_branches_eq] >>
   qspecl_assume [‘hm’, ‘key’, ‘a’] hash_map_cond_incr_thm >> gvs [] >>
   pop_assum sg_premise_tac
-  >- (fs [lookup_s_def, slots_t_lookup_def, slot_t_lookup_def, hash_mod_key_def, hash_key_fwd_def, vec_index_def, int_rem_def]) >>
+  >- (fs [lookup_s_def, slots_t_lookup_def, vec_index_def, int_rem_def]) >>
   fs [] >>
   (* TODO: lemma? *)
   sg ‘let l = len (vec_to_list hm.hash_map_slots) in
       slot_t_inv l (usize_to_int key % l) (index (usize_to_int key % l) (vec_to_list hm.hash_map_slots))’
-  >-(fs [hash_map_t_base_inv_def, slots_t_inv_def, slots_s_inv_def] >>
+  >-(fs [hash_map_t_base_inv_def, slots_t_inv_def] >>
      last_x_assum (qspec_assume ‘usize_to_int a’) >>
-     gvs [vec_index_def, int_rem_def, slot_t_inv_def, slot_s_inv_def]) >>
+     gvs [vec_index_def, int_rem_def, slot_t_inv_def] >>
+     metis_tac []) >>
   fs [] >>
   sg ‘usize_to_int a = usize_to_int key % len (vec_to_list hm.hash_map_slots)’
   >-(fs [int_rem_def]) >>
@@ -728,7 +744,7 @@ Proof
   >-(fs [int_rem_def]) >>
   fs [] >>
   sg ‘distinct_keys (list_t_v (vec_index hm.hash_map_slots a))’
-  >-(fs [slot_t_inv_def, slot_s_inv_def, vec_index_def]) >>
+  >-(fs [slot_t_inv_def, vec_index_def]) >>
   fs [hash_map_insert_in_list_back_def] >>
   progress >>
   progress >- ((* TODO: *) massage >> fs []) >>
@@ -737,12 +753,9 @@ Proof
   (* Prove the post-condition *)
   qexists ‘a'’ >>
   rw [hash_map_same_params_def]
-  >-(gvs [insert_in_slot_t_rel_def, hash_mod_key_def, hash_key_fwd_def, vec_index_def, vec_update_def, slot_t_inv_def, slot_s_inv_def] >>
-     metis_tac [])
-  >-(
-    fs [hash_mod_key_def, hash_key_fwd_def, vec_index_def, vec_update_def] >>
-    sg_dep_rewrite_goal_tac mk_vec_axiom >> gvs []) >>
-  gvs [lookup_s_def, slots_t_lookup_def, slot_t_lookup_def, hash_mod_key_def, hash_key_fwd_def, vec_index_def] >>
+  >-(gvs [insert_in_slot_t_rel_def, vec_index_def, vec_update_def, slot_t_inv_def] >>
+     metis_tac []) >>
+  gvs [lookup_s_def, slots_t_lookup_def, vec_index_def] >>
   case_tac >> fs []
 QED
 
@@ -755,12 +768,12 @@ Theorem len_FLAT_MAP_update:
 Proof
   strip_tac >>
   Induct_on ‘ls’
-  >-(rw [len_def] >> int_tac) >>
+  >-(rw [] >> int_tac) >>
   rw [] >>
-  fs [len_def, index_def, update_def] >>
-  Cases_on ‘i = 0’ >> fs [len_append]
+  fs [index_def, update_def] >>
+  Cases_on ‘i = 0’ >> fs []
   >- int_tac >>
-  sg ‘0 < i’ >- int_tac >> fs [len_append] >>
+  sg ‘0 < i’ >- int_tac >> fs [] >>
   first_x_assum (qspec_assume ‘i - 1’) >>
   fs [] >>
   (* TODO: automate *)
@@ -804,39 +817,39 @@ Proof
     rw []
     >-(
       sg_dep_rewrite_goal_tac len_FLAT_MAP_update
-      >-(fs [hash_mod_key_def, hash_key_fwd_def]) >>
+      >-(fs []) >>
       fs [insert_in_slot_t_rel_def] >>
-      fs [hash_mod_key_def, hash_key_fwd_def] >>
+      fs [] >>
       Cases_on ‘lookup_s hm key’ >>
-      fs [lookup_s_def, slots_t_lookup_def, slot_t_lookup_def, hash_mod_key_def, hash_key_fwd_def] >>
+      fs [lookup_s_def, slots_t_lookup_def] >>
       int_tac) >>
-    fs [slots_t_inv_def, slots_s_inv_def] >>
+    fs [slots_t_inv_def] >>
     rw [] >>
     (* Proof of the slot property: has the slot been updated∃ *)
     Cases_on ‘i = hash_mod_key key (len (vec_to_list hm.hash_map_slots))’ >> fs []
     >-(
       sg_dep_rewrite_goal_tac index_update_diff
-      >-(fs [hash_mod_key_def, hash_key_fwd_def]) >>
+      >-(fs []) >>
       fs [insert_in_slot_t_rel_def]) >>
     sg_dep_rewrite_goal_tac index_update_same
-    >-(fs [hash_mod_key_def, hash_key_fwd_def]) >>
+    >-(fs []) >>
     fs []) >>
   (* Prove the rest of the postcondition *)
   rw []
   >-((* The binding for key is updated *)
      fs [lookup_s_def, slots_t_lookup_def] >>
      sg_dep_rewrite_goal_tac index_update_diff
-     >-(fs [hash_mod_key_def, hash_key_fwd_def]) >>
+     >-(fs []) >>
      fs [insert_in_slot_t_rel_def])
   >-((* The other bindings are unchanged *)
      fs [lookup_s_def, slots_t_lookup_def] >>
      Cases_on ‘hash_mod_key k (len (vec_to_list hm.hash_map_slots)) = hash_mod_key key (len (vec_to_list hm.hash_map_slots))’ >> gvs []
      >-(
         sg_dep_rewrite_goal_tac index_update_diff
-        >-(fs [hash_mod_key_def, hash_key_fwd_def]) >>
+        >-(fs []) >>
         fs [insert_in_slot_t_rel_def]) >>
      sg_dep_rewrite_goal_tac index_update_same
-     >-(fs [hash_mod_key_def, hash_key_fwd_def] >> irule pos_mod_pos_lt >> massage >> fs []) >>
+     >-(fs [] >> irule pos_mod_pos_lt >> massage >> fs []) >>
      fs [insert_in_slot_t_rel_def]) >>
   (* Length *)
   Cases_on ‘lookup_s hm key’ >>
@@ -862,8 +875,8 @@ Theorem distinct_keys_lookup_NONE:
   lookup k ls = NONE
 Proof
   Induct_on ‘ls’ >> rw [] >>
-  fs [distinct_keys_def, pairwise_rel_def, EVERY_DEF, lookup_def] >>
-  Cases_on ‘h’ >> fs [lookup_def]
+  fs [distinct_keys_def, pairwise_rel_def, EVERY_DEF] >>
+  Cases_on ‘h’ >> fs []
 QED
 
 Theorem hash_map_move_elements_from_list_fwd_back_spec:
@@ -886,14 +899,11 @@ Proof
   (* TODO: improve massage to not only look at variables *)
   qspec_assume ‘hm.hash_map_num_entries’ usize_to_int_bounds >> fs [] >>
   (* TODO: automate *)
-  qspec_assume ‘list_t_v ls’ len_pos
-  >-(fs [slot_t_lookup_def, lookup_def, list_t_v_def])
-  >-(fs [len_def, list_t_v_def]) >>
+  qspec_assume ‘list_t_v ls’ len_pos >>
   (* Recursive case *)
+  progress >>
   progress
-  >-(fs [len_s_def, hash_map_t_base_inv_def, list_t_v_def, len_def] >> int_tac) >>
-  progress
-  >-(Cases_on ‘lookup_s hm u’ >> fs [len_s_def, hash_map_t_base_inv_def, list_t_v_def, len_def] >> int_tac) >>
+  >-(Cases_on ‘lookup_s hm u’ >> fs [len_s_def, hash_map_t_base_inv_def] >> int_tac) >>
   (* Prove the postcondition *)
   (* Drop the induction hypothesis *)
   last_x_assum ignore_tac >>
@@ -905,7 +915,7 @@ Proof
   fs [hash_map_same_params_def] >>
   (* *)
   sg ‘distinct_keys (list_t_v ls)’
-  >-(fs [distinct_keys_def, list_t_v_def, pairwise_rel_def, EVERY_DEF]) >>
+  >-(fs [distinct_keys_def, pairwise_rel_def, EVERY_DEF]) >>
   fs [] >>
   (* For some reason, if we introduce an assumption with [sg], the rewriting
      doesn't work (and I couldn't find any typing issue) *)
@@ -913,53 +923,33 @@ Proof
   first_assum sg_premise_tac
   >-(
     rw [] >>
-    sg ‘k ≠ u’ >-(irule distinct_keys_MEM_not_eq >> metis_tac [list_t_v_def]) >>
+    sg ‘k ≠ u’ >-(irule distinct_keys_MEM_not_eq >> metis_tac []) >>
     last_x_assum (qspec_assume ‘k’) >>
     gvs [] >>
     first_x_assum (qspecl_assume [‘k’, ‘v’]) >>
-    gvs [list_t_v_def]) >>
+    gvs []) >>
   gvs[] >>
   (* *)
   rw []
   >-(
-    sg ‘k ≠ u’ >-(fs [slot_t_lookup_def, lookup_def, list_t_v_def] >> Cases_on ‘u = k’ >> fs []) >>
-    last_x_assum (qspec_assume ‘k’) >> gvs [] >>
     first_x_assum (qspec_assume ‘k’) >>
     first_x_assum (qspec_assume ‘k’) >>
-    gvs [slot_t_lookup_def, list_t_v_def, lookup_def])
-  >-(
-    first_x_assum (qspec_assume ‘k’) >>
-    first_x_assum (qspec_assume ‘k’) >>
-    fs [slot_t_lookup_def, list_t_v_def, lookup_def] >>
-    Cases_on ‘u = k’ >> gvs [] >>  
+    fs [] >>
     sg ‘lookup k (list_t_v ls) = NONE’ >-(irule distinct_keys_lookup_NONE >> metis_tac []) >>
-    fs []) >>
+    gvs []) >>
   (* The length *)
-  fs [len_def, list_t_v_def] >>
+  fs [] >>
   int_tac
 QED
 val _ = save_spec_thm "hash_map_move_elements_from_list_fwd_back_spec"
 
-(* TODO: move *)
-Theorem drop_more_than_length:
-  ∀ ls i.
-  len ls ≤ i ⇒
-  drop i ls = []
-Proof
-  Induct_on ‘ls’ >>
-  rw [len_def, drop_def] >>
-  qspec_assume ‘ls’ len_pos >> try_tac int_tac >>
-  last_x_assum irule >>
-  int_tac
-QED
-
 (* TODO: induction theorem for vectors *)
 Theorem len_index_FLAT_MAP_list_t_v:
   ∀ slots i.
     0 ≤ i ⇒ i < len slots ⇒
     len (list_t_v (index i slots)) ≤ len (FLAT (MAP list_t_v (drop i slots)))
 Proof
-  Induct_on ‘slots’ >> rw [vec_index_def, drop_def, index_def, len_def, len_append, len_pos, update_def, drop_eq] >> try_tac int_tac >> fs [] >>
+  Induct_on ‘slots’ >> rw [vec_index_def, drop_def, index_def, len_pos, update_def, drop_eq] >> try_tac int_tac >> fs [] >>
   last_x_assum (qspec_assume ‘i - 1’) >>
   sg ‘0 ≤ i − 1 ∧ i − 1 < len slots’ >- int_tac >> fs []
 QED
@@ -971,24 +961,11 @@ Theorem len_vec_FLAT_drop_update:
   len (list_t_v (index i slots)) +
   len (FLAT (MAP list_t_v (drop (i + 1) (update slots i ListNil))))
 Proof
-  Induct_on ‘slots’ >> fs [len_def, drop_def, update_def, len_append, len_pos, index_def] >> rw [] >> try_tac int_tac >> fs [drop_eq, len_append] >>
+  Induct_on ‘slots’ >> fs [drop_def, update_def, len_pos, index_def] >> rw [] >> try_tac int_tac >> fs [drop_eq, len_append] >>
   last_x_assum (qspec_assume ‘i - 1’) >>
   sg ‘0 ≤ i − 1 ∧ i − 1 < len slots ∧ ~(i + 1 < 0) ∧ ~(i + 1 = 0)’ >- int_tac >> fs [] >> sg ‘i + 1 - 1 = i’ >- int_tac >> fs [drop_def]
 QED
 
-(* TODO: move *)
-(* TODO: add to srw_ss () ? *)
-Theorem vec_to_list_vec_update:
-  ∀ v i x. vec_to_list (vec_update v i x) = update (vec_to_list v) (usize_to_int i) x
-Proof
-  rw [vec_update_def] >>
-  qspec_assume ‘v’ vec_len_spec >>
-  qspecl_assume [‘v’, ‘i’, ‘x’] vec_update_eq >> fs [] >>
-  qspecl_assume [‘vec_to_list v’, ‘usize_to_int i’, ‘x’] update_len >>
-  sg_dep_rewrite_all_tac mk_vec_axiom >- fs [] >>
-  fs []  
-QED
-
 Theorem MEM_EVERY_not:
   ∀ k v ls.
     MEM (k, v) ls ⇒
@@ -1006,9 +983,9 @@ Theorem MEM_distinct_keys_lookup:
     distinct_keys ls ⇒
     lookup k ls = SOME v
 Proof
-  Induct_on ‘ls’ >> fs [lookup_def, distinct_keys_def, pairwise_rel_def] >>
-  rw [lookup_def] >> fs [lookup_def] >>
-  Cases_on ‘h’ >> fs [lookup_def] >> rw [] >>
+  Induct_on ‘ls’ >> fs [distinct_keys_def, pairwise_rel_def] >>
+  rw [] >> fs [] >>
+  Cases_on ‘h’ >> fs [] >> rw [] >>
   (* Absurd *)
   exfalso >>
   metis_tac [MEM_EVERY_not]
@@ -1020,9 +997,9 @@ Theorem lookup_distinct_keys_MEM:
     distinct_keys ls ⇒
     MEM (k, v) ls
 Proof
-  Induct_on ‘ls’ >> fs [lookup_def, distinct_keys_def, pairwise_rel_def] >>
-  rw [lookup_def] >> fs [lookup_def] >>
-  Cases_on ‘h’ >> fs [lookup_def] >> rw [] >>
+  Induct_on ‘ls’ >> fs [distinct_keys_def, pairwise_rel_def] >>
+  rw [] >> fs [] >>
+  Cases_on ‘h’ >> fs [] >> rw [] >>
   Cases_on ‘q = k’ >> fs []
 QED
 
@@ -1036,23 +1013,23 @@ Theorem key_MEM_j_lookup_i_is_NONE:
   slot_t_lookup k (index (usize_to_int i) (vec_to_list slots)) = NONE
 Proof
   rw [] >>
-  fs [slot_t_inv_def, slot_s_inv_def, slot_s_inv_hash_def] >>
+  fs [slot_t_inv_def] >>
   (* *)
   first_assum (qspec_assume ‘j’) >> fs [] >>
   pop_assum sg_premise_tac >- int_tac >> fs [] >>
   first_x_assum imp_res_tac >>
-  fs [hash_mod_key_def, hash_key_fwd_def] >>
+  fs [] >>
   (* Prove by contradiction *)
   first_assum (qspec_assume ‘usize_to_int i’) >> fs [] >>
   pop_assum sg_premise_tac >- int_tac >> fs [] >>
   Cases_on ‘slot_t_lookup k (index (usize_to_int i) (vec_to_list slots))’ >> fs [] >>
   sg ‘MEM (k,v) (list_t_v (index (usize_to_int i) (vec_to_list slots)))’
   >- (
-    fs [slot_t_lookup_def] >>
+    fs [] >>
     metis_tac [lookup_distinct_keys_MEM]
   ) >>
   qpat_x_assum ‘∀k. _’ imp_res_tac >>
-  fs [hash_mod_key_def, hash_key_fwd_def]
+  fs []
 QED  
 
 (* TODO: the names introduced by progress are random, which is confusing.
@@ -1095,31 +1072,31 @@ Proof
   massage
   >-(
     case_tac >- int_tac >> fs [] >>
-    sg_dep_rewrite_goal_tac drop_more_than_length >-(int_tac) >> fs [len_def] >>
+    sg_dep_rewrite_goal_tac drop_more_than_length >-(int_tac) >> fs [] >>
     strip_tac >> Cases_on ‘lookup_s hm k’ >> fs [] >>
-    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    fs [] >>
     (* Contradiction *)
     rw [] >> int_tac
     )
   >-(
     (* Same as above - TODO: this is a bit annoying, update the invariant principle (maybe base case is ≤ 0 ?) *)
-    sg_dep_rewrite_goal_tac drop_more_than_length >-(int_tac) >> fs [len_def] >>
+    sg_dep_rewrite_goal_tac drop_more_than_length >-(int_tac) >> fs [] >>
     strip_tac >> Cases_on ‘lookup_s hm k’ >> fs [] >>
-    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    fs [] >>
     (* Contradiction *)
     rw [] >> int_tac) >>
   (* Recursive case *)
   case_tac >> fs [] >>
   (* Eliminate the trivial case *)
   try_tac (
-    sg_dep_rewrite_goal_tac drop_more_than_length >-(int_tac) >> fs [len_def] >>
+    sg_dep_rewrite_goal_tac drop_more_than_length >-(int_tac) >> fs [] >>
     strip_tac >> Cases_on ‘lookup_s hm k’ >> fs [] >>
-    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    fs [] >>
     (* Contradiction *)
     rw [] >> int_tac) >>
   progress >- (fs [vec_len_def] >> massage >> fs []) >>
   progress >- (
-    fs [mem_replace_fwd_def, vec_index_def] >>
+    fs [vec_index_def] >>
     qspecl_assume [‘vec_to_list slots’, ‘usize_to_int i’] len_index_FLAT_MAP_list_t_v >>
     gvs [] >> int_tac) >>
   (* We just evaluated the call to “hash_map_move_elements_from_list_fwd_back”: prove the assumptions
@@ -1127,27 +1104,26 @@ Proof
   qpat_x_assum ‘_ ⇒ _’ sg_premise_tac
   >-(
     first_x_assum (qspec_assume ‘usize_to_int i’) >> gvs [vec_index_def] >>
-    rw [mem_replace_fwd_def]
+    rw []
     >-(first_x_assum irule >> metis_tac []) >>
-    fs [slot_t_inv_def, slot_s_inv_def]) >>
-  gvs [mem_replace_fwd_def] >>
+    fs [slot_t_inv_def]) >>
+  gvs [] >>
   (* Continue going forward *)
   progress >>
   progress >- (fs [vec_len_def] >> massage >> fs []) >>
-  progress >> fs [mem_replace_back_def, mem_replace_fwd_def] >> qspecl_assume [‘slots’, ‘i’, ‘ListNil’] vec_update_eq >>
+  progress >> fs [] >> qspecl_assume [‘slots’, ‘i’, ‘ListNil’] vec_update_eq >>
   gvs [] >>
   (* Drop the induction hypothesis *)
   last_x_assum ignore_tac
   (* TODO: when we update the theorem, progress lookups the stored (deprecated) rather than
      the inductive hypothesis *)
   (* The preconditions of the recursive call *)
-  >- (int_tac)
   >- (
     qspecl_assume [‘vec_to_list slots’, ‘usize_to_int i’] len_vec_FLAT_drop_update >> gvs [] >>
-    gvs [vec_to_list_vec_update, vec_index_def] >>
+    gvs [vec_index_def] >>
     int_tac)
   >-(
-    fs [vec_to_list_vec_update] >>
+    fs [] >>
     sg_dep_rewrite_goal_tac index_update_same
     >-(fs [] >> int_tac) >>
     fs [] >>
@@ -1158,17 +1134,18 @@ Proof
     (* Prove that index j (update slots i) = index j slots *)
     pop_assum (qspec_assume ‘int_to_usize j’) >> gvs [] >> massage >> gvs [] >>
     fs [vec_len_def] >>
-    fs [vec_to_list_vec_update] >>
     massage >> gvs [] >>
     sg ‘j ≠ usize_to_int i’ >- int_tac >> gvs [vec_index_def, vec_update_def] >>
     massage >>
-    sg_dep_rewrite_all_tac mk_vec_axiom >- fs [] >> gvs [] >>
     (* Use the fact that slot_t_lookup k (index i ... slots) = NONE *)
     last_x_assum (qspec_assume ‘k’) >>
     first_assum sg_premise_tac
     >- (
-      sg ‘usize_to_int i < j’ >- int_tac >>
-      metis_tac [key_MEM_j_lookup_i_is_NONE]) >>
+      sg ‘usize_to_int i < j’ >- int_tac >> fs [] >>
+      (* TODO: we have to rewrite key_MEM_j_lookup_i_is_NONE before applying
+         metis_tac *)
+      assume_tac key_MEM_j_lookup_i_is_NONE >> fs [] >>
+      metis_tac []) >>
     gvs [] >>
     (* Use the fact that as the key is in the slots after i, it can't be in “hm” (yet) *)
     last_x_assum (qspec_assume ‘j’) >> gvs [] >>
@@ -1180,12 +1157,11 @@ Proof
     (* Reasoning about the length *)
     qspecl_assume [‘vec_to_list slots’, ‘usize_to_int i’] len_vec_FLAT_drop_update >>
     gvs [] >>
-    fs [vec_to_list_vec_update] >>
     fs [GSYM integerTheory.INT_ADD_ASSOC, vec_index_def]) >>
   (* Same params *)
   fs [hash_map_same_params_def] >>
   (* Lookup properties *)
-  strip_tac >> fs [hash_mod_key_def, hash_key_fwd_def] >>
+  strip_tac >> fs [] >>
   sg ‘usize_to_int k % len (vec_to_list slots) < len (vec_to_list slots)’
   >- (irule pos_mod_pos_lt >> massage >> fs [] >> int_tac) >> fs [] >>
   Cases_on ‘usize_to_int i = usize_to_int k % len (vec_to_list slots)’ >> fs []
@@ -1194,14 +1170,14 @@ Proof
     sg ‘~ (usize_to_int k % len (vec_to_list slots) + 1 ≤ usize_to_int k % len (vec_to_list slots))’ >- int_tac >> fs [] >>
     (* Is the key is slot i ? *)
     (* TODO: use key_MEM_j_lookup_i_is_NONE? *)
-    Cases_on ‘slot_t_lookup k (vec_index slots i)’ >> gvs [slot_t_lookup_def, vec_index_def] >>
+    Cases_on ‘slot_t_lookup k (vec_index slots i)’ >> gvs [vec_index_def] >>
     (* The key can't be in “hm” *)
     last_x_assum (qspec_assume ‘usize_to_int i’) >>
     pop_assum sg_premise_tac >> fs [] >>
     pop_assum sg_premise_tac >> fs [] >>
     pop_assum (qspecl_assume [‘k’, ‘x’]) >>
     pop_assum sg_premise_tac
-    >-(irule lookup_distinct_keys_MEM >> gvs [slot_t_inv_def, slot_s_inv_def]) >> fs []) >>
+    >-(irule lookup_distinct_keys_MEM >> gvs [slot_t_inv_def]) >> fs []) >>
   (* Here: usize_to_int i ≠ usize_to_int k % len (vec_to_list slots) *)
   Cases_on ‘usize_to_int i ≤ usize_to_int k % len (vec_to_list slots)’ >> fs []
   >- (
@@ -1217,15 +1193,15 @@ Proof
       first_x_assum irule  >>
       last_x_assum (qspec_assume ‘usize_to_int i’) >> gvs [] >>
       (* Prove by contradiction - TODO: turn this into a lemma? *)
-      gvs [slot_t_inv_def, slot_s_inv_def, slot_s_inv_hash_def, hash_mod_key_def, hash_key_fwd_def] >>
+      gvs [slot_t_inv_def] >>
       Cases_on ‘slot_t_lookup k (vec_index slots i)’ >> fs [vec_index_def] >> exfalso >>
-      fs [slot_t_lookup_def] >>
+      fs [] >>
       imp_res_tac lookup_distinct_keys_MEM >>
       sg ‘usize_to_int k % len (vec_to_list slots) = usize_to_int i’ >- metis_tac [] >> fs []
       ) >>
     fs [] >>
     case_tac >>
-    fs [vec_to_list_vec_update] >>
+    fs [] >>
     sg_dep_rewrite_goal_tac index_update_same >> fs []
   ) >>
   (* Here: usize_to_int i > usize_to_int k % ... *)
@@ -1237,10 +1213,10 @@ Proof
     last_x_assum (qspec_assume ‘usize_to_int i’) >>
     pop_assum sg_premise_tac >> fs [] >>
     pop_assum sg_premise_tac >> fs [] >>
-    gvs [slot_t_inv_def, slot_s_inv_def, slot_s_inv_hash_def, hash_mod_key_def, hash_key_fwd_def] >>
+    gvs [slot_t_inv_def] >>
     (* Prove by contradiction *)
     Cases_on ‘slot_t_lookup k (vec_index slots i)’ >> fs [vec_index_def] >> exfalso >>
-    fs [slot_t_lookup_def] >>
+    fs [] >>
     imp_res_tac lookup_distinct_keys_MEM >>
     sg ‘usize_to_int k % len (vec_to_list slots) = usize_to_int i’ >- metis_tac [] >> fs []
   ) >>
@@ -1402,7 +1378,7 @@ Proof
      (* TODO: automate *)
      qspec_assume ‘hm.hash_map_num_entries’ usize_to_int_bounds >> fs [] >>
      int_tac)
-  >-(fs [hash_map_t_base_inv_def, slots_t_inv_def, slots_s_inv_def]) >>
+  >-(fs [hash_map_t_base_inv_def, slots_t_inv_def]) >>
   pure_rewrite_tac [hash_map_t_inv_def] >>
   fs [len_s_def, hash_map_t_base_inv_def, hash_map_t_al_v_def, hash_map_t_v_def, drop_eq] >>
   gvs [] >>
@@ -1431,7 +1407,7 @@ Proof
     int_tac) >>
   rw [] >>
   first_x_assum (qspec_assume ‘k’) >>
-  gvs [hash_mod_key_def, hash_key_fwd_def, slots_t_lookup_def, slot_t_lookup_def, lookup_s_def] >>
+  gvs [slots_t_lookup_def, lookup_s_def] >>
   massage >>
   sg ‘0 ≤ usize_to_int k % len (vec_to_list hm.hash_map_slots)’
   >- (irule pos_mod_pos_is_pos >> fs [] >> int_tac) >> fs [] >>
@@ -1498,359 +1474,479 @@ Proof
 QED
 val _ = save_spec_thm "hash_map_insert_fwd_back_spec"
 
-(*
-Theorem nth_mut_fwd_spec:
-  !(ls : 't list_t) (i : u32).
-    u32_to_int i < len (list_t_v ls) ==>
-    case nth_mut_fwd ls i of
-    | Return x => x = index (u32_to_int i) (list_t_v ls)
-    | Fail _ => F
-    | Diverge => F
+Theorem hash_map_contains_key_in_list_fwd_spec:
+  ∀ key ls.
+  hash_map_contains_key_in_list_fwd key ls = Return (slot_t_lookup key ls ≠ NONE)
 Proof
-  Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’]
-  >-(massage >> int_tac) >>
-  pure_once_rewrite_tac [nth_mut_fwd_def] >> rw [] >>
-  fs [index_eq] >>
-  progress >> progress
+  fs [hash_map_contains_key_in_list_fwd_def] >>
+  Induct_on ‘ls’ >>
+  pure_once_rewrite_tac [hash_map_contains_key_in_list_loop_fwd_def] >>
+  fs [] >>
+  (* There remains only the recursive case *)
+  rw []
 QED
+val _ = save_spec_thm "hash_map_contains_key_in_list_fwd_spec"
 
-val _ = save_spec_thm "nth_mut_fwd_spec"
-
-val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”)
-val insert_def = new_axiom ("insert_def", “
- insert (key : u32) (value : 't) (ls : (u32 # 't) list_t) : (u32 # 't) list_t result =
-  case ls of
-  | ListCons (ckey, cvalue) tl =>
-    if ckey = key
-    then Return (ListCons (ckey, value) tl)
-    else
-      do
-      tl0 <- insert key value tl;
-      Return (ListCons (ckey, cvalue) tl0)
-      od
-  | ListNil => Return (ListCons (key, value) ListNil)
- ”)
-
-(* Property that keys are pairwise distinct *)
-val distinct_keys_def = Define ‘
-  distinct_keys (ls : (u32 # 't) list) =
-    !i j.
-      0 ≤ i ⇒ i < j ⇒ j < len ls ⇒
-      FST (index i ls) ≠ FST (index j ls)
-’
-
-(* Lemma about ‘insert’, without the invariant *)
-Theorem insert_lem_aux:
-  !ls key value.
-    (* The keys are pairwise distinct *)
-    case insert key value ls of
-    | Return ls1 =>
-      (* We updated the binding *)
-      lookup key ls1 = SOME value /\
-      (* The other bindings are left unchanged *)
-      (!k. k <> key ==> lookup k ls = lookup k ls1)
-    | Fail _ => F
-    | Diverge => F
+Theorem hash_map_contains_key_fwd_spec:
+  ∀ hm key.
+  hash_map_t_inv hm ⇒
+  hash_map_contains_key_fwd hm key = Return (lookup_s hm key ≠ NONE)
 Proof
-  Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >>
-  pure_once_rewrite_tac [insert_def] >> rw []
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
-  case_tac >> rw []
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
-  >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
+  fs [hash_map_contains_key_fwd_def] >>
+  fs [hash_key_fwd_def] >>
+  rw [] >>
+  (* TODO: automate *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >> fs [] >>
+  progress >> gvs []
+  >- (
+    fs [hash_map_t_inv_def, hash_map_t_base_inv_def, vec_len_def] >>
+    massage >> int_tac) >>
+  progress >> massage >> gvs [int_rem_def]
+  >- (irule pos_mod_pos_lt >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
   progress >>
-  fs [lookup_def, lookup_raw_def, list_t_v_def]
+  fs [lookup_s_def, vec_index_def, slots_t_lookup_def]
 QED
-
-(*
- * Invariant proof 1
- *)
-
-Theorem distinct_keys_cons:
-  ∀ k v ls.
-  (∀ i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒
-  distinct_keys ls ⇒
-  distinct_keys ((k,v) :: ls)
+val _ = save_spec_thm "hash_map_contains_key_fwd_spec"
+
+Theorem hash_map_get_in_list_fwd_spec:
+  ∀ ls key.
+  case hash_map_get_in_list_fwd key ls of
+  | Diverge => F
+  | Fail _ => slot_t_lookup key ls = NONE
+  | Return x => slot_t_lookup key ls = SOME x
+Proof
+  fs [hash_map_get_in_list_fwd_def] >>
+  Induct_on ‘ls’ >> pure_once_rewrite_tac [hash_map_get_in_list_loop_fwd_def] >>
+  fs [] >>
+  rw []
+QED
+val _ = save_spec_thm "hash_map_get_in_list_fwd_spec"
+
+Theorem hash_map_get_fwd_spec:
+  ∀ hm key.
+  hash_map_t_inv hm ⇒
+  case hash_map_get_fwd hm key of
+  | Diverge => F
+  | Fail _ => lookup_s hm key = NONE
+  | Return x => lookup_s hm key = SOME x
+Proof
+  rw [hash_map_get_fwd_def] >>
+  fs [hash_key_fwd_def] >>
+  (* TODO: automate *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >> fs [] >>
+  progress >> gvs []
+  >- (
+    fs [hash_map_t_inv_def, hash_map_t_base_inv_def, vec_len_def] >>
+    massage >> int_tac) >>
+  progress >> massage >> gvs [int_rem_def]
+  >- (irule pos_mod_pos_lt >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
+  progress >>
+  gvs [lookup_s_def, vec_index_def, slots_t_lookup_def]
+QED
+val _ = save_spec_thm "hash_map_get_fwd_spec"
+
+Theorem hash_map_get_mut_in_list_fwd_spec:
+  ∀ ls key.
+  case hash_map_get_mut_in_list_fwd ls key of
+  | Diverge => F
+  | Fail _ => slot_t_lookup key ls = NONE
+  | Return x => slot_t_lookup key ls = SOME x
+Proof
+  fs [hash_map_get_mut_in_list_fwd_def] >>
+  Induct_on ‘ls’ >> pure_once_rewrite_tac [hash_map_get_mut_in_list_loop_fwd_def] >>
+  fs [] >>
+  rw []
+QED
+val _ = save_spec_thm "hash_map_get_mut_in_list_fwd_spec"
+
+Theorem hash_map_get_mut_fwd_spec:
+  ∀ hm key.
+  hash_map_t_inv hm ⇒
+  case hash_map_get_mut_fwd hm key of
+  | Diverge => F
+  | Fail _ => lookup_s hm key = NONE
+  | Return x => lookup_s hm key = SOME x
 Proof
+  rw [hash_map_get_mut_fwd_def] >>
+  fs [hash_key_fwd_def] >>
+  (* TODO: automate *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >> fs [] >>
+  progress >> gvs []
+  >- (
+    fs [hash_map_t_inv_def, hash_map_t_base_inv_def, vec_len_def] >>
+    massage >> int_tac) >>
+  progress >> massage >> gvs [int_rem_def]
+  >- (irule pos_mod_pos_lt >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
+  progress >>
+  gvs [lookup_s_def, vec_index_def, slots_t_lookup_def]
+QED
+val _ = save_spec_thm "hash_map_get_mut_fwd_spec"
+
+Theorem hash_map_get_mut_in_list_back_spec:
+  ∀ ls key nx.
+  slot_t_lookup key ls ≠ NONE ⇒
+  ∃ nls. hash_map_get_mut_in_list_back ls key nx = Return nls ∧
+  slot_t_lookup key nls = SOME nx ∧
+  (∀ k. k ≠ key ⇒ slot_t_lookup k nls = slot_t_lookup k ls)
+Proof
+  fs [hash_map_get_mut_in_list_back_def] >>
+  Induct_on ‘ls’ >> pure_once_rewrite_tac [hash_map_get_mut_in_list_loop_back_def] >>
+  fs [] >>
   rw [] >>
-  rw [distinct_keys_def] >>
-  Cases_on ‘i = 0’ >> fs []
+  fs [] >>
+  progress >>
+  fs []  
+QED
+val _ = save_spec_thm "hash_map_get_mut_in_list_back_spec"
+
+Theorem hash_map_get_mut_back_spec:
+  ∀ hm key nx.
+  lookup_s hm key ≠ NONE ⇒
+  hash_map_t_inv hm ⇒
+  ∃ hm1. hash_map_get_mut_back hm key nx = Return hm1 ∧
+  lookup_s hm1 key = SOME nx ∧
+  (∀ k. k ≠ key ⇒ lookup_s hm1 k = lookup_s hm k)
+Proof
+  rw [hash_map_get_mut_back_def] >>
+  fs [hash_key_fwd_def] >>
+  (* TODO: automate *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >> fs [] >>
+  progress >> gvs []
+  >- (
+    fs [hash_map_t_inv_def, hash_map_t_base_inv_def, vec_len_def] >>
+    massage >> int_tac) >>
+  progress >> massage >> gvs [int_rem_def]
+  (* TODO: we did this proof many times *)
+  >- (irule pos_mod_pos_lt >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
+  progress >>
+  gvs [lookup_s_def, vec_index_def, slots_t_lookup_def] >>
+  progress
+  (* TODO: again the same proof *)
+  >- (massage >> irule pos_mod_pos_lt >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
+  gvs [] >>
+  conj_tac
   >-(
-    (* Use the first hypothesis *)
-    fs [index_eq] >>
-    last_x_assum (qspecl_assume [‘j - 1’]) >>
-    sg ‘0 ≤ j - 1’ >- int_tac >>
-    fs [len_def] >>
-    sg ‘j - 1 < len ls’ >- int_tac >>
+    sg_dep_rewrite_goal_tac index_update_diff
+    >- (fs [] >> irule pos_mod_pos_lt >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
     fs []
   ) >>
-  (* Use the second hypothesis *)
-  sg ‘0 < i’ >- int_tac >>
-  sg ‘0 < j’ >- int_tac >>
-  fs [distinct_keys_def, index_eq, len_def] >>
-  first_x_assum (qspecl_assume [‘i - 1’, ‘j - 1’]) >>
-  sg ‘0 ≤ i - 1 ∧ i - 1 < j - 1 ∧ j - 1 < len ls’ >- int_tac >>
+  rw [] >>
+  Cases_on ‘usize_to_int k % len (vec_to_list hm.hash_map_slots) = usize_to_int key % len (vec_to_list hm.hash_map_slots)’ >>
+  fs []
+  >- (
+    sg_dep_rewrite_goal_tac index_update_diff
+    >- (fs [] >> irule pos_mod_pos_lt >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
+    fs []
+  ) >>
+  sg_dep_rewrite_goal_tac index_update_same
+  >- (
+    rw []
+    >- (irule pos_mod_pos_lt >> massage >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac)
+    >- (irule pos_mod_pos_lt >> massage >> fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac)
+  ) >>
   fs []
 QED
+val _ = save_spec_thm "hash_map_get_mut_back_spec"
 
-Theorem distinct_keys_tail:
-  ∀ k v ls.
-  distinct_keys ((k,v) :: ls) ⇒
-  distinct_keys ls
+Theorem hash_map_remove_from_list_fwd_spec:
+  ∀ key l i ls.
+  hash_map_remove_from_list_fwd key ls = Return (slot_t_lookup key ls)
 Proof
-  rw [distinct_keys_def] >>
-  last_x_assum (qspecl_assume [‘i + 1’, ‘j + 1’]) >>
-  fs [len_def] >>
-  sg ‘0 ≤ i + 1 ∧ i + 1 < j + 1 ∧ j + 1 < 1 + len ls’ >- int_tac >> fs [] >>
-  sg ‘0 < i + 1 ∧ 0 < j + 1’ >- int_tac >> fs [index_eq] >>
-  sg ‘i + 1 - 1 = i ∧ j + 1 - 1 = j’ >- int_tac >> fs []
+  fs [hash_map_remove_from_list_fwd_def] >>
+  Induct_on ‘ls’ >> pure_once_rewrite_tac [hash_map_remove_from_list_loop_fwd_def] >>
+  rw [] >>
+  metis_tac []
 QED
+val _ = save_spec_thm "hash_map_remove_from_list_fwd_spec"
 
-Theorem insert_index_neq:
-  ∀ q k v ls0 ls1 i.
-  (∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))) ⇒
-  q ≠ k ⇒
-  insert k v ls0 = Return ls1 ⇒
-  0 ≤ i ⇒
-  i < len (list_t_v ls1) ⇒
-  FST (index i (list_t_v ls1)) ≠ q
+Theorem lookup_SOME_not_empty:
+  ∀ ls k. lookup k ls ≠ NONE ⇒ 0 < len ls
 Proof
-  ntac 3 strip_tac >>
-  Induct_on ‘ls0’ >> rw [] >~ [‘ListNil’]
-  >-(
-    fs [insert_def] >>
-    sg ‘ls1 = ListCons (k,v) ListNil’ >- fs [] >> fs [list_t_v_def, len_def] >>
-    sg ‘i = 0’ >- int_tac >> fs [index_eq]) >>
-  Cases_on ‘t’ >>
-  Cases_on ‘i = 0’ >> fs []
-  >-(
-    qpat_x_assum ‘insert _ _ _ = _’ mp_tac >>
-    simp [MK_BOUNDED insert_def 1, bind_def] >>
-    Cases_on ‘q' = k’ >> rw []
-    >- (fs [list_t_v_def, index_eq]) >>
-    Cases_on ‘insert k v ls0’ >> fs [] >>
-    gvs [list_t_v_def, index_eq] >>
-    first_x_assum (qspec_assume ‘0’) >>
-    fs [len_def] >>
-    strip_tac >>
-    qspec_assume ‘list_t_v ls0’ len_pos >>
-    sg ‘0 < 1 + len (list_t_v ls0)’ >- int_tac >>
-    fs []) >>
-  qpat_x_assum ‘insert _ _ _ = _’ mp_tac >>
-  simp [MK_BOUNDED insert_def 1, bind_def] >>
-  Cases_on ‘q' = k’ >> rw []
-  >-(
-    fs [list_t_v_def, index_eq, len_def] >>
-    first_x_assum (qspec_assume ‘i’) >> rfs []) >>
-  Cases_on ‘insert k v ls0’ >> fs [] >>
-  gvs [list_t_v_def, index_eq] >>
-  last_x_assum (qspec_assume ‘i - 1’) >>
-  fs [len_def] >>
-  sg ‘0 ≤ i - 1 ∧ i - 1 < len (list_t_v a)’ >- int_tac >> fs [] >>
-  first_x_assum irule >>
-  rw [] >>
-  last_x_assum (qspec_assume ‘j + 1’) >>
-  rfs [] >>
-  sg ‘j + 1 < 1 + len (list_t_v ls0) ∧ j + 1 − 1 = j ∧ j + 1 ≠ 0’ >- int_tac >> fs []
+  Induct_on ‘ls’ >> fs [] >> rw [] >>
+  qspec_assume ‘ls’ len_pos >>
+  int_tac
 QED
 
-Theorem distinct_keys_insert_index_neq:
-  ∀ k v q r ls0 ls1 i.
-  distinct_keys ((q,r)::list_t_v ls0) ⇒
-  q ≠ k ⇒
-  insert k v ls0 = Return ls1 ⇒
+Theorem slot_t_lookup_SOME_not_empty:
+  ∀ ls i k.
   0 ≤ i ⇒
-  i < len (list_t_v ls1) ⇒
-  FST (index i (list_t_v ls1)) ≠ q
+  i < len ls ⇒
+  slot_t_lookup k (index i ls) ≠ NONE ⇒
+  0 < len (FLAT (MAP list_t_v ls))
 Proof
-  rw [] >>
-  (* Use the first assumption to prove the following assertion *)
-  sg ‘∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))’
+  Induct_on ‘ls’ >> rw [] >> try_tac int_tac >>
+  gvs [index_eq] >>
+  Cases_on ‘i = 0’ >> fs []
   >-(
-    strip_tac >>
-    fs [distinct_keys_def] >>
-    last_x_assum (qspecl_assume [‘0’, ‘j + 1’]) >>
-    fs [index_eq] >>
-    sg ‘j + 1 - 1 = j’ >- int_tac >> fs [len_def] >>
-    rw []>>
-    first_x_assum irule >> int_tac) >>
-  qspecl_assume [‘q’, ‘k’, ‘v’, ‘ls0’, ‘ls1’, ‘i’] insert_index_neq >>
-  fs []
+    qspec_assume ‘FLAT (MAP list_t_v ls)’ len_pos >>
+    imp_res_tac lookup_SOME_not_empty >> int_tac
+  ) >>
+  qspec_assume ‘list_t_v h’ len_pos >>
+  last_x_assum (qspecl_assume [‘i - 1’, ‘k’]) >>
+  sg ‘0 ≤ i - 1 ∧ i - 1 < len ls ∧ i ≠ 0’ >- int_tac >>
+  gvs [] >>
+  int_tac
 QED
 
-Theorem distinct_keys_insert:
-  ∀ k v ls0 ls1.
-  distinct_keys (list_t_v ls0) ⇒
-  insert k v ls0 = Return ls1 ⇒
-  distinct_keys (list_t_v ls1)
+Theorem lookup_s_SOME_not_empty:
+  ∀ hm key.
+    hash_map_t_inv hm ⇒
+    lookup_s hm key ≠ NONE ⇒ 0 < len_s hm
 Proof
-  Induct_on ‘ls0’ >~ [‘ListNil’]
-  >-(
-    rw [distinct_keys_def, list_t_v_def, insert_def] >>
-    fs [list_t_v_def, len_def] >>
-    int_tac) >>  
-  Cases >>
-  pure_once_rewrite_tac [insert_def] >> fs[] >>
-  rw [] >> fs []
-  >-(
-    (* k = q *)
-    last_x_assum ignore_tac >>
-    fs [distinct_keys_def] >>
-    rw [] >>
-    last_x_assum (qspecl_assume [‘i’, ‘j’]) >>
-    rfs [list_t_v_def, len_def] >>
-    sg ‘0 < j’ >- int_tac >>
-    Cases_on ‘i = 0’ >> gvs [index_eq]) >>
-  (* k ≠ q: recursion *)
-  Cases_on ‘insert k v ls0’ >> fs [bind_def] >>
-  last_x_assum (qspecl_assume [‘k’, ‘v’, ‘a’]) >>
-  gvs [list_t_v_def] >>
-  imp_res_tac distinct_keys_tail >> fs [] >>
-  irule distinct_keys_cons >> rw [] >>
-  metis_tac [distinct_keys_insert_index_neq]
-QED  
+  rw [lookup_s_def, slots_t_lookup_def, len_s_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
+  sg ‘0 < len (vec_to_list hm.hash_map_slots)’
+  >- (fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
+  irule slot_t_lookup_SOME_not_empty >>
+  qexists ‘usize_to_int key % len (vec_to_list hm.hash_map_slots)’ >>
+  qexists ‘key’ >>
+  rw []
+  >-(irule pos_mod_pos_is_pos >> massage >> int_tac) >>
+  irule pos_mod_pos_lt >> massage >> int_tac
+QED
 
-Theorem insert_lem:
-  !ls key value.
-    (* The keys are pairwise distinct *)
-    distinct_keys (list_t_v ls) ==>
-    case insert key value ls of
-    | Return ls1 =>
-      (* We updated the binding *)
-      lookup key ls1 = SOME value /\
-      (* The other bindings are left unchanged *)
-      (!k. k <> key ==> lookup k ls = lookup k ls1) ∧
-      (* The keys are still pairwise disjoint *)
-      distinct_keys (list_t_v ls1)
-    | Fail _ => F
-    | Diverge => F
+Theorem hash_map_remove_fwd_spec:
+  ∀ hm key.
+  hash_map_t_inv hm ⇒
+  hash_map_remove_fwd hm key = Return (lookup_s hm key)
 Proof
-  rw [] >>
-  qspecl_assume [‘ls’, ‘key’, ‘value’] insert_lem_aux >>
+  rw [hash_map_remove_fwd_def] >>
+  (* TODO: automate *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >> fs [] >>
+  sg ‘0 < usize_to_int (vec_len hm.hash_map_slots)’
+  >- (fs [hash_map_t_inv_def, hash_map_t_base_inv_def, vec_len_def] >> massage >> int_tac) >>
+  fs [vec_len_def] >> massage >>
+  (* TODO: rewriting for: usize_to_int (int_to_usize (len (vec_to_list v))) = len (vec_to_list v) *)
+  progress >>
+  progress >> fs [int_rem_def, vec_len_def] >> massage
+  >- (irule pos_mod_pos_lt >> fs []) >>
+  progress >>
+  gvs [lookup_s_def, slots_t_lookup_def, vec_index_def] >>
   case_tac >> fs [] >>
-  metis_tac [distinct_keys_insert]
+  progress >>
+  (* Prove that we can decrement the number of entries *)
+  qspecl_assume [‘hm’, ‘key’] lookup_s_SOME_not_empty >>
+  gvs [lookup_s_def, slots_t_lookup_def, len_s_def, hash_map_t_inv_def, hash_map_t_base_inv_def] >>
+  int_tac
 QED
+val _ = save_spec_thm "hash_map_remove_fwd_spec"
 
-(*
- * Invariant proof 2: functional version of the invariant
- *)
-
-Theorem distinct_keys_f_insert_for_all:
-  ∀k v k1 ls0 ls1.
-  k1 ≠ k ⇒
-  for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
-  pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
-  insert k v ls0 = Return ls1 ⇒
-  for_all (λy. k1 ≠ FST y) (list_t_v ls1)
+Theorem every_distinct_remove_every_distinct:
+  ∀ k0 k1 ls0.
+  EVERY (λy. k1 ≠ FST y) ls0 ⇒
+  EVERY (λy. k1 ≠ FST y) (remove k0 ls0)
 Proof
-  Induct_on ‘ls0’ >> rw [pairwise_rel_def] >~ [‘ListNil’] >>
-  gvs [list_t_v_def, pairwise_rel_def, for_all_def]
-  >-(gvs [MK_BOUNDED insert_def 1, bind_def, list_t_v_def, for_all_def]) >>
-  pat_undisch_tac ‘insert _ _ _ = _’ >>
-  simp [MK_BOUNDED insert_def 1, bind_def] >>
-  Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >>
-  Cases_on ‘insert k v ls0’ >>
-  gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >>
-  metis_tac []
+  Induct_on ‘ls0’ >> fs [] >> rw [] >>
+  Cases_on ‘h’ >> fs [] >>
+  case_tac >> fs []
 QED
 
-Theorem distinct_keys_f_insert:
-  ∀ k v ls0 ls1.
-  distinct_keys_f (list_t_v ls0) ⇒
-  insert k v ls0 = Return ls1 ⇒
-  distinct_keys_f (list_t_v ls1)
+Theorem hash_map_remove_from_list_back_spec:
+  ∀ key ls.
+  ∃ ls1. hash_map_remove_from_list_back key ls = Return ls1 ∧
+  (∀ l i. slot_t_inv l i ls ⇒
+    slot_t_inv l i ls1 ∧
+    list_t_v ls1 = remove key (list_t_v ls) ∧
+    slot_t_lookup key ls1 = NONE ∧
+    (∀ k. k ≠ key ⇒ slot_t_lookup k ls1 = slot_t_lookup k ls) ∧
+    (case slot_t_lookup key ls of
+     | NONE => len (list_t_v ls1) = len (list_t_v ls)
+     | SOME _ => len (list_t_v ls1) = len (list_t_v ls) - 1))
 Proof
-  Induct_on ‘ls0’ >> rw [distinct_keys_f_def] >~ [‘ListNil’]
-  >-(
-    fs [list_t_v_def, insert_def] >>
-    gvs [list_t_v_def, pairwise_rel_def, for_all_def]) >>
-  last_x_assum (qspecl_assume [‘k’, ‘v’]) >>
-  pat_undisch_tac ‘insert _ _ _ = _’ >>
-  simp [MK_BOUNDED insert_def 1, bind_def] >>
-  (* TODO: improve case_tac *)
-  Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >>
-  Cases_on ‘insert k v ls0’ >>
-  gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >>
-  metis_tac [distinct_keys_f_insert_for_all]
+  fs [hash_map_remove_from_list_back_def] >>
+  Induct_on ‘ls’ >> pure_once_rewrite_tac [hash_map_remove_from_list_loop_back_def] >>
+  fs [slot_t_inv_def] >>
+  fs [distinct_keys_def, pairwise_rel_def] >>
+  rw []
+  >- (metis_tac [])
+  >- (
+    last_x_assum ignore_tac >>
+    pop_assum ignore_tac >>
+    pop_assum ignore_tac >>
+    Induct_on ‘ls’ >> fs []
+  ) >>
+  progress >>
+  rw [] >> gvs [pairwise_rel_def]
+  >- metis_tac [every_distinct_remove_every_distinct]
+  >- metis_tac []
+  >- metis_tac []
+  >- metis_tac []
+  >- metis_tac [] >>
+  case_tac >> fs [] >- metis_tac [] >>
+  first_x_assum (qspecl_assume [‘l’, ‘i’]) >> gvs [] >>
+  pop_assum sg_premise_tac >- metis_tac [] >> fs []
 QED
+val _ = save_spec_thm "hash_map_remove_from_list_back_spec"
 
-(*
- * Proving equivalence between the two version - exercise.
- *)
-Theorem for_all_quant:
-  ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
+(* TODO: automate this *)
+Theorem hash_map_remove_back_branch_eq:
+  ∀ key hm a.
+  (case lookup key (list_t_v (vec_index hm.hash_map_slots a)) of
+    NONE =>
+      do
+        l0 <-
+          hash_map_remove_from_list_back key
+            (vec_index hm.hash_map_slots a);
+        v <- vec_index_mut_back hm.hash_map_slots a l0;
+        Return (hm with hash_map_slots := v)
+      od
+  | SOME x0 =>
+    do
+      i0 <- usize_sub hm.hash_map_num_entries (int_to_usize 1);
+      l0 <-
+        hash_map_remove_from_list_back key
+          (vec_index hm.hash_map_slots a);
+      v <- vec_index_mut_back hm.hash_map_slots a l0;
+      Return
+        (hm with <|hash_map_num_entries := i0; hash_map_slots := v|>)
+    od) =
+  (do
+   i0 <- (case lookup key (list_t_v (vec_index hm.hash_map_slots a)) of
+         | NONE => Return hm.hash_map_num_entries
+         | SOME _ => usize_sub hm.hash_map_num_entries (int_to_usize 1));
+   l0 <-
+     hash_map_remove_from_list_back key
+       (vec_index hm.hash_map_slots a);
+   v <- vec_index_mut_back hm.hash_map_slots a l0;
+   Return
+     (hm with <|hash_map_num_entries := i0; hash_map_slots := v|>)
+   od)
 Proof
-  strip_tac >> Induct_on ‘ls’
-  >-(rw [for_all_def, len_def] >> int_tac) >>
-  rw [for_all_def, len_def, index_eq] >>
-  equiv_tac
-  >-(
-    rw [] >>
-    Cases_on ‘i = 0’ >> fs [] >>
-    first_x_assum irule >>
-    int_tac) >>
-  rw []
-  >-(
-    first_x_assum (qspec_assume ‘0’) >> fs [] >>
-    first_x_assum irule >>
-    qspec_assume ‘ls’ len_pos >>
-    int_tac) >>
-  first_x_assum (qspec_assume ‘i + 1’) >>
-  fs [] >>
-  sg ‘i + 1 ≠ 0 ∧ i + 1 - 1 = i’ >- int_tac >> fs [] >>
-  first_x_assum irule >> int_tac
+  rw [bind_def] >>
+  rpt (case_tac >> fs []) >>
+  Cases_on ‘hm’ >> fs [] >>
+  fs [hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_slots_fupd_def,
+      hashmap_TypesTheory.recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def]
 QED
 
-Theorem pairwise_rel_quant:
-  ∀p ls. pairwise_rel p ls ⇔
-    (∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls))
+(* TODO: this doesn't work very well *)
+Theorem lookup_cond_decr_entries_eq:
+  ∀ hm key i.
+  hash_map_t_inv hm ⇒
+  usize_to_int i < len (vec_to_list hm.hash_map_slots) ⇒
+  ∃ j.
+  (case lookup key (list_t_v (vec_index hm.hash_map_slots i)) of
+    NONE => Return hm.hash_map_num_entries
+  | SOME v => usize_sub hm.hash_map_num_entries (int_to_usize 1)) = Return j ∧
+  (lookup key (list_t_v (vec_index hm.hash_map_slots i)) = NONE ⇒ j = hm.hash_map_num_entries) ∧
+  (lookup key (list_t_v (vec_index hm.hash_map_slots i)) ≠ NONE ⇒
+   usize_to_int j + 1 = usize_to_int hm.hash_map_num_entries)
 Proof
-  strip_tac >> Induct_on ‘ls’
-  >-(rw [pairwise_rel_def, len_def] >> int_tac) >>
-  rw [pairwise_rel_def, len_def] >>
-  equiv_tac
-  >-(
-    (* ==> *)
-    rw [] >>
-    sg ‘0 < j’ >- int_tac >>
-    Cases_on ‘i = 0’
-    >-(
-      simp [index_eq] >>
-      qspecl_assume [‘p h’, ‘ls’] (iffLR for_all_quant) >>
-      first_x_assum irule >> fs [] >> int_tac
-    ) >>
-    rw [index_eq] >>
-    first_x_assum irule >> int_tac
-  ) >>
-  (* <== *)
-  rw []
-  >-(
-    rw [for_all_quant] >>
-    first_x_assum (qspecl_assume [‘0’, ‘i + 1’]) >>
-    sg ‘0 < i + 1 ∧ i + 1 - 1 = i’ >- int_tac >>
-    fs [index_eq] >>
-    first_x_assum irule >> int_tac
-  ) >>
-  sg ‘pairwise_rel p ls’
-  >-(
-    rw [pairwise_rel_def] >>
-    first_x_assum (qspecl_assume [‘i' + 1’, ‘j' + 1’]) >>
-    sg ‘0 < i' + 1 ∧ 0 < j' + 1’ >- int_tac >>
-    fs [index_eq, int_add_minus_same_eq] >>
-    first_x_assum irule >> int_tac
-  ) >>
-  fs []
+  rw [] >>
+  case_tac >>
+  progress >>
+  qspecl_assume [‘vec_to_list hm.hash_map_slots’, ‘usize_to_int i’, ‘key’] slot_t_lookup_SOME_not_empty >>
+  gvs [vec_index_def] >>
+  fs [hash_map_t_inv_def, hash_map_t_base_inv_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
+  int_tac
 QED
 
-Theorem distinct_keys_f_eq_distinct_keys:
-  ∀ ls.
-  distinct_keys_f ls ⇔ distinct_keys ls
+(* TODO: when saving a spec theorem, check that all the variables which appear
+   in the pre/postconditions also appear in the application *)
+Theorem hash_map_remove_back_spec:
+  ∀ hm key.
+  hash_map_t_inv hm ⇒
+  ∃ hm1. hash_map_remove_back hm key = Return hm1 ∧
+  hash_map_t_inv hm1 ∧
+  lookup_s hm1 key = NONE ∧
+  (∀ k. k ≠ key ⇒ lookup_s hm1 k = lookup_s hm k) ∧
+  (case lookup_s hm key of
+   | NONE => len_s hm1 = len_s hm
+   | SOME _ => len_s hm1 = len_s hm - 1)
 Proof
-  rw [distinct_keys_def, distinct_keys_f_def] >>
-  qspecl_assume [‘(λx y. FST x ≠ FST y)’, ‘ls’] pairwise_rel_quant >>
-  fs []
+  rw [hash_map_remove_back_def] >>
+  (* TODO: automate *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >>
+  fs [vec_len_def] >>
+  sg ‘0 < usize_to_int (vec_len hm.hash_map_slots)’
+  >-(fs [hash_map_t_inv_def, hash_map_t_base_inv_def, gt_eq_lt, vec_len_def] >> massage >> fs []) >>
+  (* TODO: we have to prove this several times - it would be good to remember the preconditions
+     we proved, sometimes *)
+  sg ‘usize_to_int key % len (vec_to_list hm.hash_map_slots) < usize_to_int (vec_len hm.hash_map_slots)’
+  >- (fs [vec_len_def] >> massage >> irule pos_mod_pos_lt >> int_tac) >>
+  (* TODO: add a rewriting rule *)
+  sg ‘usize_to_int (vec_len hm.hash_map_slots) = len (vec_to_list hm.hash_map_slots)’
+  >- (fs [vec_len_def] >> massage >> fs []) >>
+  fs [vec_len_def] >>
+  massage >>
+  progress >>
+  progress >> fs [int_rem_def, vec_len_def] >>
+  progress >>
+  gvs [] >>
+  fs [hash_map_remove_back_branch_eq] >>
+  qspecl_assume [‘hm’, ‘key’, ‘a’] lookup_cond_decr_entries_eq >>
+  gvs [] >>
+  progress >>
+  progress >> fs [vec_len_def] >>
+  (* Prove the post-condition *)
+  sg ‘let i = usize_to_int key % len (vec_to_list hm.hash_map_slots) in
+      slot_t_inv (len (vec_to_list hm.hash_map_slots)) i (index i (vec_to_list hm.hash_map_slots))’
+  >- (fs [hash_map_t_inv_def, hash_map_t_base_inv_def, slots_t_inv_def]) >> fs [] >>
+  gvs [vec_index_def] >>
+  qpat_assum ‘∀l. _’ imp_res_tac >>
+  rw []
+  >- (
+    fs [hash_map_t_inv_def, hash_map_t_base_inv_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
+    rw []
+    >- (
+      (* The num_entries has been correctly updated *)
+      sg_dep_rewrite_goal_tac len_FLAT_MAP_update >- int_tac >> fs [] >> pop_assum ignore_tac >> gvs [] >>
+      (* Case analysis on: ‘lookup key (index (key % len slots) slots)’ *)
+      pop_assum mp_tac >> case_tac >> fs [] >>
+      int_tac
+    )
+    >- (
+      fs [slots_t_inv_def] >> rw [] >>
+      (* TODO: this is annoying: we proved this many times *)
+      last_x_assum (qspec_assume ‘i’) >>
+      gvs [vec_index_def] >>
+      qpat_x_assum ‘∀l. _’ imp_res_tac >>
+      Cases_on ‘i = usize_to_int key % len (vec_to_list hm.hash_map_slots)’ >> fs []
+      >- (
+        sg_dep_rewrite_goal_tac index_update_diff
+        >- (fs [] >> int_tac) >> fs []
+      ) >>
+      sg_dep_rewrite_goal_tac index_update_same
+      >- (fs [] >> int_tac) >> fs []
+    ) >>
+    (* num_entries ≤ max_load *)
+    Cases_on ‘lookup key (list_t_v (index
+                (usize_to_int key % len (vec_to_list hm.hash_map_slots))
+                (vec_to_list hm.hash_map_slots)))’ >> gvs [] >>
+    (* Remains the case where we decrment num_entries - TODO: this is too much work, should be easier *)
+    gvs [usize_sub_def, mk_usize_def] >>
+    massage >>
+    sg ‘0 ≤ len_s hm - 1 ∧ len_s hm - 1 ≤ usize_max’
+    >- (fs [len_s_def, hash_map_t_al_v_def, hash_map_t_v_def] >> int_tac) >>
+    fs [len_s_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
+    gvs [] >>
+    massage >>
+    Cases_on ‘hm.hash_map_max_load_factor’ >> gvs [] >>
+    disj1_tac >> int_tac)
+  >- (
+    fs [lookup_s_def, slots_t_lookup_def] >>
+    (* TODO: we did this too many times *)
+    sg_dep_rewrite_goal_tac index_update_diff
+    >- (fs [] >> int_tac) >> fs [] >>
+    metis_tac []
+  )
+  >- (
+    (* Lookup of k ≠ key *)
+    fs [lookup_s_def, slots_t_lookup_def] >>
+    Cases_on ‘usize_to_int k % len (vec_to_list hm.hash_map_slots) = usize_to_int key % len (vec_to_list hm.hash_map_slots)’ >> fs []
+    >- (
+      sg_dep_rewrite_goal_tac index_update_diff
+      >- (fs [] >> int_tac) >> fs [] >>
+      metis_tac []) >>
+    sg_dep_rewrite_goal_tac index_update_same
+    >- (rw [] >> try_tac int_tac >> irule pos_mod_pos_lt >> fs [] >> massage >> fs []) >> fs [] >>
+    case_tac >> fs [] >>
+    metis_tac []
+  ) >>
+  (* The length is correctly updated *)
+  fs [lookup_s_def, len_s_def, slots_t_lookup_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
+  case_tac >> gvs [] >>  
+  sg_dep_rewrite_goal_tac len_FLAT_MAP_update >> fs [] >> int_tac
 QED
+val _ = save_spec_thm "hash_map_remove_back_spec"
 
 val _ = export_theory ()
-*)
diff --git a/tests/hol4/hashmap/hashmap_PropertiesTheory.sig b/tests/hol4/hashmap/hashmap_PropertiesTheory.sig
new file mode 100644
index 00000000..39b6f048
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_PropertiesTheory.sig
@@ -0,0 +1,902 @@
+signature hashmap_PropertiesTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Axioms  *)
+    val usize_u32_bounds : thm
+  
+  (*  Definitions  *)
+    val distinct_keys_def : thm
+    val hash_map_just_before_resize_pred_def : thm
+    val hash_map_same_params_def : thm
+    val hash_map_t_al_v_def : thm
+    val hash_map_t_base_inv_def : thm
+    val hash_map_t_inv_def : thm
+    val hash_map_t_v_def : thm
+    val hash_mod_key_def : thm
+    val insert_in_slot_t_rel_def : thm
+    val len_s_def : thm
+    val list_t_v_def : thm
+    val lookup_s_def : thm
+    val pairwise_rel_def : thm
+    val slot_s_inv_def : thm
+    val slot_s_inv_hash_def : thm
+    val slot_t_inv_def : thm
+    val slot_t_lookup_def : thm
+    val slot_t_remove_def : thm
+    val slots_s_inv_def : thm
+    val slots_t_inv_def : thm
+    val slots_t_lookup_def : thm
+  
+  (*  Theorems  *)
+    val EVERY_quant_equiv : thm
+    val FLAT_ListNil_is_nil : thm
+    val MEM_EVERY_not : thm
+    val MEM_distinct_keys_lookup : thm
+    val distinct_keys_MEM_not_eq : thm
+    val distinct_keys_lookup_NONE : thm
+    val every_distinct_remove_every_distinct : thm
+    val hash_map_allocate_slots_fwd_spec : thm
+    val hash_map_allocate_slots_loop_fwd_spec : thm
+    val hash_map_clear_fwd_back_spec : thm
+    val hash_map_clear_loop_fwd_back_spec : thm
+    val hash_map_clear_loop_fwd_back_spec_aux : thm
+    val hash_map_cond_incr_thm : thm
+    val hash_map_contains_key_fwd_spec : thm
+    val hash_map_contains_key_in_list_fwd_spec : thm
+    val hash_map_get_fwd_spec : thm
+    val hash_map_get_in_list_fwd_spec : thm
+    val hash_map_get_mut_back_spec : thm
+    val hash_map_get_mut_fwd_spec : thm
+    val hash_map_get_mut_in_list_back_spec : thm
+    val hash_map_get_mut_in_list_fwd_spec : thm
+    val hash_map_insert_fwd_back_spec : thm
+    val hash_map_insert_in_list_fwd_spec : thm
+    val hash_map_insert_in_list_loop_back_EVERY_distinct_keys : thm
+    val hash_map_insert_in_list_loop_back_distinct_keys : thm
+    val hash_map_insert_in_list_loop_back_spec : thm
+    val hash_map_insert_in_list_loop_back_spec_aux : thm
+    val hash_map_insert_in_list_loop_fwd_spec : thm
+    val hash_map_insert_no_resize_fwd_back_branches_eq : thm
+    val hash_map_insert_no_resize_fwd_back_spec : thm
+    val hash_map_insert_no_resize_fwd_back_spec_aux : thm
+    val hash_map_len_spec : thm
+    val hash_map_move_elements_from_list_fwd_back_spec : thm
+    val hash_map_move_elements_fwd_back_spec : thm
+    val hash_map_move_elements_loop_fwd_back_spec_aux : thm
+    val hash_map_new_fwd_spec : thm
+    val hash_map_new_with_capacity_fwd_spec : thm
+    val hash_map_remove_back_branch_eq : thm
+    val hash_map_remove_back_spec : thm
+    val hash_map_remove_from_list_back_spec : thm
+    val hash_map_remove_from_list_fwd_spec : thm
+    val hash_map_remove_fwd_spec : thm
+    val hash_map_same_params_refl : thm
+    val hash_map_t_base_inv_len_slots : thm
+    val hash_map_try_resize_fwd_back_spec : thm
+    val key_MEM_j_lookup_i_is_NONE : thm
+    val len_FLAT_MAP_update : thm
+    val len_index_FLAT_MAP_list_t_v : thm
+    val len_vec_FLAT_drop_update : thm
+    val lookup_SOME_not_empty : thm
+    val lookup_cond_decr_entries_eq : thm
+    val lookup_def : thm
+    val lookup_distinct_keys_MEM : thm
+    val lookup_ind : thm
+    val lookup_s_SOME_not_empty : thm
+    val pairwise_rel_quant_equiv : thm
+    val remove_def : thm
+    val remove_ind : thm
+    val slot_t_lookup_SOME_not_empty : thm
+  
+  val hashmap_Properties_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [hashmap_Funs] Parent theory of "hashmap_Properties"
+   
+   [usize_u32_bounds]  Axiom
+      
+      [oracles: ] [axioms: usize_u32_bounds] [] ⊢ usize_max = u32_max
+   
+   [distinct_keys_def]  Definition
+      
+      ⊢ ∀ls. distinct_keys ls ⇔ pairwise_rel (λx y. FST x ≠ FST y) ls
+   
+   [hash_map_just_before_resize_pred_def]  Definition
+      
+      ⊢ ∀hm.
+          hash_map_just_before_resize_pred hm ⇔
+          (let
+             (dividend,divisor) = hm.hash_map_max_load_factor
+           in
+             usize_to_int hm.hash_map_num_entries =
+             usize_to_int hm.hash_map_max_load + 1 ∧
+             len (vec_to_list hm.hash_map_slots) * 2 *
+             usize_to_int dividend ≤ usize_max ∨
+             len (vec_to_list hm.hash_map_slots) * 2 *
+             usize_to_int dividend > usize_max)
+   
+   [hash_map_same_params_def]  Definition
+      
+      ⊢ ∀hm hm1.
+          hash_map_same_params hm hm1 ⇔
+          hm1.hash_map_max_load_factor = hm.hash_map_max_load_factor ∧
+          hm1.hash_map_max_load = hm.hash_map_max_load ∧
+          len (vec_to_list hm1.hash_map_slots) =
+          len (vec_to_list hm.hash_map_slots)
+   
+   [hash_map_t_al_v_def]  Definition
+      
+      ⊢ ∀hm. hash_map_t_al_v hm = FLAT (hash_map_t_v hm)
+   
+   [hash_map_t_base_inv_def]  Definition
+      
+      ⊢ ∀hm.
+          hash_map_t_base_inv hm ⇔
+          (let
+             al = hash_map_t_al_v hm
+           in
+             usize_to_int hm.hash_map_num_entries = len al ∧
+             slots_t_inv hm.hash_map_slots ∧
+             len (vec_to_list hm.hash_map_slots) > 0 ∧
+             (let
+                capacity = len (vec_to_list hm.hash_map_slots);
+                (dividend,divisor) = hm.hash_map_max_load_factor;
+                dividend = usize_to_int dividend;
+                divisor = usize_to_int divisor
+              in
+                0 < dividend ∧ dividend < divisor ∧
+                capacity * dividend ≥ divisor ∧
+                usize_to_int hm.hash_map_max_load =
+                capacity * dividend / divisor))
+   
+   [hash_map_t_inv_def]  Definition
+      
+      ⊢ ∀hm.
+          hash_map_t_inv hm ⇔
+          hash_map_t_base_inv hm ∧
+          (let
+             (dividend,divisor) = hm.hash_map_max_load_factor
+           in
+             usize_to_int hm.hash_map_num_entries ≤
+             usize_to_int hm.hash_map_max_load ∨
+             len (vec_to_list hm.hash_map_slots) * 2 *
+             usize_to_int dividend > usize_max)
+   
+   [hash_map_t_v_def]  Definition
+      
+      ⊢ ∀hm. hash_map_t_v hm = MAP list_t_v (vec_to_list hm.hash_map_slots)
+   
+   [hash_mod_key_def]  Definition
+      
+      ⊢ ∀k l.
+          hash_mod_key k l =
+          case hash_key_fwd k of
+            Return k => usize_to_int k % l
+          | Fail v3 => ARB
+          | Diverge => ARB
+   
+   [insert_in_slot_t_rel_def]  Definition
+      
+      ⊢ ∀l key value slot slot1.
+          insert_in_slot_t_rel l key value slot slot1 ⇔
+          slot_t_inv l (hash_mod_key key l) slot1 ∧
+          slot_t_lookup key slot1 = SOME value ∧
+          (∀k. k ≠ key ⇒ slot_t_lookup k slot = slot_t_lookup k slot1) ∧
+          case slot_t_lookup key slot of
+            NONE => len (list_t_v slot1) = len (list_t_v slot) + 1
+          | SOME v => len (list_t_v slot1) = len (list_t_v slot)
+   
+   [len_s_def]  Definition
+      
+      ⊢ ∀hm. len_s hm = len (hash_map_t_al_v hm)
+   
+   [list_t_v_def]  Definition
+      
+      ⊢ list_t_v ListNil = [] ∧
+        ∀k v tl. list_t_v (ListCons k v tl) = (k,v)::list_t_v tl
+   
+   [lookup_s_def]  Definition
+      
+      ⊢ ∀hm k.
+          lookup_s hm k = slots_t_lookup (vec_to_list hm.hash_map_slots) k
+   
+   [pairwise_rel_def]  Definition
+      
+      ⊢ (∀p. pairwise_rel p [] ⇔ T) ∧
+        ∀p x ls.
+          pairwise_rel p (x::ls) ⇔ EVERY (p x) ls ∧ pairwise_rel p ls
+   
+   [slot_s_inv_def]  Definition
+      
+      ⊢ ∀l i ls.
+          slot_s_inv l i ls ⇔ distinct_keys ls ∧ slot_s_inv_hash l i ls
+   
+   [slot_s_inv_hash_def]  Definition
+      
+      ⊢ ∀l i ls.
+          slot_s_inv_hash l i ls ⇔
+          ∀k v. MEM (k,v) ls ⇒ hash_mod_key k l = i
+   
+   [slot_t_inv_def]  Definition
+      
+      ⊢ ∀l i s. slot_t_inv l i s ⇔ slot_s_inv l i (list_t_v s)
+   
+   [slot_t_lookup_def]  Definition
+      
+      ⊢ ∀key ls. slot_t_lookup key ls = lookup key (list_t_v ls)
+   
+   [slot_t_remove_def]  Definition
+      
+      ⊢ ∀key ls. slot_t_remove key ls = remove key (list_t_v ls)
+   
+   [slots_s_inv_def]  Definition
+      
+      ⊢ ∀s. slots_s_inv s ⇔
+            ∀i. 0 ≤ i ⇒ i < len s ⇒ slot_t_inv (len s) i (index i s)
+   
+   [slots_t_inv_def]  Definition
+      
+      ⊢ ∀s. slots_t_inv s ⇔ slots_s_inv (vec_to_list s)
+   
+   [slots_t_lookup_def]  Definition
+      
+      ⊢ ∀s k.
+          slots_t_lookup s k =
+          (let
+             i = hash_mod_key k (len s);
+             slot = index i s
+           in
+             slot_t_lookup k slot)
+   
+   [EVERY_quant_equiv]  Theorem
+      
+      ⊢ ∀p ls. EVERY p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
+   
+   [FLAT_ListNil_is_nil]  Theorem
+      
+      ⊢ EVERY (λx. x = ListNil) ls ⇒ FLAT (MAP list_t_v ls) = []
+   
+   [MEM_EVERY_not]  Theorem
+      
+      ⊢ ∀k v ls. MEM (k,v) ls ⇒ EVERY (λx. k ≠ FST x) ls ⇒ F
+   
+   [MEM_distinct_keys_lookup]  Theorem
+      
+      ⊢ ∀k v ls. MEM (k,v) ls ⇒ distinct_keys ls ⇒ lookup k ls = SOME v
+   
+   [distinct_keys_MEM_not_eq]  Theorem
+      
+      ⊢ ∀ls k1 x1 k2 x2.
+          distinct_keys ((k1,x1)::ls) ⇒ MEM (k2,x2) ls ⇒ k2 ≠ k1
+   
+   [distinct_keys_lookup_NONE]  Theorem
+      
+      ⊢ ∀ls k x. distinct_keys ((k,x)::ls) ⇒ lookup k ls = NONE
+   
+   [every_distinct_remove_every_distinct]  Theorem
+      
+      ⊢ ∀k0 k1 ls0.
+          EVERY (λy. k1 ≠ FST y) ls0 ⇒
+          EVERY (λy. k1 ≠ FST y) (remove k0 ls0)
+   
+   [hash_map_allocate_slots_fwd_spec]  Theorem
+      
+      ⊢ ∀n. usize_to_int n ≤ usize_max ⇒
+            ∃slots.
+              hash_map_allocate_slots_fwd vec_new n = Return slots ∧
+              slots_t_inv slots ∧
+              len (vec_to_list slots) = usize_to_int n ∧
+              EVERY (λx. x = ListNil) (vec_to_list slots)
+   
+   [hash_map_allocate_slots_loop_fwd_spec]  Theorem
+      
+      ⊢ ∀slots n.
+          EVERY (λx. x = ListNil) (vec_to_list slots) ⇒
+          len (vec_to_list slots) + usize_to_int n ≤ usize_max ⇒
+          ∃nslots.
+            hash_map_allocate_slots_loop_fwd slots n = Return nslots ∧
+            len (vec_to_list nslots) =
+            len (vec_to_list slots) + usize_to_int n ∧
+            EVERY (λx. x = ListNil) (vec_to_list nslots)
+   
+   [hash_map_clear_fwd_back_spec]  Theorem
+      
+      ⊢ ∀hm.
+          hash_map_t_inv hm ⇒
+          ∃hm1.
+            hash_map_clear_fwd_back hm = Return hm1 ∧ hash_map_t_inv hm1 ∧
+            len_s hm1 = 0 ∧ ∀k. lookup_s hm1 k = NONE
+   
+   [hash_map_clear_loop_fwd_back_spec]  Theorem
+      
+      ⊢ ∀slots. ∃slots1.
+          hash_map_clear_loop_fwd_back slots (int_to_usize 0) =
+          Return slots1 ∧
+          len (vec_to_list slots1) = len (vec_to_list slots) ∧
+          (∀j. 0 ≤ j ⇒
+               j < len (vec_to_list slots) ⇒
+               index j (vec_to_list slots1) = ListNil) ∧
+          FLAT (MAP list_t_v (vec_to_list slots1)) = []
+   
+   [hash_map_clear_loop_fwd_back_spec_aux]  Theorem
+      
+      ⊢ ∀n slots i.
+          n = len (vec_to_list slots) − usize_to_int i ⇒
+          ∃slots1.
+            hash_map_clear_loop_fwd_back slots i = Return slots1 ∧
+            len (vec_to_list slots1) = len (vec_to_list slots) ∧
+            (∀j. 0 ≤ j ⇒
+                 j < usize_to_int i ⇒
+                 j < len (vec_to_list slots) ⇒
+                 index j (vec_to_list slots1) = index j (vec_to_list slots)) ∧
+            ∀j. usize_to_int i ≤ j ⇒
+                j < len (vec_to_list slots) ⇒
+                index j (vec_to_list slots1) = ListNil
+   
+   [hash_map_cond_incr_thm]  Theorem
+      
+      ⊢ ∀hm key a.
+          hash_map_t_base_inv hm ⇒
+          (slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE ⇒
+           len_s hm < usize_max) ⇒
+          ∃n. (if
+                 slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE
+               then
+                 usize_add hm.hash_map_num_entries (int_to_usize 1)
+               else Return hm.hash_map_num_entries) =
+              Return n ∧
+              if
+                slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE
+              then
+                usize_to_int n = usize_to_int hm.hash_map_num_entries + 1
+              else n = hm.hash_map_num_entries
+   
+   [hash_map_contains_key_fwd_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          hash_map_contains_key_fwd hm key =
+          Return (lookup_s hm key ≠ NONE)
+   
+   [hash_map_contains_key_in_list_fwd_spec]  Theorem
+      
+      ⊢ ∀key ls.
+          hash_map_contains_key_in_list_fwd key ls =
+          Return (slot_t_lookup key ls ≠ NONE)
+   
+   [hash_map_get_fwd_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          case hash_map_get_fwd hm key of
+            Return x => lookup_s hm key = SOME x
+          | Fail v1 => lookup_s hm key = NONE
+          | Diverge => F
+   
+   [hash_map_get_in_list_fwd_spec]  Theorem
+      
+      ⊢ ∀ls key.
+          case hash_map_get_in_list_fwd key ls of
+            Return x => slot_t_lookup key ls = SOME x
+          | Fail v1 => slot_t_lookup key ls = NONE
+          | Diverge => F
+   
+   [hash_map_get_mut_back_spec]  Theorem
+      
+      ⊢ ∀hm key nx.
+          lookup_s hm key ≠ NONE ⇒
+          hash_map_t_inv hm ⇒
+          ∃hm1.
+            hash_map_get_mut_back hm key nx = Return hm1 ∧
+            lookup_s hm1 key = SOME nx ∧
+            ∀k. k ≠ key ⇒ lookup_s hm1 k = lookup_s hm k
+   
+   [hash_map_get_mut_fwd_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          case hash_map_get_mut_fwd hm key of
+            Return x => lookup_s hm key = SOME x
+          | Fail v1 => lookup_s hm key = NONE
+          | Diverge => F
+   
+   [hash_map_get_mut_in_list_back_spec]  Theorem
+      
+      ⊢ ∀ls key nx.
+          slot_t_lookup key ls ≠ NONE ⇒
+          ∃nls.
+            hash_map_get_mut_in_list_back ls key nx = Return nls ∧
+            slot_t_lookup key nls = SOME nx ∧
+            ∀k. k ≠ key ⇒ slot_t_lookup k nls = slot_t_lookup k ls
+   
+   [hash_map_get_mut_in_list_fwd_spec]  Theorem
+      
+      ⊢ ∀ls key.
+          case hash_map_get_mut_in_list_fwd ls key of
+            Return x => slot_t_lookup key ls = SOME x
+          | Fail v1 => slot_t_lookup key ls = NONE
+          | Diverge => F
+   
+   [hash_map_insert_fwd_back_spec]  Theorem
+      
+      [oracles: DISK_THM] [axioms: usize_u32_bounds] []
+      ⊢ ∀hm key value.
+          hash_map_t_inv hm ⇒
+          (lookup_s hm key = NONE ⇒ len_s hm < usize_max) ⇒
+          ∃hm1.
+            hash_map_insert_fwd_back hm key value = Return hm1 ∧
+            hash_map_t_inv hm1 ∧ lookup_s hm1 key = SOME value ∧
+            (∀k. k ≠ key ⇒ lookup_s hm k = lookup_s hm1 k) ∧
+            case lookup_s hm key of
+              NONE => len_s hm1 = len_s hm + 1
+            | SOME v => len_s hm1 = len_s hm
+   
+   [hash_map_insert_in_list_fwd_spec]  Theorem
+      
+      ⊢ ∀ls key value. ∃b.
+          hash_map_insert_in_list_fwd key value ls = Return b ∧
+          (b ⇔ slot_t_lookup key ls = NONE)
+   
+   [hash_map_insert_in_list_loop_back_EVERY_distinct_keys]  Theorem
+      
+      ⊢ ∀k v k1 ls0 ls1.
+          k1 ≠ k ⇒
+          EVERY (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
+          pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
+          hash_map_insert_in_list_loop_back k v ls0 = Return ls1 ⇒
+          EVERY (λy. k1 ≠ FST y) (list_t_v ls1)
+   
+   [hash_map_insert_in_list_loop_back_distinct_keys]  Theorem
+      
+      ⊢ ∀k v ls0 ls1.
+          distinct_keys (list_t_v ls0) ⇒
+          hash_map_insert_in_list_loop_back k v ls0 = Return ls1 ⇒
+          distinct_keys (list_t_v ls1)
+   
+   [hash_map_insert_in_list_loop_back_spec]  Theorem
+      
+      ⊢ ∀i ls key value.
+          distinct_keys (list_t_v ls) ⇒
+          ∃ls1.
+            hash_map_insert_in_list_loop_back key value ls = Return ls1 ∧
+            ∀l. slot_s_inv_hash l (hash_mod_key key l) (list_t_v ls) ⇒
+                insert_in_slot_t_rel l key value ls ls1
+   
+   [hash_map_insert_in_list_loop_back_spec_aux]  Theorem
+      
+      ⊢ ∀ls key value. ∃ls1.
+          hash_map_insert_in_list_loop_back key value ls = Return ls1 ∧
+          slot_t_lookup key ls1 = SOME value ∧
+          (∀k. k ≠ key ⇒ slot_t_lookup k ls = slot_t_lookup k ls1) ∧
+          (∀l. slot_s_inv_hash l (hash_mod_key key l) (list_t_v ls) ⇒
+               slot_s_inv_hash l (hash_mod_key key l) (list_t_v ls1)) ∧
+          case slot_t_lookup key ls of
+            NONE => len (list_t_v ls1) = len (list_t_v ls) + 1
+          | SOME v => len (list_t_v ls1) = len (list_t_v ls)
+   
+   [hash_map_insert_in_list_loop_fwd_spec]  Theorem
+      
+      ⊢ ∀ls key value. ∃b.
+          hash_map_insert_in_list_loop_fwd key value ls = Return b ∧
+          (b ⇔ slot_t_lookup key ls = NONE)
+   
+   [hash_map_insert_no_resize_fwd_back_branches_eq]  Theorem
+      
+      ⊢ (if slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE then
+           do
+             i0 <- usize_add hm.hash_map_num_entries (int_to_usize 1);
+             l0 <-
+               hash_map_insert_in_list_back key value
+                 (vec_index hm.hash_map_slots a);
+             v <- vec_index_mut_back hm.hash_map_slots a l0;
+             Return
+               (hm with <|hash_map_num_entries := i0; hash_map_slots := v|>)
+           od
+         else
+           do
+             l0 <-
+               hash_map_insert_in_list_back key value
+                 (vec_index hm.hash_map_slots a);
+             v <- vec_index_mut_back hm.hash_map_slots a l0;
+             Return (hm with hash_map_slots := v)
+           od) =
+        do
+          i0 <-
+            if
+              slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE
+            then
+              usize_add hm.hash_map_num_entries (int_to_usize 1)
+            else Return hm.hash_map_num_entries;
+          l0 <-
+            hash_map_insert_in_list_back key value
+              (vec_index hm.hash_map_slots a);
+          v <- vec_index_mut_back hm.hash_map_slots a l0;
+          Return
+            (hm with <|hash_map_num_entries := i0; hash_map_slots := v|>)
+        od
+   
+   [hash_map_insert_no_resize_fwd_back_spec]  Theorem
+      
+      ⊢ ∀hm key value.
+          hash_map_t_base_inv hm ⇒
+          (lookup_s hm key = NONE ⇒ len_s hm < usize_max) ⇒
+          ∃hm1.
+            hash_map_insert_no_resize_fwd_back hm key value = Return hm1 ∧
+            hash_map_t_base_inv hm1 ∧ lookup_s hm1 key = SOME value ∧
+            (∀k. k ≠ key ⇒ lookup_s hm k = lookup_s hm1 k) ∧
+            (case lookup_s hm key of
+               NONE => len_s hm1 = len_s hm + 1
+             | SOME v => len_s hm1 = len_s hm) ∧
+            hash_map_same_params hm hm1
+   
+   [hash_map_insert_no_resize_fwd_back_spec_aux]  Theorem
+      
+      ⊢ ∀hm key value.
+          hash_map_t_base_inv hm ⇒
+          (lookup_s hm key = NONE ⇒ len_s hm < usize_max) ⇒
+          ∃hm1 slot1.
+            hash_map_insert_no_resize_fwd_back hm key value = Return hm1 ∧
+            len (vec_to_list hm1.hash_map_slots) =
+            len (vec_to_list hm.hash_map_slots) ∧
+            (let
+               l = len (vec_to_list hm.hash_map_slots);
+               i = hash_mod_key key (len (vec_to_list hm.hash_map_slots));
+               slot = index i (vec_to_list hm.hash_map_slots)
+             in
+               insert_in_slot_t_rel l key value slot slot1 ∧
+               vec_to_list hm1.hash_map_slots =
+               update (vec_to_list hm.hash_map_slots) i slot1 ∧
+               hm1.hash_map_max_load_factor = hm.hash_map_max_load_factor ∧
+               hm1.hash_map_max_load = hm.hash_map_max_load ∧
+               (case lookup_s hm key of
+                  NONE =>
+                    usize_to_int hm1.hash_map_num_entries =
+                    usize_to_int hm.hash_map_num_entries + 1
+                | SOME v =>
+                  hm1.hash_map_num_entries = hm.hash_map_num_entries) ∧
+               hash_map_same_params hm hm1)
+   
+   [hash_map_len_spec]  Theorem
+      
+      ⊢ ∀hm.
+          hash_map_t_base_inv hm ⇒
+          ∃x. hash_map_len_fwd hm = Return x ∧ usize_to_int x = len_s hm
+   
+   [hash_map_move_elements_from_list_fwd_back_spec]  Theorem
+      
+      ⊢ ∀hm ls.
+          (let
+             l = len (list_t_v ls)
+           in
+             hash_map_t_base_inv hm ⇒
+             len_s hm + l ≤ usize_max ⇒
+             ∃hm1.
+               hash_map_move_elements_from_list_fwd_back hm ls = Return hm1 ∧
+               hash_map_t_base_inv hm1 ∧
+               ((∀k v. MEM (k,v) (list_t_v ls) ⇒ lookup_s hm k = NONE) ⇒
+                distinct_keys (list_t_v ls) ⇒
+                (∀k. slot_t_lookup k ls = NONE ⇒
+                     lookup_s hm1 k = lookup_s hm k) ∧
+                (∀k. slot_t_lookup k ls ≠ NONE ⇒
+                     lookup_s hm1 k = slot_t_lookup k ls) ∧
+                len_s hm1 = len_s hm + l) ∧ hash_map_same_params hm hm1)
+   
+   [hash_map_move_elements_fwd_back_spec]  Theorem
+      
+      ⊢ ∀hm slots i.
+          (let
+             slots_l =
+               len
+                 (FLAT
+                    (MAP list_t_v
+                       (drop (usize_to_int i) (vec_to_list slots))))
+           in
+             hash_map_t_base_inv hm ⇒
+             len_s hm + slots_l ≤ usize_max ⇒
+             (∀j. (let
+                     l = len (vec_to_list slots)
+                   in
+                     usize_to_int i ≤ j ⇒
+                     j < l ⇒
+                     (let
+                        slot = index j (vec_to_list slots)
+                      in
+                        slot_t_inv l j slot ∧
+                        ∀k v.
+                          MEM (k,v) (list_t_v slot) ⇒ lookup_s hm k = NONE))) ⇒
+             ∃hm1 slots1.
+               hash_map_move_elements_fwd_back hm slots i =
+               Return (hm1,slots1) ∧ hash_map_t_base_inv hm1 ∧
+               len_s hm1 = len_s hm + slots_l ∧
+               (∀k. lookup_s hm1 k =
+                    case lookup_s hm k of
+                      NONE =>
+                        (let
+                           j = hash_mod_key k (len (vec_to_list slots))
+                         in
+                           if
+                             usize_to_int i ≤ j ∧
+                             j < len (vec_to_list slots)
+                           then
+                             (let
+                                slot = index j (vec_to_list slots)
+                              in
+                                lookup k (list_t_v slot))
+                           else NONE)
+                    | SOME v => SOME v) ∧ hash_map_same_params hm hm1)
+   
+   [hash_map_move_elements_loop_fwd_back_spec_aux]  Theorem
+      
+      ⊢ ∀hm slots i n.
+          (let
+             slots_l =
+               len
+                 (FLAT
+                    (MAP list_t_v
+                       (drop (usize_to_int i) (vec_to_list slots))))
+           in
+             n = len (vec_to_list slots) − usize_to_int i ⇒
+             hash_map_t_base_inv hm ⇒
+             len_s hm + slots_l ≤ usize_max ⇒
+             (∀j. (let
+                     l = len (vec_to_list slots)
+                   in
+                     usize_to_int i ≤ j ⇒
+                     j < l ⇒
+                     (let
+                        slot = index j (vec_to_list slots)
+                      in
+                        slot_t_inv l j slot ∧
+                        ∀k v.
+                          MEM (k,v) (list_t_v slot) ⇒ lookup_s hm k = NONE))) ⇒
+             ∃hm1 slots1.
+               hash_map_move_elements_loop_fwd_back hm slots i =
+               Return (hm1,slots1) ∧ hash_map_t_base_inv hm1 ∧
+               len_s hm1 = len_s hm + slots_l ∧
+               (∀k. lookup_s hm1 k =
+                    case lookup_s hm k of
+                      NONE =>
+                        (let
+                           j = hash_mod_key k (len (vec_to_list slots))
+                         in
+                           if
+                             usize_to_int i ≤ j ∧
+                             j < len (vec_to_list slots)
+                           then
+                             (let
+                                slot = index j (vec_to_list slots)
+                              in
+                                lookup k (list_t_v slot))
+                           else NONE)
+                    | SOME v => SOME v) ∧ hash_map_same_params hm hm1)
+   
+   [hash_map_new_fwd_spec]  Theorem
+      
+      ⊢ ∃hm.
+          hash_map_new_fwd = Return hm ∧ hash_map_t_inv hm ∧
+          ∀k. lookup_s hm k = NONE ∧ len_s hm = 0
+   
+   [hash_map_new_with_capacity_fwd_spec]  Theorem
+      
+      ⊢ ∀capacity max_load_dividend max_load_divisor.
+          0 < usize_to_int max_load_dividend ⇒
+          usize_to_int max_load_dividend < usize_to_int max_load_divisor ⇒
+          0 < usize_to_int capacity ⇒
+          usize_to_int capacity * usize_to_int max_load_dividend ≥
+          usize_to_int max_load_divisor ⇒
+          usize_to_int capacity * usize_to_int max_load_dividend ≤
+          usize_max ⇒
+          ∃hm.
+            hash_map_new_with_capacity_fwd capacity max_load_dividend
+              max_load_divisor =
+            Return hm ∧ hash_map_t_inv hm ∧ len_s hm = 0 ∧
+            ∀k. lookup_s hm k = NONE ∧
+                len (vec_to_list hm.hash_map_slots) = usize_to_int capacity ∧
+                hm.hash_map_max_load_factor =
+                (max_load_dividend,max_load_divisor)
+   
+   [hash_map_remove_back_branch_eq]  Theorem
+      
+      ⊢ ∀key hm a.
+          (case lookup key (list_t_v (vec_index hm.hash_map_slots a)) of
+             NONE =>
+               do
+                 l0 <-
+                   hash_map_remove_from_list_back key
+                     (vec_index hm.hash_map_slots a);
+                 v <- vec_index_mut_back hm.hash_map_slots a l0;
+                 Return (hm with hash_map_slots := v)
+               od
+           | SOME x0 =>
+             do
+               i0 <- usize_sub hm.hash_map_num_entries (int_to_usize 1);
+               l0 <-
+                 hash_map_remove_from_list_back key
+                   (vec_index hm.hash_map_slots a);
+               v <- vec_index_mut_back hm.hash_map_slots a l0;
+               Return
+                 (hm with
+                  <|hash_map_num_entries := i0; hash_map_slots := v|>)
+             od) =
+          do
+            i0 <-
+              case lookup key (list_t_v (vec_index hm.hash_map_slots a)) of
+                NONE => Return hm.hash_map_num_entries
+              | SOME v =>
+                usize_sub hm.hash_map_num_entries (int_to_usize 1);
+            l0 <-
+              hash_map_remove_from_list_back key
+                (vec_index hm.hash_map_slots a);
+            v <- vec_index_mut_back hm.hash_map_slots a l0;
+            Return
+              (hm with <|hash_map_num_entries := i0; hash_map_slots := v|>)
+          od
+   
+   [hash_map_remove_back_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          ∃hm1.
+            hash_map_remove_back hm key = Return hm1 ∧ hash_map_t_inv hm1 ∧
+            lookup_s hm1 key = NONE ∧
+            (∀k. k ≠ key ⇒ lookup_s hm1 k = lookup_s hm k) ∧
+            case lookup_s hm key of
+              NONE => len_s hm1 = len_s hm
+            | SOME v => len_s hm1 = len_s hm − 1
+   
+   [hash_map_remove_from_list_back_spec]  Theorem
+      
+      ⊢ ∀key ls. ∃ls1.
+          hash_map_remove_from_list_back key ls = Return ls1 ∧
+          ∀l i.
+            slot_t_inv l i ls ⇒
+            slot_t_inv l i ls1 ∧ list_t_v ls1 = remove key (list_t_v ls) ∧
+            slot_t_lookup key ls1 = NONE ∧
+            (∀k. k ≠ key ⇒ slot_t_lookup k ls1 = slot_t_lookup k ls) ∧
+            case slot_t_lookup key ls of
+              NONE => len (list_t_v ls1) = len (list_t_v ls)
+            | SOME v => len (list_t_v ls1) = len (list_t_v ls) − 1
+   
+   [hash_map_remove_from_list_fwd_spec]  Theorem
+      
+      ⊢ ∀key l i ls.
+          hash_map_remove_from_list_fwd key ls =
+          Return (slot_t_lookup key ls)
+   
+   [hash_map_remove_fwd_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          hash_map_remove_fwd hm key = Return (lookup_s hm key)
+   
+   [hash_map_same_params_refl]  Theorem
+      
+      ⊢ ∀hm. hash_map_same_params hm hm
+   
+   [hash_map_t_base_inv_len_slots]  Theorem
+      
+      ⊢ ∀hm.
+          hash_map_t_base_inv hm ⇒ 0 < len (vec_to_list hm.hash_map_slots)
+   
+   [hash_map_try_resize_fwd_back_spec]  Theorem
+      
+      [oracles: DISK_THM] [axioms: usize_u32_bounds] []
+      ⊢ ∀hm.
+          hash_map_t_base_inv hm ⇒
+          hash_map_just_before_resize_pred hm ⇒
+          ∃hm1.
+            hash_map_try_resize_fwd_back hm = Return hm1 ∧
+            hash_map_t_inv hm1 ∧ len_s hm1 = len_s hm ∧
+            ∀k. lookup_s hm1 k = lookup_s hm k
+   
+   [key_MEM_j_lookup_i_is_NONE]  Theorem
+      
+      ⊢ ∀i j slots k v.
+          usize_to_int i < j ⇒
+          j < len (vec_to_list slots) ⇒
+          (∀j. usize_to_int i ≤ j ⇒
+               j < len (vec_to_list slots) ⇒
+               slot_t_inv (len (vec_to_list slots)) j
+                 (index j (vec_to_list slots))) ⇒
+          MEM (k,v) (list_t_v (index j (vec_to_list slots))) ⇒
+          slot_t_lookup k (index (usize_to_int i) (vec_to_list slots)) =
+          NONE
+   
+   [len_FLAT_MAP_update]  Theorem
+      
+      ⊢ ∀x ls i.
+          0 ≤ i ⇒
+          i < len ls ⇒
+          len (FLAT (MAP list_t_v (update ls i x))) =
+          len (FLAT (MAP list_t_v ls)) + len (list_t_v x) −
+          len (list_t_v (index i ls))
+   
+   [len_index_FLAT_MAP_list_t_v]  Theorem
+      
+      ⊢ ∀slots i.
+          0 ≤ i ⇒
+          i < len slots ⇒
+          len (list_t_v (index i slots)) ≤
+          len (FLAT (MAP list_t_v (drop i slots)))
+   
+   [len_vec_FLAT_drop_update]  Theorem
+      
+      ⊢ ∀slots i.
+          0 ≤ i ⇒
+          i < len slots ⇒
+          len (FLAT (MAP list_t_v (drop i slots))) =
+          len (list_t_v (index i slots)) +
+          len (FLAT (MAP list_t_v (drop (i + 1) (update slots i ListNil))))
+   
+   [lookup_SOME_not_empty]  Theorem
+      
+      ⊢ ∀ls k. lookup k ls ≠ NONE ⇒ 0 < len ls
+   
+   [lookup_cond_decr_entries_eq]  Theorem
+      
+      ⊢ ∀hm key i.
+          hash_map_t_inv hm ⇒
+          usize_to_int i < len (vec_to_list hm.hash_map_slots) ⇒
+          ∃j. (case
+                 lookup key (list_t_v (vec_index hm.hash_map_slots i))
+               of
+                 NONE => Return hm.hash_map_num_entries
+               | SOME v =>
+                 usize_sub hm.hash_map_num_entries (int_to_usize 1)) =
+              Return j ∧
+              (lookup key (list_t_v (vec_index hm.hash_map_slots i)) = NONE ⇒
+               j = hm.hash_map_num_entries) ∧
+              (lookup key (list_t_v (vec_index hm.hash_map_slots i)) ≠ NONE ⇒
+               usize_to_int j + 1 = usize_to_int hm.hash_map_num_entries)
+   
+   [lookup_def]  Theorem
+      
+      ⊢ (∀key. lookup key [] = NONE) ∧
+        ∀v ls key k.
+          lookup key ((k,v)::ls) =
+          if k = key then SOME v else lookup key ls
+   
+   [lookup_distinct_keys_MEM]  Theorem
+      
+      ⊢ ∀k v ls. lookup k ls = SOME v ⇒ distinct_keys ls ⇒ MEM (k,v) ls
+   
+   [lookup_ind]  Theorem
+      
+      ⊢ ∀P. (∀key. P key []) ∧
+            (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
+            ∀v v1. P v v1
+   
+   [lookup_s_SOME_not_empty]  Theorem
+      
+      ⊢ ∀hm key. hash_map_t_inv hm ⇒ lookup_s hm key ≠ NONE ⇒ 0 < len_s hm
+   
+   [pairwise_rel_quant_equiv]  Theorem
+      
+      ⊢ ∀p ls.
+          pairwise_rel p ls ⇔
+          ∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls)
+   
+   [remove_def]  Theorem
+      
+      ⊢ (∀key. remove key [] = []) ∧
+        ∀v ls key k.
+          remove key ((k,v)::ls) =
+          if k = key then ls else (k,v)::remove key ls
+   
+   [remove_ind]  Theorem
+      
+      ⊢ ∀P. (∀key. P key []) ∧
+            (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
+            ∀v v1. P v v1
+   
+   [slot_t_lookup_SOME_not_empty]  Theorem
+      
+      ⊢ ∀ls i k.
+          0 ≤ i ⇒
+          i < len ls ⇒
+          slot_t_lookup k (index i ls) ≠ NONE ⇒
+          0 < len (FLAT (MAP list_t_v ls))
+   
+   
+*)
+end