diff options
author | Son Ho | 2022-02-13 02:07:40 +0100 |
---|---|---|
committer | Son Ho | 2022-02-13 02:07:40 +0100 |
commit | 2a3117216e1a0aef9df1238e59be8b98c7f2076d (patch) | |
tree | 05efceeb8608c727bfc06f750f1ea849520c23a6 | |
parent | d8aa233bba7bd79c14bf36338dbeb527ffdf5c2b (diff) |
Prove the lemmas for [insert]
-rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 1178ecc1..7425b038 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -2593,3 +2593,65 @@ val hash_map_try_resize_fwd_back_lem (#t : Type0) (hm : hash_map_t t) : let hash_map_try_resize_fwd_back_lem #t hm = hash_map_try_resize_fwd_back_lem_refin t hm; hash_map_try_resize_s_lem hm + +(*** insert *) + +/// The refinement (very close to the original function: we don't need something +/// very high level, just to clean it a bit) +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 + | Return hm' -> + if hash_map_t_len_s hm' > hm'.hash_map_max_load then + hash_map_try_resize_fwd_back t hm' + else Return hm' + +val hash_map_insert_fwd_back_lem_refin + (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : + Lemma (requires True) + (ensures ( + match hash_map_insert_fwd_back t self key value, + hash_map_insert_s self key value + with + | Fail, Fail -> True + | Return hm1, Return hm2 -> hm1 == hm2 + | _ -> False)) + +let hash_map_insert_fwd_back_lem_refin t self key value = () + +val hash_map_insert_fwd_back_lem + (t : Type0) (self : hash_map_t t) (key : usize) (value : t) : + Lemma (requires (hash_map_t_inv self)) + (ensures ( + match hash_map_insert_fwd_back t self key value with + | Fail -> + // We can fail only if: + // - the key is not in the map and we need to add it + // - we are already saturated + hash_map_t_len_s self = usize_max /\ + None? (hash_map_t_find_s self key) + | Return hm' -> + // The invariant is preserved + hash_map_t_inv hm' /\ + // [key] maps to [value] + hash_map_t_find_s hm' key == Some value /\ + // The other bindings are preserved + (forall k'. k' <> key ==> hash_map_t_find_s hm' k' == hash_map_t_find_s hm' k') /\ + // The length is incremented, iff we inserted a new key + (match hash_map_t_find_s self key with + | None -> hash_map_t_len_s hm' = hash_map_t_len_s self + 1 + | Some _ -> hash_map_t_len_s hm' = hash_map_t_len_s self))) + +let hash_map_insert_fwd_back_lem 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_slots_v self) key value; + match hash_map_insert_no_resize_fwd_back t self key value with + | Fail -> () + | Return hm' -> + if hash_map_t_len_s hm' > hm'.hash_map_max_load then + begin + hash_map_try_resize_fwd_back_lem hm' + end + else () |