summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst200
-rw-r--r--tests/fstar/hashmap/Hashmap.Properties.fst260
-rw-r--r--tests/fstar/hashmap/Hashmap.Properties.fsti20
-rw-r--r--tests/fstar/hashmap/Primitives.fst32
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst206
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst8
-rw-r--r--tests/fstar/hashmap_on_disk/Primitives.fst32
7 files changed, 383 insertions, 375 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 6e67fca4..e3ae587f 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -20,13 +20,13 @@ let rec hash_map_allocate_slots_fwd
then Return slots
else
begin match vec_push_back (list_t t) slots ListNil with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots0 ->
begin match usize_sub n 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
begin match hash_map_allocate_slots_fwd t slots0 i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v -> Return v
end
end
@@ -40,13 +40,13 @@ let hash_map_new_with_capacity_fwd
=
let v = vec_new (list_t t) in
begin match hash_map_allocate_slots_fwd t v capacity with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots ->
begin match usize_mul capacity max_load_dividend with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
begin match usize_div i max_load_divisor with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots)
end
@@ -56,7 +56,7 @@ let hash_map_new_with_capacity_fwd
(** [hashmap::HashMap::{0}::new] *)
let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
begin match hash_map_new_with_capacity_fwd t 32 4 5 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm -> Return hm
end
@@ -70,13 +70,13 @@ let rec hash_map_clear_slots_fwd_back
if i < i0
then
begin match vec_index_mut_back (list_t t) slots i ListNil with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots0 ->
begin match usize_add i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
begin match hash_map_clear_slots_fwd_back t slots0 i1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots1 -> Return slots1
end
end
@@ -87,7 +87,7 @@ let rec hash_map_clear_slots_fwd_back
let hash_map_clear_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load
v)
@@ -109,7 +109,7 @@ let rec hash_map_insert_in_list_fwd
then Return false
else
begin match hash_map_insert_in_list_fwd t key value ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b -> Return b
end
| ListNil -> Return true
@@ -127,7 +127,7 @@ let rec hash_map_insert_in_list_back
then Return (ListCons ckey value ls0)
else
begin match hash_map_insert_in_list_back t key value ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ls1 -> Return (ListCons ckey cvalue ls1)
end
| ListNil -> let l = ListNil in Return (ListCons key value l)
@@ -139,31 +139,31 @@ let hash_map_insert_no_resize_fwd_back
result (hash_map_t t)
=
begin match hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (list_t t) self.hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hash_map_insert_in_list_fwd t key value l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return inserted ->
if inserted
then
begin match usize_add self.hash_map_num_entries 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match hash_map_insert_in_list_back t key value l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhash_map_t i0 self.hash_map_max_load_factor
self.hash_map_max_load v)
@@ -172,12 +172,12 @@ let hash_map_insert_no_resize_fwd_back
end
else
begin match hash_map_insert_in_list_back t key value l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhash_map_t self.hash_map_num_entries
self.hash_map_max_load_factor self.hash_map_max_load v)
@@ -201,10 +201,10 @@ let rec hash_map_move_elements_from_list_fwd_back
begin match ls with
| ListCons k v tl ->
begin match hash_map_insert_no_resize_fwd_back t ntable k v with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable0 ->
begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable1 -> Return ntable1
end
end
@@ -221,22 +221,22 @@ let rec hash_map_move_elements_fwd_back
if i < i0
then
begin match vec_index_mut_fwd (list_t t) slots i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
let ls = mem_replace_fwd (list_t t) l ListNil in
begin match hash_map_move_elements_from_list_fwd_back t ntable ls with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable0 ->
let l0 = mem_replace_back (list_t t) l ListNil in
begin match vec_index_mut_back (list_t t) slots i l0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots0 ->
begin match usize_add i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (ntable1, slots1) -> Return (ntable1, slots1)
end
end
@@ -249,28 +249,28 @@ let rec hash_map_move_elements_fwd_back
let hash_map_try_resize_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
begin match scalar_cast U32 Usize core_num_u32_max_c with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return max_usize ->
let capacity = vec_len (list_t t) self.hash_map_slots in
begin match usize_div max_usize 2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return n1 ->
let (i, i0) = self.hash_map_max_load_factor in
begin match usize_div n1 i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
if capacity <= i1
then
begin match usize_mul capacity 2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i2 ->
begin match hash_map_new_with_capacity_fwd t i2 i i0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable ->
begin match
hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (ntable0, _) ->
Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
ntable0.hash_map_max_load ntable0.hash_map_slots)
@@ -290,15 +290,15 @@ let hash_map_insert_fwd_back
result (hash_map_t t)
=
begin match hash_map_insert_no_resize_fwd_back t self key value with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return self0 ->
begin match hash_map_len_fwd t self0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
if i > self0.hash_map_max_load
then
begin match hash_map_try_resize_fwd_back t self0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return self1 -> Return self1
end
else Return self0
@@ -317,7 +317,7 @@ let rec hash_map_contains_key_in_list_fwd
then Return true
else
begin match hash_map_contains_key_in_list_fwd t key ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b -> Return b
end
| ListNil -> Return false
@@ -327,17 +327,17 @@ let rec hash_map_contains_key_in_list_fwd
let hash_map_contains_key_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result bool =
begin match hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (list_t t) self.hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hash_map_contains_key_in_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b -> Return b
end
end
@@ -355,27 +355,27 @@ let rec hash_map_get_in_list_fwd
then Return cvalue
else
begin match hash_map_get_in_list_fwd t key ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x -> Return x
end
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
(** [hashmap::HashMap::{0}::get] *)
let hash_map_get_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result t =
begin match hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (list_t t) self.hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hash_map_get_in_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x -> Return x
end
end
@@ -393,10 +393,10 @@ let rec hash_map_get_mut_in_list_fwd
then Return cvalue
else
begin match hash_map_get_mut_in_list_fwd t key ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x -> Return x
end
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
@@ -411,28 +411,28 @@ let rec hash_map_get_mut_in_list_back
then Return (ListCons ckey ret ls0)
else
begin match hash_map_get_mut_in_list_back t key ls0 ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ls1 -> Return (ListCons ckey cvalue ls1)
end
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
(** [hashmap::HashMap::{0}::get_mut] *)
let hash_map_get_mut_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result t =
begin match hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (list_t t) self.hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hash_map_get_mut_in_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x -> Return x
end
end
@@ -445,22 +445,22 @@ let hash_map_get_mut_back
result (hash_map_t t)
=
begin match hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (list_t t) self.hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hash_map_get_mut_in_list_back t key l ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhash_map_t self.hash_map_num_entries
self.hash_map_max_load_factor self.hash_map_max_load v)
@@ -483,11 +483,11 @@ let rec hash_map_remove_from_list_fwd
let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
begin match mv_ls with
| ListCons i cvalue tl0 -> Return (Some cvalue)
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
else
begin match hash_map_remove_from_list_fwd t key tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return opt -> Return opt
end
| ListNil -> Return None
@@ -506,11 +506,11 @@ let rec hash_map_remove_from_list_back
let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
begin match mv_ls with
| ListCons i cvalue tl0 -> Return tl0
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
else
begin match hash_map_remove_from_list_back t key tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return tl0 -> Return (ListCons ckey x tl0)
end
| ListNil -> Return ListNil
@@ -520,24 +520,24 @@ let rec hash_map_remove_from_list_back
let hash_map_remove_fwd
(t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
begin match hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (list_t t) self.hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hash_map_remove_from_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x ->
begin match x with
| None -> Return None
| Some x0 ->
begin match usize_sub self.hash_map_num_entries 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (Some x0)
end
end
@@ -550,28 +550,28 @@ let hash_map_remove_fwd
let hash_map_remove_back
(t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) =
begin match hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (list_t t) self.hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hash_map_remove_from_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x ->
begin match x with
| None ->
begin match hash_map_remove_from_list_back t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhash_map_t self.hash_map_num_entries
self.hash_map_max_load_factor self.hash_map_max_load v)
@@ -579,15 +579,15 @@ let hash_map_remove_back
end
| Some x0 ->
begin match usize_sub self.hash_map_num_entries 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match hash_map_remove_from_list_back t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhash_map_t i0 self.hash_map_max_load_factor
self.hash_map_max_load v)
@@ -603,65 +603,65 @@ let hash_map_remove_back
(** [hashmap::test1] *)
let test1_fwd : result unit =
begin match hash_map_new_fwd u64 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm ->
begin match hash_map_insert_fwd_back u64 hm 0 42 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm0 ->
begin match hash_map_insert_fwd_back u64 hm0 128 18 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm1 ->
begin match hash_map_insert_fwd_back u64 hm1 1024 138 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm2 ->
begin match hash_map_insert_fwd_back u64 hm2 1056 256 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm3 ->
begin match hash_map_get_fwd u64 hm3 128 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
if not (i = 18)
- then Fail
+ then Fail Failure
else
begin match hash_map_get_mut_back u64 hm3 1024 56 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm4 ->
begin match hash_map_get_fwd u64 hm4 1024 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
if not (i0 = 56)
- then Fail
+ then Fail Failure
else
begin match hash_map_remove_fwd u64 hm4 1024 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x ->
begin match x with
- | None -> Fail
+ | None -> Fail Failure
| Some x0 ->
if not (x0 = 56)
- then Fail
+ then Fail Failure
else
begin match hash_map_remove_back u64 hm4 1024 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm5 ->
begin match hash_map_get_fwd u64 hm5 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
if not (i1 = 42)
- then Fail
+ then Fail Failure
else
begin match hash_map_get_fwd u64 hm5 128 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i2 ->
if not (i2 = 18)
- then Fail
+ then Fail Failure
else
begin match hash_map_get_fwd u64 hm5 1056
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i3 ->
if not (i3 = 256)
- then Fail
+ then Fail Failure
else Return ()
end
end
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 21a46c73..0713dc7c 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -502,7 +502,7 @@ val hash_map_allocate_slots_fwd_lem
(requires (length slots + n <= usize_max))
(ensures (
match hash_map_allocate_slots_fwd t slots n with
- | Fail -> False
+ | Fail _ -> False
| Return slots' ->
length slots' = length slots + n /\
// We leave the already allocated slots unchanged
@@ -517,14 +517,14 @@ let rec hash_map_allocate_slots_fwd_lem t slots n =
| 0 -> ()
| _ ->
begin match vec_push_back (list_t t) slots ListNil with
- | Fail -> ()
+ | Fail _ -> ()
| Return slots1 ->
begin match usize_sub n 1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return i ->
hash_map_allocate_slots_fwd_lem t slots1 i;
begin match hash_map_allocate_slots_fwd t slots1 i with
- | Fail -> ()
+ | Fail _ -> ()
| Return slots2 ->
assert(length slots1 = length slots + 1);
assert(slots1 == slots @ [ListNil]); // Triggers patterns
@@ -550,7 +550,7 @@ val hash_map_new_with_capacity_fwd_lem
capacity * max_load_dividend <= usize_max))
(ensures (
match hash_map_new_with_capacity_fwd t capacity max_load_dividend max_load_divisor with
- | Fail -> False
+ | Fail _ -> False
| Return hm ->
// The hash map invariant is satisfied
hash_map_t_inv hm /\
@@ -574,13 +574,13 @@ let hash_map_new_with_capacity_fwd_lem (t : Type0) (capacity : usize)
assert(length v = 0);
hash_map_allocate_slots_fwd_lem t v capacity;
begin match hash_map_allocate_slots_fwd t v capacity with
- | Fail -> assert(False)
+ | Fail _ -> assert(False)
| Return v0 ->
begin match usize_mul capacity max_load_dividend with
- | Fail -> assert(False)
+ | Fail _ -> assert(False)
| Return i ->
begin match usize_div i max_load_divisor with
- | Fail -> assert(False)
+ | Fail _ -> assert(False)
| Return i0 ->
let hm = Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 v0 in
slots_t_all_nil_inv_lem v0;
@@ -597,7 +597,7 @@ val hash_map_new_fwd_lem_aux (t : Type0) :
Lemma
(ensures (
match hash_map_new_fwd t with
- | Fail -> False
+ | Fail _ -> False
| Return hm ->
// The hash map invariant is satisfied
hash_map_t_inv hm /\
@@ -610,7 +610,7 @@ val hash_map_new_fwd_lem_aux (t : Type0) :
let hash_map_new_fwd_lem_aux t =
hash_map_new_with_capacity_fwd_lem t 32 4 5;
match hash_map_new_with_capacity_fwd t 32 4 5 with
- | Fail -> ()
+ | Fail _ -> ()
| Return hm -> ()
#pop-options
@@ -625,7 +625,7 @@ let rec hash_map_clear_slots_fwd_back_lem
Lemma
(ensures (
match hash_map_clear_slots_fwd_back t slots i with
- | Fail -> False
+ | Fail _ -> False
| Return slots' ->
// The length is preserved
length slots' == length slots /\
@@ -640,14 +640,14 @@ let rec hash_map_clear_slots_fwd_back_lem
if b
then
begin match vec_index_mut_back (list_t t) slots i ListNil with
- | Fail -> ()
+ | Fail _ -> ()
| Return v ->
begin match usize_add i 1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return i1 ->
hash_map_clear_slots_fwd_back_lem t v i1;
begin match hash_map_clear_slots_fwd_back t v i1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return slots1 ->
assert(length slots1 == length slots);
assert(forall (j:nat{i+1 <= j /\ j < length slots}). index slots1 j == ListNil);
@@ -666,7 +666,7 @@ val hash_map_clear_fwd_back_lem_aux
(requires (hash_map_t_base_inv self))
(ensures (
match hash_map_clear_fwd_back t self with
- | Fail -> False
+ | Fail _ -> False
| Return hm ->
// The hash map invariant is satisfied
hash_map_t_base_inv hm /\
@@ -685,7 +685,7 @@ let hash_map_clear_fwd_back_lem_aux #t self =
let v = self.hash_map_slots in
hash_map_clear_slots_fwd_back_lem t v 0;
begin match hash_map_clear_slots_fwd_back t v 0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return slots1 ->
slots_t_al_v_all_nil_is_empty_lem slots1;
let hm1 = Mkhash_map_t 0 p i slots1 in
@@ -714,7 +714,7 @@ val hash_map_insert_in_list_fwd_lem
Lemma
(ensures (
match hash_map_insert_in_list_fwd t key value ls with
- | Fail -> False
+ | Fail _ -> False
| Return b ->
b <==> (slot_t_find_s key ls == None)))
(decreases (hash_map_insert_in_list_decreases t key value ls))
@@ -730,7 +730,7 @@ let rec hash_map_insert_in_list_fwd_lem t key value ls =
begin
hash_map_insert_in_list_fwd_lem t key value ls0;
match hash_map_insert_in_list_fwd t key value ls0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return b0 -> ()
end
| ListNil ->
@@ -769,7 +769,7 @@ val hash_map_insert_in_list_back_lem_append_s
slot_t_find_s key ls == None))
(ensures (
match hash_map_insert_in_list_back t key value ls with
- | Fail -> False
+ | Fail _ -> False
| Return ls' ->
list_t_v ls' == list_t_v ls @ [(key,value)]))
(decreases (hash_map_insert_in_list_decreases t key value ls))
@@ -785,7 +785,7 @@ let rec hash_map_insert_in_list_back_lem_append_s t key value ls =
begin
hash_map_insert_in_list_back_lem_append_s t key value ls0;
match hash_map_insert_in_list_back t key value ls0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return l -> ()
end
| ListNil -> ()
@@ -800,7 +800,7 @@ val hash_map_insert_in_list_back_lem_update_s
Some? (find (same_key key) (list_t_v ls))))
(ensures (
match hash_map_insert_in_list_back t key value ls with
- | Fail -> False
+ | Fail _ -> False
| Return ls' ->
list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,value)))
(decreases (hash_map_insert_in_list_decreases t key value ls))
@@ -816,7 +816,7 @@ let rec hash_map_insert_in_list_back_lem_update_s t key value ls =
begin
hash_map_insert_in_list_back_lem_update_s t key value ls0;
match hash_map_insert_in_list_back t key value ls0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return l -> ()
end
| ListNil -> ()
@@ -829,7 +829,7 @@ val hash_map_insert_in_list_back_lem_s
Lemma
(ensures (
match hash_map_insert_in_list_back t key value ls with
- | Fail -> False
+ | Fail _ -> False
| Return ls' ->
list_t_v ls' == hash_map_insert_in_list_s key value (list_t_v ls)))
@@ -924,7 +924,7 @@ val hash_map_insert_in_list_back_lem_append
slot_t_find_s key ls == None))
(ensures (
match hash_map_insert_in_list_back t key value ls with
- | Fail -> False
+ | Fail _ -> False
| Return ls' ->
list_t_v ls' == list_t_v ls @ [(key,value)] /\
// The invariant is preserved
@@ -1044,7 +1044,7 @@ val hash_map_insert_in_list_back_lem_update
Some? (slot_t_find_s key ls)))
(ensures (
match hash_map_insert_in_list_back t key value ls with
- | Fail -> False
+ | Fail _ -> False
| Return ls' ->
let als = list_t_v ls in
list_t_v ls' == find_update (same_key key) als (key,value) /\
@@ -1096,7 +1096,7 @@ val hash_map_insert_in_list_back_lem
(requires (slot_t_inv len (hash_mod_key key len) ls))
(ensures (
match hash_map_insert_in_list_back t key value ls with
- | Fail -> False
+ | Fail _ -> False
| Return ls' ->
// The invariant is preserved
slot_t_inv len (hash_mod_key key len) ls' /\
@@ -1145,7 +1145,7 @@ let hash_map_insert_no_resize_s
result (hash_map_s t) =
// Check if the table is saturated (too many entries, and we need to insert one)
let num_entries = length (flatten hm) in
- if None? (hash_map_s_find hm key) && num_entries = usize_max then Fail
+ if None? (hash_map_s_find hm key) && num_entries = usize_max then Fail Failure
else Return (hash_map_insert_no_fail_s hm key value)
/// Prove that [hash_map_insert_no_resize_s] is refined by
@@ -1161,7 +1161,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
match hash_map_insert_no_resize_fwd_back t self key value,
hash_map_insert_no_resize_s (hash_map_t_v self) key value
with
- | Fail, Fail -> True
+ | Fail _, Fail _ -> True
| Return hm, Return hm_v ->
hash_map_t_base_inv hm /\
hash_map_t_same_params hm self /\
@@ -1172,7 +1172,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
begin match hash_key_fwd key with
- | Fail -> ()
+ | Fail _ -> ()
| Return i ->
let i0 = self.hash_map_num_entries in
let p = self.hash_map_max_load_factor in
@@ -1181,31 +1181,31 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
let i2 = vec_len (list_t t) v in
let len = length v in
begin match usize_rem i i2 with
- | Fail -> ()
+ | Fail _ -> ()
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) v hash_mod with
- | Fail -> ()
+ | Fail _ -> ()
| Return l ->
begin
// Checking that: list_t_v (index ...) == index (hash_map_t_v ...) ...
assert(list_t_v l == index (hash_map_t_v self) hash_mod);
hash_map_insert_in_list_fwd_lem t key value l;
match hash_map_insert_in_list_fwd t key value l with
- | Fail -> ()
+ | Fail _ -> ()
| Return b ->
assert(b = None? (slot_s_find key (list_t_v l)));
hash_map_insert_in_list_back_lem t len key value l;
if b
then
begin match usize_add i0 1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return i3 ->
begin
match hash_map_insert_in_list_back t key value l with
- | Fail -> ()
+ | Fail _ -> ()
| Return l0 ->
begin match vec_index_mut_back (list_t t) v hash_mod l0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return v0 ->
let self_v = hash_map_t_v self in
let hm = Mkhash_map_t i3 p i1 v0 in
@@ -1221,10 +1221,10 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
else
begin
match hash_map_insert_in_list_back t key value l with
- | Fail -> ()
+ | Fail _ -> ()
| Return l0 ->
begin match vec_index_mut_back (list_t t) v hash_mod l0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return v0 ->
let self_v = hash_map_t_v self in
let hm = Mkhash_map_t i0 p i1 v0 in
@@ -1285,7 +1285,7 @@ val hash_map_insert_no_resize_s_lem
(requires (hash_map_s_inv hm))
(ensures (
match hash_map_insert_no_resize_s hm key value with
- | Fail ->
+ | Fail _ ->
// Can fail only if we need to create a new binding in
// an already saturated map
hash_map_s_len hm = usize_max /\
@@ -1308,7 +1308,7 @@ val hash_map_insert_no_resize_s_get_same_lem
Lemma (requires (hash_map_s_inv hm))
(ensures (
match hash_map_insert_no_resize_s hm key value with
- | Fail -> True
+ | Fail _ -> True
| Return hm' ->
hash_map_s_find hm' key == Some value))
@@ -1330,7 +1330,7 @@ val hash_map_insert_no_resize_s_get_diff_lem
Lemma (requires (hash_map_s_inv hm))
(ensures (
match hash_map_insert_no_resize_s hm key value with
- | Fail -> True
+ | Fail _ -> True
| Return hm' ->
hash_map_s_find hm' key' == hash_map_s_find hm key'))
@@ -1364,7 +1364,7 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
type result_hash_map_s_nes (t : Type0) : Type0 =
res:result (hash_map_s t) {
match res with
- | Fail -> True
+ | Fail _ -> True
| Return hm -> is_pos_usize (length hm)
}
@@ -1378,7 +1378,7 @@ let rec hash_map_move_elements_from_list_s
| [] -> Return hm
| (key, value) :: ls' ->
match hash_map_insert_no_resize_s hm key value with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm' ->
hash_map_move_elements_from_list_s hm' ls'
@@ -1390,7 +1390,7 @@ val hash_map_move_elements_from_list_fwd_back_lem
match hash_map_move_elements_from_list_fwd_back t ntable ls,
hash_map_move_elements_from_list_s (hash_map_t_v ntable) (slot_t_v ls)
with
- | Fail, Fail -> True
+ | Fail _, Fail _ -> True
| Return hm', Return hm_v ->
hash_map_t_base_inv hm' /\
hash_map_t_v hm' == hm_v /\
@@ -1407,13 +1407,13 @@ let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls =
let (_,_) :: tl_v = ls_v in
hash_map_insert_no_resize_fwd_back_lem_s t ntable k v;
begin match hash_map_insert_no_resize_fwd_back t ntable k v with
- | Fail -> ()
+ | Fail _ -> ()
| Return h ->
let h_v = Return?.v (hash_map_insert_no_resize_s (hash_map_t_v ntable) k v) in
assert(hash_map_t_v h == h_v);
hash_map_move_elements_from_list_fwd_back_lem t h tl;
begin match hash_map_move_elements_from_list_fwd_back t h tl with
- | Fail -> ()
+ | Fail _ -> ()
| Return h0 -> ()
end
end
@@ -1450,7 +1450,7 @@ let rec hash_map_move_elements_s_simpl
(requires (True))
(ensures (fun res ->
match res, hash_map_move_elements_fwd_back t ntable slots i with
- | Fail, Fail -> True
+ | Fail _, Fail _ -> True
| Return (ntable1, slots1), Return (ntable2, slots2) ->
ntable1 == ntable2 /\
slots1 == slots2
@@ -1461,7 +1461,7 @@ let rec hash_map_move_elements_s_simpl
then
let slot = index slots i in
begin match hash_map_move_elements_from_list_fwd_back t ntable slot with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm' ->
let slots' = list_update slots i ListNil in
hash_map_move_elements_s_simpl t hm' slots' (i+1)
@@ -1487,7 +1487,7 @@ let rec hash_map_move_elements_s
begin
let slot = index slots i in
match hash_map_move_elements_from_list_s hm slot with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm' ->
let slots' = list_update slots i [] in
hash_map_move_elements_s hm' slots' (i+1)
@@ -1504,7 +1504,7 @@ val hash_map_move_elements_fwd_back_lem_refin
match hash_map_move_elements_fwd_back t ntable slots i,
hash_map_move_elements_s (hash_map_t_v ntable) (slots_t_v slots) i
with
- | Fail, Fail -> True // We will prove later that this is not possible
+ | Fail _, Fail _ -> True // We will prove later that this is not possible
| Return (ntable', _), Return ntable'_v ->
hash_map_t_base_inv ntable' /\
hash_map_t_v ntable' == ntable'_v /\
@@ -1567,27 +1567,27 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
if b
then
begin match vec_index_mut_fwd (list_t t) slots i with
- | Fail -> ()
+ | Fail _ -> ()
| Return l ->
let l0 = mem_replace_fwd (list_t t) l ListNil in
assert(l0 == l);
hash_map_move_elements_from_list_fwd_back_lem t ntable l0;
begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return h ->
let l1 = mem_replace_back (list_t t) l ListNil in
assert(l1 == ListNil);
assert(slot_t_v #t ListNil == []); // THIS IS IMPORTANT
begin match vec_index_mut_back (list_t t) slots i l1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return v ->
begin match usize_add i 1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return i1 ->
hash_map_move_elements_fwd_back_lem_refin t h v i1;
begin match hash_map_move_elements_fwd_back t h v i1 with
- | Fail ->
- assert(hash_map_move_elements_fwd_back t ntable slots i == Fail);
+ | Fail _ ->
+ assert(Fail? (hash_map_move_elements_fwd_back t ntable slots i));
()
| Return (ntable', v0) -> ()
end
@@ -1617,7 +1617,7 @@ let rec hash_map_move_elements_s_flat
| [] -> Return ntable
| (k,v) :: slots' ->
match hash_map_insert_no_resize_s ntable k v with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable' ->
hash_map_move_elements_s_flat ntable' slots'
@@ -1718,7 +1718,7 @@ let rec hash_map_move_elements_from_list_s_as_flat_lem #t hm ls =
| [] -> ()
| (key, value) :: ls' ->
match hash_map_insert_no_resize_s hm key value with
- | Fail -> ()
+ | Fail _ -> ()
| Return hm' ->
hash_map_move_elements_from_list_s_as_flat_lem hm' ls'
#pop-options
@@ -1728,7 +1728,7 @@ let hash_map_move_elements_s_flat_comp
(#t : Type0) (hm : hash_map_s_nes t) (slot0 slot1 : slot_s t) :
Tot (result_hash_map_s_nes t) =
match hash_map_move_elements_s_flat hm slot0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm1 -> hash_map_move_elements_s_flat hm1 slot1
/// High-level desc:
@@ -1740,7 +1740,7 @@ val hash_map_move_elements_s_flat_append_lem
match hash_map_move_elements_s_flat_comp hm slot0 slot1,
hash_map_move_elements_s_flat hm (slot0 @ slot1)
with
- | Fail, Fail -> True
+ | Fail _, Fail _ -> True
| Return hm1, Return hm2 -> hm1 == hm2
| _ -> False))
(decreases (slot0))
@@ -1751,7 +1751,7 @@ let rec hash_map_move_elements_s_flat_append_lem #t hm slot0 slot1 =
| [] -> ()
| (k,v) :: slot0' ->
match hash_map_insert_no_resize_s hm k v with
- | Fail -> ()
+ | Fail _ -> ()
| Return hm' ->
hash_map_move_elements_s_flat_append_lem hm' slot0' slot1
#pop-options
@@ -1784,7 +1784,7 @@ val hash_map_move_elements_s_lem_refin_flat
match hash_map_move_elements_s hm slots i,
hash_map_move_elements_s_flat hm (flatten_i slots i)
with
- | Fail, Fail -> True
+ | Fail _, Fail _ -> True
| Return hm, Return hm' -> hm == hm'
| _ -> False))
(decreases (length slots - i))
@@ -1797,10 +1797,10 @@ let rec hash_map_move_elements_s_lem_refin_flat #t hm slots i =
let slot = index slots i in
hash_map_move_elements_from_list_s_as_flat_lem hm slot;
match hash_map_move_elements_from_list_s hm slot with
- | Fail ->
+ | Fail _ ->
assert(flatten_i slots i == slot @ flatten_i slots (i+1));
hash_map_move_elements_s_flat_append_lem hm slot (flatten_i slots (i+1));
- assert(hash_map_move_elements_s_flat hm (flatten_i slots i) == Fail)
+ assert(Fail? (hash_map_move_elements_s_flat hm (flatten_i slots i)))
| Return hm' ->
let slots' = list_update slots i [] in
flatten_i_same_suffix slots slots' (i+1);
@@ -1859,7 +1859,7 @@ val hash_map_move_elements_s_flat_lem
hash_map_s_len hm + length al <= usize_max))
(ensures (
match hash_map_move_elements_s_flat hm al with
- | Fail -> False // We can't fail
+ | Fail _ -> False // We can't fail
| Return hm' ->
// The invariant is preserved
hash_map_s_inv hm' /\
@@ -1876,7 +1876,7 @@ let rec hash_map_move_elements_s_flat_lem #t hm al =
| (k,v) :: al' ->
hash_map_insert_no_resize_s_lem hm k v;
match hash_map_insert_no_resize_s hm k v with
- | Fail -> ()
+ | Fail _ -> ()
| Return hm' ->
assert(hash_map_s_inv hm');
assert(assoc_list_inv al');
@@ -2211,7 +2211,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
match hash_map_move_elements_fwd_back t ntable slots 0,
hash_map_move_elements_s ntable_v slots_v 0
with
- | Fail, Fail -> ()
+ | Fail _, Fail _ -> ()
| Return (ntable', _), Return ntable'_v ->
assert(hash_map_t_base_inv ntable');
assert(hash_map_t_v ntable' == ntable'_v)
@@ -2222,7 +2222,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
match hash_map_move_elements_s ntable_v slots_v 0,
hash_map_move_elements_s_flat ntable_v (flatten_i slots_v 0)
with
- | Fail, Fail -> ()
+ | Fail _, Fail _ -> ()
| Return hm, Return hm' -> assert(hm == hm')
| _ -> assert(False)
end;
@@ -2258,10 +2258,10 @@ let hash_map_try_resize_s_simpl
if capacity <= (usize_max / 2) / divid then
let ncapacity : usize = capacity * 2 in
begin match hash_map_new_with_capacity_fwd t ncapacity divid divis with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable ->
match hash_map_move_elements_fwd_back t ntable hm.hash_map_slots 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (ntable', _) ->
let hm =
{ hm with hash_map_slots = ntable'.hash_map_slots;
@@ -2294,7 +2294,7 @@ val hash_map_try_resize_fwd_back_lem_refin
match hash_map_try_resize_fwd_back t self,
hash_map_try_resize_s_simpl self
with
- | Fail, Fail -> True
+ | Fail _, Fail _ -> True
| Return hm1, Return hm2 -> hm1 == hm2
| _ -> False))
@@ -2420,7 +2420,7 @@ val hash_map_try_resize_s_simpl_lem (#t : Type0) (hm : hash_map_t t) :
))
(ensures (
match hash_map_try_resize_s_simpl hm with
- | Fail -> False
+ | Fail _ -> False
| Return hm' ->
// The full invariant is now satisfied (the full invariant is "base
// invariant" + the map is not overloaded (or can't be resized because
@@ -2442,7 +2442,7 @@ let hash_map_try_resize_s_simpl_lem #t hm =
new_max_load_lem (hash_map_t_len_s hm) capacity divid divis;
hash_map_new_with_capacity_fwd_lem t ncapacity divid divis;
match hash_map_new_with_capacity_fwd t ncapacity divid divis with
- | Fail -> ()
+ | Fail _ -> ()
| Return ntable ->
let slots = hm.hash_map_slots in
let al = flatten (slots_t_v slots) in
@@ -2461,7 +2461,7 @@ let hash_map_try_resize_s_simpl_lem #t hm =
assert(forall (k:key). hash_map_t_find_s ntable k == None);
hash_map_move_elements_fwd_back_lem t ntable hm.hash_map_slots;
match hash_map_move_elements_fwd_back t ntable hm.hash_map_slots 0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return (ntable', _) ->
hash_map_is_assoc_list_lem hm;
assert(hash_map_is_assoc_list hm (hash_map_t_al_v hm));
@@ -2502,7 +2502,7 @@ val hash_map_try_resize_fwd_back_lem (#t : Type0) (hm : hash_map_t t) :
length hm.hash_map_slots * 2 * dividend > usize_max)))
(ensures (
match hash_map_try_resize_fwd_back t hm with
- | Fail -> False
+ | Fail _ -> False
| Return hm' ->
// The full invariant is now satisfied (the full invariant is "base
// invariant" + the map is not overloaded (or can't be resized because
@@ -2525,7 +2525,7 @@ let hash_map_insert_s
(#t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
result (hash_map_t t) =
match hash_map_insert_no_resize_fwd_back t self key value with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm' ->
if hash_map_t_len_s hm' > hm'.hash_map_max_load then
hash_map_try_resize_fwd_back t hm'
@@ -2538,7 +2538,7 @@ val hash_map_insert_fwd_back_lem_refin
match hash_map_insert_fwd_back t self key value,
hash_map_insert_s self key value
with
- | Fail, Fail -> True
+ | Fail _, Fail _ -> True
| Return hm1, Return hm2 -> hm1 == hm2
| _ -> False))
@@ -2563,7 +2563,7 @@ val hash_map_insert_fwd_back_lem_aux
Lemma (requires (hash_map_t_inv self))
(ensures (
match hash_map_insert_fwd_back t self key value with
- | Fail ->
+ | Fail _ ->
// We can fail only if:
// - the key is not in the map and we need to add it
// - we are already saturated
@@ -2585,7 +2585,7 @@ let hash_map_insert_fwd_back_lem_aux #t self key value =
hash_map_insert_no_resize_fwd_back_lem_s t self key value;
hash_map_insert_no_resize_s_lem (hash_map_t_v self) key value;
match hash_map_insert_no_resize_fwd_back t self key value with
- | Fail -> ()
+ | Fail _ -> ()
| Return hm' ->
// Expanding the post of [hash_map_insert_no_resize_fwd_back_lem_s]
let self_v = hash_map_t_v self in
@@ -2634,7 +2634,7 @@ val hash_map_contains_key_in_list_fwd_lem
Lemma
(ensures (
match hash_map_contains_key_in_list_fwd t key ls with
- | Fail -> False
+ | Fail _ -> False
| Return b ->
b = Some? (slot_t_find_s key ls)))
@@ -2650,7 +2650,7 @@ let rec hash_map_contains_key_in_list_fwd_lem #t key ls =
begin
hash_map_contains_key_in_list_fwd_lem key ls0;
match hash_map_contains_key_in_list_fwd t key ls0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return b0 -> ()
end
| ListNil -> ()
@@ -2663,24 +2663,24 @@ val hash_map_contains_key_fwd_lem_aux
Lemma
(ensures (
match hash_map_contains_key_fwd t self key with
- | Fail -> False
+ | Fail _ -> False
| Return b -> b = Some? (hash_map_t_find_s self key)))
let hash_map_contains_key_fwd_lem_aux #t self key =
begin match hash_key_fwd key with
- | Fail -> ()
+ | Fail _ -> ()
| Return i ->
let v = self.hash_map_slots in
let i0 = vec_len (list_t t) v in
begin match usize_rem i i0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return hash_mod ->
begin match vec_index_fwd (list_t t) v hash_mod with
- | Fail -> ()
+ | Fail _ -> ()
| Return l ->
hash_map_contains_key_in_list_fwd_lem key l;
begin match hash_map_contains_key_in_list_fwd t key l with
- | Fail -> ()
+ | Fail _ -> ()
| Return b -> ()
end
end
@@ -2700,7 +2700,7 @@ val hash_map_get_in_list_fwd_lem
Lemma
(ensures (
match hash_map_get_in_list_fwd t key ls, slot_t_find_s key ls with
- | Fail, None -> True
+ | Fail _, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
@@ -2715,7 +2715,7 @@ let rec hash_map_get_in_list_fwd_lem #t key ls =
begin
hash_map_get_in_list_fwd_lem key ls0;
match hash_map_get_in_list_fwd t key ls0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return x -> ()
end
| ListNil -> ()
@@ -2729,26 +2729,26 @@ val hash_map_get_fwd_lem_aux
Lemma
(ensures (
match hash_map_get_fwd t self key, hash_map_t_find_s self key with
- | Fail, None -> True
+ | Fail _, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
let hash_map_get_fwd_lem_aux #t self key =
begin match hash_key_fwd key with
- | Fail -> ()
+ | Fail _ -> ()
| Return i ->
let v = self.hash_map_slots in
let i0 = vec_len (list_t t) v in
begin match usize_rem i i0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return hash_mod ->
begin match vec_index_fwd (list_t t) v hash_mod with
- | Fail -> ()
+ | Fail _ -> ()
| Return l ->
begin
hash_map_get_in_list_fwd_lem key l;
match hash_map_get_in_list_fwd t key l with
- | Fail -> ()
+ | Fail _ -> ()
| Return x -> ()
end
end
@@ -2768,7 +2768,7 @@ val hash_map_get_mut_in_list_fwd_lem
Lemma
(ensures (
match hash_map_get_mut_in_list_fwd t key ls, slot_t_find_s key ls with
- | Fail, None -> True
+ | Fail _, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
@@ -2783,7 +2783,7 @@ let rec hash_map_get_mut_in_list_fwd_lem #t key ls =
begin
hash_map_get_mut_in_list_fwd_lem key ls0;
match hash_map_get_mut_in_list_fwd t key ls0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return x -> ()
end
| ListNil -> ()
@@ -2797,26 +2797,26 @@ val hash_map_get_mut_fwd_lem_aux
Lemma
(ensures (
match hash_map_get_mut_fwd t self key, hash_map_t_find_s self key with
- | Fail, None -> True
+ | Fail _, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
let hash_map_get_mut_fwd_lem_aux #t self key =
begin match hash_key_fwd key with
- | Fail -> ()
+ | Fail _ -> ()
| Return i ->
let v = self.hash_map_slots in
let i0 = vec_len (list_t t) v in
begin match usize_rem i i0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return hash_mod ->
begin match vec_index_fwd (list_t t) v hash_mod with
- | Fail -> ()
+ | Fail _ -> ()
| Return l ->
begin
hash_map_get_mut_in_list_fwd_lem key l;
match hash_map_get_mut_in_list_fwd t key l with
- | Fail -> ()
+ | Fail _ -> ()
| Return x -> ()
end
end
@@ -2836,7 +2836,7 @@ val hash_map_get_mut_in_list_back_lem
(requires (Some? (slot_t_find_s key ls)))
(ensures (
match hash_map_get_mut_in_list_back t key ls ret with
- | Fail -> False
+ | Fail _ -> False
| Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret)
| _ -> False))
@@ -2851,7 +2851,7 @@ let rec hash_map_get_mut_in_list_back_lem #t key ls ret =
begin
hash_map_get_mut_in_list_back_lem key ls0 ret;
match hash_map_get_mut_in_list_back t key ls0 ret with
- | Fail -> ()
+ | Fail _ -> ()
| Return l -> let ls1 = ListCons ckey cvalue l in ()
end
| ListNil -> ()
@@ -2868,13 +2868,13 @@ val hash_map_get_mut_back_lem_refin
(requires (Some? (hash_map_t_find_s self key)))
(ensures (
match hash_map_get_mut_back t self key ret with
- | Fail -> False
+ | Fail _ -> False
| Return hm' ->
hash_map_t_v hm' == hash_map_insert_no_fail_s (hash_map_t_v self) key ret))
let hash_map_get_mut_back_lem_refin #t self key ret =
begin match hash_key_fwd key with
- | Fail -> ()
+ | Fail _ -> ()
| Return i ->
let i0 = self.hash_map_num_entries in
let p = self.hash_map_max_load_factor in
@@ -2882,18 +2882,18 @@ let hash_map_get_mut_back_lem_refin #t self key ret =
let v = self.hash_map_slots in
let i2 = vec_len (list_t t) v in
begin match usize_rem i i2 with
- | Fail -> ()
+ | Fail _ -> ()
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) v hash_mod with
- | Fail -> ()
+ | Fail _ -> ()
| Return l ->
begin
hash_map_get_mut_in_list_back_lem key l ret;
match hash_map_get_mut_in_list_back t key l ret with
- | Fail -> ()
+ | Fail _ -> ()
| Return l0 ->
begin match vec_index_mut_back (list_t t) v hash_mod l0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in ()
end
end
@@ -2911,7 +2911,7 @@ val hash_map_get_mut_back_lem_aux
Some? (hash_map_t_find_s hm key)))
(ensures (
match hash_map_get_mut_back t hm key ret with
- | Fail -> False
+ | Fail _ -> False
| Return hm' ->
// Functional spec
hash_map_t_v hm' == hash_map_insert_no_fail_s (hash_map_t_v hm) key ret /\
@@ -2928,7 +2928,7 @@ let hash_map_get_mut_back_lem_aux #t hm key ret =
let hm_v = hash_map_t_v hm in
hash_map_get_mut_back_lem_refin hm key ret;
match hash_map_get_mut_back t hm key ret with
- | Fail -> assert(False)
+ | Fail _ -> assert(False)
| Return hm' ->
hash_map_insert_no_fail_s_lem hm_v key ret
@@ -2942,7 +2942,7 @@ val hash_map_remove_from_list_fwd_lem
Lemma
(ensures (
match hash_map_remove_from_list_fwd t key ls with
- | Fail -> False
+ | Fail _ -> False
| Return opt_x ->
opt_x == slot_t_find_s key ls /\
(Some? opt_x ==> length (slot_t_v ls) > 0)))
@@ -2963,7 +2963,7 @@ let rec hash_map_remove_from_list_fwd_lem #t key ls =
begin
hash_map_remove_from_list_fwd_lem key tl;
match hash_map_remove_from_list_fwd t key tl with
- | Fail -> ()
+ | Fail _ -> ()
| Return opt -> ()
end
| ListNil -> ()
@@ -2979,26 +2979,26 @@ val hash_map_remove_fwd_lem_aux
hash_map_t_inv self))
(ensures (
match hash_map_remove_fwd t self key with
- | Fail -> False
+ | Fail _ -> False
| Return opt_x -> opt_x == hash_map_t_find_s self key))
let hash_map_remove_fwd_lem_aux #t self key =
begin match hash_key_fwd key with
- | Fail -> ()
+ | Fail _ -> ()
| Return i ->
let i0 = self.hash_map_num_entries in
let v = self.hash_map_slots in
let i1 = vec_len (list_t t) v in
begin match usize_rem i i1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) v hash_mod with
- | Fail -> ()
+ | Fail _ -> ()
| Return l ->
begin
hash_map_remove_from_list_fwd_lem key l;
match hash_map_remove_from_list_fwd t key l with
- | Fail -> ()
+ | Fail _ -> ()
| Return x ->
begin match x with
| None -> ()
@@ -3008,7 +3008,7 @@ let hash_map_remove_fwd_lem_aux #t self key =
assert(length (list_t_v #t l) > 0);
length_flatten_index (hash_map_t_v self) hash_mod;
match usize_sub i0 1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return _ -> ()
end
end
@@ -3036,7 +3036,7 @@ val hash_map_remove_from_list_back_lem_refin
Lemma
(ensures (
match hash_map_remove_from_list_back t key ls with
- | Fail -> False
+ | Fail _ -> False
| Return ls' ->
list_t_v ls' == hash_map_remove_from_list_s key (list_t_v ls) /\
// The length is decremented, iff the key was in the slot
@@ -3062,7 +3062,7 @@ let rec hash_map_remove_from_list_back_lem_refin #t key ls =
begin
hash_map_remove_from_list_back_lem_refin key tl;
match hash_map_remove_from_list_back t key tl with
- | Fail -> ()
+ | Fail _ -> ()
| Return l -> let ls0 = ListCons ckey x l in ()
end
| ListNil -> ()
@@ -3089,7 +3089,7 @@ val hash_map_remove_back_lem_refin
hash_map_t_inv self))
(ensures (
match hash_map_remove_back t self key with
- | Fail -> False
+ | Fail _ -> False
| Return hm' ->
hash_map_t_same_params hm' self /\
hash_map_t_v hm' == hash_map_remove_s (hash_map_t_v self) key /\
@@ -3102,7 +3102,7 @@ val hash_map_remove_back_lem_refin
let hash_map_remove_back_lem_refin #t self key =
begin match hash_key_fwd key with
- | Fail -> ()
+ | Fail _ -> ()
| Return i ->
let i0 = self.hash_map_num_entries in
let p = self.hash_map_max_load_factor in
@@ -3110,27 +3110,27 @@ let hash_map_remove_back_lem_refin #t self key =
let v = self.hash_map_slots in
let i2 = vec_len (list_t t) v in
begin match usize_rem i i2 with
- | Fail -> ()
+ | Fail _ -> ()
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) v hash_mod with
- | Fail -> ()
+ | Fail _ -> ()
| Return l ->
begin
hash_map_remove_from_list_fwd_lem key l;
match hash_map_remove_from_list_fwd t key l with
- | Fail -> ()
+ | Fail _ -> ()
| Return x ->
begin match x with
| None ->
begin
hash_map_remove_from_list_back_lem_refin key l;
match hash_map_remove_from_list_back t key l with
- | Fail -> ()
+ | Fail _ -> ()
| Return l0 ->
begin
length_flatten_update (slots_t_v v) hash_mod (list_t_v l0);
match vec_index_mut_back (list_t t) v hash_mod l0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return v0 -> ()
end
end
@@ -3140,17 +3140,17 @@ let hash_map_remove_back_lem_refin #t self key =
assert(length (list_t_v #t l) > 0);
length_flatten_index (hash_map_t_v self) hash_mod;
match usize_sub i0 1 with
- | Fail -> ()
+ | Fail _ -> ()
| Return i3 ->
begin
hash_map_remove_from_list_back_lem_refin key l;
match hash_map_remove_from_list_back t key l with
- | Fail -> ()
+ | Fail _ -> ()
| Return l0 ->
begin
length_flatten_update (slots_t_v v) hash_mod (list_t_v l0);
match vec_index_mut_back (list_t t) v hash_mod l0 with
- | Fail -> ()
+ | Fail _ -> ()
| Return v0 -> ()
end
end
@@ -3224,7 +3224,7 @@ val hash_map_remove_back_lem_aux
(requires (hash_map_t_inv self))
(ensures (
match hash_map_remove_back t self key with
- | Fail -> False
+ | Fail _ -> False
| Return hm' ->
hash_map_t_inv self /\
hash_map_t_same_params hm' self /\
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fsti b/tests/fstar/hashmap/Hashmap.Properties.fsti
index 756ae687..0a4f0134 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fsti
+++ b/tests/fstar/hashmap/Hashmap.Properties.fsti
@@ -67,7 +67,7 @@ val hash_map_new_fwd_lem (t : Type0) :
Lemma
(ensures (
match hash_map_new_fwd t with
- | Fail -> False
+ | Fail _ -> False
| Return hm ->
// The hash map invariant is satisfied
hash_map_t_inv hm /\
@@ -85,7 +85,7 @@ val hash_map_clear_fwd_back_lem
(requires (hash_map_t_inv self))
(ensures (
match hash_map_clear_fwd_back t self with
- | Fail -> False
+ | Fail _ -> False
| Return hm ->
// The hash map invariant is satisfied
hash_map_t_inv hm /\
@@ -102,7 +102,7 @@ val hash_map_len_fwd_lem (#t : Type0) (self : hash_map_t t) :
(requires (hash_map_t_inv self))
(ensures (
match hash_map_len_fwd t self with
- | Fail -> False
+ | Fail _ -> False
| Return l -> l = len_s self))
@@ -120,7 +120,7 @@ val hash_map_insert_fwd_back_lem
(requires (hash_map_t_inv self))
(ensures (
match hash_map_insert_fwd_back t self key value with
- | Fail ->
+ | Fail _ ->
// We can fail only if:
// - the key is not in the map and we thus need to add it
None? (find_s self key) /\
@@ -151,7 +151,7 @@ val hash_map_contains_key_fwd_lem
(requires (hash_map_t_inv self))
(ensures (
match hash_map_contains_key_fwd t self key with
- | Fail -> False
+ | Fail _ -> False
| Return b -> b = Some? (find_s self key)))
(**** [get'fwd] *)
@@ -163,7 +163,7 @@ val hash_map_get_fwd_lem
(requires (hash_map_t_inv self))
(ensures (
match hash_map_get_fwd t self key, find_s self key with
- | Fail, None -> True
+ | Fail _, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
@@ -181,7 +181,7 @@ val hash_map_get_mut_fwd_lem
(requires (hash_map_t_inv self))
(ensures (
match hash_map_get_mut_fwd t self key, find_s self key with
- | Fail, None -> True
+ | Fail _, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
@@ -211,7 +211,7 @@ val hash_map_get_mut_back_lem
Some? (find_s hm key)))
(ensures (
match hash_map_get_mut_back t hm key ret with
- | Fail -> False // Can't fail
+ | Fail _ -> False // Can't fail
| Return hm' ->
// The invariant is preserved
hash_map_t_inv hm' /\
@@ -234,7 +234,7 @@ val hash_map_remove_fwd_lem
(requires (hash_map_t_inv self))
(ensures (
match hash_map_remove_fwd t self key with
- | Fail -> False
+ | Fail _ -> False
| Return opt_x -> opt_x == find_s self key))
@@ -249,7 +249,7 @@ val hash_map_remove_back_lem
(requires (hash_map_t_inv self))
(ensures (
match hash_map_remove_back t self key with
- | Fail -> False
+ | Fail _ -> False
| Return hm' ->
// The invariant is preserved
hash_map_t_inv self /\
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
#pop-options
(*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
type result (a : Type0) : Type0 =
| Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
// Monadic bind and return.
// Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
match m with
| Return x -> f x
- | Fail -> Fail
+ | Fail e -> Fail e
// Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
// Normalize and unwrap a successful result (used for globals).
let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
- if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+ if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (x / y) else Fail
+ if y <> 0 then mk_scalar ty (x / y) else Fail Failure
/// The remainder operation
let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
let _ = assert_norm(int_rem (-1) (-2) = -1)
let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+ if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) :
(requires True)
(ensures (fun res ->
match res with
- | Fail -> True
+ | Fail e -> e == Failure
| Return v' -> length v' = length v + 1)) =
if length v < usize_max then begin
(**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) :
(**) assert(length (append v [x]) = length v + 1);
Return (append v [x])
end
- else Fail
+ else Fail Failure
// The **forward** function shouldn't be used
let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail
+ if i < length v then Return () else Fail Failure
let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
- if i < length v then Return (list_update v i x) else Fail
+ if i < length v then Return (list_update v i x) else Fail Failure
// The **backward** function shouldn't be used
let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail
+ if i < length v then Return (index v i) else Fail Failure
let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail
+ if i < length v then Return () else Fail Failure
let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail
+ if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
- if i < length v then Return (list_update v i nx) else Fail
+ if i < length v then Return (list_update v i nx) else Fail Failure
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 82b44dbd..d6da4562 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -21,13 +21,13 @@ let rec hashmap_hash_map_allocate_slots_fwd
then Return slots
else
begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots0 ->
begin match usize_sub n 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v -> Return v
end
end
@@ -41,13 +41,13 @@ let hashmap_hash_map_new_with_capacity_fwd
=
let v = vec_new (hashmap_list_t t) in
begin match hashmap_hash_map_allocate_slots_fwd t v capacity with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots ->
begin match usize_mul capacity max_load_dividend with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
begin match usize_div i max_load_divisor with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0
slots)
@@ -58,7 +58,7 @@ let hashmap_hash_map_new_with_capacity_fwd
(** [hashmap_main::hashmap::HashMap::{0}::new] *)
let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm -> Return hm
end
@@ -73,13 +73,13 @@ let rec hashmap_hash_map_clear_slots_fwd_back
then
begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots0 ->
begin match usize_add i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots1 -> Return slots1
end
end
@@ -91,7 +91,7 @@ let hashmap_hash_map_clear_fwd_back
(t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
begin match
hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
self.hashmap_hash_map_max_load v)
@@ -114,7 +114,7 @@ let rec hashmap_hash_map_insert_in_list_fwd
then Return false
else
begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b -> Return b
end
| HashmapListNil -> Return true
@@ -132,7 +132,7 @@ let rec hashmap_hash_map_insert_in_list_back
then Return (HashmapListCons ckey value ls0)
else
begin match hashmap_hash_map_insert_in_list_back t key value ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
end
| HashmapListNil ->
@@ -145,33 +145,33 @@ let hashmap_hash_map_insert_no_resize_fwd_back
result (hashmap_hash_map_t t)
=
begin match hashmap_hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match
vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
hash_mod with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hashmap_hash_map_insert_in_list_fwd t key value l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return inserted ->
if inserted
then
begin match usize_add self.hashmap_hash_map_num_entries 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match hashmap_hash_map_insert_in_list_back t key value l
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (hashmap_list_t t)
self.hashmap_hash_map_slots hash_mod l0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhashmap_hash_map_t i0
self.hashmap_hash_map_max_load_factor
@@ -181,12 +181,12 @@ let hashmap_hash_map_insert_no_resize_fwd_back
end
else
begin match hashmap_hash_map_insert_in_list_back t key value l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (hashmap_list_t t)
self.hashmap_hash_map_slots hash_mod l0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
self.hashmap_hash_map_max_load_factor
@@ -211,11 +211,11 @@ let rec hashmap_hash_map_move_elements_from_list_fwd_back
begin match ls with
| HashmapListCons k v tl ->
begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable0 ->
begin match
hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable1 -> Return ntable1
end
end
@@ -233,23 +233,23 @@ let rec hashmap_hash_map_move_elements_fwd_back
if i < i0
then
begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable0 ->
let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return slots0 ->
begin match usize_add i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
begin match
hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (ntable1, slots1) -> Return (ntable1, slots1)
end
end
@@ -262,28 +262,28 @@ let rec hashmap_hash_map_move_elements_fwd_back
let hashmap_hash_map_try_resize_fwd_back
(t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
begin match scalar_cast U32 Usize core_num_u32_max_c with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return max_usize ->
let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_div max_usize 2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return n1 ->
let (i, i0) = self.hashmap_hash_map_max_load_factor in
begin match usize_div n1 i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
if capacity <= i1
then
begin match usize_mul capacity 2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i2 ->
begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ntable ->
begin match
hashmap_hash_map_move_elements_fwd_back t ntable
self.hashmap_hash_map_slots 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (ntable0, _) ->
Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
(i, i0) ntable0.hashmap_hash_map_max_load
@@ -304,15 +304,15 @@ let hashmap_hash_map_insert_fwd_back
result (hashmap_hash_map_t t)
=
begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return self0 ->
begin match hashmap_hash_map_len_fwd t self0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
if i > self0.hashmap_hash_map_max_load
then
begin match hashmap_hash_map_try_resize_fwd_back t self0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return self1 -> Return self1
end
else Return self0
@@ -331,7 +331,7 @@ let rec hashmap_hash_map_contains_key_in_list_fwd
then Return true
else
begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b -> Return b
end
| HashmapListNil -> Return false
@@ -341,19 +341,19 @@ let rec hashmap_hash_map_contains_key_in_list_fwd
let hashmap_hash_map_contains_key_fwd
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool =
begin match hashmap_hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match
vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hashmap_hash_map_contains_key_in_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return b -> Return b
end
end
@@ -371,29 +371,29 @@ let rec hashmap_hash_map_get_in_list_fwd
then Return cvalue
else
begin match hashmap_hash_map_get_in_list_fwd t key ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x -> Return x
end
- | HashmapListNil -> Fail
+ | HashmapListNil -> Fail Failure
end
(** [hashmap_main::hashmap::HashMap::{0}::get] *)
let hashmap_hash_map_get_fwd
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
begin match hashmap_hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match
vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hashmap_hash_map_get_in_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x -> Return x
end
end
@@ -412,10 +412,10 @@ let rec hashmap_hash_map_get_mut_in_list_fwd
then Return cvalue
else
begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x -> Return x
end
- | HashmapListNil -> Fail
+ | HashmapListNil -> Fail Failure
end
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
@@ -430,29 +430,29 @@ let rec hashmap_hash_map_get_mut_in_list_back
then Return (HashmapListCons ckey ret ls0)
else
begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
end
- | HashmapListNil -> Fail
+ | HashmapListNil -> Fail Failure
end
(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
let hashmap_hash_map_get_mut_fwd
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
begin match hashmap_hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match
vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
hash_mod with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hashmap_hash_map_get_mut_in_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x -> Return x
end
end
@@ -465,24 +465,24 @@ let hashmap_hash_map_get_mut_back
result (hashmap_hash_map_t t)
=
begin match hashmap_hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match
vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
hash_mod with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hashmap_hash_map_get_mut_in_list_back t key l ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
hash_mod l0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
self.hashmap_hash_map_max_load_factor
@@ -508,11 +508,11 @@ let rec hashmap_hash_map_remove_from_list_fwd
HashmapListNil in
begin match mv_ls with
| HashmapListCons i cvalue tl0 -> Return (Some cvalue)
- | HashmapListNil -> Fail
+ | HashmapListNil -> Fail Failure
end
else
begin match hashmap_hash_map_remove_from_list_fwd t key tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return opt -> Return opt
end
| HashmapListNil -> Return None
@@ -533,11 +533,11 @@ let rec hashmap_hash_map_remove_from_list_back
HashmapListNil in
begin match mv_ls with
| HashmapListCons i cvalue tl0 -> Return tl0
- | HashmapListNil -> Fail
+ | HashmapListNil -> Fail Failure
end
else
begin match hashmap_hash_map_remove_from_list_back t key tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return tl0 -> Return (HashmapListCons ckey x tl0)
end
| HashmapListNil -> Return HashmapListNil
@@ -547,25 +547,25 @@ let rec hashmap_hash_map_remove_from_list_back
let hashmap_hash_map_remove_fwd
(t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) =
begin match hashmap_hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match
vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
hash_mod with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hashmap_hash_map_remove_from_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x ->
begin match x with
| None -> Return None
| Some x0 ->
begin match usize_sub self.hashmap_hash_map_num_entries 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return (Some x0)
end
end
@@ -580,29 +580,29 @@ let hashmap_hash_map_remove_back
result (hashmap_hash_map_t t)
=
begin match hashmap_hash_key_fwd key with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash ->
let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_rem hash i with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hash_mod ->
begin match
vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
hash_mod with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l ->
begin match hashmap_hash_map_remove_from_list_fwd t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x ->
begin match x with
| None ->
begin match hashmap_hash_map_remove_from_list_back t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (hashmap_list_t t)
self.hashmap_hash_map_slots hash_mod l0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
self.hashmap_hash_map_max_load_factor
@@ -611,15 +611,15 @@ let hashmap_hash_map_remove_back
end
| Some x0 ->
begin match usize_sub self.hashmap_hash_map_num_entries 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match hashmap_hash_map_remove_from_list_back t key l with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l0 ->
begin match
vec_index_mut_back (hashmap_list_t t)
self.hashmap_hash_map_slots hash_mod l0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return v ->
Return (Mkhashmap_hash_map_t i0
self.hashmap_hash_map_max_load_factor
@@ -636,69 +636,69 @@ let hashmap_hash_map_remove_back
(** [hashmap_main::hashmap::test1] *)
let hashmap_test1_fwd : result unit =
begin match hashmap_hash_map_new_fwd u64 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm ->
begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm0 ->
begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm1 ->
begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm2 ->
begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm3 ->
begin match hashmap_hash_map_get_fwd u64 hm3 128 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
if not (i = 18)
- then Fail
+ then Fail Failure
else
begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm4 ->
begin match hashmap_hash_map_get_fwd u64 hm4 1024 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
if not (i0 = 56)
- then Fail
+ then Fail Failure
else
begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x ->
begin match x with
- | None -> Fail
+ | None -> Fail Failure
| Some x0 ->
if not (x0 = 56)
- then Fail
+ then Fail Failure
else
begin match
hashmap_hash_map_remove_back u64 hm4 1024 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm5 ->
begin match hashmap_hash_map_get_fwd u64 hm5 0
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
if not (i1 = 42)
- then Fail
+ then Fail Failure
else
begin match
hashmap_hash_map_get_fwd u64 hm5 128 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i2 ->
if not (i2 = 18)
- then Fail
+ then Fail Failure
else
begin match
hashmap_hash_map_get_fwd u64 hm5 1056
with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i3 ->
if not (i3 = 256)
- then Fail
+ then Fail Failure
else Return ()
end
end
@@ -722,13 +722,13 @@ let _ = assert_norm (hashmap_test1_fwd = Return ())
let insert_on_disk_fwd
(key : usize) (value : u64) (st : state) : result (state & unit) =
begin match hashmap_utils_deserialize_fwd st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, hm) ->
begin match hashmap_hash_map_insert_fwd_back u64 hm key value with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return hm0 ->
begin match hashmap_utils_serialize_fwd hm0 st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) -> Return (st1, ())
end
end
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
index 4df039a8..106fe05a 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
@@ -19,7 +19,7 @@ val state_v : state -> hashmap_hash_map_t u64
assume
val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma (
match hashmap_utils_serialize_fwd hm st with
- | Fail -> True
+ | Fail _ -> True
| Return (st', ()) -> state_v st' == hm)
[SMTPat (hashmap_utils_serialize_fwd hm st)]
@@ -27,7 +27,7 @@ val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma (
assume
val deserialize_lem (st : state) : Lemma (
match hashmap_utils_deserialize_fwd st with
- | Fail -> True
+ | Fail _ -> True
| Return (st', hm) -> hm == state_v st /\ st' == st)
[SMTPat (hashmap_utils_deserialize_fwd st)]
@@ -38,11 +38,11 @@ val deserialize_lem (st : state) : Lemma (
/// in the hash map previously stored on disk.
val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma (
match insert_on_disk_fwd key value st with
- | Fail -> True
+ | Fail _ -> True
| Return (st', ()) ->
let hm = state_v st in
match hashmap_hash_map_insert_fwd_back u64 hm key value with
- | Fail -> False
+ | Fail _ -> False
| Return hm' -> hm' == state_v st')
let insert_on_disk_fwd_lem key value st = ()
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
#pop-options
(*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
type result (a : Type0) : Type0 =
| Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
// Monadic bind and return.
// Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
match m with
| Return x -> f x
- | Fail -> Fail
+ | Fail e -> Fail e
// Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
// Normalize and unwrap a successful result (used for globals).
let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
- if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+ if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (x / y) else Fail
+ if y <> 0 then mk_scalar ty (x / y) else Fail Failure
/// The remainder operation
let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
let _ = assert_norm(int_rem (-1) (-2) = -1)
let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+ if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) :
(requires True)
(ensures (fun res ->
match res with
- | Fail -> True
+ | Fail e -> e == Failure
| Return v' -> length v' = length v + 1)) =
if length v < usize_max then begin
(**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) :
(**) assert(length (append v [x]) = length v + 1);
Return (append v [x])
end
- else Fail
+ else Fail Failure
// The **forward** function shouldn't be used
let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail
+ if i < length v then Return () else Fail Failure
let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
- if i < length v then Return (list_update v i x) else Fail
+ if i < length v then Return (list_update v i x) else Fail Failure
// The **backward** function shouldn't be used
let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail
+ if i < length v then Return (index v i) else Fail Failure
let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail
+ if i < length v then Return () else Fail Failure
let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail
+ if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
- if i < length v then Return (list_update v i nx) else Fail
+ if i < length v then Return (list_update v i nx) else Fail Failure
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 05:50:48 +0000