summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst101
1 files changed, 92 insertions, 9 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index a698752a..f3644dc1 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -123,7 +123,7 @@ let rec pairwise_rel #a pred ls =
match ls with
| [] -> true
| x :: ls' ->
- List.Tot.for_all (pred x) ls' && pairwise_rel pred ls'
+ for_all (pred x) ls' && pairwise_rel pred ls'
/// The lack of lemmas about list manipulation is really annoying...
@@ -886,6 +886,11 @@ let hash_map_insert_no_resize_fwd_back_lem t self key value =
/// The proofs about [insert_in_list] backward are easier to do in several steps:
/// extrinsic proofs to the rescue!
/// Rk.: those proofs actually caused a lot of trouble because:
+/// - F* doesn't encode closures properly, the result being that it is very
+/// awkward to reason about functions like `map` or `find`, because we have
+/// to introduce auxiliary definitions for the parameters we give to those
+/// functions (if we use anonymous lambda functions, we're screwed by the
+/// encoding).
/// - F* is extremely bad at reasoning with quantifiers, which is made worse by
/// the fact we are blind when making proofs. This forced us to be extremely
/// careful about the way we wrote our specs/invariants (by writing "functional"
@@ -965,6 +970,8 @@ let rec hash_map_insert_in_list_back_lem_update_fun t key value ls =
/// to Coq, which makes it a bit cumbersome to prove auxiliary results like the
/// following ones...
+(** Auxiliary lemmas: append case *)
+
val slot_t_v_for_all_binding_neq_append_lem
(t : Type0) (key : usize) (value : t) (ls : list (binding t)) (b : binding t) :
Lemma
@@ -1036,6 +1043,84 @@ let hash_map_insert_in_list_back_lem_append t len key value ls =
assert(list_t_v ls' == list_t_v ls @ [(key,value)]);
slot_t_v_inv_not_find_append_end_inv_lem t len key value (list_t_v ls)
+(** Auxiliary lemmas: update case *)
+
+val slot_t_v_find_update_for_all_binding_neq_append_lem
+ (t : Type0) (key : usize) (value : t) (ls : list (binding t)) (b : binding t) :
+ Lemma
+ (requires (
+ fst b <> key /\
+ for_all (binding_neq b) ls /\
+ True
+// slot_t_v_find key ls == None
+ ))
+ (ensures (
+ let ls' = find_update (same_key key) ls (key, value) in
+ for_all (binding_neq b) ls'))
+
+#push-options "--fuel 1"
+let rec slot_t_v_find_update_for_all_binding_neq_append_lem t key value ls b =
+ match ls with
+ | [] -> ()
+ | (ck, cv) :: cls ->
+ slot_t_v_find_update_for_all_binding_neq_append_lem t key value cls b
+#pop-options
+
+/// Annoying auxiliary lemma we have to prove because there is no way to reason
+/// properly about closures.
+/// I'm really enjoying my time.
+val for_all_binding_neq_value_indep
+ (#t : Type0) (key : key) (v0 v1 : t) (ls : list (binding t)) :
+ Lemma (for_all (binding_neq (key,v0)) ls = for_all (binding_neq (key,v1)) ls)
+
+#push-options "--fuel 1"
+let rec for_all_binding_neq_value_indep #t key v0 v1 ls =
+ match ls with
+ | [] -> ()
+ | _ :: ls' -> for_all_binding_neq_value_indep #t key v0 v1 ls'
+#pop-options
+
+val slot_t_v_inv_find_append_end_inv_lem
+ (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list (binding t)) :
+ Lemma
+ (requires (
+ slot_t_v_inv len (hash_mod_key key len) ls /\
+ Some? (slot_t_v_find key ls)))
+ (ensures (
+ let ls' = find_update (same_key key) ls (key, value) in
+ slot_t_v_inv len (hash_mod_key key len) ls' /\
+ (slot_t_v_find key ls' == Some value) /\
+ (forall k'. k' <> key ==> slot_t_v_find k' ls' == slot_t_v_find k' ls)))
+
+#push-options "--z3rlimit 50 --fuel 1"
+let rec slot_t_v_inv_find_append_end_inv_lem t len key value ls =
+ match ls with
+ | [] -> ()
+ | (ck, cv) :: cls ->
+ let h = hash_mod_key key len in
+ let ls' = find_update (same_key key) ls (key, value) in
+ if ck = key then
+ begin
+ assert(ls' == (ck,value) :: cls);
+ assert(for_all (same_hash_mod_key len h) ls');
+ // For pairwise_rel: binding_neq (ck, value) is actually independent
+ // of `value`. Slightly annoying to prove in F*...
+ assert(for_all (binding_neq (ck,cv)) cls);
+ for_all_binding_neq_value_indep key cv value cls;
+ assert(for_all (binding_neq (ck,value)) cls);
+ assert(pairwise_rel binding_neq ls');
+ assert(slot_t_v_inv len (hash_mod_key key len) ls')
+ end
+ else
+ begin
+ slot_t_v_inv_find_append_end_inv_lem t len key value cls;
+ assert(for_all (same_hash_mod_key len h) ls');
+ slot_t_v_find_update_for_all_binding_neq_append_lem t key value cls (ck, cv);
+ assert(pairwise_rel binding_neq ls');
+ assert(slot_t_v_inv len h ls')
+ end
+#pop-options
+
/// [insert_in_list]: if the key is in the map, update the bindings (quantifiers)
val hash_map_insert_in_list_back_lem_update
(t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list_t t) :
@@ -1048,8 +1133,7 @@ val hash_map_insert_in_list_back_lem_update
| Fail -> False
| Return ls' ->
let als = list_t_v ls in
- let i = find_index (same_key key) als in
- list_t_v ls' == list_update als i (key,value) /\
+ list_t_v ls' == find_update (same_key key) als (key,value) /\
// The invariant is preserved
slot_t_inv len (hash_mod_key key len) ls' /\
// [key] maps to [value]
@@ -1058,13 +1142,13 @@ val hash_map_insert_in_list_back_lem_update
(forall k'. k' <> key ==> slot_t_find k' ls' == slot_t_find k' ls)))
let hash_map_insert_in_list_back_lem_update t len key value ls =
- admit()
-(* hash_map_insert_in_list_back_lem_append_fun t key value ls;
+ hash_map_insert_in_list_back_lem_update_fun t key value ls;
match hash_map_insert_in_list_back t key value ls with
| Fail -> ()
| Return ls' ->
- assert(list_t_v ls' == list_t_v ls @ [(key,value)]);
- slot_t_v_inv_not_find_append_end_inv_lem t len key value (list_t_v ls)*)
+ slot_t_v_inv_find_append_end_inv_lem t len key value (list_t_v ls)
+
+(** Final lemma about [insert_in_list] *)
/// [insert_in_list]
val hash_map_insert_in_list_back_lem
@@ -1087,8 +1171,7 @@ val hash_map_insert_in_list_back_lem
list_t_v ls' == list_t_v ls @ [(key,value)] /\
list_t_len ls' = list_t_len ls + 1
| Some _ ->
- let i = find_index (same_key key) (list_t_v ls) in
- list_t_v ls' == list_update (list_t_v ls) i (key,value) /\
+ list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,value) /\
list_t_len ls' = list_t_len ls)))
(decreases (hash_map_insert_in_list_decreases t key value ls))