summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-13 15:46:54 +0100
committerSon Ho2022-02-13 15:46:54 +0100
commitfd3694d71a03022c7fb1423c7f6fbbd528eeb987 (patch)
tree32caa77228c0b3a009841cedaed4387e0a37a17a
parent08130619b474dc87ba923e789f25dbb4a9b6ec94 (diff)
Make good progress on the invariant proofs for remove'back
-rw-r--r--tests/hashmap/Hashmap.Properties.fst150
1 files changed, 132 insertions, 18 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 08ae5714..8b53268b 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -170,6 +170,22 @@ module InteractiveHelpers = FStar.InteractiveHelpers
/// See [hash_map_insert_fwd_back_lem] for instance.
+/// The proof strategy is to do exactly as with Low* proofs (we initially tried to
+/// prove more properties in one go, but it was a mistake):
+/// - prove that, under some preconditions, the low-level functions translated
+/// from Rust refine some higher-level functions
+/// - do functional proofs about those high-level functions to prove interesting
+/// properties about the hash map operations, and invariant preservation
+/// - combine everything
+///
+/// The fact that we work in a pure setting allows us to be more modular than when
+/// working with effects. For instance we can do a case disjunction (see the proofs
+/// for insert, which study the cases where the key is already/not in the hash map
+/// in separate proofs). We can also easily prove a refinement lemma, study the
+/// model, and combine those to also prove that the low-level function preserves
+/// the invariants.
+
+
(*** List lemmas *)
val index_append_lem (#a : Type0) (ls0 ls1 : list a) (i : nat{i < length ls0 + length ls1}) :
@@ -1559,9 +1575,9 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
let hash_map_t_updated_binding
(#t : Type0) (hm : hash_map_slots_s_nes t)
- (key : usize) (value : t) (hm' : hash_map_slots_s_nes t) : Type0 =
+ (key : usize) (opt_value : option t) (hm' : hash_map_slots_s_nes t) : Type0 =
// [key] maps to [value]
- hash_map_slots_s_find hm' key == Some value /\
+ hash_map_slots_s_find hm' key == opt_value /\
// The other bindings are preserved
(forall k'. k' <> key ==> hash_map_slots_s_find hm' k' == hash_map_slots_s_find hm k')
@@ -1570,7 +1586,7 @@ let insert_post (#t : Type0) (hm : hash_map_slots_s_nes t)
// The invariant is preserved
hash_map_slots_s_inv hm' /\
// [key] maps to [value] and the other bindings are preserved
- hash_map_t_updated_binding hm key value hm' /\
+ hash_map_t_updated_binding hm key (Some value) hm' /\
// The length is incremented, iff we inserted a new key
(match hash_map_slots_s_find hm key with
| None -> hash_map_slots_s_len hm' = hash_map_slots_s_len hm + 1
@@ -2734,7 +2750,7 @@ val hash_map_insert_fwd_back_lem
// The invariant is preserved
hash_map_t_inv hm' /\
// [key] maps to [value] and the other bindings are preserved
- hash_map_t_updated_binding (hash_map_t_slots_v self) key value (hash_map_t_slots_v hm') /\
+ hash_map_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm') /\
// 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
@@ -2745,10 +2761,10 @@ let hash_map_insert_fwd_back_bindings_lem
(hm' hm'' : hash_map_t_nes t) :
Lemma
(requires (
- hash_map_t_updated_binding (hash_map_t_slots_v self) key value (hash_map_t_slots_v hm') /\
+ hash_map_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm') /\
hash_map_t_same_bindings hm' hm''))
(ensures (
- hash_map_t_updated_binding (hash_map_t_slots_v self) key value (hash_map_t_slots_v hm'')))
+ hash_map_t_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm'')))
= ()
#restart-solver
@@ -3180,23 +3196,51 @@ let hash_map_remove_fwd_lem t self key =
(*** remove'back *)
+(**** Refinement proofs *)
+
/// High-level model for [remove_from_list'back]
let hash_map_remove_from_list_s
(#t : Type0) (key : usize) (ls : slot_s t) :
slot_s t =
filter_one (not_same_key key) ls
+(*
+// TODO: remove?
+val filter_one_find (#a : Type) (f g : a -> bool) (ls : list a) :
+ Lemma
+ (requires (forall x. f x <> g x))
+ (ensures (
+ let ls' = filter_one f ls in
+ match find g ls with
+ | None -> length ls' = length ls
+ | Some _ -> length ls' + 1 = length ls))
+
+#push-options "--fuel 1"
+let rec filter_one_find #a f g ls =
+ match ls with
+ | [] -> ()
+ | x :: ls' -> filter_one_find f g ls'
+#pop-options
+*)
+
/// Refinement lemma
-val hash_map_remove_from_list_back_lem
+val hash_map_remove_from_list_back_lem_refin
(#t : Type0) (key : usize) (ls : list_t t) :
Lemma
(ensures (
match hash_map_remove_from_list_back t key ls with
| Fail -> False
- | Return ls' -> list_t_v ls' == hash_map_remove_from_list_s key (list_t_v ls)))
+ | Return ls' ->
+ list_t_v ls' == hash_map_remove_from_list_s key (list_t_v ls) /\
+ // The length is decremented, iff the key was in the slot
+ (let len = length (list_t_v ls) in
+ let len' = length (list_t_v ls') in
+ match slot_find key (list_t_v ls) with
+ | None -> len = len'
+ | Some _ -> len = len' + 1)))
#push-options "--fuel 1"
-let rec hash_map_remove_from_list_back_lem #t key ls =
+let rec hash_map_remove_from_list_back_lem_refin #t key ls =
begin match ls with
| ListCons ckey x tl ->
let b = ckey = key in
@@ -3209,7 +3253,7 @@ let rec hash_map_remove_from_list_back_lem #t key ls =
end
else
begin
- hash_map_remove_from_list_back_lem key tl;
+ hash_map_remove_from_list_back_lem_refin key tl;
match hash_map_remove_from_list_back t key tl with
| Fail -> ()
| Return l -> let ls0 = ListCons ckey x l in ()
@@ -3229,7 +3273,7 @@ let hash_map_remove_s
list_update self hash slot'
/// Refinement lemma
-val hash_map_remove_back_lem
+val hash_map_remove_back_lem_refin
(#t : Type0) (self : hash_map_t_nes t) (key : usize) :
Lemma
(requires (
@@ -3239,9 +3283,17 @@ val hash_map_remove_back_lem
(ensures (
match hash_map_remove_back t self key with
| Fail -> False
- | Return hm' -> hash_map_t_slots_v hm' == hash_map_remove_s (hash_map_t_slots_v self) key))
-
-let hash_map_remove_back_lem #t self key =
+ | Return hm' ->
+ hash_map_same_params hm' self /\
+ hash_map_t_slots_v hm' == hash_map_remove_s (hash_map_t_slots_v self) key /\
+ // The length is decremented iff the key was in the map
+ (let len = hash_map_t_len_s self in
+ let len' = hash_map_t_len_s hm' in
+ match hash_map_t_find_s self key with
+ | None -> len = len'
+ | Some _ -> len = len' + 1)))
+
+let hash_map_remove_back_lem_refin #t self key =
begin match hash_key_fwd key with
| Fail -> ()
| Return i ->
@@ -3264,11 +3316,13 @@ let hash_map_remove_back_lem #t self key =
begin match x with
| None ->
begin
- hash_map_remove_from_list_back_lem key l;
+ hash_map_remove_from_list_back_lem_refin key l;
match hash_map_remove_from_list_back t key l with
| Fail -> ()
| Return l0 ->
- begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+ begin
+ length_flatten_update (slots_t_v v) hash_mod (list_t_v l0);
+ match vec_index_mut_back (list_t t) v hash_mod l0 with
| Fail -> ()
| Return v0 -> ()
end
@@ -3282,11 +3336,13 @@ let hash_map_remove_back_lem #t self key =
| Fail -> ()
| Return i3 ->
begin
- hash_map_remove_from_list_back_lem key l;
+ hash_map_remove_from_list_back_lem_refin key l;
match hash_map_remove_from_list_back t key l with
| Fail -> ()
| Return l0 ->
- begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+ begin
+ length_flatten_update (slots_t_v v) hash_mod (list_t_v l0);
+ match vec_index_mut_back (list_t t) v hash_mod l0 with
| Fail -> ()
| Return v0 -> ()
end
@@ -3297,3 +3353,61 @@ let hash_map_remove_back_lem #t self key =
end
end
end
+
+(**** Invariants, high-level properties *)
+
+val hash_map_remove_from_list_s_lem
+ (#t : Type0) (k : usize) (slot : slot_s t) (len : usize{len > 0}) (i : usize) :
+ Lemma
+ (requires (slot_s_inv len i slot))
+ (ensures (
+ let slot' = hash_map_remove_from_list_s k slot in
+ slot_s_inv len i slot' /\
+ slot_find k slot' == None /\
+ (forall (k':key{k' <> k}). slot_find k' slot' == slot_find k' slot) /\
+ // This postcondition is necessary to prove that the invariant is preserved
+ // in the recursive calls. This allows us to do the proof in one go.
+ (forall (b:binding t). for_all (binding_neq b) slot ==> for_all (binding_neq b) slot')
+ ))
+
+#push-options "--fuel 1"
+let rec hash_map_remove_from_list_s_lem #t key slot len i =
+ match slot with
+ | [] -> ()
+ | (k',v) :: slot' ->
+ if k' <> key then
+ begin
+ hash_map_remove_from_list_s_lem key slot' len i;
+ let slot'' = hash_map_remove_from_list_s key slot' in
+ assert(for_all (same_hash_mod_key len i) ((k',v)::slot''));
+ assert(for_all (binding_neq (k',v)) slot'); // Triggers instanciation
+ assert(for_all (binding_neq (k',v)) slot'')
+ end
+ else
+ begin
+ assert(for_all (binding_neq (k',v)) slot');
+ for_all_binding_neq_find_lem key v slot'
+ end
+#pop-options
+
+// TODO: rename hash_map_t_updated_binding to hash_map_slots_updated_binding
+
+val hash_map_remove_s_lem
+ (#t : Type0) (self : hash_map_slots_s_nes t) (key : usize) :
+ Lemma
+ (requires (hash_map_slots_s_inv self))
+ (ensures (
+ let hm' = hash_map_remove_s self key in
+ // The invariant is preserved
+ hash_map_slots_s_inv hm' /\
+ // We updated the binding
+ hash_map_t_updated_binding self key None hm'))
+
+let hash_map_remove_s_lem #t self key =
+ let len = length self in
+ let hash = hash_mod_key key len in
+ let slot = index self hash in
+ hash_map_remove_from_list_s_lem key slot len hash;
+ let slot' = hash_map_remove_from_list_s key slot in
+ let hm' = list_update self hash slot' in
+ assert(hash_map_slots_s_inv self)