summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst85
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst89
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti6
3 files changed, 99 insertions, 81 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 44ad7463..950f1490 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -7,11 +7,11 @@ include Hashmap.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [hashmap::hash_key] *)
+(** [hashmap::hash_key]: forward function *)
let hash_key_fwd (k : usize) : result usize =
Return k
-(** [hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
let rec hash_map_allocate_slots_loop_fwd
(t : Type0) (slots : vec (list_t t)) (n : usize) :
Tot (result (vec (list_t t)))
@@ -24,12 +24,12 @@ let rec hash_map_allocate_slots_loop_fwd
hash_map_allocate_slots_loop_fwd t slots0 n0
else Return slots
-(** [hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots]: forward function *)
let hash_map_allocate_slots_fwd
(t : Type0) (slots : vec (list_t t)) (n : usize) : result (vec (list_t t)) =
hash_map_allocate_slots_loop_fwd t slots n
-(** [hashmap::HashMap::{0}::new_with_capacity] *)
+(** [hashmap::HashMap::{0}::new_with_capacity]: forward function *)
let hash_map_new_with_capacity_fwd
(t : Type0) (capacity : usize) (max_load_dividend : usize)
(max_load_divisor : usize) :
@@ -47,11 +47,12 @@ let hash_map_new_with_capacity_fwd
hash_map_slots = slots
}
-(** [hashmap::HashMap::{0}::new] *)
+(** [hashmap::HashMap::{0}::new]: forward function *)
let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
hash_map_new_with_capacity_fwd t 32 4 5
-(** [hashmap::HashMap::{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let rec hash_map_clear_loop_fwd_back
(t : Type0) (slots : vec (list_t t)) (i : usize) :
Tot (result (vec (list_t t)))
@@ -65,17 +66,18 @@ let rec hash_map_clear_loop_fwd_back
hash_map_clear_loop_fwd_back t slots0 i1
else Return slots
-(** [hashmap::HashMap::{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hash_map_clear_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
let* v = hash_map_clear_loop_fwd_back t self.hash_map_slots 0 in
Return { self with hash_map_num_entries = 0; hash_map_slots = v }
-(** [hashmap::HashMap::{0}::len] *)
+(** [hashmap::HashMap::{0}::len]: forward function *)
let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
Return self.hash_map_num_entries
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
let rec hash_map_insert_in_list_loop_fwd
(t : Type0) (key : usize) (value : t) (ls : list_t t) :
Tot (result bool)
@@ -89,12 +91,12 @@ let rec hash_map_insert_in_list_loop_fwd
| ListNil -> Return true
end
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: forward function *)
let hash_map_insert_in_list_fwd
(t : Type0) (key : usize) (value : t) (ls : list_t t) : result bool =
hash_map_insert_in_list_loop_fwd t key value ls
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
let rec hash_map_insert_in_list_loop_back
(t : Type0) (key : usize) (value : t) (ls : list_t t) :
Tot (result (list_t t))
@@ -110,12 +112,13 @@ let rec hash_map_insert_in_list_loop_back
| ListNil -> let l = ListNil in Return (ListCons key value l)
end
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
let hash_map_insert_in_list_back
(t : Type0) (key : usize) (value : t) (ls : list_t t) : result (list_t t) =
hash_map_insert_in_list_loop_back t key value ls
-(** [hashmap::HashMap::{0}::insert_no_resize] *)
+(** [hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hash_map_insert_no_resize_fwd_back
(t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
result (hash_map_t t)
@@ -140,7 +143,8 @@ let hash_map_insert_no_resize_fwd_back
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
-(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let rec hash_map_move_elements_from_list_loop_fwd_back
(t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
Tot (result (hash_map_t t))
@@ -153,12 +157,14 @@ let rec hash_map_move_elements_from_list_loop_fwd_back
| ListNil -> Return ntable
end
-(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hash_map_move_elements_from_list_fwd_back
(t : Type0) (ntable : hash_map_t t) (ls : list_t t) : result (hash_map_t t) =
hash_map_move_elements_from_list_loop_fwd_back t ntable ls
-(** [hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let rec hash_map_move_elements_loop_fwd_back
(t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
Tot (result ((hash_map_t t) & (vec (list_t t))))
@@ -176,14 +182,16 @@ let rec hash_map_move_elements_loop_fwd_back
hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
else Return (ntable, slots)
-(** [hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hash_map_move_elements_fwd_back
(t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
result ((hash_map_t t) & (vec (list_t t)))
=
hash_map_move_elements_loop_fwd_back t ntable slots i
-(** [hashmap::HashMap::{0}::try_resize] *)
+(** [hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hash_map_try_resize_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
@@ -206,7 +214,8 @@ let hash_map_try_resize_fwd_back
}
else Return { self with hash_map_max_load_factor = (i, i0) }
-(** [hashmap::HashMap::{0}::insert] *)
+(** [hashmap::HashMap::{0}::insert]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hash_map_insert_fwd_back
(t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
result (hash_map_t t)
@@ -217,7 +226,7 @@ let hash_map_insert_fwd_back
then hash_map_try_resize_fwd_back t self0
else Return self0
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
let rec hash_map_contains_key_in_list_loop_fwd
(t : Type0) (key : usize) (ls : list_t t) :
Tot (result bool)
@@ -231,12 +240,12 @@ let rec hash_map_contains_key_in_list_loop_fwd
| ListNil -> Return false
end
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
let hash_map_contains_key_in_list_fwd
(t : Type0) (key : usize) (ls : list_t t) : result bool =
hash_map_contains_key_in_list_loop_fwd t key ls
-(** [hashmap::HashMap::{0}::contains_key] *)
+(** [hashmap::HashMap::{0}::contains_key]: forward function *)
let hash_map_contains_key_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result bool =
let* hash = hash_key_fwd key in
@@ -245,7 +254,7 @@ let hash_map_contains_key_fwd
let* l = vec_index_fwd (list_t t) self.hash_map_slots hash_mod in
hash_map_contains_key_in_list_fwd t key l
-(** [hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
let rec hash_map_get_in_list_loop_fwd
(t : Type0) (key : usize) (ls : list_t t) :
Tot (result t) (decreases (hash_map_get_in_list_loop_decreases t key ls))
@@ -258,12 +267,12 @@ let rec hash_map_get_in_list_loop_fwd
| ListNil -> Fail Failure
end
-(** [hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list]: forward function *)
let hash_map_get_in_list_fwd
(t : Type0) (key : usize) (ls : list_t t) : result t =
hash_map_get_in_list_loop_fwd t key ls
-(** [hashmap::HashMap::{0}::get] *)
+(** [hashmap::HashMap::{0}::get]: forward function *)
let hash_map_get_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result t =
let* hash = hash_key_fwd key in
@@ -272,7 +281,7 @@ let hash_map_get_fwd
let* l = vec_index_fwd (list_t t) self.hash_map_slots hash_mod in
hash_map_get_in_list_fwd t key l
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
let rec hash_map_get_mut_in_list_loop_fwd
(t : Type0) (ls : list_t t) (key : usize) :
Tot (result t) (decreases (hash_map_get_mut_in_list_loop_decreases t ls key))
@@ -285,12 +294,12 @@ let rec hash_map_get_mut_in_list_loop_fwd
| ListNil -> Fail Failure
end
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
let hash_map_get_mut_in_list_fwd
(t : Type0) (ls : list_t t) (key : usize) : result t =
hash_map_get_mut_in_list_loop_fwd t ls key
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
let rec hash_map_get_mut_in_list_loop_back
(t : Type0) (ls : list_t t) (key : usize) (ret : t) :
Tot (result (list_t t))
@@ -306,12 +315,12 @@ let rec hash_map_get_mut_in_list_loop_back
| ListNil -> Fail Failure
end
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
let hash_map_get_mut_in_list_back
(t : Type0) (ls : list_t t) (key : usize) (ret : t) : result (list_t t) =
hash_map_get_mut_in_list_loop_back t ls key ret
-(** [hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut]: forward function *)
let hash_map_get_mut_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result t =
let* hash = hash_key_fwd key in
@@ -320,7 +329,7 @@ let hash_map_get_mut_fwd
let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in
hash_map_get_mut_in_list_fwd t l key
-(** [hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut]: backward function 0 *)
let hash_map_get_mut_back
(t : Type0) (self : hash_map_t t) (key : usize) (ret : t) :
result (hash_map_t t)
@@ -333,7 +342,7 @@ let hash_map_get_mut_back
let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
Return { self with hash_map_slots = v }
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
let rec hash_map_remove_from_list_loop_fwd
(t : Type0) (key : usize) (ls : list_t t) :
Tot (result (option t))
@@ -352,12 +361,12 @@ let rec hash_map_remove_from_list_loop_fwd
| ListNil -> Return None
end
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: forward function *)
let hash_map_remove_from_list_fwd
(t : Type0) (key : usize) (ls : list_t t) : result (option t) =
hash_map_remove_from_list_loop_fwd t key ls
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
let rec hash_map_remove_from_list_loop_back
(t : Type0) (key : usize) (ls : list_t t) :
Tot (result (list_t t))
@@ -378,12 +387,12 @@ let rec hash_map_remove_from_list_loop_back
| ListNil -> Return ListNil
end
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
let hash_map_remove_from_list_back
(t : Type0) (key : usize) (ls : list_t t) : result (list_t t) =
hash_map_remove_from_list_loop_back t key ls
-(** [hashmap::HashMap::{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove]: forward function *)
let hash_map_remove_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
let* hash = hash_key_fwd key in
@@ -397,7 +406,7 @@ let hash_map_remove_fwd
let* _ = usize_sub self.hash_map_num_entries 1 in Return (Some x0)
end
-(** [hashmap::HashMap::{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove]: backward function 0 *)
let hash_map_remove_back
(t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) =
let* hash = hash_key_fwd key in
@@ -417,7 +426,7 @@ let hash_map_remove_back
Return { self with hash_map_num_entries = i0; hash_map_slots = v }
end
-(** [hashmap::test1] *)
+(** [hashmap::test1]: forward function *)
let test1_fwd : result unit =
let* hm = hash_map_new_fwd u64 in
let* hm0 = hash_map_insert_fwd_back u64 hm 0 42 in
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index e8cd54c1..f6d9c8cf 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -8,11 +8,11 @@ include HashmapMain.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [hashmap_main::hashmap::hash_key] *)
+(** [hashmap_main::hashmap::hash_key]: forward function *)
let hashmap_hash_key_fwd (k : usize) : result usize =
Return k
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
let rec hashmap_hash_map_allocate_slots_loop_fwd
(t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
Tot (result (vec (hashmap_list_t t)))
@@ -25,14 +25,14 @@ let rec hashmap_hash_map_allocate_slots_loop_fwd
hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0
else Return slots
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *)
let hashmap_hash_map_allocate_slots_fwd
(t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
result (vec (hashmap_list_t t))
=
hashmap_hash_map_allocate_slots_loop_fwd t slots n
-(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
+(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *)
let hashmap_hash_map_new_with_capacity_fwd
(t : Type0) (capacity : usize) (max_load_dividend : usize)
(max_load_divisor : usize) :
@@ -50,11 +50,12 @@ let hashmap_hash_map_new_with_capacity_fwd
hashmap_hash_map_slots = slots
}
-(** [hashmap_main::hashmap::HashMap::{0}::new] *)
+(** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *)
let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
hashmap_hash_map_new_with_capacity_fwd t 32 4 5
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let rec hashmap_hash_map_clear_loop_fwd_back
(t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) :
Tot (result (vec (hashmap_list_t t)))
@@ -69,7 +70,8 @@ let rec hashmap_hash_map_clear_loop_fwd_back
hashmap_hash_map_clear_loop_fwd_back t slots0 i1
else Return slots
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hashmap_hash_map_clear_fwd_back
(t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0
@@ -77,12 +79,12 @@ let hashmap_hash_map_clear_fwd_back
Return
{ self with hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v }
-(** [hashmap_main::hashmap::HashMap::{0}::len] *)
+(** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *)
let hashmap_hash_map_len_fwd
(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] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
let rec hashmap_hash_map_insert_in_list_loop_fwd
(t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
Tot (result bool)
@@ -96,12 +98,12 @@ let rec hashmap_hash_map_insert_in_list_loop_fwd
| HashmapListNil -> Return true
end
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *)
let hashmap_hash_map_insert_in_list_fwd
(t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : result bool =
hashmap_hash_map_insert_in_list_loop_fwd t key value ls
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
let rec hashmap_hash_map_insert_in_list_loop_back
(t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
Tot (result (hashmap_list_t t))
@@ -118,14 +120,15 @@ let rec hashmap_hash_map_insert_in_list_loop_back
let l = HashmapListNil in Return (HashmapListCons key value l)
end
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
let hashmap_hash_map_insert_in_list_back
(t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
result (hashmap_list_t t)
=
hashmap_hash_map_insert_in_list_loop_back t key value ls
-(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
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)
@@ -158,7 +161,8 @@ let hashmap_hash_map_insert_no_resize_fwd_back
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
(t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
Tot (result (hashmap_hash_map_t t))
@@ -172,14 +176,16 @@ let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
| HashmapListNil -> Return ntable
end
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hashmap_hash_map_move_elements_from_list_fwd_back
(t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
result (hashmap_hash_map_t t)
=
hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable ls
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let rec hashmap_hash_map_move_elements_loop_fwd_back
(t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
(i : usize) :
@@ -199,7 +205,8 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back
hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
else Return (ntable, slots)
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hashmap_hash_map_move_elements_fwd_back
(t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
(i : usize) :
@@ -207,7 +214,8 @@ let hashmap_hash_map_move_elements_fwd_back
=
hashmap_hash_map_move_elements_loop_fwd_back t ntable slots i
-(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
+(** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
let hashmap_hash_map_try_resize_fwd_back
(t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
@@ -231,7 +239,8 @@ let hashmap_hash_map_try_resize_fwd_back
}
else Return { self with hashmap_hash_map_max_load_factor = (i, i0) }
-(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
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)
@@ -242,7 +251,7 @@ let hashmap_hash_map_insert_fwd_back
then hashmap_hash_map_try_resize_fwd_back t self0
else Return self0
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
let rec hashmap_hash_map_contains_key_in_list_loop_fwd
(t : Type0) (key : usize) (ls : hashmap_list_t t) :
Tot (result bool)
@@ -256,12 +265,12 @@ let rec hashmap_hash_map_contains_key_in_list_loop_fwd
| HashmapListNil -> Return false
end
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
let hashmap_hash_map_contains_key_in_list_fwd
(t : Type0) (key : usize) (ls : hashmap_list_t t) : result bool =
hashmap_hash_map_contains_key_in_list_loop_fwd t key ls
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *)
let hashmap_hash_map_contains_key_fwd
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool =
let* hash = hashmap_hash_key_fwd key in
@@ -271,7 +280,7 @@ let hashmap_hash_map_contains_key_fwd
vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in
hashmap_hash_map_contains_key_in_list_fwd t key l
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
let rec hashmap_hash_map_get_in_list_loop_fwd
(t : Type0) (key : usize) (ls : hashmap_list_t t) :
Tot (result t)
@@ -285,12 +294,12 @@ let rec hashmap_hash_map_get_in_list_loop_fwd
| HashmapListNil -> Fail Failure
end
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *)
let hashmap_hash_map_get_in_list_fwd
(t : Type0) (key : usize) (ls : hashmap_list_t t) : result t =
hashmap_hash_map_get_in_list_loop_fwd t key ls
-(** [hashmap_main::hashmap::HashMap::{0}::get] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *)
let hashmap_hash_map_get_fwd
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
let* hash = hashmap_hash_key_fwd key in
@@ -300,7 +309,7 @@ let hashmap_hash_map_get_fwd
vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in
hashmap_hash_map_get_in_list_fwd t key l
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
let rec hashmap_hash_map_get_mut_in_list_loop_fwd
(t : Type0) (ls : hashmap_list_t t) (key : usize) :
Tot (result t)
@@ -314,12 +323,12 @@ let rec hashmap_hash_map_get_mut_in_list_loop_fwd
| HashmapListNil -> Fail Failure
end
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
let hashmap_hash_map_get_mut_in_list_fwd
(t : Type0) (ls : hashmap_list_t t) (key : usize) : result t =
hashmap_hash_map_get_mut_in_list_loop_fwd t ls key
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
let rec hashmap_hash_map_get_mut_in_list_loop_back
(t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
Tot (result (hashmap_list_t t))
@@ -335,14 +344,14 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back
| HashmapListNil -> Fail Failure
end
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
let hashmap_hash_map_get_mut_in_list_back
(t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
result (hashmap_list_t t)
=
hashmap_hash_map_get_mut_in_list_loop_back t ls key ret
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *)
let hashmap_hash_map_get_mut_fwd
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
let* hash = hashmap_hash_key_fwd key in
@@ -353,7 +362,7 @@ let hashmap_hash_map_get_mut_fwd
in
hashmap_hash_map_get_mut_in_list_fwd t l key
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *)
let hashmap_hash_map_get_mut_back
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) :
result (hashmap_hash_map_t t)
@@ -370,7 +379,7 @@ let hashmap_hash_map_get_mut_back
l0 in
Return { self with hashmap_hash_map_slots = v }
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
let rec hashmap_hash_map_remove_from_list_loop_fwd
(t : Type0) (key : usize) (ls : hashmap_list_t t) :
Tot (result (option t))
@@ -391,12 +400,12 @@ let rec hashmap_hash_map_remove_from_list_loop_fwd
| HashmapListNil -> Return None
end
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *)
let hashmap_hash_map_remove_from_list_fwd
(t : Type0) (key : usize) (ls : hashmap_list_t t) : result (option t) =
hashmap_hash_map_remove_from_list_loop_fwd t key ls
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
let rec hashmap_hash_map_remove_from_list_loop_back
(t : Type0) (key : usize) (ls : hashmap_list_t t) :
Tot (result (hashmap_list_t t))
@@ -419,14 +428,14 @@ let rec hashmap_hash_map_remove_from_list_loop_back
| HashmapListNil -> Return HashmapListNil
end
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
let hashmap_hash_map_remove_from_list_back
(t : Type0) (key : usize) (ls : hashmap_list_t t) :
result (hashmap_list_t t)
=
hashmap_hash_map_remove_from_list_loop_back t key ls
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *)
let hashmap_hash_map_remove_fwd
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) =
let* hash = hashmap_hash_key_fwd key in
@@ -442,7 +451,7 @@ let hashmap_hash_map_remove_fwd
let* _ = usize_sub self.hashmap_hash_map_num_entries 1 in Return (Some x0)
end
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *)
let hashmap_hash_map_remove_back
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) :
result (hashmap_hash_map_t t)
@@ -472,7 +481,7 @@ let hashmap_hash_map_remove_back
}
end
-(** [hashmap_main::hashmap::test1] *)
+(** [hashmap_main::hashmap::test1]: forward function *)
let hashmap_test1_fwd : result unit =
let* hm = hashmap_hash_map_new_fwd u64 in
let* hm0 = hashmap_hash_map_insert_fwd_back u64 hm 0 42 in
@@ -511,7 +520,7 @@ let hashmap_test1_fwd : result unit =
(** Unit test for [hashmap_main::hashmap::test1] *)
let _ = assert_norm (hashmap_test1_fwd = Return ())
-(** [hashmap_main::insert_on_disk] *)
+(** [hashmap_main::insert_on_disk]: forward function *)
let insert_on_disk_fwd
(key : usize) (value : u64) (st : state) : result (state & unit) =
let* (st0, hm) = hashmap_utils_deserialize_fwd st in
@@ -519,7 +528,7 @@ let insert_on_disk_fwd
let* (st1, _) = hashmap_utils_serialize_fwd hm0 st0 in
Return (st1, ())
-(** [hashmap_main::main] *)
+(** [hashmap_main::main]: forward function *)
let main_fwd : result unit =
Return ()
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
index 6e54ea10..78a6c3ba 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
@@ -1,16 +1,16 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: opaque function definitions *)
+(** [hashmap_main]: external function declarations *)
module HashmapMain.Opaque
open Primitives
include HashmapMain.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [hashmap_main::hashmap_utils::deserialize] *)
+(** [hashmap_main::hashmap_utils::deserialize]: forward function *)
val hashmap_utils_deserialize_fwd
: state -> result (state & (hashmap_hash_map_t u64))
-(** [hashmap_main::hashmap_utils::serialize] *)
+(** [hashmap_main::hashmap_utils::serialize]: forward function *)
val hashmap_utils_serialize_fwd
: hashmap_hash_map_t u64 -> state -> result (state & unit)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 06:28:02 +0000