Make progress on the proofs of the hash map

6 files changed, 799 insertions, 6 deletions

diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index 157b5c00..2183ef77 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -64,6 +64,25 @@ Proof
   exfalso >> cooper_tac
 QED
 
+Definition drop_def:
+  drop (i : int) ([] : 'a list) = [] ∧
+  drop (i : int) (x :: ls) =
+    if i < 0 then x :: ls
+    else if i = 0 then x :: ls
+    else drop (i - 1) ls
+End
+
+Theorem drop_eq:
+  (∀ i. drop i [] = []) ∧
+  (∀ ls. drop 0 ls = ls) ∧
+  (∀ i x ls. drop i (x :: ls) =
+    if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then drop (i - 1) ls
+    else x :: ls)
+Proof
+  rw [drop_def] >> fs [] >> try_tac int_tac >>
+  Cases_on ‘ls’ >> fs [drop_def]
+QED
+
 Theorem len_eq_LENGTH:
   ∀ls. len ls = &(LENGTH ls)
 Proof
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
index 21545b6e..da7cdbb3 100644
--- a/backends/hol4/ilistTheory.sig
+++ b/backends/hol4/ilistTheory.sig
@@ -3,12 +3,14 @@ sig
   type thm = Thm.thm
   
   (*  Definitions  *)
+    val drop_def : thm
     val index_def : thm
     val len_def : thm
     val update_def : thm
   
   (*  Theorems  *)
     val append_len_eq : thm
+    val drop_eq : thm
     val index_eq : thm
     val index_eq_EL : thm
     val len_append : thm
@@ -20,6 +22,13 @@ sig
 (*
    [primitivesArith] Parent theory of "ilist"
    
+   [drop_def]  Definition
+      
+      ⊢ (∀i. drop i [] = []) ∧
+        ∀i x ls.
+          drop i (x::ls) =
+          if i < 0 then x::ls else if i = 0 then x::ls else drop (i − 1) ls
+   
    [index_def]  Definition
       
       ⊢ ∀i x ls.
@@ -46,6 +55,13 @@ sig
         ∀l1 l2 l1' l2'.
           len l2 = len l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')
    
+   [drop_eq]  Theorem
+      
+      ⊢ (∀i. drop i [] = []) ∧ (∀ls. drop 0 ls = ls) ∧
+        ∀i x ls.
+          drop i (x::ls) =
+          if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then drop (i − 1) ls else x::ls
+   
    [index_eq]  Theorem
       
       ⊢ (∀x ls. index 0 (x::ls) = x) ∧
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index 727fc8c2..decb1109 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -162,6 +162,12 @@ Proof
   metis_tac [INT_LE_ADDR]
 QED
 
+Theorem pos_div_pos_ge:
+  !(x y d : int). 0 <= x ==> 0 <= y ==> 0 < d ==> x >= y ==> x / d >= y / d
+Proof
+  metis_tac [pos_div_pos_le, ge_eq_le]
+QED
+
 Theorem pos_div_pos_le_init:
   !(x y : int). 0 <= x ==> 0 < y ==> x / y <= x
 Proof
@@ -223,4 +229,116 @@ Proof
   metis_tac [pos_mod_pos_is_pos, pos_mod_pos_lt]
 QED
 
+Theorem mul_pos_left_le:
+  ∀ (a x y : int). 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y
+Proof
+  rw [] >> Cases_on ‘a = 0’ >> fs [] >>
+  sg ‘0 < a’ >- cooper_tac >>
+  metis_tac [integerTheory.INT_LE_MONO]
+QED
+
+Theorem mul_pos_right_le:
+  ∀ (a x y : int). 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a
+Proof
+  rw [mul_pos_left_le, integerTheory.INT_MUL_COMM]
+QED
+
+Theorem mul_pos_left_lt:
+  ∀ (a x y : int). 0 < a ⇒ x < y ⇒ a * x < a * y
+Proof
+  metis_tac [integerTheory.INT_LT_MONO]
+QED
+
+Theorem mul_pos_right_lt:
+  ∀ (a x y : int). 0 < a ⇒ x < y ⇒ x * a < y * a
+Proof
+  metis_tac [mul_pos_left_lt, integerTheory.INT_MUL_COMM]
+QED
+
+Theorem pos_mul_left_pos_le:
+  ∀ a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x
+Proof
+  rw [] >>
+  Cases_on ‘a = 1’ >> fs [] >>
+  sg ‘0 ≤ (a - 1) * x’ >- (irule pos_mul_pos_is_pos >> int_tac) >>
+  sg ‘x ≤ x + (a - 1) * x’ >- fs [] >>
+  sg ‘a * x = 1 * x + (a - 1) * x’ >- fs [GSYM integerTheory.INT_RDISTRIB] >>
+  fs []
+QED
+
+Theorem pos_mul_right_pos_le:
+  ∀ a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a
+Proof
+  metis_tac [pos_mul_left_pos_le, integerTheory.INT_MUL_COMM]
+QED
+
+Theorem pos_mul_left_pos_lt:
+  ∀ a x. 1 < a ⇒ 0 < x ⇒ x < a * x
+Proof
+  rw [] >>
+  sg ‘a * x = 1 * x + (a - 1) * x’
+  >- (fs [GSYM integerTheory.INT_RDISTRIB]) >>
+  fs [] >>
+  sg ‘(a − 1) * x = 1 * x + (a - 2) * x’
+  >- (
+    fs [GSYM integerTheory.INT_RDISTRIB] >>
+    sg ‘1 + (a − 2) = a - 1’ >- int_tac >>
+    fs []
+    ) >>
+  fs [] >>
+  sg ‘0 ≤ (a − 2) * x’ >- (irule pos_mul_pos_is_pos >> int_tac) >>
+  int_tac
+QED
+
+Theorem pos_mul_right_pos_lt:
+  ∀ a x. 1 < a ⇒ 0 < x ⇒ x < x * a
+Proof
+  metis_tac [pos_mul_left_pos_lt, integerTheory.INT_MUL_COMM]
+QED
+
+Theorem pos_div_pos_mul_le:
+  ∀ x y. 0 ≤ x ⇒ 0 < y ⇒ (x / y) * y ≤ x
+Proof
+  rw [] >>
+  qspec_assume ‘y’ integerTheory.INT_DIVISION >>
+  sg ‘y ≠ 0 ∧ ~(y < 0)’ >- int_tac >> fs [] >>
+  first_x_assum (qspec_assume ‘x’) >>
+  fs [] >>
+  (* TODO: int_tac loops here *)
+  cooper_tac
+QED
+
+Theorem pos_mul_pos_div_pos_decompose:
+  ∀ x y z. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < z ⇒ x / z + y / z ≤ (x + y) / z
+Proof
+  rw [] >>
+  sg ‘z ≠ 0’ >- int_tac >>
+  sg ‘(x / z * z + x % z) + (y / z * z + y % z) = (x + y) / z * z + (x + y) % z’ >- metis_tac [integerTheory.INT_DIVISION] >>
+  sg ‘(x + y) % z = ((x % z) + (y % z)) % z’ >- metis_tac [integerTheory.INT_MOD_PLUS] >>
+  sg ‘0 ≤ (x % z) ∧ 0 ≤ (y % z)’ >- metis_tac [pos_mod_pos_is_pos] >>
+  sg ‘0 ≤ (x % z) + (y % z)’ >- int_tac >>
+  sg ‘((x % z) + (y % z)) % z ≤ (x % z) + (y % z)’ >- metis_tac [pos_mod_pos_le_init] >>
+  sg ‘x / z * z + y / z * z ≤ (x + y) / z * z’ >- int_tac >>
+  sg ‘x / z * z + y / z * z = (x / z + y / z) * z’ >- fs [integerTheory.INT_RDISTRIB] >> fs [] >>
+  sg ‘0 ≤ x / z’ >- (irule pos_div_pos_is_pos >> fs []) >>
+  sg ‘0 ≤ y / z’ >- (irule pos_div_pos_is_pos >> fs []) >>
+  sg ‘0 ≤ (x + y) / z’ >- (irule pos_div_pos_is_pos >> fs []) >>
+  sg ‘(x / z + y / z) * z / z ≤ (x + y) / z * z / z’
+  >- ( 
+    irule pos_div_pos_le >> fs [] >>
+    rw [] >> irule pos_mul_pos_is_pos >> fs []) >>
+  imp_res_tac integerTheory.INT_DIV_RMUL >>
+  metis_tac []
+QED
+
+Theorem pos_mul_2_div_pos_decompose:
+  ∀ x y. 0 ≤ x ⇒ 0 < y ⇒ x / y + x / y ≤ x * 2 / y
+Proof
+  rw [] >>
+  qspecl_assume [‘x’, ‘x’, ‘y’] pos_mul_pos_div_pos_decompose >> gvs [] >>
+  sg ‘x * 2 = (x * 1) + (x * 1)’
+  >- (pure_rewrite_tac [GSYM integerTheory.INT_LDISTRIB] >> fs []) >>
+  fs []  
+QED
+
 val _ = export_theory ()
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index 531797ac..84b9b67a 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -14,6 +14,8 @@ sig
     val int_of_num_inj : thm
     val le_eq_ge : thm
     val lt_eq_gt : thm
+    val mul_pos_left_le : thm
+    val mul_pos_right_le : thm
     val not_ge_eq_lt : thm
     val not_gt_eq_le : thm
     val not_le_eq_gt : thm
@@ -23,11 +25,14 @@ sig
     val pos_div_pos_is_pos : thm
     val pos_div_pos_le : thm
     val pos_div_pos_le_init : thm
+    val pos_div_pos_mul_le : thm
     val pos_mod_pos_ineqs : thm
     val pos_mod_pos_is_pos : thm
     val pos_mod_pos_le_init : thm
     val pos_mod_pos_lt : thm
+    val pos_mul_left_pos_le : thm
     val pos_mul_pos_is_pos : thm
+    val pos_mul_right_pos_le : thm
   
   val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -79,6 +84,14 @@ sig
       
       ⊢ ∀x y. x < y ⇔ y > x
    
+   [mul_pos_left_le]  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
+   
    [not_ge_eq_lt]  Theorem
       
       ⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
@@ -115,6 +128,10 @@ sig
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x
    
+   [pos_div_pos_mul_le]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y * y ≤ x
+   
    [pos_mod_pos_ineqs]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y ∧ x % y < y
@@ -131,10 +148,18 @@ sig
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y
    
+   [pos_mul_left_pos_le]  Theorem
+      
+      ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x
+   
    [pos_mul_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
    
+   [pos_mul_right_pos_le]  Theorem
+      
+      ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a
+   
    
 *)
 end
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index 0a89be4c..a90f1e32 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -272,7 +272,7 @@ fun get_spec_app (t : term) : term =
 fun get_key_normalize_thm (th : thm) : const_name * thm =
   let
     (* Transform the theroem a bit before storing it *)
-    val th = SPEC_ALL th;
+    val th = (SPEC_ALL o BETA_RULE o PURE_REWRITE_RULE [LET_DEF]) th;
     (* Retrieve the app ([f x0 ... xn]) *)
     val f = get_spec_app (concl th);
     (* Retrieve the function name *)
@@ -532,7 +532,7 @@ val progress : tactic =
     val thl =
       case Redblackmap.peek (get_spec_thms (), fname) of
         NONE => asms_thl
-      | SOME spec => spec :: asms_thl;
+      | SOME spec => asms_thl @ [spec];
     val _ =
       if null thl then
         raise (failwith "progress: could not find a suitable theorem to apply")
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index e96f7e34..38a1a09c 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -215,6 +215,21 @@ Definition lookup_s_def:
     slots_t_lookup (vec_to_list hm.hash_map_slots) k
 End
 
+Definition hash_map_same_params_def:
+  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)
+  )
+End
+
+Theorem hash_map_same_params_refl:
+  ∀ hm. hash_map_same_params hm hm
+Proof
+  fs [hash_map_same_params_def]
+QED
+val _ = export_rewrites ["hash_map_same_params_refl"]
+
 (*============================================================================*
  *============================================================================*
  *  Proofs
@@ -298,7 +313,9 @@ Theorem hash_map_new_with_capacity_fwd_spec:
   ∃ 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
+  ∀ 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)
 Proof
   rw [] >> fs [hash_map_new_with_capacity_fwd_def] >>
   progress >>
