From 5e92ae6b361f9221f5c5f9a39ab4c28a36597a77 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 11:40:59 +0100 Subject: Regenerate most of the test files --- tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 116 +++++++++++------------ 1 file changed, 58 insertions(+), 58 deletions(-) (limited to 'tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst') diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 5f227596..30bcfb2e 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -12,7 +12,7 @@ include HashmapMain.Clauses let hashmap_hash_key (k : usize) : result usize = Return k -(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: loop 0: forward function *) let rec hashmap_HashMap_allocate_slots_loop (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (n : usize) : Tot (result (alloc_vec_Vec (hashmap_List_t t))) @@ -26,14 +26,14 @@ let rec hashmap_HashMap_allocate_slots_loop hashmap_HashMap_allocate_slots_loop t slots0 n0 else Return slots -(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: forward function *) let hashmap_HashMap_allocate_slots (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (n : usize) : result (alloc_vec_Vec (hashmap_List_t t)) = hashmap_HashMap_allocate_slots_loop t slots n -(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new_with_capacity]: forward function *) let hashmap_HashMap_new_with_capacity (t : Type0) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : @@ -51,11 +51,11 @@ let hashmap_HashMap_new_with_capacity slots = slots } -(** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new]: forward function *) let hashmap_HashMap_new (t : Type0) : result (hashmap_HashMap_t t) = hashmap_HashMap_new_with_capacity t 32 4 5 -(** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec hashmap_HashMap_clear_loop (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : @@ -68,24 +68,24 @@ let rec hashmap_HashMap_clear_loop let* i1 = usize_add i 1 in let* slots0 = alloc_vec_Vec_index_mut_back (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t - t)) slots i Hashmap_List_Nil in + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) slots i + Hashmap_List_Nil in hashmap_HashMap_clear_loop t slots0 i1 else Return slots -(** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let hashmap_HashMap_clear (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = let* v = hashmap_HashMap_clear_loop t self.slots 0 in Return { self with num_entries = 0; slots = v } -(** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::len]: forward function *) let hashmap_HashMap_len (t : Type0) (self : hashmap_HashMap_t t) : result usize = Return self.num_entries -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: forward function *) let rec hashmap_HashMap_insert_in_list_loop (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : Tot (result bool) @@ -99,12 +99,12 @@ let rec hashmap_HashMap_insert_in_list_loop | Hashmap_List_Nil -> Return true end -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: forward function *) let hashmap_HashMap_insert_in_list (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : result bool = hashmap_HashMap_insert_in_list_loop t key value ls -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: backward function 0 *) let rec hashmap_HashMap_insert_in_list_loop_back (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : Tot (result (hashmap_List_t t)) @@ -121,14 +121,14 @@ let rec hashmap_HashMap_insert_in_list_loop_back let l = Hashmap_List_Nil in Return (Hashmap_List_Cons key value l) end -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: backward function 0 *) let hashmap_HashMap_insert_in_list_back (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : result (hashmap_List_t t) = hashmap_HashMap_insert_in_list_loop_back t key value ls -(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_no_resize]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let hashmap_HashMap_insert_no_resize (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) : @@ -139,7 +139,7 @@ let hashmap_HashMap_insert_no_resize let* hash_mod = usize_rem hash i in let* l = alloc_vec_Vec_index_mut (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t t)) + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in let* inserted = hashmap_HashMap_insert_in_list t key value l in if inserted @@ -148,18 +148,18 @@ let hashmap_HashMap_insert_no_resize let* l0 = hashmap_HashMap_insert_in_list_back t key value l in let* v = alloc_vec_Vec_index_mut_back (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t - t)) self.slots hash_mod l0 in + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) + self.slots hash_mod l0 in Return { self with num_entries = i0; slots = v } else let* l0 = hashmap_HashMap_insert_in_list_back t key value l in let* v = alloc_vec_Vec_index_mut_back (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t - t)) self.slots hash_mod l0 in + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) + self.slots hash_mod l0 in Return { self with slots = v } -(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec hashmap_HashMap_move_elements_from_list_loop (t : Type0) (ntable : hashmap_HashMap_t t) (ls : hashmap_List_t t) : @@ -174,7 +174,7 @@ let rec hashmap_HashMap_move_elements_from_list_loop | Hashmap_List_Nil -> Return ntable end -(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let hashmap_HashMap_move_elements_from_list (t : Type0) (ntable : hashmap_HashMap_t t) (ls : hashmap_List_t t) : @@ -182,7 +182,7 @@ let hashmap_HashMap_move_elements_from_list = hashmap_HashMap_move_elements_from_list_loop t ntable ls -(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec hashmap_HashMap_move_elements_loop (t : Type0) (ntable : hashmap_HashMap_t t) @@ -195,20 +195,20 @@ let rec hashmap_HashMap_move_elements_loop then let* l = alloc_vec_Vec_index_mut (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t - t)) slots i in + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) slots i + in let ls = core_mem_replace (hashmap_List_t t) l Hashmap_List_Nil in let* ntable0 = hashmap_HashMap_move_elements_from_list t ntable ls in let* i1 = usize_add i 1 in let l0 = core_mem_replace_back (hashmap_List_t t) l Hashmap_List_Nil in let* slots0 = alloc_vec_Vec_index_mut_back (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t - t)) slots i l0 in + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) slots i + l0 in hashmap_HashMap_move_elements_loop t ntable0 slots0 i1 else Return (ntable, slots) -(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let hashmap_HashMap_move_elements (t : Type0) (ntable : hashmap_HashMap_t t) @@ -217,7 +217,7 @@ let hashmap_HashMap_move_elements = hashmap_HashMap_move_elements_loop t ntable slots i -(** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::try_resize]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let hashmap_HashMap_try_resize (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = @@ -236,7 +236,7 @@ let hashmap_HashMap_try_resize } else Return { self with max_load_factor = (i, i0) } -(** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let hashmap_HashMap_insert (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) : @@ -248,7 +248,7 @@ let hashmap_HashMap_insert then hashmap_HashMap_try_resize t self0 else Return self0 -(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: loop 0: forward function *) let rec hashmap_HashMap_contains_key_in_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result bool) @@ -262,12 +262,12 @@ let rec hashmap_HashMap_contains_key_in_list_loop | Hashmap_List_Nil -> Return false end -(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: forward function *) let hashmap_HashMap_contains_key_in_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result bool = hashmap_HashMap_contains_key_in_list_loop t key ls -(** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key]: forward function *) let hashmap_HashMap_contains_key (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result bool = let* hash = hashmap_hash_key key in @@ -275,11 +275,11 @@ let hashmap_HashMap_contains_key let* hash_mod = usize_rem hash i in let* l = alloc_vec_Vec_index (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t t)) + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in hashmap_HashMap_contains_key_in_list t key l -(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: loop 0: forward function *) let rec hashmap_HashMap_get_in_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result t) @@ -293,12 +293,12 @@ let rec hashmap_HashMap_get_in_list_loop | Hashmap_List_Nil -> Fail Failure end -(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: forward function *) let hashmap_HashMap_get_in_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result t = hashmap_HashMap_get_in_list_loop t key ls -(** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get]: forward function *) let hashmap_HashMap_get (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result t = let* hash = hashmap_hash_key key in @@ -306,11 +306,11 @@ let hashmap_HashMap_get let* hash_mod = usize_rem hash i in let* l = alloc_vec_Vec_index (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t t)) + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in hashmap_HashMap_get_in_list t key l -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: loop 0: forward function *) let rec hashmap_HashMap_get_mut_in_list_loop (t : Type0) (ls : hashmap_List_t t) (key : usize) : Tot (result t) @@ -324,12 +324,12 @@ let rec hashmap_HashMap_get_mut_in_list_loop | Hashmap_List_Nil -> Fail Failure end -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: forward function *) let hashmap_HashMap_get_mut_in_list (t : Type0) (ls : hashmap_List_t t) (key : usize) : result t = hashmap_HashMap_get_mut_in_list_loop t ls key -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: loop 0: backward function 0 *) let rec hashmap_HashMap_get_mut_in_list_loop_back (t : Type0) (ls : hashmap_List_t t) (key : usize) (ret : t) : Tot (result (hashmap_List_t t)) @@ -345,14 +345,14 @@ let rec hashmap_HashMap_get_mut_in_list_loop_back | Hashmap_List_Nil -> Fail Failure end -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: backward function 0 *) let hashmap_HashMap_get_mut_in_list_back (t : Type0) (ls : hashmap_List_t t) (key : usize) (ret : t) : result (hashmap_List_t t) = hashmap_HashMap_get_mut_in_list_loop_back t ls key ret -(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: forward function *) let hashmap_HashMap_get_mut (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result t = let* hash = hashmap_hash_key key in @@ -360,11 +360,11 @@ let hashmap_HashMap_get_mut let* hash_mod = usize_rem hash i in let* l = alloc_vec_Vec_index_mut (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t t)) + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in hashmap_HashMap_get_mut_in_list t l key -(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: backward function 0 *) let hashmap_HashMap_get_mut_back (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (ret : t) : result (hashmap_HashMap_t t) @@ -374,16 +374,16 @@ let hashmap_HashMap_get_mut_back let* hash_mod = usize_rem hash i in let* l = alloc_vec_Vec_index_mut (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t t)) + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in let* l0 = hashmap_HashMap_get_mut_in_list_back t l key ret in let* v = alloc_vec_Vec_index_mut_back (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t t)) + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod l0 in Return { self with slots = v } -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: forward function *) let rec hashmap_HashMap_remove_from_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result (option t)) @@ -404,12 +404,12 @@ let rec hashmap_HashMap_remove_from_list_loop | Hashmap_List_Nil -> Return None end -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: forward function *) let hashmap_HashMap_remove_from_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result (option t) = hashmap_HashMap_remove_from_list_loop t key ls -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: backward function 1 *) let rec hashmap_HashMap_remove_from_list_loop_back (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result (hashmap_List_t t)) @@ -432,14 +432,14 @@ let rec hashmap_HashMap_remove_from_list_loop_back | Hashmap_List_Nil -> Return Hashmap_List_Nil end -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: backward function 1 *) let hashmap_HashMap_remove_from_list_back (t : Type0) (key : usize) (ls : hashmap_List_t t) : result (hashmap_List_t t) = hashmap_HashMap_remove_from_list_loop_back t key ls -(** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove]: forward function *) let hashmap_HashMap_remove (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result (option t) = let* hash = hashmap_hash_key key in @@ -447,7 +447,7 @@ let hashmap_HashMap_remove let* hash_mod = usize_rem hash i in let* l = alloc_vec_Vec_index_mut (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t t)) + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in let* x = hashmap_HashMap_remove_from_list t key l in begin match x with @@ -455,7 +455,7 @@ let hashmap_HashMap_remove | Some x0 -> let* _ = usize_sub self.num_entries 1 in Return (Some x0) end -(** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove]: backward function 0 *) let hashmap_HashMap_remove_back (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result (hashmap_HashMap_t t) @@ -465,7 +465,7 @@ let hashmap_HashMap_remove_back let* hash_mod = usize_rem hash i in let* l = alloc_vec_Vec_index_mut (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t t)) + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in let* x = hashmap_HashMap_remove_from_list t key l in begin match x with @@ -473,16 +473,16 @@ let hashmap_HashMap_remove_back let* l0 = hashmap_HashMap_remove_from_list_back t key l in let* v = alloc_vec_Vec_index_mut_back (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t - t)) self.slots hash_mod l0 in + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) + self.slots hash_mod l0 in Return { self with slots = v } | Some x0 -> let* i0 = usize_sub self.num_entries 1 in let* l0 = hashmap_HashMap_remove_from_list_back t key l in let* v = alloc_vec_Vec_index_mut_back (hashmap_List_t t) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (hashmap_List_t - t)) self.slots hash_mod l0 in + (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) + self.slots hash_mod l0 in Return { self with num_entries = i0; slots = v } end -- cgit v1.2.3 From 137cc7335e64fcb70c254e7fd2a6fa353fb43e61 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 14:57:38 +0100 Subject: Regenerate the files --- tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 120 +++++++++++++++-------- 1 file changed, 80 insertions(+), 40 deletions(-) (limited to 'tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst') diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 30bcfb2e..fa570309 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -8,11 +8,13 @@ include HashmapMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [hashmap_main::hashmap::hash_key]: forward function *) +(** [hashmap_main::hashmap::hash_key]: forward function + Source: 'src/hashmap.rs', lines 27:0-27:32 *) let hashmap_hash_key (k : usize) : result usize = Return k -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: loop 0: forward function + Source: 'src/hashmap.rs', lines 50:4-56:5 *) let rec hashmap_HashMap_allocate_slots_loop (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (n : usize) : Tot (result (alloc_vec_Vec (hashmap_List_t t))) @@ -26,14 +28,16 @@ let rec hashmap_HashMap_allocate_slots_loop hashmap_HashMap_allocate_slots_loop t slots0 n0 else Return slots -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: forward function + Source: 'src/hashmap.rs', lines 50:4-50:76 *) let hashmap_HashMap_allocate_slots (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (n : usize) : result (alloc_vec_Vec (hashmap_List_t t)) = hashmap_HashMap_allocate_slots_loop t slots n -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new_with_capacity]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new_with_capacity]: forward function + Source: 'src/hashmap.rs', lines 59:4-63:13 *) let hashmap_HashMap_new_with_capacity (t : Type0) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : @@ -51,12 +55,14 @@ let hashmap_HashMap_new_with_capacity slots = slots } -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new]: forward function + Source: 'src/hashmap.rs', lines 75:4-75:24 *) let hashmap_HashMap_new (t : Type0) : result (hashmap_HashMap_t t) = hashmap_HashMap_new_with_capacity t 32 4 5 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 80:4-88:5 *) let rec hashmap_HashMap_clear_loop (t : Type0) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : Tot (result (alloc_vec_Vec (hashmap_List_t t))) @@ -74,18 +80,21 @@ let rec hashmap_HashMap_clear_loop else Return slots (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 80:4-80:27 *) let hashmap_HashMap_clear (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = let* v = hashmap_HashMap_clear_loop t self.slots 0 in Return { self with num_entries = 0; slots = v } -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::len]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::len]: forward function + Source: 'src/hashmap.rs', lines 90:4-90:30 *) let hashmap_HashMap_len (t : Type0) (self : hashmap_HashMap_t t) : result usize = Return self.num_entries -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: forward function + Source: 'src/hashmap.rs', lines 97:4-114:5 *) let rec hashmap_HashMap_insert_in_list_loop (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : Tot (result bool) @@ -99,12 +108,14 @@ let rec hashmap_HashMap_insert_in_list_loop | Hashmap_List_Nil -> Return true end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: forward function + Source: 'src/hashmap.rs', lines 97:4-97:71 *) let hashmap_HashMap_insert_in_list (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : result bool = hashmap_HashMap_insert_in_list_loop t key value ls -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: backward function 0 + Source: 'src/hashmap.rs', lines 97:4-114:5 *) let rec hashmap_HashMap_insert_in_list_loop_back (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : Tot (result (hashmap_List_t t)) @@ -121,7 +132,8 @@ let rec hashmap_HashMap_insert_in_list_loop_back let l = Hashmap_List_Nil in Return (Hashmap_List_Cons key value l) end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: backward function 0 + Source: 'src/hashmap.rs', lines 97:4-97:71 *) let hashmap_HashMap_insert_in_list_back (t : Type0) (key : usize) (value : t) (ls : hashmap_List_t t) : result (hashmap_List_t t) @@ -129,7 +141,8 @@ let hashmap_HashMap_insert_in_list_back hashmap_HashMap_insert_in_list_loop_back t key value ls (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_no_resize]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 117:4-117:54 *) let hashmap_HashMap_insert_no_resize (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) : result (hashmap_HashMap_t t) @@ -160,7 +173,8 @@ let hashmap_HashMap_insert_no_resize Return { self with slots = v } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 183:4-196:5 *) let rec hashmap_HashMap_move_elements_from_list_loop (t : Type0) (ntable : hashmap_HashMap_t t) (ls : hashmap_List_t t) : Tot (result (hashmap_HashMap_t t)) @@ -175,7 +189,8 @@ let rec hashmap_HashMap_move_elements_from_list_loop end (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 183:4-183:72 *) let hashmap_HashMap_move_elements_from_list (t : Type0) (ntable : hashmap_HashMap_t t) (ls : hashmap_List_t t) : result (hashmap_HashMap_t t) @@ -183,7 +198,8 @@ let hashmap_HashMap_move_elements_from_list hashmap_HashMap_move_elements_from_list_loop t ntable ls (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 171:4-180:5 *) let rec hashmap_HashMap_move_elements_loop (t : Type0) (ntable : hashmap_HashMap_t t) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : @@ -209,7 +225,8 @@ let rec hashmap_HashMap_move_elements_loop else Return (ntable, slots) (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 171:4-171:95 *) let hashmap_HashMap_move_elements (t : Type0) (ntable : hashmap_HashMap_t t) (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) : @@ -218,7 +235,8 @@ let hashmap_HashMap_move_elements hashmap_HashMap_move_elements_loop t ntable slots i (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::try_resize]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 140:4-140:28 *) let hashmap_HashMap_try_resize (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = let* max_usize = scalar_cast U32 Usize core_u32_max in @@ -237,7 +255,8 @@ let hashmap_HashMap_try_resize else Return { self with max_load_factor = (i, i0) } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/hashmap.rs', lines 129:4-129:48 *) let hashmap_HashMap_insert (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) : result (hashmap_HashMap_t t) @@ -248,7 +267,8 @@ let hashmap_HashMap_insert then hashmap_HashMap_try_resize t self0 else Return self0 -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: loop 0: forward function + Source: 'src/hashmap.rs', lines 206:4-219:5 *) let rec hashmap_HashMap_contains_key_in_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result bool) @@ -262,12 +282,14 @@ let rec hashmap_HashMap_contains_key_in_list_loop | Hashmap_List_Nil -> Return false end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: forward function + Source: 'src/hashmap.rs', lines 206:4-206:68 *) let hashmap_HashMap_contains_key_in_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result bool = hashmap_HashMap_contains_key_in_list_loop t key ls -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key]: forward function + Source: 'src/hashmap.rs', lines 199:4-199:49 *) let hashmap_HashMap_contains_key (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result bool = let* hash = hashmap_hash_key key in @@ -279,7 +301,8 @@ let hashmap_HashMap_contains_key self.slots hash_mod in hashmap_HashMap_contains_key_in_list t key l -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: loop 0: forward function + Source: 'src/hashmap.rs', lines 224:4-237:5 *) let rec hashmap_HashMap_get_in_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result t) @@ -293,12 +316,14 @@ let rec hashmap_HashMap_get_in_list_loop | Hashmap_List_Nil -> Fail Failure end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: forward function + Source: 'src/hashmap.rs', lines 224:4-224:70 *) let hashmap_HashMap_get_in_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result t = hashmap_HashMap_get_in_list_loop t key ls -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get]: forward function + Source: 'src/hashmap.rs', lines 239:4-239:55 *) let hashmap_HashMap_get (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result t = let* hash = hashmap_hash_key key in @@ -310,7 +335,8 @@ let hashmap_HashMap_get self.slots hash_mod in hashmap_HashMap_get_in_list t key l -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: loop 0: forward function + Source: 'src/hashmap.rs', lines 245:4-254:5 *) let rec hashmap_HashMap_get_mut_in_list_loop (t : Type0) (ls : hashmap_List_t t) (key : usize) : Tot (result t) @@ -324,12 +350,14 @@ let rec hashmap_HashMap_get_mut_in_list_loop | Hashmap_List_Nil -> Fail Failure end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: forward function + Source: 'src/hashmap.rs', lines 245:4-245:86 *) let hashmap_HashMap_get_mut_in_list (t : Type0) (ls : hashmap_List_t t) (key : usize) : result t = hashmap_HashMap_get_mut_in_list_loop t ls key -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: loop 0: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: loop 0: backward function 0 + Source: 'src/hashmap.rs', lines 245:4-254:5 *) let rec hashmap_HashMap_get_mut_in_list_loop_back (t : Type0) (ls : hashmap_List_t t) (key : usize) (ret : t) : Tot (result (hashmap_List_t t)) @@ -345,14 +373,16 @@ let rec hashmap_HashMap_get_mut_in_list_loop_back | Hashmap_List_Nil -> Fail Failure end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: backward function 0 + Source: 'src/hashmap.rs', lines 245:4-245:86 *) let hashmap_HashMap_get_mut_in_list_back (t : Type0) (ls : hashmap_List_t t) (key : usize) (ret : t) : result (hashmap_List_t t) = hashmap_HashMap_get_mut_in_list_loop_back t ls key ret -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: forward function + Source: 'src/hashmap.rs', lines 257:4-257:67 *) let hashmap_HashMap_get_mut (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result t = let* hash = hashmap_hash_key key in @@ -364,7 +394,8 @@ let hashmap_HashMap_get_mut self.slots hash_mod in hashmap_HashMap_get_mut_in_list t l key -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: backward function 0 + Source: 'src/hashmap.rs', lines 257:4-257:67 *) let hashmap_HashMap_get_mut_back (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (ret : t) : result (hashmap_HashMap_t t) @@ -383,7 +414,8 @@ let hashmap_HashMap_get_mut_back self.slots hash_mod l0 in Return { self with slots = v } -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: forward function + Source: 'src/hashmap.rs', lines 265:4-291:5 *) let rec hashmap_HashMap_remove_from_list_loop (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result (option t)) @@ -404,12 +436,14 @@ let rec hashmap_HashMap_remove_from_list_loop | Hashmap_List_Nil -> Return None end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: forward function + Source: 'src/hashmap.rs', lines 265:4-265:69 *) let hashmap_HashMap_remove_from_list (t : Type0) (key : usize) (ls : hashmap_List_t t) : result (option t) = hashmap_HashMap_remove_from_list_loop t key ls -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: backward function 1 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: backward function 1 + Source: 'src/hashmap.rs', lines 265:4-291:5 *) let rec hashmap_HashMap_remove_from_list_loop_back (t : Type0) (key : usize) (ls : hashmap_List_t t) : Tot (result (hashmap_List_t t)) @@ -432,14 +466,16 @@ let rec hashmap_HashMap_remove_from_list_loop_back | Hashmap_List_Nil -> Return Hashmap_List_Nil end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: backward function 1 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: backward function 1 + Source: 'src/hashmap.rs', lines 265:4-265:69 *) let hashmap_HashMap_remove_from_list_back (t : Type0) (key : usize) (ls : hashmap_List_t t) : result (hashmap_List_t t) = hashmap_HashMap_remove_from_list_loop_back t key ls -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove]: forward function *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove]: forward function + Source: 'src/hashmap.rs', lines 294:4-294:52 *) let hashmap_HashMap_remove (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result (option t) = let* hash = hashmap_hash_key key in @@ -455,7 +491,8 @@ let hashmap_HashMap_remove | Some x0 -> let* _ = usize_sub self.num_entries 1 in Return (Some x0) end -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove]: backward function 0 *) +(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove]: backward function 0 + Source: 'src/hashmap.rs', lines 294:4-294:52 *) let hashmap_HashMap_remove_back (t : Type0) (self : hashmap_HashMap_t t) (key : usize) : result (hashmap_HashMap_t t) @@ -486,7 +523,8 @@ let hashmap_HashMap_remove_back Return { self with num_entries = i0; slots = v } end -(** [hashmap_main::hashmap::test1]: forward function *) +(** [hashmap_main::hashmap::test1]: forward function + Source: 'src/hashmap.rs', lines 315:0-315:10 *) let hashmap_test1 : result unit = let* hm = hashmap_HashMap_new u64 in let* hm0 = hashmap_HashMap_insert u64 hm 0 42 in @@ -522,7 +560,8 @@ let hashmap_test1 : result unit = if not (i3 = 256) then Fail Failure else Return () end -(** [hashmap_main::insert_on_disk]: forward function *) +(** [hashmap_main::insert_on_disk]: forward function + Source: 'src/hashmap_main.rs', lines 7:0-7:43 *) let insert_on_disk (key : usize) (value : u64) (st : state) : result (state & unit) = let* (st0, hm) = hashmap_utils_deserialize st in @@ -530,7 +569,8 @@ let insert_on_disk let* (st1, _) = hashmap_utils_serialize hm0 st0 in Return (st1, ()) -(** [hashmap_main::main]: forward function *) +(** [hashmap_main::main]: forward function + Source: 'src/hashmap_main.rs', lines 16:0-16:13 *) let main : result unit = Return () -- cgit v1.2.3