diff options
Diffstat (limited to 'tests/fstar-split/hashmap/Hashmap.Properties.fsti')
| -rw-r--r-- | tests/fstar-split/hashmap/Hashmap.Properties.fsti | 267 |
1 files changed, 0 insertions, 267 deletions
diff --git a/tests/fstar-split/hashmap/Hashmap.Properties.fsti b/tests/fstar-split/hashmap/Hashmap.Properties.fsti deleted file mode 100644 index 26c0ec06..00000000 --- a/tests/fstar-split/hashmap/Hashmap.Properties.fsti +++ /dev/null @@ -1,267 +0,0 @@ -(** Properties about the hashmap *) -module Hashmap.Properties -open Primitives -open FStar.List.Tot -open FStar.Mul -open Hashmap.Types -open Hashmap.Clauses -open Hashmap.Funs - -#set-options "--z3rlimit 50 --fuel 0 --ifuel 1" - -// Small trick to align the .fst and the .fsti -val _align_fsti : unit - -(*** Utilities *) - -type key : eqtype = usize - -type hash : eqtype = usize - -val hashMap_t_inv (#t : Type0) (hm : hashMap_t t) : Type0 - -val len_s (#t : Type0) (hm : hashMap_t t) : nat - -val find_s (#t : Type0) (hm : hashMap_t t) (k : key) : option t - -(*** Overloading *) - -/// Upon inserting *new* entries in the hash map, the slots vector is resized -/// whenever we reach the max load, unless we can't resize anymore because -/// there are already too many entries. This way, we maintain performance by -/// limiting the hash collisions. -/// This is expressed by the following property, which is maintained in the hash -/// map invariant. -val hashMap_not_overloaded_lem (#t : Type0) (hm : hashMap_t t) : - Lemma - (requires (hashMap_t_inv hm)) - (ensures ( - // The capacity is the number of slots - let capacity = length hm.slots in - // The max load factor defines a threshold on the number of entries: - // if there are more entries than a given fraction of the number of slots, - // we resize the slots vector to limit the hash collisions - let (dividend, divisor) = hm.max_load_factor in - // technicality: this postcondition won't typecheck if we don't reveal - // that divisor > 0 (because of the division) - divisor > 0 /\ - begin - // The max load, computed as a fraction of the capacity - let max_load = (capacity * dividend) / divisor in - // The number of entries inserted in the map is given by [len_s] (see - // the functional correctness lemmas, which state how this number evolves): - let len = len_s hm in - // We prove that: - // - either the number of entries is <= than the max load threshold - len <= max_load - // - or we couldn't resize the map, because then the arithmetic computations - // would overflow (note that we always multiply the number of slots by 2) - || 2* capacity * dividend > usize_max - end)) - -(*** Functional correctness *) -(**** [new'fwd] *) - -/// [new] doesn't fail and returns an empty hash map -val hashMap_new_lem (t : Type0) : - Lemma - (ensures ( - match hashMap_new t with - | Fail _ -> False - | Return hm -> - // The hash map invariant is satisfied - hashMap_t_inv hm /\ - // The hash map has a length of 0 - len_s hm = 0 /\ - // It contains no bindings - (forall k. find_s hm k == None))) - -(**** [clear] *) - -/// [clear] doesn't fail and turns the hash map into an empty map -val hashMap_clear_lem - (#t : Type0) (self : hashMap_t t) : - Lemma - (requires (hashMap_t_inv self)) - (ensures ( - match hashMap_clear t self with - | Fail _ -> False - | Return hm -> - // The hash map invariant is satisfied - hashMap_t_inv hm /\ - // The hash map has a length of 0 - len_s hm = 0 /\ - // It contains no bindings - (forall k. find_s hm k == None))) - -(**** [len] *) - -/// [len] can't fail and returns the length (the number of elements) of the hash map -val hashMap_len_lem (#t : Type0) (self : hashMap_t t) : - Lemma - (requires (hashMap_t_inv self)) - (ensures ( - match hashMap_len t self with - | Fail _ -> False - | Return l -> l = len_s self)) - - -(**** [insert'fwd_back] *) - -/// The backward function for [insert] (note it is named "...insert'fwd_back" because -/// the forward function doesn't return anything, and was thus filtered - in a -/// sense the effect of applying the forward function then the backward function is -/// entirely encompassed by the effect of the backward function alone). -/// -/// [insert'fwd_back] simply inserts a binding. -val hashMap_insert_lem - (#t : Type0) (self : hashMap_t t) (key : usize) (value : t) : - Lemma - (requires (hashMap_t_inv self)) - (ensures ( - match hashMap_insert t self key value with - | Fail _ -> - // We can fail only if: - // - the key is not in the map and we thus need to add it - None? (find_s self key) /\ - // - and we are already saturated (we can't increment the internal counter) - len_s self = usize_max - | Return hm' -> - // The invariant is preserved - hashMap_t_inv hm' /\ - // [key] maps to [value] - find_s hm' key == Some value /\ - // The other bindings are preserved - (forall k'. k' <> key ==> find_s hm' k' == find_s self k') /\ - begin - // The length is incremented, iff we inserted a new key - match find_s self key with - | None -> len_s hm' = len_s self + 1 - | Some _ -> len_s hm' = len_s self - end)) - - -(**** [contains_key] *) - -/// [contains_key'fwd] can't fail and returns `true` if and only if there is -/// a binding for key [key] -val hashMap_contains_key_lem - (#t : Type0) (self : hashMap_t t) (key : usize) : - Lemma - (requires (hashMap_t_inv self)) - (ensures ( - match hashMap_contains_key t self key with - | Fail _ -> False - | Return b -> b = Some? (find_s self key))) - -(**** [get'fwd] *) - -/// [get] returns (a shared borrow to) the binding for key [key] -val hashMap_get_lem - (#t : Type0) (self : hashMap_t t) (key : usize) : - Lemma - (requires (hashMap_t_inv self)) - (ensures ( - match hashMap_get t self key, find_s self key with - | Fail _, None -> True - | Return x, Some x' -> x == x' - | _ -> False)) - -(**** [get_mut'fwd] *) - -/// [get_mut'fwd] returns (a mutable borrow to) the binding for key [key]. -/// -/// The *forward* function models the action of getting a borrow to an element -/// in Rust, which gives the possibility of modifying this element in place. Then, -/// upon ending the borrow, the effect of the modification is modelled in the -/// translation through a call to the backward function. -val hashMap_get_mut_lem - (#t : Type0) (self : hashMap_t t) (key : usize) : - Lemma - (requires (hashMap_t_inv self)) - (ensures ( - match hashMap_get_mut t self key, find_s self key with - | Fail _, None -> True - | Return x, Some x' -> x == x' - | _ -> False)) - - -(**** [get_mut'back] *) - -/// [get_mut'back] updates the binding for key [key], without failing. -/// A call to [get_mut'back] must follow a call to [get_mut'fwd], which gives -/// us that there must be a binding for key [key] in the map (otherwise we -/// can't prove the absence of failure). -val hashMap_get_mut_back_lem - (#t : Type0) (hm : hashMap_t t) (key : usize) (ret : t) : - Lemma - (requires ( - hashMap_t_inv hm /\ - // A call to the backward function must follow a call to the forward - // function, whose success gives us that there is a binding for the key. - // In the case of *forward* functions, "success" has to be understood as - // the absence of panics. When translating code from Rust to pure lambda - // calculus, we have the property that the generated calls to the backward - // functions can't fail (because their are preceded by calls to forward - // functions, which must then have succeeded before): for a backward function, - // "failure" is to be understood as the semantics getting stuck. - // This is of course true unless we filtered the call to the forward function - // because its effect is encompassed by the backward function, as with - // [hashMap_clear]). - Some? (find_s hm key))) - (ensures ( - match hashMap_get_mut_back t hm key ret with - | Fail _ -> False // Can't fail - | Return hm' -> - // The invariant is preserved - hashMap_t_inv hm' /\ - // The length is preserved - len_s hm' = len_s hm /\ - // [key] maps to the update value, [ret] - find_s hm' key == Some ret /\ - // The other bindings are preserved - (forall k'. k' <> key ==> find_s hm' k' == find_s hm k'))) - -(**** [remove'fwd] *) - -/// [remove'fwd] returns the (optional) element which has been removed from the map -/// (the rust function *moves* it out of the map). Note that the effect of the update -/// on the map is modelles through the call to [remove'back] ([remove] takes a -/// mutable borrow to the hash map as parameter). -val hashMap_remove_lem - (#t : Type0) (self : hashMap_t t) (key : usize) : - Lemma - (requires (hashMap_t_inv self)) - (ensures ( - match hashMap_remove t self key with - | Fail _ -> False - | Return opt_x -> opt_x == find_s self key)) - - -(**** [remove'back] *) - -/// The hash map given as parameter to [remove] is given through a mutable borrow: -/// hence the backward function which gives back the updated map, without the -/// binding. -val hashMap_remove_back_lem - (#t : Type0) (self : hashMap_t t) (key : usize) : - Lemma - (requires (hashMap_t_inv self)) - (ensures ( - match hashMap_remove_back t self key with - | Fail _ -> False - | Return hm' -> - // The invariant is preserved - hashMap_t_inv self /\ - // The binding for [key] is not there anymore - find_s hm' key == None /\ - // The other bindings are preserved - (forall k'. k' <> key ==> find_s hm' k' == find_s self k') /\ - begin - // The length is decremented iff the key was in the map - let len = len_s self in - let len' = len_s hm' in - match find_s self key with - | None -> len = len' - | Some _ -> len = len' + 1 - end)) |