Make good progress on the proofs of the hashmap in HOL4

1 files changed, 686 insertions, 46 deletions

diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 2dc2f375..e96f7e34 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -1,19 +1,88 @@
-(*open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory*)
-(*open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory *)
-open primitivesLib listTheory ilistTheory hashmap_TypesTheory hashmap_FunsTheory
+open primitivesLib primitivesArithTheory primitivesTheory listTheory ilistTheory hashmap_TypesTheory hashmap_FunsTheory
 
 val _ = new_theory "hashmap_Properties"
 
+val pairwise_rel_def = Define ‘
+  pairwise_rel p [] = T ∧
+  pairwise_rel p (x :: ls) = (EVERY (p x) ls ∧ pairwise_rel p ls)
+’
+
+(* TODO: move *)
+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] >>
+  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
+QED
+
+(* TODO: move *)
+Theorem pairwise_rel_quant_equiv:
+  ∀p ls. pairwise_rel p ls ⇔
+    (∀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] >>
+  equiv_tac
+  >-(
+    (* ==> *)
+    rw [] >>
+    sg ‘0 < j’ >- int_tac >>
+    Cases_on ‘i = 0’
+    >-(
+      simp [index_eq] >>
+      qspecl_assume [‘p h’, ‘ls’] (iffLR EVERY_quant_equiv) >>
+      first_x_assum irule >> fs [] >> int_tac
+    ) >>
+    rw [index_eq] >>
+    first_x_assum irule >> int_tac
+  ) >>
+  (* <== *)
+  rw []
+  >-(
+    rw [EVERY_quant_equiv] >>
+    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 []
+QED
 
 Type key_t = “:usize”
 
-Definition for_all_def:
-  for_all p [] = T ∧
-  for_all p (x :: ls) = (p x ∧ for_all p ls)
-End
+val distinct_keys_def = Define ‘
+  distinct_keys (ls : (key_t # 't) list) =
+    pairwise_rel (\x y. FST x ≠ FST y) ls
+’
 
 (* Conversion from “:list_t” to “:list” *)
-Definition list_t_v:
+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
@@ -39,8 +108,29 @@ Definition slot_t_remove_def:
   slot_t_remove key ls = remove key (list_t_v ls)
 End
 
+Definition hash_mod_key_def:
+  hash_mod_key k (l : int) : int =
+    case hash_key_fwd k of
+    | Return k => usize_to_int k % l
+    | _ => ARB
+End
+
+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
+
 Definition slot_s_inv_def:
-  slot_s_inv (i : int) (ls : (key_t # 'b) list) : bool = (
+  slot_s_inv (l : int) (i : int) (ls : (key_t # 'b) list) : bool = (
+    distinct_keys ls ∧
+    slot_s_inv_hash l i ls
+  )
+End
+
+(* TODO: try with this invariant:
+
+Definition slot_s_inv_def:a
+  slot_s_inv (i : int) (ls : (key_t # 'b) list) : bool =
     (∀ k. lookup k ls ≠ NONE ⇒ lookup k (remove k ls) = NONE) ∧
     (∀ k v. MEM (k, v) ls ⇒
       ∃ hk. hash_key_fwd k = Return hk ⇒
@@ -48,8 +138,10 @@ Definition slot_s_inv_def:
     )
 End
 
+*)
+
 Definition slot_t_inv_def:
-  slot_t_inv (i : int) (s : 't list_t) = slot_s_inv i (list_t_v s)
+  slot_t_inv (l : int) (i : int) (s : 't list_t) = slot_s_inv l i (list_t_v s)
 End
 
 (* Representation function of the hash map as a list of slots *)
@@ -65,7 +157,7 @@ End
 
 Definition slots_s_inv_def:
   slots_s_inv (s : 'a list_t list) =
-    ∀ (i : int). 0 ≤ i ⇒ i < len s ⇒ slot_t_inv i (index i s)
+    ∀ (i : int). 0 ≤ i ⇒ i < len s ⇒ slot_t_inv (len s) i (index i s)
 End
 
 Definition slots_t_inv_def:
@@ -111,46 +203,41 @@ Definition len_s_def:
   len_s hm = len (hash_map_t_al_v hm)
 End
 
-Definition hash_mod_key_def:
-  hash_mod_key k (l : int) : int =
-    case hash_key_fwd k of
-    | Return k => usize_to_int k % l
-    | _ => ARB
-End
-
 Definition slots_t_lookup_def:
-  slots_t_find (s : 't list_t list) (k : key_t) : 't option = 
+  slots_t_lookup (s : 't list_t list) (k : key_t) : 't option = 
     let i = hash_mod_key k (len s) in
     let slot = index i s in
     slot_t_lookup k slot
 End
 
-Definition find_s_def:
-  find_s (hm : 't hash_map_t) (k : key_t) : 't option =
-    slots_t_find (vec_to_list hm.hash_map_slots) k
+Definition lookup_s_def:
+  lookup_s (hm : 't hash_map_t) (k : key_t) : 't option =
+    slots_t_lookup (vec_to_list hm.hash_map_slots) k
 End
 
-(* Proofs *)
+(*============================================================================*
+ *============================================================================*
+ *  Proofs
+ *============================================================================*
+ *============================================================================*)
 
-
-(* TODO: move *)
-Theorem for_all_append:
-  ∀ p ls0 ls1. for_all p ls0 ⇒ for_all p ls1 ⇒ for_all p (ls0 ++ ls1)
-Proof
-  Induct_on ‘ls0’ >> fs [for_all_def]
-QED
+(*============================================================================*
+ *  New
+ *============================================================================*)
 
 Theorem hash_map_allocate_slots_loop_fwd_spec:
   ∀ slots n.
-    for_all (\x. x = ListNil) (vec_to_list slots) ⇒
+    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 ∧
-      for_all (\x. x = ListNil) (vec_to_list nslots)
+      EVERY (\x. x = ListNil) (vec_to_list nslots)
 Proof
+  (* TODO: induction principle for usize, etc. *)
   Induct_on ‘usize_to_int n’ >> rw [] >> massage >- int_tac >>
   pure_once_rewrite_tac [hash_map_allocate_slots_loop_fwd_def] >>
   fs [usize_gt_def] >> massage >> fs [] >>
+  (* TODO: would be good to simply use progress here *)
   case_tac
   >-(
     sg ‘len (vec_to_list slots) ≤ usize_max’ >- int_tac >>
@@ -167,14 +254,576 @@ Proof
     massage >> gvs [] >>
     sg ‘v = usize_to_int n - 1’ >- int_tac >> fs [] >>
     (* *)
-    progress
-    >-(irule for_all_append >> fs [for_all_def])
-    >-(fs [vec_len_def, len_append, len_def] >> int_tac)
-    >-(fs [vec_len_def, len_append, len_def] >> int_tac)
+    progress >>
+    fs [vec_len_def, len_append, len_def] >>
+    int_tac
   ) >>
   fs [] >>
   int_tac
 QED
+val _ = save_spec_thm "hash_map_allocate_slots_loop_fwd_spec"
+
+Theorem hash_map_allocate_slots_fwd_spec:
+  ∀ 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)
+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] >>
+  fs [EVERY_quant_equiv] >>
+  qpat_assum ‘∀i. _’ sg_dep_rewrite_all_tac >> gvs [list_t_v_def]
+QED
+val _ = save_spec_thm "hash_map_allocate_slots_fwd_spec"
+
+(* Auxiliary lemma *)
+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]
+QED
+
+Theorem hash_map_new_with_capacity_fwd_spec:
+  ∀ 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
+Proof
+  rw [] >> fs [hash_map_new_with_capacity_fwd_def] >>
+  progress >>
+  progress >>
+  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])
+  >-(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] >>
+  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] >>
+    massage >>
+    irule pos_mod_pos_is_pos >> fs []) >>
+  first_x_assum sg_premise_tac
+  >-(
+    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    massage >>
+    irule pos_mod_pos_lt >> fs []
+  ) >>  
+  fs [list_t_v_def, lookup_def]
+QED
+val _ = save_spec_thm "hash_map_new_with_capacity_fwd_spec"
+
+Theorem hash_map_new_fwd_spec:
+ ∃ hm. hash_map_new_fwd = Return hm ∧
+   hash_map_t_inv hm ∧
+   ∀ k. lookup_s hm k = NONE ∧
+   len_s hm = 0
+Proof
+  pure_rewrite_tac [hash_map_new_fwd_def] >>
+  progress >> massage >> fs [] >>
+  assume_tac usize_bounds >> fs [u16_max_def] >>
+  int_tac
+QED
+val _ = save_spec_thm "hash_map_new_fwd_spec"
+
+(*============================================================================*
+ *  Clear
+ *============================================================================*)
+
+(* [clear]: the loop doesn't fail and simply clears the slots starting at index i *)
+Theorem hash_map_clear_loop_fwd_back_spec_aux:
+  ∀ n slots i.
+    (* Small trick to make the induction work well *)
+    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) ∧
+    (*  The slots before i are left unchanged *)
+    (∀ 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)) ∧
+    (* The slots after i are set to ListNil *)
+    (∀ j. usize_to_int i ≤ j ⇒ j < len (vec_to_list slots) ⇒
+           index j (vec_to_list slots1) = ListNil)
+Proof
+  (* TODO: induction principle for usize, etc. *)
+  Induct_on ‘n’ >> rw [] >>
+  pure_once_rewrite_tac [hash_map_clear_loop_fwd_back_def] >>
+  fs [usize_lt_def, vec_len_def] >>
+  (* TODO: automate that *)
+  qspec_assume ‘slots’ vec_len_spec >> massage
+  >-(case_tac >> rw [] >> int_tac)
+  >-(rw [] >> int_tac) >>
+  case_tac
+  >-(
+    (* usize_to_int i < len (vec_to_list slots) *)
+    progress >>
+    progress >> massage >- int_tac >>
+    qspecl_assume [‘slots’, ‘i’, ‘ListNil’] vec_update_eq >> fs [] >>
+    progress >> rw []
+    >-(
+      (* Use the induction hypothesis *)
+      last_x_assum (qspec_assume ‘j’) >> gvs [] >>
+      sg ‘j < usize_to_int i + 1’ >- int_tac >> gvs [] >>
+      (* Use the vec_update eq *)
+      last_x_assum (qspec_assume ‘int_to_usize j’) >> gvs [vec_len_def] >> massage >>
+      gvs [] >>
+      sg ‘j ≠ usize_to_int i’ >- int_tac >>
+      fs [vec_index_def] >>
+      massage) >>
+    Cases_on ‘usize_to_int i = j’ >> fs [vec_index_def] >>
+    first_x_assum (qspec_assume ‘j’) >> gvs [] >>
+    sg ‘usize_to_int i + 1 ≤ j’ >- int_tac >> gvs [])
+  >>
+  rw [] >>
+  int_tac
+QED
+
+Theorem hash_map_clear_loop_fwd_back_spec:
+  ∀ 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) ∧
+    (* All the slots are set to ListNil *)
+    (∀ j. 0 ≤ j ⇒ j < len (vec_to_list slots) ⇒
+           index j (vec_to_list slots1) = ListNil) ∧
+    (* The map is empty *)
+    (FLAT (MAP list_t_v (vec_to_list slots1)) = [])
+Proof
+  rw [] >>
+  qspecl_assume [‘len (vec_to_list slots) − 0’, ‘slots’, ‘int_to_usize 0’]
+   hash_map_clear_loop_fwd_back_spec_aux >>
+  massage >> fs [] >>
+  irule FLAT_ListNil_is_nil >>
+  fs [EVERY_quant_equiv]
+QED
+val _ = save_spec_thm "hash_map_clear_loop_fwd_back_spec"
+
+Theorem hash_map_clear_fwd_back_spec:
+  ∀ 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)
+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 []
+  >-((* 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] >>
+   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]) >>
+   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] >>
+  (* 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 [] >>
+  (* TODO: automate that *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >> fs [] >>
+  qspecl_assume [‘usize_to_int k’, ‘len (vec_to_list hm.hash_map_slots)’] integerTheory.INT_MOD_BOUNDS >>
+  sg ‘len (vec_to_list hm.hash_map_slots) ≠ 0’
+  >-(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]
+QED
+val _ = save_spec_thm "hash_map_clear_fwd_back_spec"
+  
+
+(*============================================================================*
+ *  Len
+ *============================================================================*)
+
+Theorem hash_map_len_spec:
+  ∀ hm.
+    hash_map_t_inv hm ⇒
+    ∃ x. hash_map_len_fwd hm = Return x ∧
+    usize_to_int x = len_s hm
+Proof
+  rw [hash_map_len_fwd_def, hash_map_t_inv_def, hash_map_t_base_inv_def, len_s_def]
+QED
+val _ = save_spec_thm "hash_map_len_spec"
+
+
+(*============================================================================*
+ *  Insert
+ *============================================================================*)
+
+Theorem hash_map_insert_in_list_loop_fwd_spec:
+  !ls key value.
+    ∃ b. hash_map_insert_in_list_loop_fwd key value ls = Return b ∧
+    (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] >>
+  rw []
+QED
+val _ = save_spec_thm "hash_map_insert_in_list_loop_fwd_spec"
+
+Theorem hash_map_insert_in_list_fwd_spec:
+  !ls key value.
+    ∃ b. hash_map_insert_in_list_fwd key value ls = Return b ∧
+    (b ⇔ slot_t_lookup key ls = NONE)
+Proof
+  rw [hash_map_insert_in_list_fwd_def] >> progress >> fs []
+QED
+val _ = save_spec_thm "hash_map_insert_in_list_fwd_spec"
+
+(* Lemma about ‘hash_map_insert_in_list_loop_back’, without the invariant *)
+Theorem hash_map_insert_in_list_loop_back_spec_aux:
+  !ls key value.
+    ∃ ls1. hash_map_insert_in_list_loop_back key value ls = Return ls1 ∧
+    (* We updated the binding for key *)
+    slot_t_lookup key ls1 = SOME value /\
+    (* The other bindings are left unchanged *)
+    (!k. k <> key ==> slot_t_lookup k ls = slot_t_lookup k ls1) ∧
+    (* We preserve part of the key invariant *)
+    (∀ 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)) ∧
+    (* Reasoning about the length *)
+    (case slot_t_lookup key ls of
+     | 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’] >>
+  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 []) >>
+  case_tac >> fs [] >> int_tac
+QED
+
+(* Auxiliary lemma - TODO: move *)
+Theorem hash_map_insert_in_list_loop_back_EVERY_distinct_keys:
+  ∀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)
+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]) >>
+  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 ‘hash_map_insert_in_list_loop_back k v ls0’ >>
+  gvs [distinct_keys_def, list_t_v_def, pairwise_rel_def, EVERY_DEF] >>
+  metis_tac []
+QED
+
+Theorem hash_map_insert_in_list_loop_back_distinct_keys:
+  ∀ 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)
+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]) >>
+  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 ‘hash_map_insert_in_list_loop_back k v ls0’ >>
+  gvs [distinct_keys_def, list_t_v_def, pairwise_rel_def, EVERY_DEF] >>
+  metis_tac [hash_map_insert_in_list_loop_back_EVERY_distinct_keys]
+QED
+
+Definition insert_in_slot_t_rel_def:
+  insert_in_slot_t_rel l key value slot slot1 = (
+    (* We preserve the invariant *)
+    slot_t_inv l (hash_mod_key key l) slot1 ∧
+    (* We updated the binding for key *)
+    slot_t_lookup key slot1 = SOME value /\
+    (* The other bindings are left unchanged *)
+    (!k. k <> key ==> slot_t_lookup k slot = slot_t_lookup k slot1) ∧
+    (* Reasoning about the length *)
+    (case slot_t_lookup key slot of
+     | NONE => len (list_t_v slot1) = len (list_t_v slot) + 1
+     | SOME _ => len (list_t_v slot1) = len (list_t_v slot)))
+End
+
+(* Lemma about ‘hash_map_insert_in_list_loop_back’, with the invariant *)
+Theorem hash_map_insert_in_list_loop_back_spec:
+  !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)
+Proof
+  rw [slot_t_inv_def, slot_s_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]
+QED
+val _ = save_spec_thm "hash_map_insert_in_list_loop_back_spec"
+
+(* TODO: move and use more *)
+Theorem hash_map_t_base_inv_len_slots:
+  ∀ hm. hash_map_t_base_inv hm ⇒ 0 < len (vec_to_list hm.hash_map_slots)
+Proof
+  rw [hash_map_t_base_inv_def, vec_len_def] >> int_tac
+QED
+
+(* TODO: automatic rewriting? *)
+Theorem hash_map_insert_no_resize_fwd_back_branches_eq:
+  (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)
+Proof
+  case_tac >>
+  fs [bind_def] >>
+  case_tac >>
+  case_tac >>
+  Cases_on ‘hm’ >> fs [] >>
+  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
+
+Theorem hash_map_cond_incr_thm:
+  ∀ 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)
+Proof
+  rw [] >>
+  progress >>
+  massage >>
+  fs [len_s_def, hash_map_t_base_inv_def] >>
+  (* TODO: improve massage to not only look at variables *)
+  qspec_assume ‘hm.hash_map_num_entries’ usize_to_int_bounds >> fs [] >>
+  int_tac
+QED
+
+Theorem hash_map_insert_no_resize_fwd_back_spec_aux:
+  !hm key value.
+    (* Using the base invariant, because the full invariant is preserved only
+       if we resize *)
+    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) in
+    let i = hash_mod_key key (len (vec_to_list hm.hash_map_slots)) in
+    let 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 ∧
+    (* Reasoning about the length *)
+    (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 _ => hm1.hash_map_num_entries = hm.hash_map_num_entries)
+Proof
+  rw [hash_map_insert_no_resize_fwd_back_def] >>
+  fs [hash_key_fwd_def] >>
+  (* TODO: automate this *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >>
+  (* TODO: improve massage to not only look at variables *)
+  qspec_assume ‘hm.hash_map_num_entries’ usize_to_int_bounds >> fs [] >>
+  imp_res_tac hash_map_t_base_inv_len_slots >>
+  (* TODO: update usize_rem_spec? *)
+  qspecl_assume [‘usize_to_int key’, ‘len (vec_to_list hm.hash_map_slots)’] pos_rem_pos_ineqs >>
+  progress >>
+  progress >- ( (* TODO: why not done automatically? *) massage >> fs []) >>
+  progress >> gvs [] >>
+  (* Taking care of the disjunction *)
+  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 [] >>
+  (* 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] >>
+     last_x_assum (qspec_assume ‘usize_to_int a’) >>
+     gvs [vec_index_def, int_rem_def, slot_t_inv_def, slot_s_inv_def]) >>
+  fs [] >>
+  sg ‘usize_to_int a = usize_to_int key % len (vec_to_list hm.hash_map_slots)’
+  >-(fs [int_rem_def]) >>
+  sg ‘int_rem (usize_to_int key) (len (vec_to_list hm.hash_map_slots)) = usize_to_int key % len (vec_to_list hm.hash_map_slots)’
+  >-(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 [hash_map_insert_in_list_back_def] >>
+  progress >>
+  progress >- ((* TODO: *) massage >> fs []) >>
+  (* vec_update *)
+  qspecl_assume [‘hm.hash_map_slots’, ‘a’, ‘a'’] vec_update_eq >> gvs [] >>
+  (* Prove the post-condition *)
+  qexists ‘a'’ >>
+  rw []
+  >-(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] >>
+  case_tac >> fs []
+QED
+
+(* TODO: move *)
+Theorem len_FLAT_MAP_update:
+  ∀ 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))
+Proof
+  strip_tac >>
+  Induct_on ‘ls’
+  >-(rw [len_def] >> int_tac) >>
+  rw [] >>
+  fs [len_def, index_def, update_def] >>
+  Cases_on ‘i = 0’ >> fs [len_append]
+  >- int_tac >>
+  sg ‘0 < i’ >- int_tac >> fs [len_append] >>
+  first_x_assum (qspec_assume ‘i - 1’) >>
+  fs [] >>
+  (* TODO: automate *)
+  sg ‘0 ≤ i - 1 ∧ i - 1 < len ls’ >- int_tac >> fs [] >>
+  int_tac
+QED
+
+Theorem hash_map_insert_no_resize_fwd_back_spec:
+  !hm key value.
+    (* Using the base invariant, because the full invariant is preserved only
+       if we resize *)
+    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 ∧
+    (* We preserve the invariant *)
+    hash_map_t_base_inv hm1 ∧
+    (* We updated the binding for key *)
+    lookup_s hm1 key = SOME value /\
+    (* The other bindings are left unchanged *)
+    (!k. k <> key ==> lookup_s hm k = lookup_s hm1 k) ∧
+    (* Reasoning about the length *)
+    (case lookup_s hm key of
+     | NONE => len_s hm1 = len_s hm + 1
+     | SOME _ => len_s hm1 = len_s hm)
+Proof
+  rw [] >>
+  qspecl_assume [‘hm’, ‘key’, ‘value’] hash_map_insert_no_resize_fwd_back_spec_aux >> gvs [] >>
+  (* TODO: automate this *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >>
+  (* TODO: improve massage to not only look at variables *)
+  qspec_assume ‘hm.hash_map_num_entries’ usize_to_int_bounds >> fs [] >>
+  imp_res_tac hash_map_t_base_inv_len_slots >>
+  (* TODO: update usize_rem_spec? *)
+  qspecl_assume [‘usize_to_int key’, ‘len (vec_to_list hm.hash_map_slots)’] pos_mod_pos_ineqs >>
+  massage >> gvs [] >>
+  (* We need the invariant of hm1 to prove some of the postconditions *)
+  sg ‘hash_map_t_base_inv hm1’
+  >-(
+    fs [hash_map_t_base_inv_def, hash_map_t_al_v_def, hash_map_t_v_def] >>
+    rw []
+    >-(
+      sg_dep_rewrite_goal_tac len_FLAT_MAP_update
+      >-(fs [hash_mod_key_def, hash_key_fwd_def]) >>
+      fs [insert_in_slot_t_rel_def] >>
+      fs [hash_mod_key_def, hash_key_fwd_def] >>
+      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] >>
+      int_tac) >>
+    fs [slots_t_inv_def, slots_s_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 [insert_in_slot_t_rel_def]) >>
+    sg_dep_rewrite_goal_tac index_update_same
+    >-(fs [hash_mod_key_def, hash_key_fwd_def]) >>
+    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 [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 [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 [insert_in_slot_t_rel_def]) >>
+  (* Length *)
+  Cases_on ‘lookup_s hm key’ >>
+  gvs [insert_in_slot_t_rel_def, hash_map_t_inv_def, hash_map_t_base_inv_def, len_s_def]
+QED
+val _ = save_spec_thm "hash_map_insert_no_resize_fwd_back_spec"
 
 (*
 Theorem nth_mut_fwd_spec:
@@ -414,16 +1063,6 @@ QED
  * Invariant proof 2: functional version of the invariant
  *)
 
-val pairwise_rel_def = Define ‘
-  pairwise_rel p [] = T ∧
-  pairwise_rel p (x :: ls) = (for_all (p x) ls ∧ pairwise_rel p ls)
-’
-
-val distinct_keys_f_def = Define ‘
-  distinct_keys_f (ls : (u32 # 't) list) =
-    pairwise_rel (\x y. FST x ≠ FST y) ls
-’
-
 Theorem distinct_keys_f_insert_for_all:
   ∀k v k1 ls0 ls1.
   k1 ≠ k ⇒
@@ -541,3 +1180,4 @@ Proof
 QED
 
 val _ = export_theory ()
+*)