summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst234
1 files changed, 46 insertions, 188 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 7436ec5f..e7236189 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -287,19 +287,23 @@ let list_t_index (#t : Type0) (ls : list_t t) (i : nat{i < list_t_len ls}) : bin
let slots_t_v (#t : Type0) (slots : slots_t t) : assoc_list t =
flatten (map list_t_v slots)
+// TODO: use more
+type slot_s (t : Type0) = list (binding t)
+type slots_s (t : Type0) = list (slot_s t)
+
/// High-level type for the hash-map, seen as a list of associative lists (one
/// list per slot)
-type hash_map_slots t = list (assoc_list t)
+type hash_map_slots t = list (slot_s t)
/// High-level type for the hash-map, seen as a an associative list
-type hash_map t = assoc_list t
+type hash_map_s t = assoc_list t
/// 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 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 t =
+let hash_map_t_v (#t : Type0) (hm : hash_map_t t) : hash_map_s t =
flatten (hash_map_t_slots_v hm)
let hash_key (k : key) : hash =
@@ -466,10 +470,6 @@ let slot_t_inv_from_funs_lem
()
*)
-// TODO: use more
-type slot_s (t : Type0) = list (binding t)
-type slots_s (t : Type0) = list (slot_s t)
-
let slots_inv (#t : Type0) (slots : slots_s t{length slots <= usize_max}) : Type0 =
forall(i:nat{i < length slots}).
{:pattern index slots i}
@@ -553,8 +553,7 @@ let hash_map_t_inv_repr (#t : Type0) (hm : hash_map_t t) (al : assoc_list t) : T
hash_map_t_is_al hm al
*)
-(*** Proofs *)
-(**** allocate_slots *)
+(*** allocate_slots *)
/// Auxiliary lemma
val slots_t_all_nil_inv_lem
@@ -624,7 +623,7 @@ let rec hash_map_allocate_slots_fwd_lem t slots n =
end
#pop-options
-(**** new_with_capacity *)
+(*** new_with_capacity *)
/// Under proper conditions, [new_with_capacity] doesn't fail and returns an empty hash map.
val hash_map_new_with_capacity_fwd_lem
(t : Type0) (capacity : usize)
@@ -671,7 +670,7 @@ let hash_map_new_with_capacity_fwd_lem (t : Type0) (capacity : usize)
end
#pop-options
-(**** new *)
+(*** new *)
/// [new] doesn't fail and returns an empty hash map
val hash_map_new_fwd_lem_fun (t : Type0) :
Lemma
@@ -695,7 +694,7 @@ let hash_map_new_fwd_lem_fun t =
slots_t_v_all_nil_is_empty_lem hm.hash_map_slots
#pop-options
-(**** clear_slots *)
+(*** clear_slots *)
/// [clear_slots] doesn't fail and simply clears the slots starting at index i
#push-options "--fuel 1"
let rec hash_map_clear_slots_fwd_back_lem
@@ -736,7 +735,7 @@ let rec hash_map_clear_slots_fwd_back_lem
else ()
#pop-options
-(**** clear *)
+(*** clear *)
/// [clear] doesn't fail and turns the hash map into an empty map
val hash_map_clear_fwd_back_lem_fun
(t : Type0) (self : hash_map_t t) :
@@ -771,7 +770,7 @@ let hash_map_clear_fwd_back_lem_fun t self =
end
#pop-options
-(**** len *)
+(*** len *)
/// [len]: we link it to a non-failing function.
/// Rk.: we might want to make an analysis to not use an error monad to translate
@@ -785,9 +784,9 @@ val hash_map_len_fwd_lem (t : Type0) (self : hash_map_t t) :
let hash_map_len_fwd_lem t self = ()
-(**** insert_in_list *)
+(*** insert_in_list *)
-(***** insert_in_list'fwd *)
+(**** insert_in_list'fwd *)
/// [insert_in_list_fwd]: returns true iff the key is not in the list (functional version)
val hash_map_insert_in_list_fwd_lem
@@ -820,7 +819,7 @@ let rec hash_map_insert_in_list_fwd_lem t key value ls =
end
#pop-options
-(***** insert_in_list'back *)
+(**** insert_in_list'back *)
/// The proofs about [insert_in_list] backward are easier to do in several steps:
/// extrinsic proofs to the rescue!
@@ -919,7 +918,7 @@ let hash_map_insert_in_list_back_lem_s t key value ls =
| None -> hash_map_insert_in_list_back_lem_append_s t key value ls
| Some _ -> hash_map_insert_in_list_back_lem_update_s t key value ls
-(***** Invariants of insert_in_list_s *)
+(**** Invariants of insert_in_list_s *)
/// Auxiliary lemmas
/// We work on [hash_map_insert_in_list_s], the "high-level" version of [insert_in_list'back].
@@ -1199,9 +1198,9 @@ let hash_map_insert_in_list_back_lem t len key value ls =
hash_map_insert_in_list_back_lem_s t key value ls;
hash_map_insert_in_list_s_lem t len key value (list_t_v ls)
-(**** insert_no_resize *)
+(*** insert_no_resize *)
-(***** Refinement proof *)
+(**** Refinement proof *)
/// Same strategy as for [insert_in_list]: we introduce a high-level version of
/// the function, and reason about it.
/// We work on [hash_map_slots] (we use a higher-level view of the hash-map, but
@@ -1314,7 +1313,7 @@ let hash_map_insert_no_resize_fwd_back_lem t self key value =
end
end
-(***** find after insert *)
+(**** find after insert *)
/// Lemmas about what happens if we call [find] after an insertion
val hash_map_insert_no_resize_s_get_same_lem
@@ -1367,173 +1366,32 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
end
end
-(*
-/// We also do a disjunction over the cases
-
-/// [insert_no_resize]: if the key is not in the map, we insert a new binding
-val hash_map_insert_no_resize_fwd_back_lem_insert
- (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
- Lemma
- (requires (
- hash_map_t_inv self /\
- // The key is not in the map
- None? (hash_map_t_find_s self key)))
- (ensures (
- match hash_map_insert_no_resize_fwd_back t self key value with
- | Fail -> False // Can't fail
- | Return hm ->
- // The invariant is preserved
- hash_map_t_inv hm /\
- // The number of elements is the same
- hash_map_t_len_s hm = hash_map_t_len_s self /\
- // The map has been updated with the new binding
- (hash_map_t_find_s self key == Some value) /\
- // The other bindings are left unchanged
- hash_map_t_v hm == find_update (same_key key) (hash_map_t_v self) (key,value)))
-
-/// The following function captures the "essence" of what [insert_no_resize] does
-let hash_map_t_insert_no_resize
- (#t : Type0) (hm : hash_map_t t) (key : usize) (value : t) :
- result hash_map_t t
- // Check if we need to add an element but reached saturation
- if None? (hash_map_t_find_s self key) && hash_map_t_len_s self = usize_max then Fail
- else
- // We didn't saturate: we can insert the element
- match hash_map_insert_no_resize_fwd_back_lem_insert with
- | Fail -> Fail // Shouldn't get there, but taken care of by proofs below
- |
-
- match hash_map_t_find_s self key with
- | None ->
- hash_map_t_len_s self = usize_max
-
- None? (hash_map_t_find_s self key) /\
- hash_map_t_len_s self = usize_max
-
-/// [insert_no_resize]: we prove a simple "functional" version of what happens,
-/// to simplify further reasoning.
-val hash_map_insert_no_resize_fwd_back_lem_fun
- (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
- Lemma
- (ensures (
- match hash_map_insert_no_resize_fwd_back t self key value with
- | Fail ->
- // It can fail only if the key is not in the map, and we reached saturation
- None? (hash_map_t_find_s self key) /\
- hash_map_t_len_s self = usize_max
- | Return hm ->
- // If we succeeded, we simply updated the proper slot
- let len =
- let i = hash_mod_key key
- let slots' =
- // The invariant is preserved
- hash_map_t_inv hm /\
- // The map has been updated
- hash_map_t_v hm == find_update (same_key key) (hash_map_t_v self) (key,value)))
+(*** remove_elements_from_list *)
-/// [insert_no_resize]: if the key is in the map, we succeed and update the binding.
-val hash_map_insert_no_resize_fwd_back_lem_update
- (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
- Lemma
- (requires (
- hash_map_t_inv self /\
- // The key is in the map
- Some? (find (same_key key) (hash_map_t_v self))))
- (ensures (
- match hash_map_insert_no_resize_fwd_back t self key value with
- | Fail -> False
+type hash_map_slots_res (t : Type0) = res:result (hash_map_slots t){
+ match res with
+ | Fail -> True
| Return hm ->
- // The invariant is preserved
- hash_map_t_inv hm /\
- // The map has been updated
- hash_map_t_v hm == find_update (same_key key) (hash_map_t_v self) (key,value)))
-
-
-(*
-(**** insert_no_resize *)
-
-/// Same as for [insert_in_list]: we do the proofs in several, modular steps.
-/// The strategy is to study the two disjoint cases:
-/// - the key is already in the map (we update the binding)
-/// - the key is not in the map (we add a binding)
-///
-/// We gradually prove that the resulting map, in the two cases, can be seen
-/// as the result of:
-/// - filtering the bindings for the key we want to insert
-/// - pushing the new binding at the front
-///
-/// We then prove a less "functional" variant of the result, which states that,
-/// after the insertion:
-/// - [key] maps to [value]
-/// - forall key' <> key, the binding is unchanged
-///
-/// This way, we have a consistent, high-level description of the insertion.
-///
-/// Rk.: with multimaps the high-level spec would be even simpler: we would push
-/// an element to the front of the list.
-
-/// [insert_no_resize]: if the key is in the map, we succeed and update the binding.
-val hash_map_insert_no_resize_fwd_back_lem_update
- (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
- Lemma
- (requires (
- hash_map_t_inv self /\
- // The key is in the map
- Some? (find (same_key key) (hash_map_t_v self))))
- (ensures (
- match hash_map_insert_no_resize_fwd_back t self key value with
- | Fail -> False
+ length hm <= usize_max /\
+ length hm > 0
+ }
+
+let hash_map_move_elements_from_list_s
+ (t : Type0) (hm : hash_map_slots t{length hm <= usize_max /\ length hm > 0})
+ (ls : slot t) :
+ Pure (result (hash_map_slots t))
+ (requires True)
+ (ensures (fun res ->
+ match res with
+ | Fail -> True
+ | Return hm' -> length hm' = length hm)) =
+ let add_elem (hm_res : result hash_map_slots t) (value,key) :
+ Pure (res=
+ match hm_res with
+ | Fail -> Fail
| Return hm ->
- // The invariant is preserved
- hash_map_t_inv hm /\
- // The map has been updated
- hash_map_t_v hm == find_update (same_key key) (hash_map_t_v self) (key,value)))
-
-let hash_map_insert_no_resize_fwd_back_lem_update t self key value =
- begin match hash_key_fwd key with
- | Fail -> ()
- | Return i ->
- let i0 = self.hash_map_num_entries in
- let p = self.hash_map_max_load_factor in
- let i1 = self.hash_map_max_load in
- let v = self.hash_map_slots in
- let i2 = vec_len (list_t t) v in
- begin match usize_rem i i2 with
- | Fail -> ()
- | Return hash_mod ->
- begin match vec_index_mut_fwd (list_t t) v hash_mod with
- | Fail -> ()
- | Return l ->
- // The key must be in the slot - TODO: update invariant
- assume(Some? (find (same_key key) (list_t_v l)));
- hash_map_insert_in_list_fwd_lem t key value l;
- begin match hash_map_insert_in_list_fwd t key value l with
- | Fail -> ()
- | Return b ->
- assert(not b);
- if b then assert(False)
- else
- begin
- hash_map_insert_in_list_back_lem_update t key value l;
- match hash_map_insert_in_list_back t key value l with
- | Fail -> ()
- | Return l0 ->
- begin
- match vec_index_mut_back (list_t t) v hash_mod l0 with
- | Fail -> ()
- | Return v0 ->
- let hm1 = Mkhash_map_t i0 p i1 v0 in
- assume(hash_map_t_inv hm1);
- assume(hash_map_t_v hm1 == find_update (same_key key) (hash_map_t_v self) (key,value))
- end
- end
- end
- end
- end
- end
-
-
-/// [insert_in_list]: inserting a binding is equivalent to:
-/// - filtering the list
-/// - pushing the binding to the front
-
+ hash_map_insert_no_resize_s hm
+ fold_left (fun hm_res (value,key) ->
+ match ls with
+ | [] -> Return hm
+ |