summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst305
1 files changed, 132 insertions, 173 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 1465dd41..d280d537 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -183,7 +183,10 @@ open Hashmap.Funs
/// the invariants.
-(*** List lemmas *)
+(*** Utilities *)
+
+/// We need many small helpers and lemmas, mostly about lists (and the ones we list
+/// here are not in the standard F* library).
val index_append_lem (#a : Type0) (ls0 ls1 : list a) (i : nat{i < length ls0 + length ls1}) :
Lemma (
@@ -260,41 +263,6 @@ let rec find_append #a f ls0 ls1 =
else find_append f ls0' ls1
#pop-options
-(*** Lemmas about Primitives *)
-/// TODO: move those lemmas
-
-// TODO: rename to 'insert'?
-val list_update_index_dif_lem
- (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a)
- (j : nat{j < length ls}) :
- Lemma (requires (j <> i))
- (ensures (index (list_update ls i x) j == index ls j))
- [SMTPat (index (list_update ls i x) j)]
-
-#push-options "--fuel 1"
-let rec list_update_index_dif_lem #a ls i x j =
- match ls with
- | x' :: ls ->
- if i = 0 then ()
- else if j = 0 then ()
- else
- list_update_index_dif_lem ls (i-1) x (j-1)
-#pop-options
-
-val map_list_update_lem
- (#a #b: Type0) (f : a -> Tot b)
- (ls : list a) (i : nat{i < length ls}) (x : a) :
- Lemma (list_update (map f ls) i (f x) == map f (list_update ls i x))
- [SMTPat (list_update (map f ls) i (f x))]
-
-#push-options "--fuel 1"
-let rec map_list_update_lem #a #b f ls i x =
- match ls with
- | x' :: ls' ->
- if i = 0 then ()
- else map_list_update_lem f ls' (i-1) x
-#pop-options
-
val length_flatten_update :
#a:Type
-> ls:list (list a)
@@ -363,9 +331,6 @@ let rec forall_index_equiv_list_for_all pred ls =
forall_index_equiv_list_for_all pred ls'
#pop-options
-(*** Utilities *)
-// TODO: filter the utilities
-
val find_update:
#a:Type
-> f:(a -> Tot bool)
@@ -386,34 +351,6 @@ let rec pairwise_distinct (#a : eqtype) (ls : list a) : Tot bool =
| [] -> true
| x :: ls' -> List.Tot.for_all (fun y -> x <> y) ls' && pairwise_distinct ls'
-(*
-val for_allP: #a:Type -> f:(a -> Tot Type0) -> list a -> Tot Type0
-let rec for_allP (f : 'a -> Tot Type0) (l : list 'a) : Tot Type0 =
- match l with
- | [] -> True
- | hd::tl -> f hd /\ for_allP f tl
-*)
-
-(*
-val for_all_i_aux: #a:Type -> f:(nat -> a -> Tot bool) -> list a -> nat -> Tot bool
-let rec for_all_i_aux (f : nat -> 'a -> Tot bool) (l : list 'a) (i : nat) : Tot bool =
- match l with
- | [] -> true
- | hd::tl -> f i hd && for_all_i_aux f tl (i+1)
-
-val for_all_i: #a:Type -> f:(nat -> a -> Tot bool) -> list a -> Tot bool
-let for_all_i (f : nat -> 'a -> Tot bool) (l : list 'a) : Tot bool =
- for_all_i_aux f l 0
-*)
-
-(*val pairwise_relP : #a:Type -> pred:(a -> a -> Tot Type0) -> ls:list a -> Tot Type0
-let rec pairwise_relP #a pred ls =
- match ls with
- | [] -> True
- | x :: ls' ->
- for_allP (pred x) ls' /\ pairwise_relP pred ls'
-*)
-
val pairwise_rel : #a:Type -> pred:(a -> a -> Tot bool) -> ls:list a -> Tot bool
let rec pairwise_rel #a pred ls =
match ls with
@@ -421,8 +358,6 @@ let rec pairwise_rel #a pred ls =
| x :: ls' ->
for_all (pred x) ls' && pairwise_rel pred ls'
-/// The lack of lemmas about list manipulation is really annoying...
-
#push-options "--fuel 1"
let rec flatten_append (#a : Type) (l1 l2: list (list a)) :
Lemma (flatten (l1 @ l2) == flatten l1 @ flatten l2) =
@@ -439,8 +374,45 @@ let rec flatten_append (#a : Type) (l1 l2: list (list a)) :
let fst_is_disctinct (#a : eqtype) (#b : Type0) (p0 : a & b) (p1 : a & b) : Type0 =
fst p0 <> fst p1
+(*** Lemmas about Primitives *)
+/// TODO: move those lemmas
+
+// TODO: rename to 'insert'?
+val list_update_index_dif_lem
+ (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a)
+ (j : nat{j < length ls}) :
+ Lemma (requires (j <> i))
+ (ensures (index (list_update ls i x) j == index ls j))
+ [SMTPat (index (list_update ls i x) j)]
+
+#push-options "--fuel 1"
+let rec list_update_index_dif_lem #a ls i x j =
+ match ls with
+ | x' :: ls ->
+ if i = 0 then ()
+ else if j = 0 then ()
+ else
+ list_update_index_dif_lem ls (i-1) x (j-1)
+#pop-options
+
+val map_list_update_lem
+ (#a #b: Type0) (f : a -> Tot b)
+ (ls : list a) (i : nat{i < length ls}) (x : a) :
+ Lemma (list_update (map f ls) i (f x) == map f (list_update ls i x))
+ [SMTPat (list_update (map f ls) i (f x))]
+
+#push-options "--fuel 1"
+let rec map_list_update_lem #a #b f ls i x =
+ match ls with
+ | x' :: ls' ->
+ if i = 0 then ()
+ else map_list_update_lem f ls' (i-1) x
+#pop-options
+
(*** Invariants, models *)
+let is_pos_usize (n : nat) : Type0 = 0 < n /\ n <= usize_max
+
/// The "key" type
type key : eqtype = usize
@@ -463,11 +435,9 @@ let list_t_len (#t : Type0) (ls : list_t t) : nat = length (list_t_v ls)
let list_t_index (#t : Type0) (ls : list_t t) (i : nat{i < list_t_len ls}) : binding t =
index (list_t_v ls) i
-// TODO: use more
type slot_s (t : Type0) = list (binding t)
type slots_s (t : Type0) = list (slot_s t)
-// TODO: use more
type slot_t (t : Type0) = list_t t
let slot_t_v #t = list_t_v #t
@@ -475,35 +445,31 @@ let slot_t_v #t = list_t_v #t
let slots_t_v (#t : Type0) (slots : slots_t t) : slots_s t =
map slot_t_v slots
-/// TODO: remove?
let slots_t_al_v (#t : Type0) (slots : slots_t t) : assoc_list t =
flatten (map list_t_v slots)
/// High-level type for the hash-map, seen as a list of associative lists (one
-/// list per slot)
+/// list per slot). This is the representation we use most, internally. Note that
+/// we later introduce a [map_s] representation, which is the one used in the
+/// lemmas shown to the user.
type hash_map_slots_s t = list (slot_s t)
/// High-level type for the hash-map, seen as a an associative list
type hash_map_s t = assoc_list t
-// TODO: move
-let is_pos_usize (n : nat) : Type0 = 0 < n /\ n <= usize_max
-
// 'nes': "non-empty slots"
-// TODO: use more
type hash_map_slots_s_nes (t : Type0) : Type0 =
hm:hash_map_slots_s t{is_pos_usize (length hm)}
/// Representation function for [hash_map_t] as a list of slots
-let hash_map_t_slots_v (#t : Type0) (hm : hash_map_t t) : hash_map_slots_s t =
+let hash_map_t_v (#t : Type0) (hm : hash_map_t t) : hash_map_slots_s t =
map list_t_v hm.hash_map_slots
-/// Representation function for [hash_map_t]
-let hash_map_t_v (#t : Type0) (hm : hash_map_t t) : hash_map_s t =
- flatten (hash_map_t_slots_v hm)
+/// Representation function for [hash_map_t] as an associative list
+let hash_map_t_al_v (#t : Type0) (hm : hash_map_t t) : hash_map_s t =
+ flatten (hash_map_t_v hm)
// 'nes': "non-empty slots"
-// TODO: use more
type hash_map_t_nes (t : Type0) : Type0 =
hm:hash_map_t t{is_pos_usize (length hm.hash_map_slots)}
@@ -522,24 +488,16 @@ let same_hash_mod_key (#t : Type0) (len : usize{len > 0}) (h : nat) (b : binding
let binding_neq (#t : Type0) (b0 b1 : binding t) : bool = fst b0 <> fst b1
-let has_same_binding (#t : Type0) (al : assoc_list t) ((k,v) : binding t) : Type0 =
- match find (same_key k) al with
- | None -> False
- | Some (k',v') -> v' == v
-
-let hash_map_t_mem_s (#t : Type0) (hm : hash_map_t t) (k : key) : bool =
- existsb (same_key k) (hash_map_t_v hm)
-
let hash_map_t_len_s (#t : Type0) (hm : hash_map_t t) : nat =
hm.hash_map_num_entries
-let slot_find (#t : Type0) (k : key) (slot : list (binding t)) : option t =
+let slot_s_find (#t : Type0) (k : key) (slot : list (binding t)) : option t =
match find (same_key k) slot with
| None -> None
| Some (_, v) -> Some v
let assoc_list_find (#t : Type0) (k : key) (slot : assoc_list t) : option t =
- slot_find k slot
+ slot_s_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
@@ -553,7 +511,7 @@ let hash_map_slots_s_find
(k : key) : option t =
let i = hash_mod_key k (length hm) in
let slot = index hm i in
- slot_find k slot
+ slot_s_find k slot
let hash_map_slots_s_len
(#t : Type0) (hm : hash_map_slots_s_nes t) :
@@ -604,7 +562,7 @@ let hash_map_slots_s_inv (#t : Type0) (hm : hash_map_slots_s t) : Type0 =
/// Base invariant for the hashmap (the complete invariant can be temporarily
/// broken between the moment we inserted an element and the moment we resize)
let hash_map_t_base_inv (#t : Type0) (hm : hash_map_t t) : Type0 =
- let al = hash_map_t_v hm in
+ let al = hash_map_t_al_v hm in
// [num_entries] correctly tracks the number of entries in the table
// Note that it gives us that the length of the slots array is <= usize_max:
// [> length <= usize_max
@@ -1028,7 +986,7 @@ val slot_t_v_for_all_binding_neq_append_lem
(requires (
fst b <> key /\
for_all (binding_neq b) ls /\
- slot_find key ls == None))
+ slot_s_find key ls == None))
(ensures (
for_all (binding_neq b) (ls @ [(key,value)])))
@@ -1045,12 +1003,12 @@ val slot_s_inv_not_find_append_end_inv_lem
Lemma
(requires (
slot_s_inv len (hash_mod_key key len) ls /\
- slot_find key ls == None))
+ slot_s_find key ls == None))
(ensures (
let ls' = ls @ [(key,value)] in
slot_s_inv len (hash_mod_key key len) ls' /\
- (slot_find key ls' == Some value) /\
- (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls)))
+ (slot_s_find key ls' == Some value) /\
+ (forall k'. k' <> key ==> slot_s_find k' ls' == slot_s_find k' ls)))
#push-options "--fuel 1"
let rec slot_s_inv_not_find_append_end_inv_lem t len key value ls =
@@ -1072,16 +1030,16 @@ val hash_map_insert_in_list_s_lem_append
Lemma
(requires (
slot_s_inv len (hash_mod_key key len) ls /\
- slot_find key ls == None))
+ slot_s_find key ls == None))
(ensures (
let ls' = hash_map_insert_in_list_s key value ls in
ls' == ls @ [(key,value)] /\
// The invariant is preserved
slot_s_inv len (hash_mod_key key len) ls' /\
// [key] maps to [value]
- slot_find key ls' == Some value /\
+ slot_s_find key ls' == Some value /\
// The other bindings are preserved
- (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls)))
+ (forall k'. k' <> key ==> slot_s_find k' ls' == slot_s_find k' ls)))
let hash_map_insert_in_list_s_lem_append t len key value ls =
slot_s_inv_not_find_append_end_inv_lem t len key value ls
@@ -1113,7 +1071,7 @@ let hash_map_insert_in_list_back_lem_append t len key value ls =
(** Auxiliary lemmas: update case *)
-val slot_find_update_for_all_binding_neq_append_lem
+val slot_s_find_update_for_all_binding_neq_append_lem
(t : Type0) (key : usize) (value : t) (ls : list (binding t)) (b : binding t) :
Lemma
(requires (
@@ -1124,11 +1082,11 @@ val slot_find_update_for_all_binding_neq_append_lem
for_all (binding_neq b) ls'))
#push-options "--fuel 1"
-let rec slot_find_update_for_all_binding_neq_append_lem t key value ls b =
+let rec slot_s_find_update_for_all_binding_neq_append_lem t key value ls b =
match ls with
| [] -> ()
| (ck, cv) :: cls ->
- slot_find_update_for_all_binding_neq_append_lem t key value cls b
+ slot_s_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
@@ -1150,12 +1108,12 @@ val slot_s_inv_find_append_end_inv_lem
Lemma
(requires (
slot_s_inv len (hash_mod_key key len) ls /\
- Some? (slot_find key ls)))
+ Some? (slot_s_find key ls)))
(ensures (
let ls' = find_update (same_key key) ls (key, value) in
slot_s_inv len (hash_mod_key key len) ls' /\
- (slot_find key ls' == Some value) /\
- (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls)))
+ (slot_s_find key ls' == Some value) /\
+ (forall k'. k' <> key ==> slot_s_find k' ls' == slot_s_find k' ls)))
#push-options "--z3rlimit 50 --fuel 1"
let rec slot_s_inv_find_append_end_inv_lem t len key value ls =
@@ -1180,7 +1138,7 @@ let rec slot_s_inv_find_append_end_inv_lem t len key value ls =
begin
slot_s_inv_find_append_end_inv_lem t len key value cls;
assert(for_all (same_hash_mod_key len h) ls');
- slot_find_update_for_all_binding_neq_append_lem t key value cls (ck, cv);
+ slot_s_find_update_for_all_binding_neq_append_lem t key value cls (ck, cv);
assert(pairwise_rel binding_neq ls');
assert(slot_s_inv len h ls')
end
@@ -1192,16 +1150,16 @@ val hash_map_insert_in_list_s_lem_update
Lemma
(requires (
slot_s_inv len (hash_mod_key key len) ls /\
- Some? (slot_find key ls)))
+ Some? (slot_s_find key ls)))
(ensures (
let ls' = hash_map_insert_in_list_s key value ls in
ls' == find_update (same_key key) ls (key,value) /\
// The invariant is preserved
slot_s_inv len (hash_mod_key key len) ls' /\
// [key] maps to [value]
- slot_find key ls' == Some value /\
+ slot_s_find key ls' == Some value /\
// The other bindings are preserved
- (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls)))
+ (forall k'. k' <> key ==> slot_s_find k' ls' == slot_s_find k' ls)))
let hash_map_insert_in_list_s_lem_update t len key value ls =
slot_s_inv_find_append_end_inv_lem t len key value ls
@@ -1245,16 +1203,16 @@ val hash_map_insert_in_list_s_lem
// The invariant is preserved
slot_s_inv len (hash_mod_key key len) ls' /\
// [key] maps to [value]
- slot_find key ls' == Some value /\
+ slot_s_find key ls' == Some value /\
// The other bindings are preserved
- (forall k'. k' <> key ==> slot_find k' ls' == slot_find k' ls) /\
+ (forall k'. k' <> key ==> slot_s_find k' ls' == slot_s_find k' ls) /\
// The length is incremented, iff we inserted a new key
- (match slot_find key ls with
+ (match slot_s_find key ls with
| None -> length ls' = length ls + 1
| Some _ -> length ls' = length ls)))
let hash_map_insert_in_list_s_lem t len key value ls =
- match slot_find key ls with
+ match slot_s_find key ls with
| None ->
assert_norm(length [(key,value)] = 1);
hash_map_insert_in_list_s_lem_append t len key value ls
@@ -1328,17 +1286,17 @@ val hash_map_insert_no_resize_fwd_back_lem_s
Lemma
(requires (
hash_map_t_base_inv self /\
- hash_map_slots_s_len (hash_map_t_slots_v self) = hash_map_t_len_s self))
+ hash_map_slots_s_len (hash_map_t_v self) = hash_map_t_len_s self))
(ensures (
begin
match hash_map_insert_no_resize_fwd_back t self key value,
- hash_map_insert_no_resize_s (hash_map_t_slots_v self) key value
+ hash_map_insert_no_resize_s (hash_map_t_v self) key value
with
| Fail, Fail -> True
| Return hm, Return hm_v ->
hash_map_t_base_inv hm /\
hash_map_same_params hm self /\
- hash_map_t_slots_v hm == hm_v /\
+ hash_map_t_v hm == hm_v /\
hash_map_slots_s_len hm_v == hash_map_t_len_s hm
| _ -> False
end))
@@ -1360,13 +1318,13 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
| Fail -> ()
| Return l ->
begin
- // Checking that: list_t_v (index ...) == index (hash_map_t_slots_v ...) ...
- assert(list_t_v l == index (hash_map_t_slots_v self) hash_mod);
+ // Checking that: list_t_v (index ...) == index (hash_map_t_v ...) ...
+ assert(list_t_v l == index (hash_map_t_v self) hash_mod);
hash_map_insert_in_list_fwd_lem t key value l;
match hash_map_insert_in_list_fwd t key value l with
| Fail -> ()
| Return b ->
- assert(b = None? (slot_find key (list_t_v l)));
+ assert(b = None? (slot_s_find key (list_t_v l)));
hash_map_insert_in_list_back_lem t len key value l;
if b
then
@@ -1380,9 +1338,9 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
begin match vec_index_mut_back (list_t t) v hash_mod l0 with
| Fail -> ()
| Return v0 ->
- let self_v = hash_map_t_slots_v self in
+ let self_v = hash_map_t_v self in
let hm = Mkhash_map_t i3 p i1 v0 in
- let hm_v = hash_map_t_slots_v hm in
+ let hm_v = hash_map_t_v hm in
assert(hm_v == list_update self_v hash_mod (list_t_v l0));
assert_norm(length [(key,value)] = 1);
assert(length (list_t_v l0) = length (list_t_v l) + 1);
@@ -1399,9 +1357,9 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
begin match vec_index_mut_back (list_t t) v hash_mod l0 with
| Fail -> ()
| Return v0 ->
- let self_v = hash_map_t_slots_v self in
+ let self_v = hash_map_t_v self in
let hm = Mkhash_map_t i0 p i1 v0 in
- let hm_v = hash_map_t_slots_v hm in
+ let hm_v = hash_map_t_v hm in
assert(hm_v == list_update self_v hash_mod (list_t_v l0));
assert(length (list_t_v l0) = length (list_t_v l));
length_flatten_update self_v hash_mod (list_t_v l0);
@@ -1561,12 +1519,12 @@ val hash_map_move_elements_from_list_fwd_back_lem
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)
+ hash_map_move_elements_from_list_s (hash_map_t_v ntable) (slot_t_v ls)
with
| Fail, Fail -> True
| Return hm', Return hm_v ->
hash_map_t_base_inv hm' /\
- hash_map_t_slots_v hm' == hm_v /\
+ hash_map_t_v hm' == hm_v /\
hash_map_same_params hm' ntable
| _ -> False))
(decreases (hash_map_move_elements_from_list_decreases t ntable ls))
@@ -1582,8 +1540,8 @@ let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls =
begin match hash_map_insert_no_resize_fwd_back t ntable k v with
| Fail -> ()
| Return h ->
- let h_v = Return?.v (hash_map_insert_no_resize_s (hash_map_t_slots_v ntable) k v) in
- assert(hash_map_t_slots_v h == h_v);
+ let h_v = Return?.v (hash_map_insert_no_resize_s (hash_map_t_v ntable) k v) in
+ assert(hash_map_t_v h == h_v);
hash_map_move_elements_from_list_fwd_back_lem t h tl;
begin match hash_map_move_elements_from_list_fwd_back t h tl with
| Fail -> ()
@@ -1675,12 +1633,12 @@ val hash_map_move_elements_fwd_back_lem_refin
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
+ hash_map_move_elements_s (hash_map_t_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_base_inv ntable' /\
- hash_map_t_slots_v ntable' == ntable'_v /\
+ hash_map_t_v ntable' == ntable'_v /\
hash_map_same_params ntable' ntable
| _ -> False))
(decreases (length slots - i))
@@ -2089,7 +2047,7 @@ let slots_t_inv_implies_slots_s_inv #t slots =
val hash_map_t_base_inv_implies_hash_map_slots_s_inv
(#t : Type0) (hm : hash_map_t t) :
Lemma (requires (hash_map_t_base_inv hm))
- (ensures (hash_map_slots_s_inv (hash_map_t_slots_v hm)))
+ (ensures (hash_map_slots_s_inv (hash_map_t_v hm)))
let hash_map_t_base_inv_implies_hash_map_slots_s_inv #t hm = () // same as previous
@@ -2196,10 +2154,10 @@ let hash_map_slots_s_inv_implies_assoc_list_lem #t hm =
val hash_map_t_base_inv_implies_assoc_list_lem
(#t : Type0) (hm : hash_map_t t):
Lemma (requires (hash_map_t_base_inv hm))
- (ensures (assoc_list_inv (hash_map_t_v hm)))
+ (ensures (assoc_list_inv (hash_map_t_al_v 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)
+ hash_map_slots_s_inv_implies_assoc_list_lem (hash_map_t_v hm)
/// For some reason, we can't write the below [forall] directly in the [ensures]
/// clause of the next lemma: it makes Z3 fails even with a huge rlimit.
@@ -2215,7 +2173,7 @@ let partial_hash_map_slots_s_find
(k : key{hash_mod_key k len >= offset}) : option t =
let i = hash_mod_key k len in
let slot = index hm (i - offset) in
- slot_find k slot
+ slot_s_find k slot
val not_same_hash_key_not_found_in_slot
(#t : Type0) (len : usize{len > 0})
@@ -2226,7 +2184,7 @@ val not_same_hash_key_not_found_in_slot
(requires (
hash_mod_key k len <> i /\
slot_s_inv len i slot))
- (ensures (slot_find k slot == None))
+ (ensures (slot_s_find k slot == None))
#push-options "--fuel 1"
let rec not_same_hash_key_not_found_in_slot #t len k i slot =
@@ -2287,7 +2245,7 @@ let rec partial_hash_map_slots_s_is_assoc_list_lem #t len offset hm k =
if i = 0 then
begin
// We must look in the current slot
- assert(partial_hash_map_slots_s_find len offset hm k == slot_find k slot);
+ assert(partial_hash_map_slots_s_find len offset hm k == slot_s_find k slot);
find_append (same_key k) slot (flatten hm');
assert(forall (i:nat{i < length hm'}). index hm' i == index hm (i+1)); // Triggers instantiations
key_in_previous_slot_implies_not_found #t len k (offset+1) hm';
@@ -2318,13 +2276,13 @@ let rec partial_hash_map_slots_s_is_assoc_list_lem #t len offset hm k =
val hash_map_is_assoc_list_lem (#t : Type0) (hm : hash_map_t t) :
Lemma (requires (hash_map_t_base_inv hm))
- (ensures (hash_map_is_assoc_list hm (hash_map_t_v hm)))
+ (ensures (hash_map_is_assoc_list hm (hash_map_t_al_v hm)))
let hash_map_is_assoc_list_lem #t hm =
let aux (k:key) :
- Lemma (hash_map_t_find_s hm k == assoc_list_find k (hash_map_t_v hm))
+ Lemma (hash_map_t_find_s hm k == assoc_list_find k (hash_map_t_al_v hm))
[SMTPat (hash_map_t_find_s hm k)] =
- let hm_v = hash_map_t_slots_v hm in
+ let hm_v = hash_map_t_v hm in
let len = length hm_v in
partial_hash_map_slots_s_is_assoc_list_lem #t len 0 hm_v k
in
@@ -2346,7 +2304,7 @@ val hash_map_move_elements_fwd_back_lem
(ensures (
let al = flatten (slots_t_v slots) in
match hash_map_move_elements_fwd_back t ntable slots 0,
- hash_map_move_elements_s_flat (hash_map_t_slots_v ntable) al
+ hash_map_move_elements_s_flat (hash_map_t_v ntable) al
with
| Return (ntable', _), Return ntable'_v ->
// The invariant is preserved
@@ -2360,7 +2318,7 @@ val hash_map_move_elements_fwd_back_lem
// The table can be linked to its model (we need this only to reveal
// "pretty" functional lemmas to the user in the fsti - so that we
// can write lemmas with SMT patterns - this is very F* specific)
- hash_map_t_slots_v ntable' == ntable'_v /\
+ hash_map_t_v ntable' == ntable'_v /\
// The new table contains exactly all the bindings from the slots
// Rk.: see the comment for [hash_map_is_assoc_list]
hash_map_is_assoc_list ntable' al
@@ -2376,7 +2334,7 @@ val hash_map_move_elements_fwd_back_lem
#restart-solver
#push-options "--z3rlimit 100"
let hash_map_move_elements_fwd_back_lem t ntable slots =
- let ntable_v = hash_map_t_slots_v ntable in
+ let ntable_v = hash_map_t_v ntable in
let slots_v = slots_t_v slots in
let al = flatten slots_v in
hash_map_move_elements_fwd_back_lem_refin t ntable slots 0;
@@ -2387,7 +2345,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
| 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_t_v ntable' == ntable'_v)
| _ -> assert(False)
end;
hash_map_move_elements_s_lem_refin_flat ntable_v slots_v 0;
@@ -2408,7 +2366,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
assert(hash_map_t_base_inv ntable');
assert(length ntable'.hash_map_slots = length ntable.hash_map_slots);
assert(hash_map_t_len_s ntable' = length al);
- assert(hash_map_t_slots_v ntable' == ntable'_v);
+ assert(hash_map_t_v ntable' == ntable'_v);
assert(hash_map_is_assoc_list ntable' al)
| _ -> assert(False)
#pop-options
@@ -2522,8 +2480,9 @@ let times_divid_lem (n m p : pos) : Lemma ((n * m) / p >= n * (m / p))
#pop-options
/// The good old arithmetic proofs and their unstability...
+/// It seems OK now that I moved an assertion (I ran `quake 100`).
#restart-solver
-#push-options "--z3rlimit 100 --z3cliopt smt.arith.nl=false"
+#push-options "--z3rlimit 200 --z3cliopt smt.arith.nl=false"
let new_max_load_lem
(len : usize) (capacity : usize{capacity > 0})
(divid : usize{divid > 0}) (divis : usize{divis > 0}) :
@@ -2543,11 +2502,11 @@ let new_max_load_lem
let max_load = (capacity * divid) / divis in
let ncapacity = 2 * capacity in
let nmax_load = (ncapacity * divid) / divis in
+ FStar.Math.Lemmas.paren_mul_left 2 capacity divid;
+ assert(2 * (capacity * divid) == 2 * capacity * divid); // Often broke (though given by lemma above): we moved it up
assert(nmax_load = (2 * capacity * divid) / divis);
times_divid_lem 2 (capacity * divid) divis;
assert((2 * (capacity * divid)) / divis >= 2 * ((capacity * divid) / divis));
- FStar.Math.Lemmas.paren_mul_left 2 capacity divid;
- assert(2 * (capacity * divid) == (2 * capacity * divid));
assert(nmax_load >= 2 * ((capacity * divid) / divis));
assert(nmax_load >= 2 * max_load);
assert(nmax_load >= max_load + max_load);
@@ -2600,9 +2559,9 @@ let hash_map_try_resize_s_simpl_lem #t hm =
// Proving that: length al = hm.hash_map_num_entries
assert(al == flatten (map slot_t_v slots));
assert(al == flatten (map list_t_v slots));
- assert(hash_map_t_v hm == flatten (hash_map_t_slots_v hm));
- assert(hash_map_t_v hm == flatten (map list_t_v hm.hash_map_slots));
- assert(al == hash_map_t_v hm);
+ assert(hash_map_t_al_v hm == flatten (hash_map_t_v hm));
+ assert(hash_map_t_al_v hm == flatten (map list_t_v hm.hash_map_slots));
+ assert(al == hash_map_t_al_v hm);
assert(hash_map_t_base_inv ntable);
assert(length al = hm.hash_map_num_entries);
assert(length al <= usize_max);
@@ -2615,7 +2574,7 @@ let hash_map_try_resize_s_simpl_lem #t hm =
| Fail -> ()
| Return (ntable', _) ->
hash_map_is_assoc_list_lem hm;
- assert(hash_map_is_assoc_list hm (hash_map_t_v hm));
+ assert(hash_map_is_assoc_list hm (hash_map_t_al_v hm));
let hm' =
{ hm with hash_map_slots = ntable'.hash_map_slots;
hash_map_max_load = ntable'.hash_map_max_load }
@@ -2710,7 +2669,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_slots_s_updated_binding (hash_map_t_slots_v self) key (Some value) (hash_map_t_slots_v hm') /\
+ hash_map_slots_s_updated_binding (hash_map_t_v self) key (Some value) (hash_map_t_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
@@ -2721,28 +2680,28 @@ let hash_map_insert_fwd_back_bindings_lem
(hm' hm'' : hash_map_t_nes t) :
Lemma
(requires (
- hash_map_slots_s_updated_binding (hash_map_t_slots_v self) key
- (Some value) (hash_map_t_slots_v hm') /\
+ hash_map_slots_s_updated_binding (hash_map_t_v self) key
+ (Some value) (hash_map_t_v hm') /\
hash_map_t_same_bindings hm' hm''))
(ensures (
- hash_map_slots_s_updated_binding (hash_map_t_slots_v self) key
- (Some value) (hash_map_t_slots_v hm'')))
+ hash_map_slots_s_updated_binding (hash_map_t_v self) key
+ (Some value) (hash_map_t_v hm'')))
= ()
#restart-solver
#push-options "--z3rlimit 500"
let hash_map_insert_fwd_back_lem t self key value =
hash_map_insert_no_resize_fwd_back_lem_s t self key value;
- hash_map_insert_no_resize_s_lem (hash_map_t_slots_v self) key value;
+ hash_map_insert_no_resize_s_lem (hash_map_t_v self) key value;
match hash_map_insert_no_resize_fwd_back t self key value with
| Fail -> ()
| Return hm' ->
// Expanding the post of [hash_map_insert_no_resize_fwd_back_lem_s]
- let self_v = hash_map_t_slots_v self in
+ let self_v = hash_map_t_v self in
let hm'_v = Return?.v (hash_map_insert_no_resize_s self_v key value) in
assert(hash_map_t_base_inv hm');
assert(hash_map_same_params hm' self);
- assert(hash_map_t_slots_v hm' == hm'_v);
+ assert(hash_map_t_v hm' == hm'_v);
assert(hash_map_slots_s_len hm'_v == hash_map_t_len_s hm');
// Expanding the post of [hash_map_insert_no_resize_s_lem]
assert(insert_post self_v key value hm'_v);
@@ -2758,7 +2717,7 @@ let hash_map_insert_fwd_back_lem t self key value =
// Expanding the post of [hash_map_try_resize_fwd_back_lem]
let hm'' = Return?.v (hash_map_try_resize_fwd_back t hm') in
assert(hash_map_t_inv hm'');
- let hm''_v = hash_map_t_slots_v hm'' in
+ let hm''_v = hash_map_t_v hm'' in
assert(forall k. hash_map_t_find_s hm'' k == hash_map_t_find_s hm' k);
assert(hash_map_t_len_s hm'' = hash_map_t_len_s hm'); // TODO
// Proving the post
@@ -3010,7 +2969,7 @@ val hash_map_get_mut_back_lem_refin
match hash_map_get_mut_back t self key ret with
| Fail -> False
| Return hm' ->
- hash_map_t_slots_v hm' == hash_map_insert_no_fail_s (hash_map_t_slots_v self) key ret))
+ hash_map_t_v hm' == hash_map_insert_no_fail_s (hash_map_t_v self) key ret))
let hash_map_get_mut_back_lem_refin #t self key ret =
begin match hash_key_fwd key with
@@ -3054,8 +3013,8 @@ val hash_map_get_mut_back_lem
| Fail -> False
| Return hm' ->
// Functional spec
- hash_map_t_slots_v hm' ==
- hash_map_insert_no_fail_s (hash_map_t_slots_v hm) key ret /\
+ hash_map_t_v hm' ==
+ hash_map_insert_no_fail_s (hash_map_t_v hm) key ret /\
// The invariant is preserved
hash_map_t_inv hm' /\
// The length is preserved
@@ -3066,7 +3025,7 @@ val hash_map_get_mut_back_lem
(forall k'. k' <> key ==> hash_map_t_find_s hm' k' == hash_map_t_find_s hm k')))
let hash_map_get_mut_back_lem #t hm key ret =
- let hm_v = hash_map_t_slots_v hm in
+ let hm_v = hash_map_t_v hm in
hash_map_get_mut_back_lem_refin hm key ret;
match hash_map_get_mut_back t hm key ret with
| Fail -> assert(False)
@@ -3145,7 +3104,7 @@ let hash_map_remove_fwd_lem t self key =
begin
assert(l == index v hash_mod);
assert(length (list_t_v #t l) > 0);
- length_flatten_index (hash_map_t_slots_v self) hash_mod;
+ length_flatten_index (hash_map_t_v self) hash_mod;
match usize_sub i0 1 with
| Fail -> ()
| Return _ -> ()
@@ -3178,7 +3137,7 @@ val hash_map_remove_from_list_back_lem_refin
// 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
+ match slot_s_find key (list_t_v ls) with
| None -> len = len'
| Some _ -> len = len' + 1)))
@@ -3228,7 +3187,7 @@ val hash_map_remove_back_lem_refin
| Fail -> False
| 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 /\
+ hash_map_t_v hm' == hash_map_remove_s (hash_map_t_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
@@ -3274,7 +3233,7 @@ let hash_map_remove_back_lem_refin #t self key =
begin
assert(l == index v hash_mod);
assert(length (list_t_v #t l) > 0);
- length_flatten_index (hash_map_t_slots_v self) hash_mod;
+ length_flatten_index (hash_map_t_v self) hash_mod;
match usize_sub i0 1 with
| Fail -> ()
| Return i3 ->
@@ -3306,8 +3265,8 @@ val hash_map_remove_from_list_s_lem
(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) /\
+ slot_s_find k slot' == None /\
+ (forall (k':key{k' <> k}). slot_s_find k' slot' == slot_s_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')
@@ -3364,7 +3323,7 @@ val hash_map_remove_back_lem
| Return hm' ->
hash_map_t_inv self /\
hash_map_same_params hm' self /\
- hash_map_t_slots_v hm' == hash_map_remove_s (hash_map_t_slots_v self) key /\
+ hash_map_t_v hm' == hash_map_remove_s (hash_map_t_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
@@ -3374,4 +3333,4 @@ val hash_map_remove_back_lem
let hash_map_remove_back_lem #t self key =
hash_map_remove_back_lem_refin self key;
- hash_map_remove_s_lem (hash_map_t_slots_v self) key
+ hash_map_remove_s_lem (hash_map_t_v self) key