summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2022-02-12 01:35:01 +0100
committerSon Ho2022-02-12 01:35:01 +0100
commit527c55e1182fe14c5615b219c896266129419e19 (patch)
treeef86e8a8ac9ad6b27138f12293c53b3373e8f6d3 /tests
parent9c7d6bbe727a959cd5f6eb8e35b8562fe06f3924 (diff)
Prove the refinment lemma for move_elements
Diffstat (limited to 'tests')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst78
1 files changed, 43 insertions, 35 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 8c36cec9..577398fd 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -282,11 +282,6 @@ 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
-/// Representation function for the slots.
-/// TODO: remove?
-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)
@@ -295,6 +290,14 @@ type slots_s (t : Type0) = list (slot_s t)
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
+/// Representation function for the slots.
+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)
type hash_map_slots_s t = list (slot_s t)
@@ -582,20 +585,20 @@ val slots_t_all_nil_inv_lem
let slots_t_all_nil_inv_lem #t slots = ()
#pop-options
-val slots_t_v_all_nil_is_empty_lem
+val slots_t_al_v_all_nil_is_empty_lem
(#t : Type0) (slots : vec (list_t t)) :
Lemma (requires (forall (i:nat{i < length slots}). index slots i == ListNil))
- (ensures (slots_t_v slots == []))
+ (ensures (slots_t_al_v slots == []))
#push-options "--fuel 1"
-let rec slots_t_v_all_nil_is_empty_lem #t slots =
+let rec slots_t_al_v_all_nil_is_empty_lem #t slots =
match slots with
| [] -> ()
| s :: slots' ->
assert(forall (i:nat{i < length slots'}). index slots' i == index slots (i+1));
- slots_t_v_all_nil_is_empty_lem #t slots';
- assert(slots_t_v slots == list_t_v s @ slots_t_v slots');
- assert(slots_t_v slots == list_t_v s);
+ slots_t_al_v_all_nil_is_empty_lem #t slots';
+ assert(slots_t_al_v slots == list_t_v s @ slots_t_al_v slots');
+ assert(slots_t_al_v slots == list_t_v s);
assert(index slots 0 == ListNil)
#pop-options
@@ -708,7 +711,7 @@ let hash_map_new_fwd_lem_fun t =
match hash_map_new_with_capacity_fwd t 32 4 5 with
| Fail -> ()
| Return hm ->
- slots_t_v_all_nil_is_empty_lem hm.hash_map_slots
+ slots_t_al_v_all_nil_is_empty_lem hm.hash_map_slots
#pop-options
(*** clear_slots *)
@@ -779,7 +782,7 @@ let hash_map_clear_fwd_back_lem_fun t self =
begin match hash_map_clear_slots_fwd_back t v 0 with
| Fail -> ()
| Return slots1 ->
- slots_t_v_all_nil_is_empty_lem slots1;
+ slots_t_al_v_all_nil_is_empty_lem slots1;
let hm1 = Mkhash_map_t 0 p i slots1 in
assert(hash_map_t_base_inv hm1);
assert(hash_map_t_inv hm1);
@@ -1466,52 +1469,57 @@ let rec hash_map_move_elements_s
end
else Return hm
-(*
-val hash_map_move_elements_fwd_back
+val hash_map_move_elements_fwd_back_lem
(t : Type0) (ntable : hash_map_t t)
- (slots : vec (list_t t)) (i : usize{i <= length ntable.hash_map_slots}) :
- Lemma (requires (hash_map_t_inv ntable))
+ (slots : vec (list_t t)) (i : usize{i <= length slots}) :
+ Lemma
+ (requires (
+ hash_map_t_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 hm, Return hm_v ->
- hash_map_t_inv hm /\
- hash_map_t_slots_v hm))
-
- Tot (result ((hash_map_t t) & (vec (list_t t))))
- (decreases (hash_map_move_elements_decreases t ntable slots i))
+ | Return (ntable', _), Return ntable'_v ->
+ hash_map_t_inv ntable' /\
+ hash_map_t_slots_v ntable' == ntable'_v
+ | _ -> False))
+ (decreases (length 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))
- =
+#restart-solver
+#push-options "--z3rlimit 200 --fuel 1"
+let rec hash_map_move_elements_fwd_back_lem t ntable slots i =
+ assert(hash_map_t_inv ntable);
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
+ | Fail -> ()
| Return l ->
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 with
- | Fail -> Fail
+ | Fail -> ()
| Return h ->
let l1 = mem_replace_back (list_t t) l ListNil in
+ assert(l1 == ListNil);
begin match vec_index_mut_back (list_t t) slots i l1 with
- | Fail -> Fail
+ | Fail -> ()
| Return v ->
begin match usize_add i 1 with
- | Fail -> Fail
+ | Fail -> ()
| Return i1 ->
+ hash_map_move_elements_fwd_back_lem t h v i1;
begin match hash_map_move_elements_fwd_back t h v i1 with
- | Fail -> Fail
- | Return (h0, v0) -> Return (h0, v0)
+ | Fail -> ()
+ | Return (h0, v0) -> ()
end
end
end
end
end
- else Return (ntable, slots)
+ else ()
+#pop-options
+