@@ -677,7 +694,8 @@ Theorem hash_map_insert_no_resize_fwd_back_spec_aux:
     (* 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)
+     | SOME _ => hm1.hash_map_num_entries = hm.hash_map_num_entries) ∧
+    hash_map_same_params hm hm1
 Proof
   rw [hash_map_insert_no_resize_fwd_back_def] >>
   fs [hash_key_fwd_def] >>
@@ -718,7 +736,7 @@ Proof
   qspecl_assume [‘hm.hash_map_slots’, ‘a’, ‘a'’] vec_update_eq >> gvs [] >>
   (* Prove the post-condition *)
   qexists ‘a'’ >>
-  rw []
+  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 [])
   >-(
@@ -766,7 +784,8 @@ Theorem hash_map_insert_no_resize_fwd_back_spec:
     (* 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)
+     | SOME _ => len_s hm1 = len_s hm) ∧
+    hash_map_same_params hm hm1
 Proof
   rw [] >>
   qspecl_assume [‘hm’, ‘key’, ‘value’] hash_map_insert_no_resize_fwd_back_spec_aux >> gvs [] >>
@@ -825,6 +844,602 @@ Proof
 QED
 val _ = save_spec_thm "hash_map_insert_no_resize_fwd_back_spec"
 
+(* TODO: move *)
+Theorem distinct_keys_MEM_not_eq:
+  ∀ ls k1 x1 k2 x2.
+  distinct_keys ((k1, x1) :: ls) ⇒
+  MEM (k2, x2) ls ⇒
+  k2 ≠ k1
+Proof
+  Induct_on ‘ls’ >> rw [] >>
+  fs [distinct_keys_def, pairwise_rel_def, EVERY_DEF] >>
+  metis_tac []
+QED
+
+Theorem distinct_keys_lookup_NONE:
+  ∀ ls k x.
+  distinct_keys ((k, x) :: ls) ⇒
+  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]
+QED
+
+Theorem hash_map_move_elements_from_list_fwd_back_spec:
+  ∀ 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
+Proof
+  pure_rewrite_tac [hash_map_move_elements_from_list_fwd_back_def] >>
+  Induct_on ‘ls’ >~ [‘ListNil’] >>
+  pure_once_rewrite_tac [hash_map_move_elements_from_list_loop_fwd_back_def] >> rw [] >>
+  (* 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]) >>
+  (* Recursive case *)
+  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) >>
+  (* Prove the postcondition *)
+  (* Drop the induction hypothesis *)
+  last_x_assum ignore_tac >>
+  gvs [] >>
+  sg ‘hash_map_same_params hm a'’ >- fs [hash_map_same_params_def] >> fs [] >>
+  (* TODO: we need an intro_tac *)
+  strip_tac >>
+  strip_tac >>
+  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 [] >>
+  (* For some reason, if we introduce an assumption with [sg], the rewriting
+     doesn't work (and I couldn't find any typing issue) *)
+  qpat_assum ‘(∀ k v . _) ⇒ _’ assume_tac >>
+  first_assum sg_premise_tac
+  >-(
+    rw [] >>
+    sg ‘k ≠ u’ >-(irule distinct_keys_MEM_not_eq >> metis_tac [list_t_v_def]) >>
+    last_x_assum (qspec_assume ‘k’) >>
+    gvs [] >>
+    first_x_assum (qspecl_assume [‘k’, ‘v’]) >>
+    gvs [list_t_v_def]) >>
+  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 [] >>  
+    sg ‘lookup k (list_t_v ls) = NONE’ >-(irule distinct_keys_lookup_NONE >> metis_tac []) >>
+    fs []) >>
+  (* The length *)
+  fs [len_def, list_t_v_def] >>
+  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 [] >>
+  last_x_assum (qspec_assume ‘i - 1’) >>
+  sg ‘0 ≤ i − 1 ∧ i − 1 < len slots’ >- int_tac >> fs []
+QED
+
+Theorem len_vec_FLAT_drop_update:
+  ∀ 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))))
+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] >>
+  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 ⇒
+    EVERY (\x. k ≠ FST x) ls ⇒
+      F  
+Proof
+  Induct_on ‘ls’ >> rw [EVERY_DEF] >> fs [] >>
+  Cases_on ‘h’ >> fs [] >>
+  metis_tac []
+QED
+
+Theorem MEM_distinct_keys_lookup:
+  ∀k v ls.
+    MEM (k, v) ls ⇒
+    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 [] >>
+  (* Absurd *)
+  exfalso >>
+  metis_tac [MEM_EVERY_not]
+QED
+
+Theorem lookup_distinct_keys_MEM:
+  ∀k v ls.
+    lookup k ls = SOME v ⇒
+    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 [] >>
+  Cases_on ‘q = k’ >> fs []
+QED
+
+Theorem key_MEM_j_lookup_i_is_NONE:
+  ∀ 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
+Proof
+  rw [] >>
+  fs [slot_t_inv_def, slot_s_inv_def, slot_s_inv_hash_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] >>
+  (* 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] >>
+    metis_tac [lookup_distinct_keys_MEM]
+  ) >>
+  qpat_x_assum ‘∀k. _’ imp_res_tac >>
+  fs [hash_mod_key_def, hash_key_fwd_def]
+QED  
+
+(* TODO: the names introduced by progress are random, which is confusing.
+   It also makes the proofs less stable.
+   Try to use the names given by the let-bindings. *)
+
+Theorem hash_map_move_elements_loop_fwd_back_spec_aux:
+  ∀ hm slots i n.
+    let slots_l = len (FLAT (MAP list_t_v (drop (usize_to_int i) (vec_to_list slots)))) in
+    (* Small trick for the induction *)
+    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
+      | SOME v => SOME v
+      | 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
+    ) ∧
+    hash_map_same_params hm hm1
+Proof
+  Induct_on ‘n’ >> rw [] >> pure_once_rewrite_tac [hash_map_move_elements_loop_fwd_back_def] >> fs [] >>
+  (* TODO: automate *)
+  qspec_assume ‘slots’ vec_len_spec >>
+  (* TODO: progress on usize_lt *)
+  fs [usize_lt_def, vec_len_def] >>
+  massage
+  >-(
+    case_tac >- int_tac >> fs [] >>
+    sg_dep_rewrite_goal_tac drop_more_than_length >-(int_tac) >> fs [len_def] >>
+    strip_tac >> Cases_on ‘lookup_s hm k’ >> fs [] >>
+    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    (* 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] >>
+    strip_tac >> Cases_on ‘lookup_s hm k’ >> fs [] >>
+    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    (* 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] >>
+    strip_tac >> Cases_on ‘lookup_s hm k’ >> fs [] >>
+    fs [hash_mod_key_def, hash_key_fwd_def] >>
+    (* Contradiction *)
+    rw [] >> int_tac) >>
+  progress >- (fs [vec_len_def] >> massage >> fs []) >>
+  progress >- (
+    fs [mem_replace_fwd_def, 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
+     in its postcondition *)
+  qpat_x_assum ‘_ ⇒ _’ sg_premise_tac
+  >-(
+    first_x_assum (qspec_assume ‘usize_to_int i’) >> gvs [vec_index_def] >>
+    rw [mem_replace_fwd_def]
+    >-(first_x_assum irule >> metis_tac []) >>
+    fs [slot_t_inv_def, slot_s_inv_def]) >>
+  gvs [mem_replace_fwd_def] >>
+  (* 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 >>
+  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] >>
+    int_tac)
+  >-(
+    fs [vec_to_list_vec_update] >>
+    sg_dep_rewrite_goal_tac index_update_same
+    >-(fs [] >> int_tac) >>
+    fs [] >>
+    last_x_assum (qspec_assume ‘j’) >> gvs [] >>
+    first_assum sg_premise_tac >- int_tac >>
+    fs [])
+  >-(
+    (* 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]) >>
+    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 [] >>
+    first_x_assum sg_premise_tac >- (int_tac) >> gvs [] >>
+    first_x_assum imp_res_tac) >>
+  (* The conclusion of the theorem (the post-condition) *)
+  conj_tac
+  >-(
+    (* 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] >>
+  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 []
+  >- (
+    sg ‘~ (usize_to_int i + 1 ≤ usize_to_int k % len (vec_to_list slots))’ >- int_tac >> fs [] >>
+    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] >>
+    (* 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 []) >>
+  (* 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 []
+  >- (
+    (* We have: usize_to_int i < usize_to_int k % len (vec_to_list slots)
+       The key is not in slot i, and is added (eventually) with the recursive call on
+       the remaining the slots.
+     *)
+    sg ‘usize_to_int i < usize_to_int k % len (vec_to_list slots)’ >- int_tac >> fs [] >>
+    sg ‘usize_to_int i + 1 ≤ usize_to_int k % len (vec_to_list slots)’ >- int_tac >> fs [] >>
+    (* We just need to use the fact that “lookup_s a' k = lookup_s hm k” *)
+    sg ‘lookup_s a' k = lookup_s hm k’
+    >- (
+      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] >>
+      Cases_on ‘slot_t_lookup k (vec_index slots i)’ >> fs [vec_index_def] >> exfalso >>
+      fs [slot_t_lookup_def] >>
+      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] >>
+    sg_dep_rewrite_goal_tac index_update_same >> fs []
+  ) >>
+  (* Here: usize_to_int i > usize_to_int k % ... *)
+  sg ‘~(usize_to_int i + 1 ≤ usize_to_int k % len (vec_to_list slots))’ >- int_tac >> fs [] >>
+  sg ‘lookup_s a' k = lookup_s hm k’
+  >- (
+    first_x_assum irule >>
+    (* We have to prove that the key is not in slot i *)
+    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] >>
+    (* Prove by contradiction *)
+    Cases_on ‘slot_t_lookup k (vec_index slots i)’ >> fs [vec_index_def] >> exfalso >>
+    fs [slot_t_lookup_def] >>
+    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 []
+QED
+
+Theorem hash_map_move_elements_fwd_back_spec:
+  ∀ 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
+      | SOME v => SOME v
+      | 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
+    ) ∧
+    hash_map_same_params hm hm1
+Proof
+  rw [hash_map_move_elements_fwd_back_def] >>
+  qspecl_assume [‘hm’, ‘slots’, ‘i’] hash_map_move_elements_loop_fwd_back_spec_aux >> gvs [] >>
+  pop_assum sg_premise_tac >- metis_tac [] >>
+  metis_tac []
+QED
+val _ = save_spec_thm "hash_map_move_elements_fwd_back_spec"
+
+(* We assume that usize = u32 - TODO: update the implementation of the hash map *)
+val usize_u32_bounds = new_axiom ("usize_u32_bounds", “usize_max = u32_max”)
+
+(* Predicate to characterize the state of the hash map just before we resize.
+
+   The "full" invariant is broken, as we call [try_resize]
+   only if the current number of entries is > the max load.
+
+   There are two situations:
+   - either we just reached the max load
+   - or we were already saturated and can't resize *)
+Definition hash_map_just_before_resize_pred_def:
+  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
+End
+
+Theorem hash_map_try_resize_fwd_back_spec:
+  ∀ hm.
+    (* The base invariant is satisfied *)
+    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)
+Proof
+  rw [hash_map_try_resize_fwd_back_def] >>
+  (* “_ <-- mk_usize (u32_to_int core_num_u32_max_c)” *)
+  assume_tac usize_u32_bounds >>
+  fs [core_num_u32_max_c_def, core_num_u32_max_body_def, get_return_value_def, u32_max_def] >>
+  massage >> fs [mk_usize_def, u32_max_def] >>
+  (* / 2 *)
+  progress >>
+  Cases_on ‘hm.hash_map_max_load_factor’ >> fs [] >>
+  progress >- (fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >> gvs [] >>
+  (* usize_le *)
+  fs [usize_le_def, vec_len_def] >>
+  (* TODO: automate *)
+  qspec_assume ‘hm.hash_map_slots’ vec_len_spec >> fs [vec_len_def] >>
+  massage >>
+  case_tac >>
+  (* Eliminate the case where we don't resize the hash_map *)
+  try_tac (
+    gvs [hash_map_t_inv_def, hash_map_t_base_inv_def, hash_map_just_before_resize_pred_def,
+         len_s_def, hash_map_t_al_v_def, hash_map_t_v_def, lookup_s_def] >>
+    (* Contradiction *)
+    exfalso >>
+    sg ‘len (vec_to_list hm.hash_map_slots) > 2147483647 / usize_to_int q’ >- int_tac >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q / 2 = len (vec_to_list hm.hash_map_slots) * usize_to_int q’
+    >- (
+      sg ‘len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q = (len (vec_to_list hm.hash_map_slots) * usize_to_int q) * 2’
+      >- (metis_tac [integerTheory.INT_MUL_COMM, integerTheory.INT_MUL_ASSOC]) >>
+      fs [] >>
+      irule integerTheory.INT_DIV_RMUL >> fs []) >>
+    gvs [] >>
+    sg ‘(len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q) / 2 ≤ usize_max / 2’
+    >-(irule pos_div_pos_le >> int_tac) >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q / 2 = len (vec_to_list hm.hash_map_slots) * usize_to_int q’
+    >- (
+      sg ‘len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q = (len (vec_to_list hm.hash_map_slots) * usize_to_int q) * 2’
+      >- (metis_tac [integerTheory.INT_MUL_COMM, integerTheory.INT_MUL_ASSOC]) >>
+      fs [] >>
+      irule integerTheory.INT_DIV_RMUL >> fs []) >>
+    gvs [] >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * usize_to_int q / usize_to_int q ≤ usize_max / 2 / usize_to_int q’
+    >-(irule pos_div_pos_le >> int_tac) >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * usize_to_int q / usize_to_int q = len (vec_to_list hm.hash_map_slots)’
+    >- (irule integerTheory.INT_DIV_RMUL >> int_tac) >>
+    gvs [] >>
+    fail_tac "") >>
+  (* Resize the hashmap *)
+  sg ‘0 < usize_to_int q’ >- fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >>
+  sg ‘len (vec_to_list hm.hash_map_slots) * 2 ≤ usize_max’
+  >-(
+    sg ‘len (vec_to_list hm.hash_map_slots) ≤ 2147483647’
+    >-(
+      qspecl_assume [‘2147483647’, ‘usize_to_int q’] pos_div_pos_le_init >> fs [] >>
+      gvs [] >> int_tac
+    ) >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * 2 ≤ 2147483647 * 2’
+    >- (irule mul_pos_right_le >> fs []) >>
+    fs [] >> int_tac
+  ) >>
+  progress >> gvs [] >>
+  sg ‘0 < len (vec_to_list hm.hash_map_slots)’
+  >- (fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> int_tac) >>
+  (* TODO: automate *)
+  sg ‘0 < len (vec_to_list hm.hash_map_slots) * 2’
+  >- (irule int_arithTheory.positive_product_implication >> fs []) >>
+  sg ‘len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q ≥ usize_to_int r’
+  >- (
+    sg ‘len (vec_to_list hm.hash_map_slots) * usize_to_int q >= usize_to_int r’
+    >- (fs [hash_map_t_inv_def, hash_map_t_base_inv_def]) >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * usize_to_int q ≤
+        2 * (len (vec_to_list hm.hash_map_slots) * usize_to_int q)’
+    >- (irule  pos_mul_left_pos_le >> fs []) >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q =
+        2 * (len (vec_to_list hm.hash_map_slots) * usize_to_int q)’
+    >- (metis_tac [integerTheory.INT_MUL_COMM, integerTheory.INT_MUL_ASSOC]) >>
+    int_tac
+   ) >>
+  sg ‘len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q ≤ usize_max’
+  >- (
+    sg ‘len (vec_to_list hm.hash_map_slots) * usize_to_int q ≤ (2147483647 / usize_to_int q) * usize_to_int q’
+    >- (irule mul_pos_right_le >> fs []) >>
+    sg ‘2147483647 / usize_to_int q * usize_to_int q ≤ 2147483647’
+    >- (irule pos_div_pos_mul_le >> fs []) >>
+    int_tac
+    ) >>
+  (* TODO: don't make progress transform conjunctions to implications *)
+  progress >> try_tac (fs [hash_map_t_inv_def, hash_map_t_base_inv_def] >> fail_tac "") >>
+  (* TODO: annoying that the rewriting tactics make the case disjunction over the “∨” *)
+  sg ‘hash_map_t_base_inv hm’ >- fs [hash_map_t_inv_def] >>
+  progress
+  >-(fs [hash_map_t_inv_def])
+  >-(fs [drop_eq, hash_map_t_base_inv_def, hash_map_t_v_def, hash_map_t_al_v_def] >>
+     (* 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]) >>
+  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 [] >>
+  (* TODO: lookup post condition, parameters for the new_with_capacity *)
+  conj_tac
+  >-(
+    (* Length *)
+    gvs [hash_map_same_params_def, hash_map_just_before_resize_pred_def] >> try_tac int_tac >>
+    (* We are in the case where we managed to resize the hash map *)
+    disj1_tac >>
+    sg ‘0 < len (vec_to_list hm.hash_map_slots) * usize_to_int q / usize_to_int r’
+    >- (
+      sg ‘len (vec_to_list hm.hash_map_slots) * usize_to_int q / usize_to_int r ≥ usize_to_int r / usize_to_int r’
+      >- (irule pos_div_pos_ge >> int_tac) >>
+      sg ‘usize_to_int r / usize_to_int r = 1’
+      >- (irule integerTheory.INT_DIV_ID >> int_tac) >>
+      int_tac
+      ) >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * 2 * usize_to_int q = (len (vec_to_list hm.hash_map_slots) * usize_to_int q) * 2’
+    >- metis_tac [integerTheory.INT_MUL_COMM, integerTheory.INT_MUL_ASSOC] >>
+    fs [] >>
+    sg ‘len (vec_to_list hm.hash_map_slots) * usize_to_int q / usize_to_int r +
+        len (vec_to_list hm.hash_map_slots) * usize_to_int q / usize_to_int r ≤
+        (len (vec_to_list hm.hash_map_slots) * usize_to_int q) * 2 / usize_to_int r’
+    >- (irule pos_mul_2_div_pos_decompose >> int_tac) >>
+    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] >>
+  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 [] >>
+  sg ‘usize_to_int k % len (vec_to_list hm.hash_map_slots) < len (vec_to_list hm.hash_map_slots)’
+  >- (irule pos_mod_pos_lt >> fs [] >> int_tac) >> fs []
+QED
+val _ = save_spec_thm "hash_map_try_resize_fwd_back_spec"
+
 (*
 Theorem nth_mut_fwd_spec:
   !(ls : 't list_t) (i : u32).