diff options
Diffstat (limited to 'tests/hashmap_on_disk/HashmapMain.Funs.fst')
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Funs.fst | 712 |
1 files changed, 219 insertions, 493 deletions
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst index 1b281acb..4177f77d 100644 --- a/tests/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst @@ -9,17 +9,16 @@ 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) +let hashmap_hash_key_fwd (k : usize) : result usize = Return 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)) + (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) : + Tot (result (vec (hashmap_list_t t))) + (decreases (hashmap_hash_map_allocate_slots_decreases t slots n)) = begin match n with - | 0 -> Return (st, slots) + | 0 -> Return slots | _ -> begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with | Fail -> Fail @@ -27,9 +26,9 @@ let rec hashmap_hash_map_allocate_slots_fwd begin match usize_sub n 1 with | Fail -> Fail | Return i -> - begin match hashmap_hash_map_allocate_slots_fwd t slots0 i st with + begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with | Fail -> Fail - | Return (st0, v) -> Return (st0, v) + | Return v -> Return v end end end @@ -38,62 +37,37 @@ let rec hashmap_hash_map_allocate_slots_fwd (** [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)) + (max_load_divisor : usize) : + result (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 + begin match hashmap_hash_map_allocate_slots_fwd t v capacity with | Fail -> Fail - | Return (st0, slots) -> + | Return slots -> 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 slots) + Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0 + slots) 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 +let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = + begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with | Fail -> Fail - | Return (st0, hm) -> Return (st0, hm) + | Return hm -> Return 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 slots0 -> - begin match usize_add i 1 with - | Fail -> Fail - | Return i1 -> - begin match hashmap_hash_map_clear_slots_fwd t slots0 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) : +let rec hashmap_hash_map_clear_slots_fwd_back + (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) : Tot (result (vec (hashmap_list_t t))) - (decreases (hashmap_hash_map_clear_slots_decreases t slots i st)) + (decreases (hashmap_hash_map_clear_slots_decreases t slots i)) = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 @@ -105,7 +79,7 @@ let rec hashmap_hash_map_clear_slots_back begin match usize_add i 1 with | Fail -> Fail | Return i1 -> - begin match hashmap_hash_map_clear_slots_back t slots0 i1 st with + begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with | Fail -> Fail | Return slots1 -> Return slots1 end @@ -114,23 +88,10 @@ let rec hashmap_hash_map_clear_slots_back else Return 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) - = +let hashmap_hash_map_clear_fwd_back + (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = 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 (hashmap_hash_map_t t) - = - begin match - hashmap_hash_map_clear_slots_back t self.hashmap_hash_map_slots 0 st with + hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots 0 with | Fail -> Fail | Return v -> Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor @@ -139,41 +100,39 @@ let hashmap_hash_map_clear_back (** [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) + (t : Type0) (self : hashmap_hash_map_t t) : result usize = + Return 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)) + (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : + Tot (result bool) + (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls)) = begin match ls with | HashmapListCons ckey cvalue ls0 -> if ckey = key - then Return (st, false) + then Return false else - begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 st with + begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with | Fail -> Fail - | Return (st0, b) -> Return (st0, b) + | Return b -> Return b end - | HashmapListNil -> Return (st, true) + | HashmapListNil -> Return 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) : + (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st)) + (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls)) = begin match ls with | HashmapListCons ckey cvalue ls0 -> if ckey = key then Return (HashmapListCons ckey value ls0) else - begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with + begin match hashmap_hash_map_insert_in_list_back t key value ls0 with | Fail -> Fail | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) end @@ -182,47 +141,13 @@ let rec hashmap_hash_map_insert_in_list_back 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, hash) -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i 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, inserted) -> - if inserted - 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) : +let hashmap_hash_map_insert_no_resize_fwd_back + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key st with + begin match hashmap_hash_key_fwd key with | Fail -> Fail - | Return (st0, hash) -> + | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with | Fail -> Fail @@ -232,16 +157,16 @@ let hashmap_hash_map_insert_no_resize_back hash_mod with | Fail -> Fail | Return l -> - begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with + begin match hashmap_hash_map_insert_in_list_fwd t key value l with | Fail -> Fail - | Return (_, inserted) -> + | Return inserted -> if inserted then begin match usize_add self.hashmap_hash_map_num_entries 1 with | Fail -> Fail | Return i0 -> - begin match - hashmap_hash_map_insert_in_list_back t key value l st0 with + begin match hashmap_hash_map_insert_in_list_back t key value l + with | Fail -> Fail | Return l0 -> begin match @@ -256,8 +181,7 @@ let hashmap_hash_map_insert_no_resize_back end end else - begin match hashmap_hash_map_insert_in_list_back t key value l st0 - with + begin match hashmap_hash_map_insert_in_list_back t key value l with | Fail -> Fail | Return l0 -> begin match @@ -276,104 +200,31 @@ let hashmap_hash_map_insert_no_resize_back 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_fwd t ntable k v st with - | Fail -> Fail - | Return (st0, _) -> - begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with - | Fail -> Fail - | Return ntable0 -> - begin match - hashmap_hash_map_move_elements_from_list_fwd t ntable0 tl st0 with - | Fail -> Fail - | Return (st1, _) -> Return (st1, ()) - end - 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) : +let rec hashmap_hash_map_move_elements_from_list_fwd_back + (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : Tot (result (hashmap_hash_map_t t)) - (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls - st)) + (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls)) = begin match ls with | HashmapListCons k v tl -> - begin match hashmap_hash_map_insert_no_resize_fwd t ntable k v st with + begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with | Fail -> Fail - | Return (st0, _) -> - begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with + | Return ntable0 -> + begin match + hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with | Fail -> Fail - | Return ntable0 -> - begin match - hashmap_hash_map_move_elements_from_list_back t ntable0 tl st0 with - | Fail -> Fail - | Return ntable1 -> Return ntable1 - end + | Return ntable1 -> Return ntable1 end end | HashmapListNil -> Return ntable end (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) -let rec hashmap_hash_map_move_elements_fwd +let rec hashmap_hash_map_move_elements_fwd_back (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 ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in - begin match hashmap_hash_map_move_elements_from_list_fwd t ntable ls st - with - | Fail -> Fail - | Return (st0, _) -> - begin match - hashmap_hash_map_move_elements_from_list_back t ntable ls st with - | Fail -> Fail - | Return ntable0 -> - let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in - begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with - | Fail -> Fail - | Return slots0 -> - begin match usize_add i 1 with - | Fail -> Fail - | Return i1 -> - begin match - hashmap_hash_map_move_elements_fwd t ntable0 slots0 i1 st0 with - | Fail -> Fail - | Return (st1, _) -> Return (st1, ()) - end - 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) : + (i : usize) : Tot (result ((hashmap_hash_map_t t) & (vec (hashmap_list_t t)))) - (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st)) + (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i)) = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 @@ -382,27 +233,21 @@ let rec hashmap_hash_map_move_elements_back | Fail -> Fail | Return l -> let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in - begin match hashmap_hash_map_move_elements_from_list_fwd t ntable ls st + begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls with | Fail -> Fail - | Return (st0, _) -> - begin match - hashmap_hash_map_move_elements_from_list_back t ntable ls st with + | Return ntable0 -> + let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in + begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with | Fail -> Fail - | Return ntable0 -> - let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in - begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with + | Return slots0 -> + begin match usize_add i 1 with | Fail -> Fail - | Return slots0 -> - begin match usize_add i 1 with + | Return i1 -> + begin match + hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with | Fail -> Fail - | Return i1 -> - begin match - hashmap_hash_map_move_elements_back t ntable0 slots0 i1 st0 - with - | Fail -> Fail - | Return (ntable1, slots1) -> Return (ntable1, slots1) - end + | Return (ntable1, slots1) -> Return (ntable1, slots1) end end end @@ -411,49 +256,8 @@ let rec hashmap_hash_map_move_elements_back else Return (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 capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_div 4294967295 2 with - | Fail -> Fail - | Return n1 -> - let (i, i0) = self.hashmap_hash_map_max_load_factor in - begin match usize_div n1 i with - | Fail -> Fail - | Return i1 -> - if capacity <= i1 - then - begin match usize_mul capacity 2 with - | Fail -> Fail - | Return i2 -> - begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 st with - | Fail -> Fail - | Return (st0, ntable) -> - begin match - hashmap_hash_map_move_elements_fwd t ntable - self.hashmap_hash_map_slots 0 st0 with - | Fail -> Fail - | Return (st1, _) -> - begin match - hashmap_hash_map_move_elements_back t ntable - self.hashmap_hash_map_slots 0 st0 with - | Fail -> Fail - | Return (_, _) -> Return (st1, ()) - end - 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 (hashmap_hash_map_t t) - = +let hashmap_hash_map_try_resize_fwd_back + (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_div 4294967295 2 with | Fail -> Fail @@ -467,12 +271,12 @@ let hashmap_hash_map_try_resize_back begin match usize_mul capacity 2 with | Fail -> Fail | Return i2 -> - begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 st with + begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with | Fail -> Fail - | Return (st0, ntable) -> + | Return ntable -> begin match - hashmap_hash_map_move_elements_back t ntable - self.hashmap_hash_map_slots 0 st0 with + hashmap_hash_map_move_elements_fwd_back t ntable + self.hashmap_hash_map_slots 0 with | Fail -> Fail | Return (ntable0, _) -> Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries @@ -488,96 +292,57 @@ let hashmap_hash_map_try_resize_back 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_fwd t self key value st with - | Fail -> Fail - | Return (st0, _) -> - begin match hashmap_hash_map_insert_no_resize_back t self key value st with - | Fail -> Fail - | Return self0 -> - begin match hashmap_hash_map_len_fwd t self0 st0 with - | Fail -> Fail - | Return (st1, i) -> - if i > self0.hashmap_hash_map_max_load - then - begin match - hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t - self0.hashmap_hash_map_num_entries - self0.hashmap_hash_map_max_load_factor - self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) st1 - with - | Fail -> Fail - | Return (st2, _) -> Return (st2, ()) - end - else Return (st1, ()) - end - 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) : +let hashmap_hash_map_insert_fwd_back + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_map_insert_no_resize_fwd t self key value st with + begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with | Fail -> Fail - | Return (st0, _) -> - begin match hashmap_hash_map_insert_no_resize_back t self key value st with + | Return self0 -> + begin match hashmap_hash_map_len_fwd t self0 with | Fail -> Fail - | Return self0 -> - begin match hashmap_hash_map_len_fwd t self0 st0 with - | Fail -> Fail - | Return (st1, i) -> - if i > self0.hashmap_hash_map_max_load - then - begin match - hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t - self0.hashmap_hash_map_num_entries - self0.hashmap_hash_map_max_load_factor - self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) st1 - with - | Fail -> Fail - | Return self1 -> Return self1 - end - else - Return (Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries + | Return i -> + if i > self0.hashmap_hash_map_max_load + then + begin match + hashmap_hash_map_try_resize_fwd_back t (Mkhashmap_hash_map_t + self0.hashmap_hash_map_num_entries self0.hashmap_hash_map_max_load_factor - self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) - end + self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) with + | Fail -> Fail + | Return self1 -> Return self1 + end + else + Return (Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries + self0.hashmap_hash_map_max_load_factor + self0.hashmap_hash_map_max_load self0.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)) + (t : Type0) (key : usize) (ls : hashmap_list_t t) : + Tot (result bool) + (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey x ls0 -> if ckey = key - then Return (st, true) + then Return true else - begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 st with + begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with | Fail -> Fail - | Return (st0, b) -> Return (st0, b) + | Return b -> Return b end - | HashmapListNil -> Return (st, false) + | HashmapListNil -> Return 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 + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool = + begin match hashmap_hash_key_fwd key with | Fail -> Fail - | Return (st0, hash) -> + | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with | Fail -> Fail @@ -587,9 +352,9 @@ let hashmap_hash_map_contains_key_fwd with | Fail -> Fail | Return l -> - begin match hashmap_hash_map_contains_key_in_list_fwd t key l st0 with + begin match hashmap_hash_map_contains_key_in_list_fwd t key l with | Fail -> Fail - | Return (st1, b) -> Return (st1, b) + | Return b -> Return b end end end @@ -597,30 +362,27 @@ let hashmap_hash_map_contains_key_fwd (** [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)) + (t : Type0) (key : usize) (ls : hashmap_list_t t) : + Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey cvalue ls0 -> if ckey = key - then Return (st, cvalue) + then Return cvalue else - begin match hashmap_hash_map_get_in_list_fwd t key ls0 st with + begin match hashmap_hash_map_get_in_list_fwd t key ls0 with | Fail -> Fail - | Return (st0, x) -> Return (st0, x) + | Return x -> Return 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 + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = + begin match hashmap_hash_key_fwd key with | Fail -> Fail - | Return (st0, hash) -> + | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with | Fail -> Fail @@ -630,9 +392,9 @@ let hashmap_hash_map_get_fwd with | Fail -> Fail | Return l -> - begin match hashmap_hash_map_get_in_list_fwd t key l st0 with + begin match hashmap_hash_map_get_in_list_fwd t key l with | Fail -> Fail - | Return (st1, x) -> Return (st1, x) + | Return x -> Return x end end end @@ -640,34 +402,34 @@ let hashmap_hash_map_get_fwd (** [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)) + (t : Type0) (key : usize) (ls : hashmap_list_t t) : + Tot (result t) + (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey cvalue ls0 -> if ckey = key - then Return (st, cvalue) + then Return cvalue else - begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 st with + begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with | Fail -> Fail - | Return (st0, x) -> Return (st0, x) + | Return x -> Return 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) (st : state) (ret : t) : + (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) : Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls st)) + (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey cvalue ls0 -> if ckey = key then Return (HashmapListCons ckey ret ls0) else - begin match hashmap_hash_map_get_mut_in_list_back t key ls0 st ret with + begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret with | Fail -> Fail | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) end @@ -676,12 +438,10 @@ let rec hashmap_hash_map_get_mut_in_list_back (** [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 + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = + begin match hashmap_hash_key_fwd key with | Fail -> Fail - | Return (st0, hash) -> + | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with | Fail -> Fail @@ -691,9 +451,9 @@ let hashmap_hash_map_get_mut_fwd hash_mod with | Fail -> Fail | Return l -> - begin match hashmap_hash_map_get_mut_in_list_fwd t key l st0 with + begin match hashmap_hash_map_get_mut_in_list_fwd t key l with | Fail -> Fail - | Return (st1, x) -> Return (st1, x) + | Return x -> Return x end end end @@ -701,13 +461,12 @@ let hashmap_hash_map_get_mut_fwd (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) let hashmap_hash_map_get_mut_back - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) - (ret : t) : + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key st with + begin match hashmap_hash_key_fwd key with | Fail -> Fail - | Return (st0, hash) -> + | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with | Fail -> Fail @@ -717,7 +476,7 @@ let hashmap_hash_map_get_mut_back hash_mod with | Fail -> Fail | Return l -> - begin match hashmap_hash_map_get_mut_in_list_back t key l st0 ret with + begin match hashmap_hash_map_get_mut_in_list_back t key l ret with | Fail -> Fail | Return l0 -> begin match @@ -736,9 +495,9 @@ let hashmap_hash_map_get_mut_back (** [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)) + (t : Type0) (key : usize) (ls : hashmap_list_t t) : + Tot (result (option t)) + (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey x tl -> @@ -748,22 +507,22 @@ let rec hashmap_hash_map_remove_from_list_fwd 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) + | HashmapListCons i cvalue tl0 -> Return (Some cvalue) | HashmapListNil -> Fail end else - begin match hashmap_hash_map_remove_from_list_fwd t key tl st with + begin match hashmap_hash_map_remove_from_list_fwd t key tl with | Fail -> Fail - | Return (st0, opt) -> Return (st0, opt) + | Return opt -> Return opt end - | HashmapListNil -> Return (st, None) + | HashmapListNil -> Return 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) : + (t : Type0) (key : usize) (ls : hashmap_list_t t) : Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_remove_from_list_decreases t key ls st)) + (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey x tl -> @@ -777,7 +536,7 @@ let rec hashmap_hash_map_remove_from_list_back | HashmapListNil -> Fail end else - begin match hashmap_hash_map_remove_from_list_back t key tl st with + begin match hashmap_hash_map_remove_from_list_back t key tl with | Fail -> Fail | Return tl0 -> Return (HashmapListCons ckey x tl0) end @@ -786,12 +545,10 @@ let rec hashmap_hash_map_remove_from_list_back (** [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 + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) = + begin match hashmap_hash_key_fwd key with | Fail -> Fail - | Return (st0, hash) -> + | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with | Fail -> Fail @@ -801,15 +558,15 @@ let hashmap_hash_map_remove_fwd hash_mod with | Fail -> Fail | Return l -> - begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with + begin match hashmap_hash_map_remove_from_list_fwd t key l with | Fail -> Fail - | Return (st1, x) -> + | Return x -> begin match x with - | None -> Return (st1, None) + | None -> Return None | Some x0 -> begin match usize_sub self.hashmap_hash_map_num_entries 1 with | Fail -> Fail - | Return _ -> Return (st1, Some x0) + | Return _ -> Return (Some x0) end end end @@ -819,12 +576,12 @@ let hashmap_hash_map_remove_fwd (** [hashmap_main::hashmap::HashMap::{0}::remove] *) let hashmap_hash_map_remove_back - (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (st : state) : + (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key st with + begin match hashmap_hash_key_fwd key with | Fail -> Fail - | Return (st0, hash) -> + | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with | Fail -> Fail @@ -834,12 +591,12 @@ let hashmap_hash_map_remove_back hash_mod with | Fail -> Fail | Return l -> - begin match hashmap_hash_map_remove_from_list_fwd t key l st0 with + begin match hashmap_hash_map_remove_from_list_fwd t key l with | Fail -> Fail - | Return (_, x) -> + | Return x -> begin match x with | None -> - begin match hashmap_hash_map_remove_from_list_back t key l st0 with + begin match hashmap_hash_map_remove_from_list_back t key l with | Fail -> Fail | Return l0 -> begin match @@ -856,8 +613,7 @@ let hashmap_hash_map_remove_back begin match usize_sub self.hashmap_hash_map_num_entries 1 with | Fail -> Fail | Return i0 -> - begin match hashmap_hash_map_remove_from_list_back t key l st0 - with + begin match hashmap_hash_map_remove_from_list_back t key l with | Fail -> Fail | Return l0 -> begin match @@ -878,112 +634,80 @@ let hashmap_hash_map_remove_back end (** [hashmap_main::hashmap::test1] *) -let hashmap_test1_fwd (st : state) : result (state & unit) = - begin match hashmap_hash_map_new_fwd u64 st with +let hashmap_test1_fwd : result unit = + begin match hashmap_hash_map_new_fwd u64 with | Fail -> Fail - | Return (st0, hm) -> - begin match hashmap_hash_map_insert_fwd u64 hm 0 42 st0 with + | Return hm -> + begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with | Fail -> Fail - | Return (st1, _) -> - begin match hashmap_hash_map_insert_back u64 hm 0 42 st0 with + | Return hm0 -> + begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with | Fail -> Fail - | Return hm0 -> - begin match hashmap_hash_map_insert_fwd u64 hm0 128 18 st1 with + | Return hm1 -> + begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with | Fail -> Fail - | Return (st2, _) -> - begin match hashmap_hash_map_insert_back u64 hm0 128 18 st1 with + | Return hm2 -> + begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with | Fail -> Fail - | Return hm1 -> - begin match hashmap_hash_map_insert_fwd u64 hm1 1024 138 st2 with + | Return hm3 -> + begin match hashmap_hash_map_get_fwd u64 hm3 128 with | Fail -> Fail - | Return (st3, _) -> - begin match hashmap_hash_map_insert_back u64 hm1 1024 138 st2 - with - | Fail -> Fail - | Return hm2 -> - begin match hashmap_hash_map_insert_fwd u64 hm2 1056 256 st3 - with + | Return i -> + if not (i = 18) + then Fail + else + begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with | Fail -> Fail - | Return (st4, _) -> - begin match hashmap_hash_map_insert_back u64 hm2 1056 256 st3 - with + | Return hm4 -> + begin match hashmap_hash_map_get_fwd u64 hm4 1024 with | Fail -> Fail - | Return 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_fwd u64 hm3 1024 st5 with - | Fail -> Fail - | Return (st6, _) -> - begin match - hashmap_hash_map_get_mut_back u64 hm3 1024 st5 56 - with - | Fail -> Fail - | Return hm4 -> + | Return i0 -> + if not (i0 = 56) + then Fail + else + begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with + | Fail -> Fail + | Return x -> + begin match x with + | None -> Fail + | Some x0 -> + if not (x0 = 56) + then Fail + else begin match - hashmap_hash_map_get_fwd u64 hm4 1024 st6 with + hashmap_hash_map_remove_back u64 hm4 1024 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) + | Return hm5 -> + begin match hashmap_hash_map_get_fwd u64 hm5 0 + with + | Fail -> Fail + | Return i1 -> + if not (i1 = 42) + then Fail + else + begin match + hashmap_hash_map_get_fwd u64 hm5 128 with + | Fail -> Fail + | Return i2 -> + if not (i2 = 18) then Fail else begin match - hashmap_hash_map_remove_back u64 hm4 - 1024 st7 with + hashmap_hash_map_get_fwd u64 hm5 1056 + with | Fail -> Fail - | Return hm5 -> - begin match - hashmap_hash_map_get_fwd u64 hm5 0 - st8 with - | Fail -> Fail - | Return (st9, i1) -> - if not (i1 = 42) - then Fail - else - begin match - hashmap_hash_map_get_fwd u64 hm5 - 128 st9 with - | Fail -> Fail - | Return (st10, i2) -> - if not (i2 = 18) - then Fail - else - begin match - hashmap_hash_map_get_fwd u64 - hm5 1056 st10 with - | Fail -> Fail - | Return (st11, i3) -> - if not (i3 = 256) - then Fail - else Return (st11, ()) - end - end - end + | Return i3 -> + if not (i3 = 256) + then Fail + else Return () end end - end + end end - end end - end + end end end - end end end end @@ -991,26 +715,28 @@ let hashmap_test1_fwd (st : state) : result (state & unit) = end end +(** Unit test for [hashmap_main::hashmap::test1] *) +let _ = assert_norm (hashmap_test1_fwd = Return ()) + (** [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_fwd u64 hm key value st0 with + begin match hashmap_hash_map_insert_fwd_back u64 hm key value with | Fail -> Fail - | Return (st1, _) -> - begin match hashmap_hash_map_insert_back u64 hm key value st0 with + | Return hm0 -> + begin match hashmap_utils_serialize_fwd hm0 st0 with | Fail -> Fail - | Return hm0 -> - begin match hashmap_utils_serialize_fwd hm0 st1 with - | Fail -> Fail - | Return (st2, _) -> Return (st2, ()) - end + | Return (st1, _) -> Return (st1, ()) end end end (** [hashmap_main::main] *) -let main_fwd (st : state) : result (state & unit) = Return (st, ()) +let main_fwd : result unit = Return () + +(** Unit test for [hashmap_main::main] *) +let _ = assert_norm (main_fwd = Return ()) |