diff options
author | Son Ho | 2022-02-13 21:13:22 +0100 |
---|---|---|
committer | Son Ho | 2022-02-13 21:13:22 +0100 |
commit | 1b95a1c00ab5f3d628275687cbf5f08517bce401 (patch) | |
tree | ecd50252a1b24f8829d318e62e6c63b73fc6c8fc /tests/hashmap | |
parent | 6ef6acf16f9d55acc562c8dfe1a302d02557880c (diff) |
Start working on the specs we will reveal in the .fsti
Diffstat (limited to '')
-rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 96 |
1 files changed, 78 insertions, 18 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 962af8bf..b8788c8c 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -415,7 +415,12 @@ let rec map_list_update_lem #a #b f ls i x = (*** Invariants, models *) +(**** Internals *) +/// The following invariants, models, representation functions... are mostly +/// for the purpose of the proofs. + let is_pos_usize (n : nat) : Type0 = 0 < n /\ n <= usize_max +type pos_usize = x:usize{x > 0} /// The "key" type type key : eqtype = usize @@ -514,7 +519,7 @@ let hash_map_s_find slot_s_find k slot let hash_map_s_len - (#t : Type0) (hm : hash_map_s_nes t) : + (#t : Type0) (hm : hash_map_s t) : nat = length (flatten hm) @@ -583,21 +588,76 @@ let hash_map_t_base_inv (#t : Type0) (hm : hash_map_t t) : Type0 = hm.hash_map_max_load = (capacity * dividend) / divisor end +/// We often need to frame some values +let hash_map_t_same_params (#t : Type0) (hm0 hm1 : hash_map_t t) : Type0 = + length hm0.hash_map_slots = length hm1.hash_map_slots /\ + hm0.hash_map_max_load = hm1.hash_map_max_load /\ + hm0.hash_map_max_load_factor = hm1.hash_map_max_load_factor + +(**** Invariant, models: revealed *) +/// The following invariants, etc. are meant to be revealed to the user through +/// the .fsti. + /// Invariant for the hashmap let hash_map_t_inv (#t : Type0) (hm : hash_map_t t) : Type0 = // Base invariant hash_map_t_base_inv hm /\ // The hash map is either: not overloaded, or we can't resize it - (let (dividend, divisor) = hm.hash_map_max_load_factor in - hm.hash_map_num_entries <= hm.hash_map_max_load - || length hm.hash_map_slots * 2 * dividend > usize_max) + begin + let (dividend, divisor) = hm.hash_map_max_load_factor in + hm.hash_map_num_entries <= hm.hash_map_max_load + || length hm.hash_map_slots * 2 * dividend > usize_max + end + +/// The high-level representation we give to the user +type map_s (t : Type0) = { + slots : hash_map_s t; + max_load_divid : usize; + max_load_divis : usize; +} + +val to_v (#t : Type0) (hm : hash_map_t t) : map_s t +let to_v #t hm = + let slots = hash_map_t_v hm in + let (max_load_divid, max_load_divis) = hm.hash_map_max_load_factor in + { + slots; + max_load_divid; + max_load_divis; + } + +val len_s (#t : Type0) (m : map_s t) : nat +let len_s #t m = hash_map_s_len m.slots + +let map_s_max_load (#t : Type0) (m : map_s t{m.max_load_divis > 0}) : nat = + let capacity = length m.slots in + let dividend = m.max_load_divid in + let divisor = m.max_load_divis in + (capacity * dividend) / divisor + +let map_s_base_inv (#t : Type0) (m : map_s t) : Type0 = + hash_map_s_inv m.slots /\ + // Load computation + begin + let capacity = length m.slots in + let dividend = m.max_load_divid in + let divisor = m.max_load_divis in + 0 < dividend /\ dividend < divisor /\ + capacity * dividend >= divisor + end + +let map_s_inv (#t : Type0) (m : map_s t) : Type0 = + map_s_base_inv m /\ + // The hash map is either: not overloaded, or we can't resize it + begin + let capacity = length m.slots in + let dividend = m.max_load_divid in + let divisor = m.max_load_divis in + let num_entries = len_s m in + let max_load = map_s_max_load m in + num_entries <= max_load || capacity * 2 * dividend > usize_max + end -/// We often need to frame some values -let hash_map_same_params (#t : Type0) (hm0 hm1 : hash_map_t t) : Type0 = - length hm0.hash_map_slots = length hm1.hash_map_slots /\ - hm0.hash_map_max_load = hm1.hash_map_max_load /\ - hm0.hash_map_max_load_factor = hm1.hash_map_max_load_factor - (*** allocate_slots *) /// Auxiliary lemma @@ -799,7 +859,7 @@ val hash_map_clear_fwd_back_lem_fun // The hash map invariant is satisfied hash_map_t_base_inv hm /\ // We preserved the parameters - hash_map_same_params hm self /\ + hash_map_t_same_params hm self /\ // The hash map has 0 values hash_map_t_len_s hm = 0 /\ // It contains no bindings @@ -1296,7 +1356,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s | Fail, Fail -> True | Return hm, Return hm_v -> hash_map_t_base_inv hm /\ - hash_map_same_params hm self /\ + hash_map_t_same_params hm self /\ hash_map_t_v hm == hm_v /\ hash_map_s_len hm_v == hash_map_t_len_s hm | _ -> False @@ -1526,7 +1586,7 @@ val hash_map_move_elements_from_list_fwd_back_lem | Return hm', Return hm_v -> hash_map_t_base_inv hm' /\ hash_map_t_v hm' == hm_v /\ - hash_map_same_params hm' ntable + hash_map_t_same_params hm' ntable | _ -> False)) (decreases (hash_map_move_elements_from_list_decreases t ntable ls)) @@ -1640,7 +1700,7 @@ val hash_map_move_elements_fwd_back_lem_refin | Return (ntable', _), Return ntable'_v -> hash_map_t_base_inv ntable' /\ hash_map_t_v ntable' == ntable'_v /\ - hash_map_same_params ntable' ntable + hash_map_t_same_params ntable' ntable | _ -> False)) (decreases (length slots - i)) @@ -2311,7 +2371,7 @@ val hash_map_move_elements_fwd_back_lem // The invariant is preserved hash_map_t_base_inv ntable' /\ // We preserved the parameters - hash_map_same_params ntable' ntable /\ + hash_map_t_same_params ntable' ntable /\ // The table has the same number of slots length ntable'.hash_map_slots = length ntable.hash_map_slots /\ // The count is good @@ -2714,7 +2774,7 @@ let hash_map_insert_fwd_back_lem t self key value = let self_v = hash_map_t_v self in let hm'_v = Return?.v (hash_map_insert_no_resize_s self_v key value) in assert(hash_map_t_base_inv hm'); - assert(hash_map_same_params hm' self); + assert(hash_map_t_same_params hm' self); assert(hash_map_t_v hm' == hm'_v); assert(hash_map_s_len hm'_v == hash_map_t_len_s hm'); // Expanding the post of [hash_map_insert_no_resize_s_lem] @@ -3200,7 +3260,7 @@ val hash_map_remove_back_lem_refin match hash_map_remove_back t self key with | Fail -> False | Return hm' -> - hash_map_same_params hm' self /\ + hash_map_t_same_params hm' self /\ hash_map_t_v hm' == hash_map_remove_s (hash_map_t_v self) key /\ // The length is decremented iff the key was in the map (let len = hash_map_t_len_s self in @@ -3336,7 +3396,7 @@ val hash_map_remove_back_lem | Fail -> False | Return hm' -> hash_map_t_inv self /\ - hash_map_same_params hm' self /\ + hash_map_t_same_params hm' self /\ hash_map_t_v hm' == hash_map_remove_s (hash_map_t_v self) key /\ // The length is decremented iff the key was in the map (let len = hash_map_t_len_s self in |