diff options
author | Son Ho | 2022-02-13 13:17:19 +0100 |
---|---|---|
committer | Son Ho | 2022-02-13 13:17:19 +0100 |
commit | a8ba4fb04e5e729fabbcf3c33b5affdb3207c8e2 (patch) | |
tree | 4aea489c0ee0336eb655dcb5a8df05a6cca5e86c | |
parent | aee48d6414a92d672fc6294122d6320781ca9f9b (diff) |
Prove the lemma for remove'fwd
-rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 103 |
1 files changed, 90 insertions, 13 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 532dae69..1cf5fc88 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -288,8 +288,11 @@ val length_flatten_update : -> i:nat{i < length ls} -> x:list a -> Lemma ( + // We want this property: + // ``` // length (flatten (list_update ls i x)) = // length (flatten ls) - length (index ls i) + length x + // ``` length (flatten (list_update ls i x)) + length (index ls i) = length (flatten ls) + length x) @@ -315,6 +318,24 @@ let rec length_flatten_update #a ls i x = end #pop-options + +val length_flatten_index : + #a:Type + -> ls:list (list a) + -> i:nat{i < length ls} -> + Lemma ( + length (flatten ls) >= length (index ls i)) + +#push-options "--fuel 1" +let rec length_flatten_index #a ls i = + match ls with + | x' :: ls' -> + assert(flatten ls == x' @ flatten ls'); // Triggers patterns + assert(length (flatten ls) == length x' + length (flatten ls')); + if i = 0 then () + else length_flatten_index ls' (i-1) +#pop-options + val forall_index_equiv_list_for_all (#a : Type) (pred : a -> Tot bool) (ls : list a) : Lemma ((forall (i:nat{i < length ls}). pred (index ls i)) <==> for_all pred ls) @@ -3070,14 +3091,18 @@ let hash_map_get_mut_back_lem #t hm key ret = (*** remove'fwd *) +val hash_map_remove_from_list_fwd_lem + (#t : Type0) (key : usize) (ls : list_t t) : + Lemma + (ensures ( + match hash_map_remove_from_list_fwd t key ls with + | Fail -> False + | Return opt_x -> + opt_x == slot_t_find_s key ls /\ + (Some? opt_x ==> length (slot_t_v ls) > 0))) -(* -(** [hashmap::HashMap::remove_from_list] *) -let rec hash_map_remove_from_list_fwd - (t : Type0) (key : usize) (ls : list_t t) : - Tot (result (option t)) - (decreases (hash_map_remove_from_list_decreases t key ls)) - = +#push-options "--fuel 1" +let rec hash_map_remove_from_list_fwd_lem #t key ls = begin match ls with | ListCons ckey x tl -> let b = ckey = key in @@ -3085,13 +3110,65 @@ let rec hash_map_remove_from_list_fwd then 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 + | ListCons i cvalue tl0 -> () + | ListNil -> () end else - begin match hash_map_remove_from_list_fwd t key tl with - | Fail -> Fail - | Return opt -> Return opt + begin + hash_map_remove_from_list_fwd_lem key tl; + match hash_map_remove_from_list_fwd t key tl with + | Fail -> () + | Return opt -> () + end + | ListNil -> () + end +#pop-options + +val hash_map_remove_fwd_lem + (t : Type0) (self : hash_map_t t) (key : usize) : + Lemma + (requires ( + // We need the invariant to prove that upon decrementing the entries counter, + // the counter doesn't become negative + hash_map_t_inv self)) + (ensures ( + match hash_map_remove_fwd t self key with + | Fail -> False + | Return opt_x -> opt_x == hash_map_t_find_s self key)) + +let hash_map_remove_fwd_lem t self key = + begin match hash_key_fwd key with + | 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 -> () + | Return hash_mod -> + begin match vec_index_mut_fwd (list_t t) v hash_mod with + | 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 -> () + | Return x -> + begin match x with + | None -> () + | Some x0 -> + begin + assert(l == index v hash_mod); + assert(length (list_t_v #t l) > 0); + length_flatten_index (hash_map_t_slots_v self) hash_mod; + match usize_sub i0 1 with + | Fail -> () + | Return _ -> () + end + end + end end - | ListNil -> Return None + end end + +(*** remove'back *) |