summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap
diff options
context:
space:
mode:
authorSon HO2023-07-31 16:15:58 +0200
committerGitHub2023-07-31 16:15:58 +0200
commit887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (patch)
tree92d6021eb549f7cc25501856edd58859786b7e90 /tests/fstar/hashmap
parent53adf30fe440eb8b6f58ba89f4a4c0acc7877498 (diff)
parent9b3a58e423333fc9a4a5a264c3beb0a3d951e86b (diff)
Merge pull request #31 from AeneasVerif/son_lean_backend
Improve the Lean backend
Diffstat (limited to 'tests/fstar/hashmap')
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst85
1 files changed, 47 insertions, 38 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