summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
authorSon Ho2022-02-11 15:26:03 +0100
committerSon Ho2022-02-11 15:26:03 +0100
commit8265d379754eef7be20000bb2b2f4a4686371a22 (patch)
tree22ed9d28a56b793fcafd61f3aeae618dcb01440f /tests/hashmap
parentb6bf95d8bc588aad324257d2674a2196a6b09311 (diff)
Finish the proof of [hash_map_insert_no_resize_fwd_back_le]
Diffstat (limited to 'tests/hashmap')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst38
1 files changed, 36 insertions, 2 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index c1ac8ea9..6cec0921 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -133,6 +133,38 @@ let rec map_list_update_lem #a #b f ls i x =
else map_list_update_lem f ls' (i-1) x
#pop-options
+val length_flatten_update :
+ #a:Type
+ -> ls:list (list a)
+ -> i:nat{i < length ls}
+ -> x:list a ->
+ Lemma (
+ // 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)
+
+#push-options "--fuel 1"
+let rec length_flatten_update #a ls i x =
+ 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
+ begin
+ let ls1 = x :: ls' in
+ assert(list_update ls i x == ls1);
+ assert(flatten ls1 == x @ flatten ls'); // Triggers patterns
+ assert(length (flatten ls1) == length x + length (flatten ls'));
+ ()
+ end
+ else
+ begin
+ length_flatten_update ls' (i-1) x;
+ let ls1 = x' :: list_update ls' (i-1) x in
+ assert(flatten ls1 == x' @ flatten (list_update ls' (i-1) x)) // Triggers patterns
+ end
+#pop-options
(*** Utilities *)
// TODO: filter the utilities
@@ -1240,7 +1272,8 @@ let hash_map_insert_no_resize_fwd_back_lem t self key value =
assert(hm_v == list_update self_v hash_mod (list_t_v l0));
assert_norm(length [(key,value)] = 1);
assert(length (list_t_v l0) = length (list_t_v l) + 1);
- assume(hash_map_slots_len_s hm_v = hash_map_t_len_s hm)
+ length_flatten_update self_v hash_mod (list_t_v l0);
+ assert(hash_map_slots_len_s hm_v = hash_map_t_len_s hm)
end
end
end
@@ -1257,7 +1290,8 @@ let hash_map_insert_no_resize_fwd_back_lem t self key value =
let hm_v = hash_map_t_slots_v hm in
assert(hm_v == list_update self_v hash_mod (list_t_v l0));
assert(length (list_t_v l0) = length (list_t_v l));
- assume(hash_map_slots_len_s hm_v = hash_map_t_len_s hm)
+ length_flatten_update self_v hash_mod (list_t_v l0);
+ assert(hash_map_slots_len_s hm_v = hash_map_t_len_s hm)
end
end
end