summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/hashmap/Hashmap.Properties.fst113
1 files changed, 85 insertions, 28 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 272819dc..48b125d1 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -133,6 +133,7 @@ module InteractiveHelpers = FStar.InteractiveHelpers
/// 1. 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 instead.
+/// In particular, it made [hash_map_move_elements_fwd_back_lem_refin] annoying.
///
/// I guess this specific type has something to do with the fact that F*'s type
/// inference yields a different result, in combination with the poor support for
@@ -663,10 +664,10 @@ let hash_map_t_base_inv (#t : Type0) (hm : hash_map_t t) : Type0 =
/// Invariant for the hashmap
let hash_map_t_inv (#t : Type0) (hm : hash_map_t t) : Type0 =
// Base invariant
- hash_map_t_base_inv hm
+ hash_map_t_base_inv hm /\
// The hash map is either: not overloaded, or we can't resize it
-// (hm.hash_map_num_entries <= hm.hash_map_max_load
-// || length hm.hash_map_slots * 2 > usize_max)
+ (hm.hash_map_num_entries <= hm.hash_map_max_load
+ || length hm.hash_map_slots * 2 > usize_max)
/// The following predicate links the hashmap to an associative list.
/// Note that it does not compute the representant: different (permuted)
@@ -877,13 +878,15 @@ let rec hash_map_clear_slots_fwd_back_lem
val hash_map_clear_fwd_back_lem_fun
(t : Type0) (self : hash_map_t t) :
Lemma
- (requires (hash_map_t_inv self))
+ (requires (hash_map_t_base_inv self))
(ensures (
match hash_map_clear_fwd_back t self with
| Fail -> False
| Return hm ->
// The hash map invariant is satisfied
- hash_map_t_inv hm /\
+ hash_map_t_base_inv hm /\
+ // We preserved the parameters
+ hash_map_same_params hm self /\
// The hash map has 0 values
hash_map_t_len_s hm = 0 /\
// It contains no bindings
@@ -1367,7 +1370,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
(t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
Lemma
(requires (
- hash_map_t_inv self /\
+ hash_map_t_base_inv self /\
hash_map_slots_s_len (hash_map_t_slots_v self) = hash_map_t_len_s self))
(ensures (
begin
@@ -1376,7 +1379,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
with
| Fail, Fail -> True
| Return hm, Return hm_v ->
- hash_map_t_inv hm /\
+ hash_map_t_base_inv hm /\
hash_map_same_params hm self /\
hash_map_t_slots_v hm == hm_v /\
hash_map_slots_s_len hm_v == hash_map_t_len_s hm
@@ -1580,14 +1583,14 @@ let rec hash_map_move_elements_from_list_s
/// Refinement lemma
val hash_map_move_elements_from_list_fwd_back_lem
(t : Type0) (ntable : hash_map_t_nes t) (ls : list_t t) :
- Lemma (requires (hash_map_t_inv ntable))
+ Lemma (requires (hash_map_t_base_inv ntable))
(ensures (
match hash_map_move_elements_from_list_fwd_back t ntable ls,
hash_map_move_elements_from_list_s (hash_map_t_slots_v ntable) (slot_t_v ls)
with
| Fail, Fail -> True
| Return hm', Return hm_v ->
- hash_map_t_inv hm' /\
+ hash_map_t_base_inv hm' /\
hash_map_t_slots_v hm' == hm_v /\
hash_map_same_params hm' ntable
| _ -> False))
@@ -1648,14 +1651,14 @@ val hash_map_move_elements_fwd_back_lem_refin
(slots : vec (list_t t)) (i : usize{i <= length slots}) :
Lemma
(requires (
- hash_map_t_inv ntable))
+ hash_map_t_base_inv ntable))
(ensures (
match hash_map_move_elements_fwd_back t ntable slots i,
hash_map_move_elements_s (hash_map_t_slots_v ntable) (slots_t_v slots) i
with
| Fail, Fail -> True // We will prove later that this is not possible
| Return (ntable', _), Return ntable'_v ->
- hash_map_t_inv ntable' /\
+ hash_map_t_base_inv ntable' /\
hash_map_t_slots_v ntable' == ntable'_v /\
hash_map_same_params ntable' ntable
| _ -> False))
@@ -1663,13 +1666,37 @@ val hash_map_move_elements_fwd_back_lem_refin
// 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.
+// I guess it is because
+//
+// This proof was super unstable for some reasons.
+//
+// For instance, a type abbreviation instead of the same type but expanded
+// led to a failure. This behaviour led me to the hypothesis that maybe it
+// it made F*'s type inference end up with a different result, which combined
+// with its poor support for subtyping made the proof failed.
+//
+// However, later, unwrapping a definition led to another failure.
+//
+// I thus tried to manually unfold some postconditions because it
+// seemed to work for [hash_map_move_elements_fwd_back_lem] but it didn't
+// succeed.
+//
+// I tried to increase the ifuel to 2, 3: it didn't work, and I fell back to
+// other methods. Finally out of angriness I swiched the ifuel to 4 for some
+// reason: everything worked fine.
+// I have *no clue* why 4 is the magic number.
+//
+// The terrible thing is that this refinement proof is conceptually super simple:
+// - there are maybe two arithmetic proofs, which are directly solved by the
+// precondition
+// - we need to refine the call to [hash_map_move_elements_from_list_fwd_back]:
+// this is proven by another refinement lemma we proved above
+// - there is the recursive call (trivial)
+// Huge waste of time...
#restart-solver
-#push-options "--z3rlimit 200 --fuel 1"
+#push-options "--z3rlimit 300 --fuel 1 --ifuel 4"
let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
- assert(hash_map_t_inv ntable);
+ assert(hash_map_t_base_inv ntable);
let i0 = vec_len (list_t t) slots in
let b = i < i0 in
if b
@@ -1680,6 +1707,17 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
let l0 = mem_replace_fwd (list_t t) l ListNil in
assert(l0 == l);
hash_map_move_elements_from_list_fwd_back_lem t ntable l0;
+ begin
+ match hash_map_move_elements_from_list_fwd_back t ntable l0,
+ hash_map_move_elements_from_list_s (hash_map_t_slots_v ntable) (slot_t_v l0)
+ with
+ | Fail, Fail -> ()
+ | Return hm', Return hm_v ->
+ assert(hash_map_t_base_inv hm');
+ assert(hash_map_t_slots_v hm' == hm_v);
+ assert(hash_map_same_params hm' ntable)
+ | _ -> assert(False)
+ end;
begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with
| Fail -> ()
| Return h ->
@@ -1692,9 +1730,28 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
| Fail -> ()
| Return i1 ->
hash_map_move_elements_fwd_back_lem_refin t h v i1;
+ begin
+ match hash_map_move_elements_fwd_back t h v i1,
+ hash_map_move_elements_s (hash_map_t_slots_v h) (slots_t_v v) i1
+ with
+ | Fail, Fail -> ()
+ | Return (ntable', _), Return ntable'_v ->
+ assert(hash_map_t_base_inv ntable');
+ assert(hash_map_t_slots_v ntable' == ntable'_v);
+ assert(hash_map_same_params ntable' ntable)
+ | _ -> assert(False)
+ end;
begin match hash_map_move_elements_fwd_back t h v i1 with
- | Fail -> ()
- | Return (h0, v0) -> ()
+ | Fail ->
+ assert(hash_map_move_elements_fwd_back t ntable slots i == Fail);
+ ()
+ | Return (ntable', v0) ->
+ begin
+ // Trying to prove the postcondition
+ match hash_map_move_elements_fwd_back t ntable slots i with
+ | Fail -> assert(False)
+ | Return (ntable'', _) -> assert(ntable'' == ntable')
+ end
end
end
end
@@ -2017,12 +2074,12 @@ let slots_t_inv_implies_slots_s_inv #t slots =
// Problem is: I can never really predict for sure with F*...
()
-val hash_map_t_inv_implies_hash_map_slots_s_inv
+val hash_map_t_base_inv_implies_hash_map_slots_s_inv
(#t : Type0) (hm : hash_map_t t) :
- Lemma (requires (hash_map_t_inv hm))
+ Lemma (requires (hash_map_t_base_inv hm))
(ensures (hash_map_slots_s_inv (hash_map_t_slots_v hm)))
-let hash_map_t_inv_implies_hash_map_slots_s_inv #t hm = () // same as previous
+let hash_map_t_base_inv_implies_hash_map_slots_s_inv #t hm = () // same as previous
/// Introducing a "partial" version of the hash map invariant, which operates on
/// a suffix of the hash map.
@@ -2076,12 +2133,12 @@ val hash_map_slots_s_inv_implies_assoc_list_lem
let hash_map_slots_s_inv_implies_assoc_list_lem #t hm =
partial_hash_map_slots_s_inv_implies_assoc_list_lem (length hm) 0 hm
-val hash_map_t_inv_implies_assoc_list_lem
+val hash_map_t_base_inv_implies_assoc_list_lem
(#t : Type0) (hm : hash_map_t t):
- Lemma (requires (hash_map_t_inv hm))
+ Lemma (requires (hash_map_t_base_inv hm))
(ensures (assoc_list_inv (hash_map_t_v hm)))
-let hash_map_t_inv_implies_assoc_list_lem #t hm =
+let hash_map_t_base_inv_implies_assoc_list_lem #t hm =
hash_map_slots_s_inv_implies_assoc_list_lem (hash_map_t_slots_v hm)
/// For some reason, we can't write the below [forall] directly in the [ensures]
@@ -2099,7 +2156,7 @@ val hash_map_move_elements_fwd_back_lem
Lemma
(requires (
let al = flatten (slots_t_v slots) in
- hash_map_t_inv ntable /\
+ hash_map_t_base_inv ntable /\
length al <= usize_max /\
assoc_list_inv al /\
// The table is empty
@@ -2112,7 +2169,7 @@ val hash_map_move_elements_fwd_back_lem
with
| Return (ntable', _), Return ntable'_v ->
// The invariant is preserved
- hash_map_t_inv ntable' /\
+ hash_map_t_base_inv ntable' /\
// The table has the same number of slots
length ntable'.hash_map_slots = length ntable.hash_map_slots /\
// The count is good
@@ -2144,7 +2201,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
with
| Fail, Fail -> ()
| Return (ntable', _), Return ntable'_v ->
- assert(hash_map_t_inv ntable');
+ assert(hash_map_t_base_inv ntable');
assert(hash_map_t_slots_v ntable' == ntable'_v)
| _ -> assert(False)
end;
@@ -2163,7 +2220,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
hash_map_move_elements_s_flat ntable_v al
with
| Return (ntable', _), Return ntable'_v ->
- assert(hash_map_t_inv ntable');
+ assert(hash_map_t_base_inv ntable');
assert(length ntable'.hash_map_slots = length ntable.hash_map_slots);
// Rk.: Adding the following let binding makes the proof fails even with a huge
// rlitmit. Really having fun here...