diff options
author | Son Ho | 2022-03-04 14:02:13 +0100 |
---|---|---|
committer | Son Ho | 2022-03-04 14:02:13 +0100 |
commit | 7c444591822e170a15b322c2079202466cc7a475 (patch) | |
tree | 0c9a1fc6b9b85265108647f7bdc87973edad6e17 /tests/hashmap_on_disk/HashmapMain.Funs.fst | |
parent | 479694819f7409cf92b4d0f2775853cda18c3ab4 (diff) |
Generate hashmap_on_disk
Diffstat (limited to '')
-rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Funs.fst | 949 |
1 files changed, 949 insertions, 0 deletions
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst new file mode 100644 index 00000000..0eda588f --- /dev/null +++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst @@ -0,0 +1,949 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: function definitions *) +module HashmapMain.Funs +open Primitives +include HashmapMain.Types +include HashmapMain.Opaque +include HashmapMain.Clauses + +#set-options "--z3rlimit 50 --fuel 0 --ifuel 1" + +(** [hashmap_main::hashmap::hash_key] *) +let hashmap_hash_key_fwd (k : usize) (st : state) : result (state & usize) = + Return (st, k) + +(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) +let rec hashmap_hash_map_allocate_slots_fwd + (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) (st : state) : + Tot (result (state & (vec (hashmap_list_t t)))) + (decreases (hashmap_hash_map_allocate_slots_decreases t slots n st)) + = + begin match n with + | 0 -> Return (st, slots) + | _ -> + begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with + | Fail -> Fail + | Return v -> + begin match usize_sub n 1 with + | Fail -> Fail + | Return i -> + begin match hashmap_hash_map_allocate_slots_fwd t v i st with + | Fail -> Fail + | Return (st0, v0) -> Return (st0, v0) + end + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *) +let hashmap_hash_map_new_with_capacity_fwd + (t : Type0) (capacity : usize) (max_load_dividend : usize) + (max_load_divisor : usize) (st : state) : + result (state & (hashmap_hash_map_t t)) + = + let v = vec_new (hashmap_list_t t) in + begin match hashmap_hash_map_allocate_slots_fwd t v capacity st with + | Fail -> Fail + | Return (st0, 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 (st0, Mkhashmap_hash_map_t 0 (max_load_dividend, + max_load_divisor) i0 v0) + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::new] *) +let hashmap_hash_map_new_fwd + (t : Type0) (st : state) : result (state & (hashmap_hash_map_t t)) = + begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 st with + | Fail -> Fail + | Return (st0, hm) -> Return (st0, hm) + end + +(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) +let rec hashmap_hash_map_clear_slots_fwd + (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) (st : state) : + Tot (result (state & unit)) + (decreases (hashmap_hash_map_clear_slots_decreases t slots i st)) + = + let i0 = vec_len (hashmap_list_t t) slots in + if i < i0 + then + begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil + with + | Fail -> Fail + | Return v -> + begin match usize_add i 1 with + | Fail -> Fail + | Return i1 -> + begin match hashmap_hash_map_clear_slots_fwd t v i1 st with + | Fail -> Fail + | Return (st0, _) -> Return (st0, ()) + end + end + end + else Return (st, ()) + +(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) +let rec hashmap_hash_map_clear_slots_back + (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) (st : state) : + Tot (result (state & (vec (hashmap_list_t t)))) + (decreases (hashmap_hash_map_clear_slots_decreases t slots i st)) + = + let i0 = vec_len (hashmap_list_t t) slots in + if i < i0 + then + begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil + with + | Fail -> Fail + | Return v -> + begin match usize_add i 1 with + | Fail -> Fail + | Return i1 -> + begin match hashmap_hash_map_clear_slots_back t v i1 st with + | Fail -> Fail + | Return (st0, v0) -> Return (st0, v0) + end + end + end + else Return (st, slots) + +(** [hashmap_main::hashmap::HashMap::{0}::clear] *) +let hashmap_hash_map_clear_fwd + (t : Type0) (self : hashmap_hash_map_t t) (st : state) : + result (state & unit) + = + begin match + hashmap_hash_map_clear_slots_fwd t self.hashmap_hash_map_slots 0 st with + | Fail -> Fail + | Return (st0, _) -> Return (st0, ()) + end + +(** [hashmap_main::hashmap::HashMap::{0}::clear] *) +let hashmap_hash_map_clear_back + (t : Type0) (self : hashmap_hash_map_t t) (st : state) : + result (state & (hashmap_hash_map_t t)) + = + begin match + hashmap_hash_map_clear_slots_back t self.hashmap_hash_map_slots 0 st with + | Fail -> Fail + | Return (st0, v) -> + Return (st0, Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) + end + +(** [hashmap_main::hashmap::HashMap::{0}::len] *) +let hashmap_hash_map_len_fwd + (t : Type0) (self : hashmap_hash_map_t t) (st : state) : + result (state & usize) + = + Return (st, self.hashmap_hash_map_num_entries) + +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +let rec hashmap_hash_map_insert_in_list_fwd + (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) : + Tot (result (state & bool)) + (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st)) + = + begin match ls with + | HashmapListCons ckey cvalue ls0 -> + if ckey = key + then Return (st, false) + else + begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 st with + | Fail -> Fail + | Return (st0, b) -> Return (st0, b) + end + | HashmapListNil -> Return (st, true) + end + +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +let rec hashmap_hash_map_insert_in_list_back + (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) : + Tot (result (state & (hashmap_list_t t))) + (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st)) + = + begin match ls with + | HashmapListCons ckey cvalue ls0 -> + if ckey = key + then Return (st, HashmapListCons ckey value ls0) + else + begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with + | Fail -> Fail + | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l) + end + | HashmapListNil -> + let l = HashmapListNil in Return (st, HashmapListCons key value l) + end + +(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *) +let hashmap_hash_map_insert_no_resize_fwd + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) + (st : state) : + result (state & unit) + = + begin match hashmap_hash_key_fwd key st with + | Fail -> Fail + | Return (st0, i) -> + let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod with + | Fail -> Fail + | Return l -> + begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with + | Fail -> Fail + | Return (st1, b) -> + if b + then + begin match usize_add self.hashmap_hash_map_num_entries 1 with + | Fail -> Fail + | Return _ -> Return (st1, ()) + end + else Return (st1, ()) + end + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *) +let hashmap_hash_map_insert_no_resize_back + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) + (st : state) : + result (state & (hashmap_hash_map_t t)) + = + begin match hashmap_hash_key_fwd key st with + | Fail -> Fail + | Return (st0, i) -> + let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod with + | Fail -> Fail + | Return l -> + begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with + | Fail -> Fail + | Return (st1, b) -> + if b + then + begin match usize_add self.hashmap_hash_map_num_entries 1 with + | Fail -> Fail + | Return i1 -> + begin match + hashmap_hash_map_insert_in_list_back t key value l st1 with + | Fail -> Fail + | Return (st2, l0) -> + begin match + vec_index_mut_back (hashmap_list_t t) + self.hashmap_hash_map_slots hash_mod l0 with + | Fail -> Fail + | Return v -> + Return (st2, Mkhashmap_hash_map_t i1 + self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) + end + end + end + else + begin match hashmap_hash_map_insert_in_list_back t key value l st1 + with + | Fail -> Fail + | Return (st2, l0) -> + begin match + vec_index_mut_back (hashmap_list_t t) + self.hashmap_hash_map_slots hash_mod l0 with + | Fail -> Fail + | Return v -> + Return (st2, Mkhashmap_hash_map_t + self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) + end + end + end + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) +let rec hashmap_hash_map_move_elements_from_list_fwd + (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) + (st : state) : + Tot (result (state & unit)) + (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls + st)) + = + begin match ls with + | HashmapListCons k v tl -> + begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with + | Fail -> Fail + | Return (st0, hm) -> + begin match hashmap_hash_map_move_elements_from_list_fwd t hm tl st0 with + | Fail -> Fail + | Return (st1, _) -> Return (st1, ()) + end + end + | HashmapListNil -> Return (st, ()) + end + +(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) +let rec hashmap_hash_map_move_elements_from_list_back + (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) + (st : state) : + Tot (result (state & (hashmap_hash_map_t t))) + (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls + st)) + = + begin match ls with + | HashmapListCons k v tl -> + begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with + | Fail -> Fail + | Return (st0, hm) -> + begin match hashmap_hash_map_move_elements_from_list_back t hm tl st0 + with + | Fail -> Fail + | Return (st1, hm0) -> Return (st1, hm0) + end + end + | HashmapListNil -> Return (st, ntable) + end + +(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) +let rec hashmap_hash_map_move_elements_fwd + (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) + (i : usize) (st : state) : + Tot (result (state & unit)) + (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st)) + = + let i0 = vec_len (hashmap_list_t t) slots in + if i < i0 + then + begin match vec_index_mut_fwd (hashmap_list_t t) slots i with + | Fail -> Fail + | Return l -> + let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in + begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st + with + | Fail -> Fail + | Return (st0, hm) -> + let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in + begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with + | Fail -> Fail + | Return v -> + begin match usize_add i 1 with + | Fail -> Fail + | Return i1 -> + begin match hashmap_hash_map_move_elements_fwd t hm v i1 st0 with + | Fail -> Fail + | Return (st1, _) -> Return (st1, ()) + end + end + end + end + end + else Return (st, ()) + +(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) +let rec hashmap_hash_map_move_elements_back + (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) + (i : usize) (st : state) : + Tot (result (state & ((hashmap_hash_map_t t) & (vec (hashmap_list_t t))))) + (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st)) + = + let i0 = vec_len (hashmap_list_t t) slots in + if i < i0 + then + begin match vec_index_mut_fwd (hashmap_list_t t) slots i with + | Fail -> Fail + | Return l -> + let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in + begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st + with + | Fail -> Fail + | Return (st0, hm) -> + let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in + begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with + | Fail -> Fail + | Return v -> + begin match usize_add i 1 with + | Fail -> Fail + | Return i1 -> + begin match hashmap_hash_map_move_elements_back t hm v i1 st0 with + | Fail -> Fail + | Return (st1, (hm0, v0)) -> Return (st1, (hm0, v0)) + end + end + end + end + end + else Return (st, (ntable, slots)) + +(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) +let hashmap_hash_map_try_resize_fwd + (t : Type0) (self : hashmap_hash_map_t t) (st : state) : + result (state & unit) + = + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_div 4294967295 2 with + | Fail -> Fail + | Return n1 -> + let (i0, i1) = self.hashmap_hash_map_max_load_factor in + begin match usize_div n1 i0 with + | Fail -> Fail + | Return i2 -> + if i <= i2 + then + begin match usize_mul i 2 with + | Fail -> Fail + | Return i3 -> + begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with + | Fail -> Fail + | Return (st0, hm) -> + begin match + hashmap_hash_map_move_elements_back t hm + self.hashmap_hash_map_slots 0 st0 with + | Fail -> Fail + | Return (st1, (_, _)) -> Return (st1, ()) + end + end + end + else Return (st, ()) + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) +let hashmap_hash_map_try_resize_back + (t : Type0) (self : hashmap_hash_map_t t) (st : state) : + result (state & (hashmap_hash_map_t t)) + = + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_div 4294967295 2 with + | Fail -> Fail + | Return n1 -> + let (i0, i1) = self.hashmap_hash_map_max_load_factor in + begin match usize_div n1 i0 with + | Fail -> Fail + | Return i2 -> + if i <= i2 + then + begin match usize_mul i 2 with + | Fail -> Fail + | Return i3 -> + begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with + | Fail -> Fail + | Return (st0, hm) -> + begin match + hashmap_hash_map_move_elements_back t hm + self.hashmap_hash_map_slots 0 st0 with + | Fail -> Fail + | Return (st1, (hm0, v)) -> + let v0 = + mem_replace_back (vec (hashmap_list_t t)) v + hm0.hashmap_hash_map_slots in + Return (st1, Mkhashmap_hash_map_t + self.hashmap_hash_map_num_entries (i0, i1) + hm0.hashmap_hash_map_max_load v0) + end + end + end + else + Return (st, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries ( + i0, i1) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::insert] *) +let hashmap_hash_map_insert_fwd + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) + (st : state) : + result (state & unit) + = + begin match hashmap_hash_map_insert_no_resize_back t self key value st with + | Fail -> Fail + | Return (st0, hm) -> + begin match hashmap_hash_map_len_fwd t hm st0 with + | Fail -> Fail + | Return (st1, i) -> + if i > hm.hashmap_hash_map_max_load + then + begin match + hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t + hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor + hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with + | Fail -> Fail + | Return (st2, _) -> Return (st2, ()) + end + else Return (st1, ()) + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::insert] *) +let hashmap_hash_map_insert_back + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) + (st : state) : + result (state & (hashmap_hash_map_t t)) + = + begin match hashmap_hash_map_insert_no_resize_back t self key value st with + | Fail -> Fail + | Return (st0, hm) -> + begin match hashmap_hash_map_len_fwd t hm st0 with + | Fail -> Fail + | Return (st1, i) -> + if i > hm.hashmap_hash_map_max_load + then + begin match + hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t + hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor + hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with + | Fail -> Fail + | Return (st2, hm0) -> Return (st2, hm0) + end + else + Return (st1, Mkhashmap_hash_map_t hm.hashmap_hash_map_num_entries + hm.hashmap_hash_map_max_load_factor hm.hashmap_hash_map_max_load + hm.hashmap_hash_map_slots) + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) +let rec hashmap_hash_map_contains_key_in_list_fwd + (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) : + Tot (result (state & bool)) + (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls st)) + = + begin match ls with + | HashmapListCons ckey x ls0 -> + if ckey = key + then Return (st, true) + else + begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 st with + | Fail -> Fail + | Return (st0, b) -> Return (st0, b) + end + | HashmapListNil -> Return (st, false) + end + +(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *) +let hashmap_hash_map_contains_key_fwd + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) : + result (state & bool) + = + begin match hashmap_hash_key_fwd key st with + | Fail -> Fail + | Return (st0, i) -> + let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match + vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + with + | Fail -> Fail + | Return l -> + begin match hashmap_hash_map_contains_key_in_list_fwd t key l st0 with + | Fail -> Fail + | Return (st1, b) -> Return (st1, b) + end + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) +let rec hashmap_hash_map_get_in_list_fwd + (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) : + Tot (result (state & t)) + (decreases (hashmap_hash_map_get_in_list_decreases t key ls st)) + = + begin match ls with + | HashmapListCons ckey cvalue ls0 -> + if ckey = key + then Return (st, cvalue) + else + begin match hashmap_hash_map_get_in_list_fwd t key ls0 st with + | Fail -> Fail + | Return (st0, x) -> Return (st0, x) + end + | HashmapListNil -> Fail + end + +(** [hashmap_main::hashmap::HashMap::{0}::get] *) +let hashmap_hash_map_get_fwd + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) : + result (state & t) + = + begin match hashmap_hash_key_fwd key st with + | Fail -> Fail + | Return (st0, i) -> + let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match + vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + with + | Fail -> Fail + | Return l -> + begin match hashmap_hash_map_get_in_list_fwd t key l st0 with + | Fail -> Fail + | Return (st1, x) -> Return (st1, x) + end + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +let rec hashmap_hash_map_get_mut_in_list_fwd + (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) : + Tot (result (state & t)) + (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st)) + = + begin match ls with + | HashmapListCons ckey cvalue ls0 -> + if ckey = key + then Return (st, cvalue) + else + begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 st with + | Fail -> Fail + | Return (st0, x) -> Return (st0, x) + end + | HashmapListNil -> Fail + end + +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +let rec hashmap_hash_map_get_mut_in_list_back + (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) (st : state) : + Tot (result (state & (hashmap_list_t t))) + (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st)) + = + begin match ls with + | HashmapListCons ckey cvalue ls0 -> + if ckey = key + then Return (st, HashmapListCons ckey ret ls0) + else + begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret st with + | Fail -> Fail + | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l) + end + | HashmapListNil -> Fail + end + +(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) +let hashmap_hash_map_get_mut_fwd + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) : + result (state & t) + = + begin match hashmap_hash_key_fwd key st with + | Fail -> Fail + | Return (st0, i) -> + let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod with + | Fail -> Fail + | Return l -> + begin match hashmap_hash_map_get_mut_in_list_fwd t key l st0 with + | Fail -> Fail + | Return (st1, x) -> Return (st1, x) + end + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) +let hashmap_hash_map_get_mut_back + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) + (st : state) : + result (state & (hashmap_hash_map_t t)) + = + begin match hashmap_hash_key_fwd key st with + | Fail -> Fail + | Return (st0, i) -> + let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod with + | Fail -> Fail + | Return l -> + begin match hashmap_hash_map_get_mut_in_list_back t key l ret st0 with + | Fail -> Fail + | Return (st1, l0) -> + begin match + vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod l0 with + | Fail -> Fail + | Return v -> + Return (st1, Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) + end + end + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +let rec hashmap_hash_map_remove_from_list_fwd + (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) : + Tot (result (state & (option t))) + (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st)) + = + begin match ls with + | HashmapListCons ckey x tl -> + if ckey = key + then + let mv_ls = + mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl) + HashmapListNil in + begin match mv_ls with + | HashmapListCons i cvalue tl0 -> Return (st, Some cvalue) + | HashmapListNil -> Fail + end + else + begin match hashmap_hash_map_remove_from_list_fwd t key tl st with + | Fail -> Fail + | Return (st0, opt) -> Return (st0, opt) + end + | HashmapListNil -> Return (st, None) + end + +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +let rec hashmap_hash_map_remove_from_list_back + (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) : + Tot (result (state & (hashmap_list_t t))) + (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st)) + = + begin match ls with + | HashmapListCons ckey x tl -> + if ckey = key + then + let mv_ls = + mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl) + HashmapListNil in + begin match mv_ls with + | HashmapListCons i cvalue tl0 -> Return (st, tl0) + | HashmapListNil -> Fail + end + else + begin match hashmap_hash_map_remove_from_list_back t key tl st with + | Fail -> Fail + | Return (st0, l) -> Return (st0, HashmapListCons ckey x l) + end + | HashmapListNil -> Return (st, HashmapListNil) + end + +(** [hashmap_main::hashmap::HashMap::{0}::remove] *) +let hashmap_hash_map_remove_fwd + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) : + result (state & (option t)) + = + begin match hashmap_hash_key_fwd key st with + | Fail -> Fail + | Return (st0, i) -> + let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod with + | Fail -> Fail + | Return l -> + begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with + | Fail -> Fail + | Return (st1, x) -> + begin match x with + | None -> Return (st1, None) + | Some x0 -> + begin match usize_sub self.hashmap_hash_map_num_entries 1 with + | Fail -> Fail + | Return _ -> Return (st1, Some x0) + end + end + end + end + end + end + +(** [hashmap_main::hashmap::HashMap::{0}::remove] *) +let hashmap_hash_map_remove_back + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) : + result (state & (hashmap_hash_map_t t)) + = + begin match hashmap_hash_key_fwd key st with + | Fail -> Fail + | Return (st0, i) -> + let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_rem i i0 with + | Fail -> Fail + | Return hash_mod -> + begin match + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots + hash_mod with + | Fail -> Fail + | Return l -> + begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with + | Fail -> Fail + | Return (st1, x) -> + begin match x with + | None -> + begin match hashmap_hash_map_remove_from_list_back t key l st1 with + | Fail -> Fail + | Return (st2, l0) -> + begin match + vec_index_mut_back (hashmap_list_t t) + self.hashmap_hash_map_slots hash_mod l0 with + | Fail -> Fail + | Return v -> + Return (st2, Mkhashmap_hash_map_t + self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) + end + end + | Some x0 -> + begin match usize_sub self.hashmap_hash_map_num_entries 1 with + | Fail -> Fail + | Return i1 -> + begin match hashmap_hash_map_remove_from_list_back t key l st1 + with + | Fail -> Fail + | Return (st2, l0) -> + begin match + vec_index_mut_back (hashmap_list_t t) + self.hashmap_hash_map_slots hash_mod l0 with + | Fail -> Fail + | Return v -> + Return (st2, Mkhashmap_hash_map_t i1 + self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) + end + end + end + end + end + end + end + end + +(** [hashmap_main::hashmap::test1] *) +let hashmap_test1_fwd (st : state) : result (state & unit) = + begin match hashmap_hash_map_new_fwd u64 st with + | Fail -> Fail + | Return (st0, hm) -> + begin match hashmap_hash_map_insert_back u64 hm 0 42 st0 with + | Fail -> Fail + | Return (st1, hm0) -> + begin match hashmap_hash_map_insert_back u64 hm0 128 18 st1 with + | Fail -> Fail + | Return (st2, hm1) -> + begin match hashmap_hash_map_insert_back u64 hm1 1024 138 st2 with + | Fail -> Fail + | Return (st3, hm2) -> + begin match hashmap_hash_map_insert_back u64 hm2 1056 256 st3 with + | Fail -> Fail + | Return (st4, hm3) -> + begin match hashmap_hash_map_get_fwd u64 hm3 128 st4 with + | Fail -> Fail + | Return (st5, i) -> + if not (i = 18) + then Fail + else + begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 st5 + with + | Fail -> Fail + | Return (st6, hm4) -> + begin match hashmap_hash_map_get_fwd u64 hm4 1024 st6 with + | Fail -> Fail + | Return (st7, i0) -> + if not (i0 = 56) + then Fail + else + begin match hashmap_hash_map_remove_fwd u64 hm4 1024 st7 + with + | Fail -> Fail + | Return (st8, x) -> + begin match x with + | None -> Fail + | Some x0 -> + if not (x0 = 56) + then Fail + else + begin match + hashmap_hash_map_remove_back u64 hm4 1024 st8 + with + | Fail -> Fail + | Return (st9, hm5) -> + begin match + hashmap_hash_map_get_fwd u64 hm5 0 st9 with + | Fail -> Fail + | Return (st10, i1) -> + if not (i1 = 42) + then Fail + else + begin match + hashmap_hash_map_get_fwd u64 hm5 128 st10 + with + | Fail -> Fail + | Return (st11, i2) -> + if not (i2 = 18) + then Fail + else + begin match + hashmap_hash_map_get_fwd u64 + hm5 1056 st11 with + | Fail -> Fail + | Return (st12, i3) -> + if not (i3 = 256) + then Fail + else Return (st12, ()) + end + end + end + end + end + end + end + end + end + end + end + end + end + end + +(** [hashmap_main::insert_on_disk] *) +let insert_on_disk_fwd + (key : usize) (value : u64) (st : state) : result (state & unit) = + begin match hashmap_utils_deserialize_fwd st with + | Fail -> Fail + | Return (st0, hm) -> + begin match hashmap_hash_map_insert_back u64 hm key value st0 with + | Fail -> Fail + | Return (st1, hm0) -> + begin match hashmap_utils_serialize_fwd hm0 st1 with + | Fail -> Fail + | Return (st2, _) -> Return (st2, ()) + end + end + end + +(** [hashmap_main::main] *) +let main_fwd (st : state) : result (state & unit) = Return (st, ()) + |