diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 53 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 55 |
2 files changed, 55 insertions, 53 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 0140aadc..62799976 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -8,7 +8,8 @@ include Hashmap.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap::hash_key] *) -let hash_key_fwd (k : usize) : result usize = Return k +let hash_key_fwd (k : usize) : result usize = + Return k (** [hashmap::HashMap::{0}::allocate_slots] *) let rec hash_map_allocate_slots_loop_fwd @@ -17,10 +18,10 @@ let rec hash_map_allocate_slots_loop_fwd (decreases (hash_map_allocate_slots_loop_decreases t slots n)) = if n > 0 - then begin + then let* slots0 = vec_push_back (list_t t) slots ListNil in let* n0 = usize_sub n 1 in - hash_map_allocate_slots_loop_fwd t slots0 n0 end + hash_map_allocate_slots_loop_fwd t slots0 n0 else Return slots (** [hashmap::HashMap::{0}::allocate_slots] *) @@ -52,10 +53,10 @@ let rec hash_map_clear_loop_fwd_back = let i0 = vec_len (list_t t) slots in if i < i0 - then begin + then let* i1 = usize_add i 1 in let* slots0 = vec_index_mut_back (list_t t) slots i ListNil in - hash_map_clear_loop_fwd_back t slots0 i1 end + hash_map_clear_loop_fwd_back t slots0 i1 else Return slots (** [hashmap::HashMap::{0}::clear] *) @@ -98,9 +99,9 @@ let rec hash_map_insert_in_list_loop_back | ListCons ckey cvalue tl -> if ckey = key then Return (ListCons ckey value tl) - else begin + else let* tl0 = hash_map_insert_in_list_loop_back t key value tl in - Return (ListCons ckey cvalue tl0) end + Return (ListCons ckey cvalue tl0) | ListNil -> let l = ListNil in Return (ListCons key value l) end @@ -120,17 +121,17 @@ let hash_map_insert_no_resize_fwd_back let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in let* inserted = hash_map_insert_in_list_fwd t key value l in if inserted - then begin + then let* i0 = usize_add self.hash_map_num_entries 1 in let* l0 = hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in Return (Mkhash_map_t i0 self.hash_map_max_load_factor - self.hash_map_max_load v) end - else begin + self.hash_map_max_load v) + else let* l0 = hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in Return (Mkhash_map_t self.hash_map_num_entries - self.hash_map_max_load_factor self.hash_map_max_load v) end + self.hash_map_max_load_factor self.hash_map_max_load v) (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -162,14 +163,14 @@ let rec hash_map_move_elements_loop_fwd_back = let i0 = vec_len (list_t t) slots in if i < i0 - then begin + then let* l = vec_index_mut_fwd (list_t t) slots i in let ls = mem_replace_fwd (list_t t) l ListNil in let* ntable0 = hash_map_move_elements_from_list_fwd_back t ntable ls in let* i1 = usize_add i 1 in let l0 = mem_replace_back (list_t t) l ListNil in let* slots0 = vec_index_mut_back (list_t t) slots i l0 in - hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end + hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 else Return (ntable, slots) (** [hashmap::HashMap::{0}::move_elements] *) @@ -188,13 +189,13 @@ let hash_map_try_resize_fwd_back let (i, i0) = self.hash_map_max_load_factor in let* i1 = usize_div n1 i in if capacity <= i1 - then begin + then let* i2 = usize_mul capacity 2 in let* ntable = hash_map_new_with_capacity_fwd t i2 i i0 in let* (ntable0, _) = hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 in Return (Mkhash_map_t self.hash_map_num_entries (i, i0) - ntable0.hash_map_max_load ntable0.hash_map_slots) end + ntable0.hash_map_max_load ntable0.hash_map_slots) else Return (Mkhash_map_t self.hash_map_num_entries (i, i0) self.hash_map_max_load self.hash_map_slots) @@ -293,9 +294,9 @@ let rec hash_map_get_mut_in_list_loop_back | ListCons ckey cvalue tl -> if ckey = key then Return (ListCons ckey ret tl) - else begin + else let* tl0 = hash_map_get_mut_in_list_loop_back t tl key ret in - Return (ListCons ckey cvalue tl0) end + Return (ListCons ckey cvalue tl0) | ListNil -> Fail Failure end @@ -366,9 +367,9 @@ let rec hash_map_remove_from_list_loop_back | ListCons i cvalue tl0 -> Return tl0 | ListNil -> Fail Failure end - else begin + else let* tl0 = hash_map_remove_from_list_loop_back t key tl in - Return (ListCons ckey x tl0) end + Return (ListCons ckey x tl0) | ListNil -> Return ListNil end @@ -423,31 +424,31 @@ let test1_fwd : result unit = let* i = hash_map_get_fwd u64 hm3 128 in if not (i = 18) then Fail Failure - else begin + else let* hm4 = hash_map_get_mut_back u64 hm3 1024 56 in let* i0 = hash_map_get_fwd u64 hm4 1024 in if not (i0 = 56) then Fail Failure - else begin + else let* x = hash_map_remove_fwd u64 hm4 1024 in begin match x with | None -> Fail Failure | Some x0 -> if not (x0 = 56) then Fail Failure - else begin + else let* hm5 = hash_map_remove_back u64 hm4 1024 in let* i1 = hash_map_get_fwd u64 hm5 0 in if not (i1 = 42) then Fail Failure - else begin + else let* i2 = hash_map_get_fwd u64 hm5 128 in if not (i2 = 18) then Fail Failure - else begin + else let* i3 = hash_map_get_fwd u64 hm5 1056 in - if not (i3 = 256) then Fail Failure else Return () end end end - end end end + if not (i3 = 256) then Fail Failure else Return () + end (** Unit test for [hashmap::test1] *) let _ = assert_norm (test1_fwd = Return ()) diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 51021daf..7e1a7636 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -9,7 +9,8 @@ include HashmapMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap_main::hashmap::hash_key] *) -let hashmap_hash_key_fwd (k : usize) : result usize = Return 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_loop_fwd @@ -18,10 +19,10 @@ let rec hashmap_hash_map_allocate_slots_loop_fwd (decreases (hashmap_hash_map_allocate_slots_loop_decreases t slots n)) = if n > 0 - then begin + then let* slots0 = vec_push_back (hashmap_list_t t) slots HashmapListNil in let* n0 = usize_sub n 1 in - hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 end + hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 else Return slots (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) @@ -56,11 +57,11 @@ let rec hashmap_hash_map_clear_loop_fwd_back = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 - then begin + then let* i1 = usize_add i 1 in let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil in - hashmap_hash_map_clear_loop_fwd_back t slots0 i1 end + hashmap_hash_map_clear_loop_fwd_back t slots0 i1 else Return slots (** [hashmap_main::hashmap::HashMap::{0}::clear] *) @@ -105,9 +106,9 @@ let rec hashmap_hash_map_insert_in_list_loop_back | HashmapListCons ckey cvalue tl -> if ckey = key then Return (HashmapListCons ckey value tl) - else begin + else let* tl0 = hashmap_hash_map_insert_in_list_loop_back t key value tl in - Return (HashmapListCons ckey cvalue tl0) end + Return (HashmapListCons ckey cvalue tl0) | HashmapListNil -> let l = HashmapListNil in Return (HashmapListCons key value l) end @@ -132,22 +133,21 @@ let hashmap_hash_map_insert_no_resize_fwd_back in let* inserted = hashmap_hash_map_insert_in_list_fwd t key value l in if inserted - then begin + then let* i0 = usize_add self.hashmap_hash_map_num_entries 1 in let* l0 = hashmap_hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) end - else begin + self.hashmap_hash_map_max_load v) + else let* l0 = hashmap_hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in Return (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 (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -183,7 +183,7 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 - then begin + then let* l = vec_index_mut_fwd (hashmap_list_t t) slots i in let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in let* ntable0 = @@ -191,7 +191,7 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back let* i1 = usize_add i 1 in let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i l0 in - hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end + hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 else Return (ntable, slots) (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) @@ -211,14 +211,14 @@ let hashmap_hash_map_try_resize_fwd_back let (i, i0) = self.hashmap_hash_map_max_load_factor in let* i1 = usize_div n1 i in if capacity <= i1 - then begin + then let* i2 = usize_mul capacity 2 in let* ntable = hashmap_hash_map_new_with_capacity_fwd t i2 i i0 in let* (ntable0, _) = hashmap_hash_map_move_elements_fwd_back t ntable self.hashmap_hash_map_slots 0 in Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) - ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) end + ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) else Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) @@ -321,9 +321,9 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back | HashmapListCons ckey cvalue tl -> if ckey = key then Return (HashmapListCons ckey ret tl) - else begin + else let* tl0 = hashmap_hash_map_get_mut_in_list_loop_back t tl key ret in - Return (HashmapListCons ckey cvalue tl0) end + Return (HashmapListCons ckey cvalue tl0) | HashmapListNil -> Fail Failure end @@ -406,9 +406,9 @@ let rec hashmap_hash_map_remove_from_list_loop_back | HashmapListCons i cvalue tl0 -> Return tl0 | HashmapListNil -> Fail Failure end - else begin + else let* tl0 = hashmap_hash_map_remove_from_list_loop_back t key tl in - Return (HashmapListCons ckey x tl0) end + Return (HashmapListCons ckey x tl0) | HashmapListNil -> Return HashmapListNil end @@ -475,31 +475,31 @@ let hashmap_test1_fwd : result unit = let* i = hashmap_hash_map_get_fwd u64 hm3 128 in if not (i = 18) then Fail Failure - else begin + else let* hm4 = hashmap_hash_map_get_mut_back u64 hm3 1024 56 in let* i0 = hashmap_hash_map_get_fwd u64 hm4 1024 in if not (i0 = 56) then Fail Failure - else begin + else let* x = hashmap_hash_map_remove_fwd u64 hm4 1024 in begin match x with | None -> Fail Failure | Some x0 -> if not (x0 = 56) then Fail Failure - else begin + else let* hm5 = hashmap_hash_map_remove_back u64 hm4 1024 in let* i1 = hashmap_hash_map_get_fwd u64 hm5 0 in if not (i1 = 42) then Fail Failure - else begin + else let* i2 = hashmap_hash_map_get_fwd u64 hm5 128 in if not (i2 = 18) then Fail Failure - else begin + else let* i3 = hashmap_hash_map_get_fwd u64 hm5 1056 in - if not (i3 = 256) then Fail Failure else Return () end end end - end end end + if not (i3 = 256) then Fail Failure else Return () + end (** Unit test for [hashmap_main::hashmap::test1] *) let _ = assert_norm (hashmap_test1_fwd = Return ()) @@ -513,7 +513,8 @@ let insert_on_disk_fwd Return (st1, ()) (** [hashmap_main::main] *) -let main_fwd : result unit = Return () +let main_fwd : result unit = + Return () (** Unit test for [hashmap_main::main] *) let _ = assert_norm (main_fwd = Return ()) |