Finish the proofs of the hashmap

1 files changed, 902 insertions, 0 deletions

diff --git a/tests/hol4/hashmap/hashmap_PropertiesTheory.sig b/tests/hol4/hashmap/hashmap_PropertiesTheory.sig
new file mode 100644
index 00000000..39b6f048
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_PropertiesTheory.sig
@@ -0,0 +1,902 @@
+signature hashmap_PropertiesTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Axioms  *)
+    val usize_u32_bounds : thm
+  
+  (*  Definitions  *)
+    val distinct_keys_def : thm
+    val hash_map_just_before_resize_pred_def : thm
+    val hash_map_same_params_def : thm
+    val hash_map_t_al_v_def : thm
+    val hash_map_t_base_inv_def : thm
+    val hash_map_t_inv_def : thm
+    val hash_map_t_v_def : thm
+    val hash_mod_key_def : thm
+    val insert_in_slot_t_rel_def : thm
+    val len_s_def : thm
+    val list_t_v_def : thm
+    val lookup_s_def : thm
+    val pairwise_rel_def : thm
+    val slot_s_inv_def : thm
+    val slot_s_inv_hash_def : thm
+    val slot_t_inv_def : thm
+    val slot_t_lookup_def : thm
+    val slot_t_remove_def : thm
+    val slots_s_inv_def : thm
+    val slots_t_inv_def : thm
+    val slots_t_lookup_def : thm
+  
+  (*  Theorems  *)
+    val EVERY_quant_equiv : thm
+    val FLAT_ListNil_is_nil : thm
+    val MEM_EVERY_not : thm
+    val MEM_distinct_keys_lookup : thm
+    val distinct_keys_MEM_not_eq : thm
+    val distinct_keys_lookup_NONE : thm
+    val every_distinct_remove_every_distinct : thm
+    val hash_map_allocate_slots_fwd_spec : thm
+    val hash_map_allocate_slots_loop_fwd_spec : thm
+    val hash_map_clear_fwd_back_spec : thm
+    val hash_map_clear_loop_fwd_back_spec : thm
+    val hash_map_clear_loop_fwd_back_spec_aux : thm
+    val hash_map_cond_incr_thm : thm
+    val hash_map_contains_key_fwd_spec : thm
+    val hash_map_contains_key_in_list_fwd_spec : thm
+    val hash_map_get_fwd_spec : thm
+    val hash_map_get_in_list_fwd_spec : thm
+    val hash_map_get_mut_back_spec : thm
+    val hash_map_get_mut_fwd_spec : thm
+    val hash_map_get_mut_in_list_back_spec : thm
+    val hash_map_get_mut_in_list_fwd_spec : thm
+    val hash_map_insert_fwd_back_spec : thm
+    val hash_map_insert_in_list_fwd_spec : thm
+    val hash_map_insert_in_list_loop_back_EVERY_distinct_keys : thm
+    val hash_map_insert_in_list_loop_back_distinct_keys : thm
+    val hash_map_insert_in_list_loop_back_spec : thm
+    val hash_map_insert_in_list_loop_back_spec_aux : thm
+    val hash_map_insert_in_list_loop_fwd_spec : thm
+    val hash_map_insert_no_resize_fwd_back_branches_eq : thm
+    val hash_map_insert_no_resize_fwd_back_spec : thm
+    val hash_map_insert_no_resize_fwd_back_spec_aux : thm
+    val hash_map_len_spec : thm
+    val hash_map_move_elements_from_list_fwd_back_spec : thm
+    val hash_map_move_elements_fwd_back_spec : thm
+    val hash_map_move_elements_loop_fwd_back_spec_aux : thm
+    val hash_map_new_fwd_spec : thm
+    val hash_map_new_with_capacity_fwd_spec : thm
+    val hash_map_remove_back_branch_eq : thm
+    val hash_map_remove_back_spec : thm
+    val hash_map_remove_from_list_back_spec : thm
+    val hash_map_remove_from_list_fwd_spec : thm
+    val hash_map_remove_fwd_spec : thm
+    val hash_map_same_params_refl : thm
+    val hash_map_t_base_inv_len_slots : thm
+    val hash_map_try_resize_fwd_back_spec : thm
+    val key_MEM_j_lookup_i_is_NONE : thm
+    val len_FLAT_MAP_update : thm
+    val len_index_FLAT_MAP_list_t_v : thm
+    val len_vec_FLAT_drop_update : thm
+    val lookup_SOME_not_empty : thm
+    val lookup_cond_decr_entries_eq : thm
+    val lookup_def : thm
+    val lookup_distinct_keys_MEM : thm
+    val lookup_ind : thm
+    val lookup_s_SOME_not_empty : thm
+    val pairwise_rel_quant_equiv : thm
+    val remove_def : thm
+    val remove_ind : thm
+    val slot_t_lookup_SOME_not_empty : thm
+  
+  val hashmap_Properties_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [hashmap_Funs] Parent theory of "hashmap_Properties"
+   
+   [usize_u32_bounds]  Axiom
+      
+      [oracles: ] [axioms: usize_u32_bounds] [] ⊢ usize_max = u32_max
+   
+   [distinct_keys_def]  Definition
+      
+      ⊢ ∀ls. distinct_keys ls ⇔ pairwise_rel (λx y. FST x ≠ FST y) ls
+   
+   [hash_map_just_before_resize_pred_def]  Definition
+      
+      ⊢ ∀hm.
+          hash_map_just_before_resize_pred hm ⇔
+          (let
+             (dividend,divisor) = hm.hash_map_max_load_factor
+           in
+             usize_to_int hm.hash_map_num_entries =
+             usize_to_int hm.hash_map_max_load + 1 ∧
+             len (vec_to_list hm.hash_map_slots) * 2 *
+             usize_to_int dividend ≤ usize_max ∨
+             len (vec_to_list hm.hash_map_slots) * 2 *
+             usize_to_int dividend > usize_max)
+   
+   [hash_map_same_params_def]  Definition
+      
+      ⊢ ∀hm hm1.
+          hash_map_same_params hm hm1 ⇔
+          hm1.hash_map_max_load_factor = hm.hash_map_max_load_factor ∧
+          hm1.hash_map_max_load = hm.hash_map_max_load ∧
+          len (vec_to_list hm1.hash_map_slots) =
+          len (vec_to_list hm.hash_map_slots)
+   
+   [hash_map_t_al_v_def]  Definition
+      
+      ⊢ ∀hm. hash_map_t_al_v hm = FLAT (hash_map_t_v hm)
+   
+   [hash_map_t_base_inv_def]  Definition
+      
+      ⊢ ∀hm.
+          hash_map_t_base_inv hm ⇔
+          (let
+             al = hash_map_t_al_v hm
+           in
+             usize_to_int hm.hash_map_num_entries = len al ∧
+             slots_t_inv hm.hash_map_slots ∧
+             len (vec_to_list hm.hash_map_slots) > 0 ∧
+             (let
+                capacity = len (vec_to_list hm.hash_map_slots);
+                (dividend,divisor) = hm.hash_map_max_load_factor;
+                dividend = usize_to_int dividend;
+                divisor = usize_to_int divisor
+              in
+                0 < dividend ∧ dividend < divisor ∧
+                capacity * dividend ≥ divisor ∧
+                usize_to_int hm.hash_map_max_load =
+                capacity * dividend / divisor))
+   
+   [hash_map_t_inv_def]  Definition
+      
+      ⊢ ∀hm.
+          hash_map_t_inv hm ⇔
+          hash_map_t_base_inv hm ∧
+          (let
+             (dividend,divisor) = hm.hash_map_max_load_factor
+           in
+             usize_to_int hm.hash_map_num_entries ≤
+             usize_to_int hm.hash_map_max_load ∨
+             len (vec_to_list hm.hash_map_slots) * 2 *
+             usize_to_int dividend > usize_max)
+   
+   [hash_map_t_v_def]  Definition
+      
+      ⊢ ∀hm. hash_map_t_v hm = MAP list_t_v (vec_to_list hm.hash_map_slots)
+   
+   [hash_mod_key_def]  Definition
+      
+      ⊢ ∀k l.
+          hash_mod_key k l =
+          case hash_key_fwd k of
+            Return k => usize_to_int k % l
+          | Fail v3 => ARB
+          | Diverge => ARB
+   
+   [insert_in_slot_t_rel_def]  Definition
+      
+      ⊢ ∀l key value slot slot1.
+          insert_in_slot_t_rel l key value slot slot1 ⇔
+          slot_t_inv l (hash_mod_key key l) slot1 ∧
+          slot_t_lookup key slot1 = SOME value ∧
+          (∀k. k ≠ key ⇒ slot_t_lookup k slot = slot_t_lookup k slot1) ∧
+          case slot_t_lookup key slot of
+            NONE => len (list_t_v slot1) = len (list_t_v slot) + 1
+          | SOME v => len (list_t_v slot1) = len (list_t_v slot)
+   
+   [len_s_def]  Definition
+      
+      ⊢ ∀hm. len_s hm = len (hash_map_t_al_v hm)
+   
+   [list_t_v_def]  Definition
+      
+      ⊢ list_t_v ListNil = [] ∧
+        ∀k v tl. list_t_v (ListCons k v tl) = (k,v)::list_t_v tl
+   
+   [lookup_s_def]  Definition
+      
+      ⊢ ∀hm k.
+          lookup_s hm k = slots_t_lookup (vec_to_list hm.hash_map_slots) k
+   
+   [pairwise_rel_def]  Definition
+      
+      ⊢ (∀p. pairwise_rel p [] ⇔ T) ∧
+        ∀p x ls.
+          pairwise_rel p (x::ls) ⇔ EVERY (p x) ls ∧ pairwise_rel p ls
+   
+   [slot_s_inv_def]  Definition
+      
+      ⊢ ∀l i ls.
+          slot_s_inv l i ls ⇔ distinct_keys ls ∧ slot_s_inv_hash l i ls
+   
+   [slot_s_inv_hash_def]  Definition
+      
+      ⊢ ∀l i ls.
+          slot_s_inv_hash l i ls ⇔
+          ∀k v. MEM (k,v) ls ⇒ hash_mod_key k l = i
+   
+   [slot_t_inv_def]  Definition
+      
+      ⊢ ∀l i s. slot_t_inv l i s ⇔ slot_s_inv l i (list_t_v s)
+   
+   [slot_t_lookup_def]  Definition
+      
+      ⊢ ∀key ls. slot_t_lookup key ls = lookup key (list_t_v ls)
+   
+   [slot_t_remove_def]  Definition
+      
+      ⊢ ∀key ls. slot_t_remove key ls = remove key (list_t_v ls)
+   
+   [slots_s_inv_def]  Definition
+      
+      ⊢ ∀s. slots_s_inv s ⇔
+            ∀i. 0 ≤ i ⇒ i < len s ⇒ slot_t_inv (len s) i (index i s)
+   
+   [slots_t_inv_def]  Definition
+      
+      ⊢ ∀s. slots_t_inv s ⇔ slots_s_inv (vec_to_list s)
+   
+   [slots_t_lookup_def]  Definition
+      
+      ⊢ ∀s k.
+          slots_t_lookup s k =
+          (let
+             i = hash_mod_key k (len s);
+             slot = index i s
+           in
+             slot_t_lookup k slot)
+   
+   [EVERY_quant_equiv]  Theorem
+      
+      ⊢ ∀p ls. EVERY p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
+   
+   [FLAT_ListNil_is_nil]  Theorem
+      
+      ⊢ EVERY (λx. x = ListNil) ls ⇒ FLAT (MAP list_t_v ls) = []
+   
+   [MEM_EVERY_not]  Theorem
+      
+      ⊢ ∀k v ls. MEM (k,v) ls ⇒ EVERY (λx. k ≠ FST x) ls ⇒ F
+   
+   [MEM_distinct_keys_lookup]  Theorem
+      
+      ⊢ ∀k v ls. MEM (k,v) ls ⇒ distinct_keys ls ⇒ lookup k ls = SOME v
+   
+   [distinct_keys_MEM_not_eq]  Theorem
+      
+      ⊢ ∀ls k1 x1 k2 x2.
+          distinct_keys ((k1,x1)::ls) ⇒ MEM (k2,x2) ls ⇒ k2 ≠ k1
+   
+   [distinct_keys_lookup_NONE]  Theorem
+      
+      ⊢ ∀ls k x. distinct_keys ((k,x)::ls) ⇒ lookup k ls = NONE
+   
+   [every_distinct_remove_every_distinct]  Theorem
+      
+      ⊢ ∀k0 k1 ls0.
+          EVERY (λy. k1 ≠ FST y) ls0 ⇒
+          EVERY (λy. k1 ≠ FST y) (remove k0 ls0)
+   
+   [hash_map_allocate_slots_fwd_spec]  Theorem
+      
+      ⊢ ∀n. usize_to_int n ≤ usize_max ⇒
+            ∃slots.
+              hash_map_allocate_slots_fwd vec_new n = Return slots ∧
+              slots_t_inv slots ∧
+              len (vec_to_list slots) = usize_to_int n ∧
+              EVERY (λx. x = ListNil) (vec_to_list slots)
+   
+   [hash_map_allocate_slots_loop_fwd_spec]  Theorem
+      
+      ⊢ ∀slots n.
+          EVERY (λx. x = ListNil) (vec_to_list slots) ⇒
+          len (vec_to_list slots) + usize_to_int n ≤ usize_max ⇒
+          ∃nslots.
+            hash_map_allocate_slots_loop_fwd slots n = Return nslots ∧
+            len (vec_to_list nslots) =
+            len (vec_to_list slots) + usize_to_int n ∧
+            EVERY (λx. x = ListNil) (vec_to_list nslots)
+   
+   [hash_map_clear_fwd_back_spec]  Theorem
+      
+      ⊢ ∀hm.
+          hash_map_t_inv hm ⇒
+          ∃hm1.
+            hash_map_clear_fwd_back hm = Return hm1 ∧ hash_map_t_inv hm1 ∧
+            len_s hm1 = 0 ∧ ∀k. lookup_s hm1 k = NONE
+   
+   [hash_map_clear_loop_fwd_back_spec]  Theorem
+      
+      ⊢ ∀slots. ∃slots1.
+          hash_map_clear_loop_fwd_back slots (int_to_usize 0) =
+          Return slots1 ∧
+          len (vec_to_list slots1) = len (vec_to_list slots) ∧
+          (∀j. 0 ≤ j ⇒
+               j < len (vec_to_list slots) ⇒
+               index j (vec_to_list slots1) = ListNil) ∧
+          FLAT (MAP list_t_v (vec_to_list slots1)) = []
+   
+   [hash_map_clear_loop_fwd_back_spec_aux]  Theorem
+      
+      ⊢ ∀n slots i.
+          n = len (vec_to_list slots) − usize_to_int i ⇒
+          ∃slots1.
+            hash_map_clear_loop_fwd_back slots i = Return slots1 ∧
+            len (vec_to_list slots1) = len (vec_to_list slots) ∧
+            (∀j. 0 ≤ j ⇒
+                 j < usize_to_int i ⇒
+                 j < len (vec_to_list slots) ⇒
+                 index j (vec_to_list slots1) = index j (vec_to_list slots)) ∧
+            ∀j. usize_to_int i ≤ j ⇒
+                j < len (vec_to_list slots) ⇒
+                index j (vec_to_list slots1) = ListNil
+   
+   [hash_map_cond_incr_thm]  Theorem
+      
+      ⊢ ∀hm key a.
+          hash_map_t_base_inv hm ⇒
+          (slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE ⇒
+           len_s hm < usize_max) ⇒
+          ∃n. (if
+                 slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE
+               then
+                 usize_add hm.hash_map_num_entries (int_to_usize 1)
+               else Return hm.hash_map_num_entries) =
+              Return n ∧
+              if
+                slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE
+              then
+                usize_to_int n = usize_to_int hm.hash_map_num_entries + 1
+              else n = hm.hash_map_num_entries
+   
+   [hash_map_contains_key_fwd_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          hash_map_contains_key_fwd hm key =
+          Return (lookup_s hm key ≠ NONE)
+   
+   [hash_map_contains_key_in_list_fwd_spec]  Theorem
+      
+      ⊢ ∀key ls.
+          hash_map_contains_key_in_list_fwd key ls =
+          Return (slot_t_lookup key ls ≠ NONE)
+   
+   [hash_map_get_fwd_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          case hash_map_get_fwd hm key of
+            Return x => lookup_s hm key = SOME x
+          | Fail v1 => lookup_s hm key = NONE
+          | Diverge => F
+   
+   [hash_map_get_in_list_fwd_spec]  Theorem
+      
+      ⊢ ∀ls key.
+          case hash_map_get_in_list_fwd key ls of
+            Return x => slot_t_lookup key ls = SOME x
+          | Fail v1 => slot_t_lookup key ls = NONE
+          | Diverge => F
+   
+   [hash_map_get_mut_back_spec]  Theorem
+      
+      ⊢ ∀hm key nx.
+          lookup_s hm key ≠ NONE ⇒
+          hash_map_t_inv hm ⇒
+          ∃hm1.
+            hash_map_get_mut_back hm key nx = Return hm1 ∧
+            lookup_s hm1 key = SOME nx ∧
+            ∀k. k ≠ key ⇒ lookup_s hm1 k = lookup_s hm k
+   
+   [hash_map_get_mut_fwd_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          case hash_map_get_mut_fwd hm key of
+            Return x => lookup_s hm key = SOME x
+          | Fail v1 => lookup_s hm key = NONE
+          | Diverge => F
+   
+   [hash_map_get_mut_in_list_back_spec]  Theorem
+      
+      ⊢ ∀ls key nx.
+          slot_t_lookup key ls ≠ NONE ⇒
+          ∃nls.
+            hash_map_get_mut_in_list_back ls key nx = Return nls ∧
+            slot_t_lookup key nls = SOME nx ∧
+            ∀k. k ≠ key ⇒ slot_t_lookup k nls = slot_t_lookup k ls
+   
+   [hash_map_get_mut_in_list_fwd_spec]  Theorem
+      
+      ⊢ ∀ls key.
+          case hash_map_get_mut_in_list_fwd ls key of
+            Return x => slot_t_lookup key ls = SOME x
+          | Fail v1 => slot_t_lookup key ls = NONE
+          | Diverge => F
+   
+   [hash_map_insert_fwd_back_spec]  Theorem
+      
+      [oracles: DISK_THM] [axioms: usize_u32_bounds] []
+      ⊢ ∀hm key value.
+          hash_map_t_inv hm ⇒
+          (lookup_s hm key = NONE ⇒ len_s hm < usize_max) ⇒
+          ∃hm1.
+            hash_map_insert_fwd_back hm key value = Return hm1 ∧
+            hash_map_t_inv hm1 ∧ lookup_s hm1 key = SOME value ∧
+            (∀k. k ≠ key ⇒ lookup_s hm k = lookup_s hm1 k) ∧
+            case lookup_s hm key of
+              NONE => len_s hm1 = len_s hm + 1
+            | SOME v => len_s hm1 = len_s hm
+   
+   [hash_map_insert_in_list_fwd_spec]  Theorem
+      
+      ⊢ ∀ls key value. ∃b.
+          hash_map_insert_in_list_fwd key value ls = Return b ∧
+          (b ⇔ slot_t_lookup key ls = NONE)
+   
+   [hash_map_insert_in_list_loop_back_EVERY_distinct_keys]  Theorem
+      
+      ⊢ ∀k v k1 ls0 ls1.
+          k1 ≠ k ⇒
+          EVERY (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
+          pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
+          hash_map_insert_in_list_loop_back k v ls0 = Return ls1 ⇒
+          EVERY (λy. k1 ≠ FST y) (list_t_v ls1)
+   
+   [hash_map_insert_in_list_loop_back_distinct_keys]  Theorem
+      
+      ⊢ ∀k v ls0 ls1.
+          distinct_keys (list_t_v ls0) ⇒
+          hash_map_insert_in_list_loop_back k v ls0 = Return ls1 ⇒
+          distinct_keys (list_t_v ls1)
+   
+   [hash_map_insert_in_list_loop_back_spec]  Theorem
+      
+      ⊢ ∀i ls key value.
+          distinct_keys (list_t_v ls) ⇒
+          ∃ls1.
+            hash_map_insert_in_list_loop_back key value ls = Return ls1 ∧
+            ∀l. slot_s_inv_hash l (hash_mod_key key l) (list_t_v ls) ⇒
+                insert_in_slot_t_rel l key value ls ls1
+   
+   [hash_map_insert_in_list_loop_back_spec_aux]  Theorem
+      
+      ⊢ ∀ls key value. ∃ls1.
+          hash_map_insert_in_list_loop_back key value ls = Return ls1 ∧
+          slot_t_lookup key ls1 = SOME value ∧
+          (∀k. k ≠ key ⇒ slot_t_lookup k ls = slot_t_lookup k ls1) ∧
+          (∀l. slot_s_inv_hash l (hash_mod_key key l) (list_t_v ls) ⇒
+               slot_s_inv_hash l (hash_mod_key key l) (list_t_v ls1)) ∧
+          case slot_t_lookup key ls of
+            NONE => len (list_t_v ls1) = len (list_t_v ls) + 1
+          | SOME v => len (list_t_v ls1) = len (list_t_v ls)
+   
+   [hash_map_insert_in_list_loop_fwd_spec]  Theorem
+      
+      ⊢ ∀ls key value. ∃b.
+          hash_map_insert_in_list_loop_fwd key value ls = Return b ∧
+          (b ⇔ slot_t_lookup key ls = NONE)
+   
+   [hash_map_insert_no_resize_fwd_back_branches_eq]  Theorem
+      
+      ⊢ (if slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE then
+           do
+             i0 <- usize_add hm.hash_map_num_entries (int_to_usize 1);
+             l0 <-
+               hash_map_insert_in_list_back key value
+                 (vec_index hm.hash_map_slots a);
+             v <- vec_index_mut_back hm.hash_map_slots a l0;
+             Return
+               (hm with <|hash_map_num_entries := i0; hash_map_slots := v|>)
+           od
+         else
+           do
+             l0 <-
+               hash_map_insert_in_list_back key value
+                 (vec_index hm.hash_map_slots a);
+             v <- vec_index_mut_back hm.hash_map_slots a l0;
+             Return (hm with hash_map_slots := v)
+           od) =
+        do
+          i0 <-
+            if
+              slot_t_lookup key (vec_index hm.hash_map_slots a) = NONE
+            then
+              usize_add hm.hash_map_num_entries (int_to_usize 1)
+            else Return hm.hash_map_num_entries;
+          l0 <-
+            hash_map_insert_in_list_back key value
+              (vec_index hm.hash_map_slots a);
+          v <- vec_index_mut_back hm.hash_map_slots a l0;
+          Return
+            (hm with <|hash_map_num_entries := i0; hash_map_slots := v|>)
+        od
+   
+   [hash_map_insert_no_resize_fwd_back_spec]  Theorem
+      
+      ⊢ ∀hm key value.
+          hash_map_t_base_inv hm ⇒
+          (lookup_s hm key = NONE ⇒ len_s hm < usize_max) ⇒
+          ∃hm1.
+            hash_map_insert_no_resize_fwd_back hm key value = Return hm1 ∧
+            hash_map_t_base_inv hm1 ∧ lookup_s hm1 key = SOME value ∧
+            (∀k. k ≠ key ⇒ lookup_s hm k = lookup_s hm1 k) ∧
+            (case lookup_s hm key of
+               NONE => len_s hm1 = len_s hm + 1
+             | SOME v => len_s hm1 = len_s hm) ∧
+            hash_map_same_params hm hm1
+   
+   [hash_map_insert_no_resize_fwd_back_spec_aux]  Theorem
+      
+      ⊢ ∀hm key value.
+          hash_map_t_base_inv hm ⇒
+          (lookup_s hm key = NONE ⇒ len_s hm < usize_max) ⇒
+          ∃hm1 slot1.
+            hash_map_insert_no_resize_fwd_back hm key value = Return hm1 ∧
+            len (vec_to_list hm1.hash_map_slots) =
+            len (vec_to_list hm.hash_map_slots) ∧
+            (let
+               l = len (vec_to_list hm.hash_map_slots);
+               i = hash_mod_key key (len (vec_to_list hm.hash_map_slots));
+               slot = index i (vec_to_list hm.hash_map_slots)
+             in
+               insert_in_slot_t_rel l key value slot slot1 ∧
+               vec_to_list hm1.hash_map_slots =
+               update (vec_to_list hm.hash_map_slots) i slot1 ∧
+               hm1.hash_map_max_load_factor = hm.hash_map_max_load_factor ∧
+               hm1.hash_map_max_load = hm.hash_map_max_load ∧
+               (case lookup_s hm key of
+                  NONE =>
+                    usize_to_int hm1.hash_map_num_entries =
+                    usize_to_int hm.hash_map_num_entries + 1
+                | SOME v =>
+                  hm1.hash_map_num_entries = hm.hash_map_num_entries) ∧
+               hash_map_same_params hm hm1)
+   
+   [hash_map_len_spec]  Theorem
+      
+      ⊢ ∀hm.
+          hash_map_t_base_inv hm ⇒
+          ∃x. hash_map_len_fwd hm = Return x ∧ usize_to_int x = len_s hm
+   
+   [hash_map_move_elements_from_list_fwd_back_spec]  Theorem
+      
+      ⊢ ∀hm ls.
+          (let
+             l = len (list_t_v ls)
+           in
+             hash_map_t_base_inv hm ⇒
+             len_s hm + l ≤ usize_max ⇒
+             ∃hm1.
+               hash_map_move_elements_from_list_fwd_back hm ls = Return hm1 ∧
+               hash_map_t_base_inv hm1 ∧
+               ((∀k v. MEM (k,v) (list_t_v ls) ⇒ lookup_s hm k = NONE) ⇒
+                distinct_keys (list_t_v ls) ⇒
+                (∀k. slot_t_lookup k ls = NONE ⇒
+                     lookup_s hm1 k = lookup_s hm k) ∧
+                (∀k. slot_t_lookup k ls ≠ NONE ⇒
+                     lookup_s hm1 k = slot_t_lookup k ls) ∧
+                len_s hm1 = len_s hm + l) ∧ hash_map_same_params hm hm1)
+   
+   [hash_map_move_elements_fwd_back_spec]  Theorem
+      
+      ⊢ ∀hm slots i.
+          (let
+             slots_l =
+               len
+                 (FLAT
+                    (MAP list_t_v
+                       (drop (usize_to_int i) (vec_to_list slots))))
+           in
+             hash_map_t_base_inv hm ⇒
+             len_s hm + slots_l ≤ usize_max ⇒
+             (∀j. (let
+                     l = len (vec_to_list slots)
+                   in
+                     usize_to_int i ≤ j ⇒
+                     j < l ⇒
+                     (let
+                        slot = index j (vec_to_list slots)
+                      in
+                        slot_t_inv l j slot ∧
+                        ∀k v.
+                          MEM (k,v) (list_t_v slot) ⇒ lookup_s hm k = NONE))) ⇒
+             ∃hm1 slots1.
+               hash_map_move_elements_fwd_back hm slots i =
+               Return (hm1,slots1) ∧ hash_map_t_base_inv hm1 ∧
+               len_s hm1 = len_s hm + slots_l ∧
+               (∀k. lookup_s hm1 k =
+                    case lookup_s hm k of
+                      NONE =>
+                        (let
+                           j = hash_mod_key k (len (vec_to_list slots))
+                         in
+                           if
+                             usize_to_int i ≤ j ∧
+                             j < len (vec_to_list slots)
+                           then
+                             (let
+                                slot = index j (vec_to_list slots)
+                              in
+                                lookup k (list_t_v slot))
+                           else NONE)
+                    | SOME v => SOME v) ∧ hash_map_same_params hm hm1)
+   
+   [hash_map_move_elements_loop_fwd_back_spec_aux]  Theorem
+      
+      ⊢ ∀hm slots i n.
+          (let
+             slots_l =
+               len
+                 (FLAT
+                    (MAP list_t_v
+                       (drop (usize_to_int i) (vec_to_list slots))))
+           in
+             n = len (vec_to_list slots) − usize_to_int i ⇒
+             hash_map_t_base_inv hm ⇒
+             len_s hm + slots_l ≤ usize_max ⇒
+             (∀j. (let
+                     l = len (vec_to_list slots)
+                   in
+                     usize_to_int i ≤ j ⇒
+                     j < l ⇒
+                     (let
+                        slot = index j (vec_to_list slots)
+                      in
+                        slot_t_inv l j slot ∧
+                        ∀k v.
+                          MEM (k,v) (list_t_v slot) ⇒ lookup_s hm k = NONE))) ⇒
+             ∃hm1 slots1.
+               hash_map_move_elements_loop_fwd_back hm slots i =
+               Return (hm1,slots1) ∧ hash_map_t_base_inv hm1 ∧
+               len_s hm1 = len_s hm + slots_l ∧
+               (∀k. lookup_s hm1 k =
+                    case lookup_s hm k of
+                      NONE =>
+                        (let
+                           j = hash_mod_key k (len (vec_to_list slots))
+                         in
+                           if
+                             usize_to_int i ≤ j ∧
+                             j < len (vec_to_list slots)
+                           then
+                             (let
+                                slot = index j (vec_to_list slots)
+                              in
+                                lookup k (list_t_v slot))
+                           else NONE)
+                    | SOME v => SOME v) ∧ hash_map_same_params hm hm1)
+   
+   [hash_map_new_fwd_spec]  Theorem
+      
+      ⊢ ∃hm.
+          hash_map_new_fwd = Return hm ∧ hash_map_t_inv hm ∧
+          ∀k. lookup_s hm k = NONE ∧ len_s hm = 0
+   
+   [hash_map_new_with_capacity_fwd_spec]  Theorem
+      
+      ⊢ ∀capacity max_load_dividend max_load_divisor.
+          0 < usize_to_int max_load_dividend ⇒
+          usize_to_int max_load_dividend < usize_to_int max_load_divisor ⇒
+          0 < usize_to_int capacity ⇒
+          usize_to_int capacity * usize_to_int max_load_dividend ≥
+          usize_to_int max_load_divisor ⇒
+          usize_to_int capacity * usize_to_int max_load_dividend ≤
+          usize_max ⇒
+          ∃hm.
+            hash_map_new_with_capacity_fwd capacity max_load_dividend
+              max_load_divisor =
+            Return hm ∧ hash_map_t_inv hm ∧ len_s hm = 0 ∧
+            ∀k. lookup_s hm k = NONE ∧
+                len (vec_to_list hm.hash_map_slots) = usize_to_int capacity ∧
+                hm.hash_map_max_load_factor =
+                (max_load_dividend,max_load_divisor)
+   
+   [hash_map_remove_back_branch_eq]  Theorem
+      
+      ⊢ ∀key hm a.
+          (case lookup key (list_t_v (vec_index hm.hash_map_slots a)) of
+             NONE =>
+               do
+                 l0 <-
+                   hash_map_remove_from_list_back key
+                     (vec_index hm.hash_map_slots a);
+                 v <- vec_index_mut_back hm.hash_map_slots a l0;
+                 Return (hm with hash_map_slots := v)
+               od
+           | SOME x0 =>
+             do
+               i0 <- usize_sub hm.hash_map_num_entries (int_to_usize 1);
+               l0 <-
+                 hash_map_remove_from_list_back key
+                   (vec_index hm.hash_map_slots a);
+               v <- vec_index_mut_back hm.hash_map_slots a l0;
+               Return
+                 (hm with
+                  <|hash_map_num_entries := i0; hash_map_slots := v|>)
+             od) =
+          do
+            i0 <-
+              case lookup key (list_t_v (vec_index hm.hash_map_slots a)) of
+                NONE => Return hm.hash_map_num_entries
+              | SOME v =>
+                usize_sub hm.hash_map_num_entries (int_to_usize 1);
+            l0 <-
+              hash_map_remove_from_list_back key
+                (vec_index hm.hash_map_slots a);
+            v <- vec_index_mut_back hm.hash_map_slots a l0;
+            Return
+              (hm with <|hash_map_num_entries := i0; hash_map_slots := v|>)
+          od
+   
+   [hash_map_remove_back_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          ∃hm1.
+            hash_map_remove_back hm key = Return hm1 ∧ hash_map_t_inv hm1 ∧
+            lookup_s hm1 key = NONE ∧
+            (∀k. k ≠ key ⇒ lookup_s hm1 k = lookup_s hm k) ∧
+            case lookup_s hm key of
+              NONE => len_s hm1 = len_s hm
+            | SOME v => len_s hm1 = len_s hm − 1
+   
+   [hash_map_remove_from_list_back_spec]  Theorem
+      
+      ⊢ ∀key ls. ∃ls1.
+          hash_map_remove_from_list_back key ls = Return ls1 ∧
+          ∀l i.
+            slot_t_inv l i ls ⇒
+            slot_t_inv l i ls1 ∧ list_t_v ls1 = remove key (list_t_v ls) ∧
+            slot_t_lookup key ls1 = NONE ∧
+            (∀k. k ≠ key ⇒ slot_t_lookup k ls1 = slot_t_lookup k ls) ∧
+            case slot_t_lookup key ls of
+              NONE => len (list_t_v ls1) = len (list_t_v ls)
+            | SOME v => len (list_t_v ls1) = len (list_t_v ls) − 1
+   
+   [hash_map_remove_from_list_fwd_spec]  Theorem
+      
+      ⊢ ∀key l i ls.
+          hash_map_remove_from_list_fwd key ls =
+          Return (slot_t_lookup key ls)
+   
+   [hash_map_remove_fwd_spec]  Theorem
+      
+      ⊢ ∀hm key.
+          hash_map_t_inv hm ⇒
+          hash_map_remove_fwd hm key = Return (lookup_s hm key)
+   
+   [hash_map_same_params_refl]  Theorem
+      
+      ⊢ ∀hm. hash_map_same_params hm hm
+   
+   [hash_map_t_base_inv_len_slots]  Theorem
+      
+      ⊢ ∀hm.
+          hash_map_t_base_inv hm ⇒ 0 < len (vec_to_list hm.hash_map_slots)
+   
+   [hash_map_try_resize_fwd_back_spec]  Theorem
+      
+      [oracles: DISK_THM] [axioms: usize_u32_bounds] []
+      ⊢ ∀hm.
+          hash_map_t_base_inv hm ⇒
+          hash_map_just_before_resize_pred hm ⇒
+          ∃hm1.
+            hash_map_try_resize_fwd_back hm = Return hm1 ∧
+            hash_map_t_inv hm1 ∧ len_s hm1 = len_s hm ∧
+            ∀k. lookup_s hm1 k = lookup_s hm k
+   
+   [key_MEM_j_lookup_i_is_NONE]  Theorem
+      
+      ⊢ ∀i j slots k v.
+          usize_to_int i < j ⇒
+          j < len (vec_to_list slots) ⇒
+          (∀j. usize_to_int i ≤ j ⇒
+               j < len (vec_to_list slots) ⇒
+               slot_t_inv (len (vec_to_list slots)) j
+                 (index j (vec_to_list slots))) ⇒
+          MEM (k,v) (list_t_v (index j (vec_to_list slots))) ⇒
+          slot_t_lookup k (index (usize_to_int i) (vec_to_list slots)) =
+          NONE
+   
+   [len_FLAT_MAP_update]  Theorem
+      
+      ⊢ ∀x ls i.
+          0 ≤ i ⇒
+          i < len ls ⇒
+          len (FLAT (MAP list_t_v (update ls i x))) =
+          len (FLAT (MAP list_t_v ls)) + len (list_t_v x) −
+          len (list_t_v (index i ls))
+   
+   [len_index_FLAT_MAP_list_t_v]  Theorem
+      
+      ⊢ ∀slots i.
+          0 ≤ i ⇒
+          i < len slots ⇒
+          len (list_t_v (index i slots)) ≤
+          len (FLAT (MAP list_t_v (drop i slots)))
+   
+   [len_vec_FLAT_drop_update]  Theorem
+      
+      ⊢ ∀slots i.
+          0 ≤ i ⇒
+          i < len slots ⇒
+          len (FLAT (MAP list_t_v (drop i slots))) =
+          len (list_t_v (index i slots)) +
+          len (FLAT (MAP list_t_v (drop (i + 1) (update slots i ListNil))))
+   
+   [lookup_SOME_not_empty]  Theorem
+      
+      ⊢ ∀ls k. lookup k ls ≠ NONE ⇒ 0 < len ls
+   
+   [lookup_cond_decr_entries_eq]  Theorem
+      
+      ⊢ ∀hm key i.
+          hash_map_t_inv hm ⇒
+          usize_to_int i < len (vec_to_list hm.hash_map_slots) ⇒
+          ∃j. (case
+                 lookup key (list_t_v (vec_index hm.hash_map_slots i))
+               of
+                 NONE => Return hm.hash_map_num_entries
+               | SOME v =>
+                 usize_sub hm.hash_map_num_entries (int_to_usize 1)) =
+              Return j ∧
+              (lookup key (list_t_v (vec_index hm.hash_map_slots i)) = NONE ⇒
+               j = hm.hash_map_num_entries) ∧
+              (lookup key (list_t_v (vec_index hm.hash_map_slots i)) ≠ NONE ⇒
+               usize_to_int j + 1 = usize_to_int hm.hash_map_num_entries)
+   
+   [lookup_def]  Theorem
+      
+      ⊢ (∀key. lookup key [] = NONE) ∧
+        ∀v ls key k.
+          lookup key ((k,v)::ls) =
+          if k = key then SOME v else lookup key ls
+   
+   [lookup_distinct_keys_MEM]  Theorem
+      
+      ⊢ ∀k v ls. lookup k ls = SOME v ⇒ distinct_keys ls ⇒ MEM (k,v) ls
+   
+   [lookup_ind]  Theorem
+      
+      ⊢ ∀P. (∀key. P key []) ∧
+            (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
+            ∀v v1. P v v1
+   
+   [lookup_s_SOME_not_empty]  Theorem
+      
+      ⊢ ∀hm key. hash_map_t_inv hm ⇒ lookup_s hm key ≠ NONE ⇒ 0 < len_s hm
+   
+   [pairwise_rel_quant_equiv]  Theorem
+      
+      ⊢ ∀p ls.
+          pairwise_rel p ls ⇔
+          ∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls)
+   
+   [remove_def]  Theorem
+      
+      ⊢ (∀key. remove key [] = []) ∧
+        ∀v ls key k.
+          remove key ((k,v)::ls) =
+          if k = key then ls else (k,v)::remove key ls
+   
+   [remove_ind]  Theorem
+      
+      ⊢ ∀P. (∀key. P key []) ∧
+            (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
+            ∀v v1. P v v1
+   
+   [slot_t_lookup_SOME_not_empty]  Theorem
+      
+      ⊢ ∀ls i k.
+          0 ≤ i ⇒
+          i < len ls ⇒
+          slot_t_lookup k (index i ls) ≠ NONE ⇒
+          0 < len (FLAT (MAP list_t_v ls))
+   
+   
+*)
+end