diff options
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 283 |
1 files changed, 272 insertions, 11 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index a27ee34a..741d9115 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -1391,19 +1391,24 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' = (*** move_elements_from_list *) +/// Having a great time here: if we use `result (hash_map_slots_s_res t)` as the +/// return type for [hash_map_move_elements_from_list_s] instead of having this +/// awkward match, the proof of [hash_map_move_elements_fwd_back_lem] fails. +/// I guess it comes from F*'s poor subtyping. +/// Followingly, I'm not taking any change and using [result_hash_map_slots_s] +/// everywhere. +type result_hash_map_slots_s_nes (t : Type0) : Type0 = + res:result (hash_map_slots_s t) { + match res with + | Fail -> True + | Return hm -> is_pos_usize (length hm) + } + let rec hash_map_move_elements_from_list_s (#t : Type0) (hm : hash_map_slots_s_nes t) (ls : slot_s t) : - Pure (result (hash_map_slots_s t)) - (requires (True)) - (ensures (fun res -> - // Having a great time here: if we use `result (hash_map_slots_s_res t)` - // as the return type, instead of having this awkward match, the proof - // of [hash_map_move_elements_fwd_back_lem] fails. I guess it comes from - // F*'s poor subtyping. - match res with - | Fail -> True - | Return hm -> is_pos_usize (length hm))) + // Do *NOT* use `result (hash_map_slots_s t)` + Tot (result_hash_map_slots_s_nes t) (decreases ls) = match ls with | [] -> Return hm @@ -1453,13 +1458,18 @@ let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls = (*** move_elements *) +(**** move_elements: refinement 1 *) +/// We prove a first refinement lemma: calling [move_elements] refines a function +/// which, for every slot, moves the element out of the slot. This first version is +/// almost exactly the translated function, it just uses `list` instead of `list_t`. + // Note that we ignore the returned slots (we thus don't return a pair: // only the new hash map in which we moved the elements from the slots): // this returned value is not used. let rec hash_map_move_elements_s (#t : Type0) (hm : hash_map_slots_s_nes t) (slots : slots_s t) (i : usize{i <= length slots /\ length slots <= usize_max}) : - Tot (result (hash_map_slots_s_nes t)) + Tot (result_hash_map_slots_s_nes t) (decreases (length slots - i)) = let len = length slots in if i < len then @@ -1527,3 +1537,254 @@ let rec hash_map_move_elements_fwd_back_lem t ntable slots i = else () #pop-options + +(**** move_elements: refinement 2 *) +/// We prove a second refinement lemma: calling [move_elements] refines a function +/// which which moves every binding of the hash map seen as *one* associative list +/// (and not a list of lists). + +/// [ntable] is the hash map to which we move the elements +/// [slots] is the current hash map, from which we remove the elements, and seen +/// as a "flat" associative list (and not a list of lists) +/// This is actually exactly [hash_map_move_elements_from_list_s]... +let rec hash_map_move_elements_s_flat + (#t : Type0) (ntable : hash_map_slots_s_nes t) + (slots : hash_map_s t) : + Tot (result_hash_map_slots_s_nes t) + (decreases slots) = + match slots with + | [] -> Return ntable + | (k,v) :: slots' -> + match hash_map_insert_no_resize_s ntable k v with + | Fail -> Fail + | Return ntable' -> + hash_map_move_elements_s_flat ntable' slots' + +/// The refinment lemmas +/// First, auxiliary helpers. + +/// Flatten a list of lists, starting at index i +val flatten_i : + #a:Type + -> l:list (list a) + -> i:nat{i <= length l} + -> Tot (list a) (decreases (length l - i)) + +let rec flatten_i l i = + if i < length l then + index l i @ flatten_i l (i+1) + else [] + +let _ = assert(let l = [1;2] in l == hd l :: tl l) + +val flatten_i_incr : + #a:Type + -> l:list (list a) + -> i:nat{Cons? l /\ i+1 <= length l} -> + Lemma + (ensures ( + (**) assert_norm(length (hd l :: tl l) == 1 + length (tl l)); + flatten_i l (i+1) == flatten_i (tl l) i)) + (decreases (length l - (i+1))) + +#push-options "--fuel 1" +let rec flatten_i_incr l i = + let x :: tl = l in + if i + 1 < length l then + begin + assert(flatten_i l (i+1) == index l (i+1) @ flatten_i l (i+2)); + flatten_i_incr l (i+1); + assert(flatten_i l (i+2) == flatten_i tl (i+1)); + assert(index l (i+1) == index tl i) + end + else () +#pop-options + +val flatten_0_is_flatten : + #a:Type + -> l:list (list a) -> + Lemma + (ensures (flatten_i l 0 == flatten l)) + +#push-options "--fuel 1" +let rec flatten_0_is_flatten #a l = + match l with + | [] -> () + | x :: l' -> + flatten_i_incr l 0; + flatten_0_is_flatten l' +#pop-options + +/// Auxiliary lemma +val flatten_nil_prefix_as_flatten_i : + #a:Type + -> l:list (list a) + -> i:nat{i <= length l} -> + Lemma (requires (forall (j:nat{j < i}). index l j == [])) + (ensures (flatten l == flatten_i l i)) + +#push-options "--fuel 1" +let rec flatten_nil_prefix_as_flatten_i #a l i = + if i = 0 then flatten_0_is_flatten l + else + begin + let x :: l' = l in + assert(index l 0 == []); + assert(x == []); + assert(flatten l == flatten l'); + flatten_i_incr l (i-1); + assert(flatten_i l i == flatten_i l' (i-1)); + assert(forall (j:nat{j < length l'}). index l' j == index l (j+1)); + flatten_nil_prefix_as_flatten_i l' (i-1); + assert(flatten l' == flatten_i l' (i-1)) + end +#pop-options + +/// The proof is trivial, the functions are the same. +/// Just keeping two definitions to allow changes... +val hash_map_move_elements_from_list_s_as_flat_lem + (#t : Type0) (hm : hash_map_slots_s_nes t) + (ls : slot_s t) : + Lemma + (ensures ( + hash_map_move_elements_from_list_s hm ls == + hash_map_move_elements_s_flat hm ls)) + (decreases ls) + +#push-options "--fuel 1" +let rec hash_map_move_elements_from_list_s_as_flat_lem #t hm ls = + match ls with + | [] -> () + | (key, value) :: ls' -> + match hash_map_insert_no_resize_s hm key value with + | Fail -> () + | Return hm' -> + hash_map_move_elements_from_list_s_as_flat_lem hm' ls' +#pop-options + +/// Composition of two calls to [hash_map_move_elements_s_flat] +let hash_map_move_elements_s_flat_comp + (#t : Type0) (hm : hash_map_slots_s_nes t) (slot0 slot1 : slot_s t) : + Tot (result_hash_map_slots_s_nes t) = + match hash_map_move_elements_s_flat hm slot0 with + | Fail -> Fail + | Return hm1 -> hash_map_move_elements_s_flat hm1 slot1 + +/// High-level desc: +/// move_elements (move_elements hm slot0) slo1 == move_elements hm (slot0 @ slot1) +val hash_map_move_elements_s_flat_append_lem + (#t : Type0) (hm : hash_map_slots_s_nes t) (slot0 slot1 : slot_s t) : + Lemma + (ensures ( + match hash_map_move_elements_s_flat_comp hm slot0 slot1, + hash_map_move_elements_s_flat hm (slot0 @ slot1) + with + | Fail, Fail -> True + | Return hm1, Return hm2 -> hm1 == hm2 + | _ -> False)) + (decreases (slot0)) + +#push-options "--fuel 1" +let rec hash_map_move_elements_s_flat_append_lem #t hm slot0 slot1 = + match slot0 with + | [] -> () + | (k,v) :: slot0' -> + match hash_map_insert_no_resize_s hm k v with + | Fail -> () + | Return hm' -> + hash_map_move_elements_s_flat_append_lem hm' slot0' slot1 +#pop-options + +val flatten_i_same_suffix (#a : Type) (l0 l1 : list (list a)) (i : nat) : + Lemma + (requires ( + i <= length l0 /\ + length l0 = length l1 /\ + (forall (j:nat{i <= j /\ j < length l0}). index l0 j == index l1 j))) + (ensures (flatten_i l0 i == flatten_i l1 i)) + +let rec flatten_i_same_suffix #a l0 l1 i = admit() + +/// Refinement lemma: +/// [hash_map_move_elements_s] refines [hash_map_move_elements_s_flat] +val hash_map_move_elements_s_flat_lem + (#t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)}) + (slots : slots_s t) + (i : nat{i <= length slots /\ length slots <= usize_max}) : + Lemma + (ensures ( + match hash_map_move_elements_s hm slots i, + hash_map_move_elements_s_flat hm (flatten_i slots i) + with + | Fail, Fail -> True + | Return hm, Return hm' -> hm == hm' + | _ -> False)) + (decreases (length slots - i)) + +#push-options "--fuel 1" +let rec hash_map_move_elements_s_flat_lem #t hm slots i = + let len = length slots in + if i < len then + begin + let slot = index slots i in + hash_map_move_elements_from_list_s_as_flat_lem hm slot; + match hash_map_move_elements_from_list_s hm slot with + | Fail -> + assert(flatten_i slots i == slot @ flatten_i slots (i+1)); + hash_map_move_elements_s_flat_append_lem hm slot (flatten_i slots (i+1)); + assert(hash_map_move_elements_s_flat hm (flatten_i slots i) == Fail) + | Return hm' -> + let slots' = list_update slots i [] in + flatten_i_same_suffix slots slots' (i+1); + hash_map_move_elements_s_flat_lem hm' slots' (i+1); + hash_map_move_elements_s_flat_append_lem hm slot (flatten_i slots' (i+1)); + () + end + else () +#pop-options + +(* + +/// [nhm]: the new hash map (in which we insert elements) +/// [slot]: the current slot we are emptying +/// [ohm]: the old hash map, which we are moving to [nhm] +/// [i]: the index of [slot] in [ohm] +val hash_map_move_elements_s_flat_lem + (#t : Type0) (nhm : hash_map_slots_s t{is_pos_usize (length hm)}) + (slots : slots_s t) + (i : nat{i <= length slots /\ length slots <= usize_max}) : + Lemma + (requires ( + index ohm i == slot /\ + (forall (j:nat{j < i}). index j ohm == []))) + (ensures ( + match hash_map_move_elements_from_list_s + +let rec hash_map_move_elements_from_list_s + (#t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)}) + (ls : slot_s t) : + Tot (hash_map_slots_s_nes t) (decreases ls) = + match ls with + | [] -> Return hm + | (key, value) :: ls' -> + match hash_map_insert_no_resize_s hm key value with + | Fail -> Fail + | Return hm' -> + hash_map_move_elements_from_list_s hm' ls' + +let rec hash_map_move_elements_s + (#t : Type0) (hm : hash_map_slots_s_nes t) + (slots : slots_s t) (i : usize{i <= length slots /\ length slots <= usize_max}) : + Tot (result (hash_map_slots_s_nes t)) + (decreases (length slots - i)) = + let len = length slots in + if i < len then + begin + let slot = index slots i in + match hash_map_move_elements_from_list_s hm slot with + | Fail -> Fail + | Return hm' -> + let slots' = list_update slots i [] in + hash_map_move_elements_s hm' slots' (i+1) + end + else Return hm |