From 5a96e28b8706ed945ccbb569881ca1888cd73ace Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 14 Nov 2022 11:58:31 +0100 Subject: Regenerate the files and fix the proofs --- tests/fstar/hashmap/Hashmap.Properties.fst | 260 ++++++++++++++--------------- 1 file changed, 130 insertions(+), 130 deletions(-) (limited to 'tests/fstar/hashmap/Hashmap.Properties.fst') 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 /\ -- cgit v1.2.3