From d152fec84d54aa5fb919e8c54e1351020b13ed97 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 13 Feb 2022 02:24:13 +0100 Subject: Start tracking the automatically generated/copied files for hashmap --- tests/hashmap/Hashmap.Funs.fst | 663 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 663 insertions(+) create mode 100644 tests/hashmap/Hashmap.Funs.fst (limited to 'tests/hashmap/Hashmap.Funs.fst') diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst new file mode 100644 index 00000000..3828ae98 --- /dev/null +++ b/tests/hashmap/Hashmap.Funs.fst @@ -0,0 +1,663 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap]: function definitions *) +module Hashmap.Funs +open Primitives +include Hashmap.Types +include Hashmap.Clauses + +#set-options "--z3rlimit 50 --fuel 0 --ifuel 1" + +(** [hashmap::hash_key] *) +let hash_key_fwd (k : usize) : result usize = Return k + +(** [hashmap::HashMap::allocate_slots] *) +let rec hash_map_allocate_slots_fwd + (t : Type0) (slots : vec (list_t t)) (n : usize) : + Tot (result (vec (list_t t))) + (decreases (hash_map_allocate_slots_decreases t slots n)) + = + begin match n with + | 0 -> Return slots + | _ -> + begin match vec_push_back (list_t t) slots ListNil with + | Fail -> Fail + | Return v -> + begin match usize_sub n 1 with + | Fail -> Fail + | Return i -> + begin match hash_map_allocate_slots_fwd t v i with + | Fail -> Fail + | Return v0 -> Return v0 + end + end + end + end + +(** [hashmap::HashMap::new_with_capacity] *) +let hash_map_new_with_capacity_fwd + (t : Type0) (capacity : usize) (max_load_dividend : usize) + (max_load_divisor : usize) : + result (hash_map_t t) + = + let v = vec_new (list_t t) in + begin match hash_map_allocate_slots_fwd t v capacity with + | Fail -> Fail + | Return v0 -> + begin match usize_mul capacity max_load_dividend with + | Fail -> Fail + | Return i -> + begin match usize_div i max_load_divisor with + | Fail -> Fail + | Return i0 -> + Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 v0) + end + end + end + +(** [hashmap::HashMap::new] *) +let hash_map_new_fwd (t : Type0) : result (hash_map_t t) = + begin match hash_map_new_with_capacity_fwd t 32 4 5 with + | Fail -> Fail + | Return h -> Return h + end + +(** [hashmap::HashMap::clear_slots] *) +let rec hash_map_clear_slots_fwd_back + (t : Type0) (slots : vec (list_t t)) (i : usize) : + Tot (result (vec (list_t t))) + (decreases (hash_map_clear_slots_decreases t slots i)) + = + let i0 = vec_len (list_t t) slots in + let b = i < i0 in + if b + then + begin match vec_index_mut_back (list_t t) slots i ListNil with + | Fail -> Fail + | Return v -> + begin match usize_add i 1 with + | Fail -> Fail + | Return i1 -> + begin match hash_map_clear_slots_fwd_back t v i1 with + | Fail -> Fail + | Return v0 -> Return v0 + end + end + end + else Return slots + +(** [hashmap::HashMap::clear] *) +let hash_map_clear_fwd_back + (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = + let p = self.hash_map_max_load_factor in + let i = self.hash_map_max_load in + let v = self.hash_map_slots in + begin match hash_map_clear_slots_fwd_back t v 0 with + | Fail -> Fail + | Return v0 -> let self0 = Mkhash_map_t 0 p i v0 in Return self0 + end + +(** [hashmap::HashMap::len] *) +let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize = + let i = self.hash_map_num_entries in Return i + +(** [hashmap::HashMap::insert_in_list] *) +let rec hash_map_insert_in_list_fwd + (t : Type0) (key : usize) (value : t) (ls : list_t t) : + Tot (result bool) + (decreases (hash_map_insert_in_list_decreases t key value ls)) + = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then Return false + else + begin match hash_map_insert_in_list_fwd t key value ls0 with + | Fail -> Fail + | Return b0 -> Return b0 + end + | ListNil -> Return true + end + +(** [hashmap::HashMap::insert_in_list] *) +let rec hash_map_insert_in_list_back + (t : Type0) (key : usize) (value : t) (ls : list_t t) : + Tot (result (list_t t)) + (decreases (hash_map_insert_in_list_decreases t key value ls)) + = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then let ls1 = ListCons ckey value ls0 in Return ls1 + else + begin match hash_map_insert_in_list_back t key value ls0 with + | Fail -> Fail + | Return l -> let ls1 = ListCons ckey cvalue l in Return ls1 + end + | ListNil -> let l = ListNil in let ls0 = ListCons key value l in Return ls0 + end + +(** [hashmap::HashMap::insert_no_resize] *) +let hash_map_insert_no_resize_fwd_back + (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : + result (hash_map_t t) + = + begin match hash_key_fwd key with + | Fail -> Fail + | Return i -> + let i0 = self.hash_map_num_entries in + let p = self.hash_map_max_load_factor in + let i1 = self.hash_map_max_load in + let v = self.hash_map_slots in + let i2 = vec_len (list_t t) v in + begin match usize_rem i i2 with + | Fail -> Fail + | Return hash_mod -> + begin match vec_index_mut_fwd (list_t t) v hash_mod with + | Fail -> Fail + | Return l -> + begin match hash_map_insert_in_list_fwd t key value l with + | Fail -> Fail + | Return b -> + if b + then + begin match usize_add i0 1 with + | Fail -> Fail + | Return i3 -> + begin match hash_map_insert_in_list_back t key value l with + | Fail -> Fail + | Return l0 -> + begin match vec_index_mut_back (list_t t) v hash_mod l0 with + | Fail -> Fail + | Return v0 -> + let self0 = Mkhash_map_t i3 p i1 v0 in Return self0 + end + end + end + else + begin match hash_map_insert_in_list_back t key value l with + | Fail -> Fail + | Return l0 -> + begin match vec_index_mut_back (list_t t) v hash_mod l0 with + | Fail -> Fail + | Return v0 -> + let self0 = Mkhash_map_t i0 p i1 v0 in Return self0 + end + end + end + end + end + end + +(** [hashmap::HashMap::move_elements_from_list] *) +let rec hash_map_move_elements_from_list_fwd_back + (t : Type0) (ntable : hash_map_t t) (ls : list_t t) : + Tot (result (hash_map_t t)) + (decreases (hash_map_move_elements_from_list_decreases t ntable ls)) + = + begin match ls with + | ListCons k v tl -> + begin match hash_map_insert_no_resize_fwd_back t ntable k v with + | Fail -> Fail + | Return h -> + begin match hash_map_move_elements_from_list_fwd_back t h tl with + | Fail -> Fail + | Return h0 -> Return h0 + end + end + | ListNil -> Return ntable + end + +(** [hashmap::HashMap::move_elements] *) +let rec hash_map_move_elements_fwd_back + (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) : + Tot (result ((hash_map_t t) & (vec (list_t t)))) + (decreases (hash_map_move_elements_decreases t ntable slots i)) + = + let i0 = vec_len (list_t t) slots in + let b = i < i0 in + if b + then + begin match vec_index_mut_fwd (list_t t) slots i with + | Fail -> Fail + | Return l -> + let l0 = mem_replace_fwd (list_t t) l ListNil in + begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with + | Fail -> Fail + | Return h -> + let l1 = mem_replace_back (list_t t) l ListNil in + begin match vec_index_mut_back (list_t t) slots i l1 with + | Fail -> Fail + | Return v -> + begin match usize_add i 1 with + | Fail -> Fail + | Return i1 -> + begin match hash_map_move_elements_fwd_back t h v i1 with + | Fail -> Fail + | Return (h0, v0) -> Return (h0, v0) + end + end + end + end + end + else Return (ntable, slots) + +(** [hashmap::HashMap::try_resize] *) +let hash_map_try_resize_fwd_back + (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = + let i = self.hash_map_num_entries in + let p = self.hash_map_max_load_factor in + let i0 = self.hash_map_max_load in + let v = self.hash_map_slots in + let i1 = vec_len (list_t t) v in + begin match usize_div 4294967295 2 with + | Fail -> Fail + | Return n1 -> + let (i2, i3) = p in + begin match usize_div n1 i2 with + | Fail -> Fail + | Return i4 -> + let b = i1 <= i4 in + if b + then + begin match usize_mul i1 2 with + | Fail -> Fail + | Return i5 -> + begin match hash_map_new_with_capacity_fwd t i5 i2 i3 with + | Fail -> Fail + | Return h -> + begin match hash_map_move_elements_fwd_back t h v 0 with + | Fail -> Fail + | Return (h0, v0) -> + let i6 = h0.hash_map_max_load in + let v1 = h0.hash_map_slots in + let v2 = mem_replace_back (vec (list_t t)) v0 v1 in + let self0 = Mkhash_map_t i (i2, i3) i6 v2 in + Return + self0 + end + end + end + else let self0 = Mkhash_map_t i (i2, i3) i0 v in Return self0 + end + end + +(** [hashmap::HashMap::insert] *) +let hash_map_insert_fwd_back + (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : + result (hash_map_t t) + = + begin match hash_map_insert_no_resize_fwd_back t self key value with + | Fail -> Fail + | Return h -> + begin match hash_map_len_fwd t h with + | Fail -> Fail + | Return i -> + let i0 = h.hash_map_num_entries in + let p = h.hash_map_max_load_factor in + let i1 = h.hash_map_max_load in + let v = h.hash_map_slots in + let b = i > i1 in + if b + then + begin match hash_map_try_resize_fwd_back t (Mkhash_map_t i0 p i1 v) + with + | Fail -> Fail + | Return h0 -> Return h0 + end + else let self0 = Mkhash_map_t i0 p i1 v in Return self0 + end + end + +(** [hashmap::HashMap::get_in_list] *) +let rec hash_map_get_in_list_fwd + (t : Type0) (key : usize) (ls : list_t t) : + Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls)) + = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then Return cvalue + else + begin match hash_map_get_in_list_fwd t key ls0 with + | Fail -> Fail + | Return x -> Return x + end + | ListNil -> Fail + end + +(** [hashmap::HashMap::get] *) +let hash_map_get_fwd + (t : Type0) (self : hash_map_t t) (key : usize) : result t = + begin match hash_key_fwd key with + | Fail -> Fail + | Return i -> + let v = self.hash_map_slots in + let i0 = vec_len (list_t t) v in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match vec_index_fwd (list_t t) v hash_mod with + | Fail -> Fail + | Return l -> + begin match hash_map_get_in_list_fwd t key l with + | Fail -> Fail + | Return x -> Return x + end + end + end + end + +(** [hashmap::HashMap::get_mut_in_list] *) +let rec hash_map_get_mut_in_list_fwd + (t : Type0) (key : usize) (ls : list_t t) : + Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls)) + = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then Return cvalue + else + begin match hash_map_get_mut_in_list_fwd t key ls0 with + | Fail -> Fail + | Return x -> Return x + end + | ListNil -> Fail + end + +(** [hashmap::HashMap::get_mut_in_list] *) +let rec hash_map_get_mut_in_list_back + (t : Type0) (key : usize) (ls : list_t t) (ret : t) : + Tot (result (list_t t)) + (decreases (hash_map_get_mut_in_list_decreases t key ls)) + = + begin match ls with + | ListCons ckey cvalue ls0 -> + let b = ckey = key in + if b + then let ls1 = ListCons ckey ret ls0 in Return ls1 + else + begin match hash_map_get_mut_in_list_back t key ls0 ret with + | Fail -> Fail + | Return l -> let ls1 = ListCons ckey cvalue l in Return ls1 + end + | ListNil -> Fail + end + +(** [hashmap::HashMap::get_mut] *) +let hash_map_get_mut_fwd + (t : Type0) (self : hash_map_t t) (key : usize) : result t = + begin match hash_key_fwd key with + | Fail -> Fail + | Return i -> + let v = self.hash_map_slots in + let i0 = vec_len (list_t t) v in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match vec_index_mut_fwd (list_t t) v hash_mod with + | Fail -> Fail + | Return l -> + begin match hash_map_get_mut_in_list_fwd t key l with + | Fail -> Fail + | Return x -> Return x + end + end + end + end + +(** [hashmap::HashMap::get_mut] *) +let hash_map_get_mut_back + (t : Type0) (self : hash_map_t t) (key : usize) (ret : t) : + result (hash_map_t t) + = + begin match hash_key_fwd key with + | Fail -> Fail + | Return i -> + let i0 = self.hash_map_num_entries in + let p = self.hash_map_max_load_factor in + let i1 = self.hash_map_max_load in + let v = self.hash_map_slots in + let i2 = vec_len (list_t t) v in + begin match usize_rem i i2 with + | Fail -> Fail + | Return hash_mod -> + begin match vec_index_mut_fwd (list_t t) v hash_mod with + | Fail -> Fail + | Return l -> + begin match hash_map_get_mut_in_list_back t key l ret with + | Fail -> Fail + | Return l0 -> + begin match vec_index_mut_back (list_t t) v hash_mod l0 with + | Fail -> Fail + | Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in Return self0 + end + end + end + end + end + +(** [hashmap::HashMap::remove_from_list] *) +let rec hash_map_remove_from_list_fwd + (t : Type0) (key : usize) (ls : list_t t) : + Tot (result (option t)) + (decreases (hash_map_remove_from_list_decreases t key ls)) + = + begin match ls with + | ListCons ckey x tl -> + let b = ckey = key in + if b + then + let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in + begin match mv_ls with + | ListCons i cvalue tl0 -> Return (Some cvalue) + | ListNil -> Fail + end + else + begin match hash_map_remove_from_list_fwd t key tl with + | Fail -> Fail + | Return opt -> Return opt + end + | ListNil -> Return None + end + +(** [hashmap::HashMap::remove_from_list] *) +let rec hash_map_remove_from_list_back + (t : Type0) (key : usize) (ls : list_t t) : + Tot (result (list_t t)) + (decreases (hash_map_remove_from_list_decreases t key ls)) + = + begin match ls with + | ListCons ckey x tl -> + let b = ckey = key in + if b + then + let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in + begin match mv_ls with + | ListCons i cvalue tl0 -> Return tl0 + | ListNil -> Fail + end + else + begin match hash_map_remove_from_list_back t key tl with + | Fail -> Fail + | Return l -> let ls0 = ListCons ckey x l in Return ls0 + end + | ListNil -> let ls0 = ListNil in Return ls0 + end + +(** [hashmap::HashMap::remove] *) +let hash_map_remove_fwd + (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) = + begin match hash_key_fwd key with + | Fail -> Fail + | Return i -> + let i0 = self.hash_map_num_entries in + let v = self.hash_map_slots in + let i1 = vec_len (list_t t) v in + begin match usize_rem i i1 with + | Fail -> Fail + | Return hash_mod -> + begin match vec_index_mut_fwd (list_t t) v hash_mod with + | Fail -> Fail + | Return l -> + begin match hash_map_remove_from_list_fwd t key l with + | Fail -> Fail + | Return x -> + begin match x with + | None -> Return None + | Some x0 -> + begin match usize_sub i0 1 with + | Fail -> Fail + | Return _ -> Return (Some x0) + end + end + end + end + end + end + +(** [hashmap::HashMap::remove] *) +let hash_map_remove_back + (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) = + begin match hash_key_fwd key with + | Fail -> Fail + | Return i -> + let i0 = self.hash_map_num_entries in + let p = self.hash_map_max_load_factor in + let i1 = self.hash_map_max_load in + let v = self.hash_map_slots in + let i2 = vec_len (list_t t) v in + begin match usize_rem i i2 with + | Fail -> Fail + | Return hash_mod -> + begin match vec_index_mut_fwd (list_t t) v hash_mod with + | Fail -> Fail + | Return l -> + begin match hash_map_remove_from_list_fwd t key l with + | Fail -> Fail + | Return x -> + begin match x with + | None -> + begin match hash_map_remove_from_list_back t key l with + | Fail -> Fail + | Return l0 -> + begin match vec_index_mut_back (list_t t) v hash_mod l0 with + | Fail -> Fail + | Return v0 -> + let self0 = Mkhash_map_t i0 p i1 v0 in Return self0 + end + end + | Some x0 -> + begin match usize_sub i0 1 with + | Fail -> Fail + | Return i3 -> + begin match hash_map_remove_from_list_back t key l with + | Fail -> Fail + | Return l0 -> + begin match vec_index_mut_back (list_t t) v hash_mod l0 with + | Fail -> Fail + | Return v0 -> + let self0 = Mkhash_map_t i3 p i1 v0 in Return self0 + end + end + end + end + end + end + end + end + +(** [hashmap::test1] *) +let test1_fwd : result unit = + begin match hash_map_new_fwd u64 with + | Fail -> Fail + | Return h -> + begin match hash_map_insert_fwd_back u64 h 0 42 with + | Fail -> Fail + | Return h0 -> + begin match hash_map_insert_fwd_back u64 h0 128 18 with + | Fail -> Fail + | Return h1 -> + begin match hash_map_insert_fwd_back u64 h1 1024 138 with + | Fail -> Fail + | Return h2 -> + begin match hash_map_insert_fwd_back u64 h2 1056 256 with + | Fail -> Fail + | Return h3 -> + begin match hash_map_get_fwd u64 h3 128 with + | Fail -> Fail + | Return i -> + let b = i = 18 in + let b0 = not b in + if b0 + then Fail + else + begin match hash_map_get_mut_back u64 h3 1024 56 with + | Fail -> Fail + | Return h4 -> + begin match hash_map_get_fwd u64 h4 1024 with + | Fail -> Fail + | Return i0 -> + let b1 = i0 = 56 in + let b2 = not b1 in + if b2 + then Fail + else + begin match hash_map_remove_fwd u64 h4 1024 with + | Fail -> Fail + | Return x -> + begin match x with + | None -> Fail + | Some x0 -> + let b3 = x0 = 56 in + let b4 = not b3 in + if b4 + then Fail + else + begin match hash_map_remove_back u64 h4 1024 with + | Fail -> Fail + | Return h5 -> + begin match hash_map_get_fwd u64 h5 0 with + | Fail -> Fail + | Return i1 -> + let b5 = i1 = 42 in + let b6 = not b5 in + if b6 + then Fail + else + begin match hash_map_get_fwd u64 h5 128 with + | Fail -> Fail + | Return i2 -> + let b7 = i2 = 18 in + let b8 = not b7 in + if b8 + then Fail + else + begin match hash_map_get_fwd u64 h5 1056 + with + | Fail -> Fail + | Return i3 -> + let b9 = i3 = 256 in + let b10 = not b9 in + if b10 then Fail else Return () + end + end + end + end + end + end + end + end + end + end + end + end + end + end + +(** Unit test for [hashmap::test1] *) +let _ = assert_norm (test1_fwd = Return ()) + -- cgit v1.2.3