diff options
Diffstat (limited to 'tests/hol4/hashmap_main')
| -rw-r--r-- | tests/hol4/hashmap_main/Holmakefile | 5 | ||||
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_FunsScript.sml | 647 | ||||
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig | 598 | ||||
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml | 15 | ||||
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig | 11 | ||||
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_TypesScript.sml | 27 | ||||
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig | 568 |
7 files changed, 1871 insertions, 0 deletions
diff --git a/tests/hol4/hashmap_main/Holmakefile b/tests/hol4/hashmap_main/Holmakefile new file mode 100644 index 00000000..3c4b8973 --- /dev/null +++ b/tests/hol4/hashmap_main/Holmakefile @@ -0,0 +1,5 @@ +# This file was automatically generated - modify ../Holmakefile.template instead +INCLUDES = ../../../backends/hol4 + +all: $(DEFAULT_TARGETS) +.PHONY: all diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml new file mode 100644 index 00000000..c1e30aa6 --- /dev/null +++ b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml @@ -0,0 +1,647 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: function definitions *) +open primitivesLib divDefLib +open hashmapMain_TypesTheory hashmapMain_OpaqueTheory + +val _ = new_theory "hashmapMain_Funs" + + +val hashmap_hash_key_fwd_def = Define ‘ + (** [hashmap_main::hashmap::hash_key]: forward function *) + hashmap_hash_key_fwd (k : usize) : usize result = + Return k +’ + +val [hashmap_hash_map_allocate_slots_loop_fwd_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *) + hashmap_hash_map_allocate_slots_loop_fwd + (slots : 't hashmap_list_t vec) (n : usize) : + 't hashmap_list_t vec result + = + if usize_gt n (int_to_usize 0) + then ( + do + slots0 <- vec_push_back slots HashmapListNil; + n0 <- usize_sub n (int_to_usize 1); + hashmap_hash_map_allocate_slots_loop_fwd slots0 n0 + od) + else Return slots +’ + +val hashmap_hash_map_allocate_slots_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *) + hashmap_hash_map_allocate_slots_fwd + (slots : 't hashmap_list_t vec) (n : usize) : + 't hashmap_list_t vec result + = + hashmap_hash_map_allocate_slots_loop_fwd slots n +’ + +val hashmap_hash_map_new_with_capacity_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *) + hashmap_hash_map_new_with_capacity_fwd + (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : + 't hashmap_hash_map_t result + = + let v = vec_new in + do + slots <- hashmap_hash_map_allocate_slots_fwd v capacity; + i <- usize_mul capacity max_load_dividend; + i0 <- usize_div i max_load_divisor; + Return + (<| + hashmap_hash_map_num_entries := (int_to_usize 0); + hashmap_hash_map_max_load_factor := + (max_load_dividend, max_load_divisor); + hashmap_hash_map_max_load := i0; + hashmap_hash_map_slots := slots + |>) + od +’ + +val hashmap_hash_map_new_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *) + hashmap_hash_map_new_fwd : 't hashmap_hash_map_t result = + hashmap_hash_map_new_with_capacity_fwd (int_to_usize 32) (int_to_usize 4) + (int_to_usize 5) +’ + +val [hashmap_hash_map_clear_loop_fwd_back_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_clear_loop_fwd_back + (slots : 't hashmap_list_t vec) (i : usize) : + 't hashmap_list_t vec result + = + let i0 = vec_len slots in + if usize_lt i i0 + then ( + do + i1 <- usize_add i (int_to_usize 1); + slots0 <- vec_index_mut_back slots i HashmapListNil; + hashmap_hash_map_clear_loop_fwd_back slots0 i1 + od) + else Return slots +’ + +val hashmap_hash_map_clear_fwd_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_clear_fwd_back + (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result = + do + v <- + hashmap_hash_map_clear_loop_fwd_back self.hashmap_hash_map_slots + (int_to_usize 0); + Return + (self + with + <| + hashmap_hash_map_num_entries := (int_to_usize 0); + hashmap_hash_map_slots := v + |>) + od +’ + +val hashmap_hash_map_len_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *) + hashmap_hash_map_len_fwd (self : 't hashmap_hash_map_t) : usize result = + Return self.hashmap_hash_map_num_entries +’ + +val [hashmap_hash_map_insert_in_list_loop_fwd_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *) + hashmap_hash_map_insert_in_list_loop_fwd + (key : usize) (value : 't) (ls : 't hashmap_list_t) : bool result = + (case ls of + | HashmapListCons ckey cvalue tl => + if ckey = key + then Return F + else hashmap_hash_map_insert_in_list_loop_fwd key value tl + | HashmapListNil => Return T) +’ + +val hashmap_hash_map_insert_in_list_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *) + hashmap_hash_map_insert_in_list_fwd + (key : usize) (value : 't) (ls : 't hashmap_list_t) : bool result = + hashmap_hash_map_insert_in_list_loop_fwd key value ls +’ + +val [hashmap_hash_map_insert_in_list_loop_back_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *) + hashmap_hash_map_insert_in_list_loop_back + (key : usize) (value : 't) (ls : 't hashmap_list_t) : + 't hashmap_list_t result + = + (case ls of + | HashmapListCons ckey cvalue tl => + if ckey = key + then Return (HashmapListCons ckey value tl) + else ( + do + tl0 <- hashmap_hash_map_insert_in_list_loop_back key value tl; + Return (HashmapListCons ckey cvalue tl0) + od) + | HashmapListNil => + let l = HashmapListNil in Return (HashmapListCons key value l)) +’ + +val hashmap_hash_map_insert_in_list_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *) + hashmap_hash_map_insert_in_list_back + (key : usize) (value : 't) (ls : 't hashmap_list_t) : + 't hashmap_list_t result + = + hashmap_hash_map_insert_in_list_loop_back key value ls +’ + +val hashmap_hash_map_insert_no_resize_fwd_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_insert_no_resize_fwd_back + (self : 't hashmap_hash_map_t) (key : usize) (value : 't) : + 't hashmap_hash_map_t result + = + do + hash <- hashmap_hash_key_fwd key; + let i = vec_len self.hashmap_hash_map_slots in + do + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + inserted <- hashmap_hash_map_insert_in_list_fwd key value l; + if inserted + then ( + do + i0 <- usize_add self.hashmap_hash_map_num_entries (int_to_usize 1); + l0 <- hashmap_hash_map_insert_in_list_back key value l; + v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0; + Return + (self + with + <| + hashmap_hash_map_num_entries := i0; hashmap_hash_map_slots := v + |>) + od) + else ( + do + l0 <- hashmap_hash_map_insert_in_list_back key value l; + v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0; + Return (self with <| hashmap_hash_map_slots := v |>) + od) + od + od +’ + +val [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_move_elements_from_list_loop_fwd_back + (ntable : 't hashmap_hash_map_t) (ls : 't hashmap_list_t) : + 't hashmap_hash_map_t result + = + (case ls of + | HashmapListCons k v tl => + do + ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back ntable k v; + hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable0 tl + od + | HashmapListNil => Return ntable) +’ + +val hashmap_hash_map_move_elements_from_list_fwd_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_move_elements_from_list_fwd_back + (ntable : 't hashmap_hash_map_t) (ls : 't hashmap_list_t) : + 't hashmap_hash_map_t result + = + hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls +’ + +val [hashmap_hash_map_move_elements_loop_fwd_back_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_move_elements_loop_fwd_back + (ntable : 't hashmap_hash_map_t) (slots : 't hashmap_list_t vec) + (i : usize) : + ('t hashmap_hash_map_t # 't hashmap_list_t vec) result + = + let i0 = vec_len slots in + if usize_lt i i0 + then ( + do + l <- vec_index_mut_fwd slots i; + let ls = mem_replace_fwd l HashmapListNil in + do + ntable0 <- hashmap_hash_map_move_elements_from_list_fwd_back ntable ls; + i1 <- usize_add i (int_to_usize 1); + let l0 = mem_replace_back l HashmapListNil in + do + slots0 <- vec_index_mut_back slots i l0; + hashmap_hash_map_move_elements_loop_fwd_back ntable0 slots0 i1 + od + od + od) + else Return (ntable, slots) +’ + +val hashmap_hash_map_move_elements_fwd_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_move_elements_fwd_back + (ntable : 't hashmap_hash_map_t) (slots : 't hashmap_list_t vec) + (i : usize) : + ('t hashmap_hash_map_t # 't hashmap_list_t vec) result + = + hashmap_hash_map_move_elements_loop_fwd_back ntable slots i +’ + +val hashmap_hash_map_try_resize_fwd_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_try_resize_fwd_back + (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result = + do + max_usize <- mk_usize (u32_to_int core_u32_max); + let capacity = vec_len self.hashmap_hash_map_slots in + do + n1 <- usize_div max_usize (int_to_usize 2); + let (i, i0) = self.hashmap_hash_map_max_load_factor in + do + i1 <- usize_div n1 i; + if usize_le capacity i1 + then ( + do + i2 <- usize_mul capacity (int_to_usize 2); + ntable <- hashmap_hash_map_new_with_capacity_fwd i2 i i0; + (ntable0, _) <- + hashmap_hash_map_move_elements_fwd_back ntable + self.hashmap_hash_map_slots (int_to_usize 0); + Return + (ntable0 + with + <| + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries; + hashmap_hash_map_max_load_factor := (i, i0) + |>) + od) + else Return (self with <| hashmap_hash_map_max_load_factor := (i, i0) |>) + od + od + od +’ + +val hashmap_hash_map_insert_fwd_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) + hashmap_hash_map_insert_fwd_back + (self : 't hashmap_hash_map_t) (key : usize) (value : 't) : + 't hashmap_hash_map_t result + = + do + self0 <- hashmap_hash_map_insert_no_resize_fwd_back self key value; + i <- hashmap_hash_map_len_fwd self0; + if usize_gt i self0.hashmap_hash_map_max_load + then hashmap_hash_map_try_resize_fwd_back self0 + else Return self0 + od +’ + +val [hashmap_hash_map_contains_key_in_list_loop_fwd_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *) + hashmap_hash_map_contains_key_in_list_loop_fwd + (key : usize) (ls : 't hashmap_list_t) : bool result = + (case ls of + | HashmapListCons ckey t tl => + if ckey = key + then Return T + else hashmap_hash_map_contains_key_in_list_loop_fwd key tl + | HashmapListNil => Return F) +’ + +val hashmap_hash_map_contains_key_in_list_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *) + hashmap_hash_map_contains_key_in_list_fwd + (key : usize) (ls : 't hashmap_list_t) : bool result = + hashmap_hash_map_contains_key_in_list_loop_fwd key ls +’ + +val hashmap_hash_map_contains_key_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *) + hashmap_hash_map_contains_key_fwd + (self : 't hashmap_hash_map_t) (key : usize) : bool result = + do + hash <- hashmap_hash_key_fwd key; + let i = vec_len self.hashmap_hash_map_slots in + do + hash_mod <- usize_rem hash i; + l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod; + hashmap_hash_map_contains_key_in_list_fwd key l + od + od +’ + +val [hashmap_hash_map_get_in_list_loop_fwd_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *) + hashmap_hash_map_get_in_list_loop_fwd + (key : usize) (ls : 't hashmap_list_t) : 't result = + (case ls of + | HashmapListCons ckey cvalue tl => + if ckey = key + then Return cvalue + else hashmap_hash_map_get_in_list_loop_fwd key tl + | HashmapListNil => Fail Failure) +’ + +val hashmap_hash_map_get_in_list_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *) + hashmap_hash_map_get_in_list_fwd + (key : usize) (ls : 't hashmap_list_t) : 't result = + hashmap_hash_map_get_in_list_loop_fwd key ls +’ + +val hashmap_hash_map_get_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *) + hashmap_hash_map_get_fwd + (self : 't hashmap_hash_map_t) (key : usize) : 't result = + do + hash <- hashmap_hash_key_fwd key; + let i = vec_len self.hashmap_hash_map_slots in + do + hash_mod <- usize_rem hash i; + l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod; + hashmap_hash_map_get_in_list_fwd key l + od + od +’ + +val [hashmap_hash_map_get_mut_in_list_loop_fwd_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *) + hashmap_hash_map_get_mut_in_list_loop_fwd + (ls : 't hashmap_list_t) (key : usize) : 't result = + (case ls of + | HashmapListCons ckey cvalue tl => + if ckey = key + then Return cvalue + else hashmap_hash_map_get_mut_in_list_loop_fwd tl key + | HashmapListNil => Fail Failure) +’ + +val hashmap_hash_map_get_mut_in_list_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *) + hashmap_hash_map_get_mut_in_list_fwd + (ls : 't hashmap_list_t) (key : usize) : 't result = + hashmap_hash_map_get_mut_in_list_loop_fwd ls key +’ + +val [hashmap_hash_map_get_mut_in_list_loop_back_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *) + hashmap_hash_map_get_mut_in_list_loop_back + (ls : 't hashmap_list_t) (key : usize) (ret : 't) : + 't hashmap_list_t result + = + (case ls of + | HashmapListCons ckey cvalue tl => + if ckey = key + then Return (HashmapListCons ckey ret tl) + else ( + do + tl0 <- hashmap_hash_map_get_mut_in_list_loop_back tl key ret; + Return (HashmapListCons ckey cvalue tl0) + od) + | HashmapListNil => Fail Failure) +’ + +val hashmap_hash_map_get_mut_in_list_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *) + hashmap_hash_map_get_mut_in_list_back + (ls : 't hashmap_list_t) (key : usize) (ret : 't) : + 't hashmap_list_t result + = + hashmap_hash_map_get_mut_in_list_loop_back ls key ret +’ + +val hashmap_hash_map_get_mut_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *) + hashmap_hash_map_get_mut_fwd + (self : 't hashmap_hash_map_t) (key : usize) : 't result = + do + hash <- hashmap_hash_key_fwd key; + let i = vec_len self.hashmap_hash_map_slots in + do + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + hashmap_hash_map_get_mut_in_list_fwd l key + od + od +’ + +val hashmap_hash_map_get_mut_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *) + hashmap_hash_map_get_mut_back + (self : 't hashmap_hash_map_t) (key : usize) (ret : 't) : + 't hashmap_hash_map_t result + = + do + hash <- hashmap_hash_key_fwd key; + let i = vec_len self.hashmap_hash_map_slots in + do + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + l0 <- hashmap_hash_map_get_mut_in_list_back l key ret; + v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0; + Return (self with <| hashmap_hash_map_slots := v |>) + od + od +’ + +val [hashmap_hash_map_remove_from_list_loop_fwd_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *) + hashmap_hash_map_remove_from_list_loop_fwd + (key : usize) (ls : 't hashmap_list_t) : 't option result = + (case ls of + | HashmapListCons ckey t tl => + if ckey = key + then + let mv_ls = mem_replace_fwd (HashmapListCons ckey t tl) HashmapListNil + in + (case mv_ls of + | HashmapListCons i cvalue tl0 => Return (SOME cvalue) + | HashmapListNil => Fail Failure) + else hashmap_hash_map_remove_from_list_loop_fwd key tl + | HashmapListNil => Return NONE) +’ + +val hashmap_hash_map_remove_from_list_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *) + hashmap_hash_map_remove_from_list_fwd + (key : usize) (ls : 't hashmap_list_t) : 't option result = + hashmap_hash_map_remove_from_list_loop_fwd key ls +’ + +val [hashmap_hash_map_remove_from_list_loop_back_def] = DefineDiv ‘ + (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *) + hashmap_hash_map_remove_from_list_loop_back + (key : usize) (ls : 't hashmap_list_t) : 't hashmap_list_t result = + (case ls of + | HashmapListCons ckey t tl => + if ckey = key + then + let mv_ls = mem_replace_fwd (HashmapListCons ckey t tl) HashmapListNil + in + (case mv_ls of + | HashmapListCons i cvalue tl0 => Return tl0 + | HashmapListNil => Fail Failure) + else ( + do + tl0 <- hashmap_hash_map_remove_from_list_loop_back key tl; + Return (HashmapListCons ckey t tl0) + od) + | HashmapListNil => Return HashmapListNil) +’ + +val hashmap_hash_map_remove_from_list_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *) + hashmap_hash_map_remove_from_list_back + (key : usize) (ls : 't hashmap_list_t) : 't hashmap_list_t result = + hashmap_hash_map_remove_from_list_loop_back key ls +’ + +val hashmap_hash_map_remove_fwd_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *) + hashmap_hash_map_remove_fwd + (self : 't hashmap_hash_map_t) (key : usize) : 't option result = + do + hash <- hashmap_hash_key_fwd key; + let i = vec_len self.hashmap_hash_map_slots in + do + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + x <- hashmap_hash_map_remove_from_list_fwd key l; + (case x of + | NONE => Return NONE + | SOME x0 => + do + _ <- usize_sub self.hashmap_hash_map_num_entries (int_to_usize 1); + Return (SOME x0) + od) + od + od +’ + +val hashmap_hash_map_remove_back_def = Define ‘ + (** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *) + hashmap_hash_map_remove_back + (self : 't hashmap_hash_map_t) (key : usize) : + 't hashmap_hash_map_t result + = + do + hash <- hashmap_hash_key_fwd key; + let i = vec_len self.hashmap_hash_map_slots in + do + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + x <- hashmap_hash_map_remove_from_list_fwd key l; + (case x of + | NONE => + do + l0 <- hashmap_hash_map_remove_from_list_back key l; + v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0; + Return (self with <| hashmap_hash_map_slots := v |>) + od + | SOME x0 => + do + i0 <- usize_sub self.hashmap_hash_map_num_entries (int_to_usize 1); + l0 <- hashmap_hash_map_remove_from_list_back key l; + v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0; + Return + (self + with + <| + hashmap_hash_map_num_entries := i0; hashmap_hash_map_slots := v + |>) + od) + od + od +’ + +val hashmap_test1_fwd_def = Define ‘ + (** [hashmap_main::hashmap::test1]: forward function *) + hashmap_test1_fwd : unit result = + do + hm <- hashmap_hash_map_new_fwd; + hm0 <- + hashmap_hash_map_insert_fwd_back hm (int_to_usize 0) (int_to_u64 42); + hm1 <- + hashmap_hash_map_insert_fwd_back hm0 (int_to_usize 128) (int_to_u64 18); + hm2 <- + hashmap_hash_map_insert_fwd_back hm1 (int_to_usize 1024) (int_to_u64 138); + hm3 <- + hashmap_hash_map_insert_fwd_back hm2 (int_to_usize 1056) (int_to_u64 256); + i <- hashmap_hash_map_get_fwd hm3 (int_to_usize 128); + if ~ (i = int_to_u64 18) + then Fail Failure + else ( + do + hm4 <- + hashmap_hash_map_get_mut_back hm3 (int_to_usize 1024) (int_to_u64 56); + i0 <- hashmap_hash_map_get_fwd hm4 (int_to_usize 1024); + if ~ (i0 = int_to_u64 56) + then Fail Failure + else ( + do + x <- hashmap_hash_map_remove_fwd hm4 (int_to_usize 1024); + (case x of + | NONE => Fail Failure + | SOME x0 => + if ~ (x0 = int_to_u64 56) + then Fail Failure + else ( + do + hm5 <- hashmap_hash_map_remove_back hm4 (int_to_usize 1024); + i1 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 0); + if ~ (i1 = int_to_u64 42) + then Fail Failure + else ( + do + i2 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 128); + if ~ (i2 = int_to_u64 18) + then Fail Failure + else ( + do + i3 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 1056); + if ~ (i3 = int_to_u64 256) then Fail Failure else Return () + od) + od) + od)) + od) + od) + od +’ + +(** Unit test for [hashmap_main::hashmap::test1] *) +val _ = assert_return (“hashmap_test1_fwd”) + +val insert_on_disk_fwd_def = Define ‘ + (** [hashmap_main::insert_on_disk]: forward function *) + insert_on_disk_fwd + (key : usize) (value : u64) (st : state) : (state # unit) result = + do + (st0, hm) <- hashmap_utils_deserialize_fwd st; + hm0 <- hashmap_hash_map_insert_fwd_back hm key value; + (st1, _) <- hashmap_utils_serialize_fwd hm0 st0; + Return (st1, ()) + od +’ + +val main_fwd_def = Define ‘ + (** [hashmap_main::main]: forward function *) + main_fwd : unit result = + Return () +’ + +(** Unit test for [hashmap_main::main] *) +val _ = assert_return (“main_fwd”) + +val _ = export_theory () diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig new file mode 100644 index 00000000..d4e43d9a --- /dev/null +++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig @@ -0,0 +1,598 @@ +signature hashmapMain_FunsTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val hashmap_hash_key_fwd_def : thm + val hashmap_hash_map_allocate_slots_fwd_def : thm + val hashmap_hash_map_allocate_slots_loop_fwd_def : thm + val hashmap_hash_map_clear_fwd_back_def : thm + val hashmap_hash_map_clear_loop_fwd_back_def : thm + val hashmap_hash_map_contains_key_fwd_def : thm + val hashmap_hash_map_contains_key_in_list_fwd_def : thm + val hashmap_hash_map_contains_key_in_list_loop_fwd_def : thm + val hashmap_hash_map_get_fwd_def : thm + val hashmap_hash_map_get_in_list_fwd_def : thm + val hashmap_hash_map_get_in_list_loop_fwd_def : thm + val hashmap_hash_map_get_mut_back_def : thm + val hashmap_hash_map_get_mut_fwd_def : thm + val hashmap_hash_map_get_mut_in_list_back_def : thm + val hashmap_hash_map_get_mut_in_list_fwd_def : thm + val hashmap_hash_map_get_mut_in_list_loop_back_def : thm + val hashmap_hash_map_get_mut_in_list_loop_fwd_def : thm + val hashmap_hash_map_insert_fwd_back_def : thm + val hashmap_hash_map_insert_in_list_back_def : thm + val hashmap_hash_map_insert_in_list_fwd_def : thm + val hashmap_hash_map_insert_in_list_loop_back_def : thm + val hashmap_hash_map_insert_in_list_loop_fwd_def : thm + val hashmap_hash_map_insert_no_resize_fwd_back_def : thm + val hashmap_hash_map_len_fwd_def : thm + val hashmap_hash_map_move_elements_from_list_fwd_back_def : thm + val hashmap_hash_map_move_elements_from_list_loop_fwd_back_def : thm + val hashmap_hash_map_move_elements_fwd_back_def : thm + val hashmap_hash_map_move_elements_loop_fwd_back_def : thm + val hashmap_hash_map_new_fwd_def : thm + val hashmap_hash_map_new_with_capacity_fwd_def : thm + val hashmap_hash_map_remove_back_def : thm + val hashmap_hash_map_remove_from_list_back_def : thm + val hashmap_hash_map_remove_from_list_fwd_def : thm + val hashmap_hash_map_remove_from_list_loop_back_def : thm + val hashmap_hash_map_remove_from_list_loop_fwd_def : thm + val hashmap_hash_map_remove_fwd_def : thm + val hashmap_hash_map_try_resize_fwd_back_def : thm + val hashmap_test1_fwd_def : thm + val insert_on_disk_fwd_def : thm + val main_fwd_def : thm + + val hashmapMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar +(* + [hashmapMain_Opaque] Parent theory of "hashmapMain_Funs" + + [hashmap_hash_key_fwd_def] Definition + + ⊢ ∀k. hashmap_hash_key_fwd k = Return k + + [hashmap_hash_map_allocate_slots_fwd_def] Definition + + ⊢ ∀slots n. + hashmap_hash_map_allocate_slots_fwd slots n = + hashmap_hash_map_allocate_slots_loop_fwd slots n + + [hashmap_hash_map_allocate_slots_loop_fwd_def] Definition + + ⊢ ∀slots n. + hashmap_hash_map_allocate_slots_loop_fwd slots n = + if usize_gt n (int_to_usize 0) then + do + slots0 <- vec_push_back slots HashmapListNil; + n0 <- usize_sub n (int_to_usize 1); + hashmap_hash_map_allocate_slots_loop_fwd slots0 n0 + od + else Return slots + + [hashmap_hash_map_clear_fwd_back_def] Definition + + ⊢ ∀self. + hashmap_hash_map_clear_fwd_back self = + do + v <- + hashmap_hash_map_clear_loop_fwd_back + self.hashmap_hash_map_slots (int_to_usize 0); + Return + (self with + <|hashmap_hash_map_num_entries := int_to_usize 0; + hashmap_hash_map_slots := v|>) + od + + [hashmap_hash_map_clear_loop_fwd_back_def] Definition + + ⊢ ∀slots i. + hashmap_hash_map_clear_loop_fwd_back slots i = + (let + i0 = vec_len slots + in + if usize_lt i i0 then + do + i1 <- usize_add i (int_to_usize 1); + slots0 <- vec_index_mut_back slots i HashmapListNil; + hashmap_hash_map_clear_loop_fwd_back slots0 i1 + od + else Return slots) + + [hashmap_hash_map_contains_key_fwd_def] Definition + + ⊢ ∀self key. + hashmap_hash_map_contains_key_fwd self key = + do + hash <- hashmap_hash_key_fwd key; + i <<- vec_len self.hashmap_hash_map_slots; + hash_mod <- usize_rem hash i; + l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod; + hashmap_hash_map_contains_key_in_list_fwd key l + od + + [hashmap_hash_map_contains_key_in_list_fwd_def] Definition + + ⊢ ∀key ls. + hashmap_hash_map_contains_key_in_list_fwd key ls = + hashmap_hash_map_contains_key_in_list_loop_fwd key ls + + [hashmap_hash_map_contains_key_in_list_loop_fwd_def] Definition + + ⊢ ∀key ls. + hashmap_hash_map_contains_key_in_list_loop_fwd key ls = + case ls of + HashmapListCons ckey t tl => + if ckey = key then Return T + else hashmap_hash_map_contains_key_in_list_loop_fwd key tl + | HashmapListNil => Return F + + [hashmap_hash_map_get_fwd_def] Definition + + ⊢ ∀self key. + hashmap_hash_map_get_fwd self key = + do + hash <- hashmap_hash_key_fwd key; + i <<- vec_len self.hashmap_hash_map_slots; + hash_mod <- usize_rem hash i; + l <- vec_index_fwd self.hashmap_hash_map_slots hash_mod; + hashmap_hash_map_get_in_list_fwd key l + od + + [hashmap_hash_map_get_in_list_fwd_def] Definition + + ⊢ ∀key ls. + hashmap_hash_map_get_in_list_fwd key ls = + hashmap_hash_map_get_in_list_loop_fwd key ls + + [hashmap_hash_map_get_in_list_loop_fwd_def] Definition + + ⊢ ∀key ls. + hashmap_hash_map_get_in_list_loop_fwd key ls = + case ls of + HashmapListCons ckey cvalue tl => + if ckey = key then Return cvalue + else hashmap_hash_map_get_in_list_loop_fwd key tl + | HashmapListNil => Fail Failure + + [hashmap_hash_map_get_mut_back_def] Definition + + ⊢ ∀self key ret. + hashmap_hash_map_get_mut_back self key ret = + do + hash <- hashmap_hash_key_fwd key; + i <<- vec_len self.hashmap_hash_map_slots; + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + l0 <- hashmap_hash_map_get_mut_in_list_back l key ret; + v <- vec_index_mut_back self.hashmap_hash_map_slots hash_mod l0; + Return (self with hashmap_hash_map_slots := v) + od + + [hashmap_hash_map_get_mut_fwd_def] Definition + + ⊢ ∀self key. + hashmap_hash_map_get_mut_fwd self key = + do + hash <- hashmap_hash_key_fwd key; + i <<- vec_len self.hashmap_hash_map_slots; + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + hashmap_hash_map_get_mut_in_list_fwd l key + od + + [hashmap_hash_map_get_mut_in_list_back_def] Definition + + ⊢ ∀ls key ret. + hashmap_hash_map_get_mut_in_list_back ls key ret = + hashmap_hash_map_get_mut_in_list_loop_back ls key ret + + [hashmap_hash_map_get_mut_in_list_fwd_def] Definition + + ⊢ ∀ls key. + hashmap_hash_map_get_mut_in_list_fwd ls key = + hashmap_hash_map_get_mut_in_list_loop_fwd ls key + + [hashmap_hash_map_get_mut_in_list_loop_back_def] Definition + + ⊢ ∀ls key ret. + hashmap_hash_map_get_mut_in_list_loop_back ls key ret = + case ls of + HashmapListCons ckey cvalue tl => + if ckey = key then Return (HashmapListCons ckey ret tl) + else + do + tl0 <- + hashmap_hash_map_get_mut_in_list_loop_back tl key ret; + Return (HashmapListCons ckey cvalue tl0) + od + | HashmapListNil => Fail Failure + + [hashmap_hash_map_get_mut_in_list_loop_fwd_def] Definition + + ⊢ ∀ls key. + hashmap_hash_map_get_mut_in_list_loop_fwd ls key = + case ls of + HashmapListCons ckey cvalue tl => + if ckey = key then Return cvalue + else hashmap_hash_map_get_mut_in_list_loop_fwd tl key + | HashmapListNil => Fail Failure + + [hashmap_hash_map_insert_fwd_back_def] Definition + + ⊢ ∀self key value. + hashmap_hash_map_insert_fwd_back self key value = + do + self0 <- + hashmap_hash_map_insert_no_resize_fwd_back self key value; + i <- hashmap_hash_map_len_fwd self0; + if usize_gt i self0.hashmap_hash_map_max_load then + hashmap_hash_map_try_resize_fwd_back self0 + else Return self0 + od + + [hashmap_hash_map_insert_in_list_back_def] Definition + + ⊢ ∀key value ls. + hashmap_hash_map_insert_in_list_back key value ls = + hashmap_hash_map_insert_in_list_loop_back key value ls + + [hashmap_hash_map_insert_in_list_fwd_def] Definition + + ⊢ ∀key value ls. + hashmap_hash_map_insert_in_list_fwd key value ls = + hashmap_hash_map_insert_in_list_loop_fwd key value ls + + [hashmap_hash_map_insert_in_list_loop_back_def] Definition + + ⊢ ∀key value ls. + hashmap_hash_map_insert_in_list_loop_back key value ls = + case ls of + HashmapListCons ckey cvalue tl => + if ckey = key then Return (HashmapListCons ckey value tl) + else + do + tl0 <- + hashmap_hash_map_insert_in_list_loop_back key value tl; + Return (HashmapListCons ckey cvalue tl0) + od + | HashmapListNil => + (let + l = HashmapListNil + in + Return (HashmapListCons key value l)) + + [hashmap_hash_map_insert_in_list_loop_fwd_def] Definition + + ⊢ ∀key value ls. + hashmap_hash_map_insert_in_list_loop_fwd key value ls = + case ls of + HashmapListCons ckey cvalue tl => + if ckey = key then Return F + else hashmap_hash_map_insert_in_list_loop_fwd key value tl + | HashmapListNil => Return T + + [hashmap_hash_map_insert_no_resize_fwd_back_def] Definition + + ⊢ ∀self key value. + hashmap_hash_map_insert_no_resize_fwd_back self key value = + do + hash <- hashmap_hash_key_fwd key; + i <<- vec_len self.hashmap_hash_map_slots; + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + inserted <- hashmap_hash_map_insert_in_list_fwd key value l; + if inserted then + do + i0 <- + usize_add self.hashmap_hash_map_num_entries + (int_to_usize 1); + l0 <- hashmap_hash_map_insert_in_list_back key value l; + v <- + vec_index_mut_back self.hashmap_hash_map_slots hash_mod + l0; + Return + (self with + <|hashmap_hash_map_num_entries := i0; + hashmap_hash_map_slots := v|>) + od + else + do + l0 <- hashmap_hash_map_insert_in_list_back key value l; + v <- + vec_index_mut_back self.hashmap_hash_map_slots hash_mod + l0; + Return (self with hashmap_hash_map_slots := v) + od + od + + [hashmap_hash_map_len_fwd_def] Definition + + ⊢ ∀self. + hashmap_hash_map_len_fwd self = + Return self.hashmap_hash_map_num_entries + + [hashmap_hash_map_move_elements_from_list_fwd_back_def] Definition + + ⊢ ∀ntable ls. + hashmap_hash_map_move_elements_from_list_fwd_back ntable ls = + hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls + + [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] Definition + + ⊢ ∀ntable ls. + hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls = + case ls of + HashmapListCons k v tl => + do + ntable0 <- + hashmap_hash_map_insert_no_resize_fwd_back ntable k v; + hashmap_hash_map_move_elements_from_list_loop_fwd_back + ntable0 tl + od + | HashmapListNil => Return ntable + + [hashmap_hash_map_move_elements_fwd_back_def] Definition + + ⊢ ∀ntable slots i. + hashmap_hash_map_move_elements_fwd_back ntable slots i = + hashmap_hash_map_move_elements_loop_fwd_back ntable slots i + + [hashmap_hash_map_move_elements_loop_fwd_back_def] Definition + + ⊢ ∀ntable slots i. + hashmap_hash_map_move_elements_loop_fwd_back ntable slots i = + (let + i0 = vec_len slots + in + if usize_lt i i0 then + do + l <- vec_index_mut_fwd slots i; + ls <<- mem_replace_fwd l HashmapListNil; + ntable0 <- + hashmap_hash_map_move_elements_from_list_fwd_back ntable + ls; + i1 <- usize_add i (int_to_usize 1); + l0 <<- mem_replace_back l HashmapListNil; + slots0 <- vec_index_mut_back slots i l0; + hashmap_hash_map_move_elements_loop_fwd_back ntable0 + slots0 i1 + od + else Return (ntable,slots)) + + [hashmap_hash_map_new_fwd_def] Definition + + ⊢ hashmap_hash_map_new_fwd = + hashmap_hash_map_new_with_capacity_fwd (int_to_usize 32) + (int_to_usize 4) (int_to_usize 5) + + [hashmap_hash_map_new_with_capacity_fwd_def] Definition + + ⊢ ∀capacity max_load_dividend max_load_divisor. + hashmap_hash_map_new_with_capacity_fwd capacity max_load_dividend + max_load_divisor = + (let + v = vec_new + in + do + slots <- hashmap_hash_map_allocate_slots_fwd v capacity; + i <- usize_mul capacity max_load_dividend; + i0 <- usize_div i max_load_divisor; + Return + <|hashmap_hash_map_num_entries := int_to_usize 0; + hashmap_hash_map_max_load_factor := + (max_load_dividend,max_load_divisor); + hashmap_hash_map_max_load := i0; + hashmap_hash_map_slots := slots|> + od) + + [hashmap_hash_map_remove_back_def] Definition + + ⊢ ∀self key. + hashmap_hash_map_remove_back self key = + do + hash <- hashmap_hash_key_fwd key; + i <<- vec_len self.hashmap_hash_map_slots; + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + x <- hashmap_hash_map_remove_from_list_fwd key l; + case x of + NONE => + do + l0 <- hashmap_hash_map_remove_from_list_back key l; + v <- + vec_index_mut_back self.hashmap_hash_map_slots hash_mod + l0; + Return (self with hashmap_hash_map_slots := v) + od + | SOME x0 => + do + i0 <- + usize_sub self.hashmap_hash_map_num_entries + (int_to_usize 1); + l0 <- hashmap_hash_map_remove_from_list_back key l; + v <- + vec_index_mut_back self.hashmap_hash_map_slots hash_mod + l0; + Return + (self with + <|hashmap_hash_map_num_entries := i0; + hashmap_hash_map_slots := v|>) + od + od + + [hashmap_hash_map_remove_from_list_back_def] Definition + + ⊢ ∀key ls. + hashmap_hash_map_remove_from_list_back key ls = + hashmap_hash_map_remove_from_list_loop_back key ls + + [hashmap_hash_map_remove_from_list_fwd_def] Definition + + ⊢ ∀key ls. + hashmap_hash_map_remove_from_list_fwd key ls = + hashmap_hash_map_remove_from_list_loop_fwd key ls + + [hashmap_hash_map_remove_from_list_loop_back_def] Definition + + ⊢ ∀key ls. + hashmap_hash_map_remove_from_list_loop_back key ls = + case ls of + HashmapListCons ckey t tl => + if ckey = key then + (let + mv_ls = + mem_replace_fwd (HashmapListCons ckey t tl) + HashmapListNil + in + case mv_ls of + HashmapListCons i cvalue tl0 => Return tl0 + | HashmapListNil => Fail Failure) + else + do + tl0 <- hashmap_hash_map_remove_from_list_loop_back key tl; + Return (HashmapListCons ckey t tl0) + od + | HashmapListNil => Return HashmapListNil + + [hashmap_hash_map_remove_from_list_loop_fwd_def] Definition + + ⊢ ∀key ls. + hashmap_hash_map_remove_from_list_loop_fwd key ls = + case ls of + HashmapListCons ckey t tl => + if ckey = key then + (let + mv_ls = + mem_replace_fwd (HashmapListCons ckey t tl) + HashmapListNil + in + case mv_ls of + HashmapListCons i cvalue tl0 => Return (SOME cvalue) + | HashmapListNil => Fail Failure) + else hashmap_hash_map_remove_from_list_loop_fwd key tl + | HashmapListNil => Return NONE + + [hashmap_hash_map_remove_fwd_def] Definition + + ⊢ ∀self key. + hashmap_hash_map_remove_fwd self key = + do + hash <- hashmap_hash_key_fwd key; + i <<- vec_len self.hashmap_hash_map_slots; + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd self.hashmap_hash_map_slots hash_mod; + x <- hashmap_hash_map_remove_from_list_fwd key l; + case x of + NONE => Return NONE + | SOME x0 => + monad_ignore_bind + (usize_sub self.hashmap_hash_map_num_entries + (int_to_usize 1)) (Return (SOME x0)) + od + + [hashmap_hash_map_try_resize_fwd_back_def] Definition + + ⊢ ∀self. + hashmap_hash_map_try_resize_fwd_back self = + do + max_usize <- mk_usize (u32_to_int core_u32_max); + capacity <<- vec_len self.hashmap_hash_map_slots; + n1 <- usize_div max_usize (int_to_usize 2); + (i,i0) <<- self.hashmap_hash_map_max_load_factor; + i1 <- usize_div n1 i; + if usize_le capacity i1 then + do + i2 <- usize_mul capacity (int_to_usize 2); + ntable <- hashmap_hash_map_new_with_capacity_fwd i2 i i0; + (ntable0,_) <- + hashmap_hash_map_move_elements_fwd_back ntable + self.hashmap_hash_map_slots (int_to_usize 0); + Return + (ntable0 with + <|hashmap_hash_map_num_entries := + self.hashmap_hash_map_num_entries; + hashmap_hash_map_max_load_factor := (i,i0)|>) + od + else + Return (self with hashmap_hash_map_max_load_factor := (i,i0)) + od + + [hashmap_test1_fwd_def] Definition + + ⊢ hashmap_test1_fwd = + do + hm <- hashmap_hash_map_new_fwd; + hm0 <- + hashmap_hash_map_insert_fwd_back hm (int_to_usize 0) + (int_to_u64 42); + hm1 <- + hashmap_hash_map_insert_fwd_back hm0 (int_to_usize 128) + (int_to_u64 18); + hm2 <- + hashmap_hash_map_insert_fwd_back hm1 (int_to_usize 1024) + (int_to_u64 138); + hm3 <- + hashmap_hash_map_insert_fwd_back hm2 (int_to_usize 1056) + (int_to_u64 256); + i <- hashmap_hash_map_get_fwd hm3 (int_to_usize 128); + if i ≠ int_to_u64 18 then Fail Failure + else + do + hm4 <- + hashmap_hash_map_get_mut_back hm3 (int_to_usize 1024) + (int_to_u64 56); + i0 <- hashmap_hash_map_get_fwd hm4 (int_to_usize 1024); + if i0 ≠ int_to_u64 56 then Fail Failure + else + do + x <- hashmap_hash_map_remove_fwd hm4 (int_to_usize 1024); + case x of + NONE => Fail Failure + | SOME x0 => + if x0 ≠ int_to_u64 56 then Fail Failure + else + do + hm5 <- + hashmap_hash_map_remove_back hm4 + (int_to_usize 1024); + i1 <- hashmap_hash_map_get_fwd hm5 (int_to_usize 0); + if i1 ≠ int_to_u64 42 then Fail Failure + else + do + i2 <- + hashmap_hash_map_get_fwd hm5 + (int_to_usize 128); + if i2 ≠ int_to_u64 18 then Fail Failure + else + do + i3 <- + hashmap_hash_map_get_fwd hm5 + (int_to_usize 1056); + if i3 ≠ int_to_u64 256 then Fail Failure + else Return () + od + od + od + od + od + od + + [insert_on_disk_fwd_def] Definition + + ⊢ ∀key value st. + insert_on_disk_fwd key value st = + do + (st0,hm) <- hashmap_utils_deserialize_fwd st; + hm0 <- hashmap_hash_map_insert_fwd_back hm key value; + (st1,_) <- hashmap_utils_serialize_fwd hm0 st0; + Return (st1,()) + od + + [main_fwd_def] Definition + + ⊢ main_fwd = Return () + + +*) +end diff --git a/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml new file mode 100644 index 00000000..f7221d92 --- /dev/null +++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: external function declarations *) +open primitivesLib divDefLib +open hashmapMain_TypesTheory + +val _ = new_theory "hashmapMain_Opaque" + + +(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd", + “:state -> (state # u64 hashmap_hash_map_t) result”) + +(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd", + “:u64 hashmap_hash_map_t -> state -> (state # unit) result”) + +val _ = export_theory () diff --git a/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig b/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig new file mode 100644 index 00000000..f7373609 --- /dev/null +++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig @@ -0,0 +1,11 @@ +signature hashmapMain_OpaqueTheory = +sig + type thm = Thm.thm + + val hashmapMain_Opaque_grammars : type_grammar.grammar * term_grammar.grammar +(* + [hashmapMain_Types] Parent theory of "hashmapMain_Opaque" + + +*) +end diff --git a/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml b/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml new file mode 100644 index 00000000..3f8ca9b9 --- /dev/null +++ b/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml @@ -0,0 +1,27 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: type definitions *) +open primitivesLib divDefLib + +val _ = new_theory "hashmapMain_Types" + + +Datatype: + (** [hashmap_main::hashmap::List] *) + hashmap_list_t = | HashmapListCons usize 't hashmap_list_t | HashmapListNil +End + +Datatype: + (** [hashmap_main::hashmap::HashMap] *) + hashmap_hash_map_t = + <| + hashmap_hash_map_num_entries : usize; + hashmap_hash_map_max_load_factor : (usize # usize); + hashmap_hash_map_max_load : usize; + hashmap_hash_map_slots : 't hashmap_list_t vec; + |> +End + +(** The state type used in the state-error monad *) +val _ = new_type ("state", 0) + +val _ = export_theory () diff --git a/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig b/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig new file mode 100644 index 00000000..a3e770ea --- /dev/null +++ b/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig @@ -0,0 +1,568 @@ +signature hashmapMain_TypesTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val hashmap_hash_map_t_TY_DEF : thm + val hashmap_hash_map_t_case_def : thm + val hashmap_hash_map_t_hashmap_hash_map_max_load : thm + val hashmap_hash_map_t_hashmap_hash_map_max_load_factor : thm + val hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd : thm + val hashmap_hash_map_t_hashmap_hash_map_max_load_fupd : thm + val hashmap_hash_map_t_hashmap_hash_map_num_entries : thm + val hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd : thm + val hashmap_hash_map_t_hashmap_hash_map_slots : thm + val hashmap_hash_map_t_hashmap_hash_map_slots_fupd : thm + val hashmap_hash_map_t_size_def : thm + val hashmap_list_t_TY_DEF : thm + val hashmap_list_t_case_def : thm + val hashmap_list_t_size_def : thm + + (* Theorems *) + val EXISTS_hashmap_hash_map_t : thm + val FORALL_hashmap_hash_map_t : thm + val datatype_hashmap_hash_map_t : thm + val datatype_hashmap_list_t : thm + val hashmap_hash_map_t_11 : thm + val hashmap_hash_map_t_Axiom : thm + val hashmap_hash_map_t_accessors : thm + val hashmap_hash_map_t_accfupds : thm + val hashmap_hash_map_t_case_cong : thm + val hashmap_hash_map_t_case_eq : thm + val hashmap_hash_map_t_component_equality : thm + val hashmap_hash_map_t_fn_updates : thm + val hashmap_hash_map_t_fupdcanon : thm + val hashmap_hash_map_t_fupdcanon_comp : thm + val hashmap_hash_map_t_fupdfupds : thm + val hashmap_hash_map_t_fupdfupds_comp : thm + val hashmap_hash_map_t_induction : thm + val hashmap_hash_map_t_literal_11 : thm + val hashmap_hash_map_t_literal_nchotomy : thm + val hashmap_hash_map_t_nchotomy : thm + val hashmap_hash_map_t_updates_eq_literal : thm + val hashmap_list_t_11 : thm + val hashmap_list_t_Axiom : thm + val hashmap_list_t_case_cong : thm + val hashmap_list_t_case_eq : thm + val hashmap_list_t_distinct : thm + val hashmap_list_t_induction : thm + val hashmap_list_t_nchotomy : thm + + val hashmapMain_Types_grammars : type_grammar.grammar * term_grammar.grammar +(* + [divDef] Parent theory of "hashmapMain_Types" + + [hashmap_hash_map_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('hashmap_hash_map_t'). + (∀a0'. + (∃a0 a1 a2 a3. + a0' = + (λa0 a1 a2 a3. + ind_type$CONSTR 0 (a0,a1,a2,a3) + (λn. ind_type$BOTTOM)) a0 a1 a2 a3) ⇒ + $var$('hashmap_hash_map_t') a0') ⇒ + $var$('hashmap_hash_map_t') a0') rep + + [hashmap_hash_map_t_case_def] Definition + + ⊢ ∀a0 a1 a2 a3 f. + hashmap_hash_map_t_CASE (hashmap_hash_map_t a0 a1 a2 a3) f = + f a0 a1 a2 a3 + + [hashmap_hash_map_t_hashmap_hash_map_max_load] Definition + + ⊢ ∀u p u0 v. + (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load = u0 + + [hashmap_hash_map_t_hashmap_hash_map_max_load_factor] Definition + + ⊢ ∀u p u0 v. + (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load_factor = + p + + [hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd] Definition + + ⊢ ∀f u p u0 v. + hashmap_hash_map_t u p u0 v with + hashmap_hash_map_max_load_factor updated_by f = + hashmap_hash_map_t u (f p) u0 v + + [hashmap_hash_map_t_hashmap_hash_map_max_load_fupd] Definition + + ⊢ ∀f u p u0 v. + hashmap_hash_map_t u p u0 v with + hashmap_hash_map_max_load updated_by f = + hashmap_hash_map_t u p (f u0) v + + [hashmap_hash_map_t_hashmap_hash_map_num_entries] Definition + + ⊢ ∀u p u0 v. + (hashmap_hash_map_t u p u0 v).hashmap_hash_map_num_entries = u + + [hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd] Definition + + ⊢ ∀f u p u0 v. + hashmap_hash_map_t u p u0 v with + hashmap_hash_map_num_entries updated_by f = + hashmap_hash_map_t (f u) p u0 v + + [hashmap_hash_map_t_hashmap_hash_map_slots] Definition + + ⊢ ∀u p u0 v. (hashmap_hash_map_t u p u0 v).hashmap_hash_map_slots = v + + [hashmap_hash_map_t_hashmap_hash_map_slots_fupd] Definition + + ⊢ ∀f u p u0 v. + hashmap_hash_map_t u p u0 v with + hashmap_hash_map_slots updated_by f = + hashmap_hash_map_t u p u0 (f v) + + [hashmap_hash_map_t_size_def] Definition + + ⊢ ∀f a0 a1 a2 a3. + hashmap_hash_map_t_size f (hashmap_hash_map_t a0 a1 a2 a3) = + 1 + pair_size (λv. 0) (λv. 0) a1 + + [hashmap_list_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('hashmap_list_t'). + (∀a0'. + (∃a0 a1 a2. + a0' = + (λa0 a1 a2. + ind_type$CONSTR 0 (a0,a1) + (ind_type$FCONS a2 (λn. ind_type$BOTTOM))) + a0 a1 a2 ∧ $var$('hashmap_list_t') a2) ∨ + a0' = + ind_type$CONSTR (SUC 0) (ARB,ARB) + (λn. ind_type$BOTTOM) ⇒ + $var$('hashmap_list_t') a0') ⇒ + $var$('hashmap_list_t') a0') rep + + [hashmap_list_t_case_def] Definition + + ⊢ (∀a0 a1 a2 f v. + hashmap_list_t_CASE (HashmapListCons a0 a1 a2) f v = f a0 a1 a2) ∧ + ∀f v. hashmap_list_t_CASE HashmapListNil f v = v + + [hashmap_list_t_size_def] Definition + + ⊢ (∀f a0 a1 a2. + hashmap_list_t_size f (HashmapListCons a0 a1 a2) = + 1 + (f a1 + hashmap_list_t_size f a2)) ∧ + ∀f. hashmap_list_t_size f HashmapListNil = 0 + + [EXISTS_hashmap_hash_map_t] Theorem + + ⊢ ∀P. (∃h. P h) ⇔ + ∃u0 p u v. + P + <|hashmap_hash_map_num_entries := u0; + hashmap_hash_map_max_load_factor := p; + hashmap_hash_map_max_load := u; + hashmap_hash_map_slots := v|> + + [FORALL_hashmap_hash_map_t] Theorem + + ⊢ ∀P. (∀h. P h) ⇔ + ∀u0 p u v. + P + <|hashmap_hash_map_num_entries := u0; + hashmap_hash_map_max_load_factor := p; + hashmap_hash_map_max_load := u; + hashmap_hash_map_slots := v|> + + [datatype_hashmap_hash_map_t] Theorem + + ⊢ DATATYPE + (record hashmap_hash_map_t hashmap_hash_map_num_entries + hashmap_hash_map_max_load_factor hashmap_hash_map_max_load + hashmap_hash_map_slots) + + [datatype_hashmap_list_t] Theorem + + ⊢ DATATYPE (hashmap_list_t HashmapListCons HashmapListNil) + + [hashmap_hash_map_t_11] Theorem + + ⊢ ∀a0 a1 a2 a3 a0' a1' a2' a3'. + hashmap_hash_map_t a0 a1 a2 a3 = + hashmap_hash_map_t a0' a1' a2' a3' ⇔ + a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3' + + [hashmap_hash_map_t_Axiom] Theorem + + ⊢ ∀f. ∃fn. ∀a0 a1 a2 a3. + fn (hashmap_hash_map_t a0 a1 a2 a3) = f a0 a1 a2 a3 + + [hashmap_hash_map_t_accessors] Theorem + + ⊢ (∀u p u0 v. + (hashmap_hash_map_t u p u0 v).hashmap_hash_map_num_entries = u) ∧ + (∀u p u0 v. + (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load_factor = + p) ∧ + (∀u p u0 v. + (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load = u0) ∧ + ∀u p u0 v. (hashmap_hash_map_t u p u0 v).hashmap_hash_map_slots = v + + [hashmap_hash_map_t_accfupds] Theorem + + ⊢ (∀h f. + (h with hashmap_hash_map_max_load_factor updated_by f). + hashmap_hash_map_num_entries = + h.hashmap_hash_map_num_entries) ∧ + (∀h f. + (h with hashmap_hash_map_max_load updated_by f). + hashmap_hash_map_num_entries = + h.hashmap_hash_map_num_entries) ∧ + (∀h f. + (h with hashmap_hash_map_slots updated_by f). + hashmap_hash_map_num_entries = + h.hashmap_hash_map_num_entries) ∧ + (∀h f. + (h with hashmap_hash_map_num_entries updated_by f). + hashmap_hash_map_max_load_factor = + h.hashmap_hash_map_max_load_factor) ∧ + (∀h f. + (h with hashmap_hash_map_max_load updated_by f). + hashmap_hash_map_max_load_factor = + h.hashmap_hash_map_max_load_factor) ∧ + (∀h f. + (h with hashmap_hash_map_slots updated_by f). + hashmap_hash_map_max_load_factor = + h.hashmap_hash_map_max_load_factor) ∧ + (∀h f. + (h with hashmap_hash_map_num_entries updated_by f). + hashmap_hash_map_max_load = + h.hashmap_hash_map_max_load) ∧ + (∀h f. + (h with hashmap_hash_map_max_load_factor updated_by f). + hashmap_hash_map_max_load = + h.hashmap_hash_map_max_load) ∧ + (∀h f. + (h with hashmap_hash_map_slots updated_by f). + hashmap_hash_map_max_load = + h.hashmap_hash_map_max_load) ∧ + (∀h f. + (h with hashmap_hash_map_num_entries updated_by f). + hashmap_hash_map_slots = + h.hashmap_hash_map_slots) ∧ + (∀h f. + (h with hashmap_hash_map_max_load_factor updated_by f). + hashmap_hash_map_slots = + h.hashmap_hash_map_slots) ∧ + (∀h f. + (h with hashmap_hash_map_max_load updated_by f). + hashmap_hash_map_slots = + h.hashmap_hash_map_slots) ∧ + (∀h f. + (h with hashmap_hash_map_num_entries updated_by f). + hashmap_hash_map_num_entries = + f h.hashmap_hash_map_num_entries) ∧ + (∀h f. + (h with hashmap_hash_map_max_load_factor updated_by f). + hashmap_hash_map_max_load_factor = + f h.hashmap_hash_map_max_load_factor) ∧ + (∀h f. + (h with hashmap_hash_map_max_load updated_by f). + hashmap_hash_map_max_load = + f h.hashmap_hash_map_max_load) ∧ + ∀h f. + (h with hashmap_hash_map_slots updated_by f). + hashmap_hash_map_slots = + f h.hashmap_hash_map_slots + + [hashmap_hash_map_t_case_cong] Theorem + + ⊢ ∀M M' f. + M = M' ∧ + (∀a0 a1 a2 a3. + M' = hashmap_hash_map_t a0 a1 a2 a3 ⇒ + f a0 a1 a2 a3 = f' a0 a1 a2 a3) ⇒ + hashmap_hash_map_t_CASE M f = hashmap_hash_map_t_CASE M' f' + + [hashmap_hash_map_t_case_eq] Theorem + + ⊢ hashmap_hash_map_t_CASE x f = v ⇔ + ∃u p u0 v'. x = hashmap_hash_map_t u p u0 v' ∧ f u p u0 v' = v + + [hashmap_hash_map_t_component_equality] Theorem + + ⊢ ∀h1 h2. + h1 = h2 ⇔ + h1.hashmap_hash_map_num_entries = h2.hashmap_hash_map_num_entries ∧ + h1.hashmap_hash_map_max_load_factor = + h2.hashmap_hash_map_max_load_factor ∧ + h1.hashmap_hash_map_max_load = h2.hashmap_hash_map_max_load ∧ + h1.hashmap_hash_map_slots = h2.hashmap_hash_map_slots + + [hashmap_hash_map_t_fn_updates] Theorem + + ⊢ (∀f u p u0 v. + hashmap_hash_map_t u p u0 v with + hashmap_hash_map_num_entries updated_by f = + hashmap_hash_map_t (f u) p u0 v) ∧ + (∀f u p u0 v. + hashmap_hash_map_t u p u0 v with + hashmap_hash_map_max_load_factor updated_by f = + hashmap_hash_map_t u (f p) u0 v) ∧ + (∀f u p u0 v. + hashmap_hash_map_t u p u0 v with + hashmap_hash_map_max_load updated_by f = + hashmap_hash_map_t u p (f u0) v) ∧ + ∀f u p u0 v. + hashmap_hash_map_t u p u0 v with + hashmap_hash_map_slots updated_by f = + hashmap_hash_map_t u p u0 (f v) + + [hashmap_hash_map_t_fupdcanon] Theorem + + ⊢ (∀h g f. + h with + <|hashmap_hash_map_max_load_factor updated_by f; + hashmap_hash_map_num_entries updated_by g|> = + h with + <|hashmap_hash_map_num_entries updated_by g; + hashmap_hash_map_max_load_factor updated_by f|>) ∧ + (∀h g f. + h with + <|hashmap_hash_map_max_load updated_by f; + hashmap_hash_map_num_entries updated_by g|> = + h with + <|hashmap_hash_map_num_entries updated_by g; + hashmap_hash_map_max_load updated_by f|>) ∧ + (∀h g f. + h with + <|hashmap_hash_map_max_load updated_by f; + hashmap_hash_map_max_load_factor updated_by g|> = + h with + <|hashmap_hash_map_max_load_factor updated_by g; + hashmap_hash_map_max_load updated_by f|>) ∧ + (∀h g f. + h with + <|hashmap_hash_map_slots updated_by f; + hashmap_hash_map_num_entries updated_by g|> = + h with + <|hashmap_hash_map_num_entries updated_by g; + hashmap_hash_map_slots updated_by f|>) ∧ + (∀h g f. + h with + <|hashmap_hash_map_slots updated_by f; + hashmap_hash_map_max_load_factor updated_by g|> = + h with + <|hashmap_hash_map_max_load_factor updated_by g; + hashmap_hash_map_slots updated_by f|>) ∧ + ∀h g f. + h with + <|hashmap_hash_map_slots updated_by f; + hashmap_hash_map_max_load updated_by g|> = + h with + <|hashmap_hash_map_max_load updated_by g; + hashmap_hash_map_slots updated_by f|> + + [hashmap_hash_map_t_fupdcanon_comp] Theorem + + ⊢ ((∀g f. + hashmap_hash_map_max_load_factor_fupd f ∘ + hashmap_hash_map_num_entries_fupd g = + hashmap_hash_map_num_entries_fupd g ∘ + hashmap_hash_map_max_load_factor_fupd f) ∧ + ∀h g f. + hashmap_hash_map_max_load_factor_fupd f ∘ + hashmap_hash_map_num_entries_fupd g ∘ h = + hashmap_hash_map_num_entries_fupd g ∘ + hashmap_hash_map_max_load_factor_fupd f ∘ h) ∧ + ((∀g f. + hashmap_hash_map_max_load_fupd f ∘ + hashmap_hash_map_num_entries_fupd g = + hashmap_hash_map_num_entries_fupd g ∘ + hashmap_hash_map_max_load_fupd f) ∧ + ∀h g f. + hashmap_hash_map_max_load_fupd f ∘ + hashmap_hash_map_num_entries_fupd g ∘ h = + hashmap_hash_map_num_entries_fupd g ∘ + hashmap_hash_map_max_load_fupd f ∘ h) ∧ + ((∀g f. + hashmap_hash_map_max_load_fupd f ∘ + hashmap_hash_map_max_load_factor_fupd g = + hashmap_hash_map_max_load_factor_fupd g ∘ + hashmap_hash_map_max_load_fupd f) ∧ + ∀h g f. + hashmap_hash_map_max_load_fupd f ∘ + hashmap_hash_map_max_load_factor_fupd g ∘ h = + hashmap_hash_map_max_load_factor_fupd g ∘ + hashmap_hash_map_max_load_fupd f ∘ h) ∧ + ((∀g f. + hashmap_hash_map_slots_fupd f ∘ + hashmap_hash_map_num_entries_fupd g = + hashmap_hash_map_num_entries_fupd g ∘ + hashmap_hash_map_slots_fupd f) ∧ + ∀h g f. + hashmap_hash_map_slots_fupd f ∘ + hashmap_hash_map_num_entries_fupd g ∘ h = + hashmap_hash_map_num_entries_fupd g ∘ + hashmap_hash_map_slots_fupd f ∘ h) ∧ + ((∀g f. + hashmap_hash_map_slots_fupd f ∘ + hashmap_hash_map_max_load_factor_fupd g = + hashmap_hash_map_max_load_factor_fupd g ∘ + hashmap_hash_map_slots_fupd f) ∧ + ∀h g f. + hashmap_hash_map_slots_fupd f ∘ + hashmap_hash_map_max_load_factor_fupd g ∘ h = + hashmap_hash_map_max_load_factor_fupd g ∘ + hashmap_hash_map_slots_fupd f ∘ h) ∧ + (∀g f. + hashmap_hash_map_slots_fupd f ∘ hashmap_hash_map_max_load_fupd g = + hashmap_hash_map_max_load_fupd g ∘ hashmap_hash_map_slots_fupd f) ∧ + ∀h g f. + hashmap_hash_map_slots_fupd f ∘ + hashmap_hash_map_max_load_fupd g ∘ h = + hashmap_hash_map_max_load_fupd g ∘ + hashmap_hash_map_slots_fupd f ∘ h + + [hashmap_hash_map_t_fupdfupds] Theorem + + ⊢ (∀h g f. + h with + <|hashmap_hash_map_num_entries updated_by f; + hashmap_hash_map_num_entries updated_by g|> = + h with hashmap_hash_map_num_entries updated_by f ∘ g) ∧ + (∀h g f. + h with + <|hashmap_hash_map_max_load_factor updated_by f; + hashmap_hash_map_max_load_factor updated_by g|> = + h with hashmap_hash_map_max_load_factor updated_by f ∘ g) ∧ + (∀h g f. + h with + <|hashmap_hash_map_max_load updated_by f; + hashmap_hash_map_max_load updated_by g|> = + h with hashmap_hash_map_max_load updated_by f ∘ g) ∧ + ∀h g f. + h with + <|hashmap_hash_map_slots updated_by f; + hashmap_hash_map_slots updated_by g|> = + h with hashmap_hash_map_slots updated_by f ∘ g + + [hashmap_hash_map_t_fupdfupds_comp] Theorem + + ⊢ ((∀g f. + hashmap_hash_map_num_entries_fupd f ∘ + hashmap_hash_map_num_entries_fupd g = + hashmap_hash_map_num_entries_fupd (f ∘ g)) ∧ + ∀h g f. + hashmap_hash_map_num_entries_fupd f ∘ + hashmap_hash_map_num_entries_fupd g ∘ h = + hashmap_hash_map_num_entries_fupd (f ∘ g) ∘ h) ∧ + ((∀g f. + hashmap_hash_map_max_load_factor_fupd f ∘ + hashmap_hash_map_max_load_factor_fupd g = + hashmap_hash_map_max_load_factor_fupd (f ∘ g)) ∧ + ∀h g f. + hashmap_hash_map_max_load_factor_fupd f ∘ + hashmap_hash_map_max_load_factor_fupd g ∘ h = + hashmap_hash_map_max_load_factor_fupd (f ∘ g) ∘ h) ∧ + ((∀g f. + hashmap_hash_map_max_load_fupd f ∘ + hashmap_hash_map_max_load_fupd g = + hashmap_hash_map_max_load_fupd (f ∘ g)) ∧ + ∀h g f. + hashmap_hash_map_max_load_fupd f ∘ + hashmap_hash_map_max_load_fupd g ∘ h = + hashmap_hash_map_max_load_fupd (f ∘ g) ∘ h) ∧ + (∀g f. + hashmap_hash_map_slots_fupd f ∘ hashmap_hash_map_slots_fupd g = + hashmap_hash_map_slots_fupd (f ∘ g)) ∧ + ∀h g f. + hashmap_hash_map_slots_fupd f ∘ hashmap_hash_map_slots_fupd g ∘ h = + hashmap_hash_map_slots_fupd (f ∘ g) ∘ h + + [hashmap_hash_map_t_induction] Theorem + + ⊢ ∀P. (∀u p u0 v. P (hashmap_hash_map_t u p u0 v)) ⇒ ∀h. P h + + [hashmap_hash_map_t_literal_11] Theorem + + ⊢ ∀u01 p1 u1 v1 u02 p2 u2 v2. + <|hashmap_hash_map_num_entries := u01; + hashmap_hash_map_max_load_factor := p1; + hashmap_hash_map_max_load := u1; hashmap_hash_map_slots := v1|> = + <|hashmap_hash_map_num_entries := u02; + hashmap_hash_map_max_load_factor := p2; + hashmap_hash_map_max_load := u2; hashmap_hash_map_slots := v2|> ⇔ + u01 = u02 ∧ p1 = p2 ∧ u1 = u2 ∧ v1 = v2 + + [hashmap_hash_map_t_literal_nchotomy] Theorem + + ⊢ ∀h. ∃u0 p u v. + h = + <|hashmap_hash_map_num_entries := u0; + hashmap_hash_map_max_load_factor := p; + hashmap_hash_map_max_load := u; hashmap_hash_map_slots := v|> + + [hashmap_hash_map_t_nchotomy] Theorem + + ⊢ ∀hh. ∃u p u0 v. hh = hashmap_hash_map_t u p u0 v + + [hashmap_hash_map_t_updates_eq_literal] Theorem + + ⊢ ∀h u0 p u v. + h with + <|hashmap_hash_map_num_entries := u0; + hashmap_hash_map_max_load_factor := p; + hashmap_hash_map_max_load := u; hashmap_hash_map_slots := v|> = + <|hashmap_hash_map_num_entries := u0; + hashmap_hash_map_max_load_factor := p; + hashmap_hash_map_max_load := u; hashmap_hash_map_slots := v|> + + [hashmap_list_t_11] Theorem + + ⊢ ∀a0 a1 a2 a0' a1' a2'. + HashmapListCons a0 a1 a2 = HashmapListCons a0' a1' a2' ⇔ + a0 = a0' ∧ a1 = a1' ∧ a2 = a2' + + [hashmap_list_t_Axiom] Theorem + + ⊢ ∀f0 f1. ∃fn. + (∀a0 a1 a2. fn (HashmapListCons a0 a1 a2) = f0 a0 a1 a2 (fn a2)) ∧ + fn HashmapListNil = f1 + + [hashmap_list_t_case_cong] Theorem + + ⊢ ∀M M' f v. + M = M' ∧ + (∀a0 a1 a2. + M' = HashmapListCons a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ∧ + (M' = HashmapListNil ⇒ v = v') ⇒ + hashmap_list_t_CASE M f v = hashmap_list_t_CASE M' f' v' + + [hashmap_list_t_case_eq] Theorem + + ⊢ hashmap_list_t_CASE x f v = v' ⇔ + (∃u t h. x = HashmapListCons u t h ∧ f u t h = v') ∨ + x = HashmapListNil ∧ v = v' + + [hashmap_list_t_distinct] Theorem + + ⊢ ∀a2 a1 a0. HashmapListCons a0 a1 a2 ≠ HashmapListNil + + [hashmap_list_t_induction] Theorem + + ⊢ ∀P. (∀h. P h ⇒ ∀t u. P (HashmapListCons u t h)) ∧ P HashmapListNil ⇒ + ∀h. P h + + [hashmap_list_t_nchotomy] Theorem + + ⊢ ∀hh. (∃u t h. hh = HashmapListCons u t h) ∨ hh = HashmapListNil + + +*) +end |