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