diff options
Diffstat (limited to 'tests/hashmap')
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 101 |
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)) |