summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap/Hashmap.Funs.fst
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/hashmap/Hashmap.Funs.fst')
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst24
1 files changed, 12 insertions, 12 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 14cea9cb..2074d02e 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -14,7 +14,7 @@ let hash_key_fwd (k : usize) : result usize = Return k
let rec hash_map_allocate_slots_loop_fwd
(t : Type0) (slots : vec (list_t t)) (n : usize) :
Tot (result (vec (list_t t)))
- (decreases (hash_map_allocate_slots_decreases t slots n))
+ (decreases (hash_map_allocate_slots_loop_decreases t slots n))
=
if n > 0
then
@@ -62,7 +62,7 @@ let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
let rec hash_map_clear_slots_loop_fwd_back
(t : Type0) (slots : vec (list_t t)) (i : usize) :
Tot (result (vec (list_t t)))
- (decreases (hash_map_clear_slots_decreases t slots i))
+ (decreases (hash_map_clear_slots_loop_decreases t slots i))
=
let i0 = vec_len (list_t t) slots in
if i < i0
@@ -100,7 +100,7 @@ let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
let rec hash_map_insert_in_list_loop_fwd
(t : Type0) (key : usize) (value : t) (ls : list_t t) :
Tot (result bool)
- (decreases (hash_map_insert_in_list_decreases t key value ls))
+ (decreases (hash_map_insert_in_list_loop_decreases t key value ls))
=
begin match ls with
| ListCons ckey cvalue tl ->
@@ -119,7 +119,7 @@ let hash_map_insert_in_list_fwd
let rec hash_map_insert_in_list_loop_back
(t : Type0) (key : usize) (value : t) (ls : list_t t) :
Tot (result (list_t t))
- (decreases (hash_map_insert_in_list_decreases t key value ls))
+ (decreases (hash_map_insert_in_list_loop_decreases t key value ls))
=
begin match ls with
| ListCons ckey cvalue tl ->
@@ -201,7 +201,7 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
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))
- (decreases (hash_map_move_elements_from_list_decreases t ntable ls))
+ (decreases (hash_map_move_elements_from_list_loop_decreases t ntable ls))
=
begin match ls with
| ListCons k v tl ->
@@ -222,7 +222,7 @@ let hash_map_move_elements_from_list_fwd_back
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))))
- (decreases (hash_map_move_elements_decreases t ntable slots i))
+ (decreases (hash_map_move_elements_loop_decreases t ntable slots i))
=
let i0 = vec_len (list_t t) slots in
if i < i0
@@ -315,7 +315,7 @@ let hash_map_insert_fwd_back
let rec hash_map_contains_key_in_list_loop_fwd
(t : Type0) (key : usize) (ls : list_t t) :
Tot (result bool)
- (decreases (hash_map_contains_key_in_list_decreases t key ls))
+ (decreases (hash_map_contains_key_in_list_loop_decreases t key ls))
=
begin match ls with
| ListCons ckey x tl ->
@@ -350,7 +350,7 @@ let hash_map_contains_key_fwd
(** [hashmap::HashMap::{0}::get_in_list] *)
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_decreases t key ls))
+ Tot (result t) (decreases (hash_map_get_in_list_loop_decreases t key ls))
=
begin match ls with
| ListCons ckey cvalue tl ->
@@ -385,7 +385,7 @@ let hash_map_get_fwd
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
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_decreases t ls key))
+ Tot (result t) (decreases (hash_map_get_mut_in_list_loop_decreases t ls key))
=
begin match ls with
| ListCons ckey cvalue tl ->
@@ -404,7 +404,7 @@ let hash_map_get_mut_in_list_fwd
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))
- (decreases (hash_map_get_mut_in_list_decreases t ls key))
+ (decreases (hash_map_get_mut_in_list_loop_decreases t ls key))
=
begin match ls with
| ListCons ckey cvalue tl ->
@@ -476,7 +476,7 @@ let hash_map_get_mut_back
let rec hash_map_remove_from_list_loop_fwd
(t : Type0) (key : usize) (ls : list_t t) :
Tot (result (option t))
- (decreases (hash_map_remove_from_list_decreases t key ls))
+ (decreases (hash_map_remove_from_list_loop_decreases t key ls))
=
begin match ls with
| ListCons ckey x tl ->
@@ -500,7 +500,7 @@ let hash_map_remove_from_list_fwd
let rec hash_map_remove_from_list_loop_back
(t : Type0) (key : usize) (ls : list_t t) :
Tot (result (list_t t))
- (decreases (hash_map_remove_from_list_decreases t key ls))
+ (decreases (hash_map_remove_from_list_loop_decreases t key ls))
=
begin match ls with
| ListCons ckey x tl ->