Make good progress on the proofs of the hashmap in HOL4

7 files changed, 841 insertions, 64 deletions

diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index 679ed2cd..727fc8c2 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -209,4 +209,18 @@ Proof
   cooper_tac
 QED
 
+Theorem pos_mod_pos_lt:
+  ∀ x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y
+Proof
+  rw [] >>
+  qspecl_assume [‘x’, ‘y’] integerTheory.INT_MOD_BOUNDS >>
+  sg ‘y ≠ 0 ∧ ~(y < 0)’ >- int_tac >> fs []
+QED
+
+Theorem pos_mod_pos_ineqs:
+  ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y ∧ x % y < y
+Proof
+  metis_tac [pos_mod_pos_is_pos, pos_mod_pos_lt]
+QED
+
 val _ = export_theory ()
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index f7ecccab..531797ac 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -23,8 +23,10 @@ sig
     val pos_div_pos_is_pos : thm
     val pos_div_pos_le : thm
     val pos_div_pos_le_init : 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_pos_is_pos : thm
   
   val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
@@ -113,6 +115,10 @@ sig
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x
    
+   [pos_mod_pos_ineqs]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y ∧ x % y < y
+   
    [pos_mod_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y
@@ -121,6 +127,10 @@ sig
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x
    
+   [pos_mod_pos_lt]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y
+   
    [pos_mul_pos_is_pos]  Theorem
       
       ⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index d19903b1..f256d330 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -293,15 +293,28 @@ fun inst_match_concl_in_terms (keep : thm -> bool) (ths : thm Net.net) (tml : te
     (* Then, match more precisely for every theorem found *)
     fun try_match (bvars : string Redblackset.set) t th =
       let
-        val _ = print_dbg ("inst_match_concl_in_terms: " ^ term_to_string t ^ "\n")
+        val _ = print_dbg ("inst_match_concl_in_terms:\n- thm: " ^ thm_to_string th ^
+                           "\n- term: " ^ term_to_string t ^ "\n")
         val inst_th = inst_match_concl bvars th t
         val c = concl inst_th
         val _ = print_dbg ("inst_match_concl_in_terms: matched with success\n")
       in
         (* Check that we mustn't ignore the theorem *)
-        if keep inst_th then (lhs (concl inst_th), inst_th)
+        if keep inst_th then
+          let val _ = print_dbg "inst_match_concl_in_terms: keeping theorem\n\n" in
+          (* There are several possibilities:
+             - initially, we only kept the lhs of the conclusion (with premises)
+               of the theorem
+             - now, we keep the whole theorem
+             The reason is that it happens that we can prove the premise of some
+             instantiation but not on another instantiation, even though the
+             conclusion is the same: in that case we want to keep both.
+             For instance:
+             
+           *)
+          (concl (DISCH_ALL inst_th), inst_th) end
         else
-          let val _ = print_dbg ("inst_match_concl_in_terms: matched failed\n") in
+          let val _ = print_dbg ("inst_match_concl_in_terms: ignore theorem\n\n") in
           failwith "inst_match_concl_in_terms: ignore theorem" end
       end
     (* Compose *)
@@ -311,8 +324,19 @@ fun inst_match_concl_in_terms (keep : thm -> bool) (ths : thm Net.net) (tml : te
       in
         mapfilter (try_match bvars t) matched_thms
       end
+    (* *)
+    val thms = inst_match_in_terms try_match_on_thms tml
+    (* Debug *)
+    val _ =
+      if !debug then
+        let
+          val thms_s = String.concatWith "\n" (map thm_to_string thms)
+        in
+          print ("inst_match_concl_in_terms: instantiated theorems:\n" ^ thms_s ^ "\n\n")
+        end
+      else ()
   in
-    inst_match_in_terms try_match_on_thms tml
+    thms
   end
 
 (*
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index 5339dec9..0a89be4c 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -6,6 +6,23 @@ open primitivesBaseTacLib primitivesTheory
 
 val primitives_theory_name = "primitives"
 
+val debug = ref false
+
+fun print_dbg msg = if !debug then print msg else ()
+
+fun print_dbg_goal msg (asms, g) =
+  if !debug then
+    let
+      val asms_s = map term_to_string asms
+      val g_s = term_to_string g
+      val s = "[" ^ (String.concatWith ", " asms_s) ^ "]" ^ " ⊢ " ^ g_s
+      val _ = print (msg ^ "goal: " ^ s ^ "\n")
+    in
+      ALL_TAC (asms, g)
+    end
+  else
+    ALL_TAC (asms, g)
+
 (* Small utility: compute the set of assumptions in the context.
 
    We isolate this code in a utility in order to be able to improve it:
@@ -144,7 +161,10 @@ val integer_conversion_lemmas_list = [
   u16_to_int_int_to_u16,
   u32_to_int_int_to_u32,
   u64_to_int_int_to_u64,
-  u128_to_int_int_to_u128
+  u128_to_int_int_to_u128,
+  (* Additional conservative lemmas for isize/usize *)
+  isize_to_int_int_to_isize_i16_bounds,
+  usize_to_int_int_to_usize_u16_bounds
 ]
 
 (* Using a net for efficiency *)
@@ -162,7 +182,9 @@ val integer_conversion_lemmas_net = net_of_rewrite_thms integer_conversion_lemma
  *)
 val rewrite_with_dep_int_lemmas : tactic =
   let
-    val prove_premise = full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> int_tac
+    val prove_premise =
+      (print_dbg_goal "rewrite_with_dep_int_lemmas: prove_premise:\n" >>
+       full_simp_tac simpLib.empty_ss integer_bounds_defs_list >> int_tac)
     (* Rewriting based on matching the conclusion. *)
     val then_tac1 = (fn th => full_simp_tac simpLib.empty_ss [th])
     val rewr_tac1 = apply_dep_rewrites_match_concl_with_all_tac prove_premise then_tac1
@@ -515,9 +537,18 @@ val progress : tactic =
       if null thl then
         raise (failwith "progress: could not find a suitable theorem to apply")
       else ();
+    (* Small helper to remove the equality introduced by the applied spec
+       (of the shape “f x = Return y” for instance), if there is *)
+    val remove_eq = try_tac (qpat_x_assum ‘^fgoal = _’ ignore_tac)
+    
   in
-    (* Attempt to use the theorems one by one *)
-    map_first_tac progress_with thl (asms, g)
+    (* We do 3 operations:
+       - attempt to use the theorems one by one
+       - remove (if there is) the equality introduced by the applied spec
+         (of the shape “f x = Return y” for instance)
+       - refold the monadic let-bindings
+     *)
+    (map_first_tac progress_with thl >> remove_eq >> fs [GSYM bind_def]) (asms, g)
   end
 
 (* Small utility: check that a term evaluates to “Return” (used by the unit tests) *)
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 7920454b..4378f9c3 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -24,6 +24,13 @@ End
 
 val bind_name = fst (dest_const “bind”)
 
+Theorem bind_return_fail_div_eq:
+  (bind (Return x) f = f x) ∧ (bind (Fail e) f = Fail e) ∧ (bind Diverge f = Diverge)
+Proof
+  fs [bind_def]
+QED
+val _ = BasicProvers.export_rewrites ["bind_return_fail_div_eq"]
+
 Definition return_def:
   (return : 'a -> 'a M) x =
     Return x
@@ -273,6 +280,23 @@ val all_int_to_scalar_to_int_lemmas = [
   u128_to_int_int_to_u128
 ]
 
+(* Additional conversion lemmas  for isize/usize *)
+Theorem isize_to_int_int_to_isize_i16_bounds:
+  !n. i16_min <= n /\ n <= i16_max ==> isize_to_int (int_to_isize n) = n
+Proof
+  rw [] >> irule isize_to_int_int_to_isize >>
+  assume_tac isize_bounds >>
+  int_tac
+QED
+
+Theorem usize_to_int_int_to_usize_u16_bounds:
+  !n. 0 <= n /\ n <= u16_max ==> usize_to_int (int_to_usize n) = n
+Proof
+  rw [] >> irule usize_to_int_int_to_usize >>
+  assume_tac usize_bounds >>
+  int_tac
+QED
+
 val prove_int_to_scalar_to_int_unfold_tac =
   assume_tac isize_bounds >> (* Only useful for isize of course *)
   assume_tac usize_bounds >> (* Only useful for usize of course *)
@@ -677,7 +701,7 @@ val all_div_defs = [
    In HOL4, it has the sign of the divisor.
  *)
 val int_rem_def = Define ‘int_rem (x : int) (y : int) : int =
-  if (x >= 0 /\ y >= 0) \/ (x < 0 /\ y < 0) then x % y else -(x % y)’
+  if (0 ≤ x /\ 0 ≤ y) \/ (x < 0 /\ y < 0) then x % y else -(x % y)’
 
 (* Checking consistency with Rust *)
 val _ = prove(“int_rem 1 2 = 1”, EVAL_TAC)
@@ -685,6 +709,12 @@ val _ = prove(“int_rem (-1) 2 = -1”, EVAL_TAC)
 val _ = prove(“int_rem 1 (-2) = 1”, EVAL_TAC)
 val _ = prove(“int_rem (-1) (-2) = -1”, EVAL_TAC)
 
+Theorem pos_rem_pos_ineqs:
+  ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ int_rem x y ∧ int_rem x y < y
+Proof
+  rw [int_rem_def] >> metis_tac [pos_mod_pos_ineqs]
+QED
+
 val isize_rem_def = Define ‘isize_rem x y =
   if isize_to_int y = 0 then Fail Failure else mk_isize (int_rem (isize_to_int x) (isize_to_int y))’
 val i8_rem_def = Define ‘i8_rem x y =
@@ -1781,13 +1811,14 @@ End
 
 Theorem vec_update_eq:
  ∀ v i x.
-   usize_to_int i < usize_to_int (vec_len v) ⇒
    let nv = vec_update v i x in
-   vec_len v = vec_len nv ∧
+   len (vec_to_list nv) = len (vec_to_list v) ∧
+   len (update (vec_to_list v) (usize_to_int i) x) = len (vec_to_list v) ∧
+   (usize_to_int i < len (vec_to_list v) ⇒
       vec_index nv i = x ∧
       (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒
             usize_to_int j ≠ usize_to_int i ⇒
-            vec_index nv j = vec_index v j)
+            vec_index nv j = vec_index v j))
 Proof
   rpt strip_tac >> fs [vec_update_def] >>
   qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_axiom >>
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index e4051212..7e03987b 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -213,6 +213,7 @@ sig
     val vec_update_def : thm
   
   (*  Theorems  *)
+    val bind_return_fail_div_eq : thm
     val datatype_error : thm
     val datatype_result : thm
     val error2num_11 : thm
@@ -275,6 +276,7 @@ sig
     val isize_neg_eq : thm
     val isize_rem_eq : thm
     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 mk_isize_unfold : thm
     val mk_usize_unfold : thm
@@ -283,6 +285,7 @@ sig
     val num2error_ONTO : thm
     val num2error_error2num : thm
     val num2error_thm : thm
+    val pos_rem_pos_ineqs : thm
     val result_11 : thm
     val result_Axiom : thm
     val result_case_cong : thm
@@ -333,6 +336,7 @@ sig
     val usize_mul_eq : thm
     val usize_rem_eq : thm
     val usize_sub_eq : thm
+    val usize_to_int_int_to_usize_u16_bounds : thm
     val usize_to_int_int_to_usize_unfold : thm
     val vec_index_back_spec : thm
     val vec_index_fwd_spec : thm
@@ -855,7 +859,7 @@ sig
       
       ⊢ ∀x y.
           int_rem x y =
-          if x ≥ 0 ∧ y ≥ 0 ∨ x < 0 ∧ y < 0 then x % y else -(x % y)
+          if 0 ≤ x ∧ 0 ≤ y ∨ x < 0 ∧ y < 0 then x % y else -(x % y)
    
    [is_diverge_def]  Definition
       
@@ -1366,6 +1370,11 @@ sig
           vec_update v i x =
           mk_vec (update (vec_to_list v) (usize_to_int i) x)
    
+   [bind_return_fail_div_eq]  Theorem
+      
+      ⊢ monad_bind (Return x) f = f x ∧ monad_bind (Fail e) f = Fail e ∧
+        monad_bind Diverge f = Diverge
+   
    [datatype_error]  Theorem
       
       ⊢ DATATYPE (error Failure)
@@ -1884,6 +1893,12 @@ sig
           ∃z. isize_sub x y = Return z ∧
               isize_to_int z = isize_to_int x − isize_to_int y
    
+   [isize_to_int_int_to_isize_i16_bounds]  Theorem
+      
+      [oracles: DISK_THM] [axioms: isize_to_int_int_to_isize, isize_bounds]
+      []
+      ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ isize_to_int (int_to_isize n) = n
+   
    [isize_to_int_int_to_isize_unfold]  Theorem
       
       [oracles: DISK_THM]
@@ -1932,6 +1947,10 @@ sig
       
       ⊢ num2error 0 = Failure
    
+   [pos_rem_pos_ineqs]  Theorem
+      
+      ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ int_rem x y ∧ int_rem x y < y
+   
    [result_11]  Theorem
       
       ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧
@@ -2348,6 +2367,11 @@ sig
           ∃z. usize_sub x y = Return z ∧
               usize_to_int z = usize_to_int x − usize_to_int y
    
+   [usize_to_int_int_to_usize_u16_bounds]  Theorem
+      
+      [oracles: DISK_THM] [axioms: usize_to_int_int_to_usize, usize_bounds]
+      [] ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ usize_to_int (int_to_usize n) = n
+   
    [usize_to_int_int_to_usize_unfold]  Theorem
       
       [oracles: DISK_THM]
@@ -2436,14 +2460,17 @@ sig
       [axioms: vec_to_list_num_bounds, usize_bounds,
        usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_axiom] []
       ⊢ ∀v i x.
-          usize_to_int i < usize_to_int (vec_len v) ⇒
           (let
              nv = vec_update v i x
            in
-             vec_len v = vec_len nv ∧ vec_index nv i = x ∧
-             ∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒
-                 usize_to_int j ≠ usize_to_int i ⇒
-                 vec_index nv j = vec_index v j)
+             len (vec_to_list nv) = len (vec_to_list v) ∧
+             len (update (vec_to_list v) (usize_to_int i) x) =
+             len (vec_to_list v) ∧
+             (usize_to_int i < len (vec_to_list v) ⇒
+              vec_index nv i = x ∧
+              ∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒
+                  usize_to_int j ≠ usize_to_int i ⇒
+                  vec_index nv j = vec_index v j))
    
    
 *)
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 ()
+*)