summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst201
1 files changed, 190 insertions, 11 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 89401c02..2c40f417 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -13,25 +13,51 @@ module InteractiveHelpers = FStar.InteractiveHelpers
#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
/// The proofs actually caused a lot more trouble than expected, because:
+///
/// - we are blind when doing the proofs. After a very intensive use of F* I got
-/// used to it meaning I can *do* proofs in F*, but it still takes me a tremendous
+/// used to it meaning I *can* do proofs in F*, but it still takes me a tremendous
/// amout of energy to visualize the context in my head and, for instance,
/// properly instantiate the lemmas or insert the necessary assertions in the code.
/// I actually often write assertions that I assume just to *check* that those
/// assertions make the proofs pass and are thus indeed the ones I want to prove,
/// which is something very specific to working with F*.
+///
/// - F* is extremely bad at reasoning with quantifiers, which is made worse by
/// the fact we are blind when making proofs. This forced me to be extremely
/// careful about the way I wrote the specs/invariants (by writing "functional"
-/// specs and invariants, mostly, so as not to manipulate quantifiers)
+/// specs and invariants, mostly, so as not to manipulate quantifiers), ending
+/// up proofs which are not written in the most natural and efficient manner.
+/// In particular, I had to cut the proofs into many steps just for this reason,
+/// while if I had been able to properly use quantifiers (I tried: in many
+/// situations I manage to massage F* to make it work, but in the below proofs
+/// it was horrific) I would have proven many results in one go.
+///
/// - 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).
-/// - we can't easily prove intermediate results which require a recursive proofs
+///
+/// - we can't prove intermediate results which require a recursive proofs
/// inside of other proofs, meaning that whenever we need such a result we need
/// to write an intermediate lemma, which is extremely cumbersome.
+/// What is extremely frustrating is that in most situations, those intermediate
+/// lemmas are extremely simple to prove: they would simply need 2 or 3 tactic
+/// calls in Coq or HOL4, and in F* the proof is reduced to a recursive call.
+/// Isolating the lemma (i.e., writing its signature), however, takes some
+/// non-negligible time, which is made worse by the fact that, once again,
+/// we don't have proof contexts to stare at which would help figuring out
+/// how to write such lemmas.
+///
+/// - the proofs often fail or succeed for extremely unpredictable reasons, and are
+/// extremely hard to debug. See [hash_map_slots_s_nes] below: it is simply a
+/// definition with a refinment. For some reason, at some places if we use this
+/// type abbreviation some proofs break, meaning we have to write the unfolded
+/// version.
+/// I guess it has something to do with the fact that F*'s type inference yields
+/// a different result, in combination with the poor support for subtyping. The
+/// problem is that it is extremely hard to debug, and I definitely don't want
+/// to waste time with this kind of boring, tedious proofs.
///
/// The result is that I had to poor a lot more thinking than I expected in the below
/// proofs, in particular to:
@@ -39,8 +65,8 @@ module InteractiveHelpers = FStar.InteractiveHelpers
/// - subdivide all the theorems into very small, modular lemmas that I could reason
/// about independently, in a small context, and with quick responses from F*.
///
-/// Note that in a theorem prover with tactics, most of the below proof would have
-/// been extremely straightforward.
+/// Finally, I strongly that in a theorem prover with tactics, most of the below proof
+/// would have been extremely straightforward.
(*** List lemmas *)
@@ -359,6 +385,9 @@ let slot_find (#t : Type0) (k : key) (slot : list (binding t)) : option t =
| None -> None
| Some (_, v) -> Some v
+let assoc_list_find (#t : Type0) (k : key) (slot : assoc_list t) : option t =
+ slot_find k slot
+
let slot_t_find_s (#t : Type0) (k : key) (slot : list_t t) : option t =
match find (same_key k) (list_t_v slot) with
| None -> None
@@ -367,6 +396,7 @@ let slot_t_find_s (#t : Type0) (k : key) (slot : list_t t) : option t =
// This is a simpler version of the "find" function, which captures the essence
// of what happens and operates on [hash_map_slots_s].
// TODO: useful?
+// TODO: at some point I used hash_map_slots_s_nes and it broke proofs...
let hash_map_slots_s_find
(#t : Type0) (hm : hash_map_slots_s t{length hm <= usize_max /\ length hm > 0})
(k : key) : option t =
@@ -374,6 +404,7 @@ let hash_map_slots_s_find
let slot = index hm i in
slot_find k slot
+// TODO: at some point I used hash_map_slots_s_nes and it broke proofs...
let hash_map_slots_s_len
(#t : Type0) (hm : hash_map_slots_s t{length hm <= usize_max /\ length hm > 0}) :
nat =
@@ -432,7 +463,7 @@ type slot_t_inv_not_same_keys_f (#t : Type0) (i : usize) (slot : list_t t) =
/// Invariants for the slots
let slot_s_inv
-(#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list (binding t)) : bool =
+ (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list (binding t)) : bool =
// All the bindings are in the proper slot
for_all (same_hash_mod_key len i) slot &&
// All the keys are pairwise distinct
@@ -1226,6 +1257,7 @@ let hash_map_insert_in_list_back_lem t len key value ls =
/// We work on [hash_map_slots_s] (we use a higher-level view of the hash-map, but
/// not too high).
+// TODO: at some point I used hash_map_slots_s_nes and it broke proofs...x
let hash_map_insert_no_resize_s
(#t : Type0) (hm : hash_map_slots_s t{length hm <= usize_max /\ length hm > 0})
(key : usize) (value : t) :
@@ -1260,7 +1292,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
| Return hm, Return hm_v ->
hash_map_t_inv hm /\
hash_map_t_slots_v hm == hm_v /\
- hash_map_slots_s_len hm_v = hash_map_t_len_s hm
+ hash_map_slots_s_len hm_v == hash_map_t_len_s hm
| _ -> False
end))
@@ -1334,6 +1366,46 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
end
end
+(**** insert_no_resize: invariants *)
+
+val hash_map_insert_no_resize_s_lem
+ (#t : Type0) (hm : hash_map_slots_s_nes t)
+ (key : usize) (value : t) :
+ Lemma
+ (requires (
+ hash_map_slots_s_inv hm))
+ (ensures (
+ match hash_map_insert_no_resize_s hm key value with
+ | Fail ->
+ // Can fail only if we need to create a new binding in
+ // an already saturated map
+ hash_map_slots_s_len hm = usize_max /\
+ None? (hash_map_slots_s_find hm key)
+ | Return hm' ->
+ // The invariant is preserved
+ hash_map_slots_s_inv hm' /\
+ // [key] maps to [value]
+ hash_map_slots_s_find hm' key == Some value /\
+ // The other bindings are preserved
+ (forall k'. k' <> key ==> hash_map_slots_s_find hm' k' == hash_map_slots_s_find hm k') /\
+ // 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
+ | Some _ -> hash_map_slots_s_len hm' = hash_map_slots_s_len hm)))
+
+let hash_map_insert_no_resize_s_lem #t hm key value =
+ let num_entries = length (flatten hm) in
+ if None? (hash_map_slots_s_find hm key) && num_entries = usize_max then ()
+ else
+ begin
+ let len = length hm in
+ let i = hash_mod_key key len in
+ let slot = index hm i in
+ hash_map_insert_in_list_s_lem t len key value slot;
+ let slot' = hash_map_insert_in_list_s key value slot in
+ length_flatten_update hm i slot'
+ end
+
(**** find after insert *)
/// Lemmas about what happens if we call [find] after an insertion
@@ -1500,6 +1572,11 @@ val hash_map_move_elements_fwd_back_lem
| _ -> False))
(decreases (length slots - i))
+// Rk.: if above we update some definitions to use [hash_map_slots_s_nes]
+// instead of writing refinements explicitly, it makes the proof breaks.
+// I guess it is because F* does a different type inference, which combines
+// poorly with its poor support for subtyping. Problem is: I have no idea
+// where this happens and it is extremely hard to debug.
#restart-solver
#push-options "--z3rlimit 200 --fuel 1"
let rec hash_map_move_elements_fwd_back_lem t ntable slots i =
@@ -1713,8 +1790,8 @@ let rec flatten_i_same_suffix #a l0 l1 i =
/// Refinement lemma:
/// [hash_map_move_elements_s] refines [hash_map_move_elements_s_flat]
-val hash_map_move_elements_s_flat_lem
- (#t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)})
+val hash_map_move_elements_s_lem_refin_flat
+ (#t : Type0) (hm : hash_map_slots_s_nes t)
(slots : slots_s t)
(i : nat{i <= length slots /\ length slots <= usize_max}) :
Lemma
@@ -1728,7 +1805,7 @@ val hash_map_move_elements_s_flat_lem
(decreases (length slots - i))
#push-options "--fuel 1"
-let rec hash_map_move_elements_s_flat_lem #t hm slots i =
+let rec hash_map_move_elements_s_lem_refin_flat #t hm slots i =
let len = length slots in
if i < len then
begin
@@ -1742,13 +1819,115 @@ let rec hash_map_move_elements_s_flat_lem #t hm slots i =
| Return hm' ->
let slots' = list_update slots i [] in
flatten_i_same_suffix slots slots' (i+1);
- hash_map_move_elements_s_flat_lem hm' slots' (i+1);
+ hash_map_move_elements_s_lem_refin_flat hm' slots' (i+1);
hash_map_move_elements_s_flat_append_lem hm slot (flatten_i slots' (i+1));
()
end
else ()
#pop-options
+let assoc_list_inv (#t : Type0) (al : assoc_list t) : Type0 =
+ // All the keys are pairwise distinct
+ pairwise_rel binding_neq al
+
+let disjoint_hm_al_on_key
+ (#t : Type0) (hm : hash_map_slots_s_nes t) (al : assoc_list t) (k : key) : Type0 =
+ match hash_map_slots_s_find hm k, find (same_key k) al with
+ | Some _, None
+ | None, Some _
+ | None, None -> True
+ | Some _, Some _ -> False
+
+/// Playing a dangerous game here: using forall quantifiers
+let disjoint_hm_al (#t : Type0) (hm : hash_map_slots_s_nes t) (al : assoc_list t) : Type0 =
+ forall (k:key). disjoint_hm_al_on_key hm al k
+
+let find_in_union_hm_al
+ (#t : Type0) (hm : hash_map_slots_s_nes t) (al : assoc_list t) (k : key) :
+ option t =
+ match hash_map_slots_s_find hm k with
+ | Some b -> Some b
+ | None -> assoc_list_find k al
+
+val hash_map_move_elements_s_flat_lem
+ (#t : Type0) (hm : hash_map_slots_s_nes t) (al : assoc_list t) :
+ Lemma
+ (requires (
+ // Invariants
+ hash_map_slots_s_inv hm /\
+ assoc_list_inv al /\
+ // The two are disjoint
+ disjoint_hm_al hm al /\
+ // We can add all the elements to the hashmap
+ hash_map_slots_s_len hm + length al <= usize_max))
+ (ensures (
+ match hash_map_move_elements_s_flat hm al with
+ | Fail -> False // We can't fail
+ | Return hm' ->
+ // The invariant is preserved
+ hash_map_slots_s_inv hm' /\
+ // The new hash map is the union of the two maps
+ (forall (k:key). hash_map_slots_s_find hm' k == find_in_union_hm_al hm al k)))
+ (decreases al)
+
+// TODO: here
+#push-options "--z3rlimit 200 --fuel 1"
+let rec hash_map_move_elements_s_flat_lem #t hm al =
+ match al with
+ | [] -> ()
+ | (k,v) :: al' ->
+ hash_map_insert_no_resize_s_lem hm k v;
+ match hash_map_insert_no_resize_s hm k v with
+ | Fail -> ()
+ | Return hm' ->
+ assert(hash_map_slots_s_inv hm');
+ assert(assoc_list_inv al');
+ assume(disjoint_hm_al hm' al');
+ assume(hash_map_slots_s_len hm' + length al' <= usize_max);
+ hash_map_move_elements_s_flat_lem hm' al';
+ admit()
+#pop-options
+
+val hash_map_insert_no_resize_s_lem
+ (#t : Type0) (hm : hash_map_slots_s_nes t)
+ (key : usize) (value : t) :
+ Lemma
+ (requires (
+ hash_map_slots_s_inv hm))
+ (ensures (
+ match hash_map_insert_no_resize_s hm key value with
+ | Fail ->
+ // Can fail only if we need to create a new binding in
+ // an already saturated map
+ hash_map_slots_s_len hm = usize_max /\
+ None? (hash_map_slots_s_find hm key)
+ | Return hm' ->
+ // The invariant is preserved
+ hash_map_slots_s_inv hm' /\
+ // [key] maps to [value]
+ hash_map_slots_s_find hm' key == Some value /\
+ // The other bindings are preserved
+ (forall k'. k' <> key ==> hash_map_slots_s_find hm' k' == hash_map_slots_s_find hm k') /\
+ // 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
+ | Some _ -> hash_map_slots_s_len hm' = hash_map_slots_s_len hm)))
+
+(*
+let rec hash_map_move_elements_s_flat
+ (#t : Type0) (ntable : hash_map_slots_s_nes t)
+ (slots : hash_map_s t) :
+ Tot (result_hash_map_slots_s_nes t)
+ (decreases slots) =
+ match slots with
+ | [] -> Return ntable
+ | (k,v) :: slots' ->
+ match hash_map_insert_no_resize_s ntable k v with
+ | Fail -> Fail
+ | Return ntable' ->
+ hash_map_move_elements_s_flat ntable' slots'
+
+
(*
/// [nhm]: the new hash map (in which we insert elements)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 13:47:05 +0000