summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/hashmap/Hashmap.Properties.fst129
1 files changed, 105 insertions, 24 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index aee5dbb7..69a9bc40 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -291,6 +291,10 @@ let slots_t_v (#t : Type0) (slots : slots_t t) : assoc_list t =
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 : Type0) (slot : slot_t t) : slot_s t = list_t_v slot
+
/// High-level type for the hash-map, seen as a list of associative lists (one
/// list per slot)
type hash_map_slots_s t = list (slot_s t)
@@ -306,6 +310,14 @@ 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_s t =
flatten (hash_map_t_slots_v hm)
+// TODO: move
+let is_pos_usize (n : nat) : Type0 = 0 < n /\ n <= usize_max
+
+// 'ne': "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)}
+
let hash_key (k : key) : hash =
Return?.v (hash_key_fwd k)
@@ -532,10 +544,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)
@@ -1366,33 +1378,102 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
end
end
-(*** remove_elements_from_list *)
+(*** move_elements_from_list *)
-(*
-type hash_map_slots_res (t : Type0) = res:result (hash_map_slots t){
+type hash_map_slots_s_res (t : Type0) = res:result (hash_map_slots_s t){
match res with
| Fail -> True
- | Return hm ->
- length hm <= usize_max /\
- length hm > 0
+ | Return hm -> is_pos_usize (length hm)
}
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=
+ (t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)})
+ (ls : slot_s t) :
+ Tot (hash_map_slots_s_res t) =
+ let add_elem (hm_res : hash_map_slots_s_res t) (b : binding t) :
+ hash_map_slots_s_res t =
match hm_res with
| Fail -> Fail
| Return hm ->
- hash_map_insert_no_resize_s hm
- fold_left (fun hm_res (value,key) ->
- match ls with
- | [] -> Return hm
- |
+ let (key,value) = b in
+ hash_map_insert_no_resize_s hm key value
+ in
+ fold_left add_elem (Return hm) ls
+
+/// 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))
+ (ensures (
+ match hash_map_move_elements_from_list_fwd_back t ntable ls,
+ hash_map_move_elements_from_list_s t (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_slots_v hm' == hm_v
+ | _ -> False))
+ (decreases (hash_map_move_elements_from_list_decreases t ntable ls))
+
+#push-options "--z3rlimit 100 --fuel 1"
+let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls =
+ begin match ls with
+ | ListCons k v tl ->
+ hash_map_insert_no_resize_fwd_back_lem t ntable k v;
+ begin match hash_map_insert_no_resize_fwd_back t ntable k v with
+ | Fail -> admit()
+ | Return h ->
+ 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 -> admit()
+ | Return h0 -> admit()
+ end
+ end
+ | ListNil -> ()
+ end
+#pop-options
+
+/// Refinement lemma
+val hash_map_move_elements_fwd_back_lem
+ (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
+ Lemma (requires (is_pos_usize (ntable.hash_map_num_entries)))
+ (ensures (
+ match hash_map_move_elements_fwd_back t ntable slots i,
+ hash_map_move_elements_from_list_s t ntable slots
+ with
+ | Fail ->
+ ))
+ (decreases (hash_map_move_elements_decreases t ntable slots i))
+
+let rec hash_map_move_elements_fwd_back
+ (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
+ Tot (result ((hash_map_t t) & (vec (list_t t))))
+ (decreases (hash_map_move_elements_decreases t ntable slots i))
+ =
+ let i0 = vec_len (list_t t) slots in
+ let b = i < i0 in
+ if b
+ then
+ begin match vec_index_mut_fwd (list_t t) slots i with
+ | Fail -> Fail
+ | Return l ->
+ let l0 = mem_replace_fwd (list_t t) l ListNil in
+ begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with
+ | Fail -> Fail
+ | Return h ->
+ let l1 = mem_replace_back (list_t t) l ListNil in
+ begin match vec_index_mut_back (list_t t) slots i l1 with
+ | Fail -> Fail
+ | Return v ->
+ begin match usize_add i 1 with
+ | Fail -> Fail
+ | Return i1 ->
+ begin match hash_map_move_elements_fwd_back t h v i1 with
+ | Fail -> Fail
+ | Return (h0, v0) -> Return (h0, v0)
+ end
+ end
+ end
+ end
+ end
+ else Return (ntable, slots